diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-22 01:13:56 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-22 01:13:56 +0000 |
commit | c40d5678a4bbd73bde711149004206e37176661b (patch) | |
tree | 8df1349d7568768e7e8f9f58b2361884dc9fd830 /src/theory/arith/tableau.cpp | |
parent | a101b2e309dd2818a85c954e45af586e530e289a (diff) |
- Adds column based iterators.
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index d318a70e6..ebf7dbee8 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -41,7 +41,7 @@ void Tableau::addRow(ArithVar basicVar, //The new basic variable cannot already be a basic variable Assert(!d_basicVariables.isMember(basicVar)); d_basicVariables.add(basicVar); - ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount); + ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix); d_rowsTable[basicVar] = row_current; //A variable in the row may have been made non-basic already. @@ -90,17 +90,22 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ row_s->pivot(x_s); - for(ArithVarSet::iterator basicIter = begin(), endIter = end(); - basicIter != endIter; ++basicIter){ + ArithVarSet::VarList copy(getColumn(x_s).getList()); + vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end(); + + for(; basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; if(basic == x_s) continue; ReducedRowVector& row_k = lookup(basic); - if(row_k.has(x_s)){ - row_k.substitute(*row_s); - } + Assert(row_k.has(x_s)); + + row_k.substitute(*row_s); } + Assert(getColumn(x_s).size() == 1); + Assert(getRowCount(x_s) == 1); } + void Tableau::printTableau(){ Debug("tableau") << "Tableau::d_activeRows" << endl; |