use decision_proceduret interface

The methods in prop_convt aren't used by this class.

Author: Daniel Kroening

src/solvers/flattening/functions.cpp

@@ -66,7 +66,7 @@ void functionst::add_function_constraints(const function_infot &info)
       implies_exprt implication(arguments_equal_expr,
                                 equal_exprt(*it1, *it2));
 
-      prop_conv.set_to_true(implication);
+      decision_procedure.set_to_true(implication);
     }
   }
 }

src/solvers/flattening/functions.h

@@ -16,13 +16,15 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/mathematical_expr.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/decision_procedure.h>
 
 class functionst
 {
 public:
-  explicit functionst(prop_convt &_prop_conv):
-    prop_conv(_prop_conv) { }
+  explicit functionst(decision_proceduret &_decision_procedure)
+    : decision_procedure(_decision_procedure)
+  {
+  }
 
   virtual ~functionst()
   {
@@ -37,7 +39,7 @@ class functionst
   }
 
 protected:
-  prop_convt &prop_conv;
+  decision_proceduret &decision_procedure;
 
   typedef std::set<function_application_exprt> applicationst;