Removed the variableRemovalEnabled option and d_removedRows from TheoryArith. This had been disabled for several months.

1 files changed, 0 insertions, 14 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ec2df3e17..4f111d350 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -170,13 +170,6 @@ private:
   Comparison mkIntegerEqualityFromAssignment(ArithVar v);
 
   /**
-   * If ArithVar v maps to the node n in d_removednode,
-   * then n = (= asNode(v) rhs) where rhs is a term that
-   * can be used to determine the value of n using getValue().
-   */
-  std::map<ArithVar, Node> d_removedRows;
-
-  /**
    * List of all of the inequalities asserted in the current context.
    */
   context::CDHashSet<Node, NodeHashFunction> d_diseq;
@@ -424,12 +417,6 @@ private:
    */
   bool entireStateIsConsistent();
 
-  /**
-   * Permanently removes a variable from the problem.
-   * The caller guarentees the saftey of this removal!
-   */
-  void permanentlyRemoveVariable(ArithVar v);
-
   bool isImpliedUpperBound(ArithVar var, Node exp);
   bool isImpliedLowerBound(ArithVar var, Node exp);
 
@@ -456,7 +443,6 @@ private:
     TimerStat d_simplifyTimer;
     TimerStat d_staticLearningTimer;
 
-    IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
     IntStat d_externalBranchAndBounds;