From 9aab4da2460b62273ac937ad96b7b6695b904e0d Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Sat, 11 Jul 2020 01:55:31 -0300 Subject: Adding test for whether a kind is n-ary (#4718) --- src/expr/expr_manager_template.h | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/expr/expr_manager_template.h') 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 -- cgit v1.2.3