| Age | Commit message (Expand) | Author |
|---|
| 2016-02-18 | Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug ... | ajreynol |
| 2016-02-17 | Refactor quantifiers attributes. Make quantifier elimination robust to prepro... | ajreynol |
| 2016-02-01 | Simplify fmc model construction, add regression. Improve FMF debug assertions. | ajreynol |
| 2015-11-25 | Infrastructure for partially single invocation properties. Bug fix for uncons... | ajreynol |
| 2015-11-12 | Minor fixes and improvements to purify quant, relational triggers. | ajreynol |
| 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-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol |
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress... | ajreynol |
| 2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
| 2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol |
| 2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ... | ajreynol |
| 2015-09-11 | Minor cleanup related to codatatypes. | ajreynol |
| 2015-09-06 | Improve quantifiers rewriter, minor refactoring. | ajreynol |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-08-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
| 2015-07-31 | Sygus support for inductive datatypes. | ajreynol |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix soundnes... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
| 2015-06-16 | Avoid completion for large finite types. Fix bug for --fmf-fun. | ajreynol |
| 2015-06-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | ajreynol |
| 2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
| 2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
| 2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
| 2015-02-11 | Move si solution reconstruction to own file, make more robust. Other refactor... | ajreynol |
| 2015-02-06 | Handle missing cases for single inv solution reconstruction. Minor fixes. Re... | ajreynol |
| 2015-02-05 | Working version of sygus solution reconstruction from single inv cegqi. Heur... | ajreynol |
| 2015-02-04 | Work on solution reconstruction for single inv. Fix compiler error found by ... | ajreynol |
| 2015-02-04 | Refactor sygus_util to TermDb. Initial work on solution reconstruction into ... | ajreynol |
| 2015-02-04 | Start work on simplifying single inv solutions. Minor. | ajreynol |
| 2015-01-24 | Variable patterns only look at eligible terms. Minor refactoring of quantifi... | ajreynol |
| 2015-01-24 | Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in... | ajreynol |
| 2015-01-23 | Rework inst-closure. | ajreynol |
| 2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol |
| 2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
| 2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | ajreynol |
| 2014-11-13 | More preparation for filtering relevant terms in TermDb. | ajreynol |
| 2014-11-11 | Work on synchronizing decision=justification and E-matching. | ajreynol |
| 2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements to... | ajreynol |
| 2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | ajreynol |
| 2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
| 2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | 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-07 | Refactor quantifiers attributes. | ajreynol |
| 2014-09-16 | Refactoring of conjecture generator. Determine subgoals are non-canonical ba... | ajreynol |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | ajreynol |
