| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-02-19 | Merge branch '1.3.x' | Tim King |
| 2014-02-19 | Stopping non-linear terms from entering the dio solver. Fixes bug 547. | Tim King |
| 2014-02-17 | type conversion | Tianyi Liang |
| 2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
| 2013-12-24 | Minor code cleanup. | Morgan Deters |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-11-27 | General pre-release cleanup commit | Morgan Deters |
| 2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
| 2013-09-27 | fix the infinite issue | Tianyi Liang |
| 2013-09-27 | for morgan to see the regression problems | Tianyi Liang |
| 2013-09-27 | adds model generation for strings, and a hacked way in arith engine for models | Tianyi Liang |
| 2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
| 2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
| 2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
| 2013-06-27 | Small fix for IS_INTEGER. | Morgan Deters |
| 2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
| 2013-05-22 | Add regressions for finite model finding | Andrew Reynolds |
| 2013-05-16 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters |
| 2013-05-11 | Preliminary version of finite model finding over bounded integer quantificati... | Andrew Reynolds |
| 2013-05-09 | Changing the integer normal form to increase matching. | Tim King |
| 2013-05-08 | Removing arithmetic compile warning for release | Morgan Deters |
| 2013-05-07 | Fixes a bug with arithmetic's new attempt solution infrastructure. This caus... | Tim King |
| 2013-05-07 | Improving arithmetic debugging output. | Tim King |
| 2013-05-07 | Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510. | Tim King |
| 2013-05-06 | Removing excess verbosity from ApproxSimplex (after discussing with Tim) | Morgan Deters |
