From: Clark Barrett Date: Wed, 27 Mar 2013 00:12:47 +0000 (-0400) Subject: New model-based array procedure X-Git-Tag: cvc5-1.0.0~7361^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d45b7e9594003f1d17bd5d512e6eeb68b70f6a53;p=cvc5.git New model-based array procedure --- diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index bb9a9e417..32eaff355 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -167,6 +167,20 @@ void ArrayInfo::setRIntro1Applied(const TNode a) { } +void ArrayInfo::setModelRep(const TNode a, const TNode b) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->modelRep = b; + info_map[a] = temp_info; + } else { + (*it).second->modelRep = b; + } + +} + /** * Returns the information associated with TNode a */ @@ -200,6 +214,16 @@ const bool ArrayInfo::rIntro1Applied(const TNode a) const return false; } +const TNode ArrayInfo::getModelRep(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->modelRep; + } + return TNode(); +} + const CTNodeList* ArrayInfo::getIndices(const TNode a) const{ CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 13fae2ae5..10c15fd0e 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -63,11 +63,12 @@ class Info { public: context::CDO isNonLinear; context::CDO rIntro1Applied; + context::CDO modelRep; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false) { + Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -209,6 +210,7 @@ public: void setNonLinear(const TNode a); void setRIntro1Applied(const TNode a); + void setModelRep(const TNode a, const TNode rep); /** * Returns the information associated with TNode a @@ -220,6 +222,8 @@ public: const bool rIntro1Applied(const TNode a) const; + const TNode getModelRep(const TNode a) const; + const CTNodeList* getIndices(const TNode a) const; const CTNodeList* getStores(const TNode a) const; diff --git a/src/theory/arrays/options b/src/theory/arrays/options index 755cf239c..41c56f51d 100644 --- a/src/theory/arrays/options +++ b/src/theory/arrays/options @@ -11,4 +11,10 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) +option arraysModelBased --arrays-model-based bool :default false :read-write + turn on model-based arrray solver + +option arraysEagerIndexSplitting --arrays-eager-index bool :default false :read-write + turn on eager index splitting for generated array lemmas + endmodule diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index dcf4813fc..5984296e3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -48,7 +48,7 @@ const bool d_solveWrite2 = false; // These are now options //bool d_useNonLinearOpt = true; //bool d_lazyRIntro1 = true; -const bool d_eagerIndexSplitting = true; + //bool d_eagerIndexSplitting = false; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe), @@ -58,6 +58,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_numExplain("theory::arrays::number of explanations", 0), d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), d_checkTimer("theory::arrays::checkTime"), d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"), d_ppFacts(u), @@ -79,8 +83,11 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_skolemIndex(c, 0), d_decisionRequests(c), - d_permRef(c) + d_permRef(c), + d_modelConstraints(c), + d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); @@ -88,6 +95,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC StatisticsRegistry::registerStat(&d_numExplain); StatisticsRegistry::registerStat(&d_numNonLinear); StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); + StatisticsRegistry::registerStat(&d_numGetModelValSplits); + StatisticsRegistry::registerStat(&d_numGetModelValConflicts); + StatisticsRegistry::registerStat(&d_numSetModelValSplits); + StatisticsRegistry::registerStat(&d_numSetModelValConflicts); StatisticsRegistry::registerStat(&d_checkTimer); d_true = NodeManager::currentNM()->mkConst(true); @@ -140,6 +151,128 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) { Rewriter::rewrite(a.eqNode(b)) == d_false); } + +Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck) +{ + if (!solve1) { + return term; + } + if (term[0].getKind() != kind::STORE && + term[1].getKind() != kind::STORE) { + return term; + } + TNode left = term[0]; + TNode right = term[1]; + int leftWrites = 0, rightWrites = 0; + + // Count nested writes + TNode e1 = left; + while (e1.getKind() == kind::STORE) { + ++leftWrites; + e1 = e1[0]; + } + + TNode e2 = right; + while (e2.getKind() == kind::STORE) { + ++rightWrites; + e2 = e2[0]; + } + + if (rightWrites > leftWrites) { + TNode tmp = left; + left = right; + right = tmp; + int tmpWrites = leftWrites; + leftWrites = rightWrites; + rightWrites = tmpWrites; + } + + NodeManager* nm = NodeManager::currentNM(); + if (rightWrites == 0) { + if (e1 != e2) { + return term; + } + // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF + // + // read(store, index_n) = v_n & + // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} & + // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} & + // ... + // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1 + // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0 + TNode write_i, write_j, index_i, index_j; + Node conc; + NodeBuilder<> result(kind::AND); + int i, j; + write_i = left; + for (i = leftWrites-1; i >= 0; --i) { + index_i = write_i[1]; + + // build: [index_i /= index_n && index_i /= index_(n-1) && + // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i + write_j = left; + { + NodeBuilder<> hyp(kind::AND); + for (j = leftWrites - 1; j > i; --j) { + index_j = write_j[1]; + if (!ppCheck || !ppDisequal(index_i, index_j)) { + Node hyp2(index_i.getType() == nm->booleanType()? + index_i.iffNode(index_j) : index_i.eqNode(index_j)); + hyp << hyp2.notNode(); + } + write_j = write_j[0]; + } + + Node r1 = nm->mkNode(kind::SELECT, e1, index_i); + conc = (r1.getType() == nm->booleanType())? + r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); + if (hyp.getNumChildren() != 0) { + if (hyp.getNumChildren() == 1) { + conc = hyp.getChild(0).impNode(conc); + } + else { + r1 = hyp; + conc = r1.impNode(conc); + } + } + + // And into result + result << conc; + + // Prepare for next iteration + write_i = write_i[0]; + } + } + Assert(result.getNumChildren() > 0); + if (result.getNumChildren() == 1) { + return result.getChild(0); + } + return result; + } + else { + if (!solve2) { + return term; + } + // store(...) = store(a,i,v) ==> + // store(store(...),i,select(a,i)) = a && select(store(...),i)=v + Node l = left; + Node tmp; + NodeBuilder<> nb(kind::AND); + while (right.getKind() == kind::STORE) { + tmp = nm->mkNode(kind::SELECT, l, right[1]); + nb << tmp.eqNode(right[2]); + tmp = nm->mkNode(kind::SELECT, right[0], right[1]); + l = nm->mkNode(kind::STORE, l, right[1], tmp); + right = right[0]; + } + nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck); + return nb; + } + Unreachable(); + return term; +} + + Node TheoryArrays::ppRewrite(TNode term) { if (!d_preprocess) return term; d_ppEqualityEngine.addTerm(term); @@ -163,115 +296,7 @@ Node TheoryArrays::ppRewrite(TNode term) { break; } case kind::EQUAL: { - if (!d_solveWrite) break; - if (term[0].getKind() == kind::STORE || - term[1].getKind() == kind::STORE) { - TNode left = term[0]; - TNode right = term[1]; - int leftWrites = 0, rightWrites = 0; - - // Count nested writes - TNode e1 = left; - while (e1.getKind() == kind::STORE) { - ++leftWrites; - e1 = e1[0]; - } - - TNode e2 = right; - while (e2.getKind() == kind::STORE) { - ++rightWrites; - e2 = e2[0]; - } - - if (rightWrites > leftWrites) { - TNode tmp = left; - left = right; - right = tmp; - int tmpWrites = leftWrites; - leftWrites = rightWrites; - rightWrites = tmpWrites; - } - - NodeManager* nm = NodeManager::currentNM(); - if (rightWrites == 0) { - if (e1 == e2) { - // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF - // - // read(store, index_n) = v_n & - // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} & - // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} & - // ... - // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1 - // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0 - TNode write_i, write_j, index_i, index_j; - Node conc; - NodeBuilder<> result(kind::AND); - int i, j; - write_i = left; - for (i = leftWrites-1; i >= 0; --i) { - index_i = write_i[1]; - - // build: [index_i /= index_n && index_i /= index_(n-1) && - // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i - write_j = left; - { - NodeBuilder<> hyp(kind::AND); - for (j = leftWrites - 1; j > i; --j) { - index_j = write_j[1]; - if (!ppDisequal(index_i, index_j)) { - Node hyp2(index_i.getType() == nm->booleanType()? - index_i.iffNode(index_j) : index_i.eqNode(index_j)); - hyp << hyp2.notNode(); - } - write_j = write_j[0]; - } - - Node r1 = nm->mkNode(kind::SELECT, e1, index_i); - conc = (r1.getType() == nm->booleanType())? - r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); - if (hyp.getNumChildren() != 0) { - if (hyp.getNumChildren() == 1) { - conc = hyp.getChild(0).impNode(conc); - } - else { - r1 = hyp; - conc = r1.impNode(conc); - } - } - - // And into result - result << conc; - - // Prepare for next iteration - write_i = write_i[0]; - } - } - Assert(result.getNumChildren() > 0); - if (result.getNumChildren() == 1) { - return result.getChild(0); - } - return result; - } - break; - } - else { - if (!d_solveWrite2) break; - // store(...) = store(a,i,v) ==> - // store(store(...),i,select(a,i)) = a && select(store(...),i)=v - Node l = left; - Node tmp; - NodeBuilder<> nb(kind::AND); - while (right.getKind() == kind::STORE) { - tmp = nm->mkNode(kind::SELECT, l, right[1]); - nb << tmp.eqNode(right[2]); - tmp = nm->mkNode(kind::SELECT, right[0], right[1]); - l = nm->mkNode(kind::STORE, l, right[1], tmp); - right = right[0]; - } - nb << l.eqNode(right); - return nb; - } - } + return solveWrite(term, d_solveWrite, d_solveWrite2, true); break; } default: @@ -330,6 +355,9 @@ bool TheoryArrays::propagate(TNode literal) } // Propagate away + if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) { + return true; + } bool ok = d_out->propagate(literal); if (!ok) { d_conflict = true; @@ -453,6 +481,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); + d_infoMap.setModelRep(node, node); checkStore(node); break; @@ -821,7 +850,40 @@ void TheoryArrays::presolve() ///////////////////////////////////////////////////////////////////////////// +Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual) +{ + Node skolem; + std::hash_map::iterator it = d_skolemCache.find(ref); + if (it == d_skolemCache.end()) { + NodeManager* nm = NodeManager::currentNM(); + skolem = nm->mkSkolem(name, type, comment); + d_skolemCache[ref] = skolem; + } + else { + skolem = (*it).second; + if (d_equalityEngine.hasTerm(ref) && + d_equalityEngine.hasTerm(skolem) && + d_equalityEngine.areEqual(ref, skolem)) { + makeEqual = false; + } + } + preRegisterTermInternal(skolem); + if (makeEqual) { + Node d = skolem.eqNode(ref); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + Assert(!d_conflict); + d_skolemAssertions.push_back(d); + d_skolemIndex = d_skolemIndex + 1; + } + return skolem; +} + + void TheoryArrays::check(Effort e) { + if (done() && !fullEffort(e)) { + return; + } TimerStat::CodeTimer codeTimer(d_checkTimer); while (!done() && !d_conflict) @@ -852,13 +914,18 @@ void TheoryArrays::check(Effort e) { switch (fact.getKind()) { case kind::EQUAL: d_equalityEngine.assertEquality(fact, true, fact); + if (!fact[0].getType().isArray()) { + d_modelConstraints.push_back(fact); + } break; case kind::SELECT: d_equalityEngine.assertPredicate(fact, true, fact); + d_modelConstraints.push_back(fact); break; case kind::NOT: if (fact[0].getKind() == kind::SELECT) { d_equalityEngine.assertPredicate(fact[0], false, fact); + d_modelConstraints.push_back(fact); } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) { // Assert the dis-equality d_equalityEngine.assertEquality(fact[0], false, fact); @@ -867,16 +934,7 @@ void TheoryArrays::check(Effort e) { if(fact[0][0].getType().isArray() && !d_conflict) { NodeManager* nm = NodeManager::currentNM(); TypeNode indexType = fact[0][0].getType()[0]; - TNode k; - std::hash_map::iterator it = d_diseqCache.find(fact); - if (it == d_diseqCache.end()) { - Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays"); - d_diseqCache[fact] = newk; - k = newk; - } - else { - k = (*it).second; - } + TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false); Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); @@ -887,6 +945,9 @@ void TheoryArrays::check(Effort e) { d_out->lemma(lemma); ++d_numExt; } + else { + d_modelConstraints.push_back(fact); + } } break; default: @@ -894,8 +955,11 @@ void TheoryArrays::check(Effort e) { } } - // If in conflict, output the conflict - if(!d_eagerLemmas && fullEffort(e) && !d_conflict) { + if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) { + checkModel(); + } + + if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { // generate the lemmas on the worklist Trace("arrays-lem")<<"Arrays::discharging lemmas: "<& assumptions, TNode nodeSkip) +{ + Assert(node.getKind() == kind::AND); + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if ((*child_it).getKind() == kind::AND) { + convertNodeToAssumptions(*child_it, assumptions, nodeSkip); + } + else if (*child_it != nodeSkip) { + assumptions.push_back(*child_it); + } + } +} + + +void TheoryArrays::preRegisterStores(TNode s) +{ + if (d_equalityEngine.hasTerm(s)) { + return; + } + if (s.getKind() == kind::STORE) { + preRegisterStores(s[0]); + preRegisterTermInternal(s); + } +} + + +void TheoryArrays::checkModel() +{ + d_inCheckModel = true; + d_topLevel = getSatContext()->getLevel(); + Assert(d_skolemIndex == 0); + Assert(d_skolemAssertions.empty()); + + // TODO: record and replay decisions + unsigned constraintIdx; + Node assertion, assertionToCheck; + vector assumptions; + while (true) { + int level = getSatContext()->getLevel(); + d_getModelValCache.clear(); + for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) { + assertion = d_modelConstraints[constraintIdx]; + if (getModelValRec(assertion) != d_true) { + break; + } + } + getSatContext()->popto(level); + if (constraintIdx == d_modelConstraints.size()) { + break; + } + + if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) { + assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false); + if (assertionToCheck.getKind() == kind::AND && + assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) { + TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0]; + preRegisterStores(s); + } + } + else { + assertionToCheck = assertion; + } + // TODO: try not collecting assumptions the first time + while (!setModelVal(assertionToCheck, d_true, false, true, assumptions)) { + restart: + if (assertion.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(assertion[0], assertion[1], true, assumptions); + } + else { + assumptions.push_back(assertion); + } +#ifdef CVC4_ASSERTIONS + std::set validAssumptions; + context::CDList::const_iterator assert_it2 = facts_begin(); + for (; assert_it2 != facts_end(); ++assert_it2) { + validAssumptions.insert(*assert_it2); + } + for (unsigned i = 0; i < d_decisions.size(); ++i) { + validAssumptions.insert(d_decisions[i]); + } +#endif + std::set all; + std::set explained; + unsigned i = 0; + TNode t; + for (; i < assumptions.size(); ++i) { + t = assumptions[i]; + if (t == d_true) { + continue; + } + 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()); + all.insert(*child_it); + } + } + // Expand explanation resulting from propagating a ROW lemma + else if (t.getKind() == kind::OR) { + if ((explained.find(t) == explained.end())) { + Assert(t[1].getKind() == kind::EQUAL); + d_equalityEngine.explainEquality(t[1][0], t[1][1], false, assumptions); + explained.insert(t); + } + continue; + } + else { + // Assert(validAssumptions.find(t) != validAssumptions.end()); + all.insert(t); + } + } + + bool eq = false; + Node decision, explanation; + while (!d_decisions.empty()) { + getSatContext()->pop(); + decision = d_decisions.back(); + d_decisions.pop_back(); + if (all.find(decision) != all.end()) { + 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()) { + getSatContext()->pop(); + d_decisions.pop_back(); + } + break; + } + else { + decision = Node(); + } + } + if (all.size() == 0) { + explanation = d_true; + } + if (all.size() == 1) { + // All the same, or just one + explanation = *(all.begin()); + } + else { + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++it; + } + explanation = conjunction; + d_permRef.push_back(explanation); + } + if (decision.isNull()) { + d_conflictNode = explanation; + d_conflict = true; + break; + } + d_equalityEngine.assertEquality(decision, eq, explanation); + if (!eq) decision = decision.notNode(); + Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl; + if (d_conflict) { + assumptions.clear(); + convertNodeToAssumptions(d_conflictNode, assumptions, TNode()); + assertion = d_true; + goto restart; + } + assumptions.clear(); + + // Reassert skolems if necessary + Node d; + while (d_skolemIndex < d_skolemAssertions.size()) { + d = d_skolemAssertions[d_skolemIndex]; + Assert(isLeaf(d[0])); + if (!d_equalityEngine.hasTerm(d[0])) { + preRegisterTermInternal(d[0]); + } + 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]); + } + 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); + Assert(!d_conflict); + if (!d[0].getType().isArray()) { + if (!setModelVal(d[1], d[0], false, true, assumptions)) { + assertion = d_true; + goto restart; + } + assumptions.clear(); + } + d_skolemIndex = d_skolemIndex + 1; + } + } + if (d_conflict) { + break; + } + Assert(getModelVal(assertion) == d_true); + assumptions.clear(); + } +#ifdef CVC4_ASSERTIONS + if (!d_conflict) { + context::CDList::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); + for (; assert_it != assert_it_end; ++assert_it) { + Assert(getModelVal(*assert_it) == d_true); + } + } +#endif + while (!d_decisions.empty()) { + Assert(!d_conflict); + getSatContext()->pop(); + d_decisions.pop_back(); + } + d_skolemAssertions.clear(); + d_skolemIndex = 0; + Assert(getSatContext()->getLevel() == d_topLevel); + if (d_conflict) { + Node tmp = d_conflictNode; + d_out->conflict(tmp); + } + d_inCheckModel = false; +} + + +Node TheoryArrays::getModelVal(TNode node) +{ + int level = getSatContext()->getLevel(); + d_getModelValCache.clear(); + Node ret = getModelValRec(node); + getSatContext()->popto(level); + return ret; +} + + +Node TheoryArrays::getModelValRec(TNode node) +{ + if (node.isConst()) { + return node; + } + NodeMap::iterator it = d_getModelValCache.find(node); + if (it != d_getModelValCache.end()) { + return (*it).second; + } + Node val; + switch (node.getKind()) { + case kind::NOT: + val = getModelValRec(node[0]) == d_true ? d_false : d_true; + break; + case kind::AND: { + val = d_true; + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if (getModelValRec(*child_it) != d_true) { + val = d_false; + break; + } + } + break; + } + case kind::IMPLIES: + if (getModelValRec(node[0]) == d_false) { + val = d_true; + } + else { + val = getModelValRec(node[1]); + } + case kind::EQUAL: + val = getModelValRec(node[0]); + val = (val == getModelValRec(node[1])) ? d_true : d_false; + break; + case kind::SELECT: { + NodeManager* nm = NodeManager::currentNM(); + Node indexVal = getModelValRec(node[1]); + val = Rewriter::rewrite(nm->mkNode(kind::SELECT, node[0], indexVal)); + if (val.isConst()) { + break; + } + val = Rewriter::rewrite(nm->mkNode(kind::SELECT, getModelValRec(node[0]), indexVal)); + Assert(val.isConst()); + break; + } + case kind::STORE: { + NodeManager* nm = NodeManager::currentNM(); + val = getModelValRec(node[0]); + val = Rewriter::rewrite(nm->mkNode(kind::STORE, val, getModelValRec(node[1]), getModelValRec(node[2]))); + Assert(val.isConst()); + break; + } + default: { + Assert(isLeaf(node)); + TNode eRep = d_equalityEngine.getRepresentative(node); + if (eRep.isConst()) { + val = eRep; + break; + } + TNode rep = d_infoMap.getModelRep(eRep); + if (!rep.isNull()) { + // TODO: check for loop here + val = getModelValRec(rep); + } + else { + NodeMap::iterator it = d_lastVal.find(eRep); + if (it != d_lastVal.end()) { + val = (*it).second; + if (!d_equalityEngine.hasTerm(val) || + !d_equalityEngine.areDisequal(eRep, val, true)) { + getSatContext()->push(); + ++d_numGetModelValSplits; + d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); + if (!d_conflict) { + break; + } + ++d_numGetModelValConflicts; + getSatContext()->pop(); + } + } + + TypeEnumerator te(eRep.getType()); + val = *te; + while (true) { + if (!d_equalityEngine.hasTerm(val) || + !d_equalityEngine.areDisequal(eRep, val, true)) { + getSatContext()->push(); + ++d_numGetModelValSplits; + d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); + if (!d_conflict) { + d_lastVal[eRep] = val; + break; + } + ++d_numGetModelValConflicts; + getSatContext()->pop(); + } + ++te; + if (te.isFinished()) { + Assert(false); + // TODO: conflict + break; + } + val = *te; + } + } + break; + } + } + d_getModelValCache[node] = val; + return val; +} + + +bool TheoryArrays::hasLoop(TNode node, TNode target) +{ + if (node == target) { + return true; + } + + if (isLeaf(node)) { + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); + if (!rep.isNull()) { + return hasLoop(rep, target); + } + return false; + } + + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if (hasLoop(*child_it, target)) { + return true; + } + } + + return false; +} + + +// Return true iff it we were able to modify model so that value of node has same value as val +bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, vector& assumptions) +{ + Assert(!d_conflict); + if (node == val) { + return !invert; + } + if (node.isConst()) { + if (invert) { + return (val.isConst() && node != val); + } + return val == node; + } + switch(node.getKind()) { + case kind::NOT: + Assert(val == d_true || val == d_false); + return setModelVal(node[0], val, !invert, explain, assumptions); + break; + case kind::AND: { + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + int i; + for(i = node.getNumChildren()-1; i >=0; --i) { + if (setModelVal(node[i], d_true, invert, explain, assumptions) == invert) { + return invert; + } + } + return !invert; + } + case kind::IMPLIES: + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + if (setModelVal(node[0], d_false, invert, explain, assumptions) == !invert) { + return !invert; + } + if (setModelVal(node[1], d_true, invert, explain, assumptions) == !invert) { + return !invert; + } + return invert; + case kind::EQUAL: + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + if (node[0].isConst()) { + return setModelVal(node[1], node[0], invert, explain, assumptions); + } + else { + return setModelVal(node[0], node[1], invert, explain, assumptions); + } + case kind::SELECT: { + TNode s = node[0]; + Node index = node[1]; + + while (s.getKind() == kind::STORE) { + if (setModelVal(s[1].eqNode(index), d_true, false, explain, assumptions)) { + if (setModelVal(s[2].eqNode(val), d_true, invert, explain, assumptions)) { + return true; + } + // Now try to set the indices to be disequal + if (!setModelVal(s[1].eqNode(index), d_false, false, explain, assumptions)) { + return false; + } + Unreachable(); + } + s = s[0]; + } + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(s)); + NodeManager* nm = NodeManager::currentNM(); + if (!rep.isNull()) { + // TODO: check for loop + if (explain) { + d_equalityEngine.explainEquality(s, rep, true, assumptions); + } + return setModelVal(nm->mkNode(kind::SELECT, rep, index), val, invert, explain, assumptions); + } + if (val.getKind() == kind::SELECT && val[0].getKind() == kind::STORE) { + return setModelVal(val, nm->mkNode(kind::SELECT, s, index), invert, explain, assumptions); + } + + // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val + Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false); + Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull()); + Node lookup; + bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false; + if (!isLeaf(index)) { + index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays"); + if (!index.getType().isArray()) { + checkIndex1 = true; + } + } + lookup = nm->mkNode(kind::SELECT, s, index); + Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + + Node newVarVal2; + Node index2; + TNode saveVal = val; + if (val.getKind() == kind::SELECT && val[0] == s) { + // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w' + index2 = val[1]; + if (!isLeaf(index2)) { + index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays"); + if (!index2.getType().isArray()) { + checkIndex2 = true; + } + } + if (invert) { + checkIndex3 = true; + } + lookup = nm->mkNode(kind::SELECT, s, index2); + newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2); + preRegisterTermInternal(newVarArr); + val = newVarVal2; + } + + Node d = nm->mkNode(kind::STORE, newVarArr, index, newVarVal); + preRegisterTermInternal(d); + d = s.eqNode(d); + Debug("arrays-model-based") << "Asserting array skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_skolemAssertions.push_back(d); + d_skolemIndex = d_skolemIndex + 1; + Assert(!d_conflict); + if (checkIndex1) { + if (!setModelVal(node[1], index, false, explain, assumptions)) { + return false; + } + } + if (checkIndex2) { + if (!setModelVal(saveVal[1], index2, false, explain, assumptions)) { + return false; + } + } + if (checkIndex3) { + if (!setModelVal(index2, index, true, explain, assumptions)) { + return false; + } + } + return setModelVal(newVarVal, val, invert, explain, assumptions); + } + case kind::STORE: + if (val.getKind() != kind::STORE) { + return setModelVal(val, node, invert, explain, assumptions); + } + Unreachable(); + break; + default: { + Assert(isLeaf(node)); + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); + if (!rep.isNull()) { + // Assume this array equation has already been dealt with - otherwise, it shouldn't have a rep + return true; + } + if (val.getKind() == kind::SELECT) { + return setModelVal(val, node, invert, explain, assumptions); + } + if (d_equalityEngine.hasTerm(node) && + d_equalityEngine.hasTerm(val)) { + if ((!invert && d_equalityEngine.areDisequal(node, val, true)) || + (invert && d_equalityEngine.areEqual(node, val))) { + if (explain) { + d_equalityEngine.explainEquality(node, val, invert, assumptions); + } + return false; + } + if ((!invert && d_equalityEngine.areEqual(node, val)) || + (invert && d_equalityEngine.areDisequal(node, val, true))) { + return true; + } + } + getSatContext()->push(); + Node d = node.eqNode(val); + d_decisions.push_back(invert ? d.notNode() : d); + 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) { + ++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]; + } + Node explanation = conjunction; + getSatContext()->pop(); + d_decisions.pop_back(); + d_permRef.push_back(explanation); + d = d.negate(); + Debug("arrays-model-based") << "Asserting learned literal " << d << " with explanation " << explanation << endl; + bool eq = true; + if (d.getKind() == kind::NOT) { + d = d[0]; + eq = false; + } + d_equalityEngine.assertEquality(d, eq, explanation); + if (d_conflict) { + Assert(false); + } + return false; + } + return true; + } + } + Unreachable(); + return false; +} + + Node TheoryArrays::mkAnd(std::vector& conjunctions) { Assert(conjunctions.size() > 0); @@ -916,6 +1573,15 @@ Node TheoryArrays::mkAnd(std::vector& conjunctions) TNode t; for (; i < conjunctions.size(); ++i) { t = conjunctions[i]; + if (t == d_true) { + continue; + } + + if (t.getKind() == kind::AND) { + for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { + all.insert(*child_it); + } + } // Expand explanation resulting from propagating a ROW lemma if (t.getKind() == kind::OR) { @@ -951,6 +1617,7 @@ Node TheoryArrays::mkAnd(std::vector& conjunctions) void TheoryArrays::setNonLinear(TNode a) { + if (options::arraysModelBased()) return; if (d_infoMap.isNonLinear(a)) return; Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; @@ -1063,6 +1730,86 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) } +Node TheoryArrays::removeRepLoops(TNode a, TNode rep) +{ + if (rep.getKind() != kind::STORE) { + Assert(isLeaf(rep)); + TNode tmp = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(rep)); + if (!tmp.isNull()) { + Node tmp2 = removeRepLoops(a, tmp); + if (tmp != tmp2) { + return tmp2; + } + } + return rep; + } + + Node s = removeRepLoops(a, rep[0]); + bool changed = (s != rep[0]); + + Node index = rep[1]; + Node value = rep[2]; + Node lookup; + + // TODO: Change to hasLoop? + if (!isLeaf(index)) { + changed = true; + index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false); + if (!d_equalityEngine.hasTerm(index) || + !d_equalityEngine.hasTerm(rep[1]) || + !d_equalityEngine.areEqual(rep[1], index)) { + Node d = index.eqNode(rep[1]); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_modelConstraints.push_back(d); + } + } + if (!isLeaf(value)) { + changed = true; + value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false); + if (!d_equalityEngine.hasTerm(value) || + !d_equalityEngine.hasTerm(rep[2]) || + !d_equalityEngine.areEqual(rep[2], value)) { + Node d = value.eqNode(rep[2]); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_modelConstraints.push_back(d); + } + } + if (changed) { + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STORE, s, index, value); + } + return rep; +} + + +Node TheoryArrays::expandStores(TNode s, vector& assumptions, bool checkLoop, TNode a, TNode loopRep) +{ + if (s.getKind() != kind::STORE) { + Assert(isLeaf(s)); + TNode tmp = d_equalityEngine.getRepresentative(s); + if (checkLoop && tmp == a) { + // Loop detected + d_equalityEngine.explainEquality(s, loopRep, true, assumptions); + return loopRep; + } + tmp = d_infoMap.getModelRep(tmp); + if (!tmp.isNull()) { + d_equalityEngine.explainEquality(s, tmp, true, assumptions); + return expandStores(tmp, assumptions, checkLoop, a, loopRep); + } + return s; + } + Node tmp = expandStores(s[0], assumptions, checkLoop, a, loopRep); + if (tmp != s[0]) { + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STORE, tmp, s[1], s[2]); + } + return s; +} + + void TheoryArrays::mergeArrays(TNode a, TNode b) { // Note: a is the new representative @@ -1085,7 +1832,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) checkRIntro1(b, a); } - if (options::arraysOptimizeLinear()) { + if (options::arraysOptimizeLinear() && !options::arraysModelBased()) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); if (aNL) { @@ -1120,6 +1867,74 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) checkRowLemmas(a,b); checkRowLemmas(b,a); + if (options::arraysModelBased()) { + TNode repA = d_infoMap.getModelRep(a); + Assert(repA.isNull() || d_equalityEngine.areEqual(a, repA)); + TNode repB = d_infoMap.getModelRep(b); + Assert(repB.isNull() || d_equalityEngine.areEqual(a, repB)); + Node rep; + bool done = false; + if (repA.isNull()) { + if (repB.isNull()) { + done = true; + } + else { + rep = repB; + } + } + else { + if (repB.isNull()) { + rep = repA; + } + else { + vector assumptions; + rep = expandStores(repA, assumptions, true, a, repB); + if (rep != repA) { + Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; + d_infoMap.setModelRep(a, rep); + Node reason = mkAnd(assumptions); + d_permRef.push_back(reason); + d_equalityEngine.assertEquality(repA.eqNode(rep), true, reason); + } + d_modelConstraints.push_back(rep.eqNode(repB)); + done = true; + } + } + if (!done) { + // 1. Check for store loop + TNode s = rep; + while (true) { + Assert(s.getKind() == kind::STORE); + while (s.getKind() == kind::STORE) { + s = s[0]; + } + Assert(isLeaf(s)); + TNode tmp = d_equalityEngine.getRepresentative(s); + if (tmp == a) { + d_modelConstraints.push_back(s.eqNode(rep)); + rep = TNode(); + break; + } + tmp = d_infoMap.getModelRep(tmp); + if (tmp.isNull()) { + break; + } + s = tmp; + } + if (!rep.isNull()) { + Node repOrig = rep; + rep = removeRepLoops(a, rep); + if (repOrig != rep) { + d_equalityEngine.assertEquality(repOrig.eqNode(rep), true, d_true); + } + } + if (rep != repA) { + Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; + d_infoMap.setModelRep(a, rep); + } + } + } + // merge info adds the list of the 2nd argument to the first d_infoMap.mergeInfo(a, b); @@ -1139,6 +1954,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) void TheoryArrays::checkStore(TNode a) { + if (options::arraysModelBased()) return; Trace("arrays-cri")<<"Arrays::checkStore "<print(); @@ -1323,7 +2141,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } // Prefer equality between indexes so as not to introduce new read terms - if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { + if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); getOutputChannel().requirePhase(i_eq_j, true); d_decisionRequests.push(i_eq_j); @@ -1494,7 +2312,9 @@ void TheoryArrays::conflict(TNode a, TNode b) { } else { d_conflictNode = explain(a.eqNode(b)); } - d_out->conflict(d_conflictNode); + if (!d_inCheckModel) { + d_out->conflict(d_conflictNode); + } d_conflict = true; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 172482e71..ef1f3b506 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -115,6 +115,14 @@ class TheoryArrays : public Theory { IntStat d_numNonLinear; /** splits on array variables */ IntStat d_numSharedArrayVarSplits; + /** splits in getModelVal */ + IntStat d_numGetModelValSplits; + /** conflicts in getModelVal */ + IntStat d_numGetModelValConflicts; + /** splits in setModelVal */ + IntStat d_numSetModelValSplits; + /** conflicts in setModelVal */ + IntStat d_numSetModelValConflicts; /** time spent in check() */ TimerStat d_checkTimer; @@ -152,6 +160,7 @@ class TheoryArrays : public Theory { Node preprocessTerm(TNode term); Node recursivePreprocessTerm(TNode term); bool ppDisequal(TNode a, TNode b); + Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck); public: @@ -339,17 +348,23 @@ class TheoryArrays : public Theory { CDNodeSet d_sharedOther; context::CDO d_sharedTerms; context::CDList d_reads; - std::hash_map d_diseqCache; + std::hash_map d_skolemCache; + context::CDO d_skolemIndex; + std::vector d_skolemAssertions; // The decision requests we have for the core context::CDQueue d_decisionRequests; // List of nodes that need permanent references in this context context::CDList d_permRef; + context::CDList d_modelConstraints; + Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); Node mkAnd(std::vector& conjunctions); void setNonLinear(TNode a); void checkRIntro1(TNode a, TNode b); + Node removeRepLoops(TNode a, TNode rep); + Node expandStores(TNode s, std::vector& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode()); void mergeArrays(TNode a, TNode b); void checkStore(TNode a); void checkRowForIndex(TNode i, TNode a); @@ -357,6 +372,21 @@ class TheoryArrays : public Theory { void queueRowLemma(RowLemmaType lem); void dischargeLemmas(); + std::vector d_decisions; + bool d_inCheckModel; + int d_topLevel; + void convertNodeToAssumptions(TNode node, std::vector& assumptions, TNode nodeSkip); + void preRegisterStores(TNode s); + void checkModel(); + bool hasLoop(TNode node, TNode target); + typedef std::hash_map NodeMap; + NodeMap d_getModelValCache; + NodeMap d_lastVal; + Node getModelVal(TNode node); + Node getModelValRec(TNode node); + bool setModelVal(TNode node, TNode val, bool invert, + bool explain, std::vector& assumptions); + public: eq::EqualityEngine* getEqualityEngine() {