COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $$ARGS
DEPENDS build-units)
-set(CVC4_CXXTEST_FLAGS_BLACK
+set(CVC4_UNIT_TEST_FLAGS_BLACK
-D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
-set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
+set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_UNIT_TEST_FLAGS_BLACK})
# Generate and add unit test.
macro(cvc4_add_unit_test is_white name output_dir)
set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
add_executable(${name} ${test_src})
+ target_compile_definitions(${name} PRIVATE ${CVC4_UNIT_TEST_FLAGS_BLACK})
gtest_add_tests(TARGET ${name})
target_link_libraries(${name} main-test)
target_link_libraries(${name} GTest::GTest)
add_executable(${name} ${test_src} ${test_header})
target_link_libraries(${name} main-test)
target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR})
- target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
+ target_compile_definitions(${name} PRIVATE ${CVC4_UNIT_TEST_FLAGS_BLACK})
if(USE_LFSC)
# We don't link against LFSC, because CVC4 is already linked against it.
target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
#-----------------------------------------------------------------------------#
# Add unit tests
-cvc4_add_cxx_unit_test_black(map_util_black base)
+cvc4_add_unit_test_black(map_util_black base)
--- /dev/null
+/********************* */
+/*! \file map_util_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Tim King
+ ** 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 map utility functions.
+ **
+ ** Black box testing of map utility functions.
+ **/
+
+#include <map>
+#include <set>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+
+#include "base/map_util.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+#include "test.h"
+
+using CVC4::ContainsKey;
+using CVC4::FindOrDie;
+using CVC4::FindOrNull;
+using CVC4::context::CDHashMap;
+using CVC4::context::CDInsertHashMap;
+using CVC4::context::Context;
+
+class TestMapBlack : public TestInternal
+{
+ protected:
+ /** Returns a map containing {"key"->"value", "other"->"entry"}. */
+ static const std::map<std::string, std::string>& default_map()
+ {
+ static const std::map<std::string, std::string> static_stored_map{
+ {"key", "value"}, {"other", "entry"}};
+ return static_stored_map;
+ }
+
+ /**
+ * For each <key, value> pair in source, inserts mapping from key to value
+ * using insert into dest.
+ */
+ template <class M>
+ void insert_all(const std::map<std::string, std::string>& source, M* dest)
+ {
+ for (const auto& key_value : source)
+ {
+ dest->insert(key_value.first, key_value.second);
+ }
+ }
+};
+
+TEST_F(TestMapBlack, map)
+{
+ std::map<std::string, std::string> map = default_map();
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ if (std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ *found_value = "new value";
+ }
+ EXPECT_EQ(FindOrDie(map, "other"), "new value");
+}
+
+TEST_F(TestMapBlack, constant_map)
+{
+ const std::map<std::string, std::string> map = default_map();
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+ ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key.");
+}
+
+TEST_F(TestMapBlack, unordered_map)
+{
+ std::unordered_map<std::string, std::string> map(default_map().begin(),
+ default_map().end());
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ if (std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ *found_value = "new value";
+ }
+ EXPECT_EQ(FindOrDie(map, "other"), "new value");
+}
+
+TEST_F(TestMapBlack, const_unordered_map)
+{
+ const std::unordered_map<std::string, std::string> map(default_map().begin(),
+ default_map().end());
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+ ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key.");
+}
+
+TEST_F(TestMapBlack, set)
+{
+ std::set<std::string> set{"entry", "other"};
+ ASSERT_TRUE(CVC4::ContainsKey(set, "entry"));
+ ASSERT_FALSE(CVC4::ContainsKey(set, "non member"));
+
+ const std::set<std::string> const_set{"entry", "other"};
+ ASSERT_TRUE(CVC4::ContainsKey(const_set, "entry"));
+ ASSERT_FALSE(CVC4::ContainsKey(const_set, "non member"));
+}
+
+TEST_F(TestMapBlack, unordered_set)
+{
+ std::unordered_set<std::string> set{"entry", "other"};
+ ASSERT_TRUE(CVC4::ContainsKey(set, "entry"));
+ ASSERT_FALSE(CVC4::ContainsKey(set, "non member"));
+
+ const std::unordered_set<std::string> const_set{"entry", "other"};
+ ASSERT_TRUE(CVC4::ContainsKey(const_set, "entry"));
+ ASSERT_FALSE(CVC4::ContainsKey(const_set, "non member"));
+}
+
+TEST_F(TestMapBlack, CDHashMap)
+{
+ Context context;
+ CDHashMap<std::string, std::string> map(&context);
+ insert_all(default_map(), &map);
+
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+}
+
+TEST_F(TestMapBlack, const_CDHashMap)
+{
+ Context context;
+ CDHashMap<std::string, std::string> store(&context);
+ insert_all(default_map(), &store);
+ const auto& map = store;
+
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+}
+
+TEST_F(TestMapBlack, CDInsertHashMap)
+{
+ Context context;
+ CDInsertHashMap<std::string, std::string> map(&context);
+ insert_all(default_map(), &map);
+
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+}
+
+TEST_F(TestMapBlack, const_CDInsertHashMap)
+{
+ Context context;
+ CDInsertHashMap<std::string, std::string> store(&context);
+ insert_all(default_map(), &store);
+ const auto& map = store;
+
+ ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
+ ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
+ if (const std::string* found_value = FindOrNull(map, "other"))
+ {
+ EXPECT_EQ(*found_value, "entry");
+ }
+ EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+ EXPECT_EQ(FindOrDie(map, "other"), "entry");
+}
+++ /dev/null
-/********************* */
-/*! \file map_util_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** 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 map utility functions.
- **
- ** Black box testing of map utility functions.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <map>
-#include <set>
-#include <string>
-#include <unordered_map>
-#include <unordered_set>
-
-#include "base/map_util.h"
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/cdinsert_hashmap.h"
-#include "context/context.h"
-
-using CVC4::ContainsKey;
-using CVC4::FindOrDie;
-using CVC4::FindOrNull;
-using CVC4::context::CDHashMap;
-using CVC4::context::CDInsertHashMap;
-using CVC4::context::Context;
-using std::string;
-
-class MapUtilBlack : public CxxTest::TestSuite
-{
- public:
- void setUp() override {}
- void tearDown() override {}
-
- // Returns a map containing {"key"->"value", "other"->"entry"}.
- static const std::map<string, string>& DefaultMap()
- {
- static const std::map<string, string> static_stored_map{{"key", "value"},
- {"other", "entry"}};
- return static_stored_map;
- }
-
- void testMap()
- {
- std::map<string, string> map = DefaultMap();
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- if (string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- *found_value = "new value";
- }
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value");
- }
-
- void testConstantMap()
- {
- const std::map<string, string> map = DefaultMap();
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- // Cannot do death tests for FindOrDie.
- }
-
- void testUnorderedMap()
- {
- std::unordered_map<string, string> map(DefaultMap().begin(),
- DefaultMap().end());
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- if (string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- *found_value = "new value";
- }
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value");
- }
-
- void testConstUnorderedMap()
- {
- const std::unordered_map<string, string> map(DefaultMap().begin(),
- DefaultMap().end());
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- // Cannot do death tests for FindOrDie.
- }
-
- void testSet()
- {
- std::set<string> set{"entry", "other"};
- TS_ASSERT(ContainsKey(set, "entry"));
- TS_ASSERT(!ContainsKey(set, "non member"));
-
- const std::set<string> const_set{"entry", "other"};
- TS_ASSERT(ContainsKey(const_set, "entry"));
- TS_ASSERT(!ContainsKey(const_set, "non member"));
- }
-
- void testUnorderedSet()
- {
- std::unordered_set<string> set{"entry", "other"};
- TS_ASSERT(ContainsKey(set, "entry"));
- TS_ASSERT(!ContainsKey(set, "non member"));
-
- const std::unordered_set<string> const_set{"entry", "other"};
- TS_ASSERT(ContainsKey(const_set, "entry"));
- TS_ASSERT(!ContainsKey(const_set, "non member"));
- }
-
- // For each <key, value> pair in source, inserts mapping from key to value
- // using insert into dest.
- template <class M>
- void InsertAll(const std::map<string, string>& source, M* dest)
- {
- for (const auto& key_value : source)
- {
- dest->insert(key_value.first, key_value.second);
- }
- }
-
- void testCDHashMap()
- {
- Context context;
- CDHashMap<string, string> map(&context);
- InsertAll(DefaultMap(), &map);
-
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- }
-
- void testConstCDHashMap()
- {
- Context context;
- CDHashMap<string, string> store(&context);
- InsertAll(DefaultMap(), &store);
- const auto& map = store;
-
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- }
-
- void testCDInsertHashMap()
- {
- Context context;
- CDInsertHashMap<string, string> map(&context);
- InsertAll(DefaultMap(), &map);
-
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
-
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- }
-
- void testConstCDInsertHashMap()
- {
- Context context;
- CDInsertHashMap<string, string> store(&context);
- InsertAll(DefaultMap(), &store);
- const auto& map = store;
-
- TS_ASSERT(ContainsKey(map, "key"));
- TS_ASSERT(!ContainsKey(map, "non key"));
- if (const string* found_value = FindOrNull(map, "other"))
- {
- TS_ASSERT_EQUALS(*found_value, "entry");
- }
- TS_ASSERT(FindOrNull(map, "non key") == nullptr);
- TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
- }
-
-}; /* class MapUtilBlack */
--- /dev/null
+/********************* */
+/*! \file test.h
+ ** \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 Common header for API unit test.
+ **/
+
+#ifndef CVC4__TEST__UNIT__TEST_H
+#define CVC4__TEST__UNIT__TEST_H
+
+#include "gtest/gtest.h"
+
+class TestInternal : public ::testing::Test
+{
+};
+
+#endif