Cadical with preprocessor and local search

This adds the option to enable Cadical's preprocessor and local search.  The
default remains unchanged.

The choice of preprocessor=1 and localsearch=0 for
satcheck_cadical_preprocessingt is motivated by the following data on the
HWMCC 2008 benchmarks:

0, 0: ./hwmcc08.sh  114.78s
1, 0: ./hwmcc08.sh  107.44s
2, 0: ./hwmcc08.sh  117.63s
5, 0: ./hwmcc08.sh  129.10s
1, 1: ./hwmcc08.sh  113.50s
5, 5: ./hwmcc08.sh  154.71s

Author: kroening

src/goto-checker/solver_factory.cpp

@@ -297,7 +297,8 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
     else if(solver_option == "cadical")
     {
 #if defined SATCHECK_CADICAL
-      return make_satcheck_prop<satcheck_cadicalt>(message_handler, options);
+      return make_satcheck_prop<satcheck_cadical_no_preprocessingt>(
+        message_handler, options);
 #else
       emit_solver_warning(message_handler, "cadical");
 #endif

src/solvers/sat/satcheck.h

@@ -137,8 +137,8 @@ typedef satcheck_glucose_no_simplifiert satcheck_no_simplifiert;
 
 #elif defined SATCHECK_CADICAL
 
-typedef satcheck_cadicalt satcheckt;
-typedef satcheck_cadicalt satcheck_no_simplifiert;
+typedef satcheck_cadical_no_preprocessingt satcheckt;
+typedef satcheck_cadical_no_preprocessingt satcheck_no_simplifiert;
 
 #endif
 

src/solvers/sat/satcheck_cadical.cpp

@@ -17,7 +17,7 @@ Author: Michael Tautschnig
 
 #  include <cadical.hpp>
 
-tvt satcheck_cadicalt::l_get(literalt a) const
+tvt satcheck_cadical_baset::l_get(literalt a) const
 {
   if(a.is_constant())
     return tvt(a.sign());
@@ -38,12 +38,12 @@ tvt satcheck_cadicalt::l_get(literalt a) const
   return result;
 }
 
-std::string satcheck_cadicalt::solver_text() const
+std::string satcheck_cadical_baset::solver_text() const
 {
   return std::string("CaDiCaL ") + solver->version();
 }
 
-void satcheck_cadicalt::lcnf(const bvt &bv)
+void satcheck_cadical_baset::lcnf(const bvt &bv)
 {
   for(const auto &lit : bv)
   {
@@ -85,7 +85,7 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_cadicalt::do_prop_solve(const bvt &assumptions)
+propt::resultt satcheck_cadical_baset::do_prop_solve(const bvt &assumptions)
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 
@@ -108,6 +108,12 @@ propt::resultt satcheck_cadicalt::do_prop_solve(const bvt &assumptions)
     if(!a.is_true())
       solver->assume(a.dimacs());
 
+  // set preprocessing and inprocessing limits
+  auto limit1_ret = solver->limit("preprocessing", preprocessing_limit);
+  CHECK_RETURN(limit1_ret);
+  auto limit2_ret = solver->limit("localsearch", localsearch_limit);
+  CHECK_RETURN(limit2_ret);
+
   switch(solver->solve())
   {
   case 10:
@@ -128,24 +134,30 @@ propt::resultt satcheck_cadicalt::do_prop_solve(const bvt &assumptions)
   return resultt::P_UNSATISFIABLE;
 }
 
-void satcheck_cadicalt::set_assignment(literalt a, bool value)
+void satcheck_cadical_baset::set_assignment(literalt a, bool value)
 {
   INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
   INVARIANT(false, "method not supported");
 }
 
-satcheck_cadicalt::satcheck_cadicalt(message_handlert &message_handler)
-  : cnf_solvert(message_handler), solver(new CaDiCaL::Solver())
+satcheck_cadical_baset::satcheck_cadical_baset(
+  int _preprocessing_limit,
+  int _localsearch_limit,
+  message_handlert &message_handler)
+  : cnf_solvert(message_handler),
+    solver(new CaDiCaL::Solver()),
+    preprocessing_limit(_preprocessing_limit),
+    localsearch_limit(_localsearch_limit)
 {
   solver->set("quiet", 1);
 }
 
-satcheck_cadicalt::~satcheck_cadicalt()
+satcheck_cadical_baset::~satcheck_cadical_baset()
 {
   delete solver;
 }
 
-bool satcheck_cadicalt::is_in_conflict(literalt a) const
+bool satcheck_cadical_baset::is_in_conflict(literalt a) const
 {
   return solver->failed(a.dimacs());
 }

src/solvers/sat/satcheck_cadical.h

@@ -19,11 +19,14 @@ namespace CaDiCaL // NOLINT(readability/namespace)
   class Solver; // NOLINT(readability/identifiers)
 }
 
-class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
+class satcheck_cadical_baset : public cnf_solvert, public hardness_collectort
 {
 public:
-  explicit satcheck_cadicalt(message_handlert &message_handler);
-  virtual ~satcheck_cadicalt();
+  satcheck_cadical_baset(
+    int preprocessing_limit,
+    int localsearch_limit,
+    message_handlert &);
+  virtual ~satcheck_cadical_baset();
 
   std::string solver_text() const override;
   tvt l_get(literalt a) const override;
@@ -46,6 +49,25 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
 
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver *solver;
+  int preprocessing_limit = 0, localsearch_limit = 0;
+};
+
+class satcheck_cadical_no_preprocessingt : public satcheck_cadical_baset
+{
+public:
+  explicit satcheck_cadical_no_preprocessingt(message_handlert &message_handler)
+    : satcheck_cadical_baset(0, 0, message_handler)
+  {
+  }
+};
+
+class satcheck_cadical_preprocessingt : public satcheck_cadical_baset
+{
+public:
+  explicit satcheck_cadical_preprocessingt(message_handlert &message_handler)
+    : satcheck_cadical_baset(1, 0, message_handler)
+  {
+  }
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H

unit/solvers/sat/satcheck_cadical.cpp

@@ -23,7 +23,7 @@ SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]")
 
   GIVEN("A satisfiable formula f")
   {
-    satcheck_cadicalt satcheck(message_handler);
+    satcheck_cadical_no_preprocessingt satcheck(message_handler);
     literalt f = satcheck.new_variable();
     satcheck.l_set_to_true(f);
 
@@ -42,7 +42,7 @@ SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]")
 
   GIVEN("An unsatisfiable formula f && !f")
   {
-    satcheck_cadicalt satcheck(message_handler);
+    satcheck_cadical_no_preprocessingt satcheck(message_handler);
     literalt f = satcheck.new_variable();
     satcheck.l_set_to_true(satcheck.land(f, !f));
 
@@ -54,7 +54,7 @@ SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]")
 
   GIVEN("An unsatisfiable formula false implied by a")
   {
-    satcheck_cadicalt satcheck(message_handler);
+    satcheck_cadical_no_preprocessingt satcheck(message_handler);
     literalt a = satcheck.new_variable();
     literalt a_implies_false = satcheck.lor(!a, const_literal(false));
     satcheck.l_set_to_true(a_implies_false);