riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smtio: Add support for parsing `yosys-smt2-solver-option` info statements.

This commit is contained in:
Alberto Gonzalez 2020-07-01 20:04:56 +00:00
parent 2f786fcfac
commit 654864658f
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
backends/smt2/smtio.py
View File

@ -124,6 +124,7 @@ class SmtIo:
self.timeout = 0 self.timeout = 0
self.produce_models = True self.produce_models = True
self.smt2cache = [list()] self.smt2cache = [list()]
self.smt2_options = dict()
self.p = None self.p = None
self.p_index = solvers_index self.p_index = solvers_index
solvers_index += 1 solvers_index += 1
@ -258,14 +259,17 @@ class SmtIo:
for stmt in self.info_stmts: for stmt in self.info_stmts:
self.write(stmt) self.write(stmt)
if self.forall and self.solver == "yices":
self.write("(set-option :yices-ef-max-iters 1000000000)")
if self.produce_models: if self.produce_models:
self.write("(set-option :produce-models true)") self.write("(set-option :produce-models true)")
self.write("(set-logic %s)" % self.logic) self.write("(set-logic %s)" % self.logic)
if self.forall and self.solver == "yices":
self.write("(set-option :yices-ef-max-iters 1000000000)")
for key, val in self.smt2_options.items():
self.write("(set-option {} {})".format(key, val))
def timestamp(self): def timestamp(self):
secs = int(time() - self.start_time) secs = int(time() - self.start_time)
return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60) return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
@ -468,6 +472,9 @@ class SmtIo:
fields = stmt.split() fields = stmt.split()
if fields[1] == "yosys-smt2-solver-option":
self.smt2_options[fields[2]] = fields[3]
if fields[1] == "yosys-smt2-nomem": if fields[1] == "yosys-smt2-nomem":
if self.logic is None: if self.logic is None:
self.logic_ax = False self.logic_ax = False