diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
commit | cfb3b789e26fdab73e733825950b24492c6c5e4c (patch) | |
tree | dec99da95dd6c1dd0def3adaa46d5e7e9e94b4e6 /src/expr | |
parent | aa21ac1746612b646e464615d4eeb07586f4ed36 (diff) |
First draft implementation of mkAssociative
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 57 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 13 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_template.h | 7 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 17 | ||||
-rw-r--r-- | src/expr/node_manager.h | 1 |
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); + }; /** |