summaryrefslogtreecommitdiff
path: root/src/theory/arith/tableau.h
AgeCommit message (Expand)Author
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2014-07-01Update copyrights.Morgan Deters
2014-03-07Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m...Tim King
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-04-30Draft of the new propagation code.Tim King
2013-04-26FCSimplex branch mergeTim King
2012-04-27This merges in the branch cvc4/branches/arithmetic/matrix into trunk.Tim King
2012-03-02This commit merges in the changes from branches/arithmetic/refactor0Tim King
2011-09-28variety of visibility fixes (should clean up some of the many warnings on Mac...Morgan Deters
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
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-22- Adds column based iterators.Tim King
2011-02-21- Adds the statistic d_avgNumRowsNotContainingOnPivot.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-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
2010-09-21part of review (bug #197): coding conventions, file-level documentation, re-r...Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
2010-07-09the tableaux optimizationDejan Jovanović
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-29This commit merges the decaying-rows branch into the main trunk.Tim King
2010-06-16This commit just contains miscellaneous arithmetic cleanup.Tim King
2010-06-06Some assorted fixes and local optimizations for theory arith.Tim King
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-29Couple of fixes to theory arith. pivotAndUpdate now multiplies by a_kj. And t...Tim King
2010-05-27Preregistration has been turned on. Highly experimental eager splitting suppo...Tim King
2010-05-21Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real....Tim King
2010-05-19Significant revision to theory/arith. The new draft has a lot of small bug f...Tim King
2010-04-28Merging the arithmetic theory draft (lra-init) back into the main trunk. Thi...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback