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

smtio: Emit `mode: start` options before `set-logic` command and any other options after it. 

Refer to the SMT-LIB specification, section 4.1.7.  According to the spec, some options can only be specified in `start` mode.  Once the solver sees `set-logic`, it moves to `assert` mode.
This commit is contained in:
Alberto Gonzalez 2020-07-20 22:09:44 +00:00
parent 654864658f
commit 42fb75c570
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
backends/smt2/smtio.py
View File

@ -262,12 +262,19 @@ class SmtIo:
if self.produce_models: if self.produce_models:
self.write("(set-option :produce-models true)") self.write("(set-option :produce-models true)")
#See the SMT-LIB Standard, Section 4.1.7
modestart_options = [":global-declarations", ":interactive-mode", ":produce-assertions", ":produce-assignments", ":produce-models", ":produce-proofs", ":produce-unsat-assumptions", ":produce-unsat-cores", ":random-seed"]
for key, val in self.smt2_options.items():
if key in modestart_options:
self.write("(set-option {} {})".format(key, val))
self.write("(set-logic %s)" % self.logic) self.write("(set-logic %s)" % self.logic)
if self.forall and self.solver == "yices": if self.forall and self.solver == "yices":
self.write("(set-option :yices-ef-max-iters 1000000000)") self.write("(set-option :yices-ef-max-iters 1000000000)")
for key, val in self.smt2_options.items(): for key, val in self.smt2_options.items():
if key not in modestart_options:
self.write("(set-option {} {})".format(key, val)) self.write("(set-option {} {})".format(key, val))
def timestamp(self): def timestamp(self):