Skip to content

Commit

Permalink
Fix distinct unsoundness (#890)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@Halbaroth
Halbaroth authored Oct 16, 2023
1 parent ec74b44 commit 64ad841
Show file tree
Hide file tree
Showing 4 changed files with 276 additions and 4 deletions.
19 changes: 15 additions & 4 deletions src/lib/structures/expr.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
252 changes: 252 additions & 0 deletions tests/dune.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
2 changes: 2 additions & 0 deletions tests/issues/889.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

unknown
7 changes: 7 additions & 0 deletions tests/issues/889.smt2
View file
Original file line number Diff line number Diff line change
@@ -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)

0 comments on commit 64ad841

Please sign in to comment.