Make division chainable in the smt2 parser (#2367)

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.
    */