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

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)) {