Overview of the changes:

- Preparing to remove row ejection from the code base!
- Checks for conflicts immediately after a pivot to avoid potentially wasteful search.
- Added arithvar_set.h. This replaces ArithVarSet that was previously in the Tableau, and ArithVarDenseSet.
- Removes variables that have no preregistered bounds during presolve().
- Theory::isLeafOf() currently returns true for atoms. (I was unaware.) I modified Variable::isMember() to account for this exclude atoms.
- Added statistics all over the place.


This commit effects both boolean search and simplex search so expect running times to go all over the place. The time differences should be roughly as follows:
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1486&reference_id=1447&p=10&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29

11 files changed, 427 insertions, 198 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 6cb35e518..31867c4cf 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -20,6 +20,7 @@ libarith_la_SOURCES = \
 	ordered_bounds_list.h \
 	ordered_set.h \
 	arithvar_dense_set.h \
+	arithvar_set.h \
 	tableau.h \
 	tableau.cpp \
 	simplex.h \
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
new file mode 100644
index 000000000..95617c5a0
--- /dev/null
+++ b/src/theory/arith/arithvar_set.h
@@ -0,0 +1,134 @@
+/*********************                                                        */
+/*! \file arithvar_set.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <vector>
+#include "theory/arith/arith_utilities.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
+#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * This is an abstraction of a set of ArithVars.
+ * This class is designed to provide constant time insertion, deletion, and element_of
+ * and fast iteration.
+ * The cost of doing this is that it takes O(M) where M is the total number
+ * of ArithVars in memory.
+ */
+
+class ArithVarSet {
+private:
+  typedef std::vector<ArithVar> VarList;
+  //List of the ArithVars in the set.
+  VarList d_list;
+
+  //Each ArithVar in the set is mapped to its position in d_list.
+  //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
+  std::vector<unsigned> d_posVector;
+
+public:
+  typedef VarList::const_iterator iterator;
+
+ ArithVarSet() :  d_list(), d_posVector() {}
+
+  size_t size() const {
+    return d_list.size();
+  }
+
+  size_t allocated() const {
+    return d_posVector.size();
+  }
+
+  void increaseSize(ArithVar max){
+    Assert(max >= allocated());
+    d_posVector.resize(max+1, ARITHVAR_SENTINEL);
+  }
+
+  void increaseSize(){
+    increaseSize(allocated());
+  }
+
+  bool isMember(ArithVar x) const{
+    Assert(x <  allocated());
+    return d_posVector[x] != ARITHVAR_SENTINEL;
+  }
+
+  /** Invalidates iterators */
+  void init(ArithVar x, bool val) {
+    Assert(x >= size());
+    increaseSize(x);
+    if(val){
+      add(x);
+    }
+  }
+
+  /** Invalidates iterators */
+  void add(ArithVar x){
+    Assert(!isMember(x));
+    d_posVector[x] = size();
+    d_list.push_back(x);
+  }
+
+  iterator begin() const{ return d_list.begin(); }
+  iterator end() const{ return d_list.end(); }
+
+
+  /** Invalidates iterators */
+  void remove(ArithVar x){
+    Assert(isMember(x));
+    swapToBack(x);
+    d_posVector[x] = ARITHVAR_SENTINEL;
+    d_list.pop_back();
+  }
+
+ private:
+
+  /** This should be true of all x < allocated() after every operation. */
+  bool wellFormed(ArithVar x){
+    if(d_posVector[x] == ARITHVAR_SENTINEL){
+      return true;
+    }else{
+      return d_list[d_posVector[x]] == x;
+    }
+  }
+
+  /** Swaps a member x to the back of d_list. */
+  void swapToBack(ArithVar x){
+    Assert(isMember(x));
+
+    unsigned currentPos = d_posVector[x];
+    ArithVar atBack = d_list.back();
+
+    d_list[currentPos] = atBack;
+    d_posVector[atBack] = currentPos;
+
+    d_list[size() - 1] = x;
+    d_posVector[x] = size() - 1;
+  }
+};
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 29db6cdb9..aa4e8bc13 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -188,6 +188,7 @@ public:
   static bool isMember(Node n) {
     if (n.getKind() == kind::CONST_INTEGER) return false;
     if (n.getKind() == kind::CONST_RATIONAL) return false;
+    if (isRelationOperator(n.getKind())) return false;
     return Theory::isLeafOf(n, theory::THEORY_ARITH);
   }
 
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 2e9fb7352..f7e3c112c 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -21,7 +21,10 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_statUnEjections("theory::arith::UnEjections", 0),
   d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
   d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
-  d_selectInitialConflictTime("theory::arith::selectInitialConflictTime")
+  d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
+  d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0),
+  d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0),
+  d_pivotTime("theory::arith::pivotTime")
 {
   StatisticsRegistry::registerStat(&d_statPivots);
   StatisticsRegistry::registerStat(&d_statUpdates);
@@ -33,6 +36,10 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_statEarlyConflicts);
   StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
   StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
+
+  StatisticsRegistry::registerStat(&d_pivotsAfterConflict);
+  StatisticsRegistry::registerStat(&d_checksWithWastefulPivots);
+  StatisticsRegistry::registerStat(&d_pivotTime);
 }
 
 SimplexDecisionProcedure::Statistics::~Statistics(){
@@ -46,10 +53,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
   StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
   StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
+
+  StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict);
+  StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots);
+  StatisticsRegistry::unregisterStat(&d_pivotTime);
 }
 
 
 void SimplexDecisionProcedure::ejectInactiveVariables(){
+  return; //die die die
 
   for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){
     ArithVar variable = *i;
@@ -247,6 +259,32 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
 void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
   Assert(x_i != x_j);
 
+  TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
+
+  if(Debug.isOn("arith::pivotAndUpdate")){
+    Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
+    ReducedRowVector* row_k = d_tableau.lookup(x_i);
+    for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero();
+        varIter != row_k->endNonZero();
+        ++varIter){
+
+      ArithVar var = varIter->first;
+      const Rational& coeff = varIter->second;
+      DeltaRational beta = d_partialModel.getAssignment(var);
+      Debug("arith::pivotAndUpdate") << var << beta << coeff;
+      if(d_partialModel.hasLowerBound(var)){
+        Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")";
+      }
+      if(d_partialModel.hasUpperBound(var)){
+        Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var)
+                                       << ")";
+      }
+      Debug("arith::pivotAndUpdate") << endl;
+    }
+    Debug("arith::pivotAndUpdate") << "end row"<< endl;
+  }
+
+
   ReducedRowVector* row_i = d_tableau.lookup(x_i);
   const Rational& a_ij = row_i->lookup(x_j);
 
@@ -279,11 +317,35 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
     }
   }
 
+  // Pivots
   ++(d_statistics.d_statPivots);
+  if( d_foundAConflict ){
+    ++d_pivotsSinceConflict;
+    if(d_pivotsSinceConflict == 1){
+      ++(d_statistics.d_checksWithWastefulPivots);
+    }
+    ++(d_statistics.d_pivotsAfterConflict);
+  }
+
   d_tableau.pivot(x_i, x_j);
 
   checkBasicVariable(x_j);
 
+  // Debug found conflict
+  if( !d_foundAConflict ){
+    DeltaRational beta_j = d_partialModel.getAssignment(x_j);
+
+    if(d_partialModel.belowLowerBound(x_j, beta_j, true)){
+      if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){
+        d_foundAConflict = true;
+      }
+    }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){
+      if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){
+        d_foundAConflict = true;
+      }
+    }
+  }
+
   if(Debug.isOn("tableau")){
     d_tableau.printTableau();
   }
@@ -364,7 +426,8 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
         }else{
           slack = nonbasic; break;
         }
-      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){
+      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
+        if(d_pivotStage){
           if(d_tableau.getRowCount(nonbasic) < numRows){
             slack = nonbasic;
             numRows = d_tableau.getRowCount(nonbasic);
@@ -409,26 +472,15 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
     ArithVar x_i = (*i).first;
     d_griggioRuleQueue.push(*i);
 
-    DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+    Node possibleConflict = checkBasicForConflict(x_i);
+    if(!possibleConflict.isNull()){
+      Node better = betterConflict(bestConflict, possibleConflict);
 
-    if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      ArithVar x_j = selectSlackBelow(x_i);
-      if(x_j == ARITHVAR_SENTINEL ){
-	Node better = betterConflict(bestConflict, generateConflictBelow(x_i));
-	if(better != bestConflict) ++conflictChanges;
-	bestConflict = better;
-        ++(d_statistics.d_statEarlyConflicts);
-      }
-    }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      ArithVar x_j = selectSlackAbove(x_i);
-      if(x_j == ARITHVAR_SENTINEL ){
-	Node better = betterConflict(bestConflict, generateConflictAbove(x_i));
-	if(better != bestConflict) ++conflictChanges;
-	bestConflict = better;
-        ++(d_statistics.d_statEarlyConflicts);
+      if(better != bestConflict){
+        ++conflictChanges;
       }
+      bestConflict = better;
+      ++(d_statistics.d_statEarlyConflicts);
     }
   }
   if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
@@ -438,7 +490,13 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
 Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_griggioRuleQueue.empty()) return Node::null();
 
-  Node possibleConflict = selectInitialConflict();
+  d_foundAConflict = false;
+  d_pivotsSinceConflict = 0;
+
+  Node possibleConflict = Node::null();
+  if(d_griggioRuleQueue.size() > 1){
+    possibleConflict = selectInitialConflict();
+  }
   if(possibleConflict.isNull()){
     possibleConflict = privateUpdateInconsistentVars();
   }
@@ -457,6 +515,25 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   return possibleConflict;
 }
 
+Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
+
+  Assert(d_basicManager.isMember(basic));
+  const DeltaRational& beta = d_partialModel.getAssignment(basic);
+
+  if(d_partialModel.belowLowerBound(basic, beta, true)){
+    ArithVar x_j = selectSlackBelow(basic);
+    if(x_j == ARITHVAR_SENTINEL ){
+      return generateConflictBelow(basic);
+    }
+  }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
+    ArithVar x_j = selectSlackAbove(basic);
+    if(x_j == ARITHVAR_SENTINEL ){
+      return generateConflictAbove(basic);
+    }
+  }
+  return Node::null();
+}
+
 //corresponds to Check() in dM06
 Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
   Assert(d_pivotStage || d_griggioRuleQueue.empty());
@@ -470,7 +547,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
     ArithVar x_i = selectSmallestInconsistentVar();
-    Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
+    Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == ARITHVAR_SENTINEL){
       Debug("arith_update") << "No inconsistent variables" << endl;
       return Node::null(); //sat
@@ -481,10 +558,11 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
       ejectInactiveVariables();
 
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+    ArithVar x_j = ARITHVAR_SENTINEL;
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      ArithVar x_j = selectSlackBelow(x_i);
+      x_j = selectSlackBelow(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelow(x_i); //unsat
@@ -493,13 +571,19 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      ArithVar x_j = selectSlackAbove(x_i);
+      x_j = selectSlackAbove(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAbove(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, u_i);
     }
+    Assert(x_j != ARITHVAR_SENTINEL);
+    //Check to see if we already have a conflict with x_j to prevent wasteful work
+    Node earlyConflict = checkBasicForConflict(x_j);
+    if(!earlyConflict.isNull()){
+      return earlyConflict;
+    }
   }
 
   if(d_pivotStage && iteratationNum >= d_numVariables){
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 2ae6b091d..587f468e0 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -5,7 +5,7 @@
 #define __CVC4__THEORY__ARITH__SIMPLEX_H
 
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
@@ -55,7 +55,7 @@ private:
    */
   ArithPartialModel& d_partialModel;
 
-  ArithVarDenseSet& d_basicManager;
+  ArithVarSet& d_basicManager;
   ActivityMonitor& d_activityMonitor;
 
   OutputChannel* d_out;
@@ -70,7 +70,7 @@ private:
 public:
   SimplexDecisionProcedure(const ArithConstants& constants,
                            ArithPartialModel& pm,
-                           ArithVarDenseSet& bm,
+                           ArithVarSet& bm,
                            OutputChannel* out,
                            ActivityMonitor& am,
                            Tableau& tableau) :
@@ -197,6 +197,15 @@ private:
   /** Check to make sure all of the basic variables are within their bounds. */
   void checkBasicVariable(ArithVar basic);
 
+  /**
+   * Checks a basic variable, b, to see if it is in conflict.
+   * If a conflict is discovered a node summarizing the conflict is returned.
+   * Otherwise, Node::null() is returned.
+   */
+  Node checkBasicForConflict(ArithVar b);
+
+  bool d_foundAConflict;
+  unsigned d_pivotsSinceConflict;
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
@@ -207,7 +216,11 @@ private:
     IntStat d_statEjections, d_statUnEjections;
 
     IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
+
     TimerStat d_selectInitialConflictTime;
+
+    IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots;
+    TimerStat d_pivotTime;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 1d58c5e1d..1cf6d07cd 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -33,7 +33,7 @@ void Tableau::addRow(ArithVar basicVar,
 
   //The new basic variable cannot already be a basic variable
   Assert(!isActiveBasicVariable(basicVar));
-  d_activeBasicVars.insert(basicVar);
+  d_activeBasicVars.add(basicVar);
   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
   d_rowsTable[basicVar] = row_current;
 
@@ -73,10 +73,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   d_rowsTable[x_s] = row_s;
   d_rowsTable[x_r] = NULL;
 
-  d_activeBasicVars.erase(x_r);
+  d_activeBasicVars.remove(x_r);
   d_basicManager.remove(x_r);
 
-  d_activeBasicVars.insert(x_s);
+  d_activeBasicVars.add(x_s);
   d_basicManager.add(x_s);
 
   row_s->pivot(x_s);
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 5e34ac1a2..05fcf6cf8 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -22,7 +22,7 @@
 #include "expr/attribute.h"
 
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
 #include "theory/arith/normal_form.h"
 
 #include "theory/arith/row_vector.h"
@@ -37,54 +37,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class ArithVarSet {
-private:
-  typedef std::list<ArithVar> VarList;
-
-public:
-  typedef VarList::const_iterator iterator;
-
-private:
-  VarList d_list;
-  std::vector< VarList::iterator > d_posVector;
-
-public:
-  ArithVarSet() : d_list(),  d_posVector() {}
-
-  iterator begin() const{ return d_list.begin(); }
-  iterator end() const{ return d_list.end(); }
-
-  void insert(ArithVar av){
-    Assert(inRange(av) );
-    Assert(!inSet(av) );
-
-    d_posVector[av] = d_list.insert(d_list.end(), av);
-  }
-
-  void erase(ArithVar var){
-    Assert( inRange(var) );
-    Assert( inSet(var) );
-
-    d_list.erase(d_posVector[var]);
-    d_posVector[var] = d_list.end();
-  }
-
-  void increaseSize(){
-    d_posVector.push_back(d_list.end());
-  }
-
-  bool inSet(ArithVar v) const{
-    Assert(inRange(v) );
-
-    return d_posVector[v] != d_list.end();
-  }
-
-private:
-  bool inRange(ArithVar v) const{
-    return v < d_posVector.size();
-  }
-};
-
 class Tableau {
 private:
 
@@ -95,7 +47,7 @@ private:
 
 
   ActivityMonitor& d_activityMonitor;
-  ArithVarDenseSet& d_basicManager;
+  ArithVarSet& d_basicManager;
 
   std::vector<uint32_t> d_rowCount;
 
@@ -103,7 +55,7 @@ public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) :
+  Tableau(ActivityMonitor &am, ArithVarSet& bm) :
     d_activeBasicVars(),
     d_rowsTable(),
     d_activityMonitor(am),
@@ -163,20 +115,22 @@ public:
     Assert(d_basicManager.isMember(basic));
     Assert(isActiveBasicVariable(basic));
 
-    d_activeBasicVars.erase(basic);
+    d_activeBasicVars.remove(basic);
   }
 
   void reinjectBasic(ArithVar basic){
+    AlwaysAssert(false);
+
     Assert(d_basicManager.isMember(basic));
     Assert(isEjected(basic));
 
     ReducedRowVector* row = lookupEjected(basic);
-    d_activeBasicVars.insert(basic);
+    d_activeBasicVars.add(basic);
     updateRow(row);
   }
 private:
   inline bool isActiveBasicVariable(ArithVar var){
-    return d_activeBasicVars.inSet(var);
+    return d_activeBasicVars.isMember(var);
   }
 
   void updateRow(ReducedRowVector* row);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ff79c18e6..1e1ac03ba 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -31,7 +31,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
 
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/unate_propagator.h"
@@ -58,6 +58,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_constants(NodeManager::currentNM()),
   d_partialModel(c),
   d_basicManager(),
+  d_userVariables(),
   d_activityMonitor(),
   d_diseq(c),
   d_tableau(d_activityMonitor, d_basicManager),
@@ -73,13 +74,18 @@ TheoryArith::Statistics::Statistics():
   d_statSlackVariables("theory::arith::SlackVariables", 0),
   d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
   d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
-  d_staticLearningTimer("theory::arith::staticLearningTimer")
+  d_staticLearningTimer("theory::arith::staticLearningTimer"),
+  d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
+  d_presolveTime("theory::arith::presolveTime")
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
   StatisticsRegistry::registerStat(&d_statDisequalitySplits);
   StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
   StatisticsRegistry::registerStat(&d_staticLearningTimer);
+
+  StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
+  StatisticsRegistry::registerStat(&d_presolveTime);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -88,6 +94,9 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
   StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
   StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
+
+  StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
+  StatisticsRegistry::unregisterStat(&d_presolveTime);
 }
 
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
@@ -132,34 +141,34 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
       TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
 
       if((t == cright) && (e == cleft)){
-	TNode tmp = t;
-	t = e;
-	e = tmp;
-	k = reverseRelationKind(k);
+        TNode tmp = t;
+        t = e;
+        e = tmp;
+        k = reverseRelationKind(k);
       }
       if(t == cleft && e == cright){
-	// t == cleft && e == cright
-	Assert( t == cleft );
-	Assert( e == cright );
-	switch(k){
-	case LT:   // (ite (< x y) x y)
-	case LEQ: { // (ite (<= x y) x y)
-	  Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
-	  Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
-	  Debug("arith::mins") << n << "is a min =>"  << nLeqX << nLeqY << endl;
-	  learned << nLeqX << nLeqY;
-	  break;
-	}
-	case GT: // (ite (> x y) x y)
-	case GEQ: { // (ite (>= x y) x y)
-	  Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
-	  Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
-	  Debug("arith::mins") << n << "is a max =>"  << nGeqX << nGeqY << endl;
-	  learned << nGeqX << nGeqY;
-	  break;
-	}
-	default: Unreachable();
-	}
+        // t == cleft && e == cright
+        Assert( t == cleft );
+        Assert( e == cright );
+        switch(k){
+        case LT:   // (ite (< x y) x y)
+        case LEQ: { // (ite (<= x y) x y)
+          Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
+          Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+          Debug("arith::mins") << n << "is a min =>"  << nLeqX << nLeqY << endl;
+          learned << nLeqX << nLeqY;
+          break;
+        }
+        case GT: // (ite (> x y) x y)
+        case GEQ: { // (ite (>= x y) x y)
+          Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
+          Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+          Debug("arith::mins") << n << "is a max =>"  << nGeqX << nGeqY << endl;
+          learned << nGeqX << nGeqY;
+          break;
+        }
+        default: Unreachable();
+        }
       }
     }
     // == 2-CONSTANTS ==
@@ -177,84 +186,15 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
       Debug("arith::mins") << n << " is a constant sandwich"  << nGeqMin << nLeqMax << endl;
       learned << nGeqMin << nLeqMax;
     }
-
-    // // binary OR of binary ANDs of EQUALities
-    // if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
-    //    n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
-    //    n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
-    //    (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
-    //    (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
-    //    (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
-    //    (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
-    //   // now we have (a = b && c = d) || (e = f && g = h)
-
-    //   Debug("diamonds") << "has form of a diamond!" << endl;
-
-    //   TNode
-    //     a = n[0][0][0], b = n[0][0][1],
-    //     c = n[0][1][0], d = n[0][1][1],
-    //     e = n[1][0][0], f = n[1][0][1],
-    //     g = n[1][1][0], h = n[1][1][1];
-
-    //   // test that one of {a, b} = one of {c, d}, and make "b" the
-    //   // shared node (i.e. put in the form (a = b && b = d))
-    //   // note we don't actually care about the shared ones, so the
-    //   // "swaps" below are one-sided, ignoring b and c
-    //   if(a == c) {
-    //     a = b;
-    //   } else if(a == d) {
-    //     a = b;
-    //     d = c;
-    //   } else if(b == c) {
-    //     // nothing to do
-    //   } else if(b == d) {
-    //     d = c;
-    //   } else {
-    //     // condition not satisfied
-    //     Debug("diamonds") << "+ A fails" << endl;
-    //     continue;
-    //   }
-
-    //   Debug("diamonds") << "+ A holds" << endl;
-
-    //   // same: one of {e, f} = one of {g, h}, and make "f" the
-    //   // shared node (i.e. put in the form (e = f && f = h))
-    //   if(e == g) {
-    //     e = f;
-    //   } else if(e == h) {
-    //     e = f;
-    //     h = g;
-    //   } else if(f == g) {
-    //     // nothing to do
-    //   } else if(f == h) {
-    //     h = g;
-    //   } else {
-    //     // condition not satisfied
-    //     Debug("diamonds") << "+ B fails" << endl;
-    //     continue;
-    //   }
-
-    //   Debug("diamonds") << "+ B holds" << endl;
-
-    //   // now we have (a = b && b = d) || (e = f && f = h)
-    //   // test that {a, d} == {e, h}
-    //   if( (a == e && d == h) ||
-    //       (a == h && d == e) ) {
-    //     // learn: n implies a == d
-    //     Debug("diamonds") << "+ C holds" << endl;
-    //     Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
-    //     Debug("diamonds") << "  ==> " << newEquality << endl;
-    //     learned << n.impNode(newEquality);
-    //   } else {
-    //     Debug("diamonds") << "+ C fails" << endl;
-    //   }
-    // }
   }
 }
 
 
 
-ArithVar TheoryArith::findBasicRow(ArithVar variable){
+ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
+  ArithVar bestBasic = ARITHVAR_SENTINEL;
+  unsigned rowLength = 0;
+
   for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
@@ -262,10 +202,14 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){
     ReducedRowVector* row_j = d_tableau.lookup(x_j);
 
     if(row_j->has(variable)){
-      return x_j;
+      if((bestBasic == ARITHVAR_SENTINEL) ||
+         (bestBasic != ARITHVAR_SENTINEL && row_j->size() < rowLength)){
+        bestBasic = x_j;
+        rowLength = row_j->size();
+      }
     }
   }
-  return ARITHVAR_SENTINEL;
+  return bestBasic;
 }
 
 
@@ -279,7 +223,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
     d_out->setIncomplete();
   }
 
-  if(isLeaf(n) || isStrictlyVarList){
+  if(Variable::isMember(n) || isStrictlyVarList){
     ++(d_statistics.d_statUserVariables);
     ArithVar varN = requestArithVar(n,false);
     setupInitialValue(varN);
@@ -322,6 +266,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
   d_activityMonitor.push_back(0);
 
   d_basicManager.init(varX,basic);
+  d_userVariables.init(varX, !basic);
   d_tableau.increaseSize();
 
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
@@ -710,3 +655,71 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
 void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
 
 }
+
+bool TheoryArith::entireStateIsConsistent(){
+  typedef std::vector<Node>::const_iterator VarIter;
+  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+    ArithVar var = asArithVar(*i);
+    if(!d_partialModel.assignmentIsConsistent(var)){
+      d_partialModel.printModel(var);
+      cerr << "Assignment is not consistent for " << var << *i << endl;
+      return false;
+    }
+  }
+  return true;
+}
+
+void TheoryArith::permanentlyRemoveVariable(ArithVar v){
+  //There are 3 cases
+  // 1) v is non-basic and is contained in a row
+  // 2) v is basic
+  // 3) v is non-basic and is not contained in a row
+  //  It appears that this can happen after other variables have been removed!
+  //  Tread carefullty with this one.
+
+  if(!d_basicManager.isMember(v)){
+    ArithVar basic = findShortestBasicRow(v);
+
+    if(basic == ARITHVAR_SENTINEL){
+      //Case 3) do nothing else.
+      //TODO think hard about if this is okay...
+      return;
+    }
+
+    AlwaysAssert(basic != ARITHVAR_SENTINEL);
+    d_tableau.pivot(basic, v);
+  }
+
+  Assert(d_basicManager.isMember(v));
+
+  d_tableau.ejectBasic(v);
+  //remove the row from the tableau
+  //TODO: It would be better to remove the row from the tableau
+  //and store this row in another data structure
+
+
+  Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl;
+  ++(d_statistics.d_permanentlyRemovedVariables);
+}
+
+void TheoryArith::presolve(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
+
+  typedef std::vector<Node>::const_iterator VarIter;
+  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+    Node variableNode = *i;
+    ArithVar var = asArithVar(variableNode);
+    if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){
+      //The user variable is unconstrained.
+      //Remove this variable permanently
+      permanentlyRemoveVariable(var);
+    }
+  }
+
+  //Assert(entireStateIsConsistent()); //Boy is this paranoid
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+
+  static int callCount = 0;
+  Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+  check(FULL_EFFORT);
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 5d39f626c..fa60b5fcf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/arith_rewriter.h"
@@ -39,6 +39,7 @@
 #include "util/stats.h"
 
 #include <vector>
+#include <map>
 #include <queue>
 
 namespace CVC4 {
@@ -63,6 +64,8 @@ private:
 
   std::vector<Node> d_variables;
 
+  std::map<ArithVar, ReducedRowVector*> d_removedRows;
+
   /**
    * Priority Queue of the basic variables that may be inconsistent.
    *
@@ -81,7 +84,8 @@ private:
    */
   ArithPartialModel d_partialModel;
 
-  ArithVarDenseSet d_basicManager;
+  ArithVarSet d_basicManager;
+  ArithVarSet d_userVariables;
   ActivityMonitor d_activityMonitor;
 
   /**
@@ -119,11 +123,7 @@ public:
 
   void shutdown(){ }
 
-  void presolve(){
-    static int callCount = 0;
-    Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
-    check(FULL_EFFORT);
-  }
+  void presolve();
 
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
@@ -148,15 +148,30 @@ private:
   void setupSlack(TNode left);
 
 
-
-
   /**
    * Handles the case splitting for check() for a new assertion.
    * returns true if their is a conflict.
    */
   bool assertionCases(TNode assertion);
 
-  ArithVar findBasicRow(ArithVar variable);
+  /**
+   * Returns the basic variable with the shorted row containg a non-basic variable.
+   * If no such row exists, return ARITHVAR_SENTINEL.
+   */
+  ArithVar findShortestBasicRow(ArithVar variable);
+
+  /**
+   * Debugging only routine!
+   * Returns true iff every variable is consistent in the partial model.
+   */
+  bool entireStateIsConsistent();
+
+  /**
+   * Permanently removes a variable from the problem.
+   * The caller guarentees the saftey of this removal!
+   */
+  void permanentlyRemoveVariable(ArithVar v);
+
 
   void asVectors(Polynomial& p,
                  std::vector<Rational>& coeffs,
@@ -171,6 +186,8 @@ private:
     IntStat d_statDisequalityConflicts;
     TimerStat d_staticLearningTimer;
 
+    IntStat d_permanentlyRemovedVariables;
+    TimerStat d_presolveTime;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
index 6e442ded9..e042e2320 100644
--- a/src/theory/arith/unate_propagator.cpp
+++ b/src/theory/arith/unate_propagator.cpp
@@ -47,6 +47,15 @@ bool ArithUnatePropagator::leftIsSetup(TNode left){
   return left.hasAttribute(PropagatorEqSet());
 }
 
+bool ArithUnatePropagator::hasAnyAtoms(TNode v){
+  Assert(!leftIsSetup(v)
+         || !v.getAttribute(PropagatorEqSet())->empty()
+         || !v.getAttribute(PropagatorLeqSet())->empty()
+         || !v.getAttribute(PropagatorGeqSet())->empty());
+
+  return leftIsSetup(v);
+}
+
 void ArithUnatePropagator::setupLefthand(TNode left){
   Assert(!leftIsSetup(left));
 
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index 1aab795cb..ca2135cf3 100644
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -77,6 +77,9 @@ public:
    */
   void addAtom(TNode atom);
 
+  /** Returns true if v has been added as a left hand side in an atom */
+  bool hasAnyAtoms(TNode v);
+
 private:
   /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
   void addImplication(TNode a, TNode b);