Merge pull request #5469 from fbbotero-aws/external_sat_solver

Allow CBMC to call an external sat solver

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -440,6 +440,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("external-sat-solver"))
+  {
+    options.set_option(
+      "external-sat-solver", cmdline.get_value("external-sat-solver")),
+      solver_set = true;
+  }
+
   if(cmdline.isset("yices"))
   {
     options.set_option("yices", true), solver_set=true;
@@ -1113,6 +1120,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --external-sat-solver cmd    command to invoke SAT solver process\n"
     HELP_STRING_REFINEMENT_CBMC
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -57,6 +57,7 @@ class optionst;
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
+  "(external-sat-solver):" \
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\

src/goto-checker/solver_factory.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/prop/solver_resource_limits.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
+#include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/strings/string_refinement.h>
 
@@ -131,6 +132,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
 {
   if(options.get_bool_option("dimacs"))
     return get_dimacs();
+  if(options.is_set("external-sat-solver"))
+    return get_external_sat();
   if(
     options.get_bool_option("refine") &&
     !options.get_bool_option("refine-strings"))
@@ -229,9 +232,24 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
 
   auto bv_dimacs =
     util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
+
   return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
 }
 
+std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
+{
+  no_beautification();
+  no_incremental_check();
+
+  std::string external_sat_solver = options.get_option("external-sat-solver");
+  auto prop =
+    util_make_unique<external_satt>(message_handler, external_sat_solver);
+
+  auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
+
+  return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
+}
+
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
 {
   std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {

src/goto-checker/solver_factory.h

@@ -72,6 +72,7 @@ class solver_factoryt
 
   std::unique_ptr<solvert> get_default();
   std::unique_ptr<solvert> get_dimacs();
+  std::unique_ptr<solvert> get_external_sat();
   std::unique_ptr<solvert> get_bv_refinement();
   std::unique_ptr<solvert> get_string_refinement();
   std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);

src/solvers/Makefile

@@ -184,6 +184,7 @@ SRC = $(BOOLEFORCE_SRC) \
       sat/cnf.cpp \
       sat/cnf_clause_list.cpp \
       sat/dimacs_cnf.cpp \
+      sat/external_sat.cpp \
       sat/pbs_dimacs_cnf.cpp \
       sat/resolution_proof.cpp \
       smt2/letify.cpp \

src/solvers/sat/dimacs_cnf.cpp

@@ -51,7 +51,7 @@ void dimacs_cnft::write_problem_line(std::ostream &out)
       << clauses.size() << "\n";
 }
 
-static void write_dimacs_clause(
+void dimacs_cnft::write_dimacs_clause(
   const bvt &clause,
   std::ostream &out,
   bool break_lines)
@@ -100,5 +100,5 @@ void dimacs_cnft::write_clauses(std::ostream &out)
 
 void dimacs_cnf_dumpt::lcnf(const bvt &bv)
 {
-  write_dimacs_clause(bv, out, true);
+  dimacs_cnft::write_dimacs_clause(bv, out, true);
 }

src/solvers/sat/dimacs_cnf.h

@@ -32,6 +32,9 @@ class dimacs_cnft:public cnf_clause_listt
   void set_assignment(literalt a, bool value) override;
   bool is_in_conflict(literalt l) const override;
 
+  static void
+  write_dimacs_clause(const bvt &, std::ostream &, bool break_lines);
+
 protected:
   void write_problem_line(std::ostream &out);
   void write_clauses(std::ostream &out);

src/solvers/sat/external_sat.cpp

@@ -0,0 +1,169 @@
+/// \file
+/// Allows call an external SAT solver to allow faster integration of
+/// newer SAT solvers
+/// \author Francis Botero <fbbotero@amazon.com>
+
+#include "external_sat.h"
+
+#include "dimacs_cnf.h"
+
+#include <util/exception_utils.h>
+#include <util/run.h>
+#include <util/string_utils.h>
+#include <util/tempfile.h>
+
+#include <chrono>
+#include <cstdlib>
+#include <fstream>
+#include <random>
+#include <sstream>
+#include <string>
+#include <thread>
+
+external_satt::external_satt(message_handlert &message_handler, std::string cmd)
+  : cnf_clause_list_assignmentt(message_handler), solver_cmd(std::move(cmd))
+{
+}
+
+const std::string external_satt::solver_text()
+{
+  return "External SAT solver";
+}
+
+bool external_satt::is_in_conflict(literalt) const
+{
+  UNIMPLEMENTED;
+}
+
+void external_satt::set_assignment(literalt, bool)
+{
+  UNIMPLEMENTED;
+}
+
+void external_satt::write_cnf_file(std::string cnf_file)
+{
+  log.status() << "Writing temporary CNF" << messaget::eom;
+  std::ofstream out(cnf_file);
+
+  // We start counting at 1, thus there is one variable fewer.
+  out << "p cnf " << (no_variables() - 1) << ' ' << no_clauses() << '\n';
+
+  for(auto &c : clauses)
+    dimacs_cnft::write_dimacs_clause(c, out, false);
+
+  out.close();
+}
+
+std::string external_satt::execute_solver(std::string cnf_file)
+{
+  log.status() << "Invoking SAT solver" << messaget::eom;
+  std::ostringstream response_ostream;
+  auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, "");
+
+  log.status() << "Solver returned code: " << cmd_result << messaget::eom;
+  return response_ostream.str();
+}
+
+external_satt::resultt external_satt::parse_result(std::string solver_output)
+{
+  std::istringstream response_istream(solver_output);
+  std::string line;
+  external_satt::resultt result = resultt::P_ERROR;
+  std::vector<bool> assigned_variables(no_variables(), false);
+  assignment.insert(assignment.begin(), no_variables(), tvt(false));
+
+  while(getline(response_istream, line))
+  {
+    if(line[0] == 's')
+    {
+      auto parts = split_string(line, ' ');
+      if(parts.size() < 2)
+      {
+        log.error() << "external SAT solver has provided an unexpected "
+                       "response in results.\nUnexpected reponse: "
+                    << line << messaget::eom;
+        return resultt::P_ERROR;
+      }
+
+      auto status = parts[1];
+      log.status() << "result:" << status << messaget::eom;
+      if(status == "UNSATISFIABLE")
+      {
+        return resultt::P_UNSATISFIABLE;
+      }
+      if(status == "SATISFIABLE")
+      {
+        result = resultt::P_SATISFIABLE;
+      }
+      if(status == "TIMEOUT")
+      {
+        log.error() << "external SAT solver reports a timeout" << messaget::eom;
+        return resultt::P_ERROR;
+      }
+    }
+
+    if(line[0] == 'v')
+    {
+      auto assignments = split_string(line, ' ');
+
+      // remove the first element which should be 'v' identifying
+      // the line as the satisfying assignments
+      assignments.erase(assignments.begin());
+      auto number_of_variables = no_variables();
+      for(auto &assignment_string : assignments)
+      {
+        try
+        {
+          signed long long as_long = std::stol(assignment_string);
+          size_t index = std::labs(as_long);
+
+          if(index >= number_of_variables)
+          {
+            log.error() << "SAT assignment " << as_long
+                        << " out of range of CBMC largest variable of "
+                        << (number_of_variables - 1) << messaget::eom;
+            return resultt::P_ERROR;
+          }
+          assignment[index] = tvt(as_long >= 0);
+          assigned_variables[index] = true;
+        }
+        catch(...)
+        {
+          log.error() << "SAT assignment " << assignment_string
+                      << " caused an exception while processing"
+                      << messaget::eom;
+          return resultt::P_ERROR;
+        }
+      }
+      // Assignments can span multiple lines so returning early isn't an option
+    }
+  }
+
+  if(result == resultt::P_SATISFIABLE)
+  {
+    // We don't need to check zero
+    for(size_t index = 1; index < no_variables(); index++)
+    {
+      if(!assigned_variables[index])
+      {
+        log.error() << "No assignment was found for literal: " << index
+                    << messaget::eom;
+        return resultt::P_ERROR;
+      }
+    }
+    return resultt::P_SATISFIABLE;
+  }
+
+  log.error() << "external SAT solver has provided an unexpected response"
+              << messaget::eom;
+  return resultt::P_ERROR;
+}
+
+external_satt::resultt external_satt::do_prop_solve()
+{
+  // create a temporary file
+  temporary_filet cnf_file("external-sat", ".cnf");
+  write_cnf_file(cnf_file());
+  auto output = execute_solver(cnf_file());
+  return parse_result(output);
+}

src/solvers/sat/external_sat.h

@@ -0,0 +1,38 @@
+/// \file
+/// Allows calling an external SAT solver to allow faster integration of
+/// newer SAT solvers
+/// \author Francis Botero <fbbotero@amazon.com>
+
+#ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
+#define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
+
+#include "cnf_clause_list.h"
+class external_satt : public cnf_clause_list_assignmentt
+{
+public:
+  explicit external_satt(message_handlert &message_handler, std::string cmd);
+
+  bool has_set_assumptions() const override final
+  {
+    return false;
+  }
+
+  bool has_is_in_conflict() const override final
+  {
+    return false;
+  }
+
+  const std::string solver_text() override;
+
+  bool is_in_conflict(literalt) const override;
+  void set_assignment(literalt, bool) override;
+
+protected:
+  resultt do_prop_solve() override;
+  std::string solver_cmd;
+  void write_cnf_file(std::string);
+  std::string execute_solver(std::string);
+  resultt parse_result(std::string);
+};
+
+#endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H

unit/Makefile

@@ -58,6 +58,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.cpp \
+       solvers/sat/external_sat.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \