- 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.

1 files changed, 7 insertions, 7 deletions

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 {