push and pop

[sswen0427]

Do POP and PUSH operations speed up the solution of Z3 ?
For example,there are constraints A,B,C,D,E
case 1:I add constraints A,B,C,D to the solver, then I pop the constraint D and push the constraint E, the time of solving the constraints A,B,C,E as t1
case 2:I add directly constraints A,B,C,E,the time of solving the constraints A,B,C,E as t2
Which is bigger,t1 or t2?

[NikolajBjorner]

It totally depends on use case. You have to try out on representative samples from your use case.
push/pop can amortize some overhead, but then also prevent some global simplifications.

[sswen0427]

By doing push/pop, my execution time has doubled, so why is the incremental solution slower ? Do you have any suggestions for me ? Thank you!!

[aytey]

so why is the incremental solution slower ?

I think @NikolajBjorner gave you the answer above:

it is often because the non-incremental mode can leverage much more powerful pre-processing

If you're not solving incrementally, then it means Z3 can apply some powerful rewrites to the whole SMT instance---which may be "destructive" in terms of reducing your assertions---while maintaining equisatisfiability.

When you turn on incremental solving, these same destructive rewrites may not be applicable: you could add something later on that could lead to a destructive rewrite, but because Z3 doesn't know if you will later remove that new assertion, it cannot be "break" the the original assertion.

In non-incremental mode, Z3 knows nothing is ever going to get "removed" so it can be as destructive as it likes (always retaining equisatisfiability).

Think about something like (assert (> x 10)) followed by (assert (= x 11)) -- Z3 can rewrite this to true via (to use a programming language term) constant propagation. However, if (assert (= x 11)) is "poppable", then (assert (> x 10)) cannot be rewritten "globally".

[sswen0427]

I see. It really help me a lot . Thank you . Thank you. Thank you.

[rainoftime]

It depends on the theory type you use.
For instance, for pure bit-vector constraints, the incremental solver and the non-incremental solver use different pre-processing and "backend engines".
No double the performance is different.
In my experience, the non-incremental bit-vector solver is usually faster.
However, for linear integer arithmetic, the incremental solver seems to work very well.

BTW,
in newer versions of Z3,
@NikolajBjorner may change the "backend engine" of the incremental bit-vector solver. It might work better

[sswen0427]

I am a beginner in z3, can you recommend me some scientific articles about the working principle of z3? I'd like to get a quick overview of how the z3 works. please. @NikolajBjorner