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 2 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
6 changes: 5 additions & 1 deletion src/lib/frontend/cnf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,9 +239,13 @@ 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

Copy link
Collaborator

Choose a reason for hiding this comment

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

Can you undo this whitespace change? Thanks.

| TAdistinct lt ->
E.mk_distinct ~iff:true (List.map (make_term up_qv name_base) lt)

Copy link
Collaborator

Choose a reason for hiding this comment

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

Can we avoid these changes? They don't seem useful, and keeping the patch as tiny as possible makes it easier to cherry-pick and move around if needed.

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. Besides, we should use a different constructor for TAneq? It's not documented and I'm not sure what is the expected semantic for this constructor.

Copy link
Collaborator

Choose a reason for hiding this comment

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

TAneq [x; y] is the constructor used for x <> y. "neq" is a fairly common shorthand for "not equal".

| TAle [t1;t2] ->
E.mk_builtin ~is_pos:true Sy.LE
[make_term up_qv name_base t1;
Expand Down
2 changes: 1 addition & 1 deletion src/lib/frontend/d_cnf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1337,7 +1337,7 @@ let rec mk_expr
end

| B.Distinct, _ ->
E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args)
E.mk_distinct ~iff:true (List.map aux_mk_expr args)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Same as above, can we undo this? There shouldn't be this sort of unrelated cleanup in a hotfix.


| B.Constructor _, _ ->
let name = get_basename path in
Expand Down
18 changes: 14 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,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. *)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Note: this is not specifically related to the SMT-LIB specification but to the usual definition of distinct.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Also the comment should point to #889 which will track the fix in the next branch

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Actually I didn't plan to apply this patch on next but I can.

Copy link
Collaborator

@bclement-ocp bclement-ocp Oct 16, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

Sorry, I maybe was not clear. #889 is not about this patch, #889 is about the issue with distinct. We don't need to apply the patch on next. We will fix the issue with distinct on next in a different way, which is fine, but we should still refer to it here.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ok :)

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