diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-17 17:46:31 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-17 17:46:31 +0000 |
commit | 907850f58916c4a6890156a08301a68b5be43fcb (patch) | |
tree | 251815ce8fc9cc3df1520708894417715d168268 /src/theory/arith/simplex.cpp | |
parent | 0b6743798125317a4e88366591028691fe7170f8 (diff) |
Row ejection is now completely disabled. Another commit cleaning this one up will follow shortly.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 73 |
1 files changed, 45 insertions, 28 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index f7e3c112c..9e3ba726a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -60,6 +60,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ } +/* void SimplexDecisionProcedure::ejectInactiveVariables(){ return; //die die die @@ -75,7 +76,9 @@ void SimplexDecisionProcedure::ejectInactiveVariables(){ } } } +*/ +/* void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ ++(d_statistics.d_statUnEjections); @@ -85,7 +88,9 @@ void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ DeltaRational assignment = computeRowValue(x, false); d_partialModel.setAssignment(x,safeAssignment,assignment); } +*/ +/* bool SimplexDecisionProcedure::shouldEject(ArithVar var){ if(d_partialModel.hasEitherBound(var)){ return false; @@ -98,14 +103,17 @@ bool SimplexDecisionProcedure::shouldEject(ArithVar var){ } return false; } +*/ /* procedure AssertLower( x_i >= c_i ) */ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; + /* if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } + */ if(d_partialModel.belowLowerBound(x_i, c_i, false)){ return false; //sat @@ -138,9 +146,11 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + /* if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } + */ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i return false; //sat @@ -176,9 +186,11 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; + /* if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } + */ // u_i <= c_i <= l_i // This can happen if both c_i <= x_i and x_i <= c_i are in the system. @@ -234,10 +246,10 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; - ReducedRowVector* row_j = d_tableau.lookup(x_j); + ReducedRowVector& row_j = d_tableau.lookup(x_j); - if(row_j->has(x_i)){ - const Rational& a_ji = row_j->lookup(x_i); + if(row_j.has(x_i)){ + const Rational& a_ji = row_j.lookup(x_i); const DeltaRational& assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); @@ -263,9 +275,9 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR if(Debug.isOn("arith::pivotAndUpdate")){ Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; - ReducedRowVector* row_k = d_tableau.lookup(x_i); - for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero(); - varIter != row_k->endNonZero(); + ReducedRowVector& row_k = d_tableau.lookup(x_i); + for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero(); + varIter != row_k.endNonZero(); ++varIter){ ArithVar var = varIter->first; @@ -285,8 +297,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR } - ReducedRowVector* row_i = d_tableau.lookup(x_i); - const Rational& a_ij = row_i->lookup(x_j); + ReducedRowVector& row_i = d_tableau.lookup(x_i); + const Rational& a_ij = row_i.lookup(x_j); const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); @@ -300,14 +312,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; d_partialModel.setAssignment(x_j, tmp); - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); - ++basicIter){ + ArithVarSet::iterator basicIter = d_tableau.begin(), end = d_tableau.end(); + for(; basicIter != end; ++basicIter){ ArithVar x_k = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(x_k); + ReducedRowVector& row_k = d_tableau.lookup(x_k); - if(x_k != x_i && row_k->has(x_j)){ - const Rational& a_kj = row_k->lookup(x_j); + if(x_k != x_i && row_k.has(x_j)){ + const Rational& a_kj = row_k.lookup(x_j); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); @@ -384,12 +395,12 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ template <bool above> ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ - ReducedRowVector* row_i = d_tableau.lookup(x_i); + ReducedRowVector& row_i = d_tableau.lookup(x_i); ArithVar slack = ARITHVAR_SENTINEL; uint32_t numRows = std::numeric_limits<uint32_t>::max(); - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == x_i) continue; @@ -541,7 +552,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Debug("arith") << "updateInconsistentVars" << endl; uint32_t iteratationNum = 0; - static const int EJECT_FREQUENCY = 10; + //static const int EJECT_FREQUENCY = 10; while(!d_pivotStage || iteratationNum <= d_numVariables){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } @@ -554,8 +565,10 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ } ++iteratationNum; + /* if(iteratationNum % EJECT_FREQUENCY == 0) ejectInactiveVariables(); + */ DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; @@ -605,7 +618,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector& row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getUpperConstraint(conflictVar); @@ -617,8 +630,10 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ nb << bound; - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); - nbi != end; ++nbi){ + typedef ReducedRowVector::NonZeroIterator RowIterator; + RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + + for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == conflictVar) continue; @@ -645,7 +660,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ } Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector& row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getLowerConstraint(conflictVar); @@ -656,7 +671,9 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ << " " << bound << endl; nb << bound; - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ + typedef ReducedRowVector::NonZeroIterator RowIterator; + RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == conflictVar) continue; @@ -691,11 +708,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe Assert(d_basicManager.isMember(x)); DeltaRational sum = d_constants.d_ZERO_DELTA; - ReducedRowVector* row = d_tableau.lookup(x); - for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero(); + ReducedRowVector& row = d_tableau.lookup(x); + for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero(); i != end;++i){ ArithVar nonbasic = getArithVar(*i); - if(nonbasic == row->basic()) continue; + if(nonbasic == row.basic()) continue; const Rational& coeff = getCoefficient(*i); const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); @@ -732,11 +749,11 @@ void SimplexDecisionProcedure::checkTableau(){ for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar basic = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(basic); + ReducedRowVector& row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero(); - nonbasicIter != row_k->endNonZero(); + for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero(); + nonbasicIter != row_k.endNonZero(); ++nonbasicIter){ ArithVar nonbasic = nonbasicIter->first; if(basic == nonbasic) continue; |