projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1857318) | patch
* Reversing commit r4258 (which disabled failing regressions). Fixed the problem...
authorMorgan Deters <mdeters@gmail.com>
Mon, 27 Aug 2012 19:27:28 +0000 (19:27 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 27 Aug 2012 19:27:28 +0000 (19:27 +0000)
commit58c511a607a7a3560590b49f17ee3e92b364dbcf
tree0953f80fa0386b44dec50937fbee31dd837a7393tree
parent1857318ff8b072e07bc0a802960a7b87f119688dcommit | diff
* Reversing commit r4258 (which disabled failing regressions).  Fixed the problem so they're no longer failing (in the quantifiers rewriter).  Resolves bug #381.

* Added LAMBDA kind and type rule, and Node::isClosure().

(this commit was certified error- and warning-free by the test-and-commit script.)
src/expr/node.h diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/rewriterules/theory_rewriterules_type_rules.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history