summaryrefslogtreecommitdiff
path: root/src/theory/arith/tableau.cpp
AgeCommit message (Expand)Author
2018-06-25Updated copyright headers.Aina Niemetz
2017-07-07Update copyright headers.Mathias Preiner
2016-04-20update from the masterPaulMeng
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-04-18Farkas proof coefficients.Tim King
2014-07-01Update copyrights.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-04-30Adding has bound counts and tracking for rows.Tim King
2013-04-26FCSimplex branch mergeTim King
2012-04-27This merges in the branch cvc4/branches/arithmetic/matrix into trunk.Tim King
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-03-30Merged the branch sparse-tableau into trunk.Tim King
2011-03-07Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now ...Tim King
2011-03-05- Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The d...Tim King
2011-03-03Merged the tableau-copy branch into trunk. This adds a copy constructor and o...Tim King
2011-02-26Commit to fix bug 241 (improper "using namespace std" in a header). This cau...Morgan Deters
2011-02-22- Adds column based iterators.Tim King
2011-02-19Changes:Tim King
2011-02-18Changes:Tim King
2011-02-17This commit is the promised clean up after removing row ejection.Tim King
2011-02-17Removed ActivityMonitor from arithmetic. This was only used for row ejection,...Tim King
2011-02-17Row ejection is now completely disabled. Another commit cleaning this one up ...Tim King
2011-02-16Overview of the changes:Tim King
2010-10-30Adds a hueristic from Alberto's thesis. For a fixed window the row count is u...Tim King
2010-10-29Fix for a problem caused by using a != instead of == in generateConflictBelow...Tim King
2010-10-28The Row implementation has no been replaced by RowVector and ReducedRowVector...Tim King
2010-10-23Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more ...Tim King
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-07Small tableau optimization.Tim King
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-10-02branches/arith-indexed-variables merged into the main trunk.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback