Merge pull request #5607 from diffblue/external-sat-incremental

make the 'external SAT' solver incremental

Author: kroening

src/solvers/sat/external_sat.cpp

@@ -12,13 +12,11 @@
 #include <util/string_utils.h>
 #include <util/tempfile.h>
 
-#include <chrono>
+#include <algorithm>
 #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))
@@ -46,11 +44,18 @@ void external_satt::write_cnf_file(std::string cnf_file)
   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';
+  out << "p cnf " << (no_variables() - 1) << ' '
+      << no_clauses() + assumptions.size() << '\n';
 
+  // output the problem clauses
   for(auto &c : clauses)
     dimacs_cnft::write_dimacs_clause(c, out, false);
 
+  // output the assumption clauses
+  forall_literals(it, assumptions)
+    if(!it->is_constant())
+      out << it->dimacs() << " 0\n";
+
   out.close();
 }
 
@@ -161,6 +166,14 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
 
 external_satt::resultt external_satt::do_prop_solve()
 {
+  // are we assuming 'false'?
+  if(
+    std::find(assumptions.begin(), assumptions.end(), const_literal(false)) !=
+    assumptions.end())
+  {
+    return resultt::P_UNSATISFIABLE;
+  }
+
   // create a temporary file
   temporary_filet cnf_file("external-sat", ".cnf");
   write_cnf_file(cnf_file());

src/solvers/sat/external_sat.h

@@ -14,7 +14,7 @@ class external_satt : public cnf_clause_list_assignmentt
 
   bool has_set_assumptions() const override final
   {
-    return false;
+    return true;
   }
 
   bool has_is_in_conflict() const override final
@@ -27,9 +27,16 @@ class external_satt : public cnf_clause_list_assignmentt
   bool is_in_conflict(literalt) const override;
   void set_assignment(literalt, bool) override;
 
+  void set_assumptions(const bvt &_assumptions) override
+  {
+    assumptions = _assumptions;
+  }
+
 protected:
-  resultt do_prop_solve() override;
   std::string solver_cmd;
+  bvt assumptions;
+
+  resultt do_prop_solve() override;
   void write_cnf_file(std::string);
   std::string execute_solver(std::string);
   resultt parse_result(std::string);