diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-03-15 17:01:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-15 17:01:42 -0500 |
| commit | e8f23236b7f797fd3cd8900df0422d44f1a6a7e0 (patch) | |
| tree | d0f8f1167e34509b15797e2a3b78cd21d9dff82f /src/expr/node.h | |
| parent | a74e32e26d33e18b84edee4b27e352afc5271eef (diff) | |
Adding capture avoiding substitution (#2867)
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 50add7b17..003863c8e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -459,7 +459,7 @@ public: assertTNodeNotExpired(); return getMetaKind() == kind::metakind::VARIABLE; } - + /** * Returns true if this node represents a nullary operator */ @@ -467,12 +467,11 @@ public: assertTNodeNotExpired(); return getMetaKind() == kind::metakind::NULLARY_OPERATOR; } - + inline bool isClosure() const { assertTNodeNotExpired(); return getKind() == kind::LAMBDA || getKind() == kind::FORALL - || getKind() == kind::EXISTS || getKind() == kind::REWRITE_RULE - || getKind() == kind::CHOICE; + || getKind() == kind::EXISTS || getKind() == kind::CHOICE; } /** |