Skip to content

Commit

Permalink
Merge pull request #2018 from boqwxp/qbfsat-timeout
Browse files Browse the repository at this point in the history 
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
  • Loading branch information
@clairexen
clairexen authored May 30, 2020
2 parents 0a14e1e + ea30465 commit ea46ed8
Show file tree
Hide file tree
Showing 3 changed files with 84 additions and 18 deletions.
5 changes: 3 additions & 2 deletions backends/smt2/smtbmc.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1557,8 +1557,9 @@ def smt_check_sat():
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

Expand Down
31 changes: 28 additions & 3 deletions backends/smt2/smtio.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,7 @@ def __init__(self, opts=None):
self.logic_bv = True
self.logic_dt = False
self.forall = False
self.timeout = 0
self.produce_models = True
self.smt2cache = [list()]
self.p = None
Expand All @@ -135,6 +136,7 @@ def __init__(self, opts=None):
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
Expand All @@ -147,6 +149,7 @@ def __init__(self, opts=None):
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()
Expand Down Expand Up @@ -176,25 +179,38 @@ def setup(self):
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:
self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
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:
Expand All @@ -204,6 +220,9 @@ def setup(self):
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
Expand Down Expand Up @@ -710,7 +729,7 @@ def check_sat(self):

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:
Expand All @@ -721,7 +740,7 @@ def check_sat(self):
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:
Expand Down Expand Up @@ -931,7 +950,7 @@ def wait(self):
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
Expand All @@ -940,6 +959,7 @@ def __init__(self):
self.unroll = False
self.noincr = False
self.timeinfo = os.name != "nt"
self.timeout = 0
self.logic = None
self.info_stmts = list()
self.nocomments = False
Expand All @@ -949,6 +969,8 @@ def handle(self, o, a):
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":
Expand Down Expand Up @@ -980,6 +1002,9 @@ def helpmsg(self):
-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)
Expand Down
66 changes: 53 additions & 13 deletions passes/sat/qbfsat.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,15 @@ 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;
size_t argidx;
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) {
Expand All @@ -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
Expand All @@ -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);
Expand Down Expand Up @@ -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);

Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
}
Expand Down

0 comments on commit ea46ed8

Please sign in to comment.