| Age | Commit message (Expand) | Author |
|---|
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds |
| 2017-11-14 | Make QEffort an enum (#1366) | Andrew Reynolds |
| 2017-11-01 | (Refactor) Split term util (#1303) | Andrew Reynolds |
| 2017-10-09 | Split term database (#1206) | Andrew Reynolds |
| 2017-09-25 | Fixing CID 1362917: There was a branch where d_issup was not initialized. Swi... | Tim King |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
| 2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
| 2016-09-29 | Minor cleanup and additions to quantifiers statistics. | ajreynol |
| 2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
| 2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
| 2016-05-06 | Minor clean up, fixes related to sygus. | ajreynol |
| 2016-04-20 | update from the master | PaulMeng |
| 2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
| 2016-04-10 | More work on instantiation propagation. Enable external filtering of instanti... | ajreynol |
| 2016-04-04 | New options for trigger selection, add option --strict-triggers. Do not infer... | ajreynol |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol |
| 2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
| 2015-10-26 | Extend counterexample-guided instantiation to extended theory of Int/Real, mi... | ajreynol |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-26 | Better organization of quantifiers modules, promote full saturation to module... | ajreynol |
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
| 2015-08-27 | Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S... | ajreynol |
| 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-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
| 2015-08-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
| 2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
| 2015-06-04 | Minor changes to smt comp script for quantified arith. Add option --cbqi-sat... | ajreynol |
| 2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | ajreynol |
| 2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | ajreynol |
| 2015-04-09 | Fix performance issue with variable triggers + instantiation restrictions. | ajreynol |
| 2015-04-07 | Minor fixes for cegqi. | ajreynol |
| 2015-04-01 | Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun... | ajreynol |
| 2015-03-23 | Decouple counter-example guided quantifier instantiation from Sygus. | ajreynol |
| 2015-02-22 | New trigger options. --inst-no-entail on by default. Misc cleanup. | ajreynol |
| 2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
| 2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to --full-satur... | ajreynol |
| 2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | ajreynol |
| 2014-10-13 | Refactor model builder from model engine to quant engine. Work on fairness s... | ajreynol |
| 2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
| 2014-09-23 | Support :no-pattern. | ajreynol |
| 2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ... | ajreynol |
| 2014-07-31 | New module for generating candidate equality conjectures used in inductive pr... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
