diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-07-11 01:55:31 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-10 23:55:31 -0500 |
commit | 9aab4da2460b62273ac937ad96b7b6695b904e0d (patch) | |
tree | 8fc1a5ef0f0bebc22768401c7c061182497fcf45 /src/expr/expr_manager_template.h | |
parent | b31f0397bc02b8d903dc7c1e82a1f1ae53729fa1 (diff) |
Adding test for whether a kind is n-ary (#4718)
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index db5d22fa8..3f180e951 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -574,6 +574,11 @@ class CVC4_PUBLIC ExprManager { /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + /** Whether a kind is n-ary. The test is based on n-ary kinds having their + * maximal arity as the maximal possible number of children of a node. + **/ + static bool isNAryKind(Kind fun); + /** * Return the datatype at the given index owned by this class. Type nodes are * associated with datatypes through the DatatypeIndexConstant class. The |