From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 17 Jul 2012 21:19:58 +0000 (+0000)
Subject: minor fix to prevent getValue from returning null
X-Git-Tag: cvc5-1.0.0~7918
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b83291d229c957e2becf7397d186040959602df;p=cvc5.git

minor fix to prevent getValue from returning null
---

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