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

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index cc3ebb1295fa63ce9f1424450fb3546d3c67d05d..03f001bfd0952cb28e5652c594e631e979c123bf 100644 (file)
--- 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 62dfe7c1156db87dbb2813d5b15ee9d8f415ccb4..d24fbf8096a8215c5540d18c6c6e046432cab49a 100644 (file)
--- 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
@@ -449,6 +468,10 @@ class SmtIo:
 
         fields = stmt.split()
 
+        if fields[1] == "yosys-smt2-timeout":
+            self.timeout = int(fields[2])
+            assert self.timeout > 0
+
         if fields[1] == "yosys-smt2-nomem":
             if self.logic is None:
                 self.logic_ax = False
@@ -710,7 +733,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 +744,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 +954,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 +963,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 +973,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 +1006,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)
 

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 712a46cbc36370b387e0989f066afdd10cfca3e1..d6dbf8ef4924a9fa1dec0ec2bffb08f949a3df5d 100644 (file)
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -42,6 +42,7 @@ struct QbfSolveOptions {
        bool nooptimize, nobisection;
        bool sat, unsat, show_smtbmc;
        enum Solver{Z3, Yices, CVC4} solver;
+       int timeout;
        std::string specialize_soln_file;
        std::string write_soln_soln_file;
        std::string dump_final_smt2_file;
@@ -49,7 +50,7 @@ struct QbfSolveOptions {
        QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
                        nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
                        nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
-                       solver(Yices), argidx(0) {};
+                       solver(Yices), timeout(0), argidx(0) {};
 };
 
 std::string get_solver_name(const QbfSolveOptions &opt) {
@@ -67,6 +68,11 @@ std::string get_solver_name(const QbfSolveOptions &opt) {
 void recover_solution(QbfSolutionType &sol) {
        YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
        YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+       YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
+       YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
+       YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
+       YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
+       YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
        YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
        YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
 #ifndef NDEBUG
@@ -87,14 +93,40 @@ void recover_solution(QbfSolutionType &sol) {
 #endif
                        sol.hole_to_value[loc] = val;
                }
-               else if (YS_REGEX_NS::regex_search(x, sat_regex))
+               else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
                        sat_regex_found = true;
-               else if (YS_REGEX_NS::regex_search(x, unsat_regex))
+                       sol.sat = true;
+                       sol.unknown = false;
+               }
+               else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
                        unsat_regex_found = true;
+                       sol.sat = false;
+                       sol.unknown = false;
+               }
                else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
                        sol.unknown = true;
                        log_warning("solver ran out of memory\n");
                }
+               else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
+                       sol.unknown = true;
+                       log_warning("solver timed out\n");
+               }
+               else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
+                       sol.unknown = true;
+                       log_warning("solver timed out\n");
+               }
+               else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
+                       sol.unknown = true;
+                       log_warning("solver returned \"unknown\"\n");
+               }
+               else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
+                       unsat_regex_found = true;
+                       sol.sat = false;
+                       sol.unknown = false;
+               }
+               else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
+                       sol.unknown = true;
+               }
        }
 #ifndef NDEBUG
        log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
@@ -329,7 +361,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
        const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
        const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
        const std::string smtbmc_warning = "z3: WARNING:";
-       const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
+       const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
 
        Pass::call(mod->design, smt2_command);
 
@@ -344,14 +376,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
        };
        log_header(mod->design, "Solving QBF-SAT problem.\n");
        if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str());
-       int retval = run_command(smtbmc_cmd, process_line);
-       if (retval == 0) {
-               ret.sat = true;
-               ret.unknown = false;
-       } else if (retval == 1) {
-               ret.sat = false;
-               ret.unknown = false;
-       }
+       run_command(smtbmc_cmd, process_line);
 
        recover_solution(ret);
        return ret;
@@ -514,6 +539,19 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
                        }
                        continue;
                }
+               else if (args[opt.argidx] == "-timeout") {
+                       if (args.size() <= opt.argidx + 1)
+                               log_cmd_error("timeout not specified.\n");
+                       else {
+                               int timeout = atoi(args[opt.argidx+1].c_str());
+                               if (timeout > 0)
+                                       opt.timeout = timeout;
+                               else
+                                       log_cmd_error("timeout must be greater than 0.\n");
+                               opt.argidx++;
+                       }
+                       continue;
+               }
                else if (args[opt.argidx] == "-sat") {
                        opt.sat = true;
                        continue;
@@ -625,6 +663,9 @@ struct QbfSatPass : public Pass {
                log("    -solver <solver>\n");
                log("        Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
                log("\n");
+               log("    -timeout <value>\n");
+               log("        Set the per-iteration timeout in seconds.\n");
+               log("\n");
                log("    -sat\n");
                log("        Generate an error if the solver does not return \"sat\".\n");
                log("\n");
@@ -672,7 +713,6 @@ struct QbfSatPass : public Pass {
                        QbfSolutionType ret = qbf_solve(module, opt);
                        module = design->module(module_name);
                        if (ret.unknown) {
-                               log_warning("solver did not give an answer\n");
                                if (opt.sat || opt.unsat)
                                        log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
                        }