use new handle interface in cover_goals

The literal-based interface is more specific, and cover_goals doesn't
require anything beyond what decision_proceduret offers.

Author: Daniel Kroening

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

@@ -29,8 +29,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 &&
+      prop_conv.get(g.condition).is_true())
     {
       g.status=goalt::statust::COVERED;
       _number_covered++;
@@ -50,20 +51,12 @@ void cover_goalst::constraint()
 
   for(const auto &g : goals)
     if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false())
-      disjuncts.push_back(literal_exprt(g.condition));
+      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(const auto &g : goals)
-    if(!g.condition.is_constant())
-      prop_conv.set_frozen(g.condition);
-}
-
 /// Try to cover all goals
 decision_proceduret::resultt cover_goalst::
 operator()(message_handlert &message_handler)
@@ -72,10 +65,6 @@ 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!

src/solvers/prop/cover_goals.h

@@ -15,7 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 
 #include "decision_procedure.h"
-#include "literal.h"
+
+#include <util/expr.h>
 
 class message_handlert;
 class prop_convt;
@@ -41,10 +42,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 +73,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
@@ -103,7 +104,6 @@ class cover_goalst
 private:
   void mark();
   void constraint();
-  void freeze_goal_variables();
 };
 
 #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H