Removing arithmetic legacy code and unifying functions.

3 files changed, 57 insertions, 154 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index bde771102..b1dfa8705 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -25,8 +25,6 @@ namespace theory {
 namespace arith {
 
 /* Explicitly instatiate these functions. */
-template void LinearEqualityModule::propagateNonbasics<true>(ArithVar basic, Constraint c);
-template void LinearEqualityModule::propagateNonbasics<false>(ArithVar basic, Constraint c);
 
 template ArithVar LinearEqualityModule::selectSlack<true>(ArithVar x_i, VarPreferenceFunction pf) const;
 template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const;
@@ -421,29 +419,6 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
   return result;
 }
 
-// DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
-//   DeltaRational sum(0,0);
-//   for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
-//     const Tableau::Entry& entry = (*i);
-//     ArithVar nonbasic = entry.getColVar();
-//     if(nonbasic == basic) continue;
-//     const Rational& coeff =  entry.getCoefficient();
-//     int sgn = coeff.sgn();
-//     bool ub = upperBound ? (sgn > 0) : (sgn < 0);
-
-//     const DeltaRational& bound = ub ?
-//       d_variables.getUpperBound(nonbasic):
-//       d_variables.getLowerBound(nonbasic);
-
-//     DeltaRational diff = bound * coeff;
-//     sum = sum + diff;
-//   }
-//   return sum;
-// }
-DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound) const {
-  RowIndex rid = d_tableau.basicToRowIndex(basic);
-  return computeRowBound(rid, upperBound, basic);
-}
 DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const {
   DeltaRational sum(0,0);
   for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
@@ -483,33 +458,6 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) co
   return sum;
 }
 
-// bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
-//   for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
-//     const Tableau::Entry& entry = *iter;
-
-//     ArithVar var = entry.getColVar();
-//     if(var == basic) continue;
-//     int sgn = entry.getCoefficient().sgn();
-//     if(upperBound){
-//       if( (sgn < 0 && !d_variables.hasLowerBound(var)) ||
-//           (sgn > 0 && !d_variables.hasUpperBound(var))){
-//         return false;
-//       }
-//     }else{
-//       if( (sgn < 0 && !d_variables.hasUpperBound(var)) ||
-//           (sgn > 0 && !d_variables.hasLowerBound(var))){
-//         return false;
-//       }
-//     }
-//   }
-//   return true;
-// }
-
-bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
-  RowIndex ridx = d_tableau.basicToRowIndex(basic);
-  return rowLacksBound(ridx, upperBound, basic) == NULL;
-}
-
 const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool rowUb, ArithVar skip){
   Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
   for(; !iter.atEnd(); ++iter){
@@ -530,55 +478,19 @@ const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool ro
   return NULL;
 }
 
-
-template <bool upperBound>
-void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
-  Assert(d_tableau.isBasic(basic));
-  Assert(c->getVariable() == basic);
+void LinearEqualityModule::propagateBasicFromRow(Constraint c){
+  Assert(c != NullConstraint);
+  Assert(c->isUpperBound() || c->isLowerBound());
   Assert(!c->assertedToTheTheory());
-  Assert(!upperBound || c->isUpperBound()); // upperbound implies c is an upperbound
-  Assert(upperBound || c->isLowerBound()); // !upperbound implies c is a lowerbound
-  //Assert(c->canBePropagated());
   Assert(!c->hasProof());
 
-  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
-                                   << basic <<") start" << endl;
+  bool upperBound = c->isUpperBound();
+  ArithVar basic = c->getVariable();
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
 
   vector<Constraint> bounds;
-
-  Tableau::RowIterator iter = d_tableau.basicRowIterator(basic);
-  for(; !iter.atEnd(); ++iter){
-    const Tableau::Entry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == basic) continue;
-
-    const Rational& a_ij = entry.getCoefficient();
-
-    int sgn = a_ij.sgn();
-    Assert(sgn != 0);
-    Constraint bound = NullConstraint;
-    if(upperBound){
-      if(sgn < 0){
-        bound = d_variables.getLowerBoundConstraint(nonbasic);
-      }else{
-        Assert(sgn > 0);
-        bound = d_variables.getUpperBoundConstraint(nonbasic);
-      }
-    }else{
-      if(sgn < 0){
-        bound = d_variables.getUpperBoundConstraint(nonbasic);
-      }else{
-        Assert(sgn > 0);
-        bound = d_variables.getLowerBoundConstraint(nonbasic);
-      }
-    }
-    Assert(bound != NullConstraint);
-    Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
-    bounds.push_back(bound);
-  }
+  propagateRow(bounds, ridx, upperBound, c);
   c->impliedBy(bounds);
-  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
-                                   << basic << ") done" << endl;
 }
 
 void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){
@@ -589,7 +501,6 @@ void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx,
   ArithVar v = c->getVariable();
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
                                    << v <<") start" << endl;
-  //vector<Constraint> bounds;
 
   Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
   for(; !iter.atEnd(); ++iter){
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index b1f3d00d7..4d18d5c81 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -261,9 +261,6 @@ public:
 
   void forceNewBasis(const DenseSet& newBasis);
 
-#warning "Remove legacy code."
-  bool hasBounds(ArithVar basic, bool upperBound);
-
   /**
    * Returns a pointer to the first Tableau entry on the row ridx that does not
    * have an either a lower bound/upper bound for proving a bound on skip.
@@ -416,17 +413,13 @@ private:
   BoundInfoMap& d_btracking;
   bool d_areTracking;
 
-#warning "Remove legacy code"
-  template <bool upperBound>
-  void propagateNonbasics(ArithVar basic, Constraint c);
-
 public:
-  void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){
-    propagateNonbasics<false>(basic, c);
-  }
-  void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
-    propagateNonbasics<true>(basic, c);
-  }
+  /**
+   * The constraint on a basic variable b is implied by the constraints
+   * on its row.  This is a wrapper for propagateRow().
+   */
+  void propagateBasicFromRow(Constraint c);
+
   /**
    * Exports either the explanation of an upperbound or a lower bound
    * of the basic variable basic, using the non-basic variables in the row.
@@ -442,13 +435,6 @@ public:
    */
   DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
 
-  inline DeltaRational computeLowerBound(ArithVar basic) const{
-    return computeBound(basic, false);
-  }
-  inline DeltaRational computeUpperBound(ArithVar basic) const{
-    return computeBound(basic, true);
-  }
-
   /**
    * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
    * and 2 ArithVar variables and returns one of the ArithVar variables
@@ -547,29 +533,45 @@ public:
    * The minimum/maximum is determined by the direction the non-basic is changing.
    */
   bool basicsAtBounds(const UpdateInfo& u) const;
+
 private:
+
+  /**
+   * Recomputes the bound info for a row using either the information
+   * in the bounds queue or the current information.
+   * O(row length of ridx)
+   */
   BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const;
+
 public:
+  /** Debug only routine. */
   BoundCounts debugBasicAtBoundCount(ArithVar x_i) const;
+
+  /** Track the effect of the change of coefficient for bound counting. */
   void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
+
+  /** Track the effect of multiplying a row by a sign for bound counting. */
   void trackingMultiplyRow(RowIndex ridx, int sgn);
 
+  /** Count for how many on a row have *an* upper/lower bounds. */
   BoundCounts hasBoundCount(RowIndex ri) const {
     Assert(d_variables.boundsQueueEmpty());
     return d_btracking[ri].hasBounds();
   }
 
-#warning "Remove legacy code"
+  /**
+   * Are there any non-basics on x_i's row that are not at
+   * their respective lower bounds (mod sgns).
+   * O(1) time due to the atBound() count.
+   */
   bool nonbasicsAtLowerBounds(ArithVar x_i) const;
-  bool nonbasicsAtUpperBounds(ArithVar x_i) const;
 
-#warning "Remove legacy code"
-  ArithVar _anySlackLowerBound(ArithVar x_i) const {
-    return selectSlack<true>(x_i, &LinearEqualityModule::noPreference);
-  }
-  ArithVar _anySlackUpperBound(ArithVar x_i) const {
-    return selectSlack<false>(x_i, &LinearEqualityModule::noPreference);
-  }
+  /**
+   * Are there any non-basics on x_i's row that are not at
+   * their respective upper bounds (mod sgns).
+   * O(1) time due to the atBound() count.
+   */
+  bool nonbasicsAtUpperBounds(ArithVar x_i) const;
 
 private:
   class TrackingCallback : public CoefficientChangeCallback {
@@ -616,11 +618,12 @@ public:
     return minimallyWeakConflict(false, conflictVar);
   }
 
+  /**
+   * Computes the sum of the upper/lower bound of row.
+   * The variable skip is not included in the sum.
+   */
   DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const;
 
-private:
-  DeltaRational computeBound(ArithVar basic, bool upperBound) const;
-
 public:
   void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult);
   void directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 31b6cd032..7eae2606c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1401,20 +1401,6 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
     }
   }
 
-  // Kind simpleKind = Comparison::comparisonKind(assertion);
-  // Assert(simpleKind != UNDEFINED_KIND);
-  // Assert(constraint != NullConstraint ||
-  //        simpleKind == EQUAL ||
-  //        simpleKind == DISTINCT );
-  // if(simpleKind == EQUAL || simpleKind == DISTINCT){
-  //   Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
-
-  //   if(!isSetup(eq)){
-  //     //The previous code was equivalent to:
-  //     setupAtom(eq);
-  //     constraint = d_constraintDatabase.lookup(assertion);
-  //   }
-  // }
   Assert(constraint != NullConstraint);
 
   if(constraint->negationHasProof()){
@@ -2490,9 +2476,8 @@ EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) {
 bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound){
   ++d_statistics.d_boundComputations;
 
-  DeltaRational bound = upperBound ?
-    d_linEq.computeUpperBound(basic):
-    d_linEq.computeLowerBound(basic);
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  DeltaRational bound = d_linEq.computeRowBound(ridx, upperBound, basic);
 
   if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
      (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
@@ -2540,13 +2525,7 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
       }
 
       if(!assertedToTheTheory && canBePropagated && !hasProof ){
-        if(upperBound){
-          Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic));
-          d_linEq.propagateNonbasicsUpperBound(basic, bestImplied);
-        }else{
-          Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic));
-          d_linEq.propagateNonbasicsLowerBound(basic, bestImplied);
-        }
+        d_linEq.propagateBasicFromRow(bestImplied);
         // I think this can be skipped if canBePropagated is true
         //d_learnedBounds.push(bestImplied);
         if(Debug.isOn("arith::prop")){
@@ -2570,10 +2549,20 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
 
 void TheoryArithPrivate::propagateCandidate(ArithVar basic){
   bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasBounds(basic, false)){
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+
+  bool tryLowerBound =
+    d_partialModel.strictlyAboveLowerBound(basic) &&
+    d_linEq.rowLacksBound(ridx, false, basic) == NULL;
+
+  bool tryUpperBound =
+    d_partialModel.strictlyBelowUpperBound(basic) &&
+    d_linEq.rowLacksBound(ridx, true, basic) == NULL;
+
+  if(tryLowerBound){
     success |= propagateCandidateLowerBound(basic);
   }
-  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasBounds(basic, true)){
+  if(tryUpperBound){
     success |= propagateCandidateUpperBound(basic);
   }
   if(success){