| Age | Commit message (Expand) | Author |
|---|
| 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-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-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-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | 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-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | 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 |
| 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-09-23 | Support :no-pattern. | ajreynol |
| 2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
| 2014-04-28 | Optimizations for datatypes: check for clashes modulo equality. Avoid buildi... | ajreynol |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
| 2012-10-31 | cleaning up some of the equality query stuff, implemented a new representativ... | Andrew Reynolds |
| 2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-10 | cleanup up some static data members in the quantifiers code | Andrew Reynolds |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-07-31 | Moving some instantiation-related stuff from src/theory to src/theory/quantif... | 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 |
