Merge pull request #7976 from diffblue/propt-interface

propt: change interface for solving under assumptions

Author: kroening

src/solvers/prop/prop.cpp

@@ -38,8 +38,15 @@ bvt propt::new_variables(std::size_t width)
 
 propt::resultt propt::prop_solve()
 {
+  static const bvt empty_assumptions;
   ++number_of_solver_calls;
-  return do_prop_solve();
+  return do_prop_solve(empty_assumptions);
+}
+
+propt::resultt propt::prop_solve(const bvt &assumptions)
+{
+  ++number_of_solver_calls;
+  return do_prop_solve(assumptions);
 }
 
 std::size_t propt::get_number_of_solver_calls() const

src/solvers/prop/prop.h

@@ -84,9 +84,11 @@ class propt
   // They overload this to return false and thus avoid some optimisations
   virtual bool cnf_handled_well() const { return true; }
 
-  // assumptions
-  virtual void set_assumptions(const bvt &) { }
-  virtual bool has_set_assumptions() const { return false; }
+  // solving with assumptions
+  virtual bool has_assumptions() const
+  {
+    return false;
+  }
 
   // variables
   virtual literalt new_variable()=0;
@@ -98,6 +100,7 @@ class propt
   virtual std::string solver_text() const = 0;
   enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
   resultt prop_solve();
+  resultt prop_solve(const bvt &assumptions);
 
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
@@ -122,7 +125,8 @@ class propt
   std::size_t get_number_of_solver_calls() const;
 
 protected:
-  virtual resultt do_prop_solve() = 0;
+  // solve under the given assumption
+  virtual resultt do_prop_solve(const bvt &assumptions) = 0;
 
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;

src/solvers/prop/prop_conv_solver.cpp

@@ -459,7 +459,7 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
 
-  switch(prop.prop_solve())
+  switch(prop.prop_solve(assumption_stack))
   {
   case propt::resultt::P_SATISFIABLE:
     return resultt::D_SATISFIABLE;
@@ -531,8 +531,6 @@ void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
   for(const auto &assumption : assumptions)
     assumption_stack.push_back(to_literal_expr(assumption).get_literal());
   context_size_stack.push_back(assumptions.size());
-
-  prop.set_assumptions(assumption_stack);
 }
 
 void prop_conv_solvert::push()
@@ -543,17 +541,13 @@ void prop_conv_solvert::push()
 
   assumption_stack.push_back(context_literal);
   context_size_stack.push_back(1);
-
-  prop.set_assumptions(assumption_stack);
 }
 
 void prop_conv_solvert::pop()
 {
   // We remove the context from the stack.
   assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
   context_size_stack.pop_back();
-
-  prop.set_assumptions(assumption_stack);
 }
 
 // This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it

src/solvers/refinement/bv_refinement_loop.cpp

@@ -16,7 +16,7 @@ bv_refinementt::bv_refinementt(const infot &info)
     config_(info)
 {
   // check features we need
-  PRECONDITION(prop.has_set_assumptions());
+  PRECONDITION(prop.has_assumptions());
   PRECONDITION(prop.has_set_to());
   PRECONDITION(prop.has_is_in_conflict());
 }
@@ -102,7 +102,7 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
   }
 
   push(assumptions);
-  propt::resultt result=prop.prop_solve();
+  propt::resultt result = prop.prop_solve(assumption_stack);
   pop();
 
   // clang-format off

src/solvers/sat/cnf_clause_list.h

@@ -77,7 +77,7 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
-  resultt do_prop_solve() override
+  resultt do_prop_solve(const bvt &) override
   {
     return resultt::P_ERROR;
   }

src/solvers/sat/dimacs_cnf.h

@@ -66,7 +66,7 @@ class dimacs_cnf_dumpt:public cnft
   }
 
 protected:
-  resultt do_prop_solve() override
+  resultt do_prop_solve(const bvt &) override
   {
     return resultt::P_ERROR;
   }

src/solvers/sat/external_sat.cpp

@@ -36,7 +36,7 @@ void external_satt::set_assignment(literalt, bool)
   UNIMPLEMENTED;
 }
 
-void external_satt::write_cnf_file(std::string cnf_file)
+void external_satt::write_cnf_file(std::string cnf_file, const bvt &assumptions)
 {
   log.status() << "Writing temporary CNF" << messaget::eom;
   std::ofstream out(cnf_file);
@@ -167,7 +167,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
   return resultt::P_ERROR;
 }
 
-external_satt::resultt external_satt::do_prop_solve()
+external_satt::resultt external_satt::do_prop_solve(const bvt &assumptions)
 {
   // are we assuming 'false'?
   if(
@@ -179,7 +179,7 @@ external_satt::resultt external_satt::do_prop_solve()
 
   // create a temporary file
   temporary_filet cnf_file("external-sat", ".cnf");
-  write_cnf_file(cnf_file());
+  write_cnf_file(cnf_file(), assumptions);
   auto output = execute_solver(cnf_file());
   return parse_result(output);
 }

src/solvers/sat/external_sat.h

@@ -12,7 +12,7 @@ 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
+  bool has_assumptions() const override final
   {
     return true;
   }
@@ -27,17 +27,11 @@ 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:
   std::string solver_cmd;
-  bvt assumptions;
 
-  resultt do_prop_solve() override;
-  void write_cnf_file(std::string);
+  resultt do_prop_solve(const bvt &assumptions) override;
+  void write_cnf_file(std::string, const bvt &);
   std::string execute_solver(std::string);
   resultt parse_result(std::string);
 };

src/solvers/sat/pbs_dimacs_cnf.cpp

@@ -205,8 +205,10 @@ bool pbs_dimacs_cnft::pbs_solve()
   return satisfied;
 }
 
-propt::resultt pbs_dimacs_cnft::do_prop_solve()
+propt::resultt pbs_dimacs_cnft::do_prop_solve(const bvt &assumptions)
 {
+  PRECONDITION(assumptions.empty());
+
   std::ofstream file("temp.cnf");
 
   write_dimacs_cnf(file);

src/solvers/sat/pbs_dimacs_cnf.h

@@ -58,7 +58,7 @@ class pbs_dimacs_cnft:public dimacs_cnft
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   std::set<int> assigned;
 };