Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361]#4054
Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361]#4054peterschrammel wants to merge 8 commits intodiffblue:developfrom
Conversation
| /// Solve the current formula | ||
| decision_proceduret::resultt dec_solve() override; | ||
|
|
||
| /// Convert a boolean expression \p expr |
There was a problem hiding this comment.
Nit pick: s/boolean/Boolean/
| incremental_solvert::incremental_solvert( | ||
| const namespacet &ns, | ||
| prop_convt &prop_conv) | ||
| : prop_convt(ns), prop_conv(prop_conv) |
There was a problem hiding this comment.
Though you'll now have to clean this one up...
|
|
||
| /// A `prop_convt` that wraps another `prop_convt` and provides | ||
| /// a push/pop-context interface for incremental solving | ||
| class incremental_solvert : public prop_convt |
There was a problem hiding this comment.
I'm aware this is a non-trivial ask, but it would be really nice to have a unit test documenting 1) how this is used and 2) that it works as claimed. Just pushing two or three context and solve a simple Boolean problem.
| { | ||
| // We create a new context literal. | ||
| literalt context_literal = prop_conv.convert(symbol_exprt( | ||
| "symex::context$" + std::to_string(context_literal_counter++), |
There was a problem hiding this comment.
Make this magic string a static class member?
There was a problem hiding this comment.
"symex" is certainly not happening here.
|
The naming here is confusing. The propt interface is already incremental (you could give it the What gets added is the push/pop. Call it push_pop_solver? stack_solver? |
|
Maybe context_solver? |
|
Also, |
a84771b to
157e191
Compare
f9663a4 to
be7b0bb
Compare
src/solvers/prop/context_solver.cpp
Outdated
| { | ||
| // unsupported | ||
| UNREACHABLE; | ||
| } |
There was a problem hiding this comment.
Simply return false here!
src/solvers/prop/context_solver.cpp
Outdated
| { | ||
| // unsupported | ||
| UNREACHABLE; | ||
| } |
db3620a to
d726a2b
Compare
|
The hierarchy is not quite right yet. |
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d726a2b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99902719
|
@peterschrammel This needs a rebase (and consideration of @kroening's comment). |
d726a2b to
d5eb781
Compare
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 76774fe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105672538
|
Seems like a reasonable thing to want (I note that push/pop seem to be loosing favour in the SMT community in favour of solver-under-assumption). Shout when this is ready to be reviewed. |
decision_procedure_incrementalt will then be further split into support for assumptions and contexts.
Makes it explicit which algorithms actually require this feature.
This is only provided by the prop_conv_solvert-based hierarchy at the moment and is quite specific to MiniSAT-based solvers. The functionality itself is used out-of-tree only (2LS).
Provides push/pop interface
Puts the type check into a single place
76774fe to
56caec2
Compare
Also allows using raw assumptions within contexts (as required by minimization and refinement algorithms).
56caec2 to
ac58131
Compare
Must not bypass prop_conv_solvert::set_assumptions by calling prop directly.
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: ac58131).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106293396
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 9e50465).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106306303
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
|
Obsolete |
Based on #4451 - only review last 4 commits.
Upstreams part of 2LS's push/pop incremental solver interface