ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output

7 files changed, 66 insertions, 53 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ba7973405..e298ca2a2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2238,6 +2238,7 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
 
 void SmtEngine::printModel( std::ostream& out, Model* m ){
   SmtScope smts(this);
+  Expr::dag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream( out, m );
   //m->toStream(out);
 }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index ee61c9345..62327e4dc 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -118,7 +118,7 @@ Node TheoryModel::getModelValue( TNode n ){
     }
     //evaluate the children
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node val = getModelValue( n[i] );
+      Node val = getValue( n[i] );
       Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;
       Assert( !val.isNull() );
       children.push_back( val );
@@ -216,6 +216,13 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
   }
 }
 
+/** add term */
+void TheoryModel::addTerm( Node n ){
+  if( !d_equalityEngine.hasTerm( n ) ){
+    d_equalityEngine.addTerm( n );
+  }
+}
+
 /** assert equality */
 void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
   d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
@@ -331,6 +338,7 @@ 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();
@@ -347,11 +355,14 @@ void DefaultModel::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++ ){
@@ -368,42 +379,62 @@ Node DefaultModel::getInterpretedValue( TNode n ){
         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{
-    Trace("model") << "Get interpreted value of " << n << std::endl;
+    Node ret;
     //add term to equality engine, this will enforce a value if it exists
-    d_equalityEngine.addTerm( n );
-    //first, see if the representative is defined
+    //  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 );
-    //this check is required since d_equalityEngine.hasTerm( n )
-    // does not ensure that n is in an equivalence class in d_equalityEngine
     if( d_reps.find( n )!=d_reps.end() ){
+      Trace("model") << "Return value in equality engine."<< std::endl;
       return d_reps[n];
     }
-    //second, try to choose an existing term as value
-    Trace("model") << "Choose existing value..." << std::endl;
-    std::vector< Node > v_emp;
-    Node n2 = getDomainValue( type, v_emp );
-    if( !n2.isNull() ){
-      //store the equality??   this is dangerous since it may cause representatives to change
-      //assertEquality( n, n2, true );
-      return n2;
-    }else{
-      //otherwise, choose new value
-      Trace("model") << "Choose new value..." << std::endl;
-      n2 = getNewDomainValue( type );
-      if( !n2.isNull() ){
-        //store the equality??
-        //assertEquality( n, n2, true );
-        return n2;
+    //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, just return itself (this usually should not happen)
-        return n;
+        //otherwise, choose new value
+        ret = getNewDomainValue( type );
+        if( !ret.isNull() ){
+          Trace("model") << "Choose new value." << std::endl;
+        }
       }
     }
+    if( !ret.isNull() ){
+      //store the equality
+      assertEquality( n, ret, true );
+      //this is dangerous since it may cause representatives to change
+      Assert( getRepresentative( ret )==ret );
+      return ret;
+    }else{
+      //otherwise, just return itself (this usually should not happen)
+      Trace("model") << "Return self." << std::endl;
+      return n;
+    }
   }
 }
 
diff --git a/src/theory/model.h b/src/theory/model.h
index 2f4ebfdbf..85f5dd31b 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -37,12 +37,6 @@ class TheoryModel : public Model
 {
   friend class TheoryEngineModelBuilder;
 protected:
-  /** add term function
-    *   This should be called on all terms that exist in the model.
-    *   addTerm( n ) will do any model-specific processing necessary for n,
-    *   such as contraining the interpretation of uninterpretted functions.
-    */
-  virtual void addTerm( Node n ) {}
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
 public:
@@ -94,6 +88,12 @@ public:
 public:
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+  /** add term function
+    *   addTerm( n ) will do any model-specific processing necessary for n,
+    *   such as contraining the interpretation of uninterpretted functions,
+    *   and adding n to the equality engine of this model
+    */
+  virtual void addTerm( Node n );
   /** assert equality holds in the model */
   void assertEquality( Node a, Node b, bool polarity );
   /** assert predicate holds in the model */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b03261195..6e3e27828 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -94,33 +94,14 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
 }
 
 Node FirstOrderModel::getInterpretedValue( TNode n ){
-  Debug("fo-model") << "get interpreted value " << n << std::endl;
+  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() ){
-        //use the model tree to generate the model
         d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
       }
-      return d_uf_models[n];
     }
-  /*
-  }else if( type.isArray() ){
-    if( d_array_model.find( n )!=d_array_model.end() ){
-      return d_array_model[n].getArrayValue();
-    }else{
-      //std::cout << "no array model generated for " << n << std::endl;
-    }
-  */
-  }else if( n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
-      //consult the uf model
-      int depIndex;
-      return d_uf_model_tree[ op ].getValue( this, n, depIndex );
-    }
-  }else if( n.getKind()==SELECT ){
-
   }
   return DefaultModel::getInterpretedValue( n );
 }
@@ -274,7 +255,7 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
   if( !n.hasAttribute(InstConstantAttribute()) ){
     //if evaluating a ground term, just consult the standard getValue functionality
     depIndex = -1;
-    return getModelValue( n );
+    return getValue( n );
   }else{
     Node val;
     depIndex = ri->getNumTerms()-1;
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index e66bf8040..1fc4fd76e 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -87,7 +87,6 @@ public:
   void initialize( bool considerAxioms = true );
   /** to stream function */
   void toStream( std::ostream& out );
-
 //the following functions are for evaluating quantifier bodies
 public:
   /** reset evaluation */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9809b948e..67c1aa9f6 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -197,7 +197,7 @@ void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
   if( fullModel ){
     std::map< TypeNode, TypeEnumerator* > type_enums;
     //must choose proper representatives
-    // for each equivalence class, specify the constructor as a representative
+    // for each equivalence class, specify fresh constant as representative
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
     while( !eqcs_i.isFinished() ){
       Node eqc = (*eqcs_i);
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index fd346bc3c..865e7ace9 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -129,6 +129,7 @@ public:
     */
   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);
   }