diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
commit | 349131957e91150c24a9c69f5e1f04e34494b0c6 (patch) | |
tree | 8012c2475dde1f1177f693643fb1a07e89c29538 /src/expr/metakind_template.h | |
parent | ac8b46fe3b5256e387da724b7c3abfb59d25531e (diff) |
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.
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r-- | src/expr/metakind_template.h | 15 |
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 { |