From 64ad84152b544cf9c98757bc6e90d4149c563d5b Mon Sep 17 00:00:00 2001 From: Pierrot Date: Mon, 16 Oct 2023 10:55:20 +0200 Subject: [PATCH] Fix distinct unsoundness (#890) * 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`. * Fix the smart constructor of `mk_distinct` The smart construct `mk_distinct` produces an SMT-LIB compliant expression. * Clean up --- src/lib/structures/expr.ml | 19 ++- tests/dune.inc | 252 +++++++++++++++++++++++++++++++++++++ tests/issues/889.expected | 2 + tests/issues/889.smt2 | 7 ++ 4 files changed, 276 insertions(+), 4 deletions(-) create mode 100644 tests/issues/889.expected create mode 100644 tests/issues/889.smt2 diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index fc816cd14..53adde375 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1210,10 +1210,21 @@ 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 hot fix makes sure that the smart constructor agrees with + the usual semantic of distinct when used with at least 3 arguments. + To prevent a soundness bug, we translate the expected expression into a + conjonction of binary disequations. + See issue: https://github.com/OCamlPro/alt-ergo/issues/889 *) + 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/tests/dune.inc b/tests/dune.inc index 2b26613f9..c794bd6e6 100644 --- a/tests/dune.inc +++ b/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)) diff --git a/tests/issues/889.expected b/tests/issues/889.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/889.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/889.smt2 b/tests/issues/889.smt2 new file mode 100644 index 000000000..1b9e8063a --- /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)