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

Jump to bottom

get-assignment is wrong with CDCL solver #937

Closed
bclement-ocp opened this issue Nov 16, 2023 · 3 comments
Closed

get-assignment is wrong with CDCL solver #937

bclement-ocp opened this issue Nov 16, 2023 · 3 comments
Assignees
@Stevendeo

Comments

@bclement-ocp
Copy link
Collaborator

bclement-ocp commented Nov 16, 2023 •
edited
Loading

Consider the test tests/models/bool/bool3.models.smt2 which we only test using the Tableaux solver (this is an issue, we should be testing model generation on the default solver now that this is supported).

(set-logic ALL)
(set-option :produce-assignments true)
(set-option :produce-models true)
(declare-const x Bool)
(declare-const y Bool)
(assert (or (! (and x y) :named foo) (! (and (not x) (not y)) :named bar)))
(check-sat)
(get-model)
(get-assignment)

Alt-Ergo with the (default -- using alt-ergo tests/models/bool/bool3.models.smt2) CDCL solver finds the following model and assignment:

unknown
(
  (define-fun x () Bool false)
  (define-fun y () Bool false)
)
((foo false)
 (bar false))

This is wrong: bar should be true, not false ((and (not false) (not false)) is clearly true).

I believe this should be fixed by switching to the new Dolmen implementation of :named terms, since that will automatically declare foo and bar as actual constants.
@bclement-ocp
Copy link
Collaborator Author

this is an issue, we should be testing model generation on the default solver now that this is supported

Before someone beats me to the punch: PR incoming for that.

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 16, 2023
@bclement-ocp
Use default solver for testing models
8049387 
Prior to c1e4387 (OCamlPro#829) we did not have
model generation in the default solver, and model generation required to
use the Tableaux solver, so we used the Tableaux solver when testing
models.

Since the default solver now supports model generation, we should use it
to test model generation instead, since the models generated by both
solvers can be different and most users will use the default solver
rather than the Tableaux solver.

Unfortunately, this causes some tests using `get-assignment` to fail
(see OCamlPro#937).
@bclement-ocp bclement-ocp mentioned this issue Nov 16, 2023
Merged
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 16, 2023
@bclement-ocp
Use default solver for testing models
46b2ecb 
Prior to c1e4387 (OCamlPro#829) we did not have
model generation in the default solver, and model generation required to
use the Tableaux solver, so we used the Tableaux solver when testing
models.

Since the default solver now supports model generation, we should use it
to test model generation instead, since the models generated by both
solvers can be different and most users will use the default solver
rather than the Tableaux solver.

Unfortunately, this causes some tests using `get-assignment` to fail
(see OCamlPro#937).
bclement-ocp added a commit that referenced this issue Nov 16, 2023
@bclement-ocp
Use default solver for testing models (#938)
e96d3d4 
Prior to c1e4387 (#829) we did not have
model generation in the default solver, and model generation required to
use the Tableaux solver, so we used the Tableaux solver when testing
models.

Since the default solver now supports model generation, we should use it
to test model generation instead, since the models generated by both
solvers can be different and most users will use the default solver
rather than the Tableaux solver.

Unfortunately, this causes some tests using `get-assignment` to fail
(see #937).
@bclement-ocp bclement-ocp mentioned this issue Nov 21, 2023
Merged
@Stevendeo
Copy link
Collaborator

Can we close this issue?

@bclement-ocp
Copy link
Collaborator Author

Looks like this is fixed in #961 and we forgot to link it, yes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Stevendeo Stevendeo

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Stevendeo @bclement-ocp