decision_proceduret interface #4497

kroening · 2019-04-08T11:36:52Z

This re-establishes a simpler interface for solvers. In particular, the concept of 'literal' is not exposed, which is specific to DPLL-style SAT solvers.

The new interface is in particular a much better fit for SMT2 solvers, which right now need to emulate a CNF-style interface.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-04-08T11:42:53Z

src/solvers/flattening/functions.h

@@ -37,7 +39,7 @@ class functionst
  }

 protected:
-  prop_convt &prop_conv;
+  decision_proceduret &decision_procedure;


It's strange to see a file live under flattening but then not actually use the propositional variant of a decision procedure.

It really is a 'lowering', and should move there.

peterschrammel

Lgtm as an intermediate step

peterschrammel · 2019-04-08T15:13:46Z

In particular, the concept of 'literal' is not exposed, which is specific to DPLL-style SAT solvers.

Literal is not the correct term in this context. It's a boolean variable that is equal to a predicate. I don't see anything specific to DPLL SAT here. The problem is that the interface exposes the implementation by using literalt instead of something more general.

peterschrammel · 2019-04-08T15:57:37Z

src/solvers/prop/prop_conv.h


 // API that provides a "handle" in the form of a literalt
 // for expressions.

-class prop_convt:public decision_proceduret
+class prop_convt : public prop_decision_proceduret


That means smt2_convt still implements prop_decision_proceduret.

The more I think about this PR the more doubts I have.

The predicate handle interface is something useful to have also in smt2. It is required for some of our algorithms and hence it doesn't make sense not to have a common interface for SAT-based implementations and SMT-based ones. IMO prop_decision_proceduret should be generalised, renamed and moved up into solvers/.

allredj

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

kroening · 2019-04-08T18:53:27Z

The problem here is the confusion between an interface and a particular realisation. The prop_decision_proceduret interface anticipates a particular realisation, which means it's tedious to implement for the SMT solvers.

It's fully agreed that the 'handle' for a propositional expression is useful. However, that handle shouldn't be fixed to be an integer with a sign flag. None of the users of the current interface in fact care about that.

In particular, observe that decision_proceduret already lets you get a handle for some predicate P: simply add a constraint "bX <=> P". We could add a convenience function handle(exprt) for that; the SAT-basedd solvers could implement it in the same way as they do now.

kroening · 2019-04-08T18:54:51Z

Furthermore, note that handle(exprt) would not need to be restricted to Boolean at all.

tautschnig

Stopped short of blocking this PR, but admittedly I'm not very happy with the current state.

Moving functions.{h,cpp} to lowering seems like the right thing to do and should just happen, maybe in a separate PR if there is further discussion on this one.
Let's please stop using (possibly ambiguous) abbreviations. If "prop" stands for "propositional" then let's use "propositional." If it means something else then it is even more urgent that it be spelled out.
The main concern: it seems ok that an smt_convt (also) is-a prop_convt. But the class hierarchy appears messed up to me. Why is the conversion a decision procedure? And is there actually value in the prop_convt interface at all?

kroening · 2019-04-10T14:47:22Z

Ok, let's split:

functionst is a lowering, not a flattening #4511 now moves functionst.
The renaming from prop -> propositional is agreed, but really very orthogonal to this PR. Will make separate one.
The key point of this PR is that it enables smt2_conv to become a decision_proceduret! That will need a bit more work, since the users need to use the new 'handle' interface first.

tautschnig · 2019-04-10T19:54:34Z

The key point of this PR is that it enables smt2_conv to become a decision_proceduret! That will need a bit more work, since the users need to use the new 'handle' interface first.

Would you mind elaborating as to why smt2_conv becoming a decision_proceduret is the right thing to do? We already have smt2_dect, which is documented as "Decision procedure interface for various SMT 2.x solvers."

kroening · 2019-04-10T20:35:12Z

Ah, ok, let me be more precise: right now, smt2_dect needs to implement various literalt related methods that are now required by decision_proceduret. These methods were really meant for CNF-style solvers, and thus, do not fit SMT2.

tautschnig · 2019-04-10T20:44:08Z

Ah, ok, let me be more precise: right now, smt2_dect needs to implement various literalt related methods that are now required by decision_proceduret. These methods were really meant for CNF-style solvers, and thus, do not fit SMT2.

Ok. But can we at this point achieve a clean separation between a decision procedure (which ought to implement the decision_proceduret interface) and the code converting between exprt and the decision procedure's representation (variants of *_convt)? It may make sense that a decision procedure has an X_convt, but I don't see how the is-a relationship of class X_convt : public decision_proceduret can be right.

peterschrammel · 2019-04-10T21:15:25Z

1.-3. are an improvement, in particular, generalising the handle interface (which would have made the motivation for #4440 clearer).

The changes here are orthogonal to #4450, #4451 and #4054, though, which tackle a different problem: distinguishing the various (incremental) solver features so that we don't have a god-interface prop_convtanymore, but we can clearly carve out the set of features required by each prop_convtuser.

@kroening, can you sketch a plan how you'd like to move this forward beyond 1.-3.?

kroening · 2019-04-11T11:26:27Z

@tautschnig on _convt being a decision procedure: The problem here is that an algorithm, i.e., an implementation got used as an interface. The variants of *_convt do implement decision procedures, so should inherit from decision_proceduret. The key problem I have with them is that their purpose is to combine theory solvers, and that is very much obscured. They also mix one-shot encodings and incremental encodings.

tautschnig · 2019-04-11T12:09:32Z

@tautschnig on _convt being a decision procedure: The problem here is that an algorithm, i.e., an implementation got used as an interface.

Can we just fix this?

The variants of *_convt do implement decision procedures, so should inherit from decision_proceduret.

Maybe the fix is just to rename *_convt (assuming "conv" stands for "conversion"?!)?

The key problem I have with them is that their purpose is to combine theory solvers, and that is very much obscured. They also mix one-shot encodings and incremental encodings.

That last part I again struggle with: is "encoding" and "solver" the same thing? Maybe "encoding" is such an integral part of a solver that it is. In my opinion, we care about the process going from an exprt that includes symbols via X to a model providing concrete values for (some of) those symbols. So now we can consider X a decision procedure or a solver an be done with it. Or we further decompose X into a conversion step that translates the exprt into some other representation, then runs a decision procedure on that other representation to yield a model (in yet another representation) and then allows us to convert back from some representation to values that fit the exprt.

kroening · 2019-04-11T12:23:23Z

Roadmap proposal:

We need to fix the interface that a user of a decision procedure is offered. I would propose that to offer
exprt handle(const exprt &)
No restriction on the type of the expression. Solvers that use CNF may then return a literal_exprt for Booleans. SMT-LIB solvers could return a symbol, or perhaps use a named term. BDDs could return a node number. A fallback is always to simply return the parameter, and say rely on hashing.
This could simply be added to the current decision_proceduret, along with corresponding variants of set_assumptions and get_in_conflict.
The users need to be moved to that new interface. That is mostly replacing 'literaltbyexprt`.
Then we can deprecate the literalt variants.
smt2_conv and smt2_dec can then simply stop implementing these.
In paralell, we can clean up the solver implementation, with a view towards offering an interface for theory solvers. This would replace the current 'stack' of theory solvers.

kroening · 2019-04-11T13:25:18Z

@tautschnig on _convt being a decision procedure: The problem here is that an algorithm, i.e., an implementation got used as an interface.

Can we just fix this?

That is what steps 1-3 in the proposed roadmap do.

The variants of *_convt do implement decision procedures, so should inherit from decision_proceduret.

Maybe the fix is just to rename *_convt (assuming "conv" stands for "conversion"?!)?

There is more work to do than just rename; the final name might be something well understood in the academic community, say "theory_combinationt". We could go for "solver_combinationt" to make it less scary.

That last part I again struggle with: is "encoding" and "solver" the same thing? Maybe "encoding" is such an integral part of a solver that it is. In my opinion, we care about the process going from an exprt that includes symbols via X to a model providing concrete values for (some of) those symbols. So now we can consider X a decision procedure or a solver an be done with it. Or we further decompose X into a conversion step that translates the exprt into some other representation, then runs a decision procedure on that other representation to yield a model (in yet another representation) and then allows us to convert back from some representation to values that fit the exprt.

An encoding (or "reduction") is one way of realising a solver, but there are certainly others. The process to go from a formula to a model is commonly a "decision procedure". Implementing that via reduction to something simpler is very common these days, but not essence of it. The current decision_proceduret essentially anticipates that there will be CNF at the end, and that is overly specific.

peterschrammel · 2019-04-11T13:33:29Z

along with corresponding variants of set_assumptions and get_in_conflict.

I don't think set_assumptions and get_in_conflict should be part of decision_proceduret. Not every solver can provide that functionality and also not every decision procedure user needs it. A decision procedure user should select the minimal interface that it requires.

peterschrammel · 2019-04-11T13:43:26Z

Also, #4450 (comment) must be accounted for.

peterschrammel · 2019-04-11T13:47:41Z

The lower bar for these refactorings is to make #4361 pass CI with MiniSAT. I'd call them a success if it also passes with Z3.

tautschnig · 2019-04-11T14:50:23Z

In addition to what @peterschrammel said:

[...] the final name [...]

I would just ask for a design involving that "final" name rather than intermediate steps that will come and go.

kroening · 2019-04-11T17:45:45Z

@peterschrammel The key problem with #4361 is freezing.
I think it's a dead end to impose this on on the user of the solver, and it needs to go away. SMT-LIB agrees.
I think I have an idea how to make this happen, but this should really not be a stoper for us to have the right interfaces.

kroening · 2019-04-11T17:48:00Z

@tautschnig I am not to concerned about the final name of the implementation of the combination solver. Users won't see it; they see the interface, and they see an instance that comes with a particular set of theories.
The problem right now is that we are exposing users to implementation, which means that it's not stable, and it's expensive to improve the implementation.

peterschrammel · 2019-04-11T20:36:57Z

I think I have an idea how to make this happen, but this should really not be a stoper for us to have the right interfaces.

Then this needs to be solved with highest priority - otherwise it is a stopper in doing this refactoring if we end up with the "right interfaces" that are not usable.

kroening · 2019-04-11T23:44:56Z

Item 1 now there!
Given that there are a number, I'll do a series of PRs for item 2.

tautschnig · 2019-04-11T23:55:27Z

src/solvers/prop/prop_conv.h

@@ -22,6 +22,9 @@ class prop_convt:public decision_proceduret

  using decision_proceduret::operator();

+  // handle


Maybe the notes from the roadmap (explaining that this could be a literal_exprt or a symbol or a BDD node or ...) can be copied in here instead of this comment?

Shouldn't that be abstract here and implemented in prop_conv_solvert? Only prop_conv_solvert would use literal_exprt, other implementations of prop_convt might not?

tautschnig · 2019-04-11T23:55:45Z

src/solvers/prop/decision_procedure.h

@@ -54,6 +60,7 @@ class decision_proceduret

  /// Return value of literal \p l from satisfying assignment.
  /// Return tvt::UNKNOWN if not available
+  /// This will go away, use get instead.


Mark as deprecated?

Will remove the usage first (not a lot).

tautschnig · 2019-04-11T23:55:52Z

src/solvers/prop/decision_procedure.h

@@ -34,8 +34,14 @@ class decision_proceduret
  void set_to_false(const exprt &expr);

  /// Convert a Boolean expression and return the corresponding literal
+  /// This will go away, use handle(expr) instead


Mark as deprecated? The sooner we mark it as deprecated, the earlier we can remove it ;-)

allredj

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

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

kroening added the Solvers label Apr 8, 2019

kroening assigned peterschrammel Apr 8, 2019

kroening requested review from allredj, chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, martin-cs, peterschrammel, romainbrenguier, smowton and tautschnig as code owners April 8, 2019 11:36

tautschnig reviewed Apr 8, 2019

View reviewed changes

kroening force-pushed the decision_proceduret branch from 1934a1b to 0fe5d36 Compare April 8, 2019 12:01

kroening requested review from cesaro, cristina-david and pkesseli as code owners April 8, 2019 12:01

kroening force-pushed the decision_proceduret branch 2 times, most recently from 162168d to cabf713 Compare April 8, 2019 14:43

peterschrammel approved these changes Apr 8, 2019

View reviewed changes

kroening force-pushed the decision_proceduret branch from cabf713 to 384f64e Compare April 8, 2019 14:49

peterschrammel reviewed Apr 8, 2019

View reviewed changes

kroening force-pushed the decision_proceduret branch from 384f64e to 4e1b143 Compare April 8, 2019 16:23

allredj reviewed Apr 8, 2019

View reviewed changes

tautschnig reviewed Apr 10, 2019

View reviewed changes

tautschnig assigned kroening and unassigned peterschrammel Apr 10, 2019

kroening force-pushed the decision_proceduret branch 2 times, most recently from b20067a to 541383f Compare April 11, 2019 23:44

kroening force-pushed the decision_proceduret branch from 541383f to f810a35 Compare April 11, 2019 23:45

tautschnig approved these changes Apr 11, 2019

View reviewed changes

allredj reviewed Apr 12, 2019

View reviewed changes

add the decision_proceduret::handle API

9c3774b

kroening force-pushed the decision_proceduret branch from f810a35 to 9c3774b Compare April 12, 2019 17:10

allredj reviewed Apr 12, 2019

View reviewed changes

kroening merged commit 9f63d79 into develop Apr 12, 2019

kroening deleted the decision_proceduret branch April 12, 2019 19:23

kroening mentioned this pull request Apr 13, 2019

Clean up decision_proceduret API #4530

Merged

4 tasks

		@@ -22,6 +22,9 @@ class prop_convt:public decision_proceduret

		using decision_proceduret::operator();

		// handle

decision_proceduret interface #4497

decision_proceduret interface #4497

Uh oh!

Conversation

kroening commented Apr 8, 2019

Uh oh!

tautschnig Apr 8, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Apr 8, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Apr 8, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment • 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!

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

Uh oh!

Uh oh!

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Apr 8, 2019

Uh oh!

kroening commented Apr 8, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Apr 10, 2019

Uh oh!

tautschnig commented Apr 10, 2019

Uh oh!

kroening commented Apr 10, 2019

Uh oh!

tautschnig commented Apr 10, 2019

Uh oh!

peterschrammel commented Apr 10, 2019

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

tautschnig commented Apr 11, 2019

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

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

Uh oh!

Uh oh!

peterschrammel commented Apr 11, 2019

Uh oh!

peterschrammel commented Apr 11, 2019

Uh oh!

tautschnig commented Apr 11, 2019

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

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

Uh oh!

Uh oh!

kroening commented Apr 11, 2019

Uh oh!

tautschnig Apr 11, 2019

Choose a reason for hiding this comment

Uh oh!

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

tautschnig Apr 11, 2019

peterschrammel left a comment •

edited

Loading

peterschrammel commented Apr 8, 2019 •

edited

Loading

peterschrammel Apr 8, 2019 •

edited

Loading

peterschrammel commented Apr 11, 2019 •

edited

Loading

peterschrammel commented Apr 11, 2019 •

edited

Loading

peterschrammel Apr 12, 2019 •

edited

Loading