diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-28 21:46:44 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-28 21:46:44 +0000 |
commit | 50622574025f55417be020f30a4787714977ddd1 (patch) | |
tree | cd5a5e944216d354a4745e223aed64d3307ffde6 /src/theory/arith/tableau.cpp | |
parent | d2ff1974a7cd87d841e1bcaeb0d93665f70d9259 (diff) |
The Row implementation has no been replaced by RowVector and ReducedRowVector. A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable. The Tableau is now a collection of ReduceRowVector's. A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 110 |
1 files changed, 17 insertions, 93 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 2490ed51b..c22c21a46 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -24,85 +24,6 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -Row::Row(ArithVar basic, - const std::vector< Rational >& coefficients, - const std::vector< ArithVar >& variables): - d_x_i(basic), - d_coeffs(){ - - Assert(coefficients.size() == variables.size() ); - - std::vector<Rational>::const_iterator coeffIter = coefficients.begin(); - std::vector<Rational>::const_iterator coeffEnd = coefficients.end(); - std::vector<ArithVar>::const_iterator varIter = variables.begin(); - - for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){ - const Rational& coeff = *coeffIter; - ArithVar var_i = *varIter; - - Assert(var_i != d_x_i); - Assert(!has(var_i)); - Assert(coeff != Rational(0,1)); - - d_coeffs[var_i] = coeff; - Assert(d_coeffs[var_i] != Rational(0,1)); - } -} -void Row::substitute(Row& row_s){ - ArithVar x_s = row_s.basicVar(); - - Assert(has(x_s)); - Assert(x_s != d_x_i); - - Rational zero(0,1); - - Rational a_rs = lookup(x_s); - Assert(a_rs != zero); - d_coeffs.erase(x_s); - - for(iterator iter = row_s.begin(), iter_end = row_s.end(); - iter != iter_end; ++iter){ - ArithVar x_j = iter->first; - Rational a_sj = iter->second; - a_sj *= a_rs; - CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j); - - if(coeff_iter != d_coeffs.end()){ - coeff_iter->second += a_sj; - if(coeff_iter->second == zero){ - d_coeffs.erase(coeff_iter); - } - }else{ - d_coeffs.insert(std::make_pair(x_j,a_sj)); - } - } -} - -void Row::pivot(ArithVar x_j){ - Rational negInverseA_rs = -(lookup(x_j).inverse()); - d_coeffs[d_x_i] = Rational(Integer(-1)); - d_coeffs.erase(x_j); - - d_x_i = x_j; - - for(iterator nonbasicIter = begin(), nonbasicIter_end = end(); - nonbasicIter != nonbasicIter_end; ++nonbasicIter){ - nonbasicIter->second *= negInverseA_rs; - } - -} - -void Row::printRow(){ - Debug("tableau") << d_x_i << " "; - for(iterator nonbasicIter = d_coeffs.begin(); - nonbasicIter != d_coeffs.end(); - ++nonbasicIter){ - ArithVar nb = nonbasicIter->first; - Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}"; - } - Debug("tableau") << std::endl; -} - void Tableau::addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables){ @@ -113,15 +34,15 @@ void Tableau::addRow(ArithVar basicVar, //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(basicVar)); d_activeBasicVars.insert(basicVar); - Row* row_current = new Row(basicVar,coeffs,variables); + ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs); d_rowsTable[basicVar] = row_current; //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable - std::vector<Rational>::const_iterator coeffsIter = coeffs.begin(); - std::vector<Rational>::const_iterator coeffsEnd = coeffs.end(); + vector<Rational>::const_iterator coeffsIter = coeffs.begin(); + vector<Rational>::const_iterator coeffsEnd = coeffs.end(); - std::vector<ArithVar>::const_iterator varsIter = variables.begin(); + vector<ArithVar>::const_iterator varsIter = variables.begin(); for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){ ArithVar var = *varsIter; @@ -132,7 +53,7 @@ void Tableau::addRow(ArithVar basicVar, } Assert(isActiveBasicVariable(var)); - Row* row_var = lookup(var); + ReducedRowVector* row_var = lookup(var); row_current->substitute(*row_var); } } @@ -142,7 +63,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isMember(x_r)); Assert(!d_basicManager.isMember(x_s)); - Row* row_s = lookup(x_r); + ReducedRowVector* row_s = lookup(x_r); Assert(row_s->has(x_s)); //Swap x_r and x_s in d_activeRows @@ -160,7 +81,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ for(ArithVarSet::iterator basicIter = begin(), endIter = end(); basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; - Row* row_k = lookup(basic); + if(basic == x_s) continue; + + ReducedRowVector* row_k = lookup(basic); if(row_k->has(x_s)){ d_activityMonitor[basic] += 30; row_k->substitute(*row_s); @@ -173,7 +96,7 @@ void Tableau::printTableau(){ typedef RowsTable::iterator table_iter; for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end(); rowIter != end; ++rowIter){ - Row* row_k = *rowIter; + ReducedRowVector* row_k = *rowIter; if(row_k != NULL){ row_k->printRow(); } @@ -181,18 +104,19 @@ void Tableau::printTableau(){ } -void Tableau::updateRow(Row* row){ - for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ +void Tableau::updateRow(ReducedRowVector* row){ + ArithVar basic = row->basic(); + for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){ ArithVar var = i->first; ++i; - if(d_basicManager.isMember(var)){ - Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); + if(var != basic && d_basicManager.isMember(var)){ + ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); row->substitute(*row_var); - i = row->begin(); - endIter = row->end(); + i = row->beginNonZero(); + endIter = row->endNonZero(); } } } |