Merge pull request #7519 from tautschnig/feature/bitwuzla-cvc5

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

Author: kroening

Diff for: 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 for: 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 for: 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 for: 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 for: 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 for: 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 for: 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