diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 21:56:35 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 21:56:35 +0000 |
commit | 9e28a6013e0c2c926d79254ad1e419228ea4d337 (patch) | |
tree | ea3996937d5b925df6f3def6fce64cc8d300a40e | |
parent | 9c0b0f4c42619d1de116dc73f2c5111fd27ea85c (diff) |
Fixing test failures in production build
-rw-r--r-- | src/expr/expr_manager_template.cpp | 87 | ||||
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 6 |
3 files changed, 54 insertions, 41 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 8cfd50f08..bf0e2f96e 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -252,61 +252,68 @@ Expr ExprManager::mkVar(const Type& type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { - Assert( metakind::isAssociative(kind), "Illegal kind in mkAssociative" ); + CheckArgument( metakind::isAssociative(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); - } 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); + } + + std::vector<Expr>::const_iterator it = children.begin() ; + std::vector<Expr>::const_iterator end = children.end() ; - subChildren.clear(); + /* 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); + /* 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" ); + /* 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" ); - return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) ); - } + /* 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) ); } unsigned ExprManager::minArity(Kind kind) { diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index c48afc10d..dc203061c 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,7 +1,7 @@ # All unit tests UNIT_TESTS = \ expr/expr_public \ - expr/expr_manager_public \ + expr/expr_manager_public \ expr/node_white \ expr/node_black \ expr/kind_black \ diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index e3be1bedd..78c38d782 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -338,13 +338,18 @@ public: } + /* This test is only valid if assertions are enabled. */ void testMkNodeTooFew() { +#ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( d_nodeManager->mkNode(AND), AssertionException ); Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() ); TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException ); +#endif } + /* This test is only valid if assertions are enabled. */ void testMkNodeTooMany() { +#ifdef CVC4_ASSERTIONS std::vector<Node> vars; const unsigned int max = metakind::getUpperBoundForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); @@ -352,6 +357,7 @@ public: vars.push_back( d_nodeManager->mkVar(boolType) ); } TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException ); +#endif } }; |