Add Expr_raw module that only builds unsimplified expressions

Author: filipeom

src/smtml/Expr_raw.ml

@@ -0,0 +1,39 @@
+include Expr
+
+let unop = raw_unop
+
+let binop = raw_binop
+
+let triop = raw_triop
+
+let relop = raw_relop
+
+let cvtop = raw_cvtop
+
+let naryop = raw_naryop
+
+let extract ~high ~low = raw_extract ~high ~low
+
+let concat = raw_concat
+
+let simplify = Fun.id
+
+module Bool = struct
+  let true_ = Bool.true_
+
+  let false_ = Bool.false_
+
+  let v = Bool.v
+
+  let not a = raw_unop Ty_bool Not a
+
+  let equal a b = raw_relop Ty_bool Eq a b
+
+  let distinct a b = raw_relop Ty_bool Ne a b
+
+  let and_ a b = raw_binop Ty_bool And a b
+
+  let or_ a b = raw_binop Ty_bool Or a b
+
+  let ite a b c = raw_triop Ty_bool Ite a b c
+end

src/smtml/dune

@@ -24,6 +24,7 @@
   dolmenexpr_to_expr
   eval
   expr
+  expr_raw
   interpret
   interpret_intf
   lexer