stack_decision_proceduret for solving under assumptions/contexts #4581

peterschrammel · 2019-04-28T11:18:38Z

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.

smowton · 2019-04-29T08:30:00Z

src/solvers/stack_decision_procedure.h

+\*******************************************************************/
+
+/// \file
+/// Decision procedure with incremental solving with contexts


Perhaps give an example of intended usage?

I've added two examples

smowton · 2019-04-29T08:37:35Z

src/solvers/prop/prop_conv_solver.cpp

@@ -365,7 +365,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
  return true;
 }

-void prop_conv_solvert::set_to(const exprt &expr, bool value)
+void prop_conv_solvert::do_set_to(const exprt &expr, bool value)


Give this a better name, or provide some documentation to advise a future editor on whether they want set_to or do_set_to

documentation extended

smowton · 2019-04-29T08:39:01Z

src/solvers/prop/prop_conv_solver.h

@@ -124,10 +127,24 @@ class prop_conv_solvert : public conflict_providert,

  virtual void ignoring(const exprt &expr);

-  // deliberately protected now to protect lower-level API
+  /// Actually adds the constraints to `prop`


Explicitly mention that set_to is a wrapper around this, and which one ought to be used

made private

do_set_to is not a great name, why not naming it add_constraint_to_prop?

smowton · 2019-04-29T08:43:28Z

src/solvers/prop/prop_conv_solver.cpp

+{
+  // We remove the context from the stack.
+  for(size_t i = 0; i < context_size_stack.back(); ++i)
+    assumption_stack.pop_back();


assumption_stack.resize(assumption_stack.size() - context_size_stack.back())?

Yes, should work. Shrinking resize doesn't reallocate.

tautschnig · 2019-04-29T10:39:58Z

src/solvers/stack_decision_procedure.h

+
+  /// Push a new context on the stack
+  /// This context becomes a child context nested in the current context.
+  virtual void push() = 0;


Is this equivalent to a push of an empty vector?

No - clarified in docs

tautschnig · 2019-04-29T10:42:42Z

src/solvers/stack_decision_procedure.h

+  virtual void push() = 0;
+
+  /// Pop whatever has been pushed in the last call to `push`
+  virtual void pop() = 0;


I don't think the documentation is accurate: two calls to pop wouldn't remove the same element? I think the documentation should refer to the top of the stack. And what's the behaviour when stack underflow would occur? Is an implementation expected to handle this gracefully (by ignoring it), or should it fail hard?

tautschnig · 2019-04-29T10:46:29Z

src/solvers/prop/prop_conv_solver.h

  propt &prop;

  messaget log;
+
+  static const char *context_prefix;


Can we just initialise it right here rather than in the implementation file?

What would be the advantage of that?

Fewer lines of code and easier to locate. But clearly a nit-pick and all up to you.

tautschnig · 2019-04-29T10:48:08Z

src/solvers/prop/prop_minimize.cpp

-        prop_conv.set_assumptions(assumptions);
+        exprt::operandst assumptions;
+        assumptions.push_back(literal_exprt(c));
+        prop_conv.push(assumptions);


How about simplifying all this to prop_conv.push({literal_exprt{c}});?

romainbrenguier · 2019-04-29T11:31:21Z

src/solvers/prop/prop_conv_solver.h

@@ -124,10 +127,24 @@ class prop_conv_solvert : public conflict_providert,

  virtual void ignoring(const exprt &expr);

-  // deliberately protected now to protect lower-level API
+  /// Actually adds the constraints to `prop`


do_set_to is not a great name, why not naming it add_constraint_to_prop?

Provides combined push/pop + assumptions interface

and carry over the current, partial support in smt2_convt.

Remove obsolete method declaration

peterschrammel requested review from allredj, chrisr-diffblue, kroening, martin-cs, romainbrenguier, smowton and tautschnig as code owners April 28, 2019 11:18

peterschrammel force-pushed the stack-decision-procedure branch from 8a19559 to 9ae2e3e Compare April 28, 2019 11:24

smowton approved these changes Apr 29, 2019

View reviewed changes

tautschnig approved these changes Apr 29, 2019

View reviewed changes

tautschnig assigned peterschrammel, martin-cs and romainbrenguier Apr 29, 2019

romainbrenguier approved these changes Apr 29, 2019

View reviewed changes

peterschrammel added the do not merge label Apr 29, 2019

peterschrammel unassigned martin-cs and romainbrenguier Apr 29, 2019

peterschrammel added 3 commits April 29, 2019 13:50

Decision procedure interface for solving with contexts/assumptions

c1be0a3

Provides combined push/pop + assumptions interface

Implement context-based solver on top of prop_conv_solvert

b73c67c

and carry over the current, partial support in smt2_convt.

Fixup to 13f5f0c

bc3837e

Remove obsolete method declaration

peterschrammel force-pushed the stack-decision-procedure branch from 9ae2e3e to bc3837e Compare April 29, 2019 12:50

peterschrammel removed the do not merge label Apr 29, 2019

peterschrammel merged commit afb3df7 into diffblue:develop Apr 29, 2019

peterschrammel deleted the stack-decision-procedure branch April 29, 2019 13:57

stack_decision_proceduret for solving under assumptions/contexts #4581

stack_decision_proceduret for solving under assumptions/contexts #4581

Uh oh!

Conversation

peterschrammel commented Apr 28, 2019

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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel Apr 29, 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!

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!

Uh oh!

peterschrammel Apr 29, 2019 •

edited

Loading