diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 20 | ||||
-rw-r--r-- | test/unit/Makefile.tests | 23 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 50 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 186 |
4 files changed, 241 insertions, 38 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 7a1b75cbc..84465127b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -24,8 +24,6 @@ TEST_DEPS = \ $(TEST_DEPS_DIST) \ $(TEST_DEPS_NODIST) -@mk_include@ @srcdir@/Makefile.tests - if HAVE_CXXTESTGEN AM_CPPFLAGS = \ @@ -46,8 +44,6 @@ AM_LDFLAGS_BLACK = \ AM_LDFLAGS_PUBLIC = \ @abs_top_builddir@/src/libcvc4.la -TESTS = $(UNIT_TESTS) - EXTRA_DIST = \ no_cxxtest \ $(TEST_DEPS_DIST) @@ -57,9 +53,17 @@ noinst_LTLIBRARIES = libdummy.la libdummy_la_SOURCES = expr/node_black.cpp libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la -$(TESTS:%=%.cpp): %.cpp: %.h +MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) + +@mk_include@ @srcdir@/Makefile.tests + +# We leave "TESTS" empty here; it's handled in Makefile.tests (see +# that file for comment) +# TESTS = + +$(UNIT_TESTS:%=%.cpp): %.cpp: %.h mkdir -p `dirname "$@"` - @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<" + $(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<" $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo @@ -70,15 +74,13 @@ $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo -MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp) - else # force a user-visible failure for "make check" TESTS = no_cxxtest EXTRA_DIST = \ - $(UNIT_TESTS) \ + $(UNIT_TESTS:%=%.cpp) \ $(TEST_DEPS_DIST) endif diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests index c542259b1..4f2f3dd5f 100644 --- a/test/unit/Makefile.tests +++ b/test/unit/Makefile.tests @@ -1,5 +1,20 @@ -TESTS := $(filter $(TEST_PREFIX)%,$(TESTS)) +# This makefile is separated because it's not under automake control. +# This gets confusing, because we want: +# +# 1. to (re)build only the tests in the "filtered" set of tests +# (those that we're going to run) +# 2. run only the tests in the "filtered" set of tests. +# +# It's a pain to make automake happy. -WHITE_TESTS = $(filter %_white,$(TESTS)) -BLACK_TESTS = $(filter %_black,$(TESTS)) -PUBLIC_TESTS = $(filter %_public,$(TESTS)) +# Add "filtered" tests to the set of TESTS +TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS)) + +# subsets of the tests, based on name +WHITE_TESTS = $(filter %_white,$(UNIT_TESTS)) +BLACK_TESTS = $(filter %_black,$(UNIT_TESTS)) +PUBLIC_TESTS = $(filter %_public,$(UNIT_TESTS)) + +# This rule forces automake to correctly build our filtered +# set of tests +check-TESTS: $(TESTS) diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index fd2cf3332..0693b48db 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -39,7 +39,7 @@ public: d_scope = new NodeManagerScope(d_nm); } - void tearDown(){ + void tearDown() { delete d_nm; delete d_scope; } @@ -55,7 +55,7 @@ public: Node::null(); } - void testIsNull(){ + void testIsNull() { /* bool isNull() const; */ Node a = Node::null(); @@ -73,7 +73,7 @@ public: Node e(Node::null()); } - void testDestructor(){ + void testDestructor() { /* No access to internals ? * Makes sense to only test that this is crash free. */ @@ -84,7 +84,7 @@ public: } /*tests: bool operator==(const Node& e) const */ - void testOperatorEquals(){ + void testOperatorEquals() { Node a, b, c; b = d_nm->mkVar(); @@ -122,7 +122,7 @@ public: } /* operator!= */ - void testOperatorNotEquals(){ + void testOperatorNotEquals() { Node a, b, c; @@ -157,7 +157,7 @@ public: } - void testOperatorSquare(){ + void testOperatorSquare() { /*Node operator[](int i) const */ //Basic bounds check on a node w/out children @@ -183,7 +183,7 @@ public: } /*tests: Node& operator=(const Node&); */ - void testOperatorAssign(){ + void testOperatorAssign() { Node a, b; Node c = d_nm->mkNode(NOT); @@ -197,7 +197,7 @@ public: TS_ASSERT(a==c); } - void testOperatorLessThan(){ + void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation * in the black box tests. */ @@ -232,13 +232,13 @@ public: std::vector<Node> chain; int N = 500; Node curr = d_nm->mkNode(NULL_EXPR); - for(int i=0;i<N;i++){ + for(int i=0;i<N;i++) { chain.push_back(curr); curr = d_nm->mkNode(AND,curr); } - for(int i=0;i<N;i++){ - for(int j=i+1;j<N;j++){ + for(int i=0;i<N;i++) { + for(int j=i+1;j<N;j++) { Node chain_i = chain[i]; Node chain_j = chain[j]; TS_ASSERT(chain_i<chain_j); @@ -247,7 +247,7 @@ public: } - void testHash(){ + void testHash() { /* Not sure how to test this except survial... */ Node a = d_nm->mkNode(ITE); Node b = d_nm->mkNode(ITE); @@ -257,7 +257,7 @@ public: - void testEqExpr(){ + void testEqExpr() { /*Node eqExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -272,7 +272,7 @@ public: TS_ASSERT(eq[1] == right); } - void testNotExpr(){ + void testNotExpr() { /* Node notExpr() const;*/ Node child = d_nm->mkNode(TRUE); @@ -284,7 +284,7 @@ public: TS_ASSERT(parent[0] == child); } - void testAndExpr(){ + void testAndExpr() { /*Node andExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -300,7 +300,7 @@ public: } - void testOrExpr(){ + void testOrExpr() { /*Node orExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -316,7 +316,7 @@ public: } - void testIteExpr(){ + void testIteExpr() { /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/ Node cnd = d_nm->mkNode(PLUS); @@ -333,7 +333,7 @@ public: TS_ASSERT(*(++(++ite.begin())) == elseBranch); } - void testIffExpr(){ + void testIffExpr() { /* Node iffExpr(const Node& right) const; */ Node left = d_nm->mkNode(TRUE); @@ -349,7 +349,7 @@ public: } - void testImpExpr(){ + void testImpExpr() { /* Node impExpr(const Node& right) const; */ Node left = d_nm->mkNode(TRUE); Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); @@ -363,7 +363,7 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testXorExpr(){ + void testXorExpr() { /*Node xorExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); @@ -377,26 +377,26 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testPlusExpr(){ + void testPlusExpr() { /*Node plusExpr(const Node& right) const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testUMinusExpr(){ + void testUMinusExpr() { /*Node uMinusExpr() const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testMultExpr(){ + void testMultExpr() { /* Node multExpr(const Node& right) const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testKindSingleton(Kind k){ + void testKindSingleton(Kind k) { Node n = d_nm->mkNode(k); TS_ASSERT(k == n.getKind()); } - void testGetKind(){ + void testGetKind() { /*inline Kind getKind() const; */ testKindSingleton(NOT); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index c097f2758..73a7b1a54 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -15,13 +15,46 @@ #include <cxxtest/TestSuite.h> +#include <string> + +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" #include "expr/node.h" +#include "expr/attribute.h" using namespace CVC4; +using namespace CVC4::expr; +using namespace std; + +struct Test1; +struct Test2; +struct Test3; +struct Test4; + +typedef Attribute<Test1, std::string> TestStringAttr1; +typedef Attribute<Test2, std::string> TestStringAttr2; + +typedef Attribute<Test3, bool> TestFlag1; +typedef Attribute<Test4, bool> TestFlag2; class NodeWhite : public CxxTest::TestSuite { + + NodeManagerScope *d_scope; + NodeManager *d_nm; + public: + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_nm; + delete d_scope; + } + void testNull() { Node::s_null; } @@ -29,4 +62,157 @@ public: void testCopyCtor() { Node e(Node::s_null); } + + void testBuilder() { + NodeBuilder<> b; + TS_ASSERT(b.d_ev->getId() == 0); + TS_ASSERT(b.d_ev->getKind() == UNDEFINED_KIND); + TS_ASSERT(b.d_ev->getNumChildren() == 0); + /* etc. */ + } + + void testAttributeIds() { + TS_ASSERT(VarNameAttr::s_id == 0); + TS_ASSERT(TestStringAttr1::s_id == 1); + TS_ASSERT(TestStringAttr2::s_id == 2); + TS_ASSERT(attr::LastAttributeId<string>::s_id == 3); + + TS_ASSERT(TypeAttr::s_id == 0); + TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1); + + TS_ASSERT(TestFlag1::s_id == 0); + TS_ASSERT(TestFlag2::s_id == 1); + TS_ASSERT(attr::LastAttributeId<bool>::s_id == 2); + TS_ASSERT(TestFlag1::s_bit == 0); + TS_ASSERT(TestFlag2::s_bit == 1); + TS_ASSERT(attr::BitAssignment::s_bit == 2); + } + + void testAttributes() { + AttributeManager& am = d_nm->d_am; + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node unnamed = d_nm->mkVar(); + + a.setAttribute(VarNameAttr(), "a"); + b.setAttribute(VarNameAttr(), "b"); + c.setAttribute(VarNameAttr(), "c"); + + a.setAttribute(TestFlag1(), true); + b.setAttribute(TestFlag1(), false); + c.setAttribute(TestFlag1(), false); + unnamed.setAttribute(TestFlag1(), true); + + a.setAttribute(TestFlag2(), false); + b.setAttribute(TestFlag2(), true); + c.setAttribute(TestFlag2(), true); + unnamed.setAttribute(TestFlag2(), false); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr1())); + TS_ASSERT(! b.hasAttribute(TestStringAttr1())); + TS_ASSERT(! c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + TS_ASSERT(a.getAttribute(TestFlag1())); + TS_ASSERT(! b.getAttribute(TestFlag1())); + TS_ASSERT(! c.getAttribute(TestFlag1())); + TS_ASSERT(unnamed.getAttribute(TestFlag1())); + + TS_ASSERT(! a.getAttribute(TestFlag2())); + TS_ASSERT(b.getAttribute(TestFlag2())); + TS_ASSERT(c.getAttribute(TestFlag2())); + TS_ASSERT(! unnamed.getAttribute(TestFlag2())); + + a.setAttribute(TestStringAttr1(), "foo"); + b.setAttribute(TestStringAttr1(), "bar"); + c.setAttribute(TestStringAttr1(), "baz"); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(a.hasAttribute(TestStringAttr1())); + TS_ASSERT(b.hasAttribute(TestStringAttr1())); + TS_ASSERT(c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + a.setAttribute(VarNameAttr(), "b"); + b.setAttribute(VarNameAttr(), "c"); + c.setAttribute(VarNameAttr(), "a"); + + TS_ASSERT(c.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(a.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + } }; |