diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-09-21 16:12:03 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-09-21 16:12:03 -0400 |
| commit | 8f51d131fedcd80db21f204a0b2447e70b1e88ea (patch) | |
| tree | dade3c33e738f9a7d7c9bf095e68ae2864ccf7cc /src/theory | |
| parent | 0b2152c61334b73d26f8e7f6f051f1ae64a2206d (diff) | |
Fix for sets segfault (reported by Ravi Kandhadai)
fix involves sets getModelValue handling the case when element theory
doesn't have model
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 565a5cd69..4054f3e21 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -593,11 +593,16 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { // The terms are implied to be dis-equal return EQUALITY_FALSE; } - if( d_external.d_valuation.getModelValue(a) == d_external.d_valuation.getModelValue(b) ) { - // Ther term are true in current model + Node aModelValue = d_external.d_valuation.getModelValue(a); + if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; } + Node bModelValue = d_external.d_valuation.getModelValue(b); + if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; } + if( aModelValue == bModelValue ) { + // The term are true in current model return EQUALITY_TRUE_IN_MODEL; + } else { + return EQUALITY_FALSE_IN_MODEL; } - return EQUALITY_FALSE_IN_MODEL; // } // //TODO: can we be more precise sometimes? // return EQUALITY_UNKNOWN; @@ -1561,7 +1566,9 @@ Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) if(e.isConst()) { elements_const.insert(e); } else { - elements_const.insert(d_theory.d_external.d_valuation.getModelValue(e)); + Node eModelValue = d_theory.d_external.d_valuation.getModelValue(e); + if( eModelValue.isNull() ) return eModelValue; + elements_const.insert(eModelValue); } } Node v = d_theory.elementsToShape(elements_const, n.getType()); |