Fix distinct unsoundness

This PR quickly fixes the clash between the SMT-LIB specification of
`distinct` and the implementation of this expression in AE.

Basically, we expand the expression `distinct x_1 ... x_n` into a
conjunction of binary disequalities.

Notice that the model outputted for `uf2.models.smt2` changes because I don't
preserve the old order used in `distinct`.

This fix doesn't change the smart constructor `mk_distinct`. We shouldn't
change the API on the branch v2.5.x and I add a comment to advertise the user
that this smart constructor doesn't behave as expected.

src/lib/frontend/cnf.ml

@@ -239,9 +239,29 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
           let res = make_term up_qv name_base t in
           if negated then E.neg res else res
 
-        | TAneq lt | TAdistinct lt ->
+        | TAneq lt ->
           let lt = List.map (make_term up_qv name_base) lt in
           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
+
         | TAle [t1;t2] ->
           E.mk_builtin ~is_pos:true Sy.LE
             [make_term up_qv name_base t1;

src/lib/frontend/d_cnf.ml

@@ -1337,7 +1337,23 @@ let rec mk_expr
             end
 
           | B.Distinct, _ ->
-            E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args)
+            (* 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
 
           | B.Constructor _, _ ->
             let name = get_basename path in

src/lib/structures/expr.mli

@@ -204,6 +204,11 @@ 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 *)

tests/dune.inc

@@ -170928,6 +170928,258 @@
 
 ; Auto-generated part begin
 (subdir issues
+  (rule
+   (target 889_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        889.expected
+        889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        889.expected
+        889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 889_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        889.expected
+        889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 889_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 889_cdcl.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_cdcl.output)))
+  (rule
+   (target 889_tableaux_cdcl.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_tableaux_cdcl.output)))
+  (rule
+   (target 889_tableaux.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_tableaux.output)))
+  (rule
+   (target 889_legacy.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend legacy
+             --timelimit=2
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_legacy.output)))
+  (rule
+   (target 889_dolmen.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --timelimit=2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_dolmen.output)))
+  (rule
+   (target 889_fpa.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --timelimit=2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_fpa.output)))
   (rule
    (target 777.models_tableaux.output)
    (deps (:input 777.models.smt2))

tests/issues/889.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/issues/889.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+(assert (not (distinct a b c)))
+(assert (distinct a b))
+(check-sat)

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 0)
-  (define-fun b () Int (- 2))
+  (define-fun a () Int (- 2))
+  (define-fun b () Int 0)
 )