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

feat: get-assignment statement #848

Merged
merged 15 commits into from
Nov 9, 2023
+308 −3
Merged

feat: get-assignment statement #848

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
ec769f9
Produce assignments option
Stevendeo Sep 29, 2023
a6221a4
Placeholder for get_assignments
Stevendeo Sep 29, 2023
b465653
Gathering the named formulae
Stevendeo Oct 31, 2023
c9317ef
Pulling threads up to the SAT solver
Stevendeo Oct 31, 2023
fe5c2cb
Update tests
Stevendeo Nov 2, 2023
9b461ef
Proprification
Stevendeo Nov 2, 2023
0cfbec6
Adding basic get_value
Stevendeo Nov 2, 2023
f5cc809
Update tests
Stevendeo Nov 2, 2023
5c6f05f
Poetry
Stevendeo Nov 2, 2023
083693f
Removing useless check
Stevendeo Nov 2, 2023
541b4d6
Removing spurious term selection in binder
Stevendeo Nov 2, 2023
86f8f33
Poetry
Stevendeo Nov 3, 2023
9cbf833
Adding tests
Stevendeo Nov 6, 2023
15f0560
Adding tests & handling case where model gen is disabled
Stevendeo Nov 7, 2023
9c79109
Update test
Stevendeo Nov 8, 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
40 changes: 25 additions & 15 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
@@ -886,22 +886,32 @@ let main () =

| {contents = `Get_assignment; _} ->
begin
match State.get partial_model_key st with
| Some Model ((module SAT), partial_model) ->
if State.get produce_assignment st then
handle_get_assignment
~get_value:(SAT.get_value partial_model)
st
else
if Options.get_interpretation () then begin
match State.get partial_model_key st with
| Some Model ((module SAT), partial_model) ->
if State.get produce_assignment st then
handle_get_assignment
~get_value:(SAT.get_value partial_model)
st
else
recoverable_error
"Produce assignments disabled; \
add (set-option :produce-assignments true)";
st
| None ->
(* TODO: add the location of the statement. *)
recoverable_error
"Produce assignments disabled; \
add (set-option :produce-assignments true)";
st
| None ->
(* TODO: add the location of the statement. *)
recoverable_error
"No model produced, cannot execute get-assignment.";
st
"No model produced, cannot execute get-assignment.";
st
end
else
begin
(* TODO: add the location of the statement. *)
recoverable_error
"(get-assignment) requires model generation, \
but it is disabled (try --produce-models)";
st
end
Copy link
Collaborator

Choose a reason for hiding this comment

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

I thought we determined earlier that produce-assignments should work without produce-models, why are we disabling it instead?

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'm not sure why you requested an extra test for get-assignment if not for testing this specific case. Did you mean you wanted a non-error test with no models calculated but a get-assignment response anyway? Because there already was a test without (set-option :produce-models true).
The standard states that, when in sat mode, "the solver will have identified a model A of the current logic". I think that's what confused me (the said model can be abstract, which is specified later on the standard).

Copy link
Collaborator

Choose a reason for hiding this comment

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

Yes, I wanted a successful test :) Indeed the sat does not require to have built the model explicitly.

Because there already was a test without (set-option :produce-models true).

Sorry, I must have missed it, but I still don't see it — can you point me to that test? The tests I see are bool1, bool2, bool3 that have both produce-models and produce-assignments; get-assignment1 that has neither, get-assignment2 that has produce-models but not produce-assignments and only the new get-assignment3 that has produce-assignment but not produce-models.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We should have a test without (set-option :produce-models true), otherwise looks good (modulo the integer / boolean typo).

tests/smtlib2/testfile-get-assignment1.err.dolmen.smt2 indeed has neither

Copy link
Collaborator

Choose a reason for hiding this comment

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

Ah! Sorry I was not clear, I meant without produce-models but with produce-assignments as clarified in my later message :)

end

| {contents = `Other (custom, args); _} ->
21 changes: 21 additions & 0 deletions tests/dune.inc
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion tests/smtlib/testfile-get-assignment1.err.dolmen.expected
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(error "No model produced, cannot execute get-assignment.")
(error "(get-assignment) requires model generation, but it is disabled (try --produce-models)")
3 changes: 3 additions & 0 deletions tests/smtlib/testfile-get-assignment3.err.dolmen.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@

unknown
(error "(get-assignment) requires model generation, but it is disabled (try --produce-models)")
6 changes: 6 additions & 0 deletions tests/smtlib/testfile-get-assignment3.err.dolmen.smt2
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(set-logic ALL)
(set-option :produce-assignments true)
(declare-const x Int)
(assert (! (= x 0) :named foo))
(check-sat)
(get-assignment)