Merged the tableau-copy branch into trunk. This adds a copy constructor and operator...

diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index ff75b373a0c58306cdd2bb49b6b49c34f77748a5..08bc905e0993a0ab4acdcd5749f808eb7e69d091 100644 (file)
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -63,6 +63,11 @@ public:
     return d_posVector.size();
   }
 
+  void clear(){
+    d_list.clear();
+    d_posVector.clear();
+  }
+
   void increaseSize(ArithVar max){
     Assert(max >= allocated());
     d_posVector.resize(max+1, ARITHVAR_SENTINEL);

diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 090938f283200be2e2b9937a49fce1cbd1d3d96a..9159d3d6fa4a5eb42677482f76283792cb319dfc 100644 (file)
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -304,3 +304,13 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
 */
 }
 
+void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{
+  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
+    ArithVar var = (*i).getArithVar();
+    const Rational& q = (*i).getCoefficient();
+    if(var != basic()){
+      variables.push_back(var);
+      coefficients.push_back(q);
+    }
+  }
+}

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 0fdfd7f0c3d88795fbbb1764416ddd8dceadac24..45412ad3e10afad9571c28da5d340299e1919be6 100644 (file)
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -86,9 +86,11 @@ public:
                    const std::vector< Rational >& coefficients,
                    std::vector<uint32_t>& count,
                    std::vector<ArithVarSet>& columnMatrix);
-
   ~ReducedRowVector();
 
+  void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,
+                                               std::vector< Rational >& coefficients) const;
+
   /** Returns the basic variable.*/
   ArithVar basic() const{
     Assert(basicIsSet());

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index a857653037568b2f0d0c3f1f53b607c60b87dc42..9769c628d8d9294e0a3931cde43bc852a901000a 100644 (file)
--- 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,

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 27aa1305ca49fb8aabfcff773dfa841571cb8ebb..6fe24528520cc984a5fd44187c94a8347b578178 100644 (file)
--- 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  */

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2100e0b385c6b63d298708afa7d8d6fda05e1734..3899e5e800c99e768a900cd985b0ff509df593d1 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -652,6 +652,10 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
 
 }
 
+void TheoryArith::notifyRestart(){
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+}
+
 bool TheoryArith::entireStateIsConsistent(){
   typedef std::vector<Node>::const_iterator VarIter;
   for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
@@ -727,5 +731,6 @@ void TheoryArith::presolve(){
 
   static int callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+
   check(FULL_EFFORT);
 }

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index dc841170b4d7f662346bfd6387d614c6416989df..fb39eac09f14345efac0e4af6abaee881bfa72cc 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -71,15 +71,6 @@ private:
    */
   std::map<ArithVar, Node> d_removedRows;
 
-  /**
-   * Priority Queue of the basic variables that may be inconsistent.
-   *
-   * This is required to contain at least 1 instance of every inconsistent
-   * basic variable. This is only required to be a superset though so its
-   * contents must be checked to still be basic and inconsistent.
-   */
-  std::priority_queue<ArithVar> d_possiblyInconsistent;
-
   /** Stores system wide constants to avoid unnessecary reconstruction. */
   ArithConstants d_constants;
 
@@ -157,7 +148,7 @@ public:
   void shutdown(){ }
 
   void presolve();
-
+  void notifyRestart();
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }