diff options
author | Tim King <taking@cs.nyu.edu> | 2012-03-23 23:06:29 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-03-23 23:06:29 +0000 |
commit | e322681d960a2fe26a968f6bb16d1d7b10b5215f (patch) | |
tree | 75460141ed4376241f178221de1a7bd56187dea9 /src/theory/arith/theory_arith.cpp | |
parent | 1a99b24c49f9b865a70fa626efcb96571499917e (diff) |
Removed the variableRemovalEnabled option and d_removedRows from TheoryArith. This had been disabled for several months.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 94 |
1 files changed, 3 insertions, 91 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(); } |