Potential optimization: split the solver into two

[konnov]

The following discussions proposes a hypothesis about a potential source of slowdown in Apalache, which relates to how the model checker is interacting with Z3. This hypothesis may be completely wrong, but it should be relatively easy to conduct experiments and see, whether it is wrong or not.

Assume that Init encodes a single symbolic transition and Next encodes two symbolic transitions A and B. Additionally, we are checking an invariant Inv. This is how the model checker interacts with Z3:

1. Check Init:
   1. Translate Init to Z3.
   2. Call (check). If UNSAT, terminate.
   3. Translate Inv to Z3.
   4. Call (check). If SAT, terminate.
2. Check step i for 1 <= i <= length:
   1. Check A:
      1. Save the context via (push).
      2. Translate A to Z3.
      3. Call (check). If SAT, save that A is enabled. Otherwise, save that A is disabled.
      4. Translate Inv' to Z3 (if the invariants are checked before making a step).
      5. Call (check). If SAT, terminate.
      6. Restore the context via (pop).
   2. Check B:
      1. Save the context via (push).
      2. Translate B to Z3.
      3. Call (check). If SAT, save that B is enabled. Otherwise, save that B is disabled.
      4. Translate Inv' to Z3 (if the invariants are checked before making a step).
      5. Call (check). If SAT, terminate.
      6. Restore the context via (pop).
   3. If both A and B are disabled, terminate.
   4. Translate A to Z3, if it was enabled.
   5. Translate B to Z3, if it was enabled.
   6. Encode non-deterministic choice of either A or B (modulo which ones were enabled).
   7. If the invariants are checked after making a step:
      1. Save the context via (push).
      2. Translate Inv to Z3.
      3. Call (check). If SAT, terminate.
      4. Restore the context via (pop).

There are several observations to be made here:

1. Whenever an invariant violation is found (the solver returns SAT for Inv or Inv'), the search terminates. Hence, the invariant checks gravitate towards UNSAT (the last call may result in SAT, which would produce an error).
2. Although each of A and B may be enabled or disabled after making i steps, in many practical benchmarks the actions are only disabled in a prefix and then all become enabled. Still, we are checking, whether they are enabled or not, as pruning disabled transitions significantly reduces the number of constraints. (We can disable this option with --discard-disabled=false.) Hence, these calls gravitate towards SAT.

What happens in the above interaction is that the solver is constantly switching between proving and disproving satisfiability of the context. This probably forces the solver to forget all clauses it has learned in the previous steps (how would we check that it is true?). If this is true, we are not using the incremental mode efficiently. This probably also explains the visible exponential slowdown as the number of steps increases.

If this is indeed true, we could try to help the solver to keep its learned context for SAT by using two solver instances:

1. An instance for proving mostly SAT. This one would only check, whether transitions are enabled. Sometimes, they will be disabled, but in most cases, all queries will be SAT. We do not have to use push and pop, so the solver can keep all the learned clauses.
2. An instance for proving only UNSAT. This one would only check the invariants. Again, we don't have to use push and pop. Potentially, the invariants disproven at previous steps may help the solver to prove UNSAT faster.

[thpani]

Your hypothesis makes sense to me.

In my experiments, with --discard-disabled=false I see almost uniform runtimes for the same spec (parallelizing at different steps). Whereas with --discard-disabled, runtimes are all over the place. Which would suggest that the enabledness checks "confuse" the solver.

[thpani]

However, afaict, the suggested solution would mean pushing non-deterministic choice among enabled transitions into both solver instances, which might again slow them down both?

[thpani]

Also, I'm not clear though how you would get rid of push-pop on enabledness checks?

[konnov]

True. For enabledness, we would still need push and pop.

[rodrigo7491]

I agree with @thpani that the idea makes sense, but I think it is hard to say at this stage what the effect in solving time will be.

Just to be sure I got it right, the proposed change will lock search.invariant.mode to after, given that the idea is to avoid push-pop on the second solver instance, right?