| 2015-04-21 |
Tim King | Adding an example of a tester in SMT2. |
commit | commitdiff | tree |
| 2015-04-18 |
Tim King | Farkas proof coefficients. |
commit | commitdiff | tree |
| 2015-04-17 |
Tianyi Liang | Patch for Kshitij's fix on requriePhase |
commit | commitdiff | tree |
| 2015-04-17 |
Kshitij Bansal | Merge pull request #72 from kbansal/decision-requirephase |
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Fix option --quant-fun-wd. Add mk_starexec script... |
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Handle (degenerate) case of synthesis conjectures for... |
commit | commitdiff | tree |
| 2015-04-15 |
Tim King | Enabling the regression test: test/regress/regress0... |
commit | commitdiff | tree |
| 2015-04-15 |
Clark Barrett | Fix for unconstrained bug. |
commit | commitdiff | tree |
| 2015-04-15 |
Tim King | Adding an example that violates an assertion during... |
commit | commitdiff | tree |
| 2015-04-13 |
Tim King | Making CVC4::theory::quantifiers::PrenexQuantMode publi... |
commit | commitdiff | tree |
| 2015-04-09 |
Kshitij Bansal | disable string reqressions timing out after change |
commit | commitdiff | tree |
| 2015-04-09 |
Kshitij Bansal | DE requests respect requirePhase |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix unsat-core issues related to rewrite rules, quantif... |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix performance issue with variable triggers + instanti... |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Bug fix negative contains cache. |
commit | commitdiff | tree |
| 2015-04-08 |
ajreynol | Make fun-def quantifiers carry the function app they... |
commit | commitdiff | tree |
| 2015-04-08 |
Dejan Jovanovic | Removing the reference to THEORY_BOOL from the equality... |
commit | commitdiff | tree |
| 2015-04-07 |
ajreynol | Minor fixes for cegqi. |
commit | commitdiff | tree |
| 2015-04-02 |
Kshitij Bansal | Merge pull request #71 from kbansal/const-are-triggers |
commit | commitdiff | tree |
| 2015-04-01 |
ajreynol | Improvements and bug fixes related to cbqi/cegqi. ... |
commit | commitdiff | tree |
| 2015-03-31 |
Kshitij Bansal | fix no return value warning |
commit | commitdiff | tree |
| 2015-03-31 |
Kshitij Bansal | fix echo command in --tear-down-incremental |
commit | commitdiff | tree |
| 2015-03-28 |
Tianyi Liang | printer change for string smtlib2 |
commit | commitdiff | tree |
| 2015-03-25 |
Kshitij Bansal | change const are triggers from false to true in equalit... |
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 |
| next |
projects / cvc5.git / shortlog