diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/expr/kind_map_black.h | 109 |
2 files changed, 110 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index cef4590a3..f98f434c1 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -12,6 +12,7 @@ UNIT_TESTS = \ expr/node_white \ expr/node_black \ expr/kind_black \ + expr/kind_map_black \ expr/node_builder_black \ expr/node_manager_black \ expr/node_manager_white \ diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h new file mode 100644 index 000000000..e5bcdd298 --- /dev/null +++ b/test/unit/expr/kind_map_black.h @@ -0,0 +1,109 @@ +/********************* */ +/*! \file kind_map_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, 2011 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::KindMap + ** + ** Black box testing of CVC4::KindMap. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <string> +#include <sstream> + +#include "expr/kind_map.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class KindMapBlack : public CxxTest::TestSuite { + +public: + + void testSimple() { + KindMap map; + TS_ASSERT(map.isEmpty()); + map.set(AND); + TS_ASSERT(!map.isEmpty()); + KindMap map2 = map; + TS_ASSERT(!map2.isEmpty()); + TS_ASSERT_EQUALS(map, map2); + TS_ASSERT(map.tst(AND)); + TS_ASSERT(map2.tst(AND)); + TS_ASSERT(!map.tst(OR)); + TS_ASSERT(!map2.tst(OR)); + map2 = ~map2; + TS_ASSERT(map2.tst(OR)); + TS_ASSERT(!map2.tst(AND)); + TS_ASSERT(map != map2); + TS_ASSERT(map.begin() != map.end()); + TS_ASSERT(map2.begin() != map2.end()); + map &= ~AND; + TS_ASSERT(map.isEmpty()); + map2.clear(); + TS_ASSERT(map2.isEmpty()); + TS_ASSERT_EQUALS(map2, map); + TS_ASSERT_EQUALS(map.begin(), map.end()); + TS_ASSERT_EQUALS(map2.begin(), map2.end()); + } + + void testIteration() { + KindMap m = AND & OR; + TS_ASSERT(m.isEmpty()); + for(KindMap::iterator i = m.begin(); i != m.end(); ++i) { + TS_FAIL("expected empty iterator range"); + } + m = AND | OR; + KindMap::iterator i = m.begin(); + TS_ASSERT(i != m.end()); + TS_ASSERT_EQUALS(*i, AND); + ++i; + TS_ASSERT(i != m.end()); + TS_ASSERT_EQUALS(*i, OR); + ++i; + TS_ASSERT(i == m.end()); + + m = ~m; + unsigned k = 0; + for(i = m.begin(); i != m.end(); ++i, ++k) { + while(k == AND || k == OR) { + ++k; + } + TS_ASSERT_DIFFERS(Kind(k), UNDEFINED_KIND); + TS_ASSERT_DIFFERS(Kind(k), LAST_KIND); + TS_ASSERT_EQUALS(*i, Kind(k)); + } + } + + void testConstruction() { + TS_ASSERT(!(AND & AND).isEmpty()); + TS_ASSERT((AND & ~AND).isEmpty()); + TS_ASSERT(!(AND & AND & AND).isEmpty()); + + TS_ASSERT(!(AND | AND).isEmpty()); + TS_ASSERT(!(AND | ~AND).isEmpty()); + TS_ASSERT(((AND | AND) & ~AND).isEmpty()); + TS_ASSERT(!((AND | OR) & ~AND).isEmpty()); + + TS_ASSERT((AND ^ AND).isEmpty()); + TS_ASSERT(!(AND ^ OR).isEmpty()); + TS_ASSERT(!(AND ^ AND ^ AND).isEmpty()); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException); +#endif /* CVC4_ASSERTIONS */ + } + +};/* class KindMapBlack */ |