diff options
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index a80737fe2..9b04ce9b5 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -811,6 +811,11 @@ Node TermUtil::mkNegate(Kind notk, Node n) return NodeManager::currentNM()->mkNode(notk, n); } +bool TermUtil::isNegate(Kind k) +{ + return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS; +} + bool TermUtil::isAssoc( Kind k ) { return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR |