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/expr_manager_template.h | |
parent | aa21ac1746612b646e464615d4eeb07586f4ed36 (diff) |
First draft implementation of mkAssociative
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 323f21469..4cde091ac 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -180,6 +180,19 @@ public: template <class T> Expr mkConst(const T&); + /** Create an Expr by applying an associative operator to the children. + * If <code>children.size()</code> is greater than the max arity for + * <code>kind</code>, then the expression will be broken up into + * suitably-sized chunks, taking advantage of the associativity of + * <code>kind</code>. For example, if kind <code>FOO</code> has max arity + * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return + * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>. + * The order of the arguments will be preserved in a left-to-right + * traversal of the resulting tree. + */ + Expr mkAssociative(Kind kind, const std::vector<Expr>& children); + + /** Make a function type from domain to range. */ FunctionType mkFunctionType(const Type& domain, const Type& range); |