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, 3 insertions, 3 deletions

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