diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-02 13:03:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-02 13:03:54 -0600 |
commit | f422a12f247b986ae8f6941e768ed75453fd1049 (patch) | |
tree | a111b431cdb2063488525b943f983c0779d2e835 | |
parent | 8a59d0aa0d1bacdfd1194c16ae24c3b7349c9e3f (diff) |
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.
-rw-r--r-- | src/expr/node_manager.cpp | 91 | ||||
-rw-r--r-- | src/expr/node_manager.h | 36 |
2 files changed, 127 insertions, 0 deletions
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 @@ -539,6 +539,42 @@ class NodeManager { 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., * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT |