diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index c405c795c11..49384614555 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -407,6 +407,9 @@ use default SMT1 solver (obsolete) \fB\-\-smt2\fR use default SMT2 solver (Z3) .TP +\fB\-\-bitwuzla\fR +use Bitwuzla +.TP \fB\-\-boolector\fR use Boolector .TP @@ -419,6 +422,9 @@ use CVC3 \fB\-\-cvc4\fR use CVC4 .TP +\fB\-\-cvc5\fR +use CVC5 +.TP \fB\-\-mathsat\fR use MathSAT .TP diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index d64fb48eea4..8620e2e648b 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -401,6 +401,9 @@ use default SMT1 solver (obsolete) \fB\-\-smt2\fR use default SMT2 solver (Z3) .TP +\fB\-\-bitwuzla\fR +use Boolector +.TP \fB\-\-boolector\fR use Boolector .TP @@ -413,6 +416,9 @@ use CVC3 \fB\-\-cvc4\fR use CVC4 .TP +\fB\-\-cvc5\fR +use CVC5 +.TP \fB\-\-mathsat\fR use MathSAT .TP diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 88213e5efe6..7a88b886ca6 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -163,7 +163,9 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const smt2_dect::solvert s = smt2_dect::solvert::GENERIC; - if(options.get_bool_option("boolector")) + if(options.get_bool_option("bitwuzla")) + s = smt2_dect::solvert::BITWUZLA; + else if(options.get_bool_option("boolector")) s = smt2_dect::solvert::BOOLECTOR; else if(options.get_bool_option("cprover-smt2")) s = smt2_dect::solvert::CPROVER_SMT2; @@ -173,6 +175,8 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const s = smt2_dect::solvert::CVC3; else if(options.get_bool_option("cvc4")) s = smt2_dect::solvert::CVC4; + else if(options.get_bool_option("cvc5")) + s = smt2_dect::solvert::CVC5; else if(options.get_bool_option("yices")) s = smt2_dect::solvert::YICES; else if(options.get_bool_option("z3")) @@ -525,6 +529,12 @@ static void parse_smt2_options(const cmdlinet &cmdline, optionst &options) bool solver_set = false; + if(cmdline.isset("bitwuzla")) + { + options.set_option("bitwuzla", true), solver_set = true; + options.set_option("smt2", true); + } + if(cmdline.isset("boolector")) { options.set_option("boolector", true), solver_set = true; @@ -549,6 +559,12 @@ static void parse_smt2_options(const cmdlinet &cmdline, optionst &options) options.set_option("smt2", true); } + if(cmdline.isset("cvc5")) + { + options.set_option("cvc5", true), solver_set = true; + options.set_option("smt2", true); + } + if(cmdline.isset("incremental-smt2-solver")) { options.set_option( diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index 3e4b13c9714..b9507f5a149 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -100,7 +100,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options); "(smt2)" \ "(fpa)" \ "(cvc3)" \ - "(cvc4)(boolector)(yices)(z3)" \ + "(cvc4)(cvc5)(bitwuzla)(boolector)(yices)(z3)" \ "(mathsat)" \ "(cprover-smt2)" \ "(incremental-smt2-solver):" \ @@ -124,10 +124,12 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options); " (greedy heuristic)\n" \ " --smt1 use default SMT1 solver (obsolete)\n" \ " --smt2 use default SMT2 solver (Z3)\n" \ + " --bitwuzla use Bitwuzla\n" \ " --boolector use Boolector\n" \ " --cprover-smt2 use CPROVER SMT2 solver\n" \ " --cvc3 use CVC3\n" \ " --cvc4 use CVC4\n" \ + " --cvc5 use CVC5\n" \ " --mathsat use MathSAT\n" \ " --yices use Yices\n" \ " --z3 use Z3\n" \ diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 5bfbed784cc..839b164ee0a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -83,6 +83,15 @@ smt2_convt::smt2_convt( case solvert::GENERIC: break; + case solvert::BITWUZLA: + use_FPA_theory = true; + use_array_of_bool = true; + use_as_const = true; + use_check_sat_assuming = true; + use_lambda_for_array = true; + emit_set_logic = false; + break; + case solvert::BOOLECTOR: break; @@ -103,6 +112,15 @@ smt2_convt::smt2_convt( use_as_const = true; break; + case solvert::CVC5: + logic = "ALL"; + use_array_of_bool = true; + use_as_const = true; + use_check_sat_assuming = true; + use_lambda_for_array = true; + use_datatypes = true; + break; + case solvert::MATHSAT: break; @@ -158,11 +176,13 @@ void smt2_convt::write_header() { // clang-format off case solvert::GENERIC: break; + case solvert::BITWUZLA: out << "; Generated for Bitwuzla\n"; break; case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break; case solvert::CPROVER_SMT2: out << "; Generated for the CPROVER SMT2 solver\n"; break; case solvert::CVC3: out << "; Generated for CVC 3\n"; break; case solvert::CVC4: out << "; Generated for CVC 4\n"; break; + case solvert::CVC5: out << "; Generated for CVC 5\n"; break; case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break; case solvert::YICES: out << "; Generated for Yices\n"; break; case solvert::Z3: out << "; Generated for Z3\n"; break; diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index bf51bfde940..2a2e1f3b098 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -39,10 +39,12 @@ class smt2_convt : public stack_decision_proceduret enum class solvert { GENERIC, + BITWUZLA, BOOLECTOR, CPROVER_SMT2, CVC3, CVC4, + CVC5, MATHSAT, YICES, Z3 diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index f9fe70dc950..ddfe31dfb97 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -20,10 +20,12 @@ std::string smt2_dect::decision_procedure_text() const // clang-format off return "SMT2 " + logic + (use_FPA_theory ? " (with FPA)" : "") + " using " + (solver==solvert::GENERIC?"Generic": + solver==solvert::BITWUZLA?"Bitwuzla": solver==solvert::BOOLECTOR?"Boolector": solver==solvert::CPROVER_SMT2?"CPROVER SMT2": solver==solvert::CVC3?"CVC3": solver==solvert::CVC4?"CVC4": + solver==solvert::CVC5?"CVC5": solver==solvert::MATHSAT?"MathSAT": solver==solvert::YICES?"Yices": solver==solvert::Z3?"Z3": @@ -54,6 +56,10 @@ decision_proceduret::resultt smt2_dect::dec_solve() switch(solver) { + case solvert::BITWUZLA: + argv = {"bitwuzla", temp_file_problem()}; + break; + case solvert::BOOLECTOR: argv = {"boolector", "--smt2", temp_file_problem(), "-m"}; break; @@ -79,6 +85,10 @@ decision_proceduret::resultt smt2_dect::dec_solve() argv = {"cvc4", "-L", "smt2", temp_file_problem()}; break; + case solvert::CVC5: + argv = {"cvc5", "--lang", "smtlib", temp_file_problem()}; + break; + case solvert::MATHSAT: // The options below were recommended by Alberto Griggio // on 10 July 2013