diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 137 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 73 |
2 files changed, 81 insertions, 129 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 80bcb47dd..1dd74f060 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,17 +23,13 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" -#include "theory/uf/equality_engine_impl.h" - using namespace std; - namespace CVC4 { namespace theory { namespace arrays { - // These are the options that produce the best empirical results on QF_AX benchmarks. // eagerLemmas = true // eagerIndexSplitting = false @@ -58,14 +54,12 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), d_checkTimer("theory::arrays::checkTime"), - d_ppNotify(), - d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"), + d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"), d_ppFacts(u), // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_mayEqualNotify(), - d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"), + d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"), d_notify(*this), d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"), d_conflict(c, false), @@ -91,14 +85,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - d_ppEqualityEngine.addTerm(d_true); - d_ppEqualityEngine.addTerm(d_false); - d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false); - - d_equalityEngine.addTerm(d_true); - d_equalityEngine.addTerm(d_false); - d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); - // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::SELECT); if (d_ccStore) { @@ -281,7 +267,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs case kind::EQUAL: { d_ppFacts.push_back(in); - d_ppEqualityEngine.addEquality(in[0], in[1], in); + d_ppEqualityEngine.assertEquality(in, true, in); if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; @@ -299,7 +285,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs in[0].getKind() == kind::IFF ); Node a = in[0][0]; Node b = in[0][1]; - d_ppEqualityEngine.addDisequality(a, b, in); + d_ppEqualityEngine.assertEquality(in[0], false, in); break; } default: @@ -335,10 +321,8 @@ bool TheoryArrays::propagate(TNode literal) Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); explain(literal, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; @@ -357,67 +341,40 @@ bool TheoryArrays::propagate(TNode literal) void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { - TNode lhs, rhs; - switch (literal.getKind()) { - case kind::EQUAL: - lhs = literal[0]; - rhs = literal[1]; - break; - case kind::SELECT: - lhs = literal; - rhs = d_true; - break; - case kind::NOT: - if (literal[0].getKind() == kind::EQUAL) { - // Disequalities - d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); - return; - } else { - // Predicates - lhs = literal[0]; - rhs = d_false; - break; - } - case kind::CONST_BOOLEAN: - // we get to explain true = false, since we set false to be the trigger of this - lhs = d_true; - rhs = d_false; - break; - default: - Unreachable(); + // Do the work + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); } - d_equalityEngine.explainEquality(lhs, rhs, assumptions); } - /** - * Stores in d_infoMap the following information for each term a of type array: - * - * - all i, such that there exists a term a[i] or a = store(b i v) - * (i.e. all indices it is being read atl; store(b i v) is implicitly read at - * position i due to the implicit axiom store(b i v)[i] = v ) - * - * - all the stores a is congruent to (this information is context dependent) - * - * - all store terms of the form store (a i v) (i.e. in which a appears - * directly; this is invariant because no new store terms are created) - * - * Note: completeness depends on having pre-register called on all the input - * terms before starting to instantiate lemmas. - */ +/** + * Stores in d_infoMap the following information for each term a of type array: + * + * - all i, such that there exists a term a[i] or a = store(b i v) + * (i.e. all indices it is being read atl; store(b i v) is implicitly read at + * position i due to the implicit axiom store(b i v)[i] = v ) + * + * - all the stores a is congruent to (this information is context dependent) + * + * - all store terms of the form store (a i v) (i.e. in which a appears + * directly; this is invariant because no new store terms are created) + * + * Note: completeness depends on having pre-register called on all the input + * terms before starting to instantiate lemmas. + */ void TheoryArrays::preRegisterTerm(TNode node) { Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; switch (node.getKind()) { case kind::EQUAL: - // Add the terms - // d_equalityEngine.addTerm(node[0]); - // d_equalityEngine.addTerm(node[1]); - d_equalityEngine.addTerm(node); // Add the trigger for equality - d_equalityEngine.addTriggerEquality(node[0], node[1], node); - d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); + d_equalityEngine.addTriggerEquality(node); break; case kind::SELECT: { // Reads @@ -438,7 +395,7 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(!d_equalityEngine.hasTerm(ni)); preRegisterTerm(ni); } - d_equalityEngine.addEquality(ni, s[2], d_true); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); Assert(++it == stores->end()); } } @@ -447,8 +404,7 @@ void TheoryArrays::preRegisterTerm(TNode node) // TODO: remove this or keep it if we allow Boolean elements in arrays. if (node.getType().isBoolean()) { // Get triggered for both equal and dis-equal - d_equalityEngine.addTriggerEquality(node, d_true, node); - d_equalityEngine.addTriggerEquality(node, d_false, node.notNode()); + d_equalityEngine.addTriggerPredicate(node); } d_infoMap.addIndex(node[0], node[1]); @@ -463,7 +419,7 @@ void TheoryArrays::preRegisterTerm(TNode node) // TNode i = node[1]; // TNode v = node[2]; - d_mayEqualEqualityEngine.addEquality(node, a, d_true); + d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true); // NodeManager* nm = NodeManager::currentNM(); // Node ni = nm->mkNode(kind::SELECT, node, i); @@ -508,10 +464,8 @@ void TheoryArrays::propagate(Effort e) Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; Node negatedLiteral; std::vector<TNode> assumptions; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); explain(literal, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; @@ -727,17 +681,17 @@ void TheoryArrays::check(Effort e) { // Do the work switch (fact.getKind()) { case kind::EQUAL: - d_equalityEngine.addEquality(fact[0], fact[1], fact); + d_equalityEngine.assertEquality(fact, true, fact); break; case kind::SELECT: - d_equalityEngine.addPredicate(fact, true, fact); + d_equalityEngine.assertPredicate(fact, true, fact); break; case kind::NOT: if (fact[0].getKind() == kind::SELECT) { - d_equalityEngine.addPredicate(fact[0], false, fact); + d_equalityEngine.assertPredicate(fact[0], false, fact); } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) { // Assert the dis-equality - d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); + d_equalityEngine.assertEquality(fact[0], false, fact); // Apply ArrDiseq Rule if diseq is between arrays if(fact[0][0].getType().isArray()) { @@ -764,7 +718,7 @@ void TheoryArrays::check(Effort e) { if (!d_equalityEngine.hasTerm(bk)) { preRegisterTerm(bk); } - d_equalityEngine.addDisequality(ak, bk, fact); + d_equalityEngine.assertEquality(ak.eqNode(bk), false, fact); Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n"; ++d_numExt; } @@ -807,14 +761,11 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions) for (; i < conjunctions.size(); ++i) { t = conjunctions[i]; - // Remove true node - represents axiomatically true assertion - if (t == d_true) continue; - // Expand explanation resulting from propagating a ROW lemma if (t.getKind() == kind::OR) { if ((explained.find(t) == explained.end())) { Assert(t[1].getKind() == kind::EQUAL); - d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions); + d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions); explained.insert(t); } continue; @@ -949,7 +900,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) Node ni = nm->mkNode(kind::SELECT, s, s[1]); Assert(!d_equalityEngine.hasTerm(ni)); preRegisterTerm(ni); - d_equalityEngine.addEquality(ni, s[2], d_true); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); } } @@ -1004,7 +955,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) } } - d_mayEqualEqualityEngine.addEquality(a, b, d_true); + d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true); checkRowLemmas(a,b); checkRowLemmas(b,a); @@ -1186,7 +1137,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) if (!bjExists) { preRegisterTerm(bj); } - d_equalityEngine.addEquality(aj, bj, reason); + d_equalityEngine.assertEquality(aj.eqNode(bj), true, reason); ++d_numProp; return; } @@ -1194,7 +1145,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); d_permRef.push_back(reason); - d_equalityEngine.addEquality(i, j, reason); + d_equalityEngine.assertEquality(i.eqNode(j), true, reason); ++d_numProp; return; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d18b3abde..88986ee7a 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -133,18 +133,8 @@ class TheoryArrays : public Theory { private: - // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used - class PPNotifyClass { - public: - bool notify(TNode propagation) { return true; } - void notify(TNode t1, TNode t2) { } - }; - - /** The notify class for d_ppEqualityEngine */ - PPNotifyClass d_ppNotify; - /** Equaltity engine */ - uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine; + eq::EqualityEngine d_ppEqualityEngine; // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine context::CDList<Node> d_ppFacts; @@ -187,17 +177,8 @@ class TheoryArrays : public Theory { private: - class MayEqualNotifyClass { - public: - bool notify(TNode propagation) { return true; } - void notify(TNode t1, TNode t2) { } - }; - - /** The notify class for d_mayEqualEqualityEngine */ - MayEqualNotifyClass d_mayEqualNotify; - /** Equaltity engine for determining if two arrays might be equal */ - uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine; + eq::EqualityEngine d_mayEqualEqualityEngine; public: @@ -238,37 +219,57 @@ class TheoryArrays : public Theory { private: // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module - class NotifyClass { + class NotifyClass : public eq::EqualityEngineNotify { TheoryArrays& d_arrays; public: NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} - bool notify(TNode propagation) { - Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; // Just forward to arrays - return d_arrays.propagate(propagation); + if (value) { + return d_arrays.propagate(equality); + } else { + return d_arrays.propagate(equality.notNode()); + } + } + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Unreachable(); } - void notify(TNode t1, TNode t2) { - Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; - if (t1.getType().isArray()) { - d_arrays.mergeArrays(t1, t2); - if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { - return; + bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl; + if (value) { + if (t1.getType().isArray()) { + d_arrays.mergeArrays(t1, t2); + if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { + return true; + } } + // Propagate equality between shared terms + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + d_arrays.propagate(equality); } - // Propagate equality between shared terms - Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_arrays.propagate(equality); + // TODO: implement negation propagation + return true; } - }; + bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + if (Theory::theoryOf(t1) == THEORY_BOOL) { + return d_arrays.propagate(t1.iffNode(t2)); + } else { + return d_arrays.propagate(t1.eqNode(t2)); + } + } + }; /** The notify class for d_equalityEngine */ NotifyClass d_notify; /** Equaltity engine */ - uf::EqualityEngine<NotifyClass> d_equalityEngine; + eq::EqualityEngine d_equalityEngine; // Are we in conflict? context::CDO<bool> d_conflict; |