Removing dead code that came in on commit r1740.

4 files changed, 3 insertions, 324 deletions

diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp
index a09bed8e8..151421b31 100644
--- a/src/theory/arith/arith_prop_manager.cpp
+++ b/src/theory/arith/arith_prop_manager.cpp
@@ -90,14 +90,6 @@ Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational&
   return d_propagator.getBestImpliedUpperBound(bound);
 }
 
-bool ArithPropManager::hasStrongerLowerBound(TNode n) const{
-  bool haveAcompilerWarning;
-  return true;
-}
-bool ArithPropManager::hasStrongerUpperBound(TNode n) const{
-  return true;
-}
-
 Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const {
   Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
   Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
index 1fd23dd62..55d8ae635 100644
--- a/src/theory/arith/arith_prop_manager.h
+++ b/src/theory/arith/arith_prop_manager.h
@@ -105,10 +105,6 @@ public:
     return d_propagator.getWeakerImpliedUpperBound(n);
   }
 
-
-  //Node strictlyWeakerAssertedUpperBound(TNode n) const;
-  //Node strictlyWeakerAssertedLowerBound(TNode n) const;
-
   Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const;
 
   Node strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const;
@@ -116,9 +112,6 @@ public:
   Node getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const;
   Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const;
 
-  bool hasStrongerLowerBound(TNode current) const;
-  bool hasStrongerUpperBound(TNode current) const;
-
   bool containsLiteral(TNode n) const {
     return d_propagator.containsLiteral(n);
   }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index b804cb1aa..113e80c27 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -149,17 +149,6 @@ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){
     return Node::null();
   }
-  // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){
-  //   TNode prevConstraint =  d_partialModel.getLowerConstraint(x_i);
-  //   if(prevConstraint.getKind() == EQUAL){
-  //     return Node::null();
-  //   }else{
-  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl;
-  //     Assert(prevConstraint.getKind() == AND);
-  //     d_partialModel.setLowerConstraint(x_i,original);
-  //     return Node::null();
-  //   }
-  // }
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
@@ -197,17 +186,6 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
     return Node::null(); //sat
   }
 
-  // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){
-  //   TNode prevConstraint = d_partialModel.getUpperConstraint(x_i);
-  //   if(prevConstraint.getKind() == EQUAL){
-  //     return Node::null();
-  //   }else{
-  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint  << endl;
-  //     Assert(prevConstraint.getKind() == AND);
-  //     d_partialModel.setUpperConstraint(x_i,original);
-  //     return Node::null();
-  //   }
-  // }
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
@@ -375,15 +353,11 @@ bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){
 }
 void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){
   bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) &&
-     (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) &&
-     hasLowerBounds(basic)){
+  if(d_partialModel.strictlyAboveLowerBound(basic) && hasLowerBounds(basic)){
     ++d_statistics.d_boundComputations;
     success |= propagateCandidateLowerBound(basic);
   }
-  if(d_partialModel.strictlyBelowUpperBound(basic) &&
-     (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) &&
-     hasUpperBounds(basic)){
+  if(d_partialModel.strictlyBelowUpperBound(basic) && hasUpperBounds(basic)){
     ++d_statistics.d_boundComputations;
     success |= propagateCandidateUpperBound(basic);
   }
@@ -752,18 +726,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       if(!possibleConflict.isNull()){
         return possibleConflict;
       }
-      // if(selectSlackUpperBound<pf>(x_j) == ARITHVAR_SENTINEL){
-      //   Node possibleConflict  = deduceUpperBound(x_j);
-      //   if(!possibleConflict.isNull()){
-      //     return possibleConflict;
-      //   }
-      // }
-      // if(selectSlackLowerBound<pf>(x_j) == ARITHVAR_SENTINEL){
-      //   Node possibleConflict  = deduceLowerBound(x_j);
-      //   if(!possibleConflict.isNull()){
-      //     return possibleConflict;
-      //   }
-      // }
     }
   }
   Assert(remainingIterations == 0);
@@ -905,147 +867,6 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar
 }
 
 
-// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){
-//   TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
-
-//   bool anyWeakenings = false;
-//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-//   Assert(d_partialModel.hasLowerBound(basicVar));
-//   Assert(assignment < d_partialModel.getLowerBound(basicVar));
-
-//   DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment;
-
-//   vector<WeakeningElem> weakeningElements;
-//   queue<uint32_t> potentialWeakingings;
-//   for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
-//     const TableauEntry& entry = *i;
-//     ArithVar v = entry.getColVar();
-//     const Rational& coeff = entry.getCoefficient();
-
-//     int sgn = coeff.sgn();
-//     bool ub = (sgn > 0);
-//     Node exp = ub ?
-//       d_partialModel.getUpperConstraint(v) :
-//       d_partialModel.getLowerConstraint(v);
-//     DeltaRational bound = ub?
-//       d_partialModel.getUpperBound(v) :
-//       d_partialModel.getLowerBound(v);
-//     potentialWeakingings.push(weakeningElements.size());
-//     weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp));
-//   }
-
-//   vector<Node> conflict;
-
-//   Debug("weak") << "weakenLowerBoundConflict" << endl;
-//   while(!potentialWeakingings.empty()){
-//     uint32_t pos = potentialWeakingings.front();
-//     potentialWeakingings.pop();
-
-//     WeakeningElem& curr = weakeningElements[pos];
-
-//     Node weaker = curr.upperBound?
-//       d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound):
-//       d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound);
-
-//     bool weakened = false;
-//     if(!weaker.isNull()){
-//       DeltaRational weakerBound = asDeltaRational(weaker);
-//       DeltaRational diff = weakerBound -  curr.bound;
-//       //if var == basic, weakerBound < curr.bound
-//       // multiply by -1
-//       diff = diff * (*curr.coeff);
-
-//       if(surplus > diff){
-//         ++d_statistics.d_weakenings;
-//         anyWeakenings = true;
-//         weakened = true;
-//         surplus = surplus - diff;
-
-//         Debug("weak") << "found:" << endl;
-//         if(curr.var == basicVar){
-//           Debug("weak") << "  basic: ";
-//         }
-//         Debug("weak") << "  " << surplus << " "<< diff  << endl
-//                       << "  " << curr.bound << weakerBound << endl
-//                       << "  " << curr.explanation << weaker << endl;
-
-//         if(curr.explanation.getKind() == AND){
-//           Debug("weak") << "VICTORY" << endl;
-//         }
-
-//         Assert(diff > d_DELTA_ZERO);
-//         curr.explanation = weaker;
-//         curr.bound = weakerBound;
-//       }
-//     }
-
-//     if(weakened){
-//       potentialWeakingings.push(pos);
-//     }else{
-//       if(curr.explanation.getKind() == AND){
-//         Debug("weak") << "boo: " << curr.explanation << endl;
-//       }
-//       conflict.push_back(curr.explanation);
-//     }
-//   }
-
-//   ++d_statistics.d_weakeningAttempts;
-//   if(anyWeakenings){
-//     ++d_statistics.d_weakeningSuccesses;
-//   }
-
-//   NodeBuilder<> nb(AND);
-//   nb.append(conflict);
-//   return nb;
-// }
-
-// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){
-//   Assert(d_tableau.isBasic(basicVar));
-//   Assert(selectSlackUpperBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
-
-//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-
-//   Assert(assignment.getInfinitesimalPart() <= 0);
-
-//   if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){
-//     NodeBuilder<> nb(kind::AND);
-//     explainNonbasicsUpperBound(basicVar, nb);
-//     Node explanation = maybeUnaryConvert(nb);
-//     Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl;
-//     Node res = AssertUpper(basicVar, assignment, explanation);
-//     if(res.isNull()){
-//       d_propManager.propagateArithVar(true, basicVar, assignment, explanation);
-//     }
-//     return res;
-//   }else{
-//     return Node::null();
-//   }
-// }
-
-// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){
-//   Assert(d_tableau.isBasic(basicVar));
-//   Assert(selectSlackLowerBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
-//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-
-//   if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
-
-//   Assert(assignment.getInfinitesimalPart() >= 0);
-
-//   if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){
-//     NodeBuilder<> nb(kind::AND);
-//     explainNonbasicsLowerBound(basicVar, nb);
-//     Node explanation = maybeUnaryConvert(nb);
-//     Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl;
-//     Node res = AssertLower(basicVar, assignment, explanation);
-//     if(res.isNull()){
-//       d_propManager.propagateArithVar(false, basicVar, assignment, explanation);
-//     }
-//     return res;
-//   }else{
-//     return Node::null();
-//   }
-// }
-
 Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){
   return weakenConflict(true, conflictVar);
 }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3c275fae0..e724312fa 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -368,10 +368,7 @@ void TheoryArith::check(Effort effortLevel){
 
     if(!possibleConflict.isNull()){
       d_partialModel.revertAssignmentChanges();
-      //Node simpleConflict  = BooleanSimplification::simplifyConflict(possibleConflict);
-
       Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
-
       d_simplex.clearUpdates();
       d_out->conflict(possibleConflict);
       return;
@@ -386,9 +383,6 @@ void TheoryArith::check(Effort effortLevel){
   if(possibleConflict != Node::null()){
     d_partialModel.revertAssignmentChanges();
     d_simplex.clearUpdates();
-
-    //Node simpleConflict  = BooleanSimplification::simplifyConflict(possibleConflict);
-
     Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
 
     d_out->conflict(possibleConflict);
@@ -424,16 +418,6 @@ void TheoryArith::splitDisequalities(){
       Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
       Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
       Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
-
-      // // < => !>
-      // Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode();
-      // // < => !=
-      // Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode();
-      // // > => !=
-      // Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode();
-      // // All the implication
-      // Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
-
       ++(d_statistics.d_statDisequalitySplits);
       d_out->lemma(lemma);
     }
@@ -476,112 +460,13 @@ void TheoryArith::debugPrintModel(){
   }
 }
 
-/*
-bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){
-  Node varAsNode = asNode(var);
-  const DeltaRational& ub = d_partialModel.getUpperBound(var);
-  Assert(ub.getInfinitesimalPart() <= 0 );
-  Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ;
-  Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart());
-  Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode);
-
-  return bestImplied == exp;
-}
-
-bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){
-  Node varAsNode = asNode(var);
-  const DeltaRational& lb = d_partialModel.getLowerBound(var);
-  Assert(lb.getInfinitesimalPart() >= 0 );
-  Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ;
-  Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart());
-  Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq);
-  return bestImplied == exp;
-}
-*/
-
 void TheoryArith::explain(TNode n) {
   Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
-  //Assert(n.hasAttribute(Propagated()));
 
-  //NodeBuilder<> explainBuilder(AND);
-  //internalExplain(n,explainBuilder);
   Assert(d_propManager.isPropagated(n));
   Node explanation = d_propManager.explain(n);
-  //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation);
-
   d_out->explanation(explanation, true);
 }
-/*
-void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){
-  Assert(n.hasAttribute(Propagated()));
-  Node bound = n.getAttribute(Propagated());
-
-  AlwaysAssert(bound.getKind() == kind::AND);
-
-  for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){
-    Node lit = *i;
-    if(lit.hasAttribute(Propagated())){
-      cout << "hoop the sadjklasdj" << endl;
-      internalExplain(lit, explainBuilder);
-    }else{
-      explainBuilder << lit;
-    }
-  }
-}
-*/
-/*
-static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false;
-void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){
-  Node varAsNode = asNode(var);
-  const DeltaRational& b = upperbound ?
-    d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var);
-
-  Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
-  Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
-  Kind kind;
-  if(upperbound){
-    kind = b.getInfinitesimalPart() < 0 ? LT : LEQ;
-  } else{
-    kind = b.getInfinitesimalPart() > 0 ? GT : GEQ;
-  }
-
-  Node bAsNode = NodeBuilder<2>(kind) << varAsNode
-                                      << mkRationalNode(b.getNoninfinitesimalPart());
-
-  Node bestImplied = upperbound ?
-    d_propagator.getBestImpliedUpperBound(bAsNode):
-    d_propagator.getBestImpliedLowerBound(bAsNode);
-
-  if(!bestImplied.isNull()){
-    Node satValue = d_valuation.getSatValue(bestImplied);
-    if(satValue.isNull()){
-
-      Node reason = upperbound ?
-        d_partialModel.getUpperConstraint(var) :
-        d_partialModel.getLowerConstraint(var);
-
-      //cout << getContext()->getLevel() << " " << bestImplied << " " << reason  << endl;
-      if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){
-        Node lemma = NodeBuilder<2>(IMPLIES) << reason
-                                             << bestImplied;
-
-        //Temporary
-        Node clause = BooleanSimplification::simplifyHornClause(lemma);
-        d_out->lemma(clause);
-      }else{
-        Assert(!bestImplied.hasAttribute(Propagated()));
-        bestImplied.setAttribute(Propagated(), reason);
-        d_reasons.push_back(reason);
-        d_out->propagate(bestImplied);
-      }
-    }else{
-      Assert(!satValue.isNull());
-      Assert(satValue.getKind() == CONST_BOOLEAN);
-      Assert(satValue.getConst<bool>());
-    }
-  }
-}
-*/
 
 void TheoryArith::propagate(Effort e) {
   if(quickCheckOrMore(e)){
@@ -701,19 +586,7 @@ void TheoryArith::notifyRestart(){
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
   ++d_restartsCounter;
-  /*
-  if(d_restartsCounter % d_tableauResetPeriod == 0){
-    double currentDensity = d_tableau.densityMeasure();
-    d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity);
-    if(currentDensity >= d_tableauResetDensity * d_initialDensity){
-
-      ++d_statistics.d_tableauResets;
-      d_tableauResetPeriod += s_TABLEAU_RESET_INCREMENT;
-      d_tableauResetDensity += .2;
-      d_tableau = d_initialTableau;
-    }
-  }
-  */
+
   static const bool debugResetPolicy = false;
 
   uint32_t currSize = d_tableau.size();