Move handle() from interface to implementation

The implementation should be in the implementation class.

Author: peterschrammel

src/solvers/prop/prop_conv.cpp

@@ -14,28 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
-exprt prop_convt::handle(const exprt &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);
-}
-
 void prop_convt::set_assumptions(const bvt &)
 {
   UNREACHABLE;

src/solvers/prop/prop_conv.h

@@ -26,13 +26,6 @@ class prop_convt:public decision_proceduret
 
   using decision_proceduret::operator();
 
-  /// returns a 'handle', which is an expression that
-  /// has the same value as the argument in any model
-  /// that is generated.
-  /// This may be the expression itself or a more compact
-  /// 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;
 

src/solvers/prop/prop_conv_solver.cpp

@@ -15,6 +15,28 @@ bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
   return prop.is_in_conflict(to_literal_expr(expr).get_literal());
 }
 
+exprt prop_conv_solvert::handle(const exprt &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);
+}
+
 bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
 {
   PRECONDITION(expr.type().id() == ID_bool);

src/solvers/prop/prop_conv_solver.h

@@ -64,6 +64,9 @@ class prop_conv_solvert : public conflict_providert,
   {
     return prop.has_set_assumptions();
   }
+
+  exprt handle(const exprt &expr) override;
+
   void set_all_frozen() override
   {
     freeze_all = true;

src/solvers/smt2/smt2_conv.cpp

@@ -661,6 +661,15 @@ literalt smt2_convt::convert(const exprt &expr)
   return l;
 }
 
+exprt smt2_convt::handle(const exprt &expr)
+{
+  // We can only improve Booleans.
+  if(expr.type().id() != ID_bool)
+    return expr;
+
+  return literal_exprt(convert(expr));
+}
+
 void smt2_convt::convert_literal(const literalt l)
 {
   if(l==const_literal(false))

src/solvers/smt2/smt2_conv.h

@@ -113,6 +113,7 @@ class smt2_convt:public prop_convt
   bool use_array_of_bool;
   bool emit_set_logic;
 
+  exprt handle(const exprt &expr) override;
   literalt convert(const exprt &expr) override;
   void set_frozen(literalt) override
   { /* not needed */