move l_get and convert back into prop_convt

prop_convt is an instance of decision_proceduret that uses propositional
logic.

Author: Daniel Kroening

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.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