From 9847a4eea8b6d758c06d3d95f2bfe84c57774364 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 1 May 2020 23:17:35 +0000 Subject: [PATCH] smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. --- backends/smt2/smtbmc.py | 5 ++-- backends/smt2/smtio.py | 35 ++++++++++++++++++++-- passes/sat/qbfsat.cc | 66 +++++++++++++++++++++++++++++++++-------- 3 files changed, 88 insertions(+), 18 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..d24fbf809 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 @@ -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 pass as command line argument to the solver + --timeout + set the solver timeout to the specified value (in seconds). + --logic use the specified SMT2 logic (e.g. QF_AUFBV) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 712a46cbc..d6dbf8ef4 100644 --- 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 &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 \n"); log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); log("\n"); + log(" -timeout \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"); } -- 2.30.2