Move literal convert/get to decision_proceduret

There is no instance in the code base of using decision_proceduret
without these functions.

Author: peterschrammel

src/solvers/prop/decision_procedure.h

@@ -15,7 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 #include <string>
 
+#include "literal.h"
+
 class exprt;
+class tvt;
 
 class decision_proceduret
 {
@@ -26,6 +29,9 @@ class decision_proceduret
   // returns nil if not available
   virtual exprt get(const exprt &expr) const=0;
 
+  // specialized variant of get
+  virtual tvt l_get(literalt) const = 0;
+
   // print satisfying assignment
   virtual void print_assignment(std::ostream &out) const=0;
 
@@ -39,6 +45,14 @@ class decision_proceduret
   void set_to_false(const exprt &expr)
   { set_to(expr, false); }
 
+  // conversion to handle
+  virtual literalt convert(const exprt &expr) = 0;
+
+  literalt operator()(const exprt &expr)
+  {
+    return convert(expr);
+  }
+
   // solve the problem
   enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR };
 

src/solvers/prop/prop_conv.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 &);