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

1 files changed, 8 insertions, 54 deletions

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);