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

2 files changed, 3 insertions, 105 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 590a9f1cf..85461af32 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -93,7 +93,6 @@ TheoryArith::Statistics::Statistics():
   d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
   d_simplifyTimer("theory::arith::simplifyTimer"),
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
-  d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
   d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
   d_initialTableauSize("theory::arith::initialTableauSize", 0),
@@ -114,7 +113,6 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_simplifyTimer);
   StatisticsRegistry::registerStat(&d_staticLearningTimer);
 
-  StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
   StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
@@ -140,7 +138,6 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_simplifyTimer);
   StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
 
-  StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
   StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
@@ -1215,9 +1212,9 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   case kind::PLUS: { // 2+ args
     DeltaRational value(0);
     for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
+          iend = n.end();
+        i != iend;
+        ++i) {
       value = value + getDeltaValue(*i);
     }
     return value;
@@ -1257,14 +1254,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   default:
   {
     ArithVar var = d_arithvarNodeMap.asArithVar(n);
-
-    if(d_removedRows.find(var) != d_removedRows.end()){
-      Node eq = d_removedRows.find(var)->second;
-      Assert(n == eq[0]);
-      Node rhs = eq[1];
-      return getDeltaValue(rhs);
-    }
-
     return d_partialModel.getAssignment(var);
   }
   }
@@ -1277,13 +1266,6 @@ Node TheoryArith::getValue(TNode n) {
   case kind::VARIABLE: {
     ArithVar var = d_arithvarNodeMap.asArithVar(n);
 
-    if(d_removedRows.find(var) != d_removedRows.end()){
-      Node eq = d_removedRows.find(var)->second;
-      Assert(n == eq[0]);
-      Node rhs = eq[1];
-      return getValue(rhs);
-    }
-
     DeltaRational drat = d_partialModel.getAssignment(var);
     const Rational& delta = d_partialModel.getDelta();
     Debug("getValue") << n << " " << drat << " " << delta << endl;
@@ -1401,79 +1383,9 @@ bool TheoryArith::entireStateIsConsistent(){
   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.
-
-  Assert(Options::current()->variableRemovalEnabled);
-
-  bool noRow = false;
-
-  if(!d_tableau.isBasic(v)){
-    ArithVar basic = findShortestBasicRow(v);
-
-    if(basic == ARITHVAR_SENTINEL){
-      noRow = true;
-    }else{
-      Assert(basic != ARITHVAR_SENTINEL);
-      d_tableau.pivot(basic, v);
-    }
-  }
-
-  if(d_tableau.isBasic(v)){
-    Assert(!noRow);
-
-    //remove the row from the tableau
-    Node eq =  d_tableau.rowAsEquality(v, d_arithvarNodeMap.getArithVarToNodeMap());
-    d_tableau.removeRow(v);
-
-    if(Debug.isOn("tableau")) d_tableau.printTableau();
-    Debug("arith::permanentlyRemoveVariable") << eq << endl;
-
-    Assert(d_tableau.getRowLength(v) == 0);
-    Assert(d_tableau.getColLength(v) == 0);
-    Assert(d_removedRows.find(v) ==  d_removedRows.end());
-    d_removedRows[v] = eq;
-  }
-
-  Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " << v
-                                            << ":" << d_arithvarNodeMap.asNode(v) <<endl;
-  ++(d_statistics.d_permanentlyRemovedVariables);
-}
-
 void TheoryArith::presolve(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
 
-  /* BREADCRUMB : Turn this on for QF_LRA/QF_RDL problems.
-   *
-   * The big problem for adding things back is that if they are readded they may
-   * need to be assigned an initial value at ALL context values.
-   * This is unsupported with our current datastructures.
-   *
-   * A better solution is to KNOW when the permantent removal is safe.
-   * This is true for single query QF_LRA/QF_RDL problems.
-   * Maybe a mechanism to ask "the sharing manager"
-   * if this variable/row can be used in sharing?
-   */
-  if(Options::current()->variableRemovalEnabled){
-    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 = d_arithvarNodeMap.asArithVar(variableNode);
-      if(!isSlackVariable(var) &&
-         !d_atomDatabase.hasAnyAtoms(variableNode) &&
-         !variableNode.getType().isInteger()){
-	//The user variable is unconstrained.
-	//Remove this variable permanently
-	permanentlyRemoveVariable(var);
-      }
-    }
-  }
-
   d_statistics.d_initialTableauSize.setData(d_tableau.size());
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
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;