| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
| 2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr... | 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-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
| 2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by CE... | 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-10-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | ajreynol |
| 2014-10-01 | Option for more aggressive merging in UEE. | ajreynol |
| 2014-09-29 | Add option for aggressive model filtering in conjecture generator (enumerate ... | ajreynol |
| 2014-09-16 | Refactoring of conjecture generator. Determine subgoals are non-canonical ba... | ajreynol |
| 2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change... | ajreynol |
| 2014-09-03 | Work on conjecture generator : do not generalize subterms with concrete value... | ajreynol |
| 2014-08-27 | Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict. | 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-20 | Add option for inductive strengthening based on well-founded induction for in... | 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-06-19 | Minor fixes, spelling etc. | Morgan Deters |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | ajreynol |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
| 2014-05-08 | Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min... | Andrew Reynolds |
| 2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat... | Andrew Reynolds |
