minor fix to prevent getValue from returning null

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 03bba185c8bcb000df9406fc093b653aa920612d..052051e83e401d0bd4cfab1aa667b5ce9c8fc277 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -147,45 +147,36 @@ Node TheoryModel::getValue( TNode n ){
     return n;\r
   }\r
 \r
-  // see if the value is explicitly set in the model\r
-  if( d_equalityEngine.hasTerm( n ) ){\r
-    Debug("model") << "-> Defined term." << std::endl;\r
-    return getRepresentative( n );\r
-  }else{\r
-    Node nn;\r
-    if( n.getNumChildren()>0 ){\r
-      std::vector< Node > children;\r
-      if( metakind == kind::metakind::PARAMETERIZED ){\r
-        Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;\r
-        children.push_back( n.getOperator() );\r
-      }\r
-      //evaluate the children\r
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
-        Node val = getValue( n[i] );\r
-        Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;\r
-        Assert( !val.isNull() );\r
-        children.push_back( val );\r
-      }\r
-      Debug("model-debug") << "Done eval children" << std::endl;\r
-      nn = NodeManager::currentNM()->mkNode( n.getKind(), children );\r
-    }else{\r
-      nn = n;\r
+  Node nn;\r
+  if( n.getNumChildren()>0 ){\r
+    std::vector< Node > children;\r
+    if( metakind == kind::metakind::PARAMETERIZED ){\r
+      Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;\r
+      children.push_back( n.getOperator() );\r
     }\r
-    //interpretation is the rewritten form\r
-    nn = Rewriter::rewrite( nn );\r
-\r
-    // special case: value of a constant == itself\r
-    if(metakind == kind::metakind::CONSTANT) {\r
-      Debug("model") << "-> Theory-interpreted term." << std::endl;\r
-      return nn;\r
-    }else if( d_equalityEngine.hasTerm( nn ) ){\r
-      Debug("model") << "-> Theory-interpreted (defined) term." << std::endl;\r
-      return getRepresentative( nn );\r
-    }else{\r
-      Debug("model") << "-> Model-interpreted term." << std::endl;\r
-      //otherwise, get the interpreted value in the model\r
-      return getInterpretedValue( nn );\r
+    //evaluate the children\r
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
+      Node val = getValue( n[i] );\r
+      Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;\r
+      Assert( !val.isNull() );\r
+      children.push_back( val );\r
     }\r
+    Debug("model-debug") << "Done eval children" << std::endl;\r
+    nn = NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+  }else{\r
+    nn = n;\r
+  }\r
+  //interpretation is the rewritten form\r
+  nn = Rewriter::rewrite( nn );\r
+\r
+  // special case: value of a constant == itself\r
+  if(metakind == kind::metakind::CONSTANT) {\r
+    Debug("model") << "-> Theory-interpreted term." << std::endl;\r
+    return nn;\r
+  }else{\r
+    Debug("model") << "-> Model-interpreted term." << std::endl;\r
+    //otherwise, get the interpreted value in the model\r
+    return getInterpretedValue( nn );\r
   }\r
 \r
   ////case for equality\r
@@ -346,17 +337,27 @@ Node DefaultModel::getInterpretedValue( TNode n ){
     //DO_THIS?\r
     return n;\r
   }else{\r
-    //first, try to choose an existing term as value\r
+    //first, see if the representative is defined\r
+    if( d_equalityEngine.hasTerm( n ) ){\r
+      n = d_equalityEngine.getRepresentative( n );\r
+      //this check is required since d_equalityEngine.hasTerm( n )\r
+      // does not ensure that n is in an equivalence class in d_equalityEngine\r
+      if( d_reps.find( n )!=d_reps.end() ){\r
+        return d_reps[n];\r
+      }\r
+    }\r
+    //second, try to choose an existing term as value\r
     std::vector< Node > v_emp;\r
     Node n2 = getDomainValue( type, v_emp );\r
     if( !n2.isNull() ){\r
       return n2;\r
     }else{\r
-      //otherwise, choose new valuse\r
+      //otherwise, choose new value\r
       n2 = getNewDomainValue( type, true );\r
       if( !n2.isNull() ){\r
         return n2;\r
       }else{\r
+        //otherwise, just return itself\r
         return n;\r
       }\r
     }\r