Merge pull request #2018 from boqwxp/qbfsat-timeout

smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.

2 files changed, 31 insertions, 5 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index cc3ebb129..03f001bfd 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1557,8 +1557,9 @@ else:  # not tempind, covermode
                 smt_assert(get_constr_expr(constr_asserts, i))
 
             print_msg("Solving for step %d.." % (last_check_step))
-            if smt_check_sat() != "sat":
-                print("%s No solution found!" % smt.timestamp())
+            status = smt_check_sat()
+            if status != "sat":
+                print("%s No solution found! (%s)" % (smt.timestamp(), status))
                 retstatus = "FAILED"
                 break
 
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 62dfe7c11..9f7c8c6d9 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -121,6 +121,7 @@ class SmtIo:
         self.logic_bv = True
         self.logic_dt = False
         self.forall = False
+        self.timeout = 0
         self.produce_models = True
         self.smt2cache = [list()]
         self.p = None
@@ -135,6 +136,7 @@ class SmtIo:
             self.debug_file = opts.debug_file
             self.dummy_file = opts.dummy_file
             self.timeinfo = opts.timeinfo
+            self.timeout = opts.timeout
             self.unroll = opts.unroll
             self.noincr = opts.noincr
             self.info_stmts = opts.info_stmts
@@ -147,6 +149,7 @@ class SmtIo:
             self.debug_file = None
             self.dummy_file = None
             self.timeinfo = os.name != "nt"
+            self.timeout = 0
             self.unroll = False
             self.noincr = False
             self.info_stmts = list()
@@ -176,18 +179,28 @@ class SmtIo:
                 self.popen_vargs = ['yices-smt2'] + self.solver_opts
             else:
                 self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
+            if self.timeout != 0:
+                self.popen_vargs.append('-t')
+                self.popen_vargs.append('%d' % self.timeout);
 
         if self.solver == "z3":
             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
+            if self.timeout != 0:
+                self.popen_vargs.append('-T:%d' % self.timeout);
 
         if self.solver == "cvc4":
             if self.noincr:
                 self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
             else:
                 self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+            if self.timeout != 0:
+                self.popen_vargs.append('--tlimit=%d000' % self.timeout);
 
         if self.solver == "mathsat":
             self.popen_vargs = ['mathsat'] + self.solver_opts
+            if self.timeout != 0:
+                print('timeout option is not supported for mathsat.')
+                sys.exit(1)
 
         if self.solver == "boolector":
             if self.noincr:
@@ -195,6 +208,9 @@ class SmtIo:
             else:
                 self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
             self.unroll = True
+            if self.timeout != 0:
+                print('timeout option is not supported for boolector.')
+                sys.exit(1)
 
         if self.solver == "abc":
             if len(self.solver_opts) > 0:
@@ -204,6 +220,9 @@ class SmtIo:
             self.logic_ax = False
             self.unroll = True
             self.noincr = True
+            if self.timeout != 0:
+                print('timeout option is not supported for abc.')
+                sys.exit(1)
 
         if self.solver == "dummy":
             assert self.dummy_file is not None
@@ -710,7 +729,7 @@ class SmtIo:
 
         if self.forall:
             result = self.read()
-            while result not in ["sat", "unsat", "unknown"]:
+            while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]:
                 print("%s %s: %s" % (self.timestamp(), self.solver, result))
                 result = self.read()
         else:
@@ -721,7 +740,7 @@ class SmtIo:
             print("(check-sat)", file=self.debug_file)
             self.debug_file.flush()
 
-        if result not in ["sat", "unsat"]:
+        if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]:
             if result == "":
                 print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
             else:
@@ -931,7 +950,7 @@ class SmtIo:
 class SmtOpts:
     def __init__(self):
         self.shortopts = "s:S:v"
-        self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
+        self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
         self.solver = "yices"
         self.solver_opts = list()
         self.debug_print = False
@@ -940,6 +959,7 @@ class SmtOpts:
         self.unroll = False
         self.noincr = False
         self.timeinfo = os.name != "nt"
+        self.timeout = 0
         self.logic = None
         self.info_stmts = list()
         self.nocomments = False
@@ -949,6 +969,8 @@ class SmtOpts:
             self.solver = a
         elif o == "-S":
             self.solver_opts.append(a)
+        elif o == "--timeout":
+            self.timeout = int(a)
         elif o == "-v":
             self.debug_print = True
         elif o == "--unroll":
@@ -980,6 +1002,9 @@ class SmtOpts:
     -S <opt>
         pass <opt> as command line argument to the solver
 
+    --timeout <value>
+        set the solver timeout to the specified value (in seconds).
+
     --logic <smt2_logic>
         use the specified SMT2 logic (e.g. QF_AUFBV)