summaryrefslogtreecommitdiff
path: root/src/expr/metakind_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r--src/expr/metakind_template.h15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index fda2801be..57bfc51e5 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -141,6 +141,21 @@ ${metakind_canbeatomic}
return canBeAtomic[k];
}/* kindCanBeAtomic(k) */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+static inline Kind operatorKindToKind(Kind k) {
+ static const Kind kind2kind[] = {
+ kind::UNDEFINED_KIND, /* NULL_EXPR */
+${metakind_operatorKinds}
+ kind::UNDEFINED_KIND /* LAST_KIND */
+ };
+
+ return kind2kind[k];
+}
}/* CVC4::kind namespace */
namespace expr {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback