diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-06 02:09:06 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-06 02:09:06 +0000 |
commit | 0deb883f8c5ba550fda8b90501890940fd916a1b (patch) | |
tree | 645e90ff08d9120f207970f302661a149b988714 /src/expr/expr_manager_template.h | |
parent | 4c7de64f3367940faf9c6af48631bc837795c46d (diff) |
datatype stuff in compatibility interface implemented
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 184556887..ade9a334d 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -194,6 +194,19 @@ public: Expr mkExpr(Kind kind, const std::vector<Expr>& children); /** + * Make an n-ary expression of given kind given a first arg and + * a vector of its remaining children (this can be useful where the + * kind is parameterized operator, so the first arg is really an + * arg to the kind to construct an operator) + * + * @param kind the kind of expression to build + * @param child1 the first subexpression + * @param children the remaining subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren); + + /** * Make a nullary parameterized expression with the given operator. * * @param opExpr the operator expression |