Merge pull request #2215 from boqwxp/qbfsat-solver-options

qbfsat, smt2, smtio: Add `-solver-option` to allow specifying SMT-LIBv2 `(set-option ...)` commands

1 files changed, 17 insertions, 3 deletions

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