mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.

Browse source
This commit is contained in:
Alberto Gonzalez 2020-05-01 23:17:35 +00:00
parent f9eef5e3f7
commit 9847a4eea8
No known key found for this signature in database
GPG key ID: 8395A8BA109708B2
3 changed files with 88 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
backends/smt2/smtbmc.py
View file

@ -1557,8 +1557,9 @@ else: # not tempind, covermode
smt_assert(get_constr_expr(constr_asserts, i))
print_msg("Solving for step %d.." % (last_check_step))
if smt_check_sat() != "sat":
print("%s No solution found!" % smt.timestamp())
status = smt_check_sat()
if status != "sat":
print("%s No solution found! (%s)" % (smt.timestamp(), status))
retstatus = "FAILED"
break

35
backends/smt2/smtio.py
View file

@ -121,6 +121,7 @@ class SmtIo:
self.logic_bv = True
self.logic_dt = False
self.forall = False
self.timeout = 0
self.produce_models = True
self.smt2cache = [list()]
self.p = None
@ -135,6 +136,7 @@ class SmtIo:
self.debug_file = opts.debug_file
self.dummy_file = opts.dummy_file
self.timeinfo = opts.timeinfo
self.timeout = opts.timeout
self.unroll = opts.unroll
self.noincr = opts.noincr
self.info_stmts = opts.info_stmts
@ -147,6 +149,7 @@ class SmtIo:
self.debug_file = None
self.dummy_file = None
self.timeinfo = os.name != "nt"
self.timeout = 0
self.unroll = False
self.noincr = False
self.info_stmts = list()
@ -176,18 +179,28 @@ class SmtIo:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
if self.timeout != 0:
self.popen_vargs.append('-t')
self.popen_vargs.append('%d' % self.timeout);
if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
if self.timeout != 0:
self.popen_vargs.append('-T:%d' % self.timeout);
if self.solver == "cvc4":
if self.noincr:
self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
else:
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
if self.timeout != 0:
self.popen_vargs.append('--tlimit=%d000' % self.timeout);
if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] + self.solver_opts
if self.timeout != 0:
print('timeout option is not supported for mathsat.')
sys.exit(1)
if self.solver == "boolector":
if self.noincr:
@ -195,6 +208,9 @@ class SmtIo:
else:
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
self.unroll = True
if self.timeout != 0:
print('timeout option is not supported for boolector.')
sys.exit(1)
if self.solver == "abc":
if len(self.solver_opts) > 0:
@ -204,6 +220,9 @@ class SmtIo:
self.logic_ax = False
self.unroll = True
self.noincr = True
if self.timeout != 0:
print('timeout option is not supported for abc.')
sys.exit(1)
if self.solver == "dummy":
assert self.dummy_file is not None
@ -449,6 +468,10 @@ class SmtIo:
fields = stmt.split()
if fields[1] == "yosys-smt2-timeout":
self.timeout = int(fields[2])
assert self.timeout > 0
if fields[1] == "yosys-smt2-nomem":
if self.logic is None:
self.logic_ax = False
@ -710,7 +733,7 @@ class SmtIo:
if self.forall:
result = self.read()
while result not in ["sat", "unsat", "unknown"]:
while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]:
print("%s %s: %s" % (self.timestamp(), self.solver, result))
result = self.read()
else:
@ -721,7 +744,7 @@ class SmtIo:
print("(check-sat)", file=self.debug_file)
self.debug_file.flush()
if result not in ["sat", "unsat"]:
if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]:
if result == "":
print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
else:
@ -931,7 +954,7 @@ class SmtIo:
class SmtOpts:
def __init__(self):
self.shortopts = "s:S:v"
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "yices"
self.solver_opts = list()
self.debug_print = False
@ -940,6 +963,7 @@ class SmtOpts:
self.unroll = False
self.noincr = False
self.timeinfo = os.name != "nt"
self.timeout = 0
self.logic = None
self.info_stmts = list()
self.nocomments = False
@ -949,6 +973,8 @@ class SmtOpts:
self.solver = a
elif o == "-S":
self.solver_opts.append(a)
elif o == "--timeout":
self.timeout = int(a)
elif o == "-v":
self.debug_print = True
elif o == "--unroll":
@ -980,6 +1006,9 @@ class SmtOpts:
-S <opt>
pass <opt> as command line argument to the solver
--timeout <value>
set the solver timeout to the specified value (in seconds).
--logic <smt2_logic>
use the specified SMT2 logic (e.g. QF_AUFBV)