Clean up decision_proceduret API

jbmc/src/jbmc/all_properties.cpp

@@ -105,8 +105,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   {
     // Our goal is to falsify a property, i.e., we will
     // add the negation of the property as goal.
-    literalt p = !solver.convert(g.second.as_expr());
-    cover_goals.add(p);
+    cover_goals.add(not_exprt(g.second.as_expr()));
   }
 
   status() << "Running " << solver.decision_procedure_text() << eom;

src/solvers/prop/cover_goals.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/threeval.h>
 
 #include "literal_expr.h"
-#include "prop_conv.h"
 
 cover_goalst::~cover_goalst()
 {
@@ -29,8 +28,9 @@ void cover_goalst::mark()
     o->satisfying_assignment();
 
   for(auto &g : goals)
-    if(g.status==goalt::statust::UNKNOWN &&
-       prop_conv.l_get(g.condition).is_true())
+    if(
+      g.status == goalt::statust::UNKNOWN &&
+      decision_procedure.get(g.condition).is_true())
     {
       g.status=goalt::statust::COVERED;
       _number_covered++;
@@ -48,27 +48,12 @@ void cover_goalst::constraint()
 
   // cover at least one unknown goal
 
-  for(std::list<goalt>::const_iterator
-      g_it=goals.begin();
-      g_it!=goals.end();
-      g_it++)
-    if(g_it->status==goalt::statust::UNKNOWN &&
-       !g_it->condition.is_false())
-      disjuncts.push_back(literal_exprt(g_it->condition));
+  for(const auto &g : goals)
+    if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false())
+      disjuncts.push_back(g.condition);
 
   // this is 'false' if there are no disjuncts
-  prop_conv.set_to_true(disjunction(disjuncts));
-}
-
-/// Build clause
-void cover_goalst::freeze_goal_variables()
-{
-  for(std::list<goalt>::const_iterator
-      g_it=goals.begin();
-      g_it!=goals.end();
-      g_it++)
-    if(!g_it->condition.is_constant())
-      prop_conv.set_frozen(g_it->condition);
+  decision_procedure.set_to_true(disjunction(disjuncts));
 }
 
 /// Try to cover all goals
@@ -79,17 +64,13 @@ operator()(message_handlert &message_handler)
 
   decision_proceduret::resultt dec_result;
 
-  // We use incremental solving, so need to freeze some variables
-  // to prevent them from being eliminated.
-  freeze_goal_variables();
-
   do
   {
     // We want (at least) one of the remaining goals, please!
     _iterations++;
 
     constraint();
-    dec_result = prop_conv();
+    dec_result = decision_procedure();
 
     switch(dec_result)
     {

src/solvers/prop/cover_goals.h

@@ -15,20 +15,20 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 
 #include "decision_procedure.h"
-#include "literal.h"
+
+#include <util/expr.h>
 
 class message_handlert;
-class prop_convt;
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.
 class cover_goalst
 {
 public:
-  explicit cover_goalst(prop_convt &_prop_conv):
-    _number_covered(0),
-    _iterations(0),
-    prop_conv(_prop_conv)
+  explicit cover_goalst(decision_proceduret &_decision_procedure)
+    : _number_covered(0),
+      _iterations(0),
+      decision_procedure(_decision_procedure)
   {
   }
 
@@ -41,10 +41,11 @@ class cover_goalst
 
   struct goalt
   {
-    literalt condition;
+    exprt condition;
     enum class statust { UNKNOWN, COVERED, UNCOVERED, ERROR } status;
 
-    goalt():status(statust::UNKNOWN)
+    explicit goalt(exprt _condition)
+      : condition(std::move(_condition)), status(statust::UNKNOWN)
     {
     }
   };
@@ -71,10 +72,9 @@ class cover_goalst
 
   // managing the goals
 
-  void add(const literalt condition)
+  void add(exprt condition)
   {
-    goals.push_back(goalt());
-    goals.back().condition=condition;
+    goals.emplace_back(std::move(condition));
   }
 
   // register an observer if you want to be told
@@ -95,15 +95,14 @@ class cover_goalst
 protected:
   std::size_t _number_covered;
   unsigned _iterations;
-  prop_convt &prop_conv;
+  decision_proceduret &decision_procedure;
 
   typedef std::vector<observert *> observerst;
   observerst observers;
 
 private:
   void mark();
   void constraint();
-  void freeze_goal_variables();
 };
 
 #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H

src/solvers/prop/decision_procedure.h

@@ -15,10 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <iosfwd>
 #include <string>
 
-#include "literal.h"
-
 class exprt;
-class tvt;
 
 class decision_proceduret
 {
@@ -33,10 +30,6 @@ class decision_proceduret
   /// 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
-  /// This will go away, use handle(expr) instead
-  virtual literalt convert(const exprt &expr) = 0;
-
   /// Generate a handle for an expression; this offers an efficient way
   /// to refer to the expression in subsequent calls to \ref get or
   /// \ref set_to
@@ -58,11 +51,6 @@ class decision_proceduret
   /// 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
-  /// This will go away, use get instead.
-  virtual tvt l_get(literalt l) const = 0;
-
   /// Print satisfying assignment to \p out
   virtual void print_assignment(std::ostream &out) const = 0;
 

src/solvers/prop/prop_conv.cpp

@@ -10,11 +10,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "literal_expr.h"
 
+#include <util/std_expr.h>
+
 #include <algorithm>
 
 exprt prop_convt::handle(const exprt &expr)
 {
-  return literal_exprt(convert(expr));
+  // We can only improve Booleans.
+  if(expr.type().id() != ID_bool)
+    return expr;
+
+  // We convert to a literal to obtain a 'small' handle
+  literalt l = convert(expr);
+
+  // The literal may be a constant as a result of non-trivial
+  // propagation. We return constants as such.
+  if(l.is_true())
+    return true_exprt();
+  else if(l.is_false())
+    return false_exprt();
+
+  // freeze to enable incremental use
+  set_frozen(l);
+
+  return literal_exprt(l);
 }
 
 /// determine whether a variable is in the final conflict

src/solvers/prop/prop_conv.h

@@ -11,6 +11,9 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
 
 #include "decision_procedure.h"
+#include "literal.h"
+
+class tvt;
 
 // API that provides a "handle" in the form of a literalt
 // for expressions.
@@ -29,6 +32,13 @@ class prop_convt:public decision_proceduret
   /// but solver-specific representation.
   exprt handle(const exprt &expr) override;
 
+  /// Convert a Boolean expression and return the corresponding literal
+  virtual literalt convert(const exprt &expr) = 0;
+
+  /// Return value of literal \p l from satisfying assignment.
+  /// Return tvt::UNKNOWN if not available
+  virtual tvt l_get(literalt l) const = 0;
+
   // incremental solving
   virtual void set_frozen(literalt a);
   virtual void set_frozen(const bvt &);
@@ -41,9 +51,4 @@ class prop_convt:public decision_proceduret
   virtual bool has_is_in_conflict() const { return false; }
 };
 
-//
-// an instance of the above that converts the
-// propositional skeleton by passing it to a propt
-//
-
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H