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 /test/unit/expr/node_manager_black.h | |
parent | aa21ac1746612b646e464615d4eeb07586f4ed36 (diff) |
First draft implementation of mkAssociative
Diffstat (limited to 'test/unit/expr/node_manager_black.h')
-rw-r--r-- | test/unit/expr/node_manager_black.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 6ff2b64e0..e3be1bedd 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -337,4 +337,21 @@ public: TS_ASSERT_EQUALS(ft.getRangeType(), booleanType); } + + void testMkNodeTooFew() { + 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 ); + } + + void testMkNodeTooMany() { + std::vector<Node> vars; + const unsigned int max = metakind::getUpperBoundForKind(AND); + TypeNode boolType = d_nodeManager->booleanType(); + for( unsigned int i = 0; i <= max; ++i ) { + vars.push_back( d_nodeManager->mkVar(boolType) ); + } + TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException ); + } + }; |