summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.cpp
AgeCommit message (Expand)Author
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-05-29Do not enforce dt fairness when single invocation sygus.ajreynol
2015-05-10Minor improvements to infrastructure. Minor changes to default options. Add t...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable del...ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...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-02Single invocation module for counterexample guided quantifier instantiation -...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-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-23CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a...ajreynol
2015-01-22Narrow sygus search space based on NNF and rewriting constant arguments.ajreynol
2015-01-22Do not drop patterns during boolean term rewriting. Narrow sygus search space...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
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-01Fix cegqi for synthesis without syntax.ajreynol
2014-10-24Fix typo.Morgan Deters
2014-10-16Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch...ajreynol
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by CE...ajreynol
2014-10-13CEGQI uses model. Enforce fairness in CEGQI natively.ajreynol
2014-10-13Refactor model builder from model engine to quant engine. Work on fairness s...ajreynol
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback