Added the capability to construct expressions by passing the operator instead of the kind, i.e.

Expr op = ..."f"...
em.mkExpr(op, children);

Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.

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 {