*/
void removeITEs();
+ Node intToBV(TNode n, std::hash_map<Node, Node, NodeHashFunction>& cache);
+ Node intToBVMakeBinary(TNode n, std::hash_map<Node, Node, NodeHashFunction>& cache);
+
/**
* Helper function to fix up assertion list to restore invariants needed after ite removal
*/
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]
return result.top();
}
+//TODO: clean this up
+struct intToBV_stack_element {
+ TNode node;
+ bool children_added;
+ intToBV_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};/* struct intToBV_stack_element */
+
+typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+
+Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
+ // Do a topological sort of the subexpressions and substitute them
+ vector<intToBV_stack_element> 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<intToBV_stack_element> 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<Node> 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>(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<Rational>();
+ 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());
}
}
+ if (options::solveIntAsBV() > 0) {
+ Chat() << "converting ints to bit-vectors..." << endl;
+ hash_map<Node, Node, NodeHashFunction> 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.");
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
d_modelConstraints(c),
d_lemmasSaved(c),
d_defValues(c),
+ d_readTableContext(new context::Context()),
+ d_arrayMerges(c),
d_inCheckModel(false)
{
StatisticsRegistry::registerStat(&d_numRow);
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) {
}
TheoryArrays::~TheoryArrays() {
- CNodeNListMap::iterator it = d_constReads.begin();
- for( ; it != d_constReads.end(); ++it ) {
- (*it).second->deleteSelf();
+ vector<CTNodeList*>::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);
}
}
+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<TNode>& 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<TNode>& 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<TNode, TNodeHashFunction> marked;
+ vector<TNode> index_trail;
+ vector<TNode>::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:
// 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();
// 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()) {
Assert(d_mayEqualEqualityEngine.consistent());
}
- if (!options::arraysLazyRIntro1()) {
+ if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) {
TNode i = node[1];
TNode v = node[2];
NodeManager* nm = NodeManager::currentNM();
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;
}
}
}
}
- 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()) {
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);
d_out->lemma(lemma);
++d_numExt;
}
- else {
- d_modelConstraints.push_back(fact);
- }
}
break;
default:
}
}
- 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: "<<d_RowQueue.size()<<"\n";
- while (d_RowQueue.size() > 0 && !d_conflict) {
- if (dischargeLemmas()) {
- break;
- }
- }
- }
-
- Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
-}
-
-
-void TheoryArrays::convertNodeToAssumptions(TNode node, vector<TNode>& 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<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2;
- Node modelVal, modelVal2, d;
- vector<TNode> 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<Node>::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<TNode> 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<TNode> validAssumptions;
- context::CDList<Assertion>::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<TNode> all;
- std::set<TNode> 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<TNode>::const_iterator it = all.begin();
- std::set<TNode>::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<TNode>::const_iterator it = all.begin();
- std::set<TNode>::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<TNode>::const_iterator it = all.begin();
- std::set<TNode>::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<Assertion>::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<TNode, TNode> 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<TNode> 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<TNode>& 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: "<<d_RowQueue.size()<<"\n";
+ while (d_RowQueue.size() > 0 && !d_conflict) {
+ if (dischargeLemmas()) {
+ break;
}
- return true;
}
}
- Unreachable();
- return false;
+
+ Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
}
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";
}
-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<TNode>& 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)
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) {
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<TNode> 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;
void TheoryArrays::checkStore(TNode a) {
- if (options::arraysModelBased()) return;
+ if (options::arraysWeakEquivalence()) return;
Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
if(Trace.isOn("arrays-cri")) {
void TheoryArrays::checkRowForIndex(TNode i, TNode a)
{
- if (options::arraysModelBased()) return;
+ if (options::arraysWeakEquivalence()) return;
Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
Trace("arrays-cri")<<" index "<<i<<"\n";
// look for new ROW lemmas
void TheoryArrays::checkRowLemmas(TNode a, TNode b)
{
- if (options::arraysModelBased()) return;
+ if (options::arraysWeakEquivalence()) return;
Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
if(Trace.isOn("arrays-crl"))
d_infoMap.getInfo(a)->print();
projects / cvc5.git / commitdiff