1 files changed, 27 insertions, 10 deletions
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();
   };