diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-29 21:31:12 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-29 21:32:27 -0700 |
| commit | b4d9a5bb41d4c5cf8a89de980089981d90b0cc9c (patch) | |
| tree | 87b11643d0f1f7269f3112ea56a1cdd38fde55bb /src/theory/theory_engine.cpp | |
| parent | db982d9329981683c8d791aadba7e97fa98b0bd3 (diff) | |
Added new, much faster, care graph computation for arrays
Force split on true first in combineTheories
Fix bugs in getModelValue in bit-vectors
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
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); |