First draft implementation of mkAssociative

6 files changed, 102 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6fd33113b..59dbf77e5 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -250,6 +250,63 @@ Expr ExprManager::mkVar(const Type& type) {
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 
+Expr ExprManager::mkAssociative(Kind kind,
+                                const std::vector<Expr>& children) {
+  NodeManagerScope nms(d_nodeManager);
+  const unsigned int max = maxArity(kind);
+  const unsigned int min = minArity(kind);
+  unsigned int numChildren = children.size();
+
+  if( numChildren <= max ) {
+    return mkExpr(kind,children);
+  } else {
+    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<Node> subChildren;
+
+    while( it != end && numChildren > max ) {
+      /* Grab the next max children and make a node for them. */
+      for( std::vector<Expr>::const_iterator next = it + max;
+           it != next;
+           ++it, --numChildren ) {
+        subChildren.push_back(it->getNode());
+      }
+      Node subNode = d_nodeManager->mkNode(kind,subChildren);
+      newChildren.push_back(subNode);
+
+      subChildren.clear();
+    }
+
+    /* If there's children left, "top off" the Expr. */
+    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);
+      }
+    }
+
+    /* It would be really weird if this happened, but let's make sure. */
+    Assert( newChildren.size() >= min, "Too few new children in mkAssociative" );
+    /* We could call mkAssociative recursively with newChildren in this case, but it
+     * would take an astonishing number of children to make this fail. */
+    Assert( newChildren.size() <= max, "Too many new children in mkAssociative" );
+
+    return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
+  }
+}
+
 unsigned ExprManager::minArity(Kind kind) {
   return metakind::getLowerBoundForKind(kind);
 }
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);
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 5c4e30a0c..edd49f032 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -140,6 +140,13 @@ size_t Expr::getNumChildren() const {
   return d_node->getNumChildren();
 }
 
+Expr Expr::getChild(unsigned int i) const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(i >= 0 && i < d_node->getNumChildren(), "Child index out of bounds");
+  return Expr(d_exprManager,new Node((*d_node)[i]));
+}
+
 bool Expr::hasOperator() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 08dd1d25f..6597d5f14 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -164,6 +164,13 @@ public:
   size_t getNumChildren() const;
 
   /**
+   * Returns the i'th child of this expression.
+   * @param i the index of the child to retrieve
+   * @return the child
+   */
+  Expr getChild(unsigned int i) const;
+
+  /**
    * Check if this is an expression that has an operator.
    * @return true if this expression has an operator
    */
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 3c17507cf..b2e45533a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -292,6 +292,23 @@ ${metakind_ubchildren}
   return ubs[k];
 }
 
+/** Returns true if the given kind is associative. This is used by ExprManager to
+ * decide whether it's safe to modify big expressions by changing the grouping of
+ * the arguments. */
+/* TODO: This could be generated. */
+inline bool isAssociative(::CVC4::Kind k) {
+  switch(k) {
+  case kind::AND:
+  case kind::OR:
+  case kind::MULT:
+  case kind::PLUS:
+    return true;
+
+  default:
+    return false;
+  }
+}
+
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a5f82b489..5642a8372 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -519,6 +519,7 @@ public:
    * Get the type for the given node.
    */
   TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate);
+
 };
 
 /**