Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now heuristically reset to its initial state during restarts.

4 files changed, 121 insertions, 4 deletions

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index a8bcd28cc..cb1364488 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -45,11 +45,14 @@ void Tableau::internalCopy(const Tableau& tab){
     d_rowCount.insert(d_rowCount.end(), N, 0);
   }
 
+  ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin();
   ColumnMatrix::iterator i_colIter = d_columnMatrix.begin();
   ColumnMatrix::iterator end_colIter = d_columnMatrix.end();
-  for(; i_colIter != end_colIter; ++i_colIter){
+  for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){
+    Assert(otherIter != tab.d_columnMatrix.end());
     Column& col = *i_colIter;
-    col.increaseSize(d_columnMatrix.size());
+    const Column& otherCol = *otherIter;
+    col.increaseSize(otherCol.allocated());
   }
 
   ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin();
@@ -183,3 +186,24 @@ void Tableau::printTableau(){
     }
   }
 }
+
+uint32_t Tableau::numNonZeroEntries() const {
+  uint32_t colSum = 0;
+  ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
+  for(; i != end; ++i){
+    const Column& col = *i;
+    colSum += col.size();
+  }
+  return colSum;
+}
+
+uint32_t Tableau::numNonZeroEntriesByRow() const {
+  uint32_t rowSum = 0;
+  ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
+  for(; i != end; ++i){
+    ArithVar basic = *i;
+    const ReducedRowVector& row = *(d_rowsTable[basic]);
+    rowSum += row.size();
+  }
+  return rowSum;
+}
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index dad4bb2f5..31f7cfa5a 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -156,7 +156,37 @@ public:
   ReducedRowVector* removeRow(ArithVar basic);
 
 
+  /**
+   * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size().
+   * When n >= 1,
+   *   densityMeasure() := s / (n*m - n**2 + n)
+   *                    := s / (n *(m - n + 1))
+   * When n = 0, densityMeasure() := 1
+   */
+  double densityMeasure() const{
+    Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
+    uint32_t n = getNumRows();
+    if(n == 0){
+      return 1.0;
+    }else {
+      uint32_t s = numNonZeroEntries();
+      uint32_t m = d_columnMatrix.size();
+      uint32_t divisor = (n *(m - n + 1));
+
+      Assert(n >= 1);
+      Assert(m >= n);
+      Assert(divisor > 0);
+      Assert(divisor >= s);
+
+      return (double(s)) / divisor;
+    }
+  }
+
 private:
+
+  uint32_t numNonZeroEntries() const;
+  uint32_t numNonZeroEntriesByRow() const;
+
   /** Copies the datastructures in tab to this.*/
   void internalCopy(const Tableau& tab);
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 60eed27d1..456fdb746 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -60,6 +60,10 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_userVariables(),
   d_diseq(c),
   d_tableau(),
+  d_restartsCounter(0),
+  d_initialDensity(1.0),
+  d_tableauResetDensity(2.0),
+  d_tableauResetPeriod(10),
   d_propagator(c, out),
   d_simplex(d_constants, d_partialModel, d_out, d_tableau),
   d_statistics()
@@ -74,7 +78,11 @@ TheoryArith::Statistics::Statistics():
   d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
-  d_presolveTime("theory::arith::presolveTime")
+  d_presolveTime("theory::arith::presolveTime"),
+  d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
+  d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
+  d_tableauResets("theory::arith::tableauResets", 0),
+  d_restartTimer("theory::arith::restartTimer")
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
@@ -84,6 +92,11 @@ TheoryArith::Statistics::Statistics():
 
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
+
+  StatisticsRegistry::registerStat(&d_initialTableauDensity);
+  StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
+  StatisticsRegistry::registerStat(&d_tableauResets);
+  StatisticsRegistry::registerStat(&d_restartTimer);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -95,6 +108,11 @@ TheoryArith::Statistics::~Statistics(){
 
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
+
+  StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
+  StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
+  StatisticsRegistry::unregisterStat(&d_tableauResets);
+  StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
@@ -658,7 +676,22 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
 }
 
 void TheoryArith::notifyRestart(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
+
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+
+  ++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;
+    }
+  }
 }
 
 bool TheoryArith::entireStateIsConsistent(){
@@ -731,7 +764,10 @@ void TheoryArith::presolve(){
     }
   }
 
-  //Assert(entireStateIsConsistent()); //Boy is this paranoid
+  d_initialTableau = d_tableau;
+  d_initialDensity = d_initialTableau.densityMeasure();
+  d_statistics.d_initialTableauDensity.setData(d_initialDensity);
+
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
   static int callCount = 0;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index fb39eac09..3ff83abdf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -122,6 +122,27 @@ private:
    */
   Tableau d_tableau;
 
+  /**
+   * A copy of the tableau immediately after removing variables
+   * without bounds in presolve().
+   */
+  Tableau d_initialTableau;
+
+  /** Counts the number of notifyRestart() calls to the theory. */
+  uint32_t d_restartsCounter;
+
+  /**
+   * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
+   * the density of the tableau, d, is computed.
+   * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
+   * is set to d_initialTableau.
+   */
+  double d_initialDensity;
+  double d_tableauResetDensity;
+  uint32_t d_tableauResetPeriod;
+  static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
+
+
   ArithUnatePropagator d_propagator;
   SimplexDecisionProcedure d_simplex;
 
@@ -215,6 +236,12 @@ private:
 
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
+
+    BackedStat<double> d_initialTableauDensity;
+    AverageStat d_avgTableauDensityAtRestart;
+    IntStat d_tableauResets;
+    TimerStat d_restartTimer;
+
     Statistics();
     ~Statistics();
   };