| Age | Commit message (Expand) | Author |
|---|
| 2015-05-15 | Fixes related to cbqi + E-matching. | ajreynol |
| 2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | ajreynol |
| 2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | ajreynol |
| 2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
| 2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol |
| 2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
| 2015-05-02 | Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add co... | ajreynol |
| 2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
| 2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode... | ajreynol |
| 2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm... | ajreynol |
| 2015-04-24 | Fix sygus parser for non-tokenized operators, reenable regression. Fix for --... | ajreynol |
| 2015-04-24 | Fix compiler errors due to unbalanced throw specifiers. | Clark Barrett |
| 2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
| 2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
| 2015-04-21 | Fix file permissions | Clark Barrett |
| 2015-04-21 | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. | ajreynol |
| 2015-04-16 | Fix option --quant-fun-wd. Add mk_starexec script to contrib. | ajreynol |
| 2015-04-16 | Handle (degenerate) case of synthesis conjectures for constants. Disable del... | ajreynol |
| 2015-04-13 | Making CVC4::theory::quantifiers::PrenexQuantMode public for now. | Tim King |
| 2015-04-09 | Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an... | ajreynol |
| 2015-04-09 | Fix performance issue with variable triggers + instantiation restrictions. | ajreynol |
| 2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
| 2015-04-07 | Minor fixes for cegqi. | ajreynol |
| 2015-04-01 | Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun... | ajreynol |
| 2015-03-31 | fix no return value warning | Kshitij Bansal |
| 2015-03-23 | Decouple counter-example guided quantifier instantiation from Sygus. | ajreynol |
| 2015-03-11 | Minor fixes and improvements to cegqi-si for linear arithmetic. | ajreynol |
| 2015-03-05 | Minor fixes. Extend cegqi-si to real arithmetic. | ajreynol |
| 2015-03-04 | More work on arithmetic single invocation synthesis conjectures. | ajreynol |
| 2015-02-26 | Robust strategy for single invocation LIA synthesis conjectures. Add regress... | ajreynol |
| 2015-02-22 | New trigger options. --inst-no-entail on by default. Misc cleanup. | ajreynol |
| 2015-02-13 | Handle recursive singleton case for codatatypes, add regression. Simplify im... | ajreynol |
| 2015-02-11 | Better support for solving multiple functions with cegqi-si. Minor cleanup. | 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 | Initial draft of solution reconstruction into syntax for single inv cegqi. | 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-02-03 | Simple variable elimination for single inv properties. Relax conditions for ... | ajreynol |
| 2015-02-03 | Solutions for single invocation conjectures. | 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-31 | Bug fix fairness for commutative operators in sygus. Minor. | ajreynol |
| 2015-01-31 | Lemmas instead of conflicts in sygus sym break (do not expand explanations). ... | ajreynol |
| 2015-01-30 | Generalize conflict clauses in sygus sym break, merge caches, refactor. Prep... | ajreynol |
| 2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
| 2015-01-29 | Apply global search space narrowing for multiple synth-fun, enable its confli... | ajreynol |
| 2015-01-28 | Minor refactor CEGQI. | ajreynol |
