mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Merge pull request #2017 from boqwxp/qbfsat-cvc4

Browse source 
qbfsat: Add support for CVC4.
This commit is contained in:
clairexen 2020-05-29 16:23:10 +02:00 committed by GitHub
parent 1c8d5a08a0 f9eef5e3f7
commit 5874a14d65
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
passes/sat/qbfsat.cc
View file

@ -41,7 +41,7 @@ struct QbfSolveOptions {
bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
bool nooptimize, nobisection; bool nooptimize, nobisection;
bool sat, unsat, show_smtbmc; bool sat, unsat, show_smtbmc;
enum Solver{Z3, Yices} solver; enum Solver{Z3, Yices, CVC4} solver;
std::string specialize_soln_file; std::string specialize_soln_file;
std::string write_soln_soln_file; std::string write_soln_soln_file;
std::string dump_final_smt2_file; std::string dump_final_smt2_file;
@ -57,6 +57,8 @@ std::string get_solver_name(const QbfSolveOptions &opt) {
return "z3"; return "z3";
else if (opt.solver == opt.Solver::Yices) else if (opt.solver == opt.Solver::Yices)
return "yices"; return "yices";
else if (opt.solver == opt.Solver::CVC4)
return "cvc4";
else else
log_cmd_error("unknown solver specified.\n"); log_cmd_error("unknown solver specified.\n");
return ""; return "";
@ -504,6 +506,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
opt.solver = opt.Solver::Z3; opt.solver = opt.Solver::Z3;
else if (args[opt.argidx+1] == "yices") else if (args[opt.argidx+1] == "yices")
opt.solver = opt.Solver::Yices; opt.solver = opt.Solver::Yices;
else if (args[opt.argidx+1] == "cvc4")
opt.solver = opt.Solver::CVC4;
else else
log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str());
opt.argidx++; opt.argidx++;
@ -619,7 +623,7 @@ struct QbfSatPass : public Pass {
log(" quantified bitvector problems.\n"); log(" quantified bitvector problems.\n");
log("\n"); log("\n");
log(" -solver <solver>\n"); log(" -solver <solver>\n");
log(" Use a particular solver. Choose one of: \"z3\", \"yices\".\n"); log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
log("\n"); log("\n");
log(" -sat\n"); log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n"); log(" Generate an error if the solver does not return \"sat\".\n");