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.h | |
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.h')
-rw-r--r-- | src/theory/arith/tableau.h | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 27aa1305c..6fe245285 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -63,8 +63,13 @@ public: d_rowCount(), d_columnMatrix() {} + + /** Copy constructor. */ + Tableau(const Tableau& tab); ~Tableau(); + Tableau& operator=(const Tableau& tab); + size_t getNumRows() const { return d_basicVariables.size(); } @@ -116,7 +121,6 @@ public: return *(d_rowsTable[var]); } -public: uint32_t getRowCount(ArithVar x){ Assert(x < d_rowCount.size()); AlwaysAssert(d_rowCount[x] == getColumn(x).size()); @@ -150,6 +154,14 @@ public: void printTableau(); ReducedRowVector* removeRow(ArithVar basic); + + +private: + /** Copies the datastructures in tab to this.*/ + void internalCopy(const Tableau& tab); + + /** Clears the structures in the tableau. */ + void clear(); }; }; /* namespace arith */ |