From: Clark Barrett Date: Sun, 27 Dec 2015 03:20:27 +0000 (-0800) Subject: Merged my changes from experimental branch (new array decision procedure, X-Git-Tag: cvc5-1.0.0~6126 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=815f2c96856e96e977b725254b65d68fc0323947;p=cvc5.git Merged my changes from experimental branch (new array decision procedure, translation to bit-vectors for QF_NIA). --- diff --git a/examples/README b/examples/README index d64ed3469..5f5bb0980 100644 --- a/examples/README +++ b/examples/README @@ -10,9 +10,9 @@ world" examples, and do not fully demonstrate the interfaces, but function as a starting point to using simple expressions and solving functionality through each library. -*** Targetted examples +*** Targeted examples -The "api" directory contains some more specifically-targetted +The "api" directory contains some more specifically-targeted examples (for bitvectors, for arithmetic, etc.). The "api/java" directory contains the same examples in Java. diff --git a/src/options/arrays_options b/src/options/arrays_options index 096d773ca..371554a2b 100644 --- a/src/options/arrays_options +++ b/src/options/arrays_options @@ -11,6 +11,9 @@ 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 arraysWeakEquivalence --arrays-weak-equiv bool :default false :read-write + use algorithm from Christ/Hoenicke (SMT 2014) + option arraysModelBased --arrays-model-based bool :default false :read-write turn on model-based array solver diff --git a/src/options/smt_options b/src/options/smt_options index f658d929a..d531eefbe 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -161,4 +161,6 @@ option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false Force no CPU limit when dumping models and proofs +option solveIntAsBV --solve-int-as-bv uint32_t :default 0 + endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 000cc167f..f2c45eab9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -404,6 +404,9 @@ private: */ void removeITEs(); + Node intToBV(TNode n, std::hash_map& cache); + Node intToBVMakeBinary(TNode n, std::hash_map& cache); + /** * Helper function to fix up assertion list to restore invariants needed after ite removal */ @@ -944,6 +947,12 @@ void SmtEngine::setDefaults() { if(options::forceLogic.wasSetByUser()) { d_logic = *(options::forceLogic()); } + else if (options::solveIntAsBV() > 0) { + d_logic = LogicInfo("QF_BV"); + // } else if (d_logic.getLogicString() == "QF_UFBV" && + // options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + // d_logic = LogicInfo("QF_BV"); + } // set strings-exp /* - disabled for 1.4 release [MGD 2014.06.25] @@ -1996,6 +2005,239 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map NodeMap; + +Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) { + // Do a topological sort of the subexpressions and substitute them + vector toVisit; + toVisit.push_back(n); + + while (!toVisit.empty()) + { + // The current node we are processing + intToBV_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; + + NodeMap::iterator find = cache.find(current); + if (find != cache.end()) { + toVisit.pop_back(); + continue; + } + if (stackHead.children_added) { + // Children have been processed, so rebuild this node + Node result; + NodeManager* nm = NodeManager::currentNM(); + if (current.getNumChildren() > 2 && (current.getKind() == kind::PLUS || current.getKind() == kind::MULT)) { + Assert(cache.find(current[0]) != cache.end()); + result = cache[current[0]]; + for (unsigned i = 1; i < current.getNumChildren(); ++ i) { + Assert(cache.find(current[i]) != cache.end()); + Node child = current[i]; + Node childRes = cache[current[i]]; + result = nm->mkNode(current.getKind(), result, childRes); + } + } + else { + NodeBuilder<> builder(current.getKind()); + for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + Assert(cache.find(current[i]) != cache.end()); + builder << cache[current[i]]; + } + result = builder; + } + cache[current] = result; + toVisit.pop_back(); + } else { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) { + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + NodeMap::iterator childFind = cache.find(childNode); + if (childFind == cache.end()) { + toVisit.push_back(childNode); + } + } + } else { + cache[current] = current; + toVisit.pop_back(); + } + } + } + return cache[n]; +} + +Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) { + int size = options::solveIntAsBV(); + AlwaysAssert(size > 0); + AlwaysAssert(!options::incrementalSolving()); + + vector toVisit; + NodeMap binaryCache; + Node n_binary = intToBVMakeBinary(n, binaryCache); + toVisit.push_back(TNode(n_binary)); + + while (!toVisit.empty()) + { + // The current node we are processing + intToBV_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; + + // If node is already in the cache we're done, pop from the stack + NodeMap::iterator find = cache.find(current); + if (find != cache.end()) { + toVisit.pop_back(); + continue; + } + + // Not yet substituted, so process + NodeManager* nm = NodeManager::currentNM(); + if (stackHead.children_added) { + // Children have been processed, so rebuild this node + vector children; + unsigned max = 0; + for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + Assert(cache.find(current[i]) != cache.end()); + TNode childRes = cache[current[i]]; + TypeNode type = childRes.getType(); + if (type.isBitVector()) { + unsigned bvsize = type.getBitVectorSize(); + if (bvsize > max) { + max = bvsize; + } + } + children.push_back(childRes); + } + + kind::Kind_t newKind = current.getKind(); + if (max > 0) { + switch (newKind) { + case kind::PLUS: + Assert(children.size() == 2); + newKind = kind::BITVECTOR_PLUS; + max = max + 1; + break; + case kind::MULT: + Assert(children.size() == 2); + newKind = kind::BITVECTOR_MULT; + max = max * 2; + break; + case kind::MINUS: + Assert(children.size() == 2); + newKind = kind::BITVECTOR_SUB; + max = max + 1; + break; + case kind::UMINUS: + Assert(children.size() == 1); + newKind = kind::BITVECTOR_NEG; + max = max + 1; + break; + case kind::LT: + newKind = kind::BITVECTOR_SLT; + break; + case kind::LEQ: + newKind = kind::BITVECTOR_SLE; + break; + case kind::GT: + newKind = kind::BITVECTOR_SGT; + break; + case kind::GEQ: + newKind = kind::BITVECTOR_SGE; + break; + case kind::EQUAL: + case kind::ITE: + break; + default: + if (Theory::theoryOf(current) == THEORY_BOOL) { + break; + } + throw TypeCheckingException(current.toExpr(), string("Cannot translate to BV: ") + current.toString()); + } + for (unsigned i = 0; i < children.size(); ++i) { + TypeNode type = children[i].getType(); + if (!type.isBitVector()) { + continue; + } + unsigned bvsize = type.getBitVectorSize(); + if (bvsize < max) { + // sign extend + Node signExtendOp = nm->mkConst(BitVectorSignExtend(max - bvsize)); + children[i] = nm->mkNode(signExtendOp, children[i]); + } + } + } + NodeBuilder<> builder(newKind); + for (unsigned i = 0; i < children.size(); ++i) { + builder << children[i]; + } + // Mark the substitution and continue + Node result = builder; + + result = Rewriter::rewrite(result); + cache[current] = result; + toVisit.pop_back(); + } else { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) { + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + NodeMap::iterator childFind = cache.find(childNode); + if (childFind == cache.end()) { + toVisit.push_back(childNode); + } + } + } else { + // It's a leaf: could be a variable or a numeral + Node result = current; + if (current.isVar()) { + if (current.getType() == nm->integerType()) { + result = nm->mkSkolem("__intToBV_var", nm->mkBitVectorType(size), + "Variable introduced in intToBV pass"); + } + else { + AlwaysAssert(current.getType() == nm->booleanType()); + } + } + else if (current.isConst()) { + switch (current.getKind()) { + case kind::CONST_RATIONAL: { + Rational constant = current.getConst(); + AlwaysAssert(constant.isIntegral()); + BitVector bv(size, constant.getNumerator()); + if (bv.getValue() != constant.getNumerator()) { + throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString()); + } + result = nm->mkConst(bv); + break; + } + case kind::CONST_BOOLEAN: + break; + default: + throw TypeCheckingException(current.toExpr(), string("Cannot translate const to BV: ") + current.toString()); + } + } + else { + throw TypeCheckingException(current.toExpr(), string("Cannot translate to BV: ") + current.toString()); + } + cache[current] = result; + toVisit.pop_back(); + } + } + } + return cache[n_binary]; +} + void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); spendResource(options::preprocessStep()); @@ -3218,8 +3460,17 @@ void SmtEnginePrivate::processAssertions() { } } + if (options::solveIntAsBV() > 0) { + Chat() << "converting ints to bit-vectors..." << endl; + hash_map cache; + for(unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, intToBV(d_assertions[i], cache)); + } + } + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && !d_smt.d_logic.isPure(THEORY_BV)) { + // && d_smt.d_logic.getLogicString() != "QF_UFBV") throw ModalException("Eager bit-blasting does not currently support theory combination. " "Note that in a QF_BV problem UF symbols can be introduced for division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); @@ -3697,6 +3948,11 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); r = check().asSatisfiabilityResult(); + + if (options::solveIntAsBV() > 0 &&r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + } + d_needPostsolve = true; // Dump the query if requested diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 9b2d3647e..cd0025fe2 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -192,7 +192,58 @@ void ArrayInfo::setConstArr(const TNode a, const TNode constArr) { } else { (*it).second->constArr = constArr; } - +} + +void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) { + 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->weakEquivPointer = pointer; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivPointer = pointer; + } +} + +void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) { + 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->weakEquivIndex = index; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivIndex = index; + } +} + +void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) { + 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->weakEquivSecondary = secondary; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivSecondary = secondary; + } +} + +void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) { + 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->weakEquivSecondaryReason = reason; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivSecondaryReason = reason; + } } /** @@ -248,6 +299,46 @@ const TNode ArrayInfo::getConstArr(const TNode a) const return TNode(); } +const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivPointer; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivIndex; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivSecondary; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivSecondaryReason; + } + 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 d9f77d50f..f14788ed5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -66,11 +66,23 @@ public: context::CDO rIntro1Applied; context::CDO modelRep; context::CDO constArr; + context::CDO weakEquivPointer; + context::CDO weakEquivIndex; + context::CDO weakEquivSecondary; + context::CDO weakEquivSecondaryReason; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) { + Info(context::Context* c, Backtracker* bck) + : isNonLinear(c, false), + rIntro1Applied(c, false), + modelRep(c,TNode()), + constArr(c,TNode()), + weakEquivPointer(c,TNode()), + weakEquivIndex(c,TNode()), + weakEquivSecondary(c,TNode()), + weakEquivSecondaryReason(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -213,6 +225,10 @@ public: void setModelRep(const TNode a, const TNode rep); void setConstArr(const TNode a, const TNode constArr); + void setWeakEquivPointer(const TNode a, const TNode pointer); + void setWeakEquivIndex(const TNode a, const TNode index); + void setWeakEquivSecondary(const TNode a, const TNode secondary); + void setWeakEquivSecondaryReason(const TNode a, const TNode reason); /** * Returns the information associated with TNode a */ @@ -226,6 +242,10 @@ public: const TNode getModelRep(const TNode a) const; const TNode getConstArr(const TNode a) const; + const TNode getWeakEquivPointer(const TNode a) const; + const TNode getWeakEquivIndex(const TNode a) const; + const TNode getWeakEquivSecondary(const TNode a) const; + const TNode getWeakEquivSecondaryReason(const TNode a) const; const CTNodeList* getIndices(const TNode a) const; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 89fdf7096..e4ad0e4a2 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -92,6 +92,8 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_modelConstraints(c), d_lemmasSaved(c), d_defValues(c), + d_readTableContext(new context::Context()), + d_arrayMerges(c), d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); @@ -112,10 +114,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_ppEqualityEngine.addFunctionKind(kind::SELECT); d_ppEqualityEngine.addFunctionKind(kind::STORE); - // The mayequal congruence kinds - d_mayEqualEqualityEngine.addFunctionKind(kind::SELECT); - d_mayEqualEqualityEngine.addFunctionKind(kind::STORE); - // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::SELECT); if (d_ccStore) { @@ -127,9 +125,14 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC } TheoryArrays::~TheoryArrays() { - CNodeNListMap::iterator it = d_constReads.begin(); - for( ; it != d_constReads.end(); ++it ) { - (*it).second->deleteSelf(); + vector::iterator it = d_readBucketAllocations.begin(), iend = d_readBucketAllocations.end(); + for (; it != iend; ++it) { + (*it)->deleteSelf(); + } + delete d_readTableContext; + CNodeNListMap::iterator it2 = d_constReads.begin(); + for( ; it2 != d_constReads.end(); ++it2 ) { + it2->second->deleteSelf(); } delete d_constReadsContext; StatisticsRegistry::unregisterStat(&d_numRow); @@ -393,6 +396,205 @@ void TheoryArrays::explain(TNode literal, std::vector& assumptions) { } } +TNode TheoryArrays::weakEquivGetRep(TNode node) { + TNode pointer; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return node; + } + node = pointer; + } +} + +TNode TheoryArrays::weakEquivGetRepIndex(TNode node, TNode index) { + Assert(!index.isNull()); + TNode pointer, index2; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return node; + } + index2 = d_infoMap.getWeakEquivIndex(node); + if (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) { + node = pointer; + } + else { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return node; + } + node = secondary; + } + } +} + +void TheoryArrays::visitAllLeaves(TNode reason, vector& conjunctions) { + switch (reason.getKind()) { + case kind::AND: + Assert(reason.getNumChildren() == 2); + visitAllLeaves(reason[0], conjunctions); + visitAllLeaves(reason[1], conjunctions); + break; + case kind::NOT: + conjunctions.push_back(reason); + break; + case kind::EQUAL: + d_equalityEngine.explainEquality(reason[0], reason[1], true, conjunctions); + break; + default: + Unreachable(); + } +} + +void TheoryArrays::weakEquivBuildCond(TNode node, TNode index, vector& conjunctions) { + Assert(!index.isNull()); + TNode pointer, index2; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return; + } + index2 = d_infoMap.getWeakEquivIndex(node); + if (index2.isNull()) { + // Null index means these two nodes became equal: explain the equality. + d_equalityEngine.explainEquality(node, pointer, true, conjunctions); + node = pointer; + } + else if (!d_equalityEngine.areEqual(index, index2)) { + // If indices are not equal in current context, need to add that to the lemma. + Node reason = index.eqNode(index2).notNode(); + d_permRef.push_back(reason); + conjunctions.push_back(reason); + node = pointer; + } + else { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return; + } + TNode reason = d_infoMap.getWeakEquivSecondaryReason(node); + Assert(!reason.isNull()); + visitAllLeaves(reason, conjunctions); + node = secondary; + } + } +} + +void TheoryArrays::weakEquivMakeRep(TNode node) { + TNode pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return; + } + weakEquivMakeRep(pointer); + d_infoMap.setWeakEquivPointer(pointer, node); + d_infoMap.setWeakEquivIndex(pointer, d_infoMap.getWeakEquivIndex(node)); + d_infoMap.setWeakEquivPointer(node, TNode()); + weakEquivMakeRepIndex(node); +} + +void TheoryArrays::weakEquivMakeRepIndex(TNode node) { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return; + } + TNode index = d_infoMap.getWeakEquivIndex(node); + Assert(!index.isNull()); + TNode index2 = d_infoMap.getWeakEquivIndex(secondary); + Node reason; + TNode next; + while (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) { + next = d_infoMap.getWeakEquivPointer(secondary); + d_infoMap.setWeakEquivSecondary(node, next); + reason = d_infoMap.getWeakEquivSecondaryReason(node); + if (index2.isNull()) { + reason = reason.andNode(secondary.eqNode(next)); + } + else { + reason = reason.andNode(index.eqNode(index2).notNode()); + } + d_permRef.push_back(reason); + d_infoMap.setWeakEquivSecondaryReason(node, reason); + if (next.isNull()) { + return; + } + secondary = next; + index2 = d_infoMap.getWeakEquivIndex(secondary); + } + weakEquivMakeRepIndex(secondary); + d_infoMap.setWeakEquivSecondary(secondary, node); + d_infoMap.setWeakEquivSecondaryReason(secondary, d_infoMap.getWeakEquivSecondaryReason(node)); + d_infoMap.setWeakEquivSecondary(node, TNode()); + d_infoMap.setWeakEquivSecondaryReason(node, TNode()); +} + +void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) { + std::hash_set marked; + vector index_trail; + vector::iterator it, iend; + Node equivalence_trail = reason; + Node current_reason; + TNode pointer, indexRep; + if (!index.isNull()) { + index_trail.push_back(index); + marked.insert(d_equalityEngine.getRepresentative(index)); + } + while (arrayFrom != arrayTo) { + index = d_infoMap.getWeakEquivIndex(arrayFrom); + pointer = d_infoMap.getWeakEquivPointer(arrayFrom); + if (!index.isNull()) { + indexRep = d_equalityEngine.getRepresentative(index); + if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) { + weakEquivMakeRepIndex(arrayFrom); + d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo); + current_reason = equivalence_trail; + for (it = index_trail.begin(), iend = index_trail.end(); it != iend; ++it) { + current_reason = current_reason.andNode(index.eqNode(*it).notNode()); + } + d_permRef.push_back(current_reason); + d_infoMap.setWeakEquivSecondaryReason(arrayFrom, current_reason); + } + marked.insert(indexRep); + } + else { + equivalence_trail = equivalence_trail.andNode(arrayFrom.eqNode(pointer)); + } + arrayFrom = pointer; + } +} + +void TheoryArrays::checkWeakEquiv(bool arraysMerged) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_mayEqualEqualityEngine); + for (; !eqcs_i.isFinished(); ++eqcs_i) { + Node eqc = (*eqcs_i); + if (!eqc.getType().isArray()) { + continue; + } + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_mayEqualEqualityEngine); + TNode rep = d_mayEqualEqualityEngine.getRepresentative(*eqc_i); + TNode weakEquivRep = weakEquivGetRep(rep); + for (; !eqc_i.isFinished(); ++eqc_i) { + TNode n = *eqc_i; + Assert(!arraysMerged || weakEquivGetRep(n) == weakEquivRep); + TNode pointer = d_infoMap.getWeakEquivPointer(n); + TNode index = d_infoMap.getWeakEquivIndex(n); + TNode secondary = d_infoMap.getWeakEquivSecondary(n); + Assert(pointer.isNull() == (weakEquivGetRep(n) == n)); + Assert(!pointer.isNull() || secondary.isNull()); + Assert(!index.isNull() || secondary.isNull()); + Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull() || !secondary.isNull()); + if (!pointer.isNull()) { + if (index.isNull()) { + Assert(d_equalityEngine.areEqual(n, pointer)); + } + else { + Assert((n.getKind() == kind::STORE && n[0] == pointer && n[1] == index) || + (pointer.getKind() == kind::STORE && pointer[0] == n && pointer[1] == index)); + } + } + } + } +} /** * Stores in d_infoMap the following information for each term a of type array: @@ -433,7 +635,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // The may equal needs the store d_mayEqualEqualityEngine.addTerm(store); - if (options::arraysLazyRIntro1()) { + if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { // 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(); @@ -478,7 +680,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // Record read in sharing data structure TNode index = d_equalityEngine.getRepresentative(node[1]); - if (index.isConst()) { + if (!options::arraysWeakEquivalence() && index.isConst()) { CTNodeList* temp; CNodeNListMap::iterator it = d_constReads.find(index); if (it == d_constReads.end()) { @@ -523,7 +725,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(d_mayEqualEqualityEngine.consistent()); } - if (!options::arraysLazyRIntro1()) { + if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) { TNode i = node[1]; TNode v = node[2]; NodeManager* nm = NodeManager::currentNM(); @@ -540,6 +742,17 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.addInStore(a, node); d_infoMap.setModelRep(node, node); + //Add-Store for Weak Equivalence + if (options::arraysWeakEquivalence()) { + Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a)); + Assert(weakEquivGetRep(node) == node); + d_infoMap.setWeakEquivPointer(node, node[0]); + d_infoMap.setWeakEquivIndex(node, node[1]); +#ifdef CVC4_ASSERTIONS + checkWeakEquiv(false); +#endif + } + checkStore(node); break; } @@ -724,12 +937,7 @@ void TheoryArrays::computeCareGraph() } } } - if (options::arraysModelBased()) { - checkModel(EFFORT_COMBINATION); - return; - } if (d_sharedTerms) { - // Synchronize d_constReadsContext with SAT context Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { @@ -1066,18 +1274,13 @@ 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); @@ -1097,9 +1300,6 @@ void TheoryArrays::check(Effort e) { d_out->lemma(lemma); ++d_numExt; } - else { - d_modelConstraints.push_back(fact); - } } break; default: @@ -1107,746 +1307,97 @@ void TheoryArrays::check(Effort e) { } } - if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) { - checkModel(e); - } - - if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { - // generate the lemmas on the worklist - Trace("arrays-lem")<<"Arrays::discharging lemmas: "< 0 && !d_conflict) { - if (dischargeLemmas()) { - break; - } - } - } - - Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; -} - - -void TheoryArrays::convertNodeToAssumptions(TNode node, vector& 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(Effort e) -{ - d_inCheckModel = true; - d_topLevel = getSatContext()->getLevel(); - Assert(d_skolemIndex == 0); - Assert(d_skolemAssertions.empty()); - Assert(d_lemmas.empty()); - - if (combination(e)) { - // Add constraints for shared terms - context::CDList::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; - Node modelVal, modelVal2, d; - vector assumptions; - for (; shared_it != shared_it_end; ++shared_it) { - if ((*shared_it).getType().isArray()) { - continue; - } - if ((*shared_it).isConst()) { - modelVal = (*shared_it); + if ((options::arraysEagerLemmas() || fullEffort(e)) && !d_conflict && options::arraysWeakEquivalence()) { + // Replay all array merges to update weak equivalence data structures + context::CDList::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end(); + TNode a, b, eq; + for (; it != iend; ++it) { + eq = *it; + a = eq[0]; + b = eq[1]; + weakEquivMakeRep(b); + if (weakEquivGetRep(a) == b) { + weakEquivAddSecondary(TNode(), a, b, eq); } else { - modelVal = d_valuation.getModelValue(*shared_it); - if (modelVal.isNull()) { - continue; - } - } - Assert(modelVal.isConst()); - for (shared_it2 = shared_it, ++shared_it2; shared_it2 != shared_it_end; ++shared_it2) { - if ((*shared_it2).getType() != (*shared_it).getType()) { - continue; - } - if ((*shared_it2).isConst()) { - modelVal2 = (*shared_it2); - } - else { - modelVal2 = d_valuation.getModelValue(*shared_it2); - if (modelVal2.isNull()) { - continue; - } - } - Assert(modelVal2.isConst()); - d = (*shared_it).eqNode(*shared_it2); - if (modelVal != modelVal2) { - d = d.notNode(); - } - if (!setModelVal(d, d_true, false, true, assumptions)) { - assumptions.push_back(d); - d_lemmas.push_back(mkAnd(assumptions, true)); - goto finish; - } - assumptions.clear(); - } - } - } - { - // TODO: record and replay decisions - int baseLevel = getSatContext()->getLevel(); - unsigned constraintIdx; - Node assertion, assertionToCheck; - vector assumptions; - int numrestarts = 0; - while (true || numrestarts < 1 || fullEffort(e) || combination(e)) { - ++numrestarts; - d_out->safePoint(1); - 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); + d_infoMap.setWeakEquivPointer(b, a); + d_infoMap.setWeakEquivIndex(b, TNode()); } #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]); - } + checkWeakEquiv(false); #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()) { - if (getSatContext()->getLevel() < baseLevel) { - if (all.size() == 1) { - d_lemmas.push_back(decision.negate()); - } - else { - NodeBuilder<> disjunction(kind::OR); - std::set::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << (*it).negate(); - ++it; - } - d_lemmas.push_back(disjunction); - } - goto finish; - } - all.erase(decision); - eq = false; - if (decision.getKind() == kind::NOT) { - decision = decision[0]; - eq = true; - } - while (getSatContext()->getLevel() != baseLevel && 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_lemmas.pop_back(); - d_conflictNode = explanation; - d_conflict = true; - break; - } - { - // generate lemma - if (all.size() == 0) { - d_lemmas.push_back(decision.negate()); - } - else { - NodeBuilder<> disjunction(kind::OR); - std::set::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << (*it).negate(); - ++it; - } - disjunction << decision.negate(); - d_lemmas.push_back(disjunction); - } - } - 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) { - if (!d_equalityEngine.hasTerm(d[1][0][0])) { - preRegisterTermInternal(d[1][0][0]); - } - if (!d_equalityEngine.hasTerm(d[1][0][2])) { - preRegisterTermInternal(d[1][0][2]); - } - } - if (!d_equalityEngine.hasTerm(d[1][0])) { - preRegisterTermInternal(d[1][0]); - } - if (!d_equalityEngine.hasTerm(d[1][2])) { - preRegisterTermInternal(d[1][2]); - } - if (!d_equalityEngine.hasTerm(d[1])) { - preRegisterTermInternal(d[1]); - } - } - 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; - } - // Reregister stores - if (assertionToCheck != assertion && - assertionToCheck.getKind() == kind::AND && - assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) { - TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0]; - preRegisterStores(s); - } - } - if (d_conflict) { - break; - } - // Assert(getModelVal(assertion) == d_true); - assumptions.clear(); - } -#ifdef CVC4_ASSERTIONS - if (!d_conflict && fullEffort(e)) { - 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 - } - finish: - while (!d_decisions.empty()) { - Assert(!d_conflict); - getSatContext()->pop(); - d_decisions.pop_back(); - } - d_skolemAssertions.clear(); - d_skolemIndex = 0; - while (!d_lemmas.empty()) { - Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; - d_out->splitLemma(d_lemmas.back()); #ifdef CVC4_ASSERTIONS - // Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end()); - // d_lemmasSaved.insert(d_lemmas.back()); + checkWeakEquiv(true); #endif - d_lemmas.pop_back(); - } - 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; + d_readTableContext->push(); + TNode mayRep, iRep; + CTNodeList* bucketList = NULL; + CTNodeList::const_iterator i = d_reads.begin(), readsEnd = d_reads.end(); + for (; i != readsEnd; ++i) { + const TNode& r = *i; + + Debug("arrays::weak") << "TheoryArrays::check(): checking read " << r << std::endl; + + // Find the bucket for this read. + mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]); + iRep = d_equalityEngine.getRepresentative(r[1]); + std::pair key(mayRep, iRep); + ReadBucketMap::iterator it = d_readBucketTable.find(key); + if (it == d_readBucketTable.end()) { + bucketList = new(true) CTNodeList(d_readTableContext); + d_readBucketAllocations.push_back(bucketList); + d_readBucketTable[key] = bucketList; } 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(); - } + bucketList = it->second; + } + CTNodeList::const_iterator it2 = bucketList->begin(), iend = bucketList->end(); + for (; it2 != iend; ++it2) { + const TNode& r2 = *it2; + Assert(r2.getKind() == kind::SELECT); + Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0])); + Assert(iRep == d_equalityEngine.getRepresentative(r2[1])); + if (d_equalityEngine.areEqual(r, r2)) { + continue; } - - 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(); + if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) { + // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2 + vector conjunctions; + Assert(d_equalityEngine.areEqual(r, Rewriter::rewrite(r))); + Assert(d_equalityEngine.areEqual(r2, Rewriter::rewrite(r2))); + Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate(); + d_permRef.push_back(lemma); + conjunctions.push_back(lemma); + if (r[1] != r2[1]) { + d_equalityEngine.explainEquality(r[1], r2[1], true, conjunctions); } - ++te; - if (te.isFinished()) { - Assert(false); - // TODO: conflict - break; - } - val = *te; + // TODO: get smaller lemmas by eliminating shared parts of path + weakEquivBuildCond(r[0], r[1], conjunctions); + weakEquivBuildCond(r2[0], r[1], conjunctions); + lemma = mkAnd(conjunctions, true); + d_out->lemma(lemma, false, false, true); + d_readTableContext->pop(); + return; } } - 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); + bucketList->push_back(r); } - return val == node; + d_readTableContext->pop(); } - 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; - } - } - Node d = node.eqNode(val); - Node r = Rewriter::rewrite(d); - if (r.isConst()) { - d_equalityEngine.assertEquality(d, r == d_true, d_true); - return ((r == d_true) == (!invert)); - } - getSatContext()->push(); - d_decisions.push_back(invert ? d.negate() : 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; - if (d_conflict) { - ++d_numSetModelValConflicts; - Debug("arrays-model-based") << "...which results in a conflict!" << endl; - d = d_decisions.back(); - unsigned sz = assumptions.size(); - convertNodeToAssumptions(d_conflictNode, assumptions, d); - unsigned sz2 = assumptions.size(); - Assert(sz2 > sz); - Node explanation; - if (sz2 == sz+1) { - explanation = assumptions[sz]; - } - else { - NodeBuilder<> conjunction(kind::AND); - for (unsigned i = sz; i < sz2; ++i) { - conjunction << assumptions[i]; - } - explanation = conjunction; - } - // assumptions.push_back(d); - // d_lemmas.push_back(mkAnd(assumptions, true, sz)); - // while (assumptions.size() > sz2) { - // assumptions.pop_back(); - // } - getSatContext()->pop(); - d_decisions.pop_back(); - d_permRef.push_back(explanation); - d = d.negate(); - Debug("arrays-model-based") << "Asserting learned literal2 " << 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; + if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) { + // generate the lemmas on the worklist + Trace("arrays-lem")<<"Arrays::discharging lemmas: "< 0 && !d_conflict) { + if (dischargeLemmas()) { + break; } - return true; } } - Unreachable(); - return false; + + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; } @@ -1917,7 +1468,7 @@ Node TheoryArrays::mkAnd(std::vector& conjunctions, bool invert, unsigned void TheoryArrays::setNonLinear(TNode a) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; if (d_infoMap.isNonLinear(a)) return; Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; @@ -2030,84 +1581,6 @@ 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) @@ -2127,12 +1600,12 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) while (true) { Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; - if (options::arraysLazyRIntro1()) { + if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { checkRIntro1(a, b); checkRIntro1(b, a); } - if (options::arraysOptimizeLinear() && !options::arraysModelBased()) { + if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); if (aNL) { @@ -2203,77 +1676,13 @@ 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); + if (options::arraysWeakEquivalence()) { + d_arrayMerges.push_back(a.eqNode(b)); + } + // If no more to do, break if (d_conflict || d_mergeQueue.empty()) { break; @@ -2290,7 +1699,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) void TheoryArrays::checkStore(TNode a) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; Trace("arrays-cri")<<"Arrays::checkStore "<print(); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6a023c282..28d994835 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -257,6 +257,15 @@ class TheoryArrays : public Theory { private: + TNode weakEquivGetRep(TNode node); + TNode weakEquivGetRepIndex(TNode node, TNode index); + void visitAllLeaves(TNode reason, std::vector& conjunctions); + void weakEquivBuildCond(TNode node, TNode index, std::vector& conjunctions); + void weakEquivMakeRep(TNode node); + void weakEquivMakeRepIndex(TNode node); + void weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason); + void checkWeakEquiv(bool arraysMerged); + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module class NotifyClass : public eq::EqualityEngineNotify { TheoryArrays& d_arrays; @@ -394,6 +403,12 @@ class TheoryArrays : public Theory { typedef context::CDHashMap DefValMap; DefValMap d_defValues; + typedef std::hash_map, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + ReadBucketMap d_readBucketTable; + context::Context* d_readTableContext; + context::CDList d_arrayMerges; + std::vector d_readBucketAllocations; + 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); @@ -411,17 +426,6 @@ class TheoryArrays : public Theory { 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(Effort e); - 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: diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 34a5a7dbd..60d0e1d48 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -116,11 +116,12 @@ public: * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point * @param preprocess - whether to apply more aggressive preprocessing + * @param sendAtoms - whether to ensure atoms are sent to the theory * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ virtual LemmaStatus lemma(TNode n, bool removable = false, - bool preprocess = false) + bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0; /** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0355256a3..2185f22ff 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -303,11 +303,11 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); + return d_engine->lemma(lemma, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index f493e253e..f0b616d62 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -87,7 +87,7 @@ public: push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index d1883da9f..399feb43e 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -58,7 +58,7 @@ class FakeOutputChannel : public OutputChannel { void propagateAsDecision(TNode n) throw(AssertionException) { Unimplemented(); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException) { Unimplemented(); } void requirePhase(TNode, bool) throw(AssertionException) { diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 08447b86d..c804ca307 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -70,7 +70,7 @@ public: // ignore } - LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false) + LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(AssertionException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0);