Add n-ary distinct operator (#553)

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

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
 

src/smtml/ty.ml

@@ -627,28 +627,32 @@ module Naryop = struct
     | Logor
     | Concat
     | Regexp_union
+    | Distinct
   [@@deriving ord]
 
   let hash = function
     | Logand -> 0
     | 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

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

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
 

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

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 =