diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-05 23:10:41 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-05 23:10:41 +0000 |
commit | c01318241e5082478090cba15ff71f82b3f6da6a (patch) | |
tree | fe91ce3b6e0572aaa9915727f41174347599f712 /src/theory/arith/tableau.h | |
parent | 3310588529b41924aadf706106599b99a3707a85 (diff) |
- 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.
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 14 |
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 { |