From b4d9a5bb41d4c5cf8a89de980089981d90b0cc9c Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 29 Oct 2014 21:31:12 -0700 Subject: Added new, much faster, care graph computation for arrays Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors --- src/theory/theory_engine.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'src/theory/theory_engine.cpp') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ed56890ae..7fb989a5a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -487,16 +487,16 @@ void TheoryEngine::combineTheories() { // The equality in question (order for no repetition) Node equality = carePair.a.eqNode(carePair.b); - EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); - Debug("combineTheories") << "TheoryEngine::combineTheories(): " << - (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : - es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : - es == EQUALITY_TRUE ? "EQUALITY_TRUE" : - es == EQUALITY_FALSE ? "EQUALITY_FALSE" : - es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" : - es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" : - es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" : - "Unexpected case") << endl; + // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); + // Debug("combineTheories") << "TheoryEngine::combineTheories(): " << + // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : + // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : + // es == EQUALITY_TRUE ? "EQUALITY_TRUE" : + // es == EQUALITY_FALSE ? "EQUALITY_FALSE" : + // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" : + // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" : + // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" : + // "Unexpected case") << endl; // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; @@ -505,8 +505,8 @@ void TheoryEngine::combineTheories() { // but it doesn't seem to make a big difference - need to explore more -Clark // if (true) { // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { - // Node e = ensureLiteral(equality); - // d_propEngine->requirePhase(e, true); + Node e = ensureLiteral(equality); + d_propEngine->requirePhase(e, true); // } // else if (es == EQUALITY_FALSE_IN_MODEL) { // Node e = ensureLiteral(equality); -- cgit v1.2.3