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)