From: Christopher L. Conway Date: Wed, 22 Sep 2010 20:22:16 +0000 (+0000) Subject: Fixing NodeBuilderBlack X-Git-Tag: cvc5-1.0.0~8853 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb0fc300c810f68f1e901413272c6658e31d60f9;p=cvc5.git Fixing NodeBuilderBlack --- diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index e6f8116fc..131d96bb9 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -43,6 +43,7 @@ private: NodeManager* d_nm; NodeManagerScope* d_scope; TypeNode* d_booleanType; + TypeNode* d_integerType; TypeNode* d_realType; public: @@ -52,13 +53,16 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - specKind = PLUS; + specKind = AND; + d_integerType = new TypeNode(d_nm->integerType()); d_booleanType = new TypeNode(d_nm->booleanType()); d_realType = new TypeNode(d_nm->realType()); } void tearDown() { + delete d_integerType; delete d_booleanType; + delete d_realType; delete d_scope; delete d_nm; delete d_ctxt; @@ -253,11 +257,15 @@ public: /* Kind getKind() const; */ NodeBuilder<> noKind; TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); - push_back(noKind, K); + + Node x( d_nm->mkVar( *d_integerType ) ); + noKind << x << x; + // push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); - noKind << specKind; - TS_ASSERT_EQUALS(noKind.getKind(), specKind); + noKind << PLUS; + + TS_ASSERT_EQUALS(noKind.getKind(), PLUS); Node n = noKind; @@ -265,39 +273,39 @@ public: TS_ASSERT_THROWS(noKind.getKind(), AssertionException); #endif /* CVC4_ASSERTIONS */ - NodeBuilder<> spec(specKind); - TS_ASSERT_EQUALS(spec.getKind(), specKind); - push_back(spec, K); - TS_ASSERT_EQUALS(spec.getKind(), specKind); + NodeBuilder<> spec(PLUS); + TS_ASSERT_EQUALS(spec.getKind(), PLUS); + spec << x << x ; + TS_ASSERT_EQUALS(spec.getKind(), PLUS); } void testGetNumChildren() { /* unsigned getNumChildren() const; */ + Node x( d_nm->mkVar( *d_integerType ) ); NodeBuilder<> nb; TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); - nb << specKind; - push_back(nb, K); + nb << PLUS << x << x; - TS_ASSERT_EQUALS(nb.getNumChildren(), K); + TS_ASSERT_EQUALS(nb.getNumChildren(), 2u); - push_back(nb, K); - TS_ASSERT_EQUALS(nb.getNumChildren(), K + K); + nb << x << x; + TS_ASSERT_EQUALS(nb.getNumChildren(), 4u); Node n = nb;// avoid warning on clear() nb.clear(); TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); - nb.clear(specKind); + nb.clear(PLUS); TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); - push_back(nb, K); + nb << x << x << x; - TS_ASSERT_EQUALS(nb.getNumChildren(), K); + TS_ASSERT_EQUALS(nb.getNumChildren(), 3u); - push_back(nb, K); - TS_ASSERT_EQUALS(nb.getNumChildren(), K + K); + nb << x << x << x; + TS_ASSERT_EQUALS(nb.getNumChildren(), 6u); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( nb << specKind, AssertionException ); + TS_ASSERT_THROWS( nb << PLUS, AssertionException ); n = nb; TS_ASSERT_THROWS( nb.getNumChildren(), AssertionException ); #endif /* CVC4_ASSERTIONS */ @@ -317,7 +325,7 @@ public: Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(arr[-1], AssertionException); + TS_ASSERT_THROWS(arr[-1], AssertionException&); TS_ASSERT_THROWS(arr[0], AssertionException); #endif /* CVC4_ASSERTIONS */