From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Dec 2020 19:03:54 +0000 (-0600)
Subject: Add associative utilities to node manager (#5530)
X-Git-Tag: cvc5-1.0.0~2521
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f422a12f247b986ae8f6941e768ed75453fd1049;p=cvc5.git

Add associative utilities to node manager (#5530)

Required for updating the new API to use Node utilites as backend.

These utilities are copied directly from ExprManager and converted Expr -> Node.
---

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7c847d8ce..c70cfce3b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -951,6 +951,97 @@ Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
   return bvl;
 }
 
+Node NodeManager::mkAssociative(Kind kind, const std::vector<Node>& children)
+{
+  AlwaysAssert(kind::isAssociative(kind)) << "Illegal kind in mkAssociative";
+
+  const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+  size_t numChildren = children.size();
+
+  /* If the number of children is within bounds, then there's nothing to do. */
+  if (numChildren <= max)
+  {
+    return mkNode(kind, children);
+  }
+  const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+
+  std::vector<Node>::const_iterator it = children.begin();
+  std::vector<Node>::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<Node>::const_iterator next = it + max; it != next;
+         ++it, --numChildren)
+    {
+      subChildren.push_back(*it);
+    }
+    Node subNode = mkNode(kind, subChildren);
+    newChildren.push_back(subNode);
+
+    subChildren.clear();
+  }
+
+  // add the leftover children
+  if (numChildren > 0)
+  {
+    for (; it != end; ++it)
+    {
+      newChildren.push_back(*it);
+    }
+  }
+
+  /* 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";
+
+  // recurse
+  return mkAssociative(kind, newChildren);
+}
+
+Node NodeManager::mkLeftAssociative(Kind kind,
+                                    const std::vector<Node>& children)
+{
+  Node n = children[0];
+  for (size_t i = 1, size = children.size(); i < size; i++)
+  {
+    n = mkNode(kind, n, children[i]);
+  }
+  return n;
+}
+
+Node NodeManager::mkRightAssociative(Kind kind,
+                                     const std::vector<Node>& children)
+{
+  Node n = children[children.size() - 1];
+  for (size_t i = children.size() - 1; i > 0;)
+  {
+    n = mkNode(kind, children[--i], n);
+  }
+  return n;
+}
+
+Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children)
+{
+  if (children.size() == 2)
+  {
+    // if this is the case exactly 1 pair will be generated so the
+    // AND is not required
+    return mkNode(kind, children[0], children[1]);
+  }
+  std::vector<Node> cchildren;
+  for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++)
+  {
+    cchildren.push_back(mkNode(kind, children[i], children[i + 1]));
+  }
+  return mkNode(kind::AND, cchildren);
+}
+
 Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 99db9feb2..bbb076fbc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -538,6 +538,42 @@ class NodeManager {
   /** get the canonical bound variable list for function type tn */
   Node getBoundVarListForFunctionType( TypeNode tn );
 
+  /**
+   * Create an Node 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.
+   */
+  Node mkAssociative(Kind kind, const std::vector<Node>& children);
+
+  /**
+   * Create an Node by applying an binary left-associative operator to the
+   * children. For example, mkLeftAssociative( f, { a, b, c } ) returns
+   * f( f( a, b ), c ).
+   */
+  Node mkLeftAssociative(Kind kind, const std::vector<Node>& children);
+  /**
+   * Create an Node by applying an binary right-associative operator to the
+   * children. For example, mkRightAssociative( f, { a, b, c } ) returns
+   * f( a, f( b, c ) ).
+   */
+  Node mkRightAssociative(Kind kind, const std::vector<Node>& children);
+
+  /** make chain
+   *
+   * Given a kind k and arguments t_1, ..., t_n, this returns the
+   * conjunction of:
+   *  (k t_1 t_2) .... (k t_{n-1} t_n)
+   * It is expected that k is a kind denoting a predicate, and args is a list
+   * of terms of size >= 2 such that the terms above are well-typed.
+   */
+  Node mkChain(Kind kind, const std::vector<Node>& children);
+
   /**
    * Optional flags used to control behavior of NodeManager::mkSkolem().
    * They should be composed with a bitwise OR (e.g.,