* 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.)

1 files changed, 8 insertions, 0 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 0ce042654..7108ba74a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -453,6 +453,14 @@ public:
     return getMetaKind() == kind::metakind::VARIABLE;
   }
 
+  inline bool isClosure() const {
+    assertTNodeNotExpired();
+    return getKind() == kind::LAMBDA ||
+           getKind() == kind::FORALL ||
+           getKind() == kind::EXISTS ||
+           getKind() == kind::REWRITE_RULE;
+  }
+
   /**
    * Returns the unique id of this node
    * @return the ud