diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-27 12:26:14 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-27 12:26:14 -0500 |
commit | 11110b87cb70d9c4a6dc486319adbb7dfa59fedb (patch) | |
tree | 7ce951d48330be5d48deaa280388731d40ef2517 /src/expr/expr_manager_template.h | |
parent | c6aa453fe1c34481f83ca96f5feb8b1a7ad6c734 (diff) |
Make division chainable in the smt2 parser (#2367)
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 dce1a57a5..4e0ab700c 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -301,6 +301,19 @@ public: Expr mkAssociative(Kind kind, const std::vector<Expr>& children); /** + * Create an Expr by applying an binary left-associative operator to the + * children. For example, mkLeftAssociative( f, { a, b, c } ) returns + * f( f( a, b ), c ). + */ + Expr mkLeftAssociative(Kind kind, const std::vector<Expr>& children); + /** + * Create an Expr by applying an binary right-associative operator to the + * children. For example, mkRightAssociative( f, { a, b, c } ) returns + * f( a, f( b, c ) ). + */ + Expr mkRightAssociative(Kind kind, const std::vector<Expr>& children); + + /** * Determine whether Exprs of a particular Kind have operators. * @returns true if Exprs of Kind k have operators. */ |