Use assumptions in incremental Z3SolverContext

[thpani]

We currently encode transitions in SMT like this:

;; ... prefix
(push)
;; translate transition to SMT
(push)
(assert transition-trigger-var)
(check-sat) ;; check enabledness
(push)
;; encode -invariant
(check-sat) ;; check invariant
(pop)
(pop)

The double pop operation in the end will also pop the enabledness frame (and thus – afaict – any lemmas learned during that check). (Links on how popping affects learned lemmas: [1] [2])

It seems that we could leverage assumptions to retain the lemmas learned during the enabledness check: Z3 allows passing assumptions to (check-sat) that can selectively enable parts of the formula. The problem above would then turn into

;; ... prefix
(push)
;; translate transition to SMT
(check-sat transition-trigger-var) ;; check enabledness
(push)
;; encode -invariant
(check-sat) ;; check invariant
(pop)

That should retain the lemmas learned during the enabledness check in the solver.

Maybe we could even write out the whole BMC problem at once, and only selectively call check-sat on parts of the formula; this could help with repeated invariant checks.

Subtasks (details https://github.com/informalsystems/apalache/issues/2137#issuecomment-1403599317):

• [x] #2368
• [x] #2369
• [x] #2412
• [x] #2423
• [x] #2424

[thpani]

This is not a simple refactoring though; right now Z3SolverContext.sat() doesn’t know what it’s checking. We’d need some outside dependency (probably the transition executor?) to track what assumptions to pass.

[rodrigo7491]

Seems to be an interesting idea. After having a quick look about it, I wonder if this would allow us to use specialized solvers, as described here.

[konnov]

This is not a simple refactoring though; right now Z3SolverContext.sat() doesn’t know what it’s checking. We’d need some outside dependency (probably the transition executor?) to track what assumptions to pass.

I do not think this is actually hard to implement. You could extend sat with an optional list of predicates:

https://github.com/informalsystems/apalache/blob/b39ce05b2f8f51858d6ae5262fe5812a59e7ebaf/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala#L471-L483

Then you could keep track of the predicates in a set of TransitionExecutorImpl similar to:

https://github.com/informalsystems/apalache/blob/b39ce05b2f8f51858d6ae5262fe5812a59e7ebaf/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala#L32-L38

When you find that a transition is enabled, add its predicate to the set.

[konnov]

I think it is worth time-capping this effort with 3 days. This may have a significant impact on the performance. Worth experimenting!

[thpani]

I'd be interested in working on this after the retreat!

[thpani]

I've gotten a preliminary version of this to work.

However, it is failing integration tests Bug1136, TestSets, and TestBagsExt. The fault is related to constant propagation into an exponentation operator reported here: https://github.com/Z3Prover/z3/issues/6499

[konnov]

Even if some integration tests are failing, we can do a few preliminary experiments to see, whether we get performance improvements, as we expected.

[thpani]

Capturing the current status; there are two potential encodings to explore:

1. Conditionally enable each assertion with an assumption, but keep push and pop around. The hypothesis is that this can help the solver to select in-scope assertions (#2368).
2. Remove push/pop and fully control enabled portions via assumptions. This requires updates to the caching logic whenever the model-checking algorithm performs a logical push/pop to support a monolithic, assumption-controlled encoding. Operation of the caches is currently not well-documented, see #2362.

Thus, the plan going forward is to experimentally evaluate option (1), then make further decisions on (2).

[thpani]

As the current evaluation of (1) in #2369 is a bit inconclusive, @konnov suggested to benchmark in offline mode instead.

That should give us a full assumption-based encoding for further benchmarking, without the implementation friction of figuring out how to handle caches.

[thpani]

Findings from the preliminary benchmarks (#2424):

• assumptions + push/pop sometimes results in a speed-up, but we have to investigate when.
• assumptions only (without push/pop) is by far the slowest option. We can drop this direction.
• assumptions (in general) sometimes trip Z3, because of limits in the Z3 incremental solver's preprocessing

[thpani]

As discussed synchronously, I will shelve this issue for now.

Seems expedient to revisit when we have more time to investigate, and the latest when Z3's incremental preprocessing is improved.