| Age | Commit message (Expand) | Author |
|---|
| 2014-10-13 | CEGQI uses model. Enforce fairness in CEGQI natively. | ajreynol |
| 2014-10-13 | Model building into quantifiers engine. Simplify axiom-inst mode. | ajreynol |
| 2014-10-13 | Refactor model builder from model engine to quant engine. Work on fairness s... | ajreynol |
| 2014-10-10 | Initial draft of CEGQI. | ajreynol |
| 2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
| 2014-10-08 | Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep... | ajreynol |
| 2014-10-07 | Refactor quantifiers attributes. | ajreynol |
| 2014-10-06 | Fix a resource limiting issue where interruption didn't occur promptly. Than... | Morgan Deters |
| 2014-09-26 | Finer-grained resource-limiting in quantifiers. | Morgan Deters |
| 2014-09-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
| 2014-09-23 | Do not throw error when codatatype is not well-founded. Add option for disab... | ajreynol |
| 2014-09-18 | Resource spending support in theories (and especially in quantifiers). | Morgan Deters |
| 2014-09-16 | Bug fix variable triggers with --inst-max-level : use term in EQC with minima... | ajreynol |
| 2014-09-09 | Accept user-provided triggers with variable terms. Flush lemmas before quant... | ajreynol |
| 2014-08-29 | Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev... | ajreynol |
| 2014-08-26 | Bug fixes for --purify-triggers, --dt-force-assignment. | ajreynol |
| 2014-08-25 | New option --purify-triggers. Refactoring of InstMatchGenerator. | ajreynol |
| 2014-08-21 | Avoid doing work in quantifiers engine when no quantifiers are asserted. | ajreynol |
| 2014-08-21 | Fix --inst-max-level for strategies that use arbitrary representative terms. | ajreynol |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | 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-06-19 | More proof support for CASC : include skolemization | ajreynol |
| 2014-05-30 | Fixes for --inst-max-level | ajreynol |
| 2014-05-14 | Finish --dump-instantiations option. Update scripts. | Andrew Reynolds |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | 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-05-08 | Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min... | Andrew Reynolds |
| 2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
| 2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
| 2014-04-28 | Preparation for models for co-inductive datatypes. Minor cleanup. | Andrew Reynolds |
| 2014-04-28 | Optimizations for datatypes: check for clashes modulo equality. Avoid buildi... | ajreynol |
| 2014-04-24 | Add --inst-max-level=N option for Kshitij. Support define-const command in S... | Andrew Reynolds |
| 2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ... | Andrew Reynolds |
| 2014-03-12 | Work on array pf signature, add working example. Add quantifiers proof signa... | Andrew Reynolds |
| 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-01-28 | More optimizations of quantifier instantiation data structures. | Andrew Reynolds |
| 2014-01-27 | More optimization of QCF and instantiation caching. Fix CDInstMatchTrie. | Andrew Reynolds |
| 2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | Andrew Reynolds |
| 2014-01-18 | Performance optimization for E-matching, working on using QCF module for prop... | Andrew Reynolds |
| 2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | 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-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-11-26 | Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ... | Andrew Reynolds |
| 2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to tu... | Andrew Reynolds |
