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.h | |
| parent | 68a994dbb7527b6f98975bbb776687413f23d451 (diff) | |
Core improvements to extended rewriter (#1820)
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index df88c1b30..70f8bbcee 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -291,6 +291,11 @@ public: static int getTermDepth( Node n ); /** simple negate */ static Node simpleNegate( Node n ); + /** is the kind k a negation kind? + * + * A kind k is a negation kind if <k>( <k>( n ) ) = n. + */ + static bool isNegate(Kind k); /** * Make negated term, returns the negation of n wrt Kind notk, eliminating * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x. |