| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-05-28 | Minor changes to script. Disable cbqi sat. | ajreynol |
| 2014-05-12 | Minor updates/fix to --cbqi-recurse | Andrew Reynolds |
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
| 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-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
| 2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r... | Morgan Deters |
| 2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds |
| 2014-02-14 | Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp... | Andrew Reynolds |
| 2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | 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 |
| 2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to tu... | Andrew Reynolds |
| 2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
| 2013-07-18 | Fix quantifier instantiation bug in cbqi, add default priorities in rewrite e... | Andrew Reynolds |
| 2013-06-17 | Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod... | Andrew Reynolds |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as datatype... | Andrew Reynolds |
| 2013-01-28 | made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_pro... | Andrew Reynolds |
| 2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
| 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-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-06-14 | fix quantifier non-bug | Kshitij Bansal |
| 2012-06-11 | mark a quantifiers global var as "static" so we can find it easier later | Morgan Deters |
