diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 2968d9f2f9..8d14c7b2f1 100644 --- a/src/lib/frontend/cnf.ml +++ b/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; diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index c63843a789..ef840ffc51 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1337,7 +1337,22 @@ 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 diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 2c24945573..009a678f3e 100644 --- a/src/lib/structures/expr.mli +++ b/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 *) diff --git a/tests/dune.inc b/tests/dune.inc index 7b08eee9be..d7e9cbbf10 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -178731,6 +178731,270 @@ ; 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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --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} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --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)) diff --git a/tests/issues/889.expected b/tests/issues/889.expected new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/issues/889.smt2 b/tests/issues/889.smt2 new file mode 100644 index 0000000000..1b9e8063a9 --- /dev/null +++ b/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)