From 5f875d967103452b6585d701b13a6ed5a2bf2a51 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 2 Oct 2014 16:28:00 -0700 Subject: [PATCH] Added internal support for constant arrays. --- src/theory/arrays/array_info.cpp | 24 ++++++ src/theory/arrays/array_info.h | 6 +- src/theory/arrays/options | 6 ++ src/theory/arrays/theory_arrays.cpp | 116 ++++++++++++++++++++++++---- src/theory/arrays/theory_arrays.h | 4 + src/theory/theory_engine.cpp | 22 +++--- 6 files changed, 152 insertions(+), 26 deletions(-) diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index dc907ba0b..9b2d3647e 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -181,6 +181,20 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) { } +void ArrayInfo::setConstArr(const TNode a, const TNode constArr) { + 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->constArr = constArr; + info_map[a] = temp_info; + } else { + (*it).second->constArr = constArr; + } + +} + /** * Returns the information associated with TNode a */ @@ -224,6 +238,16 @@ const TNode ArrayInfo::getModelRep(const TNode a) const return TNode(); } +const TNode ArrayInfo::getConstArr(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->constArr; + } + 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 09230bba7..f3c6385e5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -64,11 +64,12 @@ public: context::CDO isNonLinear; context::CDO rIntro1Applied; context::CDO modelRep; + context::CDO constArr; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) { + Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -210,6 +211,7 @@ public: void setRIntro1Applied(const TNode a); void setModelRep(const TNode a, const TNode rep); + void setConstArr(const TNode a, const TNode constArr); /** * Returns the information associated with TNode a */ @@ -222,6 +224,8 @@ public: const TNode getModelRep(const TNode a) const; + const TNode getConstArr(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 7d5e67350..8ed80c1f1 100644 --- a/src/theory/arrays/options +++ b/src/theory/arrays/options @@ -23,4 +23,10 @@ option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write option arraysConfig --arrays-config int :default 0 :read-write set different array option configurations - for developers only +option arraysReduceSharing --arrays-reduce-sharing bool :default false :read-write + use model information to reduce size of care graph for arrays + +option arraysPropagate --arrays-prop int :default 2 :read-write + propagation effort for arrays: 0 is none, 1 is some, 2 is full + endmodule diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index bfbf046c3..cf0eeb14b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -40,11 +40,11 @@ namespace arrays { const bool d_ccStore = false; const bool d_useArrTable = 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; // These are now options + //const bool d_propagateLemmas = true; //bool d_useNonLinearOpt = true; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; @@ -87,6 +87,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_permRef(c), d_modelConstraints(c), d_lemmasSaved(c), + d_defValues(c), d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); @@ -449,6 +450,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) if (node.getType().isArray()) { d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); + d_mayEqualEqualityEngine.addTerm(node); } else { d_equalityEngine.addTerm(node); @@ -468,7 +470,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node) break; } case kind::STORE: { - // Invariant: array terms should be preregistered before being added to the equality engine if (d_equalityEngine.hasTerm(node)) { break; } @@ -499,13 +500,28 @@ void TheoryArrays::preRegisterTermInternal(TNode node) break; } case kind::STORE_ALL: { - throw LogicException("Array theory solver does not yet support assertions using constant array value"); + if (d_equalityEngine.hasTerm(node)) { + break; + } + ArrayStoreAll storeAll = node.getConst(); + Node defaultValue = Node::fromExpr(storeAll.getExpr()); + if (!defaultValue.isConst()) { + throw LogicException("Array theory solver does not yet support non-constant default values for arrays"); + } + d_infoMap.setConstArr(node, node); + d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); + d_mayEqualEqualityEngine.addTerm(node); + Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); + d_defValues[node] = defaultValue; + break; } default: // Variables etc if (node.getType().isArray()) { d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); Assert(d_equalityEngine.getSize(node) == 1); + // The may equal needs the node + d_mayEqualEqualityEngine.addTerm(node); } else { d_equalityEngine.addTerm(node); @@ -674,7 +690,9 @@ void TheoryArrays::computeCareGraph() case EQUALITY_FALSE: case EQUALITY_FALSE_IN_MODEL: // Don't need to include this pair - continue; + if (options::arraysReduceSharing()) { + continue; + } default: break; } @@ -809,10 +827,22 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) } Node rep; - map defValues; - map::iterator it; + DefValMap::iterator it; TypeSet defaultValuesSet; + // Compute all default values already in use + if (fullModel) { + for (size_t i=0; ibegin()); } Trace("arrays-models") << "New default value = " << rep << endl; - defValues[mayRep] = rep; + d_defValues[mayRep] = rep; } else { rep = (*it).second; @@ -2036,7 +2065,42 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) } } + TNode constArrA = d_infoMap.getConstArr(a); + TNode constArrB = d_infoMap.getConstArr(b); + if (constArrA.isNull()) { + if (!constArrB.isNull()) { + d_infoMap.setConstArr(a,constArrB); + } + } + else if (!constArrB.isNull()) { + if (constArrA != constArrB) { + conflict(constArrA,constArrB); + } + } + + // If a and b have different default values associated with their mayequal equivalence classes, + // things get complicated - disallow this for now. -Clark + TNode mayRepA = d_mayEqualEqualityEngine.getRepresentative(a); + TNode mayRepB = d_mayEqualEqualityEngine.getRepresentative(b); + + DefValMap::iterator it = d_defValues.find(mayRepA); + DefValMap::iterator it2 = d_defValues.find(mayRepB); + TNode defValue; + + if (it != d_defValues.end()) { + defValue = (*it).second; + if (it2 != d_defValues.end() && (defValue != (*it2).second)) { + throw LogicException("Array theory solver does not yet support write-chains connecting two different constant arrays"); + } + } + else if (it2 != d_defValues.end()) { + defValue = (*it2).second; + } d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true); + if (!defValue.isNull()) { + mayRepA = d_mayEqualEqualityEngine.getRepresentative(a); + d_defValues[mayRepA] = defValue; + } checkRowLemmas(a,b); checkRowLemmas(b,a); @@ -2168,6 +2232,17 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) Assert(a.getType().isArray()); Assert(d_equalityEngine.getRepresentative(a) == a); + TNode constArr = d_infoMap.getConstArr(a); + if (!constArr.isNull()) { + ArrayStoreAll storeAll = constArr.getConst(); + Node defValue = Node::fromExpr(storeAll.getExpr()); + Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i); + if (!d_equalityEngine.hasTerm(selConst)) { + preRegisterTermInternal(selConst); + } + d_equalityEngine.assertEquality(selConst.eqNode(defValue), true, d_true); + } + const CTNodeList* stores = d_infoMap.getStores(a); const CTNodeList* instores = d_infoMap.getInStores(a); size_t it = 0; @@ -2211,15 +2286,25 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) d_infoMap.getInfo(b)->print(); const CTNodeList* i_a = d_infoMap.getIndices(a); + size_t it = 0; + TNode constArr = d_infoMap.getConstArr(b); + if (!constArr.isNull()) { + for( ; it < i_a->size(); ++it) { + TNode i = (*i_a)[it]; + Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i); + if (!d_equalityEngine.hasTerm(selConst)) { + preRegisterTermInternal(selConst); + } + } + } + const CTNodeList* st_b = d_infoMap.getStores(b); const CTNodeList* inst_b = d_infoMap.getInStores(b); - - size_t it = 0; size_t its; RowLemmaType lem; - for( ; it < i_a->size(); ++it) { + for(it = 0 ; it < i_a->size(); ++it) { TNode i = (*i_a)[it]; its = 0; for ( ; its < st_b->size(); ++its) { @@ -2277,8 +2362,9 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) bool bothExist = ajExists && bjExists; // If propagating, check propagations - if (d_propagateLemmas) { - if (d_equalityEngine.areDisequal(i,j,true)) { + int prop = options::arraysPropagate(); + if (prop > 0) { + if (d_equalityEngine.areDisequal(i,j,true) && (bothExist || prop > 1)) { Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("< d_lemmasSaved; std::vector d_lemmas; + // Default values for each mayEqual equivalence class + typedef context::CDHashMap DefValMap; + DefValMap d_defValues; + Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); Node mkAnd(std::vector& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b943a7ee5..ed56890ae 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -501,16 +501,18 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); - if (true) { - if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { - Node e = ensureLiteral(equality); - d_propEngine->requirePhase(e, true); - } - else if (es == EQUALITY_FALSE_IN_MODEL) { - Node e = ensureLiteral(equality); - d_propEngine->requirePhase(e, false); - } - } + // This code is supposed to force preference to follow what the theory models already have + // but it doesn't seem to make a big difference - need to explore more -Clark + // if (true) { + // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { + // Node e = ensureLiteral(equality); + // d_propEngine->requirePhase(e, true); + // } + // else if (es == EQUALITY_FALSE_IN_MODEL) { + // Node e = ensureLiteral(equality); + // d_propEngine->requirePhase(e, false); + // } + // } } } -- 2.30.2