From e81c18a693f46cd780a99bf27c8c5fad8e5ef77f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 13 Oct 2023 17:13:50 +0200 Subject: [PATCH 1/3] 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 | 22 ++- src/lib/frontend/d_cnf.ml | 18 +- src/lib/structures/expr.mli | 5 + tests/dune.inc | 252 ++++++++++++++++++++++++++++ tests/issues/889.expected | 2 + tests/issues/889.smt2 | 7 + tests/models/uf/uf2.models.expected | 4 +- 7 files changed, 306 insertions(+), 4 deletions(-) create mode 100644 tests/issues/889.expected create mode 100644 tests/issues/889.smt2 diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 2968d9f2f..8d14c7b2f 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 c63843a78..8e9571065 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/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 diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 2c2494557..009a678f3 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 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) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected index 3c1182254..fe82a1338 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 0) - (define-fun b () Int (- 2)) + (define-fun a () Int (- 2)) + (define-fun b () Int 0) ) From c55c0864cf122c5cabfe7241f34e26957111eb3f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 13 Oct 2023 18:20:36 +0200 Subject: [PATCH 2/3] 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)) ) From af207101673c29b0d44bdaa95976822cdbe7b79f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 16 Oct 2023 10:17:48 +0200 Subject: [PATCH 3/3] Clean up --- src/lib/frontend/cnf.ml | 6 +----- src/lib/frontend/d_cnf.ml | 2 +- src/lib/structures/expr.ml | 7 ++++--- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index b650ccf56..2968d9f2f 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -239,13 +239,9 @@ 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 -> + | TAneq lt | TAdistinct lt -> let lt = List.map (make_term up_qv name_base) lt in E.mk_distinct ~iff:true lt - - | TAdistinct lt -> - 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 [make_term up_qv name_base t1; diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 328c94a6e..c63843a78 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1337,7 +1337,7 @@ let rec mk_expr end | B.Distinct, _ -> - E.mk_distinct ~iff:true (List.map aux_mk_expr args) + E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args) | B.Constructor _, _ -> let name = get_basename path in diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 5dc0d89bb..53adde375 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1211,10 +1211,11 @@ let mk_nary_eq l = vrai 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. + (* 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. *) + 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