More misc. arithmetic cleanup. Removing unused files and functions. Also removing an ugly forward declaration that was needed to get error set bound information on basic variables.

1 files changed, 0 insertions, 208 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index b1dfa8705..1c32f80e4 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -55,7 +55,6 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
   d_basicVariableUpdates(f),
   d_increasing(1),
   d_decreasing(-1),
-  d_relevantErrorBuffer(),
   d_btracking(boundsTracking),
   d_areTracking(false),
   d_trackCallback(this)
@@ -851,213 +850,6 @@ void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb,
   row_bi.addInSgn(nb_inf, oldSgn, currSgn);
 }
 
-void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){
-  ArithVar nb = inf.nonbasic();
-  int sgn = inf.nonbasicDirection();
-  Assert(sgn != 0);
-  Assert(!d_tableau.isBasic(nb));
-
-
-  // Error variables moving in the correct direction
-  Assert(d_relevantErrorBuffer.empty());
-
-  // phases :
-  enum ComputeSafePhase {
-    NoBoundSelected,
-    NbsBoundSelected,
-    BasicBoundSelected,
-    DegenerateBoundSelected
-  } phase;
-
-  phase = NoBoundSelected;
-
-  static int instance = 0;
-  Debug("computeSafeUpdate") << "computeSafeUpdate " <<  (++instance) << endl;
-
-  if(sgn > 0 && d_variables.hasUpperBound(nb)){
-    Constraint ub = d_variables.getUpperBoundConstraint(nb);
-    inf.updatePureFocus(ub->getValue() - d_variables.getAssignment(nb), ub);
-
-    Assert(inf.nonbasicDelta().sgn() == sgn);
-    Debug("computeSafeUpdate") << "computeSafeUpdate " <<  inf.limiting() << endl;
-    phase = NbsBoundSelected;
-  }else if(sgn < 0 && d_variables.hasLowerBound(nb)){
-    Constraint lb = d_variables.getLowerBoundConstraint(nb);
-    inf.updatePureFocus(lb->getValue() - d_variables.getAssignment(nb), lb);
-
-    Assert(inf.nonbasicDelta().sgn() == sgn);
-
-    Debug("computeSafeUpdate") << "computeSafeUpdate " <<  inf.limiting() << endl;
-    phase = NbsBoundSelected;
-  }
-
-  Tableau::ColIterator basicIter = d_tableau.colIterator(nb);
-  for(; !basicIter.atEnd(); ++basicIter){
-    const Tableau::Entry& entry = *basicIter;
-    Assert(entry.getColVar() == nb);
-
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-    const Rational& a_ji = entry.getCoefficient();
-    int basic_movement = sgn * a_ji.sgn();
-
-    Debug("computeSafeUpdate")
-      << "computeSafeUpdate: "
-      << basic << ", "
-      << basic_movement << ", "
-      << d_variables.cmpAssignmentUpperBound(basic) << ", "
-      << d_variables.cmpAssignmentLowerBound(basic) << ", "
-      << a_ji << ", "
-      << d_variables.getAssignment(basic) << endl;
-
-    Constraint proposal = NullConstraint;
-
-    if(basic_movement > 0){
-      if(d_variables.cmpAssignmentLowerBound(basic) < 0){
-        d_relevantErrorBuffer.push_back(&entry);
-      }
-      if(d_variables.hasUpperBound(basic) &&
-         d_variables.cmpAssignmentUpperBound(basic) <= 0){
-        proposal = d_variables.getUpperBoundConstraint(basic);
-      }
-    }else if(basic_movement < 0){
-      if(d_variables.cmpAssignmentUpperBound(basic) > 0){
-        d_relevantErrorBuffer.push_back(&entry);
-      }
-      if(d_variables.hasLowerBound(basic) &&
-         d_variables.cmpAssignmentLowerBound(basic) >= 0){
-        proposal = d_variables.getLowerBoundConstraint(basic);
-      }
-    }
-    if(proposal != NullConstraint){
-      const Rational& coeff = entry.getCoefficient();
-      DeltaRational diff = proposal->getValue() - d_variables.getAssignment(basic);
-      diff /= coeff;
-      int cmp = phase == NoBoundSelected ? 0 : diff.cmp(inf.nonbasicDelta());
-      Assert(diff.sgn() == sgn || diff.sgn() == 0);
-      bool prefer = false;
-      switch(phase){
-      case NoBoundSelected:
-        prefer = true;
-        break;
-      case NbsBoundSelected:
-        prefer = (sgn > 0 && cmp < 0 ) || (sgn < 0 && cmp > 0);
-        break;
-      case BasicBoundSelected:
-        prefer =
-          (sgn > 0 && cmp < 0 ) ||
-          (sgn < 0 && cmp > 0) ||
-          (cmp == 0 && basic == (this->*pref)(basic, inf.leaving()));
-        break;
-      case DegenerateBoundSelected:
-        prefer = cmp == 0 && basic == (this->*pref)(basic, inf.leaving());
-        break;
-      }
-      if(prefer){
-        inf.updatePivot(diff, coeff, proposal);
-
-        phase = (diff.sgn() != 0) ? BasicBoundSelected : DegenerateBoundSelected;
-      }
-    }
-  }
-
-  if(phase == DegenerateBoundSelected){
-    inf.setErrorsChange(0);
-  }else{
-    computedFixed(inf);
-  }
-  inf.determineFocusDirection();
-
-  d_relevantErrorBuffer.clear();
-}
-
-void LinearEqualityModule::computedFixed(UpdateInfo& proposal){
-  Assert(proposal.nonbasicDirection() != 0);
-  Assert(!d_tableau.isBasic(proposal.nonbasic()));
-
-  //bool unconstrained = (proposal.d_limiting == NullConstraint);
-
-  Assert(!proposal.unbounded() || !d_relevantErrorBuffer.empty());
-
-  Assert(proposal.unbounded() ||
-         proposal.nonbasicDelta().sgn() == proposal.nonbasicDirection());
-
-  // proposal.d_value is the max
-
-  UpdateInfo max;
-  int dropped = 0;
-  //Constraint maxFix = NullConstraint;
-  //DeltaRational maxAmount;
-
-  EntryPointerVector::const_iterator i = d_relevantErrorBuffer.begin();
-  EntryPointerVector::const_iterator i_end = d_relevantErrorBuffer.end();
-  for(; i != i_end; ++i){
-    const Tableau::Entry& entry = *(*i);
-    Assert(entry.getColVar() == proposal.nonbasic());
-
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-    const Rational& a_ji = entry.getCoefficient();
-    int basic_movement = proposal.nonbasicDirection() * a_ji.sgn();
-
-    DeltaRational theta;
-    DeltaRational proposedValue;
-    if(!proposal.unbounded()){
-      theta = proposal.nonbasicDelta() * a_ji;
-      proposedValue = theta + d_variables.getAssignment(basic);
-    }
-
-    Constraint fixed = NullConstraint;
-
-    if(basic_movement < 0){
-      Assert(d_variables.cmpAssignmentUpperBound(basic) > 0);
-
-      if(proposal.unbounded() || d_variables.cmpToUpperBound(basic, proposedValue) <= 0){
-        --dropped;
-        fixed = d_variables.getUpperBoundConstraint(basic);
-      }
-    }else if(basic_movement > 0){
-      Assert(d_variables.cmpAssignmentLowerBound(basic) < 0);
-
-      if(proposal.unbounded() || d_variables.cmpToLowerBound(basic, proposedValue) >= 0){
-        --dropped;
-        fixed = d_variables.getLowerBoundConstraint(basic);
-      }
-    }
-    if(fixed != NullConstraint){
-      DeltaRational amount = fixed->getValue() - d_variables.getAssignment(basic);
-      amount /= a_ji;
-      Assert(amount.sgn() == proposal.nonbasicDirection());
-
-      if(max.uninitialized()){
-        max = UpdateInfo(proposal.nonbasic(), proposal.nonbasicDirection());
-        max.updatePivot(amount, a_ji, fixed, dropped);
-      }else{
-        int cmp = amount.cmp(max.nonbasicDelta());
-        bool prefer =
-          (proposal.nonbasicDirection() < 0 && cmp < 0) ||
-          (proposal.nonbasicDirection() > 0 && cmp > 0) ||
-          (cmp == 0 && fixed->getVariable() < max.limiting()->getVariable());
-
-        if(prefer){
-          max.updatePivot(amount, a_ji, fixed, dropped);
-        }else{
-          max.setErrorsChange(dropped);
-        }
-      }
-    }
-  }
-  Assert(dropped < 0 || !proposal.unbounded());
-
-  if(dropped < 0){
-    proposal = max;
-  }else{
-    Assert(dropped == 0);
-    Assert(proposal.nonbasicDelta().sgn() != 0);
-    Assert(proposal.nonbasicDirection() != 0);
-    proposal.setErrorsChange(0);
-  }
-  Assert(proposal.errorsChange() == dropped);
-}
-
 ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const{
   if(vec.empty()) {
     return ARITHVAR_SENTINEL;