From 91dc8c3016eb234415d2abc7f8b9a9b9d6520e18 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Fri, 27 Feb 2026 17:55:30 +0000 Subject: [PATCH] Add n-ary `distinct` operator (#553) Closes #553 --- src/smtml/feature_extraction.ml | 1 + src/smtml/mappings.ml | 1 + src/smtml/ty.ml | 8 ++++++-- src/smtml/ty.mli | 1 + src/smtml/typed.ml | 5 +++++ src/smtml/typed.mli | 4 ++++ test/integration/test_solver.ml | 22 ++++++++++++++++++++++ 7 files changed, 40 insertions(+), 2 deletions(-) diff --git a/src/smtml/feature_extraction.ml b/src/smtml/feature_extraction.ml index 0d0cfef5..d40b69ed 100644 --- a/src/smtml/feature_extraction.ml +++ b/src/smtml/feature_extraction.ml @@ -149,6 +149,7 @@ let string_of_naryop (naryop : Ty.Naryop.t) : string = | Logor -> "Logor" | Concat -> "Concat" | Regexp_union -> "Regexp_union" + | Distinct -> "Distinct" let string_of_expr_kind (e : Expr.expr) _ty : string = match e with diff --git a/src/smtml/mappings.ml b/src/smtml/mappings.ml index b8f66a82..1a921d18 100644 --- a/src/smtml/mappings.ml +++ b/src/smtml/mappings.ml @@ -105,6 +105,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct match op with | Naryop.Logand -> M.logand l | Logor -> M.logor l + | Distinct -> M.distinct l | _ -> Fmt.failwith {|Bool: Unsupported n-ary operator "%a"|} Naryop.pp op diff --git a/src/smtml/ty.ml b/src/smtml/ty.ml index c4bcf213..44a3a6ca 100644 --- a/src/smtml/ty.ml +++ b/src/smtml/ty.ml @@ -627,6 +627,7 @@ module Naryop = struct | Logor | Concat | Regexp_union + | Distinct [@@deriving ord] let hash = function @@ -634,21 +635,24 @@ module Naryop = struct | Logor -> 1 | Concat -> 2 | Regexp_union -> 3 + | Distinct -> 4 let equal op1 op2 = match (op1, op2) with | Logand, Logand | Logor, Logor | Concat, Concat - | Regexp_union, Regexp_union -> + | Regexp_union, Regexp_union + | Distinct, Distinct -> true - | (Logand | Logor | Concat | Regexp_union), _ -> false + | (Logand | Logor | Concat | Regexp_union | Distinct), _ -> false let pp fmt = function | Logand -> Fmt.string fmt "and" | Logor -> Fmt.string fmt "or" | Concat -> Fmt.string fmt "++" | Regexp_union -> Fmt.string fmt "union" + | Distinct -> Fmt.string fmt "distinct" end module Smtlib = struct diff --git a/src/smtml/ty.mli b/src/smtml/ty.mli index bd868675..89a79a0a 100644 --- a/src/smtml/ty.mli +++ b/src/smtml/ty.mli @@ -280,6 +280,7 @@ module Naryop : sig | Logor (** Logical OR. *) | Concat (** Concatenation. *) | Regexp_union (** Union of regular expressions. *) + | Distinct [@@deriving ord] val hash : t -> int diff --git a/src/smtml/typed.ml b/src/smtml/typed.ml index 33c3f3b6..c4a429ad 100644 --- a/src/smtml/typed.ml +++ b/src/smtml/typed.ml @@ -482,6 +482,11 @@ module Bool = struct let[@inline] eq (a : 'a expr) (b : 'a expr) = Expr.relop Types.bool Eq a b + let[@inline] distinct (es : 'a expr list) = + (* Typically this encodes a symbolic constraint: (distinct x y z), so no + need to waste time trying to simplify. Just use `raw_naryop`. *) + Expr.raw_naryop Types.bool Distinct es + let[@inline] ite c (r1 : 'a expr) (r2 : 'a expr) : 'a expr = Expr.triop Types.bool Ite c r1 r2 diff --git a/src/smtml/typed.mli b/src/smtml/typed.mli index da1ca8d8..0a143a50 100644 --- a/src/smtml/typed.mli +++ b/src/smtml/typed.mli @@ -127,6 +127,10 @@ module Bool : sig (** [eq t1 t2] returns true if [t1] and [t2] are structurally equal. *) val eq : 'a expr -> 'a expr -> t + (** [distinct es] returns true if all expressions in the list [es] are + pair-wise distinct. *) + val distinct : 'a expr list -> t + (** [ite cond then_ else_] constructs an if-then-else expression. Returns [then_] if [cond] evaluates to true, and [else_] otherwise. *) val ite : t -> 'a expr -> 'a expr -> 'a expr diff --git a/test/integration/test_solver.ml b/test/integration/test_solver.ml index 1ef2958a..328b05cd 100644 --- a/test/integration/test_solver.ml +++ b/test/integration/test_solver.ml @@ -111,6 +111,27 @@ module Make (M : Mappings_intf.S_with_fresh) = struct let val_x = Option.bind model (fun m -> Model.evaluate m symbol_x) in assert (match val_x with Some v -> Value.equal v (Int 5) | None -> false) + let test_distinct solver_module = + let open Typed in + let module Solver = (val solver_module : Solver_intf.S) in + let solver = Solver.create ~logic:LIA () in + let x = symbol Types.int "x" in + let y = symbol Types.int "y" in + let z = symbol Types.int "z" in + Solver.add solver [ (Bool.distinct [ x; y; z ] :> Expr.t) ]; + Solver.add solver [ (Bool.eq x (Int.v 1) :> Expr.t) ]; + Solver.add solver [ (Bool.eq y (Int.v 1) :> Expr.t) ]; + assert_unsat ~f:"test_distinct_unsat" (Solver.check solver []); + Solver.reset solver; + let x = symbol Types.int "x" in + let y = symbol Types.int "y" in + let z = symbol Types.int "z" in + Solver.add solver [ (Bool.distinct [ x; y; z ] :> Expr.t) ]; + Solver.add solver [ (Bool.eq x (Int.v 1) :> Expr.t) ]; + Solver.add solver [ (Bool.eq y (Int.v 2) :> Expr.t) ]; + Solver.add solver [ (Bool.eq z (Int.v 3) :> Expr.t) ]; + assert_sat ~f:"test_distinct_sat" (Solver.check solver []) + let test_lia_1 solver_module = let open Infix in let module Solver = (val solver_module : Solver_intf.S) in @@ -123,6 +144,7 @@ module Make (M : Mappings_intf.S_with_fresh) = struct "test_lia" >::: [ "test_lia_0" >:: with_solver test_lia_0 ; "test_lia_1" >:: with_solver test_lia_1 + ; "test_distinct" >:: with_solver test_distinct ] let test_lra =