From: Clark Barrett Date: Fri, 20 Apr 2012 23:30:08 +0000 (+0000) Subject: Updates to array theory - much more lazy about introduction of reads X-Git-Tag: cvc5-1.0.0~8222 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04e81f6d12cad8f2519aa6c94adee52aadd71ec3;p=cvc5.git Updates to array theory - much more lazy about introduction of reads Also disabled eager lemmas - slows down QF_AX but gets new examples in QF_AUFBV --- diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index cd6c38a7f..643fbaedf 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -67,22 +67,24 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ void ArrayInfo::addIndex(const Node a, const TNode i) { Assert(a.getType().isArray()); Assert(!i.getType().isArray()); // temporary for flat arrays + Trace("arrays-ind")<<"Arrays::addIndex "<* temp_indices; + CTNodeList* temp_indices; Info* temp_info; CNodeInfoMap::iterator it = info_map.find(a); if(it == info_map.end()) { - temp_indices = new List(bck); - temp_indices->append(i); + temp_indices = new(true) CTNodeList(ct); + temp_indices->push_back(i); temp_info = new Info(ct, bck); temp_info->indices = temp_indices; - info_map[a] = temp_info; } else { temp_indices = (*it).second->indices; - temp_indices->append(i); + if (! inList(temp_indices, i)) { + temp_indices->push_back(i); + } } if(Trace.isOn("arrays-ind")) { printList((*(info_map.find(a))).second->indices); @@ -153,6 +155,19 @@ void ArrayInfo::setNonLinear(const TNode a) { } +void ArrayInfo::setRIntro1Applied(const TNode a) { + 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->rIntro1Applied = true; + info_map[a] = temp_info; + } else { + (*it).second->rIntro1Applied = true; + } + +} /** * Returns the information associated with TNode a @@ -171,16 +186,25 @@ const bool ArrayInfo::isNonLinear(const TNode a) const CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) - return (*it).second->isNonLinear; + return (*it).second->isNonLinear; + return false; +} + +const bool ArrayInfo::rIntro1Applied(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) + return (*it).second->rIntro1Applied; return false; } -List* ArrayInfo::getIndices(const TNode a) const{ +const CTNodeList* ArrayInfo::getIndices(const TNode a) const{ CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) { return (*it).second->indices; } - return emptyListI; + return emptyList; } const CTNodeList* ArrayInfo::getStores(const TNode a) const{ @@ -221,16 +245,16 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ if(Trace.isOn("arrays-mergei")) (*itb).second->print(); - List* lista_i = (*ita).second->indices; + CTNodeList* lista_i = (*ita).second->indices; CTNodeList* lista_st = (*ita).second->stores; CTNodeList* lista_inst = (*ita).second->in_stores; - List* listb_i = (*itb).second->indices; + CTNodeList* listb_i = (*itb).second->indices; CTNodeList* listb_st = (*itb).second->stores; CTNodeList* listb_inst = (*itb).second->in_stores; - lista_i->concat(listb_i); + mergeLists(lista_i, listb_i); mergeLists(lista_st, listb_st); mergeLists(lista_inst, listb_inst); @@ -269,13 +293,13 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ Trace("arrays-mergei")<<" adding second element's info \n"; (*itb).second->print(); - List* listb_i = (*itb).second->indices; + CTNodeList* listb_i = (*itb).second->indices; CTNodeList* listb_st = (*itb).second->stores; CTNodeList* listb_inst = (*itb).second->in_stores; Info* temp_info = new Info(ct, bck); - (temp_info->indices)->concat(listb_i); + mergeLists(temp_info->indices, listb_i); mergeLists(temp_info->stores, listb_st); mergeLists(temp_info->in_stores, listb_inst); info_map[a] = temp_info; diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 3eae369ca..b34232b8f 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -83,12 +83,13 @@ bool inList(const CTNodeList* l, const TNode el); class Info { public: context::CDO isNonLinear; - List* indices; + context::CDO rIntro1Applied; + CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false) { - indices = new List(bck); + Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false) { + indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -97,6 +98,7 @@ public: ~Info() { //FIXME! //indices->deleteSelf(); + indices->deleteSelf(); stores->deleteSelf(); in_stores->deleteSelf(); } @@ -105,7 +107,7 @@ public: * prints the information */ void print() const { - Assert(indices != NULL && stores!= NULL); // && equals != NULL); + Assert(indices != NULL && stores!= NULL && in_stores != NULL); Trace("arrays-info")<<" indices "; printList(indices); Trace("arrays-info")<<" stores "; @@ -134,8 +136,6 @@ private: CNodeInfoMap info_map; CTNodeList* emptyList; - List* emptyListI; - /* == STATISTICS == */ @@ -191,7 +191,6 @@ public: d_maxList("theory::arrays::maxList",0), d_tableSize("theory::arrays::infoTableSize", info_map) { emptyList = new(true) CTNodeList(ct); - emptyListI = new List(bck); emptyInfo = new Info(ct, bck); StatisticsRegistry::registerStat(&d_mergeInfoTimer); StatisticsRegistry::registerStat(&d_avgIndexListLength); @@ -231,6 +230,7 @@ public: void addInStore(const TNode a, const TNode st); void setNonLinear(const TNode a); + void setRIntro1Applied(const TNode a); /** * Returns the information associated with TNode a @@ -240,7 +240,9 @@ public: const bool isNonLinear(const TNode a) const; - List* getIndices(const TNode a) const; + const bool rIntro1Applied(const TNode a) const; + + const CTNodeList* getIndices(const TNode a) const; const CTNodeList* getStores(const TNode a) const; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4a61ca64d..c02f90bf0 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -35,15 +35,19 @@ namespace arrays { // These are the options that produce the best empirical results on QF_AX benchmarks. +// eagerLemmas = true +// eagerIndexSplitting = false + // 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_eagerLemmas = false; +const bool d_propagateLemmas = true; const bool d_preprocess = true; const bool d_solveWrite = true; +const bool d_solveWrite2 = false; const bool d_useNonLinearOpt = true; - +const bool d_eagerIndexSplitting = true; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARRAY, c, u, out, valuation), @@ -246,6 +250,7 @@ Node TheoryArrays::ppRewrite(TNode term) { 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; @@ -414,9 +419,30 @@ void TheoryArrays::preRegisterTerm(TNode node) d_equalityEngine.addTriggerEquality(node[0], node[1], node); d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); break; - case kind::SELECT: + case kind::SELECT: { // Reads d_equalityEngine.addTerm(node); + TNode store = d_equalityEngine.getRepresentative(node[0]); + + // Apply RIntro1 rule to any stores equal to store if not done already + const CTNodeList* stores = d_infoMap.getStores(store); + CTNodeList::const_iterator it = stores->begin(); + if (it != stores->end()) { + NodeManager* nm = NodeManager::currentNM(); + TNode s = *it; + if (!d_infoMap.rIntro1Applied(s)) { + d_infoMap.setRIntro1Applied(s); + Assert(s.getKind()==kind::STORE); + Node ni = nm->mkNode(kind::SELECT, s, s[1]); + if (ni != node) { + Assert(!d_equalityEngine.hasTerm(ni)); + preRegisterTerm(ni); + } + d_equalityEngine.addEquality(ni, s[2], d_true); + Assert(++it == stores->end()); + } + } + // Maybe it's a predicate // TODO: remove this or keep it if we allow Boolean elements in arrays. if (node.getType().isBoolean()) { @@ -426,27 +452,27 @@ void TheoryArrays::preRegisterTerm(TNode node) } d_infoMap.addIndex(node[0], node[1]); - checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0])); + checkRowForIndex(node[1], store); d_reads.push_back(node); break; - + } case kind::STORE: { d_equalityEngine.addTriggerTerm(node); TNode a = node[0]; - TNode i = node[1]; - TNode v = node[2]; + // TNode i = node[1]; + // TNode v = node[2]; - d_mayEqualEqualityEngine.addEquality(node, node[0], d_true); + d_mayEqualEqualityEngine.addEquality(node, a, d_true); - NodeManager* nm = NodeManager::currentNM(); - Node ni = nm->mkNode(kind::SELECT, node, i); - if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTerm(ni); - } + // NodeManager* nm = NodeManager::currentNM(); + // Node ni = nm->mkNode(kind::SELECT, node, i); + // if (!d_equalityEngine.hasTerm(ni)) { + // preRegisterTerm(ni); + // } - // Apply RIntro1 Rule - d_equalityEngine.addEquality(ni, v, d_true); + // // Apply RIntro1 Rule + // d_equalityEngine.addEquality(ni, v, d_true); d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); @@ -574,13 +600,14 @@ void TheoryArrays::computeCareGraph() Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl; // If the terms are already known to be equal, we are also in good shape - if (d_equalityEngine.areEqual(r1, r2)) { + if (d_equalityEngine.hasTerm(r1) && d_equalityEngine.hasTerm(r2) && 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 + Assert(d_equalityEngine.hasTerm(r1[0]) && d_equalityEngine.hasTerm(r2[0])); if (r1[0].getType() != r2[0].getType() || (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) || d_equalityEngine.areDisequal(r1[0], r2[0])) { @@ -592,6 +619,11 @@ void TheoryArrays::computeCareGraph() TNode x = r1[1]; TNode y = r2[1]; + if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; + continue; + } + EqualityStatus eqStatus = getEqualityStatus(x, y); if (eqStatus != EQUALITY_UNKNOWN) { @@ -599,11 +631,6 @@ void TheoryArrays::computeCareGraph() continue; } - if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { - Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; - continue; - } - // Get representative trigger terms TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x); TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y); @@ -819,7 +846,7 @@ void TheoryArrays::setNonLinear(TNode a) d_infoMap.setNonLinear(a); ++d_numNonLinear; - List* i_a = d_infoMap.getIndices(a); + const CTNodeList* i_a = d_infoMap.getIndices(a); const CTNodeList* st_a = d_infoMap.getStores(a); const CTNodeList* inst_a = d_infoMap.getInStores(a); @@ -833,10 +860,10 @@ void TheoryArrays::setNonLinear(TNode a) } // Instantiate ROW lemmas that were ignored before - List::const_iterator itl = i_a->begin(); + CTNodeList::const_iterator it2 = i_a->begin(); RowLemmaType lem; - for(; itl != i_a->end(); ++itl ) { - TNode i = *itl; + for(; it2 != i_a->end(); ++it2 ) { + TNode i = *it2; it = inst_a->begin(); for ( ; it !=inst_a->end(); ++it) { TNode store = *it; @@ -851,6 +878,79 @@ void TheoryArrays::setNonLinear(TNode a) } +/***** + * When two array equivalence classes are merged, we may need to apply RIntro1 to a store in one of the EC's + * Here, we check the stores in a to see if any need RIntro1 applied + * We apply RIntro1 whenever: + * (a) a store becomes equal to another store + * (b) a store becomes equal to any term t such that read(t,i) exists + * (c) a store becomes equal to the root array of the store (i.e. store(store(...store(a,i,v)...)) = a) + */ +void TheoryArrays::checkRIntro1(TNode a, TNode b) +{ + const CTNodeList* astores = d_infoMap.getStores(a); + // Apply RIntro1 if applicable + CTNodeList::const_iterator it = astores->begin(); + + if (it == astores->end()) { + // No stores in this equivalence class - return + return; + } + + ++it; + if (it != astores->end()) { + // More than one store: should have already been applied + Assert(d_infoMap.rIntro1Applied(*it)); + Assert(d_infoMap.rIntro1Applied(*(--it))); + return; + } + + // Exactly one store - see if we need to apply RIntro1 + --it; + TNode s = *it; + Assert(s.getKind() == kind::STORE); + if (d_infoMap.rIntro1Applied(s)) { + // RIntro1 already applied to s + return; + } + + // Should be no reads from this EC + Assert(d_infoMap.getIndices(a)->begin() == d_infoMap.getIndices(a)->end()); + + bool apply = false; + if (d_infoMap.getStores(b)->size() > 0) { + // Case (a): two stores become equal + apply = true; + } + else { + const CTNodeList* i_b = d_infoMap.getIndices(b); + if (i_b->begin() != i_b->end()) { + // Case (b): there are reads from b + apply = true; + } + else { + // Get root array of s + TNode e1 = s[0]; + while (e1.getKind() == kind::STORE) { + e1 = e1[0]; + } + Assert(d_equalityEngine.hasTerm(e1)); + if (d_equalityEngine.areEqual(e1, b)) { + apply = true; + } + } + } + + if (apply) { + NodeManager* nm = NodeManager::currentNM(); + d_infoMap.setRIntro1Applied(s); + Node ni = nm->mkNode(kind::SELECT, s, s[1]); + Assert(!d_equalityEngine.hasTerm(ni)); + preRegisterTerm(ni); + d_equalityEngine.addEquality(ni, s[2], d_true); + } +} + void TheoryArrays::mergeArrays(TNode a, TNode b) { @@ -867,6 +967,11 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) Node n; while (true) { + Trace("arrays-merge") << spaces(getContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; + + checkRIntro1(a, b); + checkRIntro1(b, a); + if (d_useNonLinearOpt) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); @@ -887,7 +992,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) else { // Check for new non-linear arrays const CTNodeList* astores = d_infoMap.getStores(a); - const CTNodeList* bstores = d_infoMap.getStores(a); + const CTNodeList* bstores = d_infoMap.getStores(b); Assert(astores->size() <= 1 && bstores->size() <= 1); if (astores->size() > 0 && bstores->size() > 0) { setNonLinear(a); @@ -934,8 +1039,8 @@ void TheoryArrays::checkStore(TNode a) { TNode brep = d_equalityEngine.getRepresentative(b); if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) { - List* js = d_infoMap.getIndices(brep); - List::const_iterator it = js->begin(); + const CTNodeList* js = d_infoMap.getIndices(brep); + CTNodeList::const_iterator it = js->begin(); RowLemmaType lem; for(; it!= js->end(); ++it) { @@ -1001,11 +1106,11 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(b)->print(); - List* i_a = d_infoMap.getIndices(a); + const CTNodeList* i_a = d_infoMap.getIndices(a); const CTNodeList* st_b = d_infoMap.getStores(b); const CTNodeList* inst_b = d_infoMap.getInStores(b); - List::const_iterator it = i_a->begin(); + CTNodeList::const_iterator it = i_a->begin(); CTNodeList::const_iterator its; RowLemmaType lem; @@ -1059,38 +1164,31 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } NodeManager* nm = NodeManager::currentNM(); - 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; - } - } + // Try to avoid introducing new read terms: track whether these already exist + bool ajExists = d_equalityEngine.hasTerm(aj); + bool bjExists = d_equalityEngine.hasTerm(bj); + bool bothExist = ajExists && bjExists; - //Propagation + // If propagating, check propagations if (d_propagateLemmas) { if (d_equalityEngine.areDisequal(i,j)) { Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j)); d_permRef.push_back(reason); + if (!ajExists) { + preRegisterTerm(aj); + } + if (!bjExists) { + preRegisterTerm(bj); + } d_equalityEngine.addEquality(aj, bj, reason); ++d_numProp; return; } - if (d_equalityEngine.areDisequal(aj,bj)) { + if (bothExist && d_equalityEngine.areDisequal(aj,bj)) { Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); d_permRef.push_back(reason); @@ -1100,9 +1198,23 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } } + // If equivalent lemma already exists, don't enqueue this one + if (d_useArrTable) { + Node tableEntry = NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN, a, b, i, j); + if (d_equalityEngine.getSize(tableEntry) != 1) { + return; + } + } + + // Prefer equality between indexes so as not to introduce new read terms + if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j)) { + Node split = d_valuation.ensureLiteral(i.eqNode(j)); + d_out->propagateAsDecision(split); + } + // TODO: maybe add triggers here - if (d_eagerLemmas) { + if (d_eagerLemmas || bothExist) { Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); Node eq2 = nm->mkNode(kind::EQUAL, i, j); Node lemma = nm->mkNode(kind::OR, eq2, eq1); @@ -1141,7 +1253,7 @@ void TheoryArrays::dischargeLemmas() // 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_equalityEngine.hasTerm(aj) && d_equalityEngine.hasTerm(bj) && d_equalityEngine.areEqual(aj,bj))) { d_RowQueue.push(l); continue; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 12dbd771d..99b976b9d 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -304,6 +304,7 @@ class TheoryArrays : public Theory { Node mkAnd(std::vector& conjunctions); void setNonLinear(TNode a); + void checkRIntro1(TNode a, TNode b); void mergeArrays(TNode a, TNode b); void checkStore(TNode a); void checkRowForIndex(TNode i, TNode a);