CODEWITHSUNDEEP
optimizationtimeoutz3
谭思危
谭思危

Reputation: 11

How to specify soft timeout in z3py

z3 has "-t" to set the soft timeout (in milli seconds). But when I use z3 in Python, I cannot set "-t" through "set_option" or "Optimize.set" API.

I try all the following methods. But it does not work.

opt = Optimize()
set_option("soft timeout, 600)
set_option("opt.soft_timeout", True)  # 600 s
opt.set("t", 60 * 1000)
opt.set("soft_timeout", True)
opt.set("soft timeout", True)
opt.set("smt.soft_timeout", True)

Please tell me how to set "-t" in the Python API of z3.

Upvotes: 1

Views: 49

Answers (1)

alias
alias

Reputation: 30525

Use set as a method of the opt class. Something like this:

from z3 import *

opt = Optimize()
opt.set("timeout", 600)

I'm not sure if the parameter itself is called timeout, you need to double-check what it is really called. Otherwise the above syntax should work.

Upvotes: 0

Related Questions