summaryrefslogtreecommitdiff
path: root/src/expr/metakind_template.h
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2010-04-30 23:55:18 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2010-04-30 23:55:18 +0000
commitcb9a9b98b018106a02b31f2442f347a944d8dda8 (patch)
tree1669047e13e1224114e9fcea83b212dd6d72836d /src/expr/metakind_template.h
parent349131957e91150c24a9c69f5e1f04e34494b0c6 (diff)
Fix for bug 115, mapping was going in the wrong direction.
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r--src/expr/metakind_template.h8
1 files changed, 3 insertions, 5 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 57bfc51e5..5b0ac150b 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -148,13 +148,11 @@ ${metakind_canbeatomic}
* VARIABLE to APPLY_UF.
*/
static inline Kind operatorKindToKind(Kind k) {
- static const Kind kind2kind[] = {
- kind::UNDEFINED_KIND, /* NULL_EXPR */
+ switch (k) {
${metakind_operatorKinds}
- kind::UNDEFINED_KIND /* LAST_KIND */
+ default:
+ return kind::UNDEFINED_KIND; /* LAST_KIND */
};
-
- return kind2kind[k];
}
}/* CVC4::kind namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback