How does an incremental solution work in Z3?

Question

I have a question about how the Z3 gradually solves problems. After reading some answers here, I found the following:

• There are two ways to use Z3 for an incremental solution: one is push / pop (stack) mode, the other is assumptions. Soft / hard restrictions in Z3 .
• In stack mode, z3 will forget all the studied lemmas in the global field (am I right?) Even after one local “pop” Efficiency of reinforcing constraints in SMT solvers
• In assumptions mode (I don’t know the name, this is the name that comes to my mind), z3 will not simplify some formulas, for example. spread of meaning. on demand z3 behavior change for unsat core

I made some comparison (you can request formulas, they are just too big to put 4fun on growth), but here are my observations: according to some formulas, including quantifiers, the assumption mode is faster. In some formulas with a large number of logical variables (assumption variables), the stack mode is faster than the assumption mode.

Are they carried out for specific purposes? How does an incremental solution work in Z3?

Answer 1

Yes, there are essentially two additional modes.

Stack Based: Using push (), pop (), you create a local context following the stack discipline. Assertions added under push () are deleted after pop () is matched. In addition, any lemmas that are generated by clicking are deleted. Use push () / pop () to emulate a state freeze and add additional restrictions on the frozen state, and then return to the frozen state. This has the advantage of freeing up all additional memory overhead (for example, the lemmas studied) created within push (). The working assumption is that the lemma under study will not be useful anymore.

Based on assumptions: using additional assumption literals passed to check () / check_sat (), you can (1) retrieve unsatisfactory kernels over assumption literals, (2) get local increment without garbage collectors, which are obtained regardless of assumptions. In other words, if Z3 is studying a lemma that does not contain any literary assumptions, it expects them not to be garbage collected. To make good use of assumption literals, you will also have to add them to formulas. Thus, the trade-off is that the provisions used with the assumptions contain some amount of inflation. For example, if you want to take some formula (<= xy) locally, then you add a sentence (=> p (<= xy)) and take p when you call the check_sat () function. Note that the original assumption was one. Z3 effectively distributes units. With wording that uses assumption literals, it is no longer a unit at the basic search level. This leads to additional overhead. Units become binary sentences, binary sentences become triple sentences, etc.

Differentiation between the push / pop function is performed for the SMT Z3 module by default. This is the engine that most formulas will use. Z3 contains several engine portfolios. For example, for clean tasks with bit vectors, Z3 may end up using a syntax mechanism. The increment in the processor is implemented differently than the default engine. Here, increment is implemented using assumption literals. Any statement that you add to the push scope is validated as the implication (=> scope_literals) formula. check_sat () in such a scope will have to deal with guess literals. On the other hand, any consequence (lemma) that does not depend on the current volume is not garbage collection in pop ().

In optimization mode, when you approve optimization goals or when you use optimization objects by API, you can also call push / pop. Similarly with fixed points. For these two functions, push / pop is essentially for user convenience. There is no internal increment. The reason is that these two modes use substantial pre-processing, which is super non-incremental.