Booster: Optimise handling of known predicates when rewriting

[geo2a]

When processing an "execute" request, we are rewriting from one Pattern to one or more Patterns. In Booster, we assume definedness of the initial Pattern, i.e. it must have no "bad" applications of partial functions and the constrains should not be inconsistent.

Since the introduction of the SMT solver into Booster, we have been very conservative in how we interact with it, potentially leaving a lot of performance on the table. We should optimise the communication of the constraints of the initial Pattern, aka the known predicates, aka "the path condition" to the solver:

• when starting an execute request, we should check the consistency of the constraints to make sure we are not rewriting inside a vacuous state (this is done in 4012 evaluate pattern pruning #4020)
• if the constraints are consistent, we will reuse the created Z3 scope for all subsequent queries, hopefully making the side condition checks very fast
• when we add new constraints to the current Pattern withing the same "execute" request, we have two options:
  • the conservative option would be to pop the scope, add the ensured condition to the known predicates, push them ch check-sat;
  • the more performant option is to push the scope before checking the ensures conditions and avoid re-checking the previous know truth.

We will need to re-think how we do solver retries. Currently, we do a hard reset every time we retry, which restarts the solver. We should instead to a soft reset:

• pop the last scope, which includes the predicate we are checking
• reuse the previous scopes that contain the known predicates
• change the timeout setting, push and check sat

The comments to this issue will outline the specific changes that need to be done to the SMT-related types and function in Booster to implement this approach.

[PetarMax]

I think that we always want the ground truth G at the top of the Z3 stack, knowing it's SAT.

Then, when we're checking a branching on P, we do:

• add P, check SAT, pop
• add !P, check SAT, pop

get the results back and G is still at the top of the stack. There are indications that Z3 is able to reuse the information it learned from proving G SAT, because the checks of G /\ P and G /\ !P are much faster than just the check of G.

When an ensures P comes, should we not do the following?

• add P, check SAT
  • if SAT, drop the top of the stack (to avoid accumulation), push, and we have the (new) ground truth at the top of the stack;
  • if UNSAT, the branch is vacuous, do whatever is appropriate.

[jberthold]

Some notes from a first code inspection:

• needs additional state above the SMT.Runner.SMTContext level
  • each request during a rewrite/simplification (isSat, checkPredicates) will send the path condition again.
  • The current path cond. needs to be checked against the one used most recently (and pushed).
  • additional constraints added since the last time (set diff) need to be translated and asserted to z3 (and pushed)
• the state is now two-fold (or we add this to SMTContext), remembering pushed assertions, which needs more careful management
• we have to refactor to remove the hardResetSolver calls
• on retry, we need to re-push the last known path cond. (as a whole) and check isSat for it to seed the solver (probably
  timeout prone?) before re-trying the actual request at hand.

[jberthold]

As it turned out from lido experiments, it is a much bigger benefit to reduce the amount of prelude and ground truth assertions than to keep them around as state in Z3. Closing