modified getValue to return Expr instead of Node

1 files changed, 9 insertions, 7 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 51d5a77b5..67640c309 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -46,6 +46,15 @@ void TheoryModel::reset(){
   d_rep_set.clear();
 }
 
+Expr TheoryModel::getValue( const Expr& expr ){
+  Node n = Node::fromExpr( expr );
+  //apply substitutions
+  Node nn = d_substitutions.apply( n );
+  //get value in model
+  Node ret = getModelValue( nn );
+  return ret.toExpr();
+}
+
 void TheoryModel::toStream( std::ostream& out ){
   /*//for debugging
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -114,13 +123,6 @@ Node TheoryModel::getModelValue( TNode n ){
   }
 }
 
-Node TheoryModel::getValue( TNode n ){
-  //apply substitutions
-  Node nn = d_substitutions.apply( n );
-  //get value in model
-  return getModelValue( nn );
-}
-
 Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
   if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
     //try to find a pre-existing arbitrary element