Fix inconsistencies with implies operator (#549)

src/smtml/expr.ml

@@ -701,6 +701,8 @@ module Bool = struct
     | Some true, _ | _, Some true -> true_
     | _ -> binop Ty_bool Or b1 b2
 
+  let implies a b = binop Ty_bool Implies a b
+
   let ite c r1 r2 = triop Ty_bool Ite c r1 r2
 end
 

src/smtml/expr_intf.ml

@@ -347,6 +347,9 @@ module type S = sig
     (** [or_ expr1 expr2] constructs a logical OR expression. *)
     val or_ : t -> t -> t
 
+    (** [implies expr1 expr2] constructs a logical implication. *)
+    val implies : t -> t -> t
+
     (** [ite cond then_ else_] constructs an if-then-else expression. *)
     val ite : t -> t -> t -> t
   end

src/smtml/expr_raw.ml

@@ -39,5 +39,7 @@ module Bool = struct
 
   let or_ a b = raw_binop Ty_bool Or a b
 
+  let implies a b = raw_binop Ty_bool Implies a b
+
   let ite a b c = raw_triop Ty_bool Ite a b c
 end

src/smtml/typed.ml

@@ -478,7 +478,7 @@ module Bool = struct
 
   let[@inline] xor a b = Expr.binop Types.bool Xor a b
 
-  let[@inline] implies a b = or_ (not a) b
+  let[@inline] implies a b = Expr.Bool.implies a b
 
   let[@inline] eq (a : 'a expr) (b : 'a expr) = Expr.relop Types.bool Eq a b