diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-03 16:34:48 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-03 16:34:48 +0000 |
commit | 3c8309cbf3f6549d9cc54fe45ccb5bb32a106d8e (patch) | |
tree | 8383e8e393ec7ec04c3cb1da02102e8876cc1adb /src/theory/arith/tableau.cpp | |
parent | 7cd7c850304caa12827c0deab1752293655d1248 (diff) |
Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau.
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 65 |
1 files changed, 64 insertions, 1 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index a85765303..9769c628d 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -20,18 +20,81 @@ #include "theory/arith/tableau.h" +using namespace std; using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -using namespace std; + +Tableau::Tableau(const Tableau& tab){ + internalCopy(tab); +} + +void Tableau::internalCopy(const Tableau& tab){ + uint32_t N = tab.d_rowsTable.size(); + + Debug("tableau::copy") << "tableau copy "<< N << endl; + + if(N > 1){ + d_columnMatrix.insert(d_columnMatrix.end(), N, ArithVarSet()); + d_rowsTable.insert(d_rowsTable.end(), N, NULL); + d_basicVariables.increaseSize(N-1); + + Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated()); + + d_rowCount.insert(d_rowCount.end(), N, 0); + } + + ColumnMatrix::iterator i_colIter = d_columnMatrix.begin(); + ColumnMatrix::iterator end_colIter = d_columnMatrix.end(); + for(; i_colIter != end_colIter; ++i_colIter){ + Column& col = *i_colIter; + col.increaseSize(d_columnMatrix.size()); + } + + ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin(); + ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end(); + for(; i_basicIter != i_basicEnd; ++i_basicIter){ + ArithVar basicVar = *i_basicIter; + const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar]; + + Assert(otherRow != NULL); + + std::vector< ArithVar > variables; + std::vector< Rational > coefficients; + otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients); + + ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix); + + Debug("tableau::copy") << "copying " << basicVar << endl; + copy->printRow(); + + d_basicVariables.add(basicVar); + d_rowsTable[basicVar] = copy; + } +} + +Tableau& Tableau::operator=(const Tableau& other){ + clear(); + internalCopy(other); + return (*this); +} Tableau::~Tableau(){ + clear(); +} + +void Tableau::clear(){ while(!d_basicVariables.empty()){ ArithVar curr = *(d_basicVariables.begin()); ReducedRowVector* vec = removeRow(curr); delete vec; } + + d_rowsTable.clear(); + d_basicVariables.clear(); + d_rowCount.clear(); + d_columnMatrix.clear(); } void Tableau::addRow(ArithVar basicVar, |