From 654864658f17a26d760995462e57481ff81b037c Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Jul 2020 20:04:56 +0000 Subject: smtio: Add support for parsing `yosys-smt2-solver-option` info statements. --- backends/smt2/smtio.py | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 4ac437c36..6191eabf6 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -124,6 +124,7 @@ class SmtIo: self.timeout = 0 self.produce_models = True self.smt2cache = [list()] + self.smt2_options = dict() self.p = None self.p_index = solvers_index solvers_index += 1 @@ -258,14 +259,17 @@ class SmtIo: for stmt in self.info_stmts: self.write(stmt) - if self.forall and self.solver == "yices": - self.write("(set-option :yices-ef-max-iters 1000000000)") - if self.produce_models: self.write("(set-option :produce-models true)") 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): secs = int(time() - self.start_time) return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60) @@ -468,6 +472,9 @@ class SmtIo: fields = stmt.split() + if fields[1] == "yosys-smt2-solver-option": + self.smt2_options[fields[2]] = fields[3] + if fields[1] == "yosys-smt2-nomem": if self.logic is None: self.logic_ax = False -- cgit v1.2.3 From 42fb75c57092714fce0394817154cdd5d63e9d2b Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Mon, 20 Jul 2020 22:09:44 +0000 Subject: 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. --- backends/smt2/smtio.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 6191eabf6..516091011 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -262,13 +262,20 @@ class SmtIo: if self.produce_models: 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) 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)) + if key not in modestart_options: + self.write("(set-option {} {})".format(key, val)) def timestamp(self): secs = int(time() - self.start_time) -- cgit v1.2.3