4

I am running Z3 on UFBV queries. Currently the query contains 2 calls check-sat. If I put push 1 just after check-sat, Z3 solves the query in 30sec. If I don't put any push 1 at all, thus have two calls check-sat without any push 1 between them, then Z3 solves it in 200sec. Interesting. Any specific reasons or just a coincidence?

Ayrat
  • 1,221
  • 1
  • 18
  • 36

1 Answers1

7

Z3 3.x has a "strategy specification language" based on tactics and tacticals. I'm not "advertising" that yet because it is working in progress. The basic idea is described in this slide deck. We have a different built-in strategy for each logic. The strategies usually do not support incremental solving, because they may apply transformations that use a "closed-world" assumption. Example, we have transformations that map 0-1 linear integer arithmetic into SAT. Whenever Z3 detects that the user "wants" incremental solving (e.g., multiple check-sat commands, push&pop commands), it switches to a general purpose solver. In future versions, we will provide more features for controlling Z3 behavior.

BTW, if you have two consecutive (check-sat) (check-sat) commands, Z3 not necessarily enters in incremental mode. It will enter only if there is an assert or push command between the two calls.

Now, suppose your query is of the form: (check-sat) <assertions> (check-sat), and your second query is of the form (check-sat) <assertions> (push) (check-sat). In both cases, Z3 will be in incremental mode in the second (check-sat). However, the behavior is still not the same. The incremental solver "compiles" the asserted formulas to an internal format, and its behavior is affected if a push command has been executed. For example, it will use a more efficient encoding of binary clauses only if there is no user scope. By user scope, I mean, the number of push commands - number of pop commands. It does that because the data-structure used in the more efficient encoding does not have an efficient undo/inverse operation.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Both versions of the query are incremental. The difference is in having `push`. Non incremental query is solved in 8sec.) Does `push` change tactics? Or it is due to different _program flow_ in case of push? (e.g. additional copying that could change order of constraints..) – Ayrat Feb 03 '12 at 17:58
  • Z3 automatically assumes it is in incremental mode if `push` is used. – Leonardo de Moura Feb 03 '12 at 18:10
  • Yes, I see your point, Leo. But Z3 assumes both queries to be incremental (since in the first - 2 calls to `check-sat`, in the second - 2 calls to `check-sat` and also `push`. So..what is the difference?:) – Ayrat Feb 05 '12 at 14:32
  • I see, you are comparing `(check-sat) ... (check-sat)` with `(check-sat) ... (push) (check-sat)`. I will update the answer. – Leonardo de Moura Feb 05 '12 at 15:47