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-05-26 | Checking that equalities belong to the arithmetic theory in the solve() routine. | Tim King |
2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
2016-12-09 | Fixing a use after free bug in Polynomial::denominatorLCM. | 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-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | 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 |
2013-03-21 | Better error in case of nonlinear assertions while in linear logic | Morgan Deters |
2012-11-12 | Improved error reporting for improperly using non-linear division in linear a... | Tim King |
2012-11-11 | Fixes for the arithmetic normal form and rewriter to handle arbitrary constan... | Tim King |
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-06-12 | Fix to yesterday's change in arithmetic. | Tim King |
2012-06-11 | Fix to term normalization of integer equalities. Adds a regression test that ... | Tim King |
2012-05-18 | This commit removes the dead psuedoboolean code. | 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-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-02-13 | 3 heuristics were added to arithmetic. A heuristic for detecting an encoding ... | Tim King |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-10-31 | enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d... | Morgan Deters |
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-10-02 | branches/arith-indexed-variables merged into the main trunk. | Tim King |
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 |