summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-12-09 12:17:26 -0800
committerGitHub <noreply@github.com>2020-12-09 12:17:26 -0800
commiteed1028716c90df8f26aa1afa948f2deeb1cbdb7 (patch)
tree9d005cb5cfbaabf83710b41db621f7c4b230a18a /test/unit
parentea41cab78f69fbd600784c6a8c990477fda2f7fe (diff)
google test: expr: Migrate kind_map_black. (#5640)
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/expr/CMakeLists.txt2
-rw-r--r--test/unit/expr/kind_map_black.cpp115
-rw-r--r--test/unit/expr/kind_map_black.h107
3 files changed, 116 insertions, 108 deletions
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 1b619b2f2..3d732df5e 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -14,7 +14,7 @@
cvc4_add_unit_test_black(attribute_black expr)
cvc4_add_unit_test_white(attribute_white expr)
cvc4_add_cxx_unit_test_black(kind_black expr)
-cvc4_add_cxx_unit_test_black(kind_map_black expr)
+cvc4_add_unit_test_black(kind_map_black expr)
cvc4_add_cxx_unit_test_black(node_black expr)
cvc4_add_cxx_unit_test_black(node_algorithm_black expr)
cvc4_add_cxx_unit_test_black(node_builder_black expr)
diff --git a/test/unit/expr/kind_map_black.cpp b/test/unit/expr/kind_map_black.cpp
new file mode 100644
index 000000000..0ad26d004
--- /dev/null
+++ b/test/unit/expr/kind_map_black.cpp
@@ -0,0 +1,115 @@
+/********************* */
+/*! \file kind_map_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. 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 <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind_map.h"
+#include "test_expr.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestExprBlackKindMap : public TestExprBlack
+{
+};
+
+TEST_F(TestExprBlackKindMap, simple)
+{
+ KindMap map;
+ ASSERT_TRUE(map.isEmpty());
+ map.set(AND);
+ ASSERT_FALSE(map.isEmpty());
+ KindMap map2 = map;
+ ASSERT_FALSE(map2.isEmpty());
+ EXPECT_EQ(map, map2);
+ ASSERT_TRUE(map.tst(AND));
+ ASSERT_TRUE(map2.tst(AND));
+ ASSERT_FALSE(map.tst(OR));
+ ASSERT_FALSE(map2.tst(OR));
+ map2 = ~map2;
+ ASSERT_TRUE(map2.tst(OR));
+ ASSERT_FALSE(map2.tst(AND));
+ EXPECT_NE(map, map2);
+ EXPECT_NE(map.begin(), map.end());
+ EXPECT_NE(map2.begin(), map2.end());
+ map &= ~AND;
+ ASSERT_TRUE(map.isEmpty());
+ map2.clear();
+ ASSERT_TRUE(map2.isEmpty());
+ EXPECT_EQ(map2, map);
+ EXPECT_EQ(map.begin(), map.end());
+ EXPECT_EQ(map2.begin(), map2.end());
+}
+
+TEST_F(TestExprBlackKindMap, iteration)
+{
+ KindMap m = AND & OR;
+ ASSERT_TRUE(m.isEmpty());
+ for (KindMap::iterator i = m.begin(); i != m.end(); ++i)
+ {
+ ASSERT_TRUE(false) << "expected empty iterator range";
+ }
+ m = AND | OR;
+ KindMap::iterator i = m.begin();
+ EXPECT_NE(i, m.end());
+ EXPECT_EQ(*i, AND);
+ ++i;
+ EXPECT_NE(i, m.end());
+ EXPECT_EQ(*i, OR);
+ ++i;
+ EXPECT_EQ(i, m.end());
+
+ m = ~m;
+ uint32_t k = 0;
+ for (i = m.begin(); i != m.end(); ++i, ++k)
+ {
+ while (k == AND || k == OR)
+ {
+ ++k;
+ }
+ EXPECT_NE(Kind(k), UNDEFINED_KIND);
+ EXPECT_NE(Kind(k), LAST_KIND);
+ EXPECT_EQ(*i, Kind(k));
+ }
+}
+
+TEST_F(TestExprBlackKindMap, construction)
+{
+ ASSERT_FALSE((AND & AND).isEmpty());
+ ASSERT_TRUE((AND & ~AND).isEmpty());
+ ASSERT_FALSE((AND & AND & AND).isEmpty());
+
+ ASSERT_FALSE((AND | AND).isEmpty());
+ ASSERT_FALSE((AND | ~AND).isEmpty());
+ ASSERT_TRUE(((AND | AND) & ~AND).isEmpty());
+ ASSERT_FALSE(((AND | OR) & ~AND).isEmpty());
+
+ ASSERT_TRUE((AND ^ AND).isEmpty());
+ ASSERT_FALSE((AND ^ OR).isEmpty());
+ ASSERT_FALSE((AND ^ AND ^ AND).isEmpty());
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_THROW(~LAST_KIND, AssertArgumentException);
+#endif
+}
+
+} // namespace test
+} // namespace CVC4
diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h
deleted file mode 100644
index 59d54c91f..000000000
--- a/test/unit/expr/kind_map_black.h
+++ /dev/null
@@ -1,107 +0,0 @@
-/********************* */
-/*! \file kind_map_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. 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, AssertArgumentException&);
-#endif /* CVC4_ASSERTIONS */
- }
-
-};/* class KindMapBlack */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback