diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-27 13:55:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-27 13:55:08 -0500 |
commit | dc6e0f9c0489e733a70e6715b8dfba4e7fa4f0bd (patch) | |
tree | f9a52b7fb2054a0c1a31e5433e8e1c507d21e9a6 /src/theory/quantifiers/term_util.cpp | |
parent | 68a994dbb7527b6f98975bbb776687413f23d451 (diff) |
Core improvements to extended rewriter (#1820)
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 |