Merge pull request #804 from diffblue/cadical

add cadical solver option

.github/workflows/pull-request-checks.yaml

@@ -38,11 +38,11 @@ jobs:
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
-      - name: Get minisat
+      - name: Get cadical and minisat
         run: |
-          make -C lib/cbmc/src minisat2-download
+          make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
-        run: make -C src -j4 CXX="ccache g++"
+        run: make -C src -j4 CXX="ccache g++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run unit tests
         run: make -C unit -j4 CXX="ccache g++"
       - name: Run the ebmc tests with SAT

CHANGELOG

@@ -1,3 +1,7 @@
+# EBMC 5.4
+
+* BMC: Cadical support with --cadical
+
 # EBMC 5.3
 
 * SystemVerilog: fix for nets implicitly declared for port connections

src/ebmc/ebmc_parse_options.h

@@ -42,6 +42,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(interpolation-word)(interpolator):(bdd)"
         "(ranking-function):"
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
+        "(minisat)(cadical)"
         "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
         "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
         "(random-traces)(trace-steps):(random-seed):(traces):"

src/ebmc/ebmc_solver_factory.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/flattening/boolbv.h>
 #include <solvers/prop/prop.h>
 #include <solvers/sat/satcheck.h>
+#include <solvers/sat/satcheck_cadical.h>
+#include <solvers/sat/satcheck_minisat2.h>
 #include <solvers/smt2/smt2_dec.h>
 
 #include "ebmc_error.h"
@@ -136,17 +138,33 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
   else
   {
     // the 'default' solver
-    return [](const namespacet &ns, message_handlert &message_handler)
+    return [&cmdline](const namespacet &ns, message_handlert &message_handler)
     {
-      auto prop = std::unique_ptr<propt>(new satcheckt{message_handler});
+      std::unique_ptr<propt> sat_solver;
+
+      if(cmdline.isset("cadical"))
+      {
+#ifdef SATCHECK_CADICAL
+        sat_solver =
+          std::unique_ptr<propt>(new satcheck_cadicalt{message_handler});
+#else
+        throw ebmc_errort() << "support for Cadical not configured";
+#endif
+      }
+      else
+      {
+        sat_solver = std::unique_ptr<propt>(
+          new satcheck_minisat_simplifiert{message_handler});
+      }
 
       messaget message(message_handler);
-      message.status() << "Using " << prop->solver_text() << messaget::eom;
+      message.status() << "Using " << sat_solver->solver_text()
+                       << messaget::eom;
 
       auto dec = std::unique_ptr<stack_decision_proceduret>(
-        new boolbvt{ns, *prop, message_handler});
+        new boolbvt{ns, *sat_solver, message_handler});
 
-      return ebmc_solvert{std::move(prop), std::move(dec)};
+      return ebmc_solvert{std::move(sat_solver), std::move(dec)};
     };
   }
 }