diff options
| author | Miodrag Milanovic <mmicko@gmail.com> | 2023-01-09 16:14:01 +0100 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2023-01-09 16:14:01 +0100 |
| commit | e3c0fd8b1031de5e7d1a4d263452c4245e3fe32d (patch) | |
| tree | a983dc25405f959abc44ae607cd11b3278162032 /passes | |
| parent | f2c689403ace0637b7455bac8f1e8d4bc312e74f (diff) | |
| download | yosys-e3c0fd8b1031de5e7d1a4d263452c4245e3fe32d.tar.gz yosys-e3c0fd8b1031de5e7d1a4d263452c4245e3fe32d.tar.bz2 yosys-e3c0fd8b1031de5e7d1a4d263452c4245e3fe32d.zip | |
qbfsat support for cvc5, fixes #3608
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/sat/qbfsat.cc | 6 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 4580f194e..42d3e188a 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -416,6 +416,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.solver = opt.Solver::Yices; else if (args[opt.argidx+1] == "cvc4") opt.solver = opt.Solver::CVC4; + else if (args[opt.argidx+1] == "cvc5") + opt.solver = opt.Solver::CVC5; else log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); opt.argidx++; @@ -542,8 +544,8 @@ struct QbfSatPass : public Pass { log(" hope that the solver supports optimizing quantified bitvector problems.\n"); log("\n"); log(" -solver <solver>\n"); - log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); - log(" (default: yices)\n"); + log(" Use a particular solver. Choose one of: \"z3\", \"yices\", \"cvc4\"\n"); + log(" and \"cvc5\". (default: yices)\n"); log("\n"); log(" -solver-option <name> <value>\n"); log(" Set the specified solver option in the SMT-LIBv2 problem file.\n"); diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h index c96c6f818..8fb6093bc 100644 --- a/passes/sat/qbfsat.h +++ b/passes/sat/qbfsat.h @@ -29,7 +29,7 @@ struct QbfSolveOptions { bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false; bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false; bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; - enum Solver{Z3, Yices, CVC4} solver = Yices; + enum Solver{Z3, Yices, CVC4, CVC5} solver = Yices; enum OptimizationLevel{O0, O1, O2} oflag = O0; dict<std::string, std::string> solver_options; int timeout = 0; @@ -45,6 +45,8 @@ struct QbfSolveOptions { return "yices"; else if (solver == Solver::CVC4) return "cvc4"; + else if (solver == Solver::CVC5) + return "cvc5"; log_cmd_error("unknown solver specified.\n"); return ""; |