Skip to content

SMT back-end: add support for Bitwuzla and CVC 5 #7519

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 4, 2023
Merged

SMT back-end: add support for Bitwuzla and CVC 5 #7519

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions doc/man/cbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -419,6 +422,9 @@ use CVC3
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
\fB\-\-mathsat\fR
use MathSAT
.TP
Expand Down
6 changes: 6 additions & 0 deletions doc/man/jbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -413,6 +416,9 @@ use CVC3
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
\fB\-\-mathsat\fR
use MathSAT
.TP
Expand Down
18 changes: 17 additions & 1 deletion src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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"))
Expand Down Expand Up @@ -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;
Expand All @@ -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(
Expand Down
4 changes: 3 additions & 1 deletion src/goto-checker/solver_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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):" \
Expand All @@ -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" \
Expand Down
20 changes: 20 additions & 0 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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;

Expand Down Expand Up @@ -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;
Expand Down
2 changes: 2 additions & 0 deletions src/solvers/smt2/smt2_conv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions src/solvers/smt2/smt2_dec.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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":
Expand Down Expand Up @@ -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;
Expand All @@ -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
Expand Down