From ba03942a69a80ac93217e17b076673a522e50680 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 27 Mar 2013 16:38:41 -0400 Subject: [PATCH] Updates to model-based array solver Minor fixes to bv and theory_engine --- src/theory/arrays/theory_arrays.cpp | 157 +++++++++++++++++++++++----- src/theory/arrays/theory_arrays.h | 5 +- src/theory/bv/bitblaster.cpp | 7 +- src/theory/theory_engine.cpp | 6 +- 4 files changed, 141 insertions(+), 34 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 5984296e3..62de6092b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -583,6 +583,7 @@ void TheoryArrays::computeCareGraph() } } } + if (options::arraysModelBased()) return; if (d_sharedTerms) { vector< pair > currentPairs; @@ -956,7 +957,7 @@ void TheoryArrays::check(Effort e) { } if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) { - checkModel(); + checkModel(e); } if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { @@ -995,14 +996,65 @@ void TheoryArrays::preRegisterStores(TNode s) } -void TheoryArrays::checkModel() +void TheoryArrays::checkModel(Effort e) { d_inCheckModel = true; d_topLevel = getSatContext()->getLevel(); Assert(d_skolemIndex == 0); Assert(d_skolemAssertions.empty()); + Assert(d_lemmas.empty()); + if (fullEffort(e)) { + // Add constraints for shared terms + context::CDList::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; + Node modelVal, modelVal2, d; + vector assumptions; + bool invert; + for (; shared_it != shared_it_end; ++shared_it) { + if ((*shared_it).getType().isArray()) { + continue; + } + if ((*shared_it).isConst()) { + modelVal = (*shared_it); + } + else { + modelVal = d_valuation.getModelValue(*shared_it); + if (modelVal.isNull()) { + continue; + } + } + Assert(modelVal.isConst()); + for (shared_it2 = shared_it, ++shared_it2; shared_it2 != shared_it_end; ++shared_it2) { + if ((*shared_it2).getType() != (*shared_it).getType()) { + continue; + } + if ((*shared_it2).isConst()) { + modelVal2 = (*shared_it2); + } + else { + modelVal2 = d_valuation.getModelValue(*shared_it2); + if (modelVal2.isNull()) { + continue; + } + } + Assert(modelVal2.isConst()); + invert = (modelVal != modelVal2); + d = (*shared_it).eqNode(*shared_it2); + if (modelVal != modelVal2) { + d = d.notNode(); + } + if (!setModelVal(d, d_true, false, true, assumptions)) { + assumptions.push_back(d); + d_lemmas.push_back(mkAnd(assumptions, true)); + goto finish; + } + assumptions.clear(); + } + } + } + { // TODO: record and replay decisions + int baseLevel = getSatContext()->getLevel(); unsigned constraintIdx; Node assertion, assertionToCheck; vector assumptions; @@ -1061,7 +1113,7 @@ void TheoryArrays::checkModel() } if (t.getKind() == kind::AND) { for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { - // Assert(validAssumptions.find(*child_it) != validAssumptions.end()); + Assert(validAssumptions.find(*child_it) != validAssumptions.end()); all.insert(*child_it); } } @@ -1075,10 +1127,11 @@ void TheoryArrays::checkModel() continue; } else { - // Assert(validAssumptions.find(t) != validAssumptions.end()); + Assert(validAssumptions.find(t) != validAssumptions.end()); all.insert(t); } } + // d_lemmas.push_back(mkAnd(assumptions, true)); bool eq = false; Node decision, explanation; @@ -1087,13 +1140,16 @@ void TheoryArrays::checkModel() decision = d_decisions.back(); d_decisions.pop_back(); if (all.find(decision) != all.end()) { + if (getSatContext()->getLevel() < baseLevel) { + goto finish; + } all.erase(decision); eq = false; if (decision.getKind() == kind::NOT) { decision = decision[0]; eq = true; } - while (!d_decisions.empty() && all.find(d_decisions.back()) == all.end()) { + while (getSatContext()->getLevel() != baseLevel && all.find(d_decisions.back()) == all.end()) { getSatContext()->pop(); d_decisions.pop_back(); } @@ -1122,6 +1178,7 @@ void TheoryArrays::checkModel() d_permRef.push_back(explanation); } if (decision.isNull()) { + // d_lemmas.pop_back(); d_conflictNode = explanation; d_conflict = true; break; @@ -1148,12 +1205,22 @@ void TheoryArrays::checkModel() if (d[0].getType().isArray()) { Assert(d[1].getKind() == kind::STORE); if (d[1][0].getKind() == kind::STORE) { - preRegisterTermInternal(d[1][0][0]); - preRegisterTermInternal(d[1][0][2]); + if (!d_equalityEngine.hasTerm(d[1][0][0])) { + preRegisterTermInternal(d[1][0][0]); + } + if (!d_equalityEngine.hasTerm(d[1][0][2])) { + preRegisterTermInternal(d[1][0][2]); + } + } + if (!d_equalityEngine.hasTerm(d[1][0])) { + preRegisterTermInternal(d[1][0]); + } + if (!d_equalityEngine.hasTerm(d[1][2])) { + preRegisterTermInternal(d[1][2]); + } + if (!d_equalityEngine.hasTerm(d[1])) { + preRegisterTermInternal(d[1]); } - preRegisterTermInternal(d[1][0]); - preRegisterTermInternal(d[1][2]); - preRegisterTermInternal(d[1]); } Debug("arrays-model-based") << "Re-asserting skolem equality " << d << endl; d_equalityEngine.assertEquality(d, true, d_true); @@ -1171,7 +1238,7 @@ void TheoryArrays::checkModel() if (d_conflict) { break; } - Assert(getModelVal(assertion) == d_true); + // Assert(getModelVal(assertion) == d_true); assumptions.clear(); } #ifdef CVC4_ASSERTIONS @@ -1182,6 +1249,8 @@ void TheoryArrays::checkModel() } } #endif + } + finish: while (!d_decisions.empty()) { Assert(!d_conflict); getSatContext()->pop(); @@ -1189,6 +1258,11 @@ void TheoryArrays::checkModel() } d_skolemAssertions.clear(); d_skolemIndex = 0; + while (!d_lemmas.empty()) { + Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; + d_out->lemma(d_lemmas.back()); + d_lemmas.pop_back(); + } Assert(getSatContext()->getLevel() == d_topLevel); if (d_conflict) { Node tmp = d_conflictNode; @@ -1527,17 +1601,30 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, d_equalityEngine.assertEquality(d, !invert, d_decisions.back()); Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl; ++d_numSetModelValSplits; - while (d_conflict) { + if (d_conflict) { ++d_numSetModelValConflicts; Debug("arrays-model-based") << "...which results in a conflict!" << endl; d = d_decisions.back(); unsigned sz = assumptions.size(); convertNodeToAssumptions(d_conflictNode, assumptions, d); - NodeBuilder<> conjunction(kind::AND); - for (unsigned i = sz; i < assumptions.size(); ++i) { - conjunction << assumptions[i]; + unsigned sz2 = assumptions.size(); + Assert(sz2 > sz); + Node explanation; + if (sz2 == sz+1) { + explanation = assumptions[sz]; } - Node explanation = conjunction; + else { + NodeBuilder<> conjunction(kind::AND); + for (unsigned i = sz; i < sz2; ++i) { + conjunction << assumptions[i]; + } + explanation = conjunction; + } + // assumptions.push_back(d); + // d_lemmas.push_back(mkAnd(assumptions, true, sz)); + // while (assumptions.size() > sz2) { + // assumptions.pop_back(); + // } getSatContext()->pop(); d_decisions.pop_back(); d_permRef.push_back(explanation); @@ -1562,52 +1649,64 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, } -Node TheoryArrays::mkAnd(std::vector& conjunctions) +Node TheoryArrays::mkAnd(std::vector& conjunctions, bool invert, unsigned startIndex) { Assert(conjunctions.size() > 0); std::set all; std::set explained; - unsigned i = 0; + unsigned i = startIndex; TNode t; for (; i < conjunctions.size(); ++i) { t = conjunctions[i]; if (t == d_true) { continue; } - - if (t.getKind() == kind::AND) { + else if (t.getKind() == kind::AND) { for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { + if (*child_it == d_true) { + continue; + } all.insert(*child_it); } } - - // Expand explanation resulting from propagating a ROW lemma - if (t.getKind() == kind::OR) { + else if (t.getKind() == kind::OR) { + // Expand explanation resulting from propagating a ROW lemma if ((explained.find(t) == explained.end())) { Assert(t[1].getKind() == kind::EQUAL); d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions); explained.insert(t); } - continue; } - all.insert(t); + else { + all.insert(t); + } } if (all.size() == 0) { - return d_true; + return invert ? d_false : d_true; } if (all.size() == 1) { // All the same, or just one - return *(all.begin()); + if (invert) { + return (*(all.begin())).negate(); + } + else { + return *(all.begin()); + } } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder<> conjunction(invert ? kind::OR : kind::AND); std::set::const_iterator it = all.begin(); std::set::const_iterator it_end = all.end(); while (it != it_end) { - conjunction << *it; + if (invert) { + conjunction << (*it).negate(); + } + else { + conjunction << *it; + } ++ it; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index ef1f3b506..b659a8e68 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -358,9 +358,10 @@ class TheoryArrays : public Theory { // List of nodes that need permanent references in this context context::CDList d_permRef; context::CDList d_modelConstraints; + std::vector d_lemmas; Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); - Node mkAnd(std::vector& conjunctions); + Node mkAnd(std::vector& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); void checkRIntro1(TNode a, TNode b); Node removeRepLoops(TNode a, TNode rep); @@ -377,7 +378,7 @@ class TheoryArrays : public Theory { int d_topLevel; void convertNodeToAssumptions(TNode node, std::vector& assumptions, TNode nodeSkip); void preRegisterStores(TNode s); - void checkModel(); + void checkModel(Effort e); bool hasLoop(TNode node, TNode target); typedef std::hash_map NodeMap; NodeMap d_getModelValCache; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 9a52a05a5..feca721c9 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -412,8 +412,11 @@ bool Bitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } -bool Bitblaster::hasValue(TNode a) { - Assert (d_termCache.find(a) != d_termCache.end()); +Node Bitblaster::getVarValue(TNode a) { + if (d_termCache.find(a) == d_termCache.end()) { + Assert(isSharedTerm(a)); + return Node(); + } Bits bits = d_termCache[a]; for (int i = bits.size() -1; i >= 0; --i) { SatValue bit_value; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b89ca8fa4..1c297eda6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1194,8 +1194,12 @@ Node TheoryEngine::getExplanation(TNode node) { theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) { if(Dump.isOn("t-lemmas")) { + Node n = node; + if (negated) { + n = node.negate(); + } Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << QueryCommand(node.toExpr()); + << QueryCommand(n.toExpr()); } // Share with other portfolio threads -- 2.30.2