Make division chainable in the smt2 parser (#2367)

2 files changed, 47 insertions, 23 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5d5c1ef68..e6b89b498 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -928,21 +928,21 @@ Expr ExprManager::mkAssociative(Kind kind,
       "Illegal kind in mkAssociative: %s",
       kind::kindToString(kind).c_str());
 
-  NodeManagerScope nms(d_nodeManager);
   const unsigned int max = maxArity(kind);
-  const unsigned int min = minArity(kind);
   unsigned int numChildren = children.size();
 
   /* If the number of children is within bounds, then there's nothing to do. */
   if( numChildren <= max ) {
     return mkExpr(kind,children);
   }
+  NodeManagerScope nms(d_nodeManager);
+  const unsigned int min = minArity(kind);
 
   std::vector<Expr>::const_iterator it = children.begin() ;
   std::vector<Expr>::const_iterator end = children.end() ;
 
   /* The new top-level children and the children of each sub node */
-  std::vector<Node> newChildren;
+  std::vector<Expr> newChildren;
   std::vector<Node> subChildren;
 
   while( it != end && numChildren > max ) {
@@ -953,39 +953,50 @@ Expr ExprManager::mkAssociative(Kind kind,
       subChildren.push_back(it->getNode());
     }
     Node subNode = d_nodeManager->mkNode(kind,subChildren);
-    newChildren.push_back(subNode);
+    newChildren.push_back(subNode.toExpr());
 
     subChildren.clear();
   }
 
-  /* If there's children left, "top off" the Expr. */
+  // add the leftover children
   if(numChildren > 0) {
-    /* If the leftovers are too few, just copy them into newChildren;
-     * otherwise make a new sub-node  */
-    if(numChildren < min) {
-      for(; it != end; ++it) {
-        newChildren.push_back(it->getNode());
-      }
-    } else {
-      for(; it != end; ++it) {
-        subChildren.push_back(it->getNode());
-      }
-      Node subNode = d_nodeManager->mkNode(kind, subChildren);
-      newChildren.push_back(subNode);
+    for (; it != end; ++it)
+    {
+      newChildren.push_back(*it);
     }
   }
 
-  /* It's inconceivable we could have enough children for this to fail
-   * (more than 2^32, in most cases?). */
-  AlwaysAssert( newChildren.size() <= max,
-                "Too many new children in mkAssociative" );
-
   /* It would be really weird if this happened (it would require
    * min > 2, for one thing), but let's make sure. */
   AlwaysAssert( newChildren.size() >= min,
                 "Too few new children in mkAssociative" );
 
-  return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
+  // recurse
+  return mkAssociative(kind, newChildren);
+}
+
+Expr ExprManager::mkLeftAssociative(Kind kind,
+                                    const std::vector<Expr>& children)
+{
+  NodeManagerScope nms(d_nodeManager);
+  Node n = children[0];
+  for (unsigned i = 1, size = children.size(); i < size; i++)
+  {
+    n = d_nodeManager->mkNode(kind, n, children[i].getNode());
+  }
+  return n.toExpr();
+}
+
+Expr ExprManager::mkRightAssociative(Kind kind,
+                                     const std::vector<Expr>& children)
+{
+  NodeManagerScope nms(d_nodeManager);
+  Node n = children[children.size() - 1];
+  for (unsigned i = children.size() - 1; i > 0;)
+  {
+    n = d_nodeManager->mkNode(kind, children[--i].getNode(), n);
+  }
+  return n.toExpr();
 }
 
 unsigned ExprManager::minArity(Kind kind) {
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.
    */