diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-17 21:19:58 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-17 21:19:58 +0000 |
| commit | 2b83291d229c957e2becf7397d186040959602df (patch) | |
| tree | 3e3300af92ff26f425348cab38c7b3f19c3719b4 | |
| parent | a7091c61d6661079cfef6b489809579a0c6ac792 (diff) | |
minor fix to prevent getValue from returning null
| -rw-r--r-- | src/theory/model.cpp | 79 |
1 files changed, 40 insertions, 39 deletions
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;
}
}
|