diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-06-29 04:41:18 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-20 21:54:56 +0000 |
| commit | 2f786fcfacfadfba7b4080a8016c7efa3ac4bd13 (patch) | |
| tree | 0190b951e378818cc52ebf47c3836839149c6007 | |
| parent | f0379853371bfcf9217c3c0de15b3927b6f09e44 (diff) | |
| download | yosys-2f786fcfacfadfba7b4080a8016c7efa3ac4bd13.tar.gz yosys-2f786fcfacfadfba7b4080a8016c7efa3ac4bd13.tar.bz2 yosys-2f786fcfacfadfba7b4080a8016c7efa3ac4bd13.zip | |
qbfsat: Add `-solver-option` option.
| -rw-r--r-- | passes/sat/qbfsat.cc | 15 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 1 |
2 files changed, 15 insertions, 1 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 46f7f5070..6db7d4b64 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -215,7 +215,6 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; - const std::string smt2_command = stringf("write_smt2 -stbv -wires %s/problem%d.smt2", tempdir_name.c_str(), iter_num); const std::string smtbmc_warning = "z3: WARNING:"; const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(), @@ -223,6 +222,10 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), tempdir_name.c_str(), iter_num); + std::string smt2_command = "write_smt2 -stbv -wires "; + for (auto &solver_opt : opt.solver_options) + smt2_command += stringf("-solver-option %s %s ", solver_opt.first.c_str(), solver_opt.second.c_str()); + smt2_command += stringf("%s/problem%d.smt2", tempdir_name.c_str(), iter_num); Pass::call(mod->design, smt2_command); auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) { @@ -419,6 +422,13 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { } continue; } + else if (args[opt.argidx] == "-solver-option") { + if (args.size() <= opt.argidx + 2) + log_cmd_error("solver option name and value not fully specified.\n"); + opt.solver_options.emplace(args[opt.argidx+1], args[opt.argidx+2]); + opt.argidx += 2; + continue; + } else if (args[opt.argidx] == "-timeout") { if (args.size() <= opt.argidx + 1) log_cmd_error("timeout not specified.\n"); @@ -533,6 +543,9 @@ struct QbfSatPass : public Pass { log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); log(" (default: yices)\n"); log("\n"); + log(" -solver-option <name> <value>\n"); + log(" Set the specified solver option in the SMT-LIBv2 problem file.\n"); + log("\n"); log(" -timeout <value>\n"); log(" Set the per-iteration timeout in seconds.\n"); log(" (default: no timeout)\n"); diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h index 401f9c7a6..c96c6f818 100644 --- a/passes/sat/qbfsat.h +++ b/passes/sat/qbfsat.h @@ -31,6 +31,7 @@ struct QbfSolveOptions { bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; enum Solver{Z3, Yices, CVC4} solver = Yices; enum OptimizationLevel{O0, O1, O2} oflag = O0; + dict<std::string, std::string> solver_options; int timeout = 0; std::string specialize_soln_file = ""; std::string write_soln_soln_file = ""; |