From 3df8013300486129fc06f3a20d43def1f34a221a Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 18 Aug 2014 22:02:25 -0700 Subject: Better getEqualityStatus for arrays, smarter combination of theories --- src/theory/arrays/theory_arrays.cpp | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'src/theory/arrays') diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e73c059d4..6b91400e8 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -566,12 +566,11 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { // The terms are implied to be equal return EQUALITY_TRUE; } - if (d_equalityEngine.areDisequal(a, b, false)) { + else if (d_equalityEngine.areDisequal(a, b, false)) { // The terms are implied to be dis-equal return EQUALITY_FALSE; } - //TODO: can we be more precise sometimes? - return EQUALITY_UNKNOWN; + return EQUALITY_UNKNOWN;//FALSE_IN_MODEL; } @@ -665,18 +664,17 @@ void TheoryArrays::computeCareGraph() // Should have been propagated to us Assert(false); break; - case EQUALITY_FALSE_AND_PROPAGATED: - // Should have been propagated to us - Assert(false); - break; - case EQUALITY_FALSE: case EQUALITY_TRUE: // Missed propagation - need to add the pair so that theory engine can force propagation Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl; break; + case EQUALITY_FALSE_AND_PROPAGATED: + // Should have been propagated to us + Assert(false); + case EQUALITY_FALSE: case EQUALITY_FALSE_IN_MODEL: - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; - break; + // Don't need to include this pair + continue; default: break; } -- cgit v1.2.3