diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 13 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 20 |
2 files changed, 30 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 526b36352..a79c0bd99 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1387,6 +1387,10 @@ struct Smt2Backend : public Backend { log(" use the given template file. the line containing only the token '%%%%'\n"); log(" is replaced with the regular output of this command.\n"); log("\n"); + log(" -solver-option <option> <value>\n"); + log(" emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n"); + log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n"); + log("\n"); log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n"); log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n"); log("\n"); @@ -1441,6 +1445,7 @@ struct Smt2Backend : public Backend { std::ifstream template_f; bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false; bool forallmode = false; + dict<std::string, std::string> solver_options; log_header(design, "Executing SMT2 backend.\n"); @@ -1484,6 +1489,11 @@ struct Smt2Backend : public Backend { verbose = true; continue; } + if (args[argidx] == "-solver-option" && argidx+2 < args.size()) { + solver_options.emplace(args[argidx+1], args[argidx+2]); + argidx += 2; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -1514,6 +1524,9 @@ struct Smt2Backend : public Backend { if (statedt) *f << stringf("; yosys-smt2-stdt\n"); + for (auto &it : solver_options) + *f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str()); + std::vector<RTLIL::Module*> sorted_modules; // extract module dependencies diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 4ac437c36..516091011 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,24 @@ 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)") + #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(): + if key not in modestart_options: + 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 +479,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 |