projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 181333d) | patch
- Adds a buffer to the ReducedRowVector addRowTimesConstant operation to reduce the...
authorTim King <taking@cs.nyu.edu>
Sun, 27 Feb 2011 17:34:37 +0000 (17:34 +0000)
committerTim King <taking@cs.nyu.edu>
Sun, 27 Feb 2011 17:34:37 +0000 (17:34 +0000)
commit8d52dbabb099cb66cfffe0d63397764d8a53b21c
tree134fdc9d7837686f7f1ec2800eb9d7d2d6066db7tree
parent181333d85ccf9daea71285299493c4b0b0008f49commit | diff
- Adds a buffer to the ReducedRowVector addRowTimesConstant operation to reduce the number of allocations made.  Compare cluster jobs 1585 and 1584 for the expected performance increase.
src/theory/arith/row_vector.cpp diff | blob | history
src/theory/arith/row_vector.h diff | blob | history