diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-05-01 08:12:23 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-05-25 20:39:03 +0000 |
| commit | f9eef5e3f710684c8cfe5430190b5cf4f7c2e34e (patch) | |
| tree | efcbeb5fac832eb2f3f2d934feb2e07d25dcf5db /passes/sat | |
| parent | 54570a39780f750aa7bfd616f12c58bcf121bbdf (diff) | |
| download | yosys-f9eef5e3f710684c8cfe5430190b5cf4f7c2e34e.tar.gz yosys-f9eef5e3f710684c8cfe5430190b5cf4f7c2e34e.tar.bz2 yosys-f9eef5e3f710684c8cfe5430190b5cf4f7c2e34e.zip | |
qbfsat: Add support for CVC4.
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/qbfsat.cc | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 5ec20d621..712a46cbc 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -41,7 +41,7 @@ struct QbfSolveOptions { bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; bool nooptimize, nobisection; bool sat, unsat, show_smtbmc; - enum Solver{Z3, Yices} solver; + enum Solver{Z3, Yices, CVC4} solver; std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; @@ -57,6 +57,8 @@ std::string get_solver_name(const QbfSolveOptions &opt) { return "z3"; else if (opt.solver == opt.Solver::Yices) return "yices"; + else if (opt.solver == opt.Solver::CVC4) + return "cvc4"; else log_cmd_error("unknown solver specified.\n"); return ""; @@ -504,6 +506,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.solver = opt.Solver::Z3; else if (args[opt.argidx+1] == "yices") opt.solver = opt.Solver::Yices; + else if (args[opt.argidx+1] == "cvc4") + opt.solver = opt.Solver::CVC4; else log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); opt.argidx++; @@ -619,7 +623,7 @@ struct QbfSatPass : public Pass { log(" quantified bitvector problems.\n"); log("\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(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); |