diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
commit | cfb3b789e26fdab73e733825950b24492c6c5e4c (patch) | |
tree | dec99da95dd6c1dd0def3adaa46d5e7e9e94b4e6 /src/expr/metakind_template.h | |
parent | aa21ac1746612b646e464615d4eeb07586f4ed36 (diff) |
First draft implementation of mkAssociative
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r-- | src/expr/metakind_template.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 3c17507cf..b2e45533a 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -292,6 +292,23 @@ ${metakind_ubchildren} return ubs[k]; } +/** Returns true if the given kind is associative. This is used by ExprManager to + * decide whether it's safe to modify big expressions by changing the grouping of + * the arguments. */ +/* TODO: This could be generated. */ +inline bool isAssociative(::CVC4::Kind k) { + switch(k) { + case kind::AND: + case kind::OR: + case kind::MULT: + case kind::PLUS: + return true; + + default: + return false; + } +} + }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ }/* CVC4 namespace */ |