From e322681d960a2fe26a968f6bb16d1d7b10b5215f Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 23 Mar 2012 23:06:29 +0000 Subject: [PATCH] Removed the variableRemovalEnabled option and d_removedRows from TheoryArith. This had been disabled for several months. --- src/theory/arith/theory_arith.cpp | 94 +------------------------------ src/theory/arith/theory_arith.h | 14 ----- src/util/options.cpp | 9 --- src/util/options.h | 3 - 4 files changed, 3 insertions(+), 117 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) <variableRemovalEnabled){ - typedef std::vector::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 @@ -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 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 175b7f228..d3426e152 100644 --- 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 cdcefa14f..4bf8b5b75 100644 --- 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; -- 2.30.2