From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Wed, 1 Jul 2020 20:04:56 +0000 (+0000)
Subject: smtio: Add support for parsing `yosys-smt2-solver-option` info statements.
X-Git-Tag: working-ls180~368^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=654864658f17a26d760995462e57481ff81b037c;p=yosys.git

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

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