| Age | Commit message (Expand) | Author |
|---|
| 2016-04-20 | update from the master | PaulMeng |
| 2016-01-28 | Adding listeners to Options. | Tim King |
| 2016-01-15 | Type enumerators take optional argument indicating fixed cardinalities of uni... | ajreynol |
| 2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
| 2016-01-05 | Add SmtGlobals Class | Tim King |
| 2015-12-24 | Miscellaneous fixes | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-03 | Fixing typo. | Tim King |
| 2015-10-26 | This commit fixes a bug related to a public header depending on a compiler fl... | Tim King |
| 2015-06-15 | Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr... | Tim King |
| 2015-06-14 | Handing the case in replay where a cut is directly in conflict with an existi... | Tim King |
| 2015-06-14 | Fixes for shared term normalization in replay for constraint construction. | Tim King |
| 2015-06-14 | Turning off aggressive arith ite simplifications during incremental solving. | Tim King |
| 2015-06-13 | Restricting TheoryArith to computeRelevantTerms. | Tim King |
| 2015-06-13 | A return value for an ApproxGLPK::loadVB() failure case was incorrect. | Tim King |
| 2015-06-12 | In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n... | Tim King |
| 2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
| 2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
| 2015-04-18 | Farkas proof coefficients. | Tim King |
| 2015-03-25 | change const are triggers from false to true in equality engines | Kshitij Bansal |
| 2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
| 2014-11-17 | Short-circuit in TheoryArithPrivate::check(), care of Tim. | Morgan Deters |
| 2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
| 2014-08-24 | improvements to sets sharing | Kshitij Bansal |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-25 | Fixing the previous bugfix. | Tim King |
| 2014-06-24 | Alternative lazier heuristic for assertion rewriting. | Tim King |
| 2014-06-24 | Fixing a soundness bug in arithmetic and a roubustness problem in rings. | Tim King |
| 2014-06-21 | Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ... | Morgan Deters |
| 2014-06-19 | Fix GLPK builds: correct access specifier on cut classes. | Morgan Deters |
| 2014-06-19 | disable unate lemmas when using incremental mode | Kshitij Bansal |
| 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-19 | This commit adds a priority queue implementation. This is to avoid compilati... | Tim King |
| 2014-06-19 | Clean up glpk detection a little, fix a detection bug. | Morgan Deters |
| 2014-06-10 | Merging Tim's pseudoboolean work from his fmcad14 branch. | Tim King |
| 2014-06-06 | Patch for the subtype theoryof mode to make the equalities over disequal type... | Tim King |
| 2014-05-12 | Merging in additional glpk options and statistics from CAV submission. | Tim King |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-29 | Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrit... | Morgan Deters |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
| 2014-03-26 | Merging in a fix from 1.3.x. | Tim King |
| 2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
| 2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
| 2014-03-08 | Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-gr... | Morgan Deters |
| 2014-03-08 | Fixing name changes that cam in from the merge. | Tim King |
| 2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
| 2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King |
| 2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r... | Morgan Deters |
| 2014-02-19 | Merge branch 'master' of github.com:CVC4/CVC4 | Tim King |
