| Age | Commit message (Expand) | Author |
|---|
| 2015-08-26 | Minor improvements to cbqi, fix bug in solving with vts symbols, round up for... | ajreynol |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-02-22 | New trigger options. --inst-no-entail on by default. Misc cleanup. | ajreynol |
| 2015-01-24 | Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in... | ajreynol |
| 2015-01-23 | Rework inst-closure. | ajreynol |
| 2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol |
| 2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
| 2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
| 2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
| 2014-10-10 | Initial draft of CEGQI. | ajreynol |
| 2014-10-07 | Refactor quantifiers attributes. | ajreynol |
| 2014-09-03 | check() optimization | Kshitij Bansal |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-19 | More proof support for CASC : include skolemization | ajreynol |
| 2014-06-03 | Support E-matching/QCF for Set operators. | ajreynol |
| 2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat... | Andrew Reynolds |
| 2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r... | Morgan Deters |
| 2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-07-22 | Add option --cbqi-recurse. | Andrew Reynolds |
| 2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
| 2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-02-07 | Only put quantifier assertions in model equality engine if fullModel==true | Morgan Deters |
| 2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters |
| 2013-01-26 | another fix for quantifier models (related to bug 486) | Morgan Deters |
| 2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters |
| 2012-12-11 | adding cache for preprocessing datatypes terms to fix bug 475, fix for handli... | Andrew Reynolds |
| 2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
| 2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
