| Age | Commit message (Expand) | Author |
|---|
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-12-10 | Add option fmf-empty-sorts. | ajreynol |
| 2015-11-25 | Infrastructure for partially single invocation properties. Bug fix for uncons... | ajreynol |
| 2015-11-18 | Option for midpoints in cbqi. | 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-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-10-16 | Add option to interleave enumerative instantiation with other strategies. | ajreynol |
| 2015-09-26 | Better organization of quantifiers modules, promote full saturation to module... | ajreynol |
| 2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol |
| 2015-09-06 | Improve quantifiers rewriter, minor refactoring. | ajreynol |
| 2015-08-30 | Minor improvement to sygus sol reconstruction. | ajreynol |
| 2015-08-28 | Improvements to sygus, register equivalent terms based on rewrites of origina... | 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-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-07-12 | Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms. | ajreynol |
| 2015-07-05 | Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu... | ajreynol |
| 2015-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | 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-04 | Minor changes to smt comp script for quantified arith. Add option --cbqi-sat... | ajreynol |
| 2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
| 2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | 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-02-02 | Single invocation module for counterexample guided quantifier instantiation -... | ajreynol |
| 2015-02-01 | Generalization of sygus lemmas based on arguments and content. | ajreynol |
| 2015-01-30 | Generalize conflict clauses in sygus sym break, merge caches, refactor. Prep... | ajreynol |
| 2015-01-29 | Apply global search space narrowing for multiple synth-fun, enable its confli... | ajreynol |
| 2015-01-27 | Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled.... | ajreynol |
| 2015-01-24 | Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in... | ajreynol |
| 2015-01-23 | CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a... | ajreynol |
| 2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol |
| 2015-01-22 | Do not drop patterns during boolean term rewriting. Narrow sygus search space... | ajreynol |
| 2015-01-21 | Initial work on sygusNormalForm. | ajreynol |
| 2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. Add... | ajreynol |
| 2015-01-16 | Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de... | ajreynol |
| 2015-01-14 | sygus input language and benchmark | Morgan Deters |
| 2014-12-28 | Disable prenex by default when using fmf bound int, minor improvement to data... | ajreynol |
| 2014-12-22 | Add misc trigger options. | ajreynol |
| 2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
| 2014-11-21 | Change default option to --inst-when=full-last-call (interleave instantiation... | ajreynol |
| 2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | ajreynol |
