Introduce a new --sat-solver option to allow selecting the backend SAT solver

Author: zhassan-aws

doc/man/cbmc.1

@@ -388,6 +388,9 @@ enable caching of repeated dereferences
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
 .TP
+\fB\-\-sat\-solver\fR solver
+use specified SAT solver
+.TP
 \fB\-\-external\-sat\-solver\fR cmd
 command to invoke SAT solver process
 .TP

doc/man/jbmc.1

@@ -382,6 +382,9 @@ enable caching of repeated dereferences
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
 .TP
+\fB\-\-sat\-solver\fR solver
+use specified SAT solver
+.TP
 \fB\-\-external\-sat\-solver\fR \fIcmd\fR
 command to invoke SAT solver process
 .TP

regression/cbmc/sat-solver-error/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = 0;
+  assert(x * y == y);
+  return 0;
+}

regression/cbmc/sat-solver-error/test.desc

@@ -0,0 +1,7 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend paths-lifo-expected-failure
+test.c
+--sat-solver non-existing-solver
+^EXIT=1$
+^SIGNAL=0$
+unknown solver 'non-existing-solver'
+--

regression/cbmc/sat-solver-warning/test.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = x;
+  x /= 2;
+  y /= 2;
+  assert(x == y);
+  return 0;
+}

regression/cbmc/sat-solver-warning/test.desc

@@ -0,0 +1,9 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend 
+test.c
+--sat-solver lingeling
+^EXIT=0$
+^SIGNAL=0$
+The specified solver, 'lingeling', is not available\. The default solver will be used instead\.
+\[main\.assertion\.1] line \d+ assertion x == y: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/sat-solver/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = x / 2;
+  assert(y != x);
+  assert(y <= x);
+  return 0;
+}

regression/cbmc/sat-solver/test.desc

@@ -0,0 +1,10 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend 
+test.c
+--sat-solver cadical
+^EXIT=10$
+^SIGNAL=0$
+Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
+\[main\.assertion\.1] line \d+ assertion y != x: FAILURE
+\[main\.assertion\.2] line \d+ assertion y <= x: SUCCESS
+^VERIFICATION FAILED$
+--

regression/validate-trace-xml-schema/check.py

@@ -42,6 +42,7 @@
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],
     ['unknown-argument-suggestion', 'test.desc'],
+    ['sat-solver-error', 'test.desc'],
     # this one produces XML intermingled with main XML output when used with --xml-ui
     ['graphml_witness2', 'test.desc'],
     # these are producing coverage goals which aren't included in the schema

src/goto-checker/solver_factory.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/cmdline.h>
 #include <util/exception_utils.h>
+#include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/message.h>
 #include <util/options.h>
@@ -151,7 +152,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
     return get_incremental_smt2(incremental_smt2_solver);
   if(options.get_bool_option("smt2"))
     return get_smt2(get_smt2_solver_type());
-  return get_default();
+  return get_sat_solver();
 }
 
 /// Uses the options to pick an SMT 2.0 solver
@@ -213,20 +214,148 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
   return satcheck;
 }
 
-std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
+std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_sat_solver()
 {
   auto solver = util_make_unique<solvert>();
-  if(
-    options.get_bool_option("beautify") ||
-    !options.get_bool_option("sat-preprocessor")) // no simplifier
+  bool solver_set = false;
+  if(options.is_set("sat-solver"))
   {
-    // simplifier won't work with beautification
-    solver->set_prop(
-      make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
+    const std::string &solver_option = options.get_option("sat-solver");
+    if(solver_option == "zchaff")
+    {
+#if defined SATCHECK_ZCHAFF
+      solver->set_prop(
+        make_satcheck_prop<satcheck_zchafft>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("zchaff");
+#endif
+    }
+    else if(solver_option == "booleforce")
+    {
+#if defined SATCHECK_BOOLERFORCE
+      solver->set_prop(
+        make_satcheck_prop<satcheck_booleforcet>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("booleforce");
+#endif
+    }
+    else if(solver_option == "minisat1")
+    {
+#if defined SATCHECK_MINISAT1
+      solver->set_prop(
+        make_satcheck_prop<satcheck_minisat1t>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("minisat1");
+#endif
+    }
+    else if(solver_option == "minisat2")
+    {
+#if defined SATCHECK_MINISAT2
+      if(
+        options.get_bool_option("beautify") ||
+        !options.get_bool_option("sat-preprocessor")) // no simplifier
+      {
+        // simplifier won't work with beautification
+        solver->set_prop(make_satcheck_prop<satcheck_minisat_no_simplifiert>(
+          message_handler, options));
+      }
+      else // with simplifier
+      {
+        solver->set_prop(make_satcheck_prop<satcheck_minisat_simplifiert>(
+          message_handler, options));
+      }
+      solver_set = true;
+#else
+      emit_solver_warning("minisat2");
+#endif
+    }
+    else if(solver_option == "ipasir")
+    {
+#if defined SATCHECK_IPASIR
+      solver->set_prop(
+        make_satcheck_prop<satcheck_ipasirt>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("ipasir");
+#endif
+    }
+    else if(solver_option == "picosat")
+    {
+#if defined SATCHECK_PICOSAT
+      solver->set_prop(
+        make_satcheck_prop<satcheck_picosatt>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("picosat");
+#endif
+    }
+    else if(solver_option == "lingeling")
+    {
+#if defined SATCHECK_LINGELING
+      solver->set_prop(
+        make_satcheck_prop<satcheck_lingelingt>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("lingeling");
+#endif
+    }
+    else if(solver_option == "glucose")
+    {
+#if defined SATCHECK_GLUCOSE
+      if(
+        options.get_bool_option("beautify") ||
+        !options.get_bool_option("sat-preprocessor")) // no simplifier
+      {
+        // simplifier won't work with beautification
+        solver->set_prop(make_satcheck_prop<satcheck_glucose_no_simplifiert>(
+          message_handler, options));
+      }
+      else // with simplifier
+      {
+        solver->set_prop(make_satcheck_prop<satcheck_glucose_simplifiert>(
+          message_handler, options));
+      }
+      solver_set = true;
+#else
+      emit_solver_warning("glucose");
+#endif
+    }
+    else if(solver_option == "cadical")
+    {
+#if defined SATCHECK_CADICAL
+      solver->set_prop(
+        make_satcheck_prop<satcheck_cadicalt>(message_handler, options));
+      solver_set = true;
+#else
+      emit_solver_warning("cadical");
+#endif
+    }
+    else
+    {
+      messaget log(message_handler);
+      log.error() << "unknown solver '" << solver_option << "'"
+                  << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
   }
-  else // with simplifier
+  if(!solver_set)
   {
-    solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
+    // default solver
+    if(
+      options.get_bool_option("beautify") ||
+      !options.get_bool_option("sat-preprocessor")) // no simplifier
+    {
+      // simplifier won't work with beautification
+      solver->set_prop(
+        make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
+    }
+    else // with simplifier
+    {
+      solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
+    }
   }
 
   bool get_array_constraints =
@@ -245,6 +374,14 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
   return solver;
 }
 
+void solver_factoryt::emit_solver_warning(const std::string &solver)
+{
+  messaget log(message_handler);
+  log.warning() << "The specified solver, '" << solver
+                << "', is not available. "
+                << "The default solver will be used instead." << messaget::eom;
+}
+
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
 {
   no_beautification();
@@ -517,6 +654,9 @@ static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
 
   if(cmdline.isset("dimacs"))
     options.set_option("dimacs", true);
+
+  if(cmdline.isset("sat-solver"))
+    options.set_option("sat-solver", cmdline.get_value("sat-solver"));
 }
 
 static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)

src/goto-checker/solver_factory.h

@@ -70,7 +70,7 @@ class solver_factoryt final
   message_handlert &message_handler;
   const bool output_xml_in_refinement;
 
-  std::unique_ptr<solvert> get_default();
+  std::unique_ptr<solvert> get_sat_solver();
   std::unique_ptr<solvert> get_dimacs();
   std::unique_ptr<solvert> get_external_sat();
   std::unique_ptr<solvert> get_bv_refinement();
@@ -89,6 +89,9 @@ class solver_factoryt final
   // consistency checks during solver creation
   void no_beautification();
   void no_incremental_check();
+
+  // emit a warning for non-existent solver
+  void emit_solver_warning(const std::string &solver);
 };
 
 /// Parse solver-related command-line parameters in \p cmdline and set
@@ -104,6 +107,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(mathsat)"                                                                  \
   "(cprover-smt2)"                                                             \
   "(incremental-smt2-solver):"                                                 \
+  "(sat-solver):"                                                              \
   "(external-sat-solver):"                                                     \
   "(no-sat-preprocessor)"                                                      \
   "(beautify)"                                                                 \
@@ -126,6 +130,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   " --smt2                       use default SMT2 solver (Z3)\n"               \
   " --bitwuzla                   use Bitwuzla\n"                               \
   " --boolector                  use Boolector\n"                              \
+  " --sat-solver solver          use specified SAT solver\n"                   \
   " --cprover-smt2               use CPROVER SMT2 solver\n"                    \
   " --cvc3                       use CVC3\n"                                   \
   " --cvc4                       use CVC4\n"                                   \