google test: expr: Migrate kind_black. (#5634)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 10 Dec 2020 14:11:43 +0000 (06:11 -0800)
committerGitHub <noreply@github.com>
Thu, 10 Dec 2020 14:11:43 +0000 (15:11 +0100)
test/unit/expr/CMakeLists.txt
test/unit/expr/kind_black.cpp [new file with mode: 0644]
test/unit/expr/kind_black.h [deleted file]

index 3d732df5e9c6c979c36da25cdc9c5d0a3d6805af..8494064fbd0041c711df077b3d5ccaf980548959 100644 (file)
@@ -13,7 +13,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_unit_test_black(kind_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)
diff --git a/test/unit/expr/kind_black.cpp b/test/unit/expr/kind_black.cpp
new file mode 100644 (file)
index 0000000..93b7c15
--- /dev/null
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file kind_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, 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::Kind.
+ **
+ ** Black box testing of CVC4::Kind.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind.h"
+#include "test_expr.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestExprBlackKind : public TestExprBlack
+{
+ protected:
+  void SetUp() override
+  {
+    undefined = UNDEFINED_KIND;
+    null = NULL_EXPR;
+    last = LAST_KIND;
+    beyond = ((int32_t)LAST_KIND) + 1;
+    unknown = (Kind)beyond;
+  }
+
+  bool string_is_as_expected(Kind k, const char* s)
+  {
+    std::stringstream act;
+    std::stringstream exp;
+    act << k;
+    exp << s;
+    return act.str() == exp.str();
+  }
+
+  Kind undefined;
+  Kind unknown;
+  Kind null;
+  Kind last;
+  int32_t beyond;
+};
+
+TEST_F(TestExprBlackKind, equality)
+{
+  EXPECT_EQ(undefined, UNDEFINED_KIND);
+  EXPECT_EQ(last, LAST_KIND);
+}
+
+TEST_F(TestExprBlackKind, order)
+{
+  EXPECT_LT((int32_t)undefined, (int32_t)null);
+  EXPECT_LT((int32_t)null, (int32_t)last);
+  EXPECT_LT((int32_t)undefined, (int32_t)last);
+  EXPECT_LT((int32_t)last, (int32_t)unknown);
+}
+
+TEST_F(TestExprBlackKind, output)
+{
+  ASSERT_TRUE(string_is_as_expected(undefined, "UNDEFINED_KIND"));
+  ASSERT_TRUE(string_is_as_expected(null, "NULL"));
+  ASSERT_TRUE(string_is_as_expected(last, "LAST_KIND"));
+}
+
+TEST_F(TestExprBlackKind, output_concat)
+{
+  std::stringstream act, exp;
+  act << undefined << null << last << unknown;
+  exp << "UNDEFINED_KIND"
+      << "NULL"
+      << "LAST_KIND"
+      << "?";
+  EXPECT_EQ(act.str(), exp.str());
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
deleted file mode 100644 (file)
index 9374e2b..0000000
+++ /dev/null
@@ -1,93 +0,0 @@
-/*********************                                                        */
-/*! \file kind_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, Morgan Deters
- ** 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::Kind.
- **
- ** Black box testing of CVC4::Kind.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <string>
-#include <sstream>
-
-#include "expr/kind.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-class KindBlack : public CxxTest::TestSuite {
-  Kind undefined;
-  Kind null;
-  Kind last;
-  
-  //easier to define in setup
-  int beyond;
-  Kind unknown;
-
- public:
-  void setUp() override
-  {
-    undefined = UNDEFINED_KIND;
-    null = NULL_EXPR;
-    last = LAST_KIND;
-    beyond = ((int)LAST_KIND) + 1;
-    unknown = (Kind)beyond;
-  }
-
-  
-  void testEquality(){
-
-    TS_ASSERT_EQUALS(undefined, UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(last, LAST_KIND);
-  }
-  
-  void testOrder(){
-    TS_ASSERT_LESS_THAN(int(undefined), int(null));
-    TS_ASSERT_LESS_THAN(int(null), int(last));
-    TS_ASSERT_LESS_THAN(int(undefined), int(last));
-    TS_ASSERT_LESS_THAN(int(last), int(unknown));
-  }
-
-  bool stringIsAsExpected(Kind k, const char * s){
-    stringstream act;
-    stringstream exp;
-
-    act << k;
-    exp << s;
-    
-    string actCreated = act.str();
-    string expCreated = exp.str();
-    return actCreated == expCreated;
-  }
-
-  void testOperatorLtLt() {
-
-    TS_ASSERT(stringIsAsExpected(undefined, "UNDEFINED_KIND"));
-    TS_ASSERT(stringIsAsExpected(null, "NULL"));
-    TS_ASSERT(stringIsAsExpected(last, "LAST_KIND"));    
-
-  }
-  void testOperatorLtLtConcat() {
-
-    stringstream act, exp;
-    act << undefined << null << last << unknown;
-    exp << "UNDEFINED_KIND" << "NULL" << "LAST_KIND" << "?";
-    
-    string actCreated = act.str();
-    string expCreated = exp.str();
-    
-    TS_ASSERT_EQUALS(actCreated, expCreated);
-  }
-
-};