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)
--- /dev/null
+/********************* */
+/*! \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
+++ /dev/null
-/********************* */
-/*! \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);
- }
-
-};