mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 19:52:31 +00:00
Code Activity

qbfsat support for cvc5, fixes #3608

Browse source
This commit is contained in:
Miodrag Milanovic 2023-01-09 16:14:01 +01:00
parent f2c689403a
commit e3c0fd8b10
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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