summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-07 21:42:51 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-07 21:42:51 +0000
commit557e6c09dcc9068e848796772bc775542f4fc599 (patch)
treef20e6c9b1b6c7312e99ecc89d8a4d45bd64642aa /test
parentf7668d89c65b66a8aa5b17a19f56831d48878298 (diff)
NodeSelfIterator implementation and unit test (resolves bug #204); also fix ParserBlack unit test initialization
Diffstat (limited to 'test')
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/node_black.h4
-rw-r--r--test/unit/expr/node_self_iterator_black.h81
-rw-r--r--test/unit/parser/parser_black.h38
4 files changed, 118 insertions, 6 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 059d1d163..83dc888d4 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -16,6 +16,7 @@ UNIT_TESTS = \
expr/attribute_white \
expr/attribute_black \
expr/declaration_scope_black \
+ expr/node_self_iterator_black \
parser/parser_black \
parser/parser_builder_black \
prop/cnf_stream_black \
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6c5d8888f..5389e1308 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -39,8 +39,8 @@ private:
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
- TypeNode *d_booleanType;
- TypeNode *d_realType;
+ TypeNode* d_booleanType;
+ TypeNode* d_realType;
public:
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
new file mode 100644
index 000000000..5627a9db5
--- /dev/null
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -0,0 +1,81 @@
+/********************* */
+/*! \file node_self_iterator_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::expr::NodeSelfIterator
+ **
+ ** Black box testing of CVC4::expr::NodeSelfIterator
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_self_iterator.h"
+#include "expr/node_builder.h"
+#include "expr/convenience_node_builders.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+using namespace CVC4::expr;
+using namespace std;
+
+class NodeSelfIteratorBlack : public CxxTest::TestSuite {
+private:
+
+ Context* d_ctxt;
+ NodeManager* d_nodeManager;
+ NodeManagerScope* d_scope;
+ TypeNode* d_booleanType;
+ TypeNode* d_realType;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nodeManager = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nodeManager);
+ d_booleanType = new TypeNode(d_nodeManager->booleanType());
+ d_realType = new TypeNode(d_nodeManager->realType());
+ }
+
+ void tearDown() {
+ delete d_booleanType;
+ delete d_scope;
+ delete d_nodeManager;
+ delete d_ctxt;
+ }
+
+ void testSelfIteration() {
+ Node x = d_nodeManager->mkVar("x", *d_booleanType);
+ Node y = d_nodeManager->mkVar("y", *d_booleanType);
+ Node x_and_y = x && y;
+ NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
+ TS_ASSERT(i != x_and_y.end());
+ TS_ASSERT(j != x_and_y.end());
+ TS_ASSERT(*i == x_and_y);
+ TS_ASSERT(*j == x_and_y);
+ TS_ASSERT(*i++ == x_and_y);
+ TS_ASSERT(*j++ == x_and_y);
+ TS_ASSERT(i == NodeSelfIterator::selfEnd(x_and_y));
+ TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
+ TS_ASSERT(i == x_and_y.end());
+ TS_ASSERT(j == x_and_y.end());
+ i = x_and_y.begin();
+ TS_ASSERT(i != x_and_y.end());
+ TS_ASSERT(*i == x);
+ TS_ASSERT(*++i == y);
+ TS_ASSERT(++i == x_and_y.end());
+ }
+
+};
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 0e0835327..88a6eaf57 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -169,21 +169,33 @@ protected:
}
ParserBlack(InputLanguage lang) :
- d_lang(lang),
- d_exprManager(new ExprManager()) {
+ d_lang(lang) {
}
-public:
- virtual ~ParserBlack() {
+ void setUp() {
+cout << "SET UP\n";
+ d_exprManager = new ExprManager;
+ }
+
+ void tearDown() {
delete d_exprManager;
}
};
class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
+ typedef ParserBlack super;
public:
Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void testGoodCvc4Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("ASSERT TRUE;");
@@ -228,9 +240,19 @@ public:
};
class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
+ typedef ParserBlack super;
+
public:
SmtParserTest() : ParserBlack(LANG_SMTLIB) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void testGoodSmtInputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("(benchmark foo :assumption true)");
@@ -286,6 +308,14 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
public:
Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void setupContext(Smt2& parser) {
parser.addTheory(Smt2::THEORY_CORE);
super::setupContext(parser);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback