diff options
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 41 |
1 files changed, 18 insertions, 23 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index df80c1118..aaeadb629 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -48,7 +48,6 @@ Row::Row(ArithVar basic, Assert(d_coeffs[var_i] != Rational(0,1)); } } - void Row::subsitute(Row& row_s){ ArithVar x_s = row_s.basicVar(); @@ -115,7 +114,7 @@ void Tableau::addRow(ArithVar basicVar, Assert(!isActiveBasicVariable(basicVar)); d_activeBasicVars.insert(basicVar); Row* row_current = new Row(basicVar,coeffs,variables); - d_activeRows[basicVar] = row_current; + 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 @@ -143,23 +142,22 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isBasic(x_r)); Assert(!d_basicManager.isBasic(x_s)); - RowsTable::iterator ptrRow_r = d_activeRows.find(x_r); - Assert(ptrRow_r != d_activeRows.end()); - - Row* row_s = (*ptrRow_r).second; - + Row* row_s = lookup(x_r); Assert(row_s->has(x_s)); - row_s->pivot(x_s); - d_activeRows.erase(ptrRow_r); + //Swap x_r and x_s in d_activeRows + d_rowsTable[x_s] = row_s; + d_rowsTable[x_r] = NULL; + d_activeBasicVars.erase(x_r); d_basicManager.makeNonbasic(x_r); - d_activeRows.insert(std::make_pair(x_s,row_s)); d_activeBasicVars.insert(x_s); d_basicManager.makeBasic(x_s); - for(VarSet::iterator basicIter = begin(), endIter = end(); + row_s->pivot(x_s); + + for(ArithVarSet::iterator basicIter = begin(), endIter = end(); basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; Row* row_k = lookup(basic); @@ -169,19 +167,16 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ } } } - void Tableau::printTableau(){ - for(VarSet::iterator basicIter = begin(), endIter = end(); - basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - Row* row_k = lookup(basic); - row_k->printRow(); - } - for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter = d_inactiveRows.end(); - basicIter != endIter; ++basicIter){ - ArithVar basic = (*basicIter).first; - Row* row_k = lookupEjected(basic); - row_k->printRow(); + Debug("tableau") << "Tableau::d_activeRows" << endl; + + typedef RowsTable::iterator table_iter; + for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end(); + rowIter != end; ++rowIter){ + Row* row_k = *rowIter; + if(row_k != NULL){ + row_k->printRow(); + } } } |