From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Sep 2012 21:44:22 +0000 (+0000)
Subject: updates to model generation : do not modify equality engine during getValue, other... 
X-Git-Tag: cvc5-1.0.0~7781
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6d2a808e4981f81e4a638d25582e8542e89b716;p=cvc5.git

updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 8aec39309..96b5d6945 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -28,8 +28,8 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
-TheoryModel::TheoryModel( context::Context* c, std::string name ) :
-d_substitutions( c ), d_equalityEngine( c, name ){
+TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) :
+d_substitutions( c ), d_equalityEngine( c, name ), d_enableFuncModels( enableFuncModels ){
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   // The kinds we are treating as function application in congruence
@@ -44,6 +44,8 @@ d_substitutions( c ), d_equalityEngine( c, name ){
 void TheoryModel::reset(){
   d_reps.clear();
   d_rep_set.clear();
+  d_uf_terms.clear();
+  d_uf_models.clear();
 }
 
 Node TheoryModel::getValue( TNode n ){
@@ -142,6 +144,80 @@ Node TheoryModel::getModelValue( TNode n ){
   }
 }
 
+Node TheoryModel::getInterpretedValue( TNode n ){
+  Trace("model") << "Get interpreted value of " << n << std::endl;
+  TypeNode type = n.getType();
+  if( type.isFunction() || type.isPredicate() ){
+    //for function models
+    if( d_enableFuncModels ){
+      if( d_uf_models.find( n )!=d_uf_models.end() ){
+        //pre-existing function model
+        Trace("model") << "Return function value." << std::endl;
+        return d_uf_models[n];
+      }else{
+        Trace("model") << "Return arbitrary function value." << std::endl;
+        //otherwise, choose the constant default value
+        uf::UfModelTree ufmt( n );
+        Node default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(),
+                                              "a placeholder variable to query for a default value in model construction" ) );
+        ufmt.setDefaultValue( this, default_v );
+        return ufmt.getFunctionValue( "$x" );
+      }
+    }else{
+      return n;
+    }
+  }else{
+    Trace("model-debug") << "check rep..." << std::endl;
+    Node ret;
+    //check if the representative is defined
+    n = d_equalityEngine.hasTerm( n ) ? d_equalityEngine.getRepresentative( n ) : n;
+    Trace("model-debug") << "rep is..." << n << std::endl;
+    if( d_reps.find( n )!=d_reps.end() ){
+      Trace("model") << "Return value in equality engine."<< std::endl;
+      return d_reps[n];
+    }
+    Trace("model-debug") << "check apply uf models..." << std::endl;
+    //if it is APPLY_UF, we must consult the corresponding function if it exists
+    if( n.getKind()==APPLY_UF ){
+      Node op = n.getOperator();
+      if( d_uf_models.find( op )!=d_uf_models.end() ){
+        std::vector< Node > lam_children;
+        lam_children.push_back( d_uf_models[ op ] );
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          lam_children.push_back( n[i] );
+        }
+        Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children );
+        ret = Rewriter::rewrite( app_lam );
+        Trace("model") << "Consult UF model." << std::endl;
+      }
+    }
+    Trace("model-debug") << "check existing..." << std::endl;
+    if( ret.isNull() ){
+      //second, try to choose an existing term as value
+      std::vector< Node > v_emp;
+      ret = getDomainValue( type, v_emp );
+      if( !ret.isNull() ){
+        Trace("model") << "Choose existing value." << std::endl;
+      }
+    }
+    Trace("model-debug") << "check new..." << std::endl;
+    if( ret.isNull() ){
+      //otherwise, choose new value
+      ret = getNewDomainValue( type );
+      if( !ret.isNull() ){
+        Trace("model") << "Choose new value." << std::endl;
+      }
+    }
+    if( !ret.isNull() ){
+      return ret;
+    }else{
+      //otherwise, just return itself (this usually should not happen)
+      Trace("model") << "Return self." << std::endl;
+      return n;
+    }
+  }
+}
+
 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
@@ -156,7 +232,7 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
 
 //FIXME: need to ensure that theory enumerators exist for each sort
 Node TheoryModel::getNewDomainValue( TypeNode tn ){
-#if 1
+#if 0
   if( tn==NodeManager::currentNM()->booleanType() ){
     if( d_rep_set.d_type_reps[tn].empty() ){
       return d_false;
@@ -221,6 +297,14 @@ void TheoryModel::addTerm( Node n ){
   if( !d_equalityEngine.hasTerm( n ) ){
     d_equalityEngine.addTerm( n );
   }
+  //must collect UF terms
+  if( d_enableFuncModels && n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
+      d_uf_terms[ op ].push_back( n );
+      Trace("model-add-term-uf") << "Add term " << n << std::endl;
+    }
+  }
 }
 
 /** assert equality */
@@ -332,120 +416,6 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){
   }
 }
 
-DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) :
-TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){
-
-}
-
-void DefaultModel::addTerm( Node n ){
-  TheoryModel::addTerm( n );
-  //must collect UF terms
-  if( d_enableFuncModels && n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
-      d_uf_terms[ op ].push_back( n );
-    }
-  }
-}
-
-void DefaultModel::reset(){
-  d_uf_terms.clear();
-  d_uf_models.clear();
-  TheoryModel::reset();
-}
-
-Node DefaultModel::getInterpretedValue( TNode n ){
-  Trace("model") << "Get interpreted value of " << n << std::endl;
-  TypeNode type = n.getType();
-  if( type.isFunction() || type.isPredicate() ){
-    //for function models
-    if( d_enableFuncModels ){
-      //create the function value for the model
-      if( d_uf_models.find( n )==d_uf_models.end() ){
-        Trace("model") << "Creating function value..." << std::endl;
-        uf::UfModelTree ufmt( n );
-        Node default_v;
-        for( size_t i=0; i<d_uf_terms[n].size(); i++ ){
-          Node un = d_uf_terms[n][i];
-          Node v = getRepresentative( un );
-          ufmt.setValue( this, un, v );
-          default_v = v;
-        }
-        if( default_v.isNull() ){
-          //choose default value from model if none exists
-          default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValue_$$", type.getRangeType(), "a default value term from model construction" ) );
-        }
-        ufmt.setDefaultValue( this, default_v );
-        ufmt.simplify();
-        d_uf_models[n] = ufmt.getFunctionValue( "$x" );
-      }
-      Trace("model") << "Return function value." << std::endl;
-      return d_uf_models[n];
-    }else{
-      return n;
-    }
-  }else{
-    Node ret;
-    //add term to equality engine, this will enforce a value if it exists
-    //  for example, if a = b = c1, and f( a ) = c2, then adding f( b ) should force
-    //    f( b ) to be equal to c2.
-    addTerm( n );
-    //check if the representative is defined
-    n = d_equalityEngine.getRepresentative( n );
-    if( d_reps.find( n )!=d_reps.end() ){
-      Trace("model") << "Return value in equality engine."<< std::endl;
-      return d_reps[n];
-    }
-    //if it is APPLY_UF, we must consult the corresponding function if it exists
-    if( n.getKind()==APPLY_UF ){
-      Node op = n.getOperator();
-      if( d_uf_models.find( op )!=d_uf_models.end() ){
-        std::vector< Node > lam_children;
-        lam_children.push_back( d_uf_models[ op ] );
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          lam_children.push_back( n[i] );
-        }
-        Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children );
-        ret = Rewriter::rewrite( app_lam );
-        Trace("model") << "Consult UF model." << std::endl;
-      }
-    }
-    if( ret.isNull() ){
-      //second, try to choose an existing term as value
-      std::vector< Node > v_emp;
-      ret = getDomainValue( type, v_emp );
-      if( !ret.isNull() ){
-        Trace("model") << "Choose existing value." << std::endl;
-      }else{
-        //otherwise, choose new value
-        ret = getNewDomainValue( type );
-        if( !ret.isNull() ){
-          Trace("model") << "Choose new value." << std::endl;
-        }
-      }
-    }
-    if( !ret.isNull() ){
-      Node prev = n;
-      //store the equality
-      assertEquality( n, ret, true );
-      //add it to the map of representatives
-      n = d_equalityEngine.getRepresentative( n );
-      if( d_reps.find( n )==d_reps.end() ){
-        d_reps[n] = ret;
-        d_rep_set.add( ret );
-      }
-      //TODO: make sure that this doesn't affect the representatives in the equality engine
-      //  in other words, we need to be sure that all representatives of the equality engine
-      //  are still representatives after this function, or else d_reps should be modified.
-      return ret;
-    }else{
-      //otherwise, just return itself (this usually should not happen)
-      Trace("model") << "Return self." << std::endl;
-      return n;
-    }
-  }
-}
-
 TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
 
 }
@@ -502,9 +472,10 @@ void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){
           assertedReps[ eqc ] = const_rep;
         }else{
           if( fullModel ){
-            //assertion failure?
             Trace("model-warn") << "No representative specified for equivalence class " << eqc << std::endl;
             Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
+            //TODO: select proper representative
+            //Unimplemented("No representative specified for equivalence class");
           }
           //assertedReps[ eqc ] = chooseRepresentative( tm, eqc, fullModel );
           assertedReps[ eqc ] = eqc;
@@ -533,6 +504,35 @@ void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){
   processBuildModel( tm, fullModel );
 }
 
+void TheoryEngineModelBuilder::processBuildModel( TheoryModel* m, bool fullModel ){
+  if( fullModel ){
+    //construct function values
+    for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+      Trace("model-func") << "Creating function value..." << it->first << std::endl;
+      Node n = it->first;
+      if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
+        TypeNode type = n.getType();
+        uf::UfModelTree ufmt( n );
+        Node default_v;
+        for( size_t i=0; i<it->second.size(); i++ ){
+          Node un = it->second[i];
+          Node v = m->getRepresentative( un );
+          ufmt.setValue( m, un, v );
+          default_v = v;
+        }
+        if( default_v.isNull() ){
+          //choose default value from model if none exists
+          default_v = m->getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(),
+                                              "a placeholder variable to query for a default value in model construction" ) );
+        }
+        ufmt.setDefaultValue( m, default_v );
+        ufmt.simplify();
+        m->d_uf_models[n] = ufmt.getFunctionValue( "$x" );
+      }
+    }
+  }
+}
+
 Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
   //try to get a new domain value
   Node rep = m->getNewDomainValue( eqc.getType() );
@@ -550,12 +550,12 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r,
                                                         std::map< Node, bool >& normalizing ){
   Trace("temb-normalize") << r << std::endl;
   if( normalized.find( r )!=normalized.end() ){
-    //Message() << " -> already normalized, return " << reps[r] << std::endl;
+    Trace("temb-normalize") << " -> already normalized, return " << reps[r] << std::endl;
     return reps[r];
   }else if( normalizing.find( r )!=normalizing.end() && normalizing[r] ){
     //this case is to handle things like when store( A, e, i ) is given
     //       as a representative for array A.
-    //Message() << " -> currently normalizing, give up : " << r << std::endl;
+    Trace("temb-normalize") << " -> currently normalizing, give up : " << r << std::endl;
     return r;
   }else if( reps.find( r )!=reps.end() ){
     normalizing[ r ] = true;
@@ -563,13 +563,13 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r,
     normalizing[ r ] = false;
     normalized[ r ] = true;
     reps[ r ] = retNode;
-    //Message() << " --> returned " << retNode << " for " << r << std::endl;
+    Trace("temb-normalize") << " --> returned " << retNode << " for " << r << std::endl;
     return retNode;
   }else if( m->d_equalityEngine.hasTerm( r ) ){
     normalizing[ r ] = true;
     //return the normalized representative from the model
     r = m->d_equalityEngine.getRepresentative( r );
-    //Message() << " -> it is the representative " << r << std::endl;
+    Trace("temb-normalize") << " -> it is the representative " << r << std::endl;
     Node retNode = normalizeRepresentative( m, r, reps, normalized, normalizing );
     normalizing[ r ] = false;
     return retNode;
@@ -582,7 +582,7 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r,
       r = normalizeNode( m, r, reps, normalized, normalizing );
       normalizing[ r ] = false;
     }
-    //Message() << " -> unknown, return " << r << std::endl;
+    Trace("temb-normalize") << " -> unknown, return " << r << std::endl;
     return r;
   }
 }
@@ -591,7 +591,7 @@ Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map<
                                               std::map< Node, bool >& normalized,
                                               std::map< Node, bool >& normalizing ){
   if( r.getNumChildren()>0 ){
-    //Message() << " ---> normalize " << r << " " << r.getNumChildren() << " " << r.getKind() << std::endl;
+    Trace("temb-normalize") << " ---> normalize " << r << " " << r.getNumChildren() << " " << r.getKind() << std::endl;
     //non-leaf case: construct representative from children
     std::vector< Node > children;
     if( r.getMetaKind() == kind::metakind::PARAMETERIZED ){
@@ -603,10 +603,10 @@ Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map<
     }
     Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
     retNode = Rewriter::rewrite( retNode );
-    if( retNode!=r ){
+    //if( retNode!=r ){
       //assure that it is made equal in the model
-      m->assertEquality( r, retNode, true );
-    }
+      //m->assertEquality( r, retNode, true );
+    //}
     return retNode;
   }else{
     return r;
diff --git a/src/theory/model.h b/src/theory/model.h
index adf97df9e..de4d57d2e 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -40,7 +40,7 @@ protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
 public:
-  TheoryModel( context::Context* c, std::string name );
+  TheoryModel( context::Context* c, std::string name, bool enableFuncModels );
   virtual ~TheoryModel(){}
   /** equality engine containing all known equalities/disequalities */
   eq::EqualityEngine d_equalityEngine;
@@ -54,15 +54,15 @@ public:
 protected:
   /** reset the model */
   virtual void reset();
-  /** get interpreted value
-    *  This function is called when the value of the node cannot be determined by the theory rewriter
-    *  This should function should return a representative in d_reps
-    */
-  virtual Node getInterpretedValue( TNode n ) = 0;
   /**
    * Get model value function.  This function is called by getValue
    */
   Node getModelValue( TNode n );
+  /** get interpreted value
+    *  This function is called when the value of the node cannot be determined by the theory rewriter
+    *  This should function should return a representative in d_reps
+    */
+  virtual Node getInterpretedValue( TNode n );
 public:
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
@@ -125,28 +125,12 @@ public:
   void printRepresentativeDebug( const char* c, Node r );
   /** print representative function */
   void printRepresentative( std::ostream& out, Node r );
-};
-
-/** Default model class
-  *   The getInterpretedValue function will choose an existing value arbitrarily.
-  *   If none are found, then it will create a new value.
-  */
-class DefaultModel : public TheoryModel
-{
-protected:
+public:
   /** whether function models are enabled */
   bool d_enableFuncModels;
-  /** add term */
-  void addTerm( Node n );
-public:
-  DefaultModel( context::Context* c, std::string name, bool enableFuncModels );
-  virtual ~DefaultModel(){}
   //necessary information for function models
   std::map< Node, std::vector< Node > > d_uf_terms;
   std::map< Node, Node > d_uf_models;
-public:
-  void reset();
-  Node getInterpretedValue( TNode n );
 };
 
 /** TheoryEngineModelBuilder class
@@ -159,7 +143,7 @@ protected:
   /** pointer to theory engine */
   TheoryEngine* d_te;
   /** process build model */
-  virtual void processBuildModel( TheoryModel* m, bool fullModel ){}
+  virtual void processBuildModel( TheoryModel* m, bool fullModel );
   /** choose representative for unconstrained equivalence class */
   virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
   /** normalize representative */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 6e3e27828..e0723f432 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : DefaultModel( c, name, true ),
+FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
 d_axiom_asserted( c, false ), d_forall_asserts( c ){
 
 }
@@ -41,11 +41,11 @@ void FirstOrderModel::assertQuantifier( Node n ){
 }
 
 void FirstOrderModel::reset(){
-  DefaultModel::reset();
+  TheoryModel::reset();
 }
 
 void FirstOrderModel::addTerm( Node n ){
-  DefaultModel::addTerm( n );
+  TheoryModel::addTerm( n );
 }
 
 void FirstOrderModel::initialize( bool considerAxioms ){
@@ -94,16 +94,16 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
 }
 
 Node FirstOrderModel::getInterpretedValue( TNode n ){
-  Trace("fo-model") << "get interpreted value " << n << std::endl;
-  TypeNode type = n.getType();
+  //Trace("fo-model") << "get interpreted value " << n << std::endl;
+  /*TypeNode type = n.getType();
   if( type.isFunction() || type.isPredicate() ){
     if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
       if( d_uf_models.find( n )==d_uf_models.end() ){
         d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
       }
     }
-  }
-  return DefaultModel::getInterpretedValue( n );
+  }*/
+  return TheoryModel::getInterpretedValue( n );
 }
 
 void FirstOrderModel::toStream(std::ostream& out){
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 1fc4fd76e..64e5fc904 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -39,7 +39,7 @@ namespace quantifiers{
 
 class TermDb;
 
-class FirstOrderModel : public DefaultModel
+class FirstOrderModel : public TheoryModel
 {
 private:
   //add term function
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index c09346f35..8eac4da95 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -76,8 +76,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
     //update models
     for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
       it->second.update( fm );
+      Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
+      //construct function values
+      fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
     }
-
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
   }else{
     d_curr_model = fm;
     //build model for relevant symbols contained in quantified formulas
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d69f43908..932f11f74 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -86,7 +86,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_quantEngine = new QuantifiersEngine(context, this);
 
   // build model information if applicable
-  d_curr_model = new theory::DefaultModel( context, "DefaultModel", true );
+  d_curr_model = new theory::TheoryModel( context, "DefaultModel", true );
   d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
 
   Rewriter::init();
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index f2324e5d2..5ec0d9776 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -130,7 +130,7 @@ class TheoryEngine {
   /**
    * Default model object
    */
-  theory::DefaultModel* d_curr_model;
+  theory::TheoryModel* d_curr_model;
   /**
    * Model builder object
    */
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 8c79f69df..424b2c117 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -262,6 +262,13 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
   }
 }
 
+Node UfModelTree::getFunctionValue( std::vector< Node >& args ){
+  Node body = d_tree.getFunctionValue( args, 0, Node::null() );
+  body = Rewriter::rewrite( body );
+  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
+  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
+}
+
 Node UfModelTree::getFunctionValue( const char* argPrefix ){
   TypeNode type = d_op.getType();
   std::vector< Node > vars;
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 865e7ace9..efcbbef89 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -127,12 +127,7 @@ public:
   /** getFunctionValue
     *   Returns a representation of this function.
     */
-  Node getFunctionValue( std::vector< Node >& args ){
-    Node body = d_tree.getFunctionValue( args, 0, Node::null() );
-    body = Rewriter::rewrite( body );
-    Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
-    return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
-  }
+  Node getFunctionValue( std::vector< Node >& args );
   /** getFunctionValue for args with set prefix */
   Node getFunctionValue( const char* argPrefix );
   /** update