| Age | Commit message (Expand) | Author |
|---|
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
| 2015-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | ajreynol |
| 2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
| 2015-04-13 | Making CVC4::theory::quantifiers::PrenexQuantMode public for now. | Tim King |
| 2015-01-23 | CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a... | ajreynol |
| 2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
| 2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
| 2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | ajreynol |
| 2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
| 2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by CE... | ajreynol |
| 2014-10-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | ajreynol |
| 2014-07-31 | New module for generating candidate equality conjectures used in inductive pr... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
| 2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
| 2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds |
| 2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q... | Andrew Reynolds |
| 2014-02-14 | Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp... | Andrew Reynolds |
| 2014-02-04 | Add variable ordering for QCF to accelerate matching procedure. Preparing fo... | Andrew Reynolds |
| 2014-01-24 | Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ... | Andrew Reynolds |
| 2014-01-17 | More optimizations for quantifiers conflict find. Add trust user patterns mode. | Andrew Reynolds |
| 2014-01-10 | Add stats to quantifiers conflict find. Added option for qcf. Working on ha... | Andrew Reynolds |
| 2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
| 2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-04 | disable model-generation by default in cvc3 compatibility layer. should fix ... | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
