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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/arith/tableau.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
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){ |