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.

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.

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.

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

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.

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

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

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.

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.

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

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.

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

• decision_proceduret
• decision_procedure_incrementalt
• decision_procedure_assumptionst
• decision_procedure_contextst

Obsolete.