- Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The difference is that set.isMember(x) for an ArithVar x s.t. x > set.allocated() returns false for PermissiveBackArithVarSet and is an assertion failure for ArithVarSet. This cuts down on the memory usage of the ColumnMatrix slightly.

6 files changed, 45 insertions, 26 deletions

diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 08bc905e0..89b1c9507 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -32,11 +32,20 @@ namespace arith {
  * This is an abstraction of a set of ArithVars.
  * This class is designed to provide constant time insertion, deletion, and element_of
  * and fast iteration.
- * The cost of doing this is that it takes O(M) where M is the total number
- * of ArithVars in memory.
+ *
+ * ArithVarSets come in 2 varieties ArithVarSet, and PermissiveBackArithVarSet.
+ * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars
+ * that are greater than allocated(). Asking isMember() of such an ArithVar
+ * is an assertion failure. The cost of doing this is that it takes O(M)
+ * where M is the total number of ArithVars in memory.
+ *
+ * PermissiveBackArithVarSet means that all ArithVars are implicitly not in the set,
+ * and any ArithVar past the end of d_posVector is not in the set.
+ * A permissiveBack allows for less memory to be consumed on average.
+ *
  */
-
-class ArithVarSet {
+template <bool permissiveBack>
+class ArithVarSetImpl {
 public:
   typedef std::vector<ArithVar> VarList;
 private:
@@ -50,7 +59,7 @@ private:
 public:
   typedef VarList::const_iterator iterator;
 
-  ArithVarSet() :  d_list(), d_posVector() {}
+  ArithVarSetImpl() :  d_list(), d_posVector() {}
 
   size_t size() const {
     return d_list.size();
@@ -78,13 +87,17 @@ public:
   }
 
   bool isMember(ArithVar x) const{
-    Assert(x <  allocated());
-    return d_posVector[x] != ARITHVAR_SENTINEL;
+    if(permissiveBack && x >=  allocated()){
+      return false;
+    }else{
+      Assert(x <  allocated());
+      return d_posVector[x] != ARITHVAR_SENTINEL;
+    }
   }
 
   /** Invalidates iterators */
   void init(ArithVar x, bool val) {
-    Assert(x >= size());
+    Assert(x >= allocated());
     increaseSize(x);
     if(val){
       add(x);
@@ -94,6 +107,9 @@ public:
   /** Invalidates iterators */
   void add(ArithVar x){
     Assert(!isMember(x));
+    if(permissiveBack && x >=  allocated()){
+      increaseSize(x);
+    }
     d_posVector[x] = size();
     d_list.push_back(x);
   }
@@ -139,6 +155,9 @@ public:
   }
 };
 
+typedef ArithVarSetImpl<false> ArithVarSet;
+typedef ArithVarSetImpl<true> PermissiveBackArithVarSet;
+
 }; /* namespace arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 9159d3d6f..8edfb8612 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -182,7 +182,7 @@ ReducedRowVector::ReducedRowVector(ArithVar basic,
                                    const std::vector<ArithVar>& variables,
                                    const std::vector<Rational>& coefficients,
                                    std::vector<uint32_t>& counts,
-                                   std::vector<ArithVarSet>& cm):
+                                   std::vector<PermissiveBackArithVarSet>& cm):
   d_basic(basic), d_rowCount(counts),  d_columnMatrix(cm)
 {
   zip(variables, coefficients, d_entries);
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 45412ad3e..5fd471700 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -76,7 +76,7 @@ private:
   ArithVarContainsSet d_contains;
 
   std::vector<uint32_t>& d_rowCount;
-  std::vector<ArithVarSet>& d_columnMatrix;
+  std::vector<PermissiveBackArithVarSet>& d_columnMatrix;
 
 
 public:
@@ -85,7 +85,7 @@ public:
                    const std::vector< ArithVar >& variables,
                    const std::vector< Rational >& coefficients,
                    std::vector<uint32_t>& count,
-                   std::vector<ArithVarSet>& columnMatrix);
+                   std::vector< PermissiveBackArithVarSet >& columnMatrix);
   ~ReducedRowVector();
 
   void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 7e83e1b9e..0e2c3797e 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -198,8 +198,8 @@ set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
 
 set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
   set<ArithVar> has;
-  ArithVarSet::iterator basicIter = tab.beginColumn(v);
-  ArithVarSet::iterator endIter = tab.endColumn(v);
+  Column::iterator basicIter = tab.beginColumn(v);
+  Column::iterator endIter = tab.endColumn(v);
   for(; basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
     has.insert(basic);
@@ -222,8 +222,8 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   DeltaRational diff = v - assignment_x_i;
 
   Assert(matchingSets(d_tableau, x_i));
-  ArithVarSet::iterator basicIter = d_tableau.beginColumn(x_i);
-  ArithVarSet::iterator endIter   = d_tableau.endColumn(x_i);
+  Column::iterator basicIter = d_tableau.beginColumn(x_i);
+  Column::iterator endIter   = d_tableau.endColumn(x_i);
   for(; basicIter != endIter; ++basicIter){
     ArithVar x_j = *basicIter;
     ReducedRowVector& row_j = d_tableau.lookup(x_j);
@@ -295,8 +295,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
 
 
   Assert(matchingSets(d_tableau, x_j));
-  ArithVarSet::iterator basicIter = d_tableau.beginColumn(x_j);
-  ArithVarSet::iterator endIter   = d_tableau.endColumn(x_j);
+  Column::iterator basicIter = d_tableau.beginColumn(x_j);
+  Column::iterator endIter   = d_tableau.endColumn(x_j);
   for(; basicIter != endIter; ++basicIter){
     ArithVar x_k = *basicIter;
     ReducedRowVector& row_k = d_tableau.lookup(x_k);
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 9769c628d..a8bcd28cc 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -36,7 +36,7 @@ void Tableau::internalCopy(const Tableau& tab){
   Debug("tableau::copy") << "tableau copy "<< N << endl;
 
   if(N > 1){
-    d_columnMatrix.insert(d_columnMatrix.end(), N, ArithVarSet());
+    d_columnMatrix.insert(d_columnMatrix.end(), N, Column());
     d_rowsTable.insert(d_rowsTable.end(), N, NULL);
     d_basicVariables.increaseSize(N-1);
 
@@ -155,7 +155,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
 
   row_s->pivot(x_s);
 
-  ArithVarSet::VarList copy(getColumn(x_s).getList());
+  Column::VarList copy(getColumn(x_s).getList());
   vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
 
   for(; basicIter != endIter; ++basicIter){
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 6fe245285..dad4bb2f5 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -37,7 +37,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef ArithVarSet Column;
+typedef PermissiveBackArithVarSet Column;
 
 typedef std::vector<Column> ColumnMatrix;
 
@@ -79,15 +79,15 @@ public:
     d_rowsTable.push_back(NULL);
     d_rowCount.push_back(0);
 
-    d_columnMatrix.push_back(ArithVarSet());
+    d_columnMatrix.push_back(PermissiveBackArithVarSet());
 
     //TODO replace with version of ArithVarSet that handles misses as non-entries
     // not as buffer overflows
-    ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
-    for(; i != end; ++i){
-      Column& col = *i;
-      col.increaseSize(d_columnMatrix.size());
-    }
+    // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
+    // for(; i != end; ++i){
+    //   Column& col = *i;
+    //   col.increaseSize(d_columnMatrix.size());
+    // }
   }
 
   bool isBasic(ArithVar v) const {