diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
commit | 1433806056059339dd16ae8e431feaae23553150 (patch) | |
tree | cf678baa687b1a19e479c28a1c01470bb2f120c7 /src/theory/arrays | |
parent | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff) |
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 50 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 |
2 files changed, 28 insertions, 28 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a62ebed06..80bcb47dd 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -49,8 +49,8 @@ const bool d_solveWrite2 = false; const bool d_useNonLinearOpt = true; const bool d_eagerIndexSplitting = true; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : - Theory(THEORY_ARRAY, c, u, out, valuation), +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo), d_numRow("theory::arrays::number of Row lemmas", 0), d_numExt("theory::arrays::number of Ext lemmas", 0), d_numProp("theory::arrays::number of propagations", 0), @@ -316,11 +316,11 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs bool TheoryArrays::propagate(TNode literal) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl; return false; } @@ -332,7 +332,7 @@ bool TheoryArrays::propagate(TNode literal) // If asserted, we're done or in conflict if (isAsserted) { if (!satValue) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral; if (normalized != d_false) { @@ -349,7 +349,7 @@ bool TheoryArrays::propagate(TNode literal) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); return true; @@ -407,7 +407,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { */ void TheoryArrays::preRegisterTerm(TNode node) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; switch (node.getKind()) { case kind::EQUAL: @@ -495,17 +495,17 @@ void TheoryArrays::preRegisterTerm(TNode node) void TheoryArrays::propagate(Effort e) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl; if (!d_conflict) { for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; bool satValue; Node normalized = Rewriter::rewrite(literal); if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { d_out->propagate(literal); } else { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; Node negatedLiteral; std::vector<TNode> assumptions; if (normalized != d_false) { @@ -526,7 +526,7 @@ void TheoryArrays::propagate(Effort e) Node TheoryArrays::explain(TNode literal) { ++d_numExplain; - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; explain(literal, assumptions); return mkAnd(assumptions); @@ -539,7 +539,7 @@ Node TheoryArrays::explain(TNode literal) void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; + Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; d_equalityEngine.addTriggerTerm(t); if (t.getType().isArray()) { d_sharedArrays.insert(t,true); @@ -716,7 +716,7 @@ void TheoryArrays::check(Effort e) { Assertion assertion = get(); TNode fact = assertion.assertion; - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; // If the assertion doesn't have a literal, it's a shared equality Assert(assertion.isPreregistered || @@ -777,7 +777,7 @@ void TheoryArrays::check(Effort e) { // If in conflict, output the conflict if (d_conflict) { - Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; d_out->conflict(d_conflictNode); } else { @@ -791,7 +791,7 @@ void TheoryArrays::check(Effort e) { } } - Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl; + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; } @@ -844,7 +844,7 @@ void TheoryArrays::setNonLinear(TNode a) { if (d_infoMap.isNonLinear(a)) return; - Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; d_infoMap.setNonLinear(a); ++d_numNonLinear; @@ -873,7 +873,7 @@ void TheoryArrays::setNonLinear(TNode a) TNode j = store[1]; TNode c = store[0]; lem = make_quad(store, c, j, i); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; queueRowLemma(lem); } } @@ -969,7 +969,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) Node n; while (true) { - Trace("arrays-merge") << spaces(getContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; + Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; checkRIntro1(a, b); checkRIntro1(b, a); @@ -1049,7 +1049,7 @@ void TheoryArrays::checkStore(TNode a) { TNode j = *it; if (i == j) continue; lem = make_quad(a,b,i,j); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; queueRowLemma(lem); } } @@ -1078,7 +1078,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) TNode j = store[1]; if (i == j) continue; lem = make_quad(store, store[0], j, i); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(lem); } @@ -1090,7 +1090,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) TNode j = instore[1]; if (i == j) continue; lem = make_quad(instore, instore[0], j, i); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(lem); } } @@ -1126,7 +1126,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) TNode j = store[1]; TNode c = store[0]; lem = make_quad(store, c, j, i); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; queueRowLemma(lem); } } @@ -1141,7 +1141,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) TNode j = store[1]; TNode c = store[0]; lem = make_quad(store, c, j, i); - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; queueRowLemma(lem); } } @@ -1177,7 +1177,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // If propagating, check propagations if (d_propagateLemmas) { if (d_equalityEngine.areDisequal(i,j)) { - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n"; + Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n"; Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j)); d_permRef.push_back(reason); if (!ajExists) { @@ -1191,7 +1191,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) return; } if (bothExist && d_equalityEngine.areDisequal(aj,bj)) { - Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; + 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); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 99b976b9d..d18b3abde 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -122,7 +122,7 @@ class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryArrays(); std::string identify() const { return std::string("TheoryArrays"); } @@ -244,13 +244,13 @@ class TheoryArrays : public Theory { NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} bool notify(TNode propagation) { - Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; // Just forward to arrays return d_arrays.propagate(propagation); } void notify(TNode t1, TNode t2) { - Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + 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)) { |