riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3615 from YosysHQ/qbfsat_cvc5 

qbfsat support for cvc5, fixes #3608
This commit is contained in:
Miodrag Milanović 2023-01-10 11:38:16 +01:00 committed by GitHub
parent f2c689403a e3c0fd8b10
commit 2b622258a2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
passes/sat/qbfsat.cc
View File

@ -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");

4
passes/sat/qbfsat.h
View File

@ -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 "";