Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau.

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,