| Age | Commit message (Expand) | Author |
|---|
| 2018-02-07 | Add remaining transcendental functions (#1551) | Andrew Reynolds |
| 2017-07-17 | Use is_sorted, merge, copy from std (#199) | Andres Noetzli |
| 2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring of... | ajreynol |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
| 2016-04-20 | update from the master | PaulMeng |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-04-18 | Farkas proof coefficients. | Tim King |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-19 | Fix for pre-C++11 is_sorted(). | Morgan Deters |
| 2014-06-19 | Final preparations for arithmetic for building with libc++. | Morgan Deters |
| 2014-06-06 | Patch for the subtype theoryof mode to make the equalities over disequal type... | Tim King |
| 2014-03-26 | Merging in a fix from 1.3.x. | Tim King |
| 2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
| 2014-02-19 | Stopping non-linear terms from entering the dio solver. Fixes bug 547. | Tim King |
| 2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
| 2013-05-09 | Changing the integer normal form to increase matching. | Tim King |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2012-11-08 | Improved support for division by zero. This adds the *_TOTAL kinds and unint... | Tim King |
| 2012-11-07 | Fix to a bug in integer mod lemmas. | Tim King |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-09-29 | This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ... | Tim King |
| 2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
| 2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
| 2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
| 2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
| 2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
| 2012-03-28 | Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AG... | Tim King |
| 2012-02-15 | This commit merges into trunk the branch branches/arithmetic/integers2 from r... | Tim King |
| 2011-10-28 | Adding a check in Polynomial::parsePolynomial to better enforce the arithmeti... | Tim King |
| 2011-09-16 | fix numerous documentation issues; doxygen complains much less, now | Morgan Deters |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
| 2011-03-17 | - Removes arith_constants.h | Tim King |
| 2011-02-16 | Overview of the changes: | Tim King |
| 2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
| 2010-10-28 | The Row implementation has no been replaced by RowVector and ReducedRowVector... | Tim King |
| 2010-10-13 | Removed vector<Monomial> monos from Polynomial. Now using expr::NodeSelfIter... | Tim King |
| 2010-10-12 | IDENTITY has been removed. | Tim King |
| 2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
| 2010-09-21 | part of review (bug #197): coding conventions, file-level documentation, re-r... | Morgan Deters |
| 2010-09-16 | Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. ... | Tim King |
| 2010-09-13 | * New normal form for arithmetic is in place. | Tim King |
