| 2015-03-28 |
Tianyi Liang | printer change for string smtlib2 |
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Parsing support for define-fun-rec/define-funs-rec. |
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Decouple counter-example guided quantifier instantiatio... |
commit | commitdiff | tree |
| 2015-03-16 |
Tianyi Liang | Add requirePhase len(x) = 0. |
commit | commitdiff | tree |
| 2015-03-16 |
Liana Hadarean | Fixed proof unitialized memory and minor memory leaks. |
commit | commitdiff | tree |
| 2015-03-14 |
Tianyi Liang | Bug fix for BV |
commit | commitdiff | tree |
| 2015-03-14 |
Tianyi Liang | Patches for 32-bit ARM |
commit | commitdiff | tree |
| 2015-03-14 |
Dejan Jovanovic | Updating resize for occurence lists to properly resize... |
commit | commitdiff | tree |
| 2015-03-11 |
ajreynol | Strings split on constant lengths, add length=0 to... |
commit | commitdiff | tree |
| 2015-03-11 |
ajreynol | Minor fixes and improvements to cegqi-si for linear... |
commit | commitdiff | tree |
| 2015-03-10 |
ajreynol | CNF proofs. Infrastructure for preprocessing proofs... |
commit | commitdiff | tree |
| 2015-03-05 |
ajreynol | Minor fixes. Extend cegqi-si to real arithmetic. |
commit | commitdiff | tree |
| 2015-03-04 |
ajreynol | More work on arithmetic single invocation synthesis... |
commit | commitdiff | tree |
| 2015-02-28 |
Kshitij Bansal | Revert "dummy commit to force nightly builds" |
commit | commitdiff | tree |
| 2015-02-26 |
ajreynol | Robust strategy for single invocation LIA synthesis... |
commit | commitdiff | tree |
| 2015-02-25 |
Tianyi Liang | Switch back to eager loop temporarily. |
commit | commitdiff | tree |
| 2015-02-25 |
Tianyi Liang | minor fix for internal string print |
commit | commitdiff | tree |
| 2015-02-22 |
ajreynol | New trigger options. --inst-no-entail on by default... |
commit | commitdiff | tree |
| 2015-02-19 |
Kshitij Bansal | dummy commit to force nightly builds |
commit | commitdiff | tree |
| 2015-02-16 |
Kshitij Bansal | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2015-02-16 |
Kshitij Bansal | webget: curl follow redirect |
commit | commitdiff | tree |
| 2015-02-14 |
ajreynol | Fix unit tests. |
commit | commitdiff | tree |
| 2015-02-14 |
Kshitij Bansal | attempt to fix win32 builds |
commit | commitdiff | tree |
| 2015-02-13 |
ajreynol | Minor cleanup, remove unused files. |
commit | commitdiff | tree |
| 2015-02-13 |
ajreynol | Handle recursive singleton case for codatatypes, add... |
commit | commitdiff | tree |
| 2015-02-12 |
Kshitij Bansal | try curl before wget, workaround for issue with FTP... |
commit | commitdiff | tree |
| 2015-02-12 |
Tim King | Changing CXXFLAGS for custom cln installation in config... |
commit | commitdiff | tree |
| 2015-02-11 |
ajreynol | Better support for solving multiple functions with... |
commit | commitdiff | tree |
| 2015-02-11 |
ajreynol | Move si solution reconstruction to own file, make more... |
commit | commitdiff | tree |
| 2015-02-06 |
ajreynol | Handle missing cases for single inv solution reconstruc... |
commit | commitdiff | tree |
| 2015-02-06 |
Tianyi Liang | Minor clean up |
commit | commitdiff | tree |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2015-02-06 |
Tianyi Liang | Improved string performance, thanks to Peter's benchmarks. |
commit | commitdiff | tree |
| 2015-02-06 |
Tianyi Liang | Improved string performance, thanks to Peter's benchmarks. |
commit | commitdiff | tree |
| 2015-02-05 |
ajreynol | Working version of sygus solution reconstruction from... |
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Initial draft of solution reconstruction into syntax... |
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Work on solution reconstruction for single inv. Fix... |
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Refactor sygus_util to TermDb. Initial work on solutio... |
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Start work on simplifying single inv solutions. Minor. |
commit | commitdiff | tree |
| 2015-02-03 |
ajreynol | Simple variable elimination for single inv properties... |
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Solutions for single invocation conjectures. |
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Single invocation module for counterexample guided... |
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Representative programs must be minimal size, minor... |
commit | commitdiff | tree |
| 2015-02-01 |
ajreynol | Generalization of sygus lemmas based on arguments and... |
commit | commitdiff | tree |
| 2015-01-31 |
ajreynol | Bug fix fairness for commutative operators in sygus... |
commit | commitdiff | tree |
| 2015-01-31 |
ajreynol | Lemmas instead of conflicts in sygus sym break (do... |
commit | commitdiff | tree |
| 2015-01-30 |
ajreynol | Generalize conflict clauses in sygus sym break, merge... |
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Apply sygus search space narrowing for all subprograms... |
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Restrict LtePartialInst instantiations based on E-match... |
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Apply global search space narrowing for multiple synth... |
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Add module for sygus search space narrowing based on... |
commit | commitdiff | tree |
| 2015-01-28 |
ajreynol | Minor refactor CEGQI. |
commit | commitdiff | tree |
| 2015-01-27 |
ajreynol | Always miniscope nested quantifiers. Disable miniscopi... |
commit | commitdiff | tree |
| 2015-01-27 |
ajreynol | Recognize when synthesis conjectures are in single... |
commit | commitdiff | tree |
| 2015-01-26 |
ajreynol | Output solutions for synthesis conjectures with --dump... |
commit | commitdiff | tree |
| 2015-01-26 |
ajreynol | Generalize sygus search space narrowing to arbitrary... |
commit | commitdiff | tree |
| 2015-01-24 |
ajreynol | Variable patterns only look at eligible terms. Minor... |
commit | commitdiff | tree |
| 2015-01-24 |
ajreynol | Add --lte-restrict-inst-closure option. Push dt.size... |
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | Refactor sygus arg nf. Minor improvements. |
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | CEGQI fairness based on term height. Fix sygus-nf... |
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | Rework inst-closure. |
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Narrow sygus search space based on NNF and rewriting... |
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Add option --lte-partial-inst. Remove inst-closure. |
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Do not drop patterns during boolean term rewriting... |
commit | commitdiff | tree |
| 2015-01-21 |
ajreynol | Avoid redundant constant arguments for SygusNormalForm... |
commit | commitdiff | tree |
| 2015-01-21 |
ajreynol | Initial work on sygusNormalForm. |
commit | commitdiff | tree |
| 2015-01-20 |
ajreynol | Mark datatypes as sygus. Add option to normalize sygus... |
commit | commitdiff | tree |
| 2015-01-20 |
ajreynol | Handle miniscoping of conjunctions in synthesis propert... |
commit | commitdiff | tree |
| 2015-01-19 |
Tim King | Adding tests for get-value output for arithmetic. |
commit | commitdiff | tree |
| 2015-01-19 |
Tim King | Adding an additional search path to configure.ac for... |
commit | commitdiff | tree |
| 2015-01-17 |
ajreynol | Avoid name conflicts for multiple synth-fun. |
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Linearize multiplication by constants in sygus grammars... |
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Allow uninterpreted/defined functions in Sygus grammars... |
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Minor: Ensure indexed terms are in EE. Add support... |
commit | commitdiff | tree |
| 2015-01-14 |
Morgan Deters | sygus input language and benchmark |
commit | commitdiff | tree |
| 2015-01-13 |
Morgan Deters | Fix #line numbering. |
commit | commitdiff | tree |
| 2015-01-13 |
Morgan Deters | Fix a memory issue in ResourceManager on 32-bit (resolv... |
commit | commitdiff | tree |
| 2015-01-13 |
Morgan Deters | Remove private #include. |
commit | commitdiff | tree |
| 2015-01-13 |
Morgan Deters | Fix typo. |
commit | commitdiff | tree |
| 2015-01-13 |
Morgan Deters | Remove old .orig files that were added to the repository. |
commit | commitdiff | tree |
| 2015-01-11 |
Tianyi Liang | adjusted to both v2.0 and v2.5 string literals |
commit | commitdiff | tree |
| 2015-01-09 |
Tianyi Liang | blocked unprintable characters in string literals; |
commit | commitdiff | tree |
| 2015-01-08 |
Tianyi Liang | switch ascii encoding to unsigned char |
commit | commitdiff | tree |
| 2015-01-07 |
Tianyi Liang | patch to the last commit |
commit | commitdiff | tree |
| 2015-01-07 |
Tianyi Liang | bug fix, thanks to Pierre's report |
commit | commitdiff | tree |
| 2015-01-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2015-01-07 |
Tianyi Liang | added initial AX rules; |
commit | commitdiff | tree |
| 2015-01-07 |
Tianyi Liang | added initial AX rules; |
commit | commitdiff | tree |
| 2014-12-28 |
ajreynol | Disable prenex by default when using fmf bound int... |
commit | commitdiff | tree |
| 2014-12-27 |
Dejan Jovanovic | Adding an option to the equality engine constructor... |
commit | commitdiff | tree |
| 2014-12-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-12-22 |
Tianyi Liang | bug fix for constant regular expression model building |
commit | commitdiff | tree |
| 2014-12-22 |
Tianyi Liang | bug fix for constant regular expression model building |
commit | commitdiff | tree |
| 2014-12-22 |
ajreynol | Do not collapse wrongly applied selectors for non-well... |
commit | commitdiff | tree |
| 2014-12-21 |
ajreynol | Add misc trigger options. |
commit | commitdiff | tree |
| 2014-12-16 |
Morgan Deters | Fix oversight in dumping assertions in preprocessing. |
commit | commitdiff | tree |
| 2014-12-12 |
ajreynol | Add cvc parsing support for cardinality constraints... |
commit | commitdiff | tree |
| 2014-12-11 |
Morgan Deters | Minor fixes to language bindings. (Resolves #607.) |
commit | commitdiff | tree |
| 2014-12-11 |
ajreynol | Option to enable/disable cyclicity check in datatypes. |
commit | commitdiff | tree |
| 2014-12-11 |
Tianyi Liang | bug fix, thanks to Guy's example. |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog