From c55c0864cf122c5cabfe7241f34e26957111eb3f Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Fri, 13 Oct 2023 18:20:36 +0200
Subject: [PATCH] Fix the smart constructor of `mk_distinct`

The smart construct `mk_distinct` produces an SMT-LIB compliant
expression.
---
 src/lib/frontend/cnf.ml             | 18 +-----------------
 src/lib/frontend/d_cnf.ml           | 18 +-----------------
 src/lib/structures/expr.ml          | 18 ++++++++++++++----
 src/lib/structures/expr.mli         |  5 -----
 tests/models/uf/uf2.models.expected |  4 ++--
 5 files changed, 18 insertions(+), 45 deletions(-)

diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml
index 8d14c7b2f..b650ccf56 100644
--- a/src/lib/frontend/cnf.ml
+++ b/src/lib/frontend/cnf.ml
@@ -244,23 +244,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
           E.mk_distinct ~iff:true lt
 
         | TAdistinct lt ->
-          (* The current implementation of the distinct expression in
-             Expr clashes with the SMT-LIB specification when used with
-             at least 3 arguments. To prevent a soundness bug, we
-             translate the expected expression into a conjonction
-             of disequations of size 2. *)
-          let args = Array.of_list lt in
-          let acc = ref E.vrai in
-          for i = 0 to Array.length args - 1 do
-            for j = i + 1 to Array.length args - 1 do
-              acc :=
-                E.(mk_and
-                     (mk_distinct ~iff:true
-                        [make_term up_qv name_base args.(i);
-                         make_term up_qv name_base args.(j)]) !acc false)
-            done;
-          done;
-          !acc
+          E.mk_distinct ~iff:true (List.map (make_term up_qv name_base) lt)
 
         | TAle [t1;t2] ->
           E.mk_builtin ~is_pos:true Sy.LE
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 8e9571065..328c94a6e 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1337,23 +1337,7 @@ let rec mk_expr
             end
 
           | B.Distinct, _ ->
-            (* The current implementation of the distinct expression in
-               Expr clashes with the SMT-LIB specification when used with
-               at least 3 arguments. To prevent a soundness bug, we
-               translate the expected expression into a conjonction
-               of disequations of size 2. *)
-            let args = Array.of_list args in
-            let acc = ref E.vrai in
-            for i = 0 to Array.length args - 1 do
-              for j = i + 1 to Array.length args - 1 do
-                acc :=
-                  E.(mk_and
-                       (mk_distinct ~iff:true
-                          [aux_mk_expr args.(i); aux_mk_expr args.(j)])
-                       !acc false)
-              done;
-            done;
-            !acc
+            E.mk_distinct ~iff:true (List.map aux_mk_expr args)
 
           | B.Constructor _, _ ->
             let name = get_basename path in
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index fc816cd14..5dc0d89bb 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1210,10 +1210,20 @@ let mk_nary_eq l =
   with Exit ->
     vrai
 
-let mk_distinct ~iff tl =
-  match tl with
-  | [a; b] -> neg (mk_eq ~iff a b)
-  | _ -> neg (mk_nary_eq tl)
+let mk_distinct ~iff args =
+  (* This fix makes sure that the smart constructor agrees with
+     the SMT-LIB specification when used with at least 3 arguments.
+     To prevent a soundness bug, we translate the expected expression into a
+     conjonction of binary disequations. *)
+  let args = Array.of_list args in
+  let acc = ref vrai in
+  for i = 0 to Array.length args - 1 do
+    for j = i + 1 to Array.length args - 1 do
+      acc :=
+        mk_and (neg (mk_eq ~iff args.(i) args.(j))) !acc false
+    done;
+  done;
+  !acc
 
 let mk_builtin ~is_pos n l =
   let pos =
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 009a678f3..2c2494557 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -204,11 +204,6 @@ val pred : t -> t
 
 val mk_eq : iff:bool -> t -> t -> t
 val mk_distinct : iff:bool -> t list -> t
-(** [mk_distinct [t_1; ...; t_n]] produces the expression:
-      t_1 <> t_2 /\ t_2 <> t_3 /\ ... /\ t_(n-1) <> t_n.
-    WARNING: this smart constructor doesn't build the SMT-LIB expression
-     distinct! *)
-
 val mk_builtin : is_pos:bool -> Symbols.builtin -> t list -> t
 
 (** simple smart constructors for formulas *)
diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected
index fe82a1338..3c1182254 100644
--- a/tests/models/uf/uf2.models.expected
+++ b/tests/models/uf/uf2.models.expected
@@ -2,6 +2,6 @@
 unknown
 (
   (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 2 0))
-  (define-fun a () Int (- 2))
-  (define-fun b () Int 0)
+  (define-fun a () Int 0)
+  (define-fun b () Int (- 2))
 )