cover_goalst does not need prop_convt

No methods of prop_convt are used.

Author: Daniel Kroening

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()
 {
@@ -31,7 +30,7 @@ void cover_goalst::mark()
   for(auto &g : goals)
     if(
       g.status == goalt::statust::UNKNOWN &&
-      prop_conv.get(g.condition).is_true())
+      decision_procedure.get(g.condition).is_true())
     {
       g.status=goalt::statust::COVERED;
       _number_covered++;
@@ -54,7 +53,7 @@ void cover_goalst::constraint()
       disjuncts.push_back(g.condition);
 
   // this is 'false' if there are no disjuncts
-  prop_conv.set_to_true(disjunction(disjuncts));
+  decision_procedure.set_to_true(disjunction(disjuncts));
 }
 
 /// Try to cover all goals
@@ -71,7 +70,7 @@ operator()(message_handlert &message_handler)
     _iterations++;
 
     constraint();
-    dec_result = prop_conv();
+    dec_result = decision_procedure();
 
     switch(dec_result)
     {

src/solvers/prop/cover_goals.h

@@ -19,17 +19,16 @@ Author: Daniel Kroening, [email protected]
 #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)
   {
   }
 
@@ -96,7 +95,7 @@ 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;