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

peterschrammel · 2019-02-03T18:15:21Z

Based on #4451 - only review last 4 commits.

Upstreams part of 2LS's push/pop incremental solver interface

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.

tautschnig · 2019-02-03T18:20:47Z

src/solvers/prop/incremental_solver.h

+  /// Solve the current formula
+  decision_proceduret::resultt dec_solve() override;
+
+  /// Convert a boolean expression \p expr


Nit pick: s/boolean/Boolean/

tautschnig · 2019-02-03T18:22:35Z

src/solvers/prop/incremental_solver.cpp

+incremental_solvert::incremental_solvert(
+  const namespacet &ns,
+  prop_convt &prop_conv)
+  : prop_convt(ns), prop_conv(prop_conv)


#4043 makes the useless namespacet go away...

Though you'll now have to clean this one up...

tautschnig · 2019-02-03T18:24:44Z

src/solvers/prop/incremental_solver.h

+
+/// A `prop_convt` that wraps another `prop_convt` and provides
+/// a push/pop-context interface for incremental solving
+class incremental_solvert : public prop_convt


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.

tautschnig · 2019-02-03T18:26:17Z

src/solvers/prop/incremental_prop_conv_solver.cpp

+{
+  // We create a new context literal.
+  literalt context_literal = prop_conv.convert(symbol_exprt(
+    "symex::context$" + std::to_string(context_literal_counter++),


Make this magic string a static class member?

"symex" is certainly not happening here.

kroening · 2019-02-03T18:37:00Z

The naming here is confusing. The propt interface is already incremental (you could give it the get_number_of_solver_calls() method).

What gets added is the push/pop. Call it push_pop_solver? stack_solver?

kroening · 2019-02-03T18:38:32Z

Maybe context_solver?

kroening · 2019-02-03T18:39:50Z

Also, set_assumptions becomes unusable, I suppose? I would then add an implementation with PRECONDITION(false).

kroening · 2019-02-05T20:16:59Z

src/solvers/prop/context_solver.cpp

+{
+  // unsupported
+  UNREACHABLE;
+}


Simply return false here!

kroening · 2019-02-05T20:17:11Z

src/solvers/prop/context_solver.cpp

+{
+  // unsupported
+  UNREACHABLE;
+}


kroening · 2019-02-06T10:06:23Z

The hierarchy is not quite right yet.
There should an interface, which extends decision_proceduret; it shouldn't prescribe implementation via propt.
Then there's a particular kind of implementing this, using propt, which will be derived from prop_convt.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: d726a2b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99902719

tautschnig · 2019-03-07T09:04:06Z

@peterschrammel This needs a rebase (and consideration of @kroening's comment).

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 76774fe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105672538

martin-cs · 2019-03-25T14:53:25Z

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

Also allows using raw assumptions within contexts (as required by minimization and refinement algorithms).

Must not bypass prop_conv_solvert::set_assumptions by calling prop directly.

allredj

⚠️
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

⚠️
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.

peterschrammel · 2019-04-30T15:50:01Z

Obsolete

peterschrammel requested review from chrisr-diffblue, kroening, martin-cs, smowton and tautschnig as code owners February 3, 2019 18:15

tautschnig previously approved these changes Feb 3, 2019

View reviewed changes

peterschrammel changed the title ~~Incremental solver interface~~ Context-based solver interface for incremental solvers Feb 3, 2019

peterschrammel force-pushed the incremental-solver-interface branch from a84771b to 157e191 Compare February 3, 2019 22:24

peterschrammel requested review from allredj and romainbrenguier as code owners February 3, 2019 22:24

peterschrammel force-pushed the incremental-solver-interface branch 4 times, most recently from f9663a4 to be7b0bb Compare February 3, 2019 23:01

tautschnig assigned peterschrammel Feb 4, 2019

kroening reviewed Feb 5, 2019

View reviewed changes

src/solvers/prop/context_solver.cpp Outdated

{

// unsupported

UNREACHABLE;

}

Copy link

Member

kroening Feb 5, 2019

Choose a reason for hiding this comment

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

Same here

peterschrammel reacted with thumbs up emoji

peterschrammel force-pushed the incremental-solver-interface branch 3 times, most recently from db3620a to d726a2b Compare February 6, 2019 09:25

allredj reviewed Feb 6, 2019

View reviewed changes

peterschrammel added the do not merge label Feb 8, 2019

peterschrammel mentioned this pull request Feb 18, 2019

Add counting number of solver calls #4218

Merged

7 tasks

tautschnig added the Needs rebase label Mar 7, 2019

peterschrammel force-pushed the incremental-solver-interface branch from d726a2b to d5eb781 Compare March 10, 2019 16:34

allredj reviewed Mar 25, 2019

View reviewed changes

peterschrammel mentioned this pull request Mar 28, 2019

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

Closed

7 tasks

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 ~~[WIP] Context-based solver interface for incremental solvers [blocks: 4361]~~ [WIP] Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361] Mar 28, 2019

peterschrammel added dependent - do not merge and removed do not merge labels Mar 28, 2019

peterschrammel added 4 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).

Decision procedure interface for incremental solving with contexts

30b6353

Provides push/pop interface

Allow getting context-based incremental solver

bd5970c

Puts the type check into a single place

peterschrammel force-pushed the incremental-solver-interface branch from 76774fe to 56caec2 Compare March 28, 2019 23:35

Implement context-based solver on top of prop_conv_solvert

ac58131

Also allows using raw assumptions within contexts (as required by minimization and refinement algorithms).

peterschrammel force-pushed the incremental-solver-interface branch from 56caec2 to ac58131 Compare March 29, 2019 08:48

peterschrammel requested review from cesaro, cristina-david, danpoe, hannes-steffenhagen-diffblue and pkesseli as code owners March 29, 2019 08:48

Make bv_refinementt compatible with contexts

9e50465

Must not bypass prop_conv_solvert::set_assumptions by calling prop directly.

allredj reviewed Mar 29, 2019

View reviewed changes

peterschrammel changed the title ~~[WIP] Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361]~~ Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361] Mar 29, 2019

peterschrammel removed the work in progress label Mar 29, 2019

allredj reviewed Mar 29, 2019

View reviewed changes

peterschrammel mentioned this pull request Apr 10, 2019

decision_proceduret interface #4497

Merged

3 tasks

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 incremental-solver-interface branch April 30, 2019 15:50

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

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

Uh oh!

Conversation

peterschrammel commented Feb 3, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 3, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 3, 2019

Uh oh!

kroening commented Feb 3, 2019

Uh oh!

kroening commented Feb 3, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 6, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 7, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Mar 25, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Apr 30, 2019

Uh oh!

Uh oh!

peterschrammel commented Feb 3, 2019 •

edited

Loading

tautschnig Feb 3, 2019 •

edited

Loading