From 3df8013300486129fc06f3a20d43def1f34a221a Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 18 Aug 2014 22:02:25 -0700 Subject: [PATCH] Better getEqualityStatus for arrays, smarter combination of theories --- src/theory/arrays/theory_arrays.cpp | 18 ++++++------ src/theory/theory_engine.cpp | 43 +++++++++++++++++++++++++---- src/theory/theory_engine.h | 5 ++++ src/theory/valuation.cpp | 8 +----- 4 files changed, 52 insertions(+), 22 deletions(-) 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; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 01387637e..ffe4258cd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -405,7 +405,7 @@ void TheoryEngine::check(Theory::Effort effort) { propagate(effort); // We do combination if all has been processed and we are in fullcheck - if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) { + if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl; combineTheories(); @@ -453,7 +453,7 @@ void TheoryEngine::check(Theory::Effort effort) { void TheoryEngine::combineTheories() { - Trace("sharing") << "TheoryEngine::combineTheories()" << endl; + Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl; TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); @@ -471,25 +471,46 @@ void TheoryEngine::combineTheories() { // Call on each parametric theory to give us its care graph CVC4_FOR_EACH_THEORY; - Trace("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl; + Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl; // Now add splitters for the ones we are interested in CareGraph::const_iterator care_it = careGraph.begin(); CareGraph::const_iterator care_it_end = careGraph.end(); + for (; care_it != care_it_end; ++ care_it) { const CarePair& carePair = *care_it; - Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl; + Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl; Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); // 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; // We need to split on it - Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl; + Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); + if (false) { + if (es == EQUALITY_TRUE_IN_MODEL) { + Node e = ensureLiteral(equality); + d_propEngine->requirePhase(e, true); + } + else if (es == EQUALITY_FALSE_IN_MODEL) { + Node e = ensureLiteral(equality); + d_propEngine->requirePhase(e, false); + } + } } } @@ -1182,6 +1203,18 @@ Node TheoryEngine::getModelValue(TNode var) { return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } + +Node TheoryEngine::ensureLiteral(TNode n) { + Debug("ensureLiteral") << "rewriting: " << n << std::endl; + Node rewritten = Rewriter::rewrite(n); + Debug("ensureLiteral") << " got: " << rewritten << std::endl; + Node preprocessed = preprocess(rewritten); + Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl; + d_propEngine->ensureLiteral(preprocessed); + return preprocessed; +} + + void TheoryEngine::printInstantiations( std::ostream& out ) { if( d_quantEngine ){ d_quantEngine->printInstantiations( out ); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index eec4f1168..e589e8f87 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -758,6 +758,11 @@ public: */ Node getModelValue(TNode var); + /** + * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal + */ + Node ensureLiteral(TNode n); + /** * Print all instantiations made by the quantifiers module. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 72d878782..b2d7f4b21 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -88,13 +88,7 @@ Node Valuation::getModelValue(TNode var) { } Node Valuation::ensureLiteral(TNode n) { - Debug("ensureLiteral") << "rewriting: " << n << std::endl; - Node rewritten = Rewriter::rewrite(n); - Debug("ensureLiteral") << " got: " << rewritten << std::endl; - Node preprocessed = d_engine->preprocess(rewritten); - Debug("ensureLiteral") << "preproced: " << preprocessed << std::endl; - d_engine->getPropEngine()->ensureLiteral(preprocessed); - return preprocessed; + return d_engine->ensureLiteral(n); } bool Valuation::isDecision(Node lit) const { -- 2.30.2