Removed the variableRemovalEnabled option and d_removedRows from TheoryArith. This...

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 590a9f1cfe84229c7fbdcae9dfa9121a64308553..85461af329a9066eb5ca99c29aeefbc8554bf627 100644 (file)
--- 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 ec2df3e175c6e0cdc82dcbd856c51d844994e517..4f111d35096c688eb8717f33251af4bf996afe6c 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -169,13 +169,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.
    */
@@ -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;

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 175b7f228cacd9b3a21fb89df4da2018989b52a4..d3426e1526ed23ba022062a716b32e21bd1c1fc5 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -96,7 +96,6 @@ Options::Options() :
   replayFilename(""),
   replayStream(NULL),
   replayLog(NULL),
-  variableRemovalEnabled(false),
   arithPropagation(true),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
@@ -178,7 +177,6 @@ Additional CVC4 options:\n\
    --random-seed=S        sets the random seed for the sat solver\n\
    --restart-int-base=I   sets the base restart interval for the sat solver (I=25 by default)\n\
    --restart-int-inc=F    sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\
-   --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
@@ -189,7 +187,6 @@ Additional CVC4 options:\n\
 ";
 
 
-#warning "Change CL options as --disable-variable-removal cannot do anything currently."
 
 static const string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -352,7 +349,6 @@ enum OptionValue {
   RANDOM_SEED,
   SAT_RESTART_FIRST,
   SAT_RESTART_INC,
-  ARITHMETIC_VARIABLE_REMOVAL,
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
@@ -443,7 +439,6 @@ static struct option cmdlineOptions[] = {
   { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
   { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
   { "print-winner", no_argument     , NULL, PRINT_WINNER  },
-  { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
   { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
@@ -789,10 +784,6 @@ throw(OptionException) {
 #endif /* CVC4_REPLAY */
       break;
 
-    case ARITHMETIC_VARIABLE_REMOVAL:
-      variableRemovalEnabled = false;
-      break;
-
     case ARITHMETIC_PROPAGATION:
       arithPropagation = false;
       break;

diff --git a/src/util/options.h b/src/util/options.h
index cdcefa14fac6830675de2efc94d3014af8adb99a..4bf8b5b75e222ffd91c4e3be87358df91bd2e0d9 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -178,9 +178,6 @@ struct CVC4_PUBLIC Options {
   /** Log to write replay instructions to; NULL if not logging. */
   std::ostream* replayLog;
 
-  /** Determines whether arithmetic will try to variables. */
-  bool variableRemovalEnabled;
-
   /** Turn on and of arithmetic propagation. */
   bool arithPropagation;