Merge pull request #4440 from peterschrammel/clean-up-decision-procedure

Clean up decision_proceduret

Author: peterschrammel

jbmc/src/jbmc/bmc.cpp

@@ -54,7 +54,7 @@ decision_proceduret::resultt bmct::run_decision_procedure()
 
   status() << "Running " << prop_conv.decision_procedure_text() << eom;
 
-  decision_proceduret::resultt dec_result = prop_conv.dec_solve();
+  decision_proceduret::resultt dec_result = prop_conv();
 
   {
     auto solver_stop = std::chrono::steady_clock::now();

jbmc/src/jbmc/bmc.h

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 #include <map>
 
-#include <util/decision_procedure.h>
 #include <util/invariant.h>
 #include <util/options.h>
 #include <util/ui_message.h>
@@ -31,6 +30,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
+#include <solvers/prop/decision_procedure.h>
+
 class cbmc_solverst;
 
 /// \brief Bounded model checking or path exploration for goto-programs

src/goto-checker/goto_symex_property_decider.cpp

@@ -103,7 +103,7 @@ void goto_symex_property_decidert::add_constraint_from_goals(
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
 {
-  return solver->prop_conv().dec_solve();
+  return solver->prop_conv()();
 }
 
 prop_convt &goto_symex_property_decidert::get_solver() const

src/goto-instrument/accelerate/scratch_program.cpp

@@ -12,7 +12,8 @@ Author: Matt Lewis
 #include "scratch_program.h"
 
 #include <util/fixedbv.h>
-#include <util/decision_procedure.h>
+
+#include <solvers/prop/decision_procedure.h>
 
 #include <goto-symex/slice.h>
 
@@ -69,7 +70,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
   std::cout << "Finished symex, invoking decision procedure.\n";
 #endif
 
-  return (checker->dec_solve()==decision_proceduret::resultt::D_SATISFIABLE);
+  return ((*checker)() == decision_proceduret::resultt::D_SATISFIABLE);
 }
 
 exprt scratch_programt::eval(const exprt &e)

src/solvers/Makefile

@@ -144,6 +144,7 @@ SRC = $(BOOLEFORCE_SRC) \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
+      prop/decision_procedure.cpp \
       prop/literal.cpp \
       prop/minimize.cpp \
       prop/prop.cpp \

src/solvers/prop/cover_goals.cpp

@@ -88,7 +88,7 @@ operator()(message_handlert &message_handler)
     _iterations++;
 
     constraint();
-    dec_result=prop_conv.dec_solve();
+    dec_result = prop_conv();
 
     switch(dec_result)
     {

src/solvers/prop/cover_goals.h

@@ -14,8 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
-#include <util/decision_procedure.h>
-
+#include "decision_procedure.h"
 #include "literal.h"
 
 class message_handlert;

src/util/decision_procedure.cpp renamed to src/solvers/prop/decision_procedure.cpp

@@ -14,3 +14,18 @@ Author: Daniel Kroening, [email protected]
 decision_proceduret::~decision_proceduret()
 {
 }
+
+decision_proceduret::resultt decision_proceduret::operator()()
+{
+  return dec_solve();
+}
+
+void decision_proceduret::set_to_true(const exprt &expr)
+{
+  set_to(expr, true);
+}
+
+void decision_proceduret::set_to_false(const exprt &expr)
+{
+  set_to(expr, false);
+}

src/solvers/prop/decision_procedure.h

@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+Module: Decision Procedure Interface
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Decision Procedure Interface
+
+#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+
+#include <iosfwd>
+#include <string>
+
+#include "literal.h"
+
+class exprt;
+class tvt;
+
+class decision_proceduret
+{
+public:
+  /// For a Boolean expression \p expr, add the constraint 'expr' if \p value
+  /// is `true`, otherwise add 'not expr'
+  virtual void set_to(const exprt &expr, bool value) = 0;
+
+  /// For a Boolean expression \p expr, add the constraint 'expr'
+  void set_to_true(const exprt &expr);
+
+  /// For a Boolean expression \p expr, add the constraint 'not expr'
+  void set_to_false(const exprt &expr);
+
+  /// Convert a Boolean expression and return the corresponding literal
+  virtual literalt convert(const exprt &expr) = 0;
+
+  /// Result of running the decision procedure
+  enum class resultt
+  {
+    D_SATISFIABLE,
+    D_UNSATISFIABLE,
+    D_ERROR
+  };
+
+  /// Run the decision procedure to solve the problem
+  resultt operator()();
+
+  /// Return \p expr with variables replaced by values from satisfying
+  /// assignment if available.
+  /// Return `nil` if not available
+  virtual exprt get(const exprt &expr) const = 0;
+
+  /// Return value of literal \p l from satisfying assignment.
+  /// Return tvt::UNKNOWN if not available
+  virtual tvt l_get(literalt l) const = 0;
+
+  /// Print satisfying assignment to \p out
+  virtual void print_assignment(std::ostream &out) const = 0;
+
+  /// Return a textual description of the decision procedure
+  virtual std::string decision_procedure_text() const = 0;
+
+  /// Return the number of incremental solver calls
+  virtual std::size_t get_number_of_solver_calls() const = 0;
+
+  virtual ~decision_proceduret();
+
+protected:
+  /// Run the decision procedure to solve the problem
+  virtual resultt dec_solve() = 0;
+};
+
+/// Add Boolean constraint \p src to decision procedure \p dest
+inline decision_proceduret &
+operator<<(decision_proceduret &dest, const exprt &src)
+{
+  dest.set_to_true(src);
+  return dest;
+}
+
+#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H

src/solvers/prop/minimize.cpp

@@ -123,7 +123,7 @@ void prop_minimizet::operator()()
         bvt assumptions;
         assumptions.push_back(c);
         prop_conv.set_assumptions(assumptions);
-        dec_result=prop_conv.dec_solve();
+        dec_result = prop_conv();
 
         switch(dec_result)
         {
@@ -153,6 +153,6 @@ void prop_minimizet::operator()()
 
     bvt assumptions; // no assumptions
     prop_conv.set_assumptions(assumptions);
-    prop_conv.dec_solve();
+    (void)prop_conv();
   }
 }

src/solvers/prop/prop_conv.h

@@ -13,11 +13,11 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <map>
 
-#include <util/decision_procedure.h>
 #include <util/expr.h>
 #include <util/message.h>
 #include <util/std_expr.h>
 
+#include "decision_procedure.h"
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"
@@ -30,19 +30,8 @@ class prop_convt:public decision_proceduret
 public:
   virtual ~prop_convt() { }
 
-  // conversion to handle
-  virtual literalt convert(const exprt &expr)=0;
-
-  literalt operator()(const exprt &expr)
-  {
-    return convert(expr);
-  }
-
   using decision_proceduret::operator();
 
-  // specialised variant of get
-  virtual tvt l_get(literalt a) const=0;
-
   // incremental solving
   virtual void set_frozen(literalt a);
   virtual void set_frozen(const bvt &);
@@ -56,9 +45,6 @@ class prop_convt:public decision_proceduret
 
   // Resource limits:
   virtual void set_time_limit_seconds(uint32_t) {}
-
-  /// Returns the number of incremental solver calls
-  virtual std::size_t get_number_of_solver_calls() const = 0;
 };
 
 //

src/util/Makefile

@@ -8,7 +8,6 @@ SRC = allocate_objects.cpp \
       cmdline.cpp \
       config.cpp \
       cout_message.cpp \
-      decision_procedure.cpp \
       dstring.cpp \
       endianness_map.cpp \
       expr.cpp \