| 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 |
| 2014-12-09 |
Morgan Deters | Better error description (related to bug 605). |
commit | commitdiff | tree |
| 2014-12-09 |
Morgan Deters | Cleanup. |
commit | commitdiff | tree |
| 2014-12-06 |
Tianyi Liang | Added string constant in java api example. |
commit | commitdiff | tree |
| 2014-12-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-12-06 |
Tianyi Liang | Added C++/Java api examples; |
commit | commitdiff | tree |
| 2014-12-06 |
Tianyi Liang | Added C++/Java api examples; |
commit | commitdiff | tree |
| 2014-12-06 |
ajreynol | Fix dt.size care graph. |
commit | commitdiff | tree |
| 2014-12-05 |
Tianyi Liang | Relaxed the constant requirement for regular expression... |
commit | commitdiff | tree |
| 2014-12-04 |
Tianyi Liang | clean up and improve intersection |
commit | commitdiff | tree |
| 2014-12-04 |
Morgan Deters | Fix valgrind-flagged error about uninitialized value. |
commit | commitdiff | tree |
| 2014-12-04 |
Morgan Deters | Fix segfault in lambdas when constructed via API. |
commit | commitdiff | tree |
| 2014-12-04 |
Morgan Deters | Fix UnsatCore in language bindings. |
commit | commitdiff | tree |
| 2014-12-04 |
Martin Brain | Floating point infrastructure. |
commit | commitdiff | tree |
| 2014-12-03 |
Kshitij Bansal | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2014-12-03 |
Kshitij Bansal | Revert "Disable constants sharing in eq engine, disable... |
commit | commitdiff | tree |
| 2014-12-03 |
Tianyi Liang | disable inter cache |
commit | commitdiff | tree |
| 2014-11-28 |
ajreynol | Synchronize conjecture generation with E-matching.... |
commit | commitdiff | tree |
| 2014-11-27 |
Tianyi Liang | add intersection rewriting |
commit | commitdiff | tree |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-11-27 |
Tianyi Liang | add more regexp rewriting |
commit | commitdiff | tree |
| 2014-11-27 |
Tianyi Liang | add more functions for regular expressions |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog