From 8fdb8bb8bd862bf82744da2af2134756c411c4e6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 4 Feb 2023 16:15:17 +0000 Subject: [PATCH] SMT back-end: add support for Bitwuzla and CVC 5 Adds support for two actively developed SMT solvers, with the caveat that these do not currently pass all regression tests (Bitwuzla fails two tests, CVC 5 times out on one and fails on nine others). Some performance data running (in `regression/cbmc`, for varying values of ``): ``` /usr/bin/time -v ../test.pl -e -c "../../../build/bin/cbmc " \ -X broken-smt-backend -X thorough-smt-backend \ -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \ -X broken-z3-smt-backend -X thorough-z3-smt-backend ``` Note that the following data has bias: it only has the subset of tests that all back-ends are expected to be able to solve. That is, some SMT solver may be faster on this minimum common set of tests, but might be unable to solve tests that another (possibly slower) solver can handle. * Bitwuzla (`--bitwuzla` for ``): ``` User time (seconds): 90.59 System time (seconds): 8.68 Elapsed (wall clock) time (h:mm:ss or m:ss): 1:39.31 Maximum resident set size (kbytes): 81240 Exit status: 2 ``` * CVC 5 (`--cvc5` for ``): ``` User time (seconds): 483.24 System time (seconds): 10.69 Elapsed (wall clock) time (h:mm:ss or m:ss): 8:14.18 Maximum resident set size (kbytes): 473876 Exit status: 10 ``` * Z3 (`--z3` for ``): ``` User time (seconds): 202.90 System time (seconds): 11.29 Elapsed (wall clock) time (h:mm:ss or m:ss): 3:34.21 Maximum resident set size (kbytes): 131760 Exit status: 0 ``` * In-tree SMT solver (`--cprover-smt2` for ``): ``` User time (seconds): 64.08 System time (seconds): 9.44 Elapsed (wall clock) time (h:mm:ss or m:ss): 1:13.51 Maximum resident set size (kbytes): 81932 Exit status: 0 ``` * SAT back-end (omitting ``): ``` User time (seconds): 33.43 System time (seconds): 7.94 Elapsed (wall clock) time (h:mm:ss or m:ss): 0:41.29 Maximum resident set size (kbytes): 79088 Exit status: 0 ``` --- doc/man/cbmc.1 | 6 ++++++ doc/man/jbmc.1 | 6 ++++++ src/goto-checker/solver_factory.cpp | 18 +++++++++++++++++- src/goto-checker/solver_factory.h | 4 +++- src/solvers/smt2/smt2_conv.cpp | 20 ++++++++++++++++++++ src/solvers/smt2/smt2_conv.h | 2 ++ src/solvers/smt2/smt2_dec.cpp | 10 ++++++++++ 7 files changed, 64 insertions(+), 2 deletions(-) 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