Add basic Catch2 tests structure for noodler

VeriFIT · Nov 8, 2022 · 9c323e4 · 9c323e4
1 parent 1811d2c
commit 9c323e4
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 0 deletions.
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
@@ -1,5 +1,7 @@
 add_subdirectory(fuzzing)
 add_subdirectory(lp)
+add_subdirectory(noodler)
+
 ################################################################################
 # z3-test executable
 ################################################################################

diff --git a/src/test/noodler/CMakeLists.txt b/src/test/noodler/CMakeLists.txt
@@ -0,0 +1,30 @@
+find_package(Catch2 3 REQUIRED)
+
+# These tests can use the Catch2-provided main
+z3_add_component(noodler
+    EXCLUDE_FROM_ALL
+    NOT_LIBZ3_COMPONENT # Don't put this component inside libz3
+    SOURCES
+        inclusion-graph-node.cc
+    COMPONENT_DEPENDENCIES
+        smt
+)
+
+add_executable(test-noodler
+        main.cc
+)
+target_link_libraries(test-noodler PRIVATE Catch2::Catch2WithMain)
+z3_add_install_tactic_rule(noodler)
+z3_add_memory_initializer_rule(noodler)
+z3_add_gparams_register_modules_rule(noodler)
+target_compile_definitions(test-noodler PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(test-noodler PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_link_libraries(test-noodler PRIVATE noodler)
+target_include_directories(test-noodler PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+z3_append_linker_flag_list_to_target(test-noodler ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+z3_add_component_dependencies_to_target(test-noodler noodler)
+
+
+# These tests need their own main
+#add_executable(custom-main-tests test.cpp test-main.cpp)
+#target_link_libraries(custom-main-tests PRIVATE Catch2::Catch2)
diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -0,0 +1,16 @@
+#include <iostream>
+
+#include <catch2/catch_test_macros.hpp>
+
+#include <smt/theory_str_noodler/inclusion_graph_node.h>
+
+using namespace smt::noodler;
+
+TEST_CASE( "Inclusion graph node", "[noodler]" ) {
+    auto predicate{ Predicate(PredicateType::Equation) };
+    CHECK(predicate.get_type() == PredicateType::Equation);
+
+    constexpr auto term_name{ "x_1" };
+    auto term{ BasicTerm(term_name, BasicTermType::Variable) };
+    CHECK(term.get_name() == term_name);
+}
diff --git a/src/test/noodler/main.cc b/src/test/noodler/main.cc