projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3310588) | patch
- Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The differenc...
authorTim King <taking@cs.nyu.edu>
Sat, 5 Mar 2011 23:10:41 +0000 (23:10 +0000)
committerTim King <taking@cs.nyu.edu>
Sat, 5 Mar 2011 23:10:41 +0000 (23:10 +0000)
commitc01318241e5082478090cba15ff71f82b3f6da6a
treefe91ce3b6e0572aaa9915727f41174347599f712tree
parent3310588529b41924aadf706106599b99a3707a85commit | 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.
src/theory/arith/arithvar_set.h diff | blob | history
src/theory/arith/row_vector.cpp diff | blob | history
src/theory/arith/row_vector.h diff | blob | history
src/theory/arith/simplex.cpp diff | blob | history
src/theory/arith/tableau.cpp diff | blob | history
src/theory/arith/tableau.h diff | blob | history