From a652dac0a817922b6fbe6b44f528120fc6d72355 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Fri, 27 Feb 2026 17:13:35 +0000 Subject: [PATCH] Fix inconsistencies with `implies` operator (#549) - Defines `Expr.Bool.implies` using the `Implies` constructor - Makes `Typed.Bool.implies` use `Expr.Bool.implies` Closes #549 --- src/smtml/expr.ml | 2 ++ src/smtml/expr_intf.ml | 3 +++ src/smtml/expr_raw.ml | 2 ++ src/smtml/typed.ml | 2 +- 4 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 9a0c454e..70a8a72d 100644 --- a/src/smtml/expr.ml +++ b/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 diff --git a/src/smtml/expr_intf.ml b/src/smtml/expr_intf.ml index 1ecf754b..82b7034a 100644 --- a/src/smtml/expr_intf.ml +++ b/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 diff --git a/src/smtml/expr_raw.ml b/src/smtml/expr_raw.ml index aa1d511b..e28b1654 100644 --- a/src/smtml/expr_raw.ml +++ b/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 diff --git a/src/smtml/typed.ml b/src/smtml/typed.ml index fbf90cd4..33c3f3b6 100644 --- a/src/smtml/typed.ml +++ b/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