diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 1577 |
1 files changed, 787 insertions, 790 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 03a9d7a4c..718483143 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,45 +23,87 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" +#include "theory/uf/equality_engine_impl.h" + using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::arrays; -TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : +namespace CVC4 { +namespace theory { +namespace arrays { + + +// These are the options that produce the best empirical results on QF_AX benchmarks. +// Use static configuration of options for now +const bool d_ccStore = false; +const bool d_useArrTable = false; +const bool d_eagerLemmas = true; +const bool d_propagateLemmas = false; +const bool d_preprocess = true; +const bool d_solveWrite = true; +const bool d_useNonLinearOpt = true; + + +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARRAY, c, u, out, valuation), - d_ccChannel(this), - d_cc(c, &d_ccChannel), - d_unionFind(c), - d_backtracker(c), - d_infoMap(c,&d_backtracker), - d_disequalities(c), - d_equalities(c), - d_prop_queue(c), - d_atoms(), - d_explanations(c), - d_conflict(), d_numRow("theory::arrays::number of Row lemmas", 0), d_numExt("theory::arrays::number of Ext lemmas", 0), d_numProp("theory::arrays::number of propagations", 0), 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_checkTimer("theory::arrays::checkTime"), - d_donePreregister(false) + d_ppNotify(), + d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"), + d_ppFacts(u), + // d_ppCache(u), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_mayEqualNotify(), + d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"), + d_conflict(c, false), + d_backtracker(c), + d_infoMap(c, &d_backtracker), + d_mergeQueue(c), + d_mergeInProgress(false), + d_RowQueue(u), + d_RowAlreadyAdded(u), + d_sharedArrays(c), + d_sharedTerms(c, false), + d_reads(c), + d_permRef(c) { - //d_backtracker = new Backtracker<TNode>(c); - //d_infoMap = ArrayInfo(c, d_backtracker); - StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); StatisticsRegistry::registerStat(&d_numProp); StatisticsRegistry::registerStat(&d_numExplain); + StatisticsRegistry::registerStat(&d_numNonLinear); + StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); StatisticsRegistry::registerStat(&d_checkTimer); + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); + + d_ppEqualityEngine.addTerm(d_true); + d_ppEqualityEngine.addTerm(d_false); + d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false); + + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::SELECT); + if (d_ccStore) { + d_equalityEngine.addFunctionKind(kind::STORE); + } + d_equalityEngine.addFunctionKind(kind::EQUAL); + if (d_useArrTable) { + d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN); + } } @@ -71,159 +113,27 @@ TheoryArrays::~TheoryArrays() { StatisticsRegistry::unregisterStat(&d_numExt); StatisticsRegistry::unregisterStat(&d_numProp); StatisticsRegistry::unregisterStat(&d_numExplain); + StatisticsRegistry::unregisterStat(&d_numNonLinear); + StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits); StatisticsRegistry::unregisterStat(&d_checkTimer); } -void TheoryArrays::addSharedTerm(TNode t) { - Trace("arrays") << "Arrays::addSharedTerm(): " - << t << endl; -} - - -void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { -} - -void TheoryArrays::notifyCongruent(TNode a, TNode b) { - Trace("arrays") << "Arrays::notifyCongruent(): " - << a << " = " << b << endl; - if(!d_conflict.isNull()) { - return; - } - merge(a,b); -} - - -void TheoryArrays::check(Effort e) { - TimerStat::CodeTimer codeTimer(d_checkTimer); - - if(!d_donePreregister ) { - // only start looking for lemmas after preregister on all input terms - // has been called - return; - } - - Trace("arrays") <<"Arrays::start check "; - while(!done()) { - Node assertion = get(); - Trace("arrays") << "Arrays::check(): " << assertion << endl; - - switch(assertion.getKind()) { - case kind::EQUAL: - case kind::IFF: - d_cc.addEquality(assertion); - if(!d_conflict.isNull()) { - // addEquality can cause a notify congruent which calls merge - // which can lead to a conflict - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - merge(assertion[0], assertion[1]); - break; - case kind::NOT: - { - Assert(assertion[0].getKind() == kind::EQUAL || - assertion[0].getKind() == kind::IFF ); - Node a = assertion[0][0]; - Node b = assertion[0][1]; - addDiseq(assertion[0]); - - d_cc.addTerm(a); - d_cc.addTerm(b); - - if(!d_conflict.isNull()) { - // we got notified through notifyCongruent which called merge - // after addTerm since we weren't watching a or b before - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - else if(find(a) == find(b)) { - Node conflict = constructConflict(assertion[0]); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - Assert(!d_cc.areCongruent(a,b)); - if(a.getType().isArray()) { - queueExtLemma(a, b); - } - break; - } - default: - Unhandled(assertion.getKind()); - } - - } - - if(fullEffort(e)) { - // generate the lemmas on the worklist - //while(!d_RowQueue.empty() || ! d_extQueue.empty()) { - dischargeLemmas(); - Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n"; - //} - } - Trace("arrays") << "Arrays::check(): done" << endl; -} - -Node TheoryArrays::getValue(TNode n) { - NodeManager* nodeManager = NodeManager::currentNM(); - - switch(n.getKind()) { +///////////////////////////////////////////////////////////////////////////// +// PREPROCESSING +///////////////////////////////////////////////////////////////////////////// - case kind::VARIABLE: - Unhandled(kind::VARIABLE); - - case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - - default: - Unhandled(n.getKind()); - } -} - -Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - switch(in.getKind()) { - case kind::EQUAL: - { - d_staticFactManager.addEq(in); - if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { - outSubstitutions.addSubstitution(in[0], in[1]); - return PP_ASSERT_STATUS_SOLVED; - } - if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { - outSubstitutions.addSubstitution(in[1], in[0]); - return PP_ASSERT_STATUS_SOLVED; - } - break; - } - case kind::NOT: - { - Assert(in[0].getKind() == kind::EQUAL || - in[0].getKind() == kind::IFF ); - Node a = in[0][0]; - Node b = in[0][1]; - d_staticFactManager.addDiseq(in[0]); - break; - } - default: - break; - } - return PP_ASSERT_STATUS_UNSOLVED; -} -Node TheoryArrays::preprocessTerm(TNode term) { +Node TheoryArrays::ppRewrite(TNode term) { + if (!d_preprocess) return term; switch (term.getKind()) { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j if (term[0].getKind() == kind::STORE && - d_staticFactManager.areDiseq(term[0][1], term[1])) { + (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) || + (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; } break; @@ -233,7 +143,8 @@ Node TheoryArrays::preprocessTerm(TNode term) { // IF i != j and j comes before i in the ordering if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && - d_staticFactManager.areDiseq(term[1], term[0][1])) { + (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) || + (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2]; Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2]; return outer; @@ -241,6 +152,7 @@ Node TheoryArrays::preprocessTerm(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]; @@ -295,7 +207,8 @@ Node TheoryArrays::preprocessTerm(TNode term) { NodeBuilder<> hyp(kind::AND); for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; - if (d_staticFactManager.areDiseq(index_i, index_j)) { + if (d_ppEqualityEngine.areDisequal(index_i, index_j) || + (index_i.isConst() && index_j.isConst() && index_i != index_j)) { continue; } Node hyp2(index_i.getType() == nm->booleanType()? @@ -338,7 +251,7 @@ Node TheoryArrays::preprocessTerm(TNode term) { Node l = left; Node tmp; NodeBuilder<> nb(kind::AND); - while (right.getKind() == STORE) { + 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]); @@ -357,699 +270,683 @@ Node TheoryArrays::preprocessTerm(TNode term) { return term; } -Node TheoryArrays::recursivePreprocessTerm(TNode term) { - unsigned nc = term.getNumChildren(); - if (nc == 0 || - (theoryOf(term) != theory::THEORY_ARRAY && - term.getType() != NodeManager::currentNM()->booleanType())) { - return term; - } - NodeMap::iterator find = d_ppCache.find(term); - if (find != d_ppCache.end()) { - return (*find).second; - } - NodeBuilder<> newNode(term.getKind()); - unsigned i; - for (i = 0; i < nc; ++i) { - newNode << recursivePreprocessTerm(term[i]); - } - Node newTerm = Rewriter::rewrite(newNode); - Node newTerm2 = preprocessTerm(newTerm); - if (newTerm != newTerm2) { - newTerm = recursivePreprocessTerm(Rewriter::rewrite(newTerm2)); - } - d_ppCache[term] = newTerm; - return newTerm; -} -Node TheoryArrays::ppRewrite(TNode atom) { - if (d_donePreregister) return atom; - Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str()); - return recursivePreprocessTerm(atom); +Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { + switch(in.getKind()) { + case kind::EQUAL: + { + d_ppFacts.push_back(in); + d_ppEqualityEngine.addEquality(in[0], in[1], in); + if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + outSubstitutions.addSubstitution(in[0], in[1]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + outSubstitutions.addSubstitution(in[1], in[0]); + return PP_ASSERT_STATUS_SOLVED; + } + break; + } + case kind::NOT: + { + d_ppFacts.push_back(in); + Assert(in[0].getKind() == kind::EQUAL || + in[0].getKind() == kind::IFF ); + Node a = in[0][0]; + Node b = in[0][1]; + d_ppEqualityEngine.addDisequality(a, b, in); + break; + } + default: + break; + } + return PP_ASSERT_STATUS_UNSOLVED; } -void TheoryArrays::merge(TNode a, TNode b) { - Assert(d_conflict.isNull()); +///////////////////////////////////////////////////////////////////////////// +// T-PROPAGATION / REGISTRATION +///////////////////////////////////////////////////////////////////////////// - Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl; - /* - * take care of the congruence closure part - */ +bool TheoryArrays::propagate(TNode literal) +{ + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl; - // make "a" the one with shorter diseqList - CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a); - CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); + // If already in conflict, no more propagation + if (d_conflict) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl; + return false; + } - if(deq_ia != d_disequalities.end()) { - if(deq_ib == d_disequalities.end() || - (*deq_ia).second->size() > (*deq_ib).second->size()) { - TNode tmp = a; - a = b; - b = tmp; + // See if the literal has been asserted already + Node normalized = Rewriter::rewrite(literal); + bool satValue = false; + bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); + + // If asserted, we're done or in conflict + if (isAsserted) { + if (!satValue) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + std::vector<TNode> assumptions; + Node negatedLiteral; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return false; } + // Propagate even if already known in SAT - could be a new equation between shared terms + // (terms that weren't shared when the literal was asserted!) } - a = find(a); - b = find(b); - if( a == b) { - return; - } + // Nothing, just enqueue it for propagation and mark it as asserted already + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + d_literalsToPropagate.push_back(literal); + return true; +}/* TheoryArrays::propagate(TNode) */ - // b becomes the canon of a - setCanon(a, b); - - deq_ia = d_disequalities.find(a); - map<TNode, TNode> alreadyDiseqs; - if(deq_ia != d_disequalities.end()) { - /* - * Collecting the disequalities of b, no need to check for conflicts - * since the representative of b does not change and we check all the things - * in a's class when we look at the diseq list of find(a) - */ - - CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); - if(deq_ib != d_disequalities.end()) { - CTNodeListAlloc* deq = (*deq_ib).second; - for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) { - TNode deqn = *j; - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - Assert(sp == b || tp == b); - if(sp == b) { - alreadyDiseqs[tp] = deqn; - } else { - alreadyDiseqs[sp] = deqn; - } - } - } - /* - * Looking for conflicts in the a disequality list. Note - * that at this point a and b are already merged. Also has - * the side effect that it adds them to the list of b (which - * became the canonical representative) - */ - - CTNodeListAlloc* deqa = (*deq_ia).second; - for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) { - TNode deqn = (*i); - Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - - if(find(s) == find(t)) { - d_conflict = deqn; +void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::SELECT: + lhs = literal; + rhs = d_true; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); return; - } - Assert( sp == b || tp == b); - - // make sure not to add duplicates - - if(sp == b) { - if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[tp] = deqn; - } } else { - if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[sp] = deqn; - } + // Predicates + lhs = literal[0]; + rhs = d_false; + break; } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} + + /** + * Stores in d_infoMap the following information for each term a of type array: + * + * - all i, such that there exists a term a[i] or a = store(b i v) + * (i.e. all indices it is being read atl; store(b i v) is implicitly read at + * position i due to the implicit axiom store(b i v)[i] = v ) + * + * - all the stores a is congruent to (this information is context dependent) + * + * - all store terms of the form store (a i v) (i.e. in which a appears + * directly; this is invariant because no new store terms are created) + * + * Note: completeness depends on having pre-register called on all the input + * terms before starting to instantiate lemmas. + */ +void TheoryArrays::preRegisterTerm(TNode node) +{ + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; + + switch (node.getKind()) { + case kind::EQUAL: + // Add the terms + // d_equalityEngine.addTerm(node[0]); + // d_equalityEngine.addTerm(node[1]); + d_equalityEngine.addTerm(node); + // Add the trigger for equality + d_equalityEngine.addTriggerEquality(node[0], node[1], node); + d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); + break; + case kind::SELECT: + // Reads + d_equalityEngine.addTerm(node); + // Maybe it's a predicate + // TODO: remove this or keep it if we allow Boolean elements in arrays. + if (node.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerEquality(node, d_true, node); + d_equalityEngine.addTriggerEquality(node, d_false, node.notNode()); } - } - // TODO: check for equality propagations - // a and b are find(a) and find(b) here - checkPropagations(a,b); + d_infoMap.addIndex(node[0], node[1]); + checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0])); + d_reads.push_back(node); + break; - if(a.getType().isArray()) { - checkRowLemmas(a,b); - checkRowLemmas(b,a); - // note the change in order, merge info adds the list of - // the 2nd argument to the first - d_infoMap.mergeInfo(b, a); - } + case kind::STORE: { + d_equalityEngine.addTriggerTerm(node); + TNode a = node[0]; + TNode i = node[1]; + TNode v = node[2]; -} + d_mayEqualEqualityEngine.addEquality(node, node[0], d_true); + NodeManager* nm = NodeManager::currentNM(); + Node ni = nm->mkNode(kind::SELECT, node, i); + if (!d_equalityEngine.hasTerm(ni)) { + preRegisterTerm(ni); + } -void TheoryArrays::checkPropagations(TNode a, TNode b) { - EqLists::const_iterator ita = d_equalities.find(a); - EqLists::const_iterator itb = d_equalities.find(b); + // Apply RIntro1 Rule + d_equalityEngine.addEquality(ni, v, d_true); - if(ita != d_equalities.end()) { - if(itb!= d_equalities.end()) { - // because b is the canonical representative - List<TNode>* eqsa = (*ita).second; - List<TNode>* eqsb = (*itb).second; + d_infoMap.addStore(node, node); + d_infoMap.addInStore(a, node); - for(List<TNode>::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) { - Node eq = *it; - Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); - if(find(eq[0])== find(eq[1])) { - d_prop_queue.push_back(eq); - } - } - eqsb->concat(eqsa); + checkStore(node); + break; + } + default: + // Variables etc + if (node.getType().isArray()) { + d_equalityEngine.addTriggerTerm(node); } else { - List<TNode>* eqsb = new List<TNode>(&d_backtracker); - List<TNode>* eqsa = (*ita).second; - d_equalities.insert(b, eqsb); - eqsb->concat(eqsa); + d_equalityEngine.addTerm(node); } - } else { - List<TNode>* eqsb = new List<TNode>(&d_backtracker); - d_equalities.insert(b, eqsb); - List<TNode>* eqsa = new List<TNode>(&d_backtracker); - d_equalities.insert(a, eqsa); - eqsb->concat(eqsa); + break; } } -bool TheoryArrays::isNonLinear(TNode a) { - Assert(a.getType().isArray()); - const CTNodeList* inst = d_infoMap.getInStores(find(a)); - if(inst->size()<=1) { - return false; - } - return true; -} - -bool TheoryArrays::isAxiom(TNode t1, TNode t2) { - Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n"; - if(t1.getKind() == kind::SELECT) { - TNode a = t1[0]; - TNode i = t1[1]; - - if(a.getKind() == kind::STORE) { - TNode b = a[0]; - TNode j = a[1]; - TNode v = a[2]; - if(i == j && v == t2) { - Trace("arrays-axiom")<<"Arrays::isAxiom true\n"; - return true; +void TheoryArrays::propagate(Effort e) +{ + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl; + if (!d_conflict) { + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; + bool satValue; + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + d_out->propagate(literal); + } else { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; + Node negatedLiteral; + std::vector<TNode> assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; } } } - return false; + } -Node TheoryArrays::constructConflict(TNode diseq) { - Trace("arrays") << "arrays: begin constructConflict()" << endl; - Trace("arrays") << "arrays: using diseq == " << diseq << endl; +Node TheoryArrays::explain(TNode literal) +{ + ++d_numExplain; + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; + std::vector<TNode> assumptions; + explain(literal, assumptions); + return mkAnd(assumptions); +} + - // returns the reason the two terms are equal - Node explanation = d_cc.explain(diseq[0], diseq[1]); +///////////////////////////////////////////////////////////////////////////// +// SHARING +///////////////////////////////////////////////////////////////////////////// - NodeBuilder<> nb(kind::AND); - if(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF) { - // if the explanation is only one literal - if(!isAxiom(explanation[0], explanation[1]) && - !isAxiom(explanation[1], explanation[0])) { - nb<<explanation; - } +void TheoryArrays::addSharedTerm(TNode t) { + Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; + d_equalityEngine.addTriggerTerm(t); + if (t.getType().isArray()) { + d_sharedArrays.insert(t,true); } else { - Assert(explanation.getKind() == kind::AND); - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); i++) { - if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) { - nb<<*i; - } - } + d_sharedTerms = true; } - - nb<<diseq.notNode(); - Node conflict = nb; - Trace("arrays") << "conflict constructed : " << conflict << endl; - return conflict; } -/* -void TheoryArrays::addAtom(TNode eq) { - Assert(eq.getKind() == kind::EQUAL); - - TNode lhs = eq[0]; - TNode rhs = eq[1]; - - appendToAtomList(find(lhs), rhs); - appendToAtomList(find(rhs), lhs); -} -void TheoryArrays::appendToAtomList(TNode a, TNode b) { - Assert(find(a) == a); - - NodeTNodesMap::const_iterator it = d_atoms.find(a); - if(it != d_atoms.end()) { - (*it).second->push_back(b); +EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { + Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)); + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; } - else { - CTNodeList* list = new (true)CTNodeList(getContext()); - list->push_back(b); - d_atoms[a] = list; + if (d_equalityEngine.areDisequal(a, b)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; } - + //TODO: can we be more precise sometimes? + return EQUALITY_UNKNOWN; } -*/ -void TheoryArrays::addEq(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - TNode a = eq[0]; - TNode b = eq[1]; - - // don't need to say find(a) because due to the structure of the lists it gets - // automatically added - appendToEqList(a, eq); - appendToEqList(b, eq); - -} -void TheoryArrays::appendToEqList(TNode n, TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - EqLists::const_iterator it = d_equalities.find(n); - if(it == d_equalities.end()) { - List<TNode>* eqs = new List<TNode>(&d_backtracker); - eqs->append(eq); - d_equalities.insert(n, eqs); - } else { - List<TNode>* eqs = (*it).second; - eqs->append(eq); +void TheoryArrays::computeCareGraph() +{ + if (d_sharedArrays.size() > 0) { + context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); + for (; it1 != iend; ++it1) { + for (it2 = it1, ++it2; it2 != iend; ++it2) { + EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first); + if (eqStatusArr != EQUALITY_UNKNOWN) { + continue; + } + Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN); + addCarePair((*it1).first, (*it2).first); + ++d_numSharedArrayVarSplits; + return; + } + } } -} + if (d_sharedTerms) { -void TheoryArrays::addDiseq(TNode diseq) { - Assert(diseq.getKind() == kind::EQUAL || - diseq.getKind() == kind::IFF); - TNode a = diseq[0]; - TNode b = diseq[1]; + vector< pair<TNode, TNode> > currentPairs; - appendToDiseqList(find(a), diseq); - appendToDiseqList(find(b), diseq); + // Go through the read terms and see if there are any to split on + unsigned size = d_reads.size(); + for (unsigned i = 0; i < size; ++ i) { + TNode r1 = d_reads[i]; -} + for (unsigned j = i + 1; j < size; ++ j) { + TNode r2 = d_reads[j]; -void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { - Trace("arrays") << "appending " << eq << endl - << " to diseq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - CNodeTNodesMap::iterator deq_i = d_disequalities.find(of); - CTNodeListAlloc* deq; - if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false, - ContextMemoryAllocator<TNode>(getContext()->getCMM())); - d_disequalities.insertDataFromContextMemory(of, deq); - } else { - deq = (*deq_i).second; - } + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl; - deq->push_back(eq); -} + // 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; + continue; + } + if (r1[0] != r2[0]) { + // If arrays are known to be disequal, or cannot become equal, we can continue + if (d_equalityEngine.areDisequal(r1[0], r2[0]) || + (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; + continue; + } + } -/** - * Iterates through the indices of a and stores of b and checks if any new - * Row lemmas need to be instantiated. - */ -bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); + TNode x = r1[1]; + TNode y = r2[1]; - if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 || - d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) { - return true; - } + EqualityStatus eqStatus = getEqualityStatus(x, y); - return false; -} + if (eqStatus != EQUALITY_UNKNOWN) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl; + continue; + } -bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { - NodeManager* nm = NodeManager::currentNM(); - Node aj = nm->mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); + if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; + continue; + } - if(find(i) == find(j) || find(aj) == find(bj)) { - Trace("arrays") << "isRedundantInContext valid " - << a << " " << b << " " << i << " " << j << endl; - checkRowForIndex(j, b); // why am i doing this? - checkRowForIndex(i, a); - return true; - } - Trace("arrays") << "isRedundantInContext " << a << endl - << "isRedundantInContext " << b << endl - << "isRedundantInContext " << i << endl - << "isRedundantInContext " << j << endl; - Node ieqj = i.eqNode(j); - Node literal1 = Rewriter::rewrite(ieqj); - bool hasValue1, satValue1; - Node ff = nm->mkConst<bool>(false); - Node tt = nm->mkConst<bool>(true); - if (literal1 == ff) { - hasValue1 = true; - satValue1 = false; - } else if (literal1 == tt) { - hasValue1 = true; - satValue1 = true; - } else { - hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); - } - if (hasValue1) { - if (satValue1) { - Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl; - return true; - } - Node ajeqbj = aj.eqNode(bj); - Node literal2 = Rewriter::rewrite(ajeqbj); - bool hasValue2, satValue2; - if (literal2 == ff) { - hasValue2 = true; - satValue2 = false; - } else if (literal2 == tt) { - hasValue2 = true; - satValue2 = true; - } else { - hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); - } - if (hasValue2) { - if (satValue2) { - Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl; - return true; + // Get representative trigger terms + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y); + + EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); + switch (eqStatusDomain) { + case EQUALITY_FALSE_AND_PROPAGATED: + case EQUALITY_FALSE: + continue; + break; + case EQUALITY_TRUE_AND_PROPAGATED: + case EQUALITY_TRUE: + // Should have been propagated to us + Assert(false); + continue; + break; + case EQUALITY_FALSE_IN_MODEL: + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl; + continue; + break; + default: + break; + } + + // Otherwise, add this pair + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl; + addCarePair(x_shared, y_shared); } - // conflict - Assert(!satValue1 && !satValue2); - Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL); - NodeBuilder<2> nb(kind::AND); - //literal1 = areDisequal(literal1[0], literal1[1]); - //literal2 = areDisequal(literal2[0], literal2[1]); - Assert(!literal1.isNull() && !literal2.isNull()); - nb << literal1.notNode() << literal2.notNode(); - literal1 = nb; - d_conflict = Node::null(); - d_out->conflict(literal1); - Trace("arrays") << "TheoryArrays::isRedundantInContext() " - << "conflict via lemma: " << literal1 << endl; - return true; } } - if(alreadyAddedRow(a, b, i, j)) { - Trace("arrays") << "isRedundantInContext already added " - << a << " " << b << " " << i << " " << j << endl; - return true; - } - return false; } -TNode TheoryArrays::areDisequal(TNode a, TNode b) { - Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n"; - - a = find(a); - b = find(b); - - CNodeTNodesMap::const_iterator it = d_disequalities.find(a); - if(it!= d_disequalities.end()) { - CTNodeListAlloc::const_iterator i = (*it).second->begin(); - for( ; i!= (*it).second->end(); i++) { - Trace("arrays-prop") << " " << *i << "\n"; - TNode s = (*i)[0]; - TNode t = (*i)[1]; - - Assert(find(s) == a || find(t) == a); - TNode sp, tp; - if(find(t) == a) { - sp = find(t); - tp = find(s); - } - else { - sp = find(s); - tp = find(t); - } - if(tp == b) { - return *i; - } +///////////////////////////////////////////////////////////////////////////// +// MODEL GENERATION +///////////////////////////////////////////////////////////////////////////// - } - } - Trace("arrays-prop") << " not disequal \n"; - return TNode::null(); -} -bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { - Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; +Node TheoryArrays::getValue(TNode n) +{ + // TODO: Implement this + NodeManager* nodeManager = NodeManager::currentNM(); - NodeManager* nm = NodeManager::currentNM(); - Node aj = nm->mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); + switch(n.getKind()) { - Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj); - Node eq_ij = nm->mkNode(kind::EQUAL, i, j); - - // first check if the current context implies NOT (i = j) - // in which case we can propagate a[j] = b[j] - // FIXME: does i = j need to be a SAT literal or can we propagate anyway? - - // if it does not have an atom we must add the lemma (do we?!) - if(d_atoms.count(eq_aj_bj) != 0 || - d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) { - Node diseq = areDisequal(i, j); - // check if the current context implies that (NOT i = j) - if(diseq != TNode::null()) { - // if it's unassigned - Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull(); - if(d_valuation.getSatValue(eq_aj_bj).isNull()) { - d_out->propagate(eq_aj_bj); - ++d_numProp; - // save explanation - d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq)); - return true; - } + case kind::VARIABLE: + Unhandled(kind::VARIABLE); - } - } + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - // now check if the current context implies NOT a[j] = b[j] - // in which case we propagate i = j + default: + Unhandled(n.getKind()); + } +} - // we can't propagate if it does not have an atom - if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) { - Node diseq = areDisequal(aj, bj); - Assert(TNode::null() == Node::null()); +///////////////////////////////////////////////////////////////////////////// +// NOTIFICATIONS +///////////////////////////////////////////////////////////////////////////// - if(diseq != TNode::null()) { - if(d_valuation.getSatValue(eq_ij) == Node::null()) { - d_out->propagate(eq_ij); - ++d_numProp; - // save explanation - d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq)); - return true; - } - } - } - Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; - return false; +void TheoryArrays::presolve() +{ + Trace("arrays")<<"Presolving \n"; } -Node TheoryArrays::explain(TNode n) { +///////////////////////////////////////////////////////////////////////////// +// MAIN SOLVER +///////////////////////////////////////////////////////////////////////////// - Trace("arrays")<<"Arrays::explain start for "<<n<<"\n"; - ++d_numExplain; - - Assert(n.getKind()==kind::EQUAL); - Node explanation = d_cc.explain(n[0], n[1]); +void TheoryArrays::check(Effort e) { + TimerStat::CodeTimer codeTimer(d_checkTimer); - NodeBuilder<> nb(kind::AND); + while (!done() && !d_conflict) + { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; + + // If the assertion doesn't have a literal, it's a shared equality + Assert(assertion.isPreregistered || + ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || + (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && + d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); + + // Do the work + switch (fact.getKind()) { + case kind::EQUAL: + d_equalityEngine.addEquality(fact[0], fact[1], fact); + break; + case kind::SELECT: + d_equalityEngine.addPredicate(fact, true, fact); + break; + case kind::NOT: + if (fact[0].getKind() == kind::SELECT) { + d_equalityEngine.addPredicate(fact[0], false, fact); + } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) { + // Assert the dis-equality + d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); + + // Apply ArrDiseq Rule if diseq is between arrays + if(fact[0][0].getType().isArray()) { + NodeManager* nm = NodeManager::currentNM(); + TypeNode indexType = fact[0][0].getType()[0]; + TNode k; + std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact); + if (it == d_diseqCache.end()) { + Node newk = nm->mkVar(indexType); + Dump.declareVar(newk.toExpr(), + "an extensional lemma index variable from the theory of arrays"); + d_diseqCache[fact] = newk; + k = newk; + } + else { + k = (*it).second; + } - if(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF) { - // if the explanation is only one literal - if(!isAxiom(explanation[0], explanation[1]) && - !isAxiom(explanation[1], explanation[0])) { - nb<<explanation; + Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); + Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); + if (!d_equalityEngine.hasTerm(ak)) { + preRegisterTerm(ak); + } + if (!d_equalityEngine.hasTerm(bk)) { + preRegisterTerm(bk); + } + d_equalityEngine.addDisequality(ak, bk, fact); + Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n"; + ++d_numExt; + } + } + break; + default: + Unreachable(); } } + + // If in conflict, output the conflict + if (d_conflict) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; + d_out->conflict(d_conflictNode); + } else { - Assert(explanation.getKind() == kind::AND); - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); i++) { - if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) { - nb<<*i; - } + // Otherwise we propagate + propagate(e); + + if(!d_eagerLemmas && fullEffort(e)) { + // generate the lemmas on the worklist + Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; + dischargeLemmas(); } } - Node reason = nb; - - return reason; - - /* - context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator - it = d_explanations.find(n); - Assert(it!= d_explanations.end()); - TNode diseq = (*it).second.second; - TNode s = diseq[0]; - TNode t = diseq[1]; - TNode eq = (*it).second.first; - TNode a = eq[0]; - TNode b = eq[1]; + Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl; +} - Assert ((find(a) == find(s) && find(b) == find(t)) || - (find(a) == find(t) && find(b) == find(s))); +Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions) +{ + Assert(conjunctions.size() > 0); - if(find(a) == find(t)) { - TNode temp = t; - t = s; - s = temp; - } + std::set<TNode> all; + std::set<TNode> explained; - // construct the explanation + unsigned i = 0; + TNode t; + for (; i < conjunctions.size(); ++i) { + t = conjunctions[i]; - NodeBuilder<> nb(kind::AND); - Node explanation1 = d_cc.explain(a, s); - Node explanation2 = d_cc.explain(b, t); + // Remove true node - represents axiomatically true assertion + if (t == d_true) continue; - if(explanation1.getKind() == kind::AND) { - for(TNode::iterator i= TNode(explanation1).begin(); - i!=TNode(explanation1).end(); ++i) { - nb << *i; + // Expand explanation resulting from propagating a ROW lemma + if (t.getKind() == kind::OR) { + if ((explained.find(t) == explained.end())) { + Assert(t[1].getKind() == kind::EQUAL); + d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions); + explained.insert(t); + } + continue; } - } else { - Assert(explanation1.getKind() == kind::EQUAL || - explanation1.getKind() == kind::IFF); - nb << explanation1; + all.insert(t); } - if(explanation2.getKind() == kind::AND) { - for(TNode::iterator i= TNode(explanation2).begin(); - i!=TNode(explanation2).end(); ++i) { - nb << *i; - } - } else { - Assert(explanation2.getKind() == kind::EQUAL || - explanation2.getKind() == kind::IFF); - nb << explanation2; + Assert(all.size() > 0); + if (all.size() == 1) { + // All the same, or just one + return *(all.begin()); + } + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; } - nb << diseq; - Node reason = nb; - d_out->explanation(reason); - Trace("arrays")<<"explanation "<< reason<<" done \n"; - */ + return conjunction; } -void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; - if(Trace.isOn("arrays-crl")) - d_infoMap.getInfo(a)->print(); - Trace("arrays-crl")<<" ------------ and "<<b<<"\n"; - if(Trace.isOn("arrays-crl")) - d_infoMap.getInfo(b)->print(); +void TheoryArrays::setNonLinear(TNode a) +{ + if (d_infoMap.isNonLinear(a)) return; + + Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; + d_infoMap.setNonLinear(a); + ++d_numNonLinear; List<TNode>* i_a = d_infoMap.getIndices(a); - const CTNodeList* st_b = d_infoMap.getStores(b); - const CTNodeList* inst_b = d_infoMap.getInStores(b); + const CTNodeList* st_a = d_infoMap.getStores(a); + const CTNodeList* inst_a = d_infoMap.getInStores(a); - List<TNode>::const_iterator it = i_a->begin(); - CTNodeList::const_iterator its; + CTNodeList::const_iterator it = st_a->begin(); - for( ; it != i_a->end(); it++ ) { - TNode i = *it; - its = st_b->begin(); - for ( ; its != st_b->end(); its++) { - TNode store = *its; + // Propagate non-linearity down chain of stores + for(; it!= st_a->end(); ++it) { + TNode store = *it; + Assert(store.getKind()==kind::STORE); + setNonLinear(store[0]); + } + + // Instantiate ROW lemmas that were ignored before + List<TNode>::const_iterator itl = i_a->begin(); + RowLemmaType lem; + for(; itl != i_a->end(); ++itl ) { + TNode i = *itl; + it = inst_a->begin(); + for ( ; it !=inst_a->end(); ++it) { + TNode store = *it; Assert(store.getKind() == kind::STORE); TNode j = store[1]; TNode c = store[0]; - - if( !isRedundantRowLemma(store, c, j, i)){ - //&&!propagateFromRow(store, c, j, i)) { - queueRowLemma(store, c, j, i); - } + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + queueRowLemma(lem); } - } - it = i_a->begin(); +} - for( ; it != i_a->end(); it++ ) { - TNode i = *it; - its = inst_b->begin(); - for ( ; its !=inst_b->end(); its++) { - TNode store = *its; - Assert(store.getKind() == kind::STORE); - TNode j = store[1]; - TNode c = store[0]; - if ( isNonLinear(c) - &&!isRedundantRowLemma(store, c, j, i)){ - //&&!propagateFromRow(store, c, j, i)) { - queueRowLemma(store, c, j, i); +void TheoryArrays::mergeArrays(TNode a, TNode b) +{ + // Note: a is the new representative + Assert(a.getType().isArray() && b.getType().isArray()); + + if (d_mergeInProgress) { + // Nested call to mergeArrays, just push on the queue and return + d_mergeQueue.push(a.eqNode(b)); + return; + } + + d_mergeInProgress = true; + + Node n; + while (true) { + if (d_useNonLinearOpt) { + bool aNL = d_infoMap.isNonLinear(a); + bool bNL = d_infoMap.isNonLinear(b); + if (aNL) { + if (bNL) { + // already both marked as non-linear - no need to do anything + } + else { + // Set b to be non-linear + setNonLinear(b); + } } + else { + if (bNL) { + // Set a to be non-linear + setNonLinear(a); + } + else { + // Check for new non-linear arrays + const CTNodeList* astores = d_infoMap.getStores(a); + const CTNodeList* bstores = d_infoMap.getStores(a); + Assert(astores->size() <= 1 && bstores->size() <= 1); + if (astores->size() > 0 && bstores->size() > 0) { + setNonLinear(a); + setNonLinear(b); + } + } + } + } + + d_mayEqualEqualityEngine.addEquality(a, b, d_true); + checkRowLemmas(a,b); + checkRowLemmas(b,a); + + // merge info adds the list of the 2nd argument to the first + d_infoMap.mergeInfo(a, b); + + // If no more to do, break + if (d_conflict || d_mergeQueue.empty()) { + break; } - } - Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; + // Otherwise, prepare for next iteration + n = d_mergeQueue.front(); + a = n[0]; + b = n[1]; + d_mergeQueue.pop(); + } + d_mergeInProgress = false; } -/** - * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the - * same and a and b are also not identical. - * - */ - -inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); - // construct lemma - NodeManager* nm = NodeManager::currentNM(); - Node aj = nm->mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); - Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); - Node eq2 = nm->mkNode(kind::EQUAL, i, j); - Node lem = nm->mkNode(kind::OR, eq2, eq1); +void TheoryArrays::checkStore(TNode a) { + Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; + if(Trace.isOn("arrays-cri")) { + d_infoMap.getInfo(a)->print(); + } + Assert(a.getType().isArray()); + Assert(a.getKind()==kind::STORE); + TNode b = a[0]; + TNode i = a[1]; + TNode brep = d_equalityEngine.getRepresentative(b); - Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; - d_RowAlreadyAdded.insert(make_quad(a,b,i,j)); - d_out->lemma(lem); - ++d_numRow; + if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) { + List<TNode>* js = d_infoMap.getIndices(brep); + List<TNode>::const_iterator it = js->begin(); + RowLemmaType lem; + for(; it!= js->end(); ++it) { + TNode j = *it; + if (i == j) continue; + lem = make_quad(a,b,i,j); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; + queueRowLemma(lem); + } + } } -/** - * Because a is now being read at position i check if new lemmas can be - * instantiated for all store terms equal to a and all store terms of the form - * store(a _ _ ) - */ -void TheoryArrays::checkRowForIndex(TNode i, TNode a) { +void TheoryArrays::checkRowForIndex(TNode i, TNode a) +{ Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n"; Trace("arrays-cri")<<" index "<<i<<"\n"; @@ -1057,107 +954,207 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { d_infoMap.getInfo(a)->print(); } Assert(a.getType().isArray()); + Assert(d_equalityEngine.getRepresentative(a) == a); const CTNodeList* stores = d_infoMap.getStores(a); const CTNodeList* instores = d_infoMap.getInStores(a); CTNodeList::const_iterator it = stores->begin(); + RowLemmaType lem; - for(; it!= stores->end(); it++) { + for(; it!= stores->end(); ++it) { TNode store = *it; Assert(store.getKind()==kind::STORE); TNode j = store[1]; - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundantRowLemma(store, store[0], j, i)) { - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; - queueRowLemma(store, store[0], j, i); - } + if (i == j) continue; + lem = make_quad(store, store[0], j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; + queueRowLemma(lem); } - it = instores->begin(); - for(; it!= instores->end(); it++) { - TNode instore = *it; - Assert(instore.getKind()==kind::STORE); - TNode j = instore[1]; - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundantRowLemma(instore, instore[0], j, i)) { - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; - queueRowLemma(instore, instore[0], j, i); + if (!d_useNonLinearOpt || d_infoMap.isNonLinear(a)) { + it = instores->begin(); + for(; it!= instores->end(); ++it) { + TNode instore = *it; + Assert(instore.getKind()==kind::STORE); + TNode j = instore[1]; + if (i == j) continue; + lem = make_quad(instore, instore[0], j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; + queueRowLemma(lem); } } - } -void TheoryArrays::checkStore(TNode a) { - Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; - - if(Trace.isOn("arrays-cri")) { +// a just became equal to b +// look for new ROW lemmas +void TheoryArrays::checkRowLemmas(TNode a, TNode b) +{ + Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; + if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(a)->print(); - } - Assert(a.getType().isArray()); - Assert(a.getKind()==kind::STORE); - TNode b = a[0]; - TNode i = a[1]; + Trace("arrays-crl")<<" ------------ and "<<b<<"\n"; + if(Trace.isOn("arrays-crl")) + d_infoMap.getInfo(b)->print(); - List<TNode>* js = d_infoMap.getIndices(b); - List<TNode>::const_iterator it = js->begin(); + List<TNode>* i_a = d_infoMap.getIndices(a); + const CTNodeList* st_b = d_infoMap.getStores(b); + const CTNodeList* inst_b = d_infoMap.getInStores(b); + + List<TNode>::const_iterator it = i_a->begin(); + CTNodeList::const_iterator its; - for(; it!= js->end(); it++) { - TNode j = *it; + RowLemmaType lem; - if(!isRedundantRowLemma(a, b, i, j)) { - //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; - queueRowLemma(a,b,i,j); + for( ; it != i_a->end(); ++it ) { + TNode i = *it; + its = st_b->begin(); + for ( ; its != st_b->end(); ++its) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + queueRowLemma(lem); } } + if (!d_useNonLinearOpt || d_infoMap.isNonLinear(b)) { + for(it = i_a->begin() ; it != i_a->end(); ++it ) { + TNode i = *it; + its = inst_b->begin(); + for ( ; its !=inst_b->end(); ++its) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + queueRowLemma(lem); + } + } + } + Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } -inline void TheoryArrays::queueExtLemma(TNode a, TNode b) { + +void TheoryArrays::queueRowLemma(RowLemmaType lem) +{ + if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) { + return; + } + TNode a = lem.first; + TNode b = lem.second; + TNode i = lem.third; + TNode j = lem.fourth; Assert(a.getType().isArray() && b.getType().isArray()); + if (d_equalityEngine.areEqual(a,b) || + d_equalityEngine.areEqual(i,j)) { + return; + } - d_extQueue.insert(make_pair(a,b)); -} + NodeManager* nm = NodeManager::currentNM(); -void TheoryArrays::queueRowLemma(TNode a, TNode b, TNode i, TNode j) { - Assert(a.getType().isArray() && b.getType().isArray()); -//if(!isRedundantInContext(a,b,i,j)) { - d_RowQueue.insert(make_quad(a, b, i, j)); -} + Node aj = nm->mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + if (!d_equalityEngine.hasTerm(aj)) { + preRegisterTerm(aj); + } + if (!d_equalityEngine.hasTerm(bj)) { + preRegisterTerm(bj); + } + + if (d_equalityEngine.areEqual(aj,bj)) { + return; + } + + if (d_useArrTable) { + Node tableEntry = nm->mkNode(kind::ARR_TABLE_FUN, a, b, i, j); + if (d_equalityEngine.getSize(tableEntry) != 1) { + return; + } + } -/** -* Adds a new Ext lemma of the form -* a = b OR a[k]!=b[k], for a new variable k -*/ + //Propagation + if (d_propagateLemmas) { + if (d_equalityEngine.areDisequal(i,j)) { + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n"; + Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j)); + d_permRef.push_back(reason); + d_equalityEngine.addEquality(aj, bj, reason); + ++d_numProp; + return; + } + if (d_equalityEngine.areDisequal(aj,bj)) { + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; + Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); + d_permRef.push_back(reason); + d_equalityEngine.addEquality(i, j, reason); + ++d_numProp; + return; + } + } -inline void TheoryArrays::addExtLemma(TNode a, TNode b) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); + // TODO: maybe add triggers here - Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n"; - Trace("arrays-cle")<<" and "<<b<<" \n"; + if (d_eagerLemmas) { + Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); + Node eq2 = nm->mkNode(kind::EQUAL, i, j); + Node lemma = nm->mkNode(kind::OR, eq2, eq1); + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n"; + d_RowAlreadyAdded.insert(lem); + d_out->lemma(lemma); + ++d_numRow; + } + else { + d_RowQueue.push(lem); + } +} - if( d_extAlreadyAdded.count(make_pair(a, b)) == 0 - && d_extAlreadyAdded.count(make_pair(b, a)) == 0) { +void TheoryArrays::dischargeLemmas() +{ + size_t sz = d_RowQueue.size(); + for (unsigned count = 0; count < sz; ++count) { + RowLemmaType l = d_RowQueue.front(); + d_RowQueue.pop(); + if (d_RowAlreadyAdded.count(l) != 0) { + continue; + } - NodeManager* nm = NodeManager::currentNM(); - TypeNode ixType = a.getType()[0]; - Node k = nm->mkVar(ixType); - Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays"); - Node eq = nm->mkNode(kind::EQUAL, a, b); - Node ak = nm->mkNode(kind::SELECT, a, k); - Node bk = nm->mkNode(kind::SELECT, b, k); - Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk)); - Node lem = nm->mkNode(kind::OR, eq, neq); + TNode a = l.first; + TNode b = l.second; + TNode i = l.third; + TNode j = l.fourth; + Assert(a.getType().isArray() && b.getType().isArray()); + + NodeManager* nm = NodeManager::currentNM(); + Node aj = nm->mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + + // Check for redundant lemma + // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context) + if (d_equalityEngine.areEqual(i,j) || + d_equalityEngine.areEqual(a,b) || + d_equalityEngine.areEqual(aj,bj)) { + d_RowQueue.push(l); + continue; + } - Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n"; - d_extAlreadyAdded.insert(make_pair(a,b)); - d_out->lemma(lem); - ++d_numExt; - return; - } + // construct lemma + Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); + Node eq2 = nm->mkNode(kind::EQUAL, i, j); + Node lem = nm->mkNode(kind::OR, eq2, eq1); - Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; + d_RowAlreadyAdded.insert(l); + d_out->lemma(lem); + ++d_numRow; + } } + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |