diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
commit | b390cfa8f095048472cb3dd0b9ccc22fbd51f411 (patch) | |
tree | de6d485b9b164806f408d714cd50e7da7db5da6c /src/theory/arrays/theory_arrays.cpp | |
parent | 28096861af9b01e4bad6059346446d97b9708cb7 (diff) |
Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 44e362f90..15636fc72 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -86,12 +86,19 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); + // The preprocessing congruence kinds + 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) { d_equalityEngine.addFunctionKind(kind::STORE); } - d_equalityEngine.addFunctionKind(kind::EQUAL); if (d_useArrTable) { d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN); } @@ -118,12 +125,13 @@ TheoryArrays::~TheoryArrays() { Node TheoryArrays::ppRewrite(TNode term) { if (!d_preprocess) return term; + d_ppEqualityEngine.addTerm(term); switch (term.getKind()) { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j if (term[0].getKind() == kind::STORE && - (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) || + (d_ppEqualityEngine.areDisequal(term[0][1], term[1], false) || (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; } @@ -134,7 +142,7 @@ Node TheoryArrays::ppRewrite(TNode term) { // IF i != j and j comes before i in the ordering if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && - (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) || + (d_ppEqualityEngine.areDisequal(term[1], term[0][1], false) || (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2]; Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2]; @@ -198,7 +206,7 @@ Node TheoryArrays::ppRewrite(TNode term) { NodeBuilder<> hyp(kind::AND); for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; - if (d_ppEqualityEngine.areDisequal(index_i, index_j) || + if (d_ppEqualityEngine.areDisequal(index_i, index_j, false) || (index_i.isConst() && index_j.isConst() && index_i != index_j)) { continue; } @@ -374,6 +382,7 @@ void TheoryArrays::preRegisterTerm(TNode node) switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality + // NOTE: note that if the equality is true or false already, it might not be added d_equalityEngine.addTriggerEquality(node); break; case kind::SELECT: { @@ -385,6 +394,9 @@ void TheoryArrays::preRegisterTerm(TNode node) // Reads TNode store = d_equalityEngine.getRepresentative(node[0]); + // The may equal needs the store + d_mayEqualEqualityEngine.addTerm(store); + // 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(); @@ -460,7 +472,8 @@ void TheoryArrays::preRegisterTerm(TNode node) break; } // Invariant: preregistered terms are exactly the terms in the equality engine - Assert(d_equalityEngine.hasTerm(node)); + // Disabled, see comment above for kind::EQUAL + // Assert(d_equalityEngine.hasTerm(node) || !d_equalityEngine.consistent()); } @@ -525,7 +538,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { // The terms are implied to be equal return EQUALITY_TRUE; } - if (d_equalityEngine.areDisequal(a, b)) { + if (d_equalityEngine.areDisequal(a, b, false)) { // The terms are implied to be dis-equal return EQUALITY_FALSE; } @@ -576,10 +589,10 @@ void TheoryArrays::computeCareGraph() if (r1[0] != r2[0]) { // If arrays are known to be disequal, or cannot become equal, we can continue - Assert(d_equalityEngine.hasTerm(r1[0]) && d_equalityEngine.hasTerm(r2[0])); + Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0])); if (r1[0].getType() != r2[0].getType() || (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) || - d_equalityEngine.areDisequal(r1[0], r2[0])) { + d_equalityEngine.areDisequal(r1[0], r2[0], false)) { Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; continue; } @@ -704,7 +717,7 @@ void TheoryArrays::check(Effort e) { case kind::NOT: if (fact[0].getKind() == kind::SELECT) { d_equalityEngine.assertPredicate(fact[0], false, fact); - } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) { + } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) { // Assert the dis-equality d_equalityEngine.assertEquality(fact[0], false, fact); @@ -1141,7 +1154,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // If propagating, check propagations if (d_propagateLemmas) { - if (d_equalityEngine.areDisequal(i,j)) { + if (d_equalityEngine.areDisequal(i,j,true)) { Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n"; Node aj_eq_bj = aj.eqNode(bj); Node i_eq_j = i.eqNode(j); @@ -1157,7 +1170,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) ++d_numProp; return; } - if (bothExist && d_equalityEngine.areDisequal(aj,bj)) { + if (bothExist && d_equalityEngine.areDisequal(aj,bj,true)) { Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; Node aj_eq_bj = aj.eqNode(bj); Node i_eq_j = i.eqNode(j); @@ -1178,7 +1191,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } // Prefer equality between indexes so as not to introduce new read terms - if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j)) { + if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { Node split = d_valuation.ensureLiteral(i.eqNode(j)); d_out->propagateAsDecision(split); } |