diff options
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; |