Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix distinct unsoundness #890

Merged
merged 3 commits into from
Oct 16, 2023
Merged

Fix distinct unsoundness #890

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e81c18a
Fix distinct unsoundness
Halbaroth Oct 13, 2023
c55c086
Fix the smart constructor of `mk_distinct`
Halbaroth Oct 13, 2023
af20710
Clean up
Halbaroth Oct 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 15 additions & 4 deletions src/lib/structures/expr.ml
View file
Open in desktop
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
Comment on lines +1219 to +1227
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: it doesn't really matter here as this is a hotfix but conversion to an array is not needed:

let distinct_from x acc ys =
  List.fold_left (fun acc y -> mk_and (neg (mk_eq ~iff x y)) acc) acc ys
in let rec distinct_aux acc = function
  | [] -> acc
  | x :: ys -> distinct_aux (distinct_from x acc ys) ys
in distinct_aux acc args

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know but I think the imperative version is the easier to read and a bit less error-prone. It's a matter of taste.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is not only a matter of taste (I also find the imperative version easier to read in this specific case); the imperative version is slower and uses more memory because of the call to Array.of_list. It is entirely negligible here (hence why it's a nit), just pointing that out.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure ;)


let mk_builtin ~is_pos n l =
let pos =
Expand Down
252 changes: 252 additions & 0 deletions tests/dune.inc
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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)
Loading