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

[peterschrammel]

Based on #4449, only review last 2 commits.

• decision_proceduret can now be used instead instead of prop_convt in most of the codebase.
• decision_procedure_incrementalt is only used where incremental solving is actually necessary.

In the next step decision_procedure_incrementalt will then be further split into support for assumptions (see #4451) and contexts (see #4054).

• 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]

decision_proceduret can now be used instead instead of prop_convt in most of the codebase.
decision_procedure_incrementalt is only used where incremental solving is actually necessary.

I haven't looked at the actual commits, but would certainly require @kroening to comment on this. To me, it seems a bit surprising. My assumption was that prop_convt is the part that takes care of translating some higher-level representation into a solver-level representation.

[peterschrammel]

takes care of translating some higher-level representation into a solver-level representation.

That might have been the initial intuition, but actually smt2_convt implements the same interface without any prop involved.

[kroening]

This does not make sense to me -- the decision procedure interface was already designed to be incremental, and has already been used in this fashion.

[kroening]

@tautschnig has the right intuition here. The key idea isn't the conversion, but the fact that prop_conv offers a 'handle' for predicates. This is also what smt2_conv offers. However, the 'handle' has now been pushed up to decision_proceduret, which turns prop_convt into an implementation as opposed to an interface.

[peterschrammel]

This does not make sense to me -- the decision procedure interface was already designed to be incremental, and has already been used in this fashion.

No, decision_proceduret could not / cannot be used incrementally with MiniSAT under the hood, for example, because the freezing functionality is missing.

[kroening]

The way forward is to consider what's an interface, who consumes that, and what implementations of that interface should exist.

[peterschrammel]

Also, look at #4451 to see how I'm going to move this forward.

[kroening]

The problem that Minisat with preprocessed needs freezing is a special case; this shouldn't necessarily be imposed on all users of incremental solving. It's certainly by no means intuitive.

[peterschrammel]

The problem that Minisat with preprocessed needs freezing is a special case; this shouldn't necessarily be imposed on all users of incremental solving. It's certainly by no means intuitive.

Unfortunately, you cannot hide that and just ignore it.

[tautschnig]

@kroening I do think that class names need to be changed - prop_conv are two, ambiguous abbreviations (property conversion? propositional conversion? something else?).

[peterschrammel]

If we can get rid of decision_procedure_incrementalt at some point because no special treatment for MiniSAT&Co is required anymore, then even better - it will just drop out of the hierarchy.

[allredj]

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

@kroening, please have a look at the proposed hierarchy of interfaces:

• decision_proceduret
• decision_procedure_incrementalt
• decision_procedure_assumptionst
• decision_procedure_contextst

[peterschrammel]

Obsolete.