CODEWITHSUNDEEP
pythonpython-3.xz3z3py
Inkane
Inkane

Reputation: 1500

Is it possible to query z3's Python API on whether a timeout occured?

I want to limit the time z3 can spend on some problem, which works by setting a timeout with:

from z3 import *
solver = Solver()
solver.set(timeout=60000)
# add constraints to solver
result = solver.check()

However, I'd like to check whether a timeout actually occurred. result is unknown in that case, but that might afaik also occur because the issue is not decidable (I'm using theories which are in general not decidable).

So, is there a way to find out whether a timeout has occurred?

Upvotes: 1

Views: 131

Answers (1)

alias
alias

Reputation: 30428

Sure, simply use the reason_unknown call:

from z3 import *
solver = Solver()
solver.set(timeout=1)
x, y = Ints('x y')
solver.add(x**y == x)
result = solver.check()
print result
print solver.reason_unknown()

This prints:

unknown
timeout

Upvotes: 2

Related Questions