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

tautschnig · tautschnig · commit 8fdb8bb8bd86 · 2023-02-04T16:15:17.000Z
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
`&lt;SOLVER&gt;`):
```
/usr/bin/time -v ../test.pl -e -c "../../../build/bin/cbmc &lt;SOLVER&gt;" \
  -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 `&lt;SOLVER&gt;`):
```
  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 `&lt;SOLVER&gt;`):
```
  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 `&lt;SOLVER&gt;`):
```
  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 `&lt;SOLVER&gt;`):
```
  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 `&lt;SOLVER&gt;`):
```
  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
```
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
