Don't hc bool values unecessarily

lib/expr.ml

@@ -345,12 +345,10 @@ let triop' (ty : Ty.t) (op : triop) (e1 : t) (e2 : t) (e3 : t) : t =
 [@@inline]
 
 let triop ty (op : triop) (e1 : t) (e2 : t) (e3 : t) : t =
-  match (view e1, view e2, view e3) with
-  | Val v1, Val v2, Val v3 -> value (Eval.triop ty op v1 v2 v3)
-  | Val v, _, _ -> (
-    match op with
-    | Ite -> ( match v with True -> e2 | False -> e3 | _ -> assert false )
-    | _ -> triop' ty op e1 e2 e3 )
+  match (op, view e1, view e2, view e3) with
+  | Ite, Val True, _, _ -> e2
+  | Ite, Val False, _, _ -> e3
+  | op, Val v1, Val v2, Val v3 -> value (Eval.triop ty op v1 v2 v3)
   | _ -> triop' ty op e1 e2 e3
 
 let relop' (ty : Ty.t) (op : relop) (hte1 : t) (hte2 : t) : t =
@@ -515,41 +513,44 @@ module Bool = struct
     | Val False -> Some false
     | _ -> None
 
-  let v b = make (match b with true -> Val True | false -> Val False)
+  let true_ = value True
+
+  let false_ = value False
+
+  let to_val b = if b then true_ else false_
 
-  let not (b : t) =
-    match of_val (view b) with
-    | Some b -> v (not b)
+  let not_ (b : t) =
+    let bexpr = view b in
+    match of_val bexpr with
+    | Some b -> to_val (not b)
     | None -> (
-      match view b with
+      match bexpr with
       | Unop (Ty_bool, Not, cond) -> cond
-      | _ -> unop' Ty_bool Not b )
+      | _ -> unop Ty_bool Not b )
 
-  let ( = ) (b1 : t) (b2 : t) =
+  let equal (b1 : t) (b2 : t) =
     match (view b1, view b2) with
-    | Val True, Val True | Val False, Val False -> value True
-    | _ -> relop' Ty_bool Eq b1 b2
+    | Val True, Val True | Val False, Val False -> true_
+    | _ -> relop Ty_bool Eq b1 b2
 
   let distinct (b1 : t) (b2 : t) =
     match (view b1, view b2) with
-    | Val True, Val False | Val False, Val True -> value True
-    | _ -> relop' Ty_bool Ne b1 b2
+    | Val True, Val False | Val False, Val True -> true_
+    | _ -> relop Ty_bool Ne b1 b2
 
   let and_ (b1 : t) (b2 : t) =
     match (of_val (view b1), of_val (view b2)) with
-    | Some b1, Some b2 -> v (b1 && b2)
     | Some true, _ -> b2
     | _, Some true -> b1
-    | Some false, _ | _, Some false -> value False
-    | _ -> binop' Ty_bool And b1 b2
+    | Some false, _ | _, Some false -> false_
+    | _ -> binop Ty_bool And b1 b2
 
   let or_ (b1 : t) (b2 : t) =
     match (of_val (view b1), of_val (view b2)) with
-    | Some b1, Some b2 -> v (b1 || b2)
     | Some false, _ -> b2
     | _, Some false -> b1
-    | Some true, _ | _, Some true -> value True
-    | _ -> binop' Ty_bool Or b1 b2
+    | Some true, _ | _, Some true -> true_
+    | _ -> binop Ty_bool Or b1 b2
 
   let ite (c : t) (r1 : t) (r2 : t) = triop Ty_bool Ite c r1 r2
 end

lib/expr.mli

@@ -131,11 +131,13 @@ module Hc : sig
 end
 
 module Bool : sig
-  val v : bool -> t
+  val true_ : t
 
-  val not : t -> t
+  val false_ : t
 
-  val ( = ) : t -> t -> t
+  val not_ : t -> t
+
+  val equal : t -> t -> t
 
   val distinct : t -> t -> t
 

test/unit/test_expr_hc.ml

@@ -1,6 +1,9 @@
 open Smtml
 open Expr
 
+(* We already have some hc exprs in the table *)
+let length0 = Expr.Hc.length ()
+
 let () =
   let module I32 = Expr.Bitv.I32 in
   assert (I32.sym "x" == I32.sym "x");
@@ -13,9 +16,9 @@ let () =
   let b = binop (Ty_bitv 32) Add left_b right_b in
   assert (a == b);
   (*
-     There should be only 3 elements in the hashcons table:
+     There should be only 3 elements added in the hashcons table:
        1. x
        2. y
        3. x + y
   *)
-  assert (Expr.Hc.length () == 3)
+  assert (Expr.Hc.length () - length0 == 3)

test/unit/test_relop.ml

@@ -97,7 +97,11 @@ let () =
 
 (* app *)
 let () =
-  assert (relop Ty_app Eq (app (`Op "undefined") []) (app (`Op "undefined") []) = value True);
-  assert (relop Ty_app Ne (app (`Op "undefined") []) (app (`Op "undefined") []) = value False);
+  assert (
+    relop Ty_app Eq (app (`Op "undefined") []) (app (`Op "undefined") [])
+    = value True );
+  assert (
+    relop Ty_app Ne (app (`Op "undefined") []) (app (`Op "undefined") [])
+    = value False );
   assert (relop Ty_app Eq (app (`Op "undefined") []) (int 1) = value False);
-  assert (relop Ty_app Eq (int 1) (app (`Op "undefined") []) = value False)
+  assert (relop Ty_app Eq (int 1) (app (`Op "undefined") []) = value False)

test/unit/test_simplify.ml

@@ -13,7 +13,7 @@ let () =
     let binary = binop' (Ty_bitv 32) Add (I32.v 1l) (I32.v 1l) in
     simplify binary = I32.v 2l );
   assert (
-    let triop = triop' Ty_bool Ite (Bool.v true) (I32.v 1l) (I32.v 0l) in
+    let triop = triop' Ty_bool Ite Bool.true_ (I32.v 1l) (I32.v 0l) in
     simplify triop = I32.v 1l );
   assert (
     let relop = relop' (Ty_bitv 32) Lt (I32.v 2l) (I32.v 1l) in