summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2015-04-08Make fun-def quantifiers carry the function app they define, make fun-def uti...ajreynol
2015-04-07Minor fixes for cegqi.ajreynol
2015-04-01Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun...ajreynol
2015-03-31fix no return value warningKshitij Bansal
2015-03-23Decouple counter-example guided quantifier instantiation from Sygus.ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other refactor...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...ajreynol
2015-02-05Working version of sygus solution reconstruction from single inv cegqi. Heur...ajreynol
2015-02-04Initial draft of solution reconstruction into syntax for single inv cegqi.ajreynol
2015-02-04Work on solution reconstruction for single inv. Fix compiler error found by ...ajreynol
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ...ajreynol
2015-02-04Start work on simplifying single inv solutions. Minor.ajreynol
2015-02-03Simple variable elimination for single inv properties. Relax conditions for ...ajreynol
2015-02-03Solutions for single invocation conjectures.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
2015-02-01Generalization of sygus lemmas based on arguments and content.ajreynol
2015-01-31Bug fix fairness for commutative operators in sygus. Minor.ajreynol
2015-01-31Lemmas instead of conflicts in sygus sym break (do not expand explanations). ...ajreynol
2015-01-30Generalize conflict clauses in sygus sym break, merge caches, refactor. Prep...ajreynol
2015-01-29Restrict LtePartialInst instantiations based on E-matching, promote to quanti...ajreynol
2015-01-29Apply global search space narrowing for multiple synth-fun, enable its confli...ajreynol
2015-01-28Minor refactor CEGQI.ajreynol
2015-01-27Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled....ajreynol
2015-01-27Recognize when synthesis conjectures are in single invocation fragment.ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2015-01-24Variable patterns only look at eligible terms. Minor refactoring of quantifi...ajreynol
2015-01-24Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in...ajreynol
2015-01-23CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a...ajreynol
2015-01-23Rework inst-closure.ajreynol
2015-01-22Narrow sygus search space based on NNF and rewriting constant arguments.ajreynol
2015-01-22Add option --lte-partial-inst. Remove inst-closure.ajreynol
2015-01-22Do not drop patterns during boolean term rewriting. Narrow sygus search space...ajreynol
2015-01-21Initial work on sygusNormalForm.ajreynol
2015-01-20Mark datatypes as sygus. Add option to normalize sygus terms in search. Add...ajreynol
2015-01-20Handle miniscoping of conjunctions in synthesis properties. Refactor constru...ajreynol
2015-01-16Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de...ajreynol
2015-01-16Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus...ajreynol
2015-01-14sygus input language and benchmarkMorgan Deters
2014-12-28Disable prenex by default when using fmf bound int, minor improvement to data...ajreynol
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-22Add misc trigger options.ajreynol
2014-11-28Synchronize conjecture generation with E-matching. Minor fix to --full-satur...ajreynol
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback