diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-06-29 23:01:56 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-01 19:55:16 +0000 |
| commit | 95e801681146eef6fce177e84701cddf1b822e23 (patch) | |
| tree | 0bcaf48a2ef5cf4a6f2740f6562a7634524c36a2 | |
| parent | 8cd60be654c60b1242ea7fc166b2f1a18c1a59c5 (diff) | |
| download | yosys-95e801681146eef6fce177e84701cddf1b822e23.tar.gz yosys-95e801681146eef6fce177e84701cddf1b822e23.tar.bz2 yosys-95e801681146eef6fce177e84701cddf1b822e23.zip | |
qbfsat: Clean up external executable command lines and update temporary directory name.
| -rw-r--r-- | passes/sat/qbfsat.cc | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index e4dfcaa0c..8a526ecbe 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -220,9 +220,13 @@ 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 = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2"; + 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 = yosys_smtbmc_exe + " -s " + (opt.get_solver_name()) + (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"; + 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(), + (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(), + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), + tempdir_name.c_str(), iter_num); Pass::call(mod->design, smt2_command); @@ -249,7 +253,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret, best_soln; - const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); + const std::string tempdir_name = make_temp_dir("/tmp/yosys-qbfsat-XXXXXX"); RTLIL::Module *module = mod; RTLIL::Design *design = module->design; std::string module_name = module->name.str(); |