CODEWITHSUNDEEP
z3z3py
Venkatesh-Prasad Ranganath
Venkatesh-Prasad Ranganath

Reputation: 1886

Why does z3.check() slow when it is immediately preceded by z3.push()?

The below Python snippet illustrates a strage performance behavior of Z3. Without push() call, the z3 checks the formula in 0.1s. With push() (and no extra assertions), z3 takes 0.8s. A similar outcome occurs even after swapping s.append(f) and s.push().

import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)

Any idea why does this slowdown occur? And, how can it be addressed?

I'm using z3-4.3.2.bb56885147e4-x64-osx-10.9.2.

Upvotes: 4

Views: 1024

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Your example uses "push" in the second instantiation. This makes a huge difference. Z3's bit-vector solver is (not yet) amenable to incremental use over the API. It works only for stand-along assertions and does not interoperate with scopes (push/pop). The first invocation uses the bit-vector SAT solver. There is no "push/pop" going on. The second invocation follows a call to "push". Z3 then determines that in order to track scope dependencies it has to use the incremental SMT core, which does not benefit from the more efficient bit-vector solver.

Upvotes: 5

Related Questions