cprover: add external SMT2 solver backend (--smt2-solver)

src/cprover/counterexample_found.cpp

@@ -14,13 +14,17 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/cout_message.h>
 #include <util/simplify_expr.h>
 
+#include <solvers/decision_procedure.h>
 #include <solvers/sat/satcheck.h>
 
 #include "axioms.h"
 #include "bv_pointers_wide.h"
+#include "cprover_smt2_dec.h"
 #include "simplify_state_expr.h"
 #include "state.h"
 
+#include <memory>
+
 void show_assignment(const bv_pointers_widet &solver)
 {
 #if 0
@@ -56,6 +60,11 @@ void show_assignment(const bv_pointers_widet &solver)
 #endif
 }
 
+void show_assignment(const decision_proceduret &)
+{
+  // no-op: debug output not available for generic decision procedures
+}
+
 static exprt evaluator_rec(
   const std::unordered_map<exprt, exprt, irep_hash> &memory,
   const decision_proceduret &solver,
@@ -106,7 +115,7 @@ static exprt evaluator(
 propertyt::tracet counterexample(
   const std::vector<framet> &frames,
   const workt &work,
-  const bv_pointers_widet &solver,
+  const decision_proceduret &solver,
   const axiomst &axioms,
   const namespacet &ns)
 {
@@ -175,7 +184,8 @@ std::optional<propertyt::tracet> counterexample_found(
   const workt &work,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &ns)
+  const namespacet &ns,
+  const std::string &smt2_solver_binary)
 {
   auto &f = frames[work.frame.index];
 
@@ -185,8 +195,28 @@ std::optional<propertyt::tracet> counterexample_found(
     {
       cout_message_handlert message_handler;
       message_handler.set_verbosity(verbose ? 10 : 1);
-      satcheckt satcheck(message_handler);
-      bv_pointers_widet solver(ns, satcheck, message_handler);
+
+      std::unique_ptr<decision_proceduret> solver_ptr;
+      std::unique_ptr<satcheckt> satcheck_ptr;
+      std::unique_ptr<bv_pointers_widet> bv_ptr;
+
+      if(!smt2_solver_binary.empty())
+      {
+        solver_ptr = std::make_unique<cprover_smt2_dect>(
+          ns, smt2_solver_binary, message_handler);
+      }
+      else
+      {
+        satcheck_ptr = std::make_unique<satcheckt>(message_handler);
+        bv_ptr = std::make_unique<bv_pointers_widet>(
+          ns, *satcheck_ptr, message_handler);
+      }
+
+      decision_proceduret &solver =
+        smt2_solver_binary.empty()
+          ? static_cast<decision_proceduret &>(*bv_ptr)
+          : static_cast<decision_proceduret &>(*solver_ptr);
+
       axiomst axioms(solver, address_taken, verbose, ns);
 
       // These are initial states, i.e., initial_state(ς) ⇒ SInitial(ς).
@@ -198,12 +228,12 @@ std::optional<propertyt::tracet> counterexample_found(
       switch(solver())
       {
       case decision_proceduret::resultt::D_SATISFIABLE:
-        if(verbose)
-          show_assignment(solver);
         return counterexample(frames, work, solver, axioms, ns);
       case decision_proceduret::resultt::D_UNSATISFIABLE:
         break;
       case decision_proceduret::resultt::D_ERROR:
+        if(!smt2_solver_binary.empty())
+          break; // conservatively treat as no counterexample found
         throw "error reported by solver";
       }
     }

src/cprover/counterexample_found.h

@@ -14,17 +14,21 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "solver_types.h"
 
+#include <string>
 #include <unordered_set>
 
 std::optional<propertyt::tracet> counterexample_found(
   const std::vector<framet> &,
   const workt &,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &);
+  const namespacet &,
+  const std::string &smt2_solver_binary = "");
 
 class bv_pointers_widet;
+class decision_proceduret;
 
 void show_assignment(const bv_pointers_widet &);
+void show_assignment(const decision_proceduret &);
 
 #endif // CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H

src/cprover/cprover_parse_options.cpp

@@ -277,6 +277,8 @@ int cprover_parse_optionst::main()
 
     solver_options.trace = cmdline.isset("trace");
     solver_options.verbose = cmdline.isset("verbose");
+    solver_options.smt2_solver_binary =
+      cmdline.isset("smt2-solver") ? cmdline.get_value("smt2-solver") : "";
 
     // solve
     auto result = state_encoding_solver(

src/cprover/cprover_parse_options.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, dkr@amazon.com
   "(safety)(no-safety)(no-assertions)"                                         \
   "(contract):"                                                                \
   "(solve)(unwind):(trace)"                                                    \
+  "(smt2-solver):"                                                             \
   "(inline)(no-inline)"                                                        \
   "D:I:"                                                                       \
   "(32)(64)"                                                                   \

src/cprover/cprover_smt2_dec.h

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: SMT2 decision procedure for cprover state encoding
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPROVER_CPROVER_SMT2_DEC_H
+#define CPROVER_CPROVER_CPROVER_SMT2_DEC_H
+
+#include <solvers/smt2/smt2_dec.h>
+
+/// SMT2 decision procedure configured for cprover's state encoding.
+/// Uses datatypes for structs (instead of bitvector flattening) to
+/// support mathematical types (integer, real, string).
+class cprover_smt2_dect : public smt2_dect
+{
+public:
+  cprover_smt2_dect(
+    const namespacet &_ns,
+    const std::string &_solver_binary,
+    message_handlert &_message_handler)
+    : smt2_dect(
+        _ns,
+        "",
+        "cprover",
+        "ALL",
+        smt2_convt::solvert::GENERIC,
+        _solver_binary,
+        _message_handler)
+  {
+    use_array_of_bool = true;
+    use_as_const = true;
+    use_datatypes = true;
+  }
+};
+
+#endif // CPROVER_CPROVER_CPROVER_SMT2_DEC_H

src/cprover/inductiveness.cpp

@@ -20,12 +20,14 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "axioms.h"
 #include "bv_pointers_wide.h"
 #include "counterexample_found.h"
+#include "cprover_smt2_dec.h"
 #include "propagate.h"
 #include "solver.h"
 
 #include <algorithm>
 #include <iomanip>
 #include <iostream>
+#include <memory>
 
 bool is_subsumed(
   const std::unordered_set<exprt, irep_hash> &a1,
@@ -34,7 +36,8 @@ bool is_subsumed(
   const exprt &b,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &ns)
+  const namespacet &ns,
+  const std::string &smt2_solver_binary)
 {
   if(b == true)
     return true; // anything subsumes 'true'
@@ -51,8 +54,30 @@ bool is_subsumed(
 #else
   message_handler.set_verbosity(1);
 #endif
-  satcheckt satcheck(message_handler);
-  bv_pointers_widet solver(ns, satcheck, message_handler);
+
+  std::unique_ptr<decision_proceduret> solver_ptr;
+  if(!smt2_solver_binary.empty())
+  {
+    solver_ptr = std::make_unique<cprover_smt2_dect>(
+      ns, smt2_solver_binary, message_handler);
+  }
+
+  // SAT solver objects (only used when not using SMT2)
+  std::unique_ptr<satcheckt> satcheck_ptr;
+  std::unique_ptr<bv_pointers_widet> bv_ptr;
+  if(smt2_solver_binary.empty())
+  {
+    satcheck_ptr = std::make_unique<satcheckt>(message_handler);
+    bv_ptr =
+      std::make_unique<bv_pointers_widet>(ns, *satcheck_ptr, message_handler);
+    solver_ptr = nullptr;
+  }
+
+  decision_proceduret &solver =
+    smt2_solver_binary.empty()
+      ? static_cast<decision_proceduret &>(*bv_ptr)
+      : static_cast<decision_proceduret &>(*solver_ptr);
+
   axiomst axioms(solver, address_taken, verbose, ns);
 
   // check if a => b is valid,
@@ -82,6 +107,8 @@ bool is_subsumed(
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     return true;
   case decision_proceduret::resultt::D_ERROR:
+    if(!smt2_solver_binary.empty())
+      return false; // conservatively treat unknown/error as not subsumed
     throw "error reported by solver";
   }
 
@@ -173,7 +200,8 @@ inductiveness_resultt inductiveness_check(
                 invariant,
                 address_taken,
                 solver_options.verbose,
-                ns))
+                ns,
+                solver_options.smt2_solver_binary))
       {
         if(solver_options.verbose)
           std::cout << "subsumed " << format(invariant) << '\n';
@@ -231,7 +259,12 @@ inductiveness_resultt inductiveness_check(
 #endif
 
     auto counterexample_found = ::counterexample_found(
-      frames, work, address_taken, solver_options.verbose, ns);
+      frames,
+      work,
+      address_taken,
+      solver_options.verbose,
+      ns,
+      solver_options.smt2_solver_binary);
 
     if(counterexample_found)
     {

src/cprover/solver.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_CPROVER_SOLVER_H
 #define CPROVER_CPROVER_SOLVER_H
 
+#include <string>
 #include <vector>
 
 class exprt;
@@ -30,6 +31,7 @@ class solver_optionst
   bool trace;
   bool verbose;
   std::size_t loop_limit;
+  std::string smt2_solver_binary; // empty = use built-in SAT solver
 };
 
 solver_resultt