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

1 files changed, 7 insertions, 10 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e183e0e1b..7f0088f5b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -53,8 +53,8 @@ namespace arith {
 const uint32_t RESET_START = 2;
 
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_ARITH, c, u, out, valuation),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_ARITH, c, u, out, valuation, logicInfo),
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
@@ -904,7 +904,7 @@ Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){
 }
 
 Node TheoryArith::dioCutting(){
-  context::Context::ScopedPush speculativePush(getContext());
+  context::Context::ScopedPush speculativePush(getSatContext());
   //DO NOT TOUCH THE OUTPUTSTREAM
 
   //TODO: Improve this
@@ -1043,7 +1043,7 @@ Node TheoryArith::assertionCases(TNode assertion){
   //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
   Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
 
-  Debug("arith::assertions")  << "arith assertion @" << getContext()->getLevel()
+  Debug("arith::assertions")  << "arith assertion @" << getSatContext()->getLevel()
                               <<"(" << assertion
                               << " \\-> "
     //<< determineLeftVariable(assertion, simpleKind)
@@ -1352,7 +1352,7 @@ void TheoryArith::debugPrintModel(){
 
 Node TheoryArith::explain(TNode n) {
 
-  Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+  Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
 
   Constraint c = d_constraintDatabase.lookup(n);
   if(c != NullConstraint){
@@ -1387,7 +1387,7 @@ void TheoryArith::propagate(Effort e) {
     }else if(!c->assertedToTheTheory()){
 
       Node literal = c->getLiteral();
-      Debug("arith::prop") << "propagating @" << getContext()->getLevel() << " " << literal << endl;
+      Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
 
       d_out->propagate(literal);
     }else{
@@ -1578,9 +1578,6 @@ Node TheoryArith::getValue(TNode n) {
   }
 }
 
-void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
-}
-
 void TheoryArith::notifyRestart(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
 
@@ -1674,7 +1671,7 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
   if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
      (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
 
-#warning "Policy point"
+    // TODO: "Policy point"
     //We are only going to recreate the functionality for now.
     //In the future this can be improved to generate a temporary constraint
     //if none exists.