diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-30 01:06:37 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-30 01:06:37 +0000 |
commit | d35d086268fa2a3d9b3c387157e4c54f1b967e0e (patch) | |
tree | 182fedc920cc2709f61901c4a07c577fcd1bde86 /src/theory/arith/simplex.cpp | |
parent | 4000100e143e364be9f292c38fa1158e3a516c55 (diff) |
Merged the branch sparse-tableau into trunk.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 235 |
1 files changed, 116 insertions, 119 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 6e73ca999..1a9c39984 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -209,36 +209,38 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& return Node::null(); } -set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){ - set<ArithVar> has; - for(ArithVarSet::iterator basicIter = tab.begin(); - basicIter != tab.end(); - ++basicIter){ - ArithVar basic = *basicIter; - ReducedRowVector& row = tab.lookup(basic); - - if(row.has(v)){ - has.insert(basic); - } - } - return has; -} - -set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){ - set<ArithVar> has; - Column::iterator basicIter = tab.beginColumn(v); - Column::iterator endIter = tab.endColumn(v); - for(; basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - has.insert(basic); - } - return has; -} - - +// set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){ +// set<ArithVar> has; +// for(ArithVarSet::const_iterator basicIter = tab.beginBasic(); +// basicIter != tab.endBasic(); +// ++basicIter){ +// ArithVar basic = *basicIter; +// ReducedRowVector& row = tab.lookup(basic); + +// if(row.has(v)){ +// has.insert(basic); +// } +// } +// return has; +// } + +// set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){ +// set<ArithVar> has; +// Column::iterator basicIter = tab.beginColumn(v); +// Column::iterator endIter = tab.endColumn(v); +// for(; basicIter != endIter; ++basicIter){ +// ArithVar basic = *basicIter; +// has.insert(basic); +// } +// return has; +// } + + +/* bool matchingSets(Tableau& tab, ArithVar v){ return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v); } +*/ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ Assert(!d_tableau.isBasic(x_i)); @@ -249,15 +251,17 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ << assignment_x_i << "|-> " << v << endl; DeltaRational diff = v - assignment_x_i; - Assert(matchingSets(d_tableau, x_i)); - Column::iterator basicIter = d_tableau.beginColumn(x_i); - Column::iterator endIter = d_tableau.endColumn(x_i); - for(; basicIter != endIter; ++basicIter){ - ArithVar x_j = *basicIter; - ReducedRowVector& row_j = d_tableau.lookup(x_j); + //Assert(matchingSets(d_tableau, x_i)); + Tableau::ColIterator basicIter = d_tableau.colIterator(x_i); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + Assert(entry.getColVar() == x_i); + + ArithVar x_j = entry.getRowVar(); + //ReducedRowVector& row_j = d_tableau.lookup(x_j); - Assert(row_j.has(x_i)); - const Rational& a_ji = row_j.lookup(x_i); + //const Rational& a_ji = row_j.lookup(x_i); + const Rational& a_ji = entry.getCoefficient(); const DeltaRational& assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); @@ -268,13 +272,34 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ d_partialModel.setAssignment(x_i, v); - Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_i)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_i)); + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i)); + double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i)); (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); - if(Debug.isOn("paranoid:check_tableau")){ - checkTableau(); + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } +} + +void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){ + Debug("arith::simplex:row") << "debugRowSimplex(" + << x_i << "|->" << x_j + << ")" << endl; + + for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + + ArithVar var = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + DeltaRational beta = d_partialModel.getAssignment(var); + Debug("arith::simplex:row") << var << beta << coeff; + if(d_partialModel.hasLowerBound(var)){ + Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")"; + } + if(d_partialModel.hasUpperBound(var)){ + Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")"; + } + Debug("arith::simplex:row") << endl; } + Debug("arith::simplex:row") << "end row"<< endl; } void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ @@ -282,32 +307,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); - if(Debug.isOn("arith::pivotAndUpdate")){ - Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; - ReducedRowVector& row_k = d_tableau.lookup(x_i); - for(ReducedRowVector::const_iterator varIter = row_k.begin(); - varIter != row_k.end(); - ++varIter){ - - ArithVar var = (*varIter).getArithVar(); - const Rational& coeff = (*varIter).getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(var); - Debug("arith::pivotAndUpdate") << var << beta << coeff; - if(d_partialModel.hasLowerBound(var)){ - Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")"; - } - if(d_partialModel.hasUpperBound(var)){ - Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var) - << ")"; - } - Debug("arith::pivotAndUpdate") << endl; - } - Debug("arith::pivotAndUpdate") << "end row"<< endl; - } + if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); } + + const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j); + Assert(!entry_ij.blank()); - ReducedRowVector& row_i = d_tableau.lookup(x_i); - const Rational& a_ij = row_i.lookup(x_j); + const Rational& a_ij = entry_ij.getCoefficient(); const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); @@ -322,16 +328,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR d_partialModel.setAssignment(x_j, tmp); - Assert(matchingSets(d_tableau, x_j)); - Column::iterator basicIter = d_tableau.beginColumn(x_j); - Column::iterator endIter = d_tableau.endColumn(x_j); - for(; basicIter != endIter; ++basicIter){ - ArithVar x_k = *basicIter; - ReducedRowVector& row_k = d_tableau.lookup(x_k); - - Assert(row_k.has(x_j)); + //Assert(matchingSets(d_tableau, x_j)); + for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + Assert(entry.getColVar() == x_j); + ArithVar x_k = entry.getRowVar(); if(x_k != x_i ){ - const Rational& a_kj = row_k.lookup(x_j); + const Rational& a_kj = entry.getCoefficient(); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); @@ -342,8 +345,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR // Pivots ++(d_statistics.d_statPivots); - Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j)); + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j)); + double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j)); (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference); d_tableau.pivot(x_i, x_j); @@ -367,14 +370,18 @@ ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& s } } -ArithVar SimplexDecisionProcedure::minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ +ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ Assert(x != ARITHVAR_SENTINEL); Assert(y != ARITHVAR_SENTINEL); Assert(!simp.d_tableau.isBasic(x)); Assert(!simp.d_tableau.isBasic(y)); - if(simp.d_tableau.getRowCount(x) > simp.d_tableau.getRowCount(y)){ - return y; - } else { + uint32_t xLen = simp.d_tableau.getColLength(x); + uint32_t yLen = simp.d_tableau.getColLength(y); + if( xLen > yLen){ + return y; + } else if( xLen== yLen ){ + return minVarOrder(simp,x,y); + }else{ return x; } } @@ -389,27 +396,22 @@ ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProc }else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){ return x; }else { - return minRowCount(simp, x, y); + return minColLength(simp, x, y); } } template <bool above, SimplexDecisionProcedure::PreferenceFunction pref> ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ - ReducedRowVector& row_i = d_tableau.lookup(x_i); - ArithVar slack = ARITHVAR_SENTINEL; - for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == x_i) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); int sgn = a_ij.sgn(); - if(( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) || - (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic))) { + if(isAcceptableSlack<above>(sgn, nonbasic)){ //If one of the above conditions is met, we have found an acceptable //nonbasic variable to pivot x_i with. We can now choose which one we //prefer the most. @@ -563,7 +565,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Assert(remainingIterations > 0); while(remainingIterations > 0){ - if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; @@ -612,8 +614,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ - ReducedRowVector& row_i = d_tableau.lookup(conflictVar); - NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getUpperConstraint(conflictVar); @@ -624,13 +624,13 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ nb << bound; - ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - - for(; nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); + for(; !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == conflictVar) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); Assert(a_ij != d_ZERO); int sgn = a_ij.sgn(); @@ -655,8 +655,6 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ } Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ - ReducedRowVector& row_i = d_tableau.lookup(conflictVar); - NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getLowerConstraint(conflictVar); @@ -667,12 +665,13 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ nb << bound; - ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - for(; nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); + for(; !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == conflictVar) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); int sgn = a_ij.sgn(); Assert(a_ij != d_ZERO); @@ -706,12 +705,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe Assert(d_tableau.isBasic(x)); DeltaRational sum(0); - ReducedRowVector& row = d_tableau.lookup(x); - for(ReducedRowVector::const_iterator i = row.begin(), end = row.end(); - i != end;++i){ - ArithVar nonbasic = (*i).getArithVar(); - if(nonbasic == row.basic()) continue; - const Rational& coeff = (*i).getCoefficient(); + for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){ + const TableauEntry& entry = (*i); + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x) continue; + const Rational& coeff = entry.getCoefficient(); const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); sum = sum + (assignment * coeff); @@ -726,21 +724,20 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe * checkTableau(); * } */ -void SimplexDecisionProcedure::checkTableau(){ - - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); ++basicIter){ +void SimplexDecisionProcedure::debugCheckTableau(){ + ArithVarSet::const_iterator basicIter = d_tableau.beginBasic(); + ArithVarSet::const_iterator endIter = d_tableau.endBasic(); + for(; basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; - ReducedRowVector& row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin(); - nonbasicIter != row_k.end(); - ++nonbasicIter){ - ArithVar nonbasic = (*nonbasicIter).getArithVar(); + Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic); + for(; !nonbasicIter.atEnd(); ++nonbasicIter){ + const TableauEntry& entry = *nonbasicIter; + ArithVar nonbasic = entry.getColVar(); if(basic == nonbasic) continue; - const Rational& coeff = (*nonbasicIter).getCoefficient(); + const Rational& coeff = entry.getCoefficient(); DeltaRational beta = d_partialModel.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl; sum = sum + (beta*coeff); |