From b4d9a5bb41d4c5cf8a89de980089981d90b0cc9c Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 29 Oct 2014 21:31:12 -0700 Subject: [PATCH] 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/arrays/theory_arrays.cpp | 227 ++++++++++++++++-------- src/theory/arrays/theory_arrays.h | 31 ++++ src/theory/bv/bv_subtheory_bitblast.cpp | 6 +- src/theory/theory_engine.cpp | 24 +-- 4 files changed, 200 insertions(+), 88 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 13314b46e..e0056e4a9 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -82,6 +82,9 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_constReadsList(c), + d_constReadsContext(new context::Context()), + d_contextPopper(c, d_constReadsContext), d_skolemIndex(c, 0), d_decisionRequests(c), d_permRef(c), @@ -124,7 +127,11 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC } TheoryArrays::~TheoryArrays() { - + CNodeNListMap::iterator it = d_constReads.begin(); + for( ; it != d_constReads.end(); ++it ) { + (*it).second->deleteSelf(); + } + delete d_constReadsContext; StatisticsRegistry::unregisterStat(&d_numRow); StatisticsRegistry::unregisterStat(&d_numExt); StatisticsRegistry::unregisterStat(&d_numProp); @@ -136,7 +143,6 @@ TheoryArrays::~TheoryArrays() { StatisticsRegistry::unregisterStat(&d_numSetModelValSplits); StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts); StatisticsRegistry::unregisterStat(&d_checkTimer); - } void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -464,7 +470,32 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); - d_reads.push_back(node); + + // Synchronize d_constReadsContext with SAT context + Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); + while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { + d_constReadsContext->push(); + } + + // Record read in sharing data structure + TNode index = d_equalityEngine.getRepresentative(node[1]); + if (index.isConst()) { + CTNodeList* temp; + CNodeNListMap::iterator it = d_constReads.find(index); + if (it == d_constReads.end()) { + temp = new(true) CTNodeList(d_constReadsContext); + d_constReads[index] = temp; + } + else { + temp = (*it).second; + } + temp->push_back(node); + d_constReadsList.push_back(node); + } + else { + d_reads.push_back(node); + } + Assert((d_isPreRegistered.insert(node), true)); checkRowForIndex(node[1], store); break; @@ -604,6 +635,76 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { } +void TheoryArrays::checkPair(TNode r1, TNode r2) +{ + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl; + + TNode x = r1[1]; + TNode y = r2[1]; + Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY)); + + if (d_equalityEngine.hasTerm(x) && d_equalityEngine.hasTerm(y) && + (d_equalityEngine.areEqual(x,y) || d_equalityEngine.areDisequal(x,y,false))) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl; + return; + } + + // If the terms are already known to be equal, we are also in good shape + if (d_equalityEngine.areEqual(r1, r2)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl; + return; + } + + if (r1[0] != r2[0]) { + // If arrays are known to be disequal, or cannot become equal, we can continue + Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0])); + if (r1[0].getType() != r2[0].getType() || + d_equalityEngine.areDisequal(r1[0], r2[0], false)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; + return; + } + else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) { + return; + } + } + + if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; + return; + } + + // Get representative trigger terms + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY); + EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); + switch (eqStatusDomain) { + case EQUALITY_TRUE_AND_PROPAGATED: + // Should have been propagated to us + Assert(false); + break; + 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: + // This is unlikely, but I think it could happen + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl; + return; + default: + // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN + break; + } + + // Add this pair + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl; + addCarePair(x_shared, y_shared); +} + + void TheoryArrays::computeCareGraph() { if (d_sharedArrays.size() > 0) { @@ -630,93 +731,69 @@ void TheoryArrays::computeCareGraph() } if (d_sharedTerms) { - vector< pair > currentPairs; + // Synchronize d_constReadsContext with SAT context + Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); + while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { + d_constReadsContext->push(); + } // Go through the read terms and see if there are any to split on + + // Give constReadsContext a push so that all the work it does here is erased - models can change if context changes at all + // The context is popped at the end. If this loop is interrupted for some reason, we have to make sure the context still + // gets popped or the solver will be in an inconsistent state + d_constReadsContext->push(); unsigned size = d_reads.size(); for (unsigned i = 0; i < size; ++ i) { TNode r1 = d_reads[i]; - // Make sure shared terms were identified correctly - // Assert(theoryOf(r1[0]) == THEORY_ARRAY || isShared(r1[0])); - // Assert(theoryOf(r1[1]) == THEORY_ARRAY || - // d_sharedOther.find(r1[1]) != d_sharedOther.end()); + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1 << std::endl; + Assert(d_equalityEngine.hasTerm(r1)); + TNode x = r1[1]; - for (unsigned j = i + 1; j < size; ++ j) { - TNode r2 = d_reads[j]; - - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl; + if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; + continue; + } + Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY); - // If the terms are already known to be equal, we are also in good shape - if (d_equalityEngine.hasTerm(r1) && d_equalityEngine.hasTerm(r2) && d_equalityEngine.areEqual(r1, r2)) { - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl; - continue; + // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check + // Also, insert this read in the list at the proper index + + if (!x_shared.isConst()) { + x_shared = d_valuation.getModelValue(x_shared); + } + if (!x_shared.isNull()) { + CTNodeList* temp; + CNodeNListMap::iterator it = d_constReads.find(x_shared); + if (it == d_constReads.end()) { + // This is the only x_shared with this model value - no need to create any splits + temp = new(true) CTNodeList(d_constReadsContext); + d_constReads[x_shared] = temp; } - - if (r1[0] != r2[0]) { - // If arrays are known to be disequal, or cannot become equal, we can continue - Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0])); - if (r1[0].getType() != r2[0].getType() || - d_equalityEngine.areDisequal(r1[0], r2[0], false)) { - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; - continue; - } - else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) { - if (r2.getType().getCardinality().isInfinite()) { - continue; - } - // TODO: add a disequality split for these two arrays - continue; + else { + temp = (*it).second; + for (size_t j = 0; j < temp->size(); ++j) { + checkPair(r1, (*temp)[j]); } } - - TNode x = r1[1]; - TNode y = r2[1]; - - if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY) || !d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) { - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; - continue; - } - - EqualityStatus eqStatus = getEqualityStatus(x, y); - - if (eqStatus != EQUALITY_UNKNOWN) { - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl; - continue; + temp->push_back(r1); + } + else { + // We don't know the model value for x. Just do brute force examination of all pairs of reads + for (unsigned j = 0; j < size; ++j) { + TNode r2 = d_reads[j]; + Assert(d_equalityEngine.hasTerm(r2)); + checkPair(r1,r2); } - - // Get representative trigger terms - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY); - EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); - switch (eqStatusDomain) { - case EQUALITY_TRUE_AND_PROPAGATED: - // Should have been propagated to us - Assert(false); - break; - 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: - // Don't need to include this pair - if (options::arraysReduceSharing()) { - continue; - } - default: - break; + for (unsigned j = 0; j < d_constReadsList.size(); ++j) { + TNode r2 = d_constReadsList[j]; + Assert(d_equalityEngine.hasTerm(r2)); + checkPair(r1,r2); } - - - // Otherwise, add this pair - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl; - addCarePair(x_shared, y_shared); } } + d_constReadsContext->pop(); } } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 649232dae..a22ab2515 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -215,6 +215,9 @@ class TheoryArrays : public Theory { /** Equaltity engine for determining if two arrays might be equal */ eq::EqualityEngine d_mayEqualEqualityEngine; + // Helper for computeCareGraph + void checkPair(TNode r1, TNode r2); + public: void addSharedTerm(TNode t); @@ -347,7 +350,35 @@ class TheoryArrays : public Theory { CDNodeSet d_sharedArrays; CDNodeSet d_sharedOther; context::CDO d_sharedTerms; + + // Map from constant values to read terms that read from that values equal to that constant value in the current model + // When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList) + // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time. + // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time. + typedef std::hash_map CNodeNListMap; + CNodeNListMap d_constReads; context::CDList d_reads; + context::CDList d_constReadsList; + context::Context* d_constReadsContext; + /** Helper class to keep d_constReadsContext in sync with satContext */ + class ContextPopper : public context::ContextNotifyObj { + context::Context* d_satContext; + context::Context* d_contextToPop; + protected: + void contextNotifyPop() { + if (d_contextToPop->getLevel() > d_satContext->getLevel()) { + d_contextToPop->pop(); + } + } + public: + ContextPopper(context::Context* context, context::Context* contextToPop) + :context::ContextNotifyObj(context), d_satContext(context), + d_contextToPop(contextToPop) + {} + + };/* class ContextPopper */ + ContextPopper d_contextPopper; + std::hash_map d_skolemCache; context::CDO d_skolemIndex; std::vector d_skolemAssertions; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 35542fc68..d0b99f869 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -219,7 +219,11 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { Node BitblastSolver::getModelValue(TNode node) { - Node val = d_bitblaster->getTermModel(node, false); + if (d_bv->d_invalidateModelCache.get()) { + d_bitblaster->invalidateModelCache(); + } + d_bv->d_invalidateModelCache.set(false); + Node val = d_bitblaster->getTermModel(node, true); return val; } 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); -- 2.30.2