Separate interface for solving under assumptions [depends: 4450, blocks: 4054] by peterschrammel · Pull Request #4451 · diffblue/cbmc

peterschrammel · 2019-03-28T10:24:21Z

Based on #4450, only review last commit.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

martin-cs

Am unsure but I guess it makes sense to resolve the discussion around #4450 first.

martin-cs · 2019-03-28T11:54:45Z

src/solvers/prop/decision_procedure_assumptions.cpp

+
+void decision_procedure_assumptionst::set_assumptions(const bvt &)
+{
+  UNREACHABLE;


Could this be pure virtual or something else? Base implementations of methods that are just "nope!" make me kinda nervous.

True, I've actually thought I had patched that. Will change.

martin-cs · 2019-03-28T11:57:12Z

src/solvers/prop/decision_procedure_assumptions.h

+{
+public:
+  /// Set assumptions for the next call to operator() to solve the problem
+  virtual void set_assumptions(const bvt &);


Why is this / should this be a separate call? If the solver is deterministic then it's not like you are going to call solve multiple times? One reason it might be separate is that you want to be able to call this multiple times, but, if that is the case, do you need interfaces to manage and remove these?

There is no particular reason except legacy. You can remove assumptions by passing an empty bvt.

If we are going to refactor then really the assumptions should be an argument to the solve call and not stateful.

Better yet; it can be an argument and a result of the solve call so we can get back a reduced set of assumptions that are sufficient to give UNSAT.

peterschrammel · 2019-03-28T14:51:12Z

@martin-cs, another question is whether is_in_conflict should be placed on top of assumptions. This would be justified as smt2_convt can emulate assumptions, but cannot do is_in_conflict.

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).

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: a17fb36).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106239885
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.

martin-cs · 2019-03-29T16:52:48Z

To my mind is_in_conflict is something for an incremental solver interface (i.e. the main interface) rather than solve under assumption. If you are monotonically adding to a set of constraints then tracking (maybe triggering solve?) when a call to solve has returned UNSAT is a meaningful thing to do. If you are working with assumptions then it is just making the interface more stateful than it needs to be.

peterschrammel · 2019-03-29T22:36:07Z

@martin-cs, no. Minisat Solver.cc:401: ...express the final conflict in terms of assumptions. Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and stores the result in 'out_conflict'.

martin-cs · 2019-04-01T07:53:07Z

@peterschrammel : my point is that this could be wrapped by this API and made into a single call to solve : set of assumptions -> SAT | set of contradictory assumptions. The actual solver is going to be very stateful but our interface to it can be a lot less stateful.

peterschrammel · 2019-04-30T15:51:49Z

obsolete

peterschrammel added Solvers cleanup dependent - do not merge labels Mar 28, 2019

peterschrammel requested review from allredj, cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, pkesseli, romainbrenguier, smowton and tautschnig as code owners March 28, 2019 10:24

peterschrammel mentioned this pull request Mar 28, 2019

Use decision_proceduret instead of prop_convt [depends: 4533, blocks: 4451] #4450

Closed

7 tasks

martin-cs reviewed Mar 28, 2019

View reviewed changes

peterschrammel force-pushed the inremental-dp-assumptions branch from 6b7e292 to 1de02f5 Compare March 28, 2019 14:19

peterschrammel force-pushed the inremental-dp-assumptions branch 3 times, most recently from 03739c1 to de0f768 Compare March 28, 2019 17:29

peterschrammel added 2 commits March 28, 2019 17:33

Rename prop_convt to decision_procedure_incrementalt

9bb9d1a

decision_procedure_incrementalt will then be further split into support for assumptions and contexts.

Update decision procedure docs

8927b7d

peterschrammel changed the title ~~Separate interface for solving under assumptions [depends: 4450]~~ Separate interface for solving under assumptions [depends: 4450, blocks: 4054] Mar 28, 2019

peterschrammel added the blocker label Mar 28, 2019

peterschrammel added 2 commits March 28, 2019 20:33

Split out decision procedure with solving under assumptions

f62db13

Makes it explicit which algorithms actually require this feature.

Split out is_in_conflict solver capability

a17fb36

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).

peterschrammel force-pushed the inremental-dp-assumptions branch from de0f768 to a17fb36 Compare March 28, 2019 20:34

allredj reviewed Mar 28, 2019

View reviewed changes

peterschrammel mentioned this pull request Mar 29, 2019

Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361] #4054

Closed

7 tasks

peterschrammel mentioned this pull request Apr 10, 2019

decision_proceduret interface #4497

Merged

3 tasks

peterschrammel self-assigned this Apr 15, 2019

peterschrammel mentioned this pull request Apr 28, 2019

stack_decision_proceduret for solving under assumptions/contexts #4581

Merged

7 tasks

peterschrammel closed this Apr 30, 2019

peterschrammel deleted the inremental-dp-assumptions branch April 30, 2019 15:51

Conversation

peterschrammel commented Mar 28, 2019

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 28, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel Mar 28, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel Mar 28, 2019

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 28, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel Mar 28, 2019

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 29, 2019

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 29, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Mar 28, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Mar 29, 2019

Uh oh!

peterschrammel commented Mar 29, 2019

Uh oh!

martin-cs commented Apr 1, 2019

Uh oh!

peterschrammel commented Apr 30, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants