Link libMata to z3 and tests-noodler

VeriFIT · Dec 2, 2022 · 0c3fd01 · 0c3fd01
1 parent 150af5a
commit 0c3fd01
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 0 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,4 @@
+[submodule "extern/lib/mata"]
+	path = extern/lib/mata
+	url = https://github.com/Adda0/mata.git
+	branch = z3_import
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -10,6 +10,12 @@ project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
 message(STATUS "Z3 version ${Z3_VERSION}")
 
+################################################################################
+# Extern Libraries
+################################################################################
+
+add_subdirectory(extern/lib/mata)
+
 ################################################################################
 # Message for polluted source tree sanity checks
 ################################################################################

diff --git a/extern/lib/mata b/extern/lib/mata
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -165,6 +165,14 @@ endif()
 # shared library the dependent libraries are specified on the link command line
 # so that if those are also shared libraries they are referenced by `libz3.so`.
 target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
+target_include_directories(libz3 PRIVATE ${PROJECT_SOURCE_DIR}/extern/lib/mata/include)
+target_link_libraries(libz3 PRIVATE mata re2 simlib)
+target_link_directories(libz3 PRIVATE
+        ${PROJECT_BINARY_DIR}
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/src
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/re2
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/simlib
+)
 
 # This is currently only for the OpenMP flags. It needs to be set
 # via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
@@ -42,6 +42,15 @@ set_target_properties(shell PROPERTIES
     CXX_VISIBILITY_PRESET hidden
     VISIBILITY_INLINES_HIDDEN ON)
 
+target_include_directories(shell PRIVATE ${PROJECT_SOURCE_DIR}/extern/lib/mata/include)
+target_link_libraries(shell PRIVATE mata re2 simlib)
+target_link_directories(shell PRIVATE
+        ${PROJECT_BINARY_DIR}
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/src
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/re2
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/simlib
+        )
+
 z3_add_install_tactic_rule(${shell_deps})
 z3_add_memory_initializer_rule(${shell_deps})
 z3_add_gparams_register_modules_rule(${shell_deps})

diff --git a/src/test/noodler/CMakeLists.txt b/src/test/noodler/CMakeLists.txt
@@ -15,6 +15,16 @@ add_executable(test-noodler
         main.cc
         inclusion-graph-node.cc
 )
+
+target_include_directories(test-noodler PRIVATE ${PROJECT_SOURCE_DIR}/extern/lib/mata/include)
+target_link_libraries(test-noodler PRIVATE mata re2 simlib)
+target_link_directories(test-noodler PRIVATE
+        ${PROJECT_BINARY_DIR}
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/src
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/re2
+        ${PROJECT_BINARY_DIR}/extern/lib/mata/3rdparty/simlib
+)
+
 z3_add_install_tactic_rule(${z3_test_deps})
 z3_add_memory_initializer_rule(${z3_test_deps})
 z3_add_gparams_register_modules_rule(${z3_test_deps})

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -1,6 +1,7 @@
 #include <iostream>
 
 #include <catch2/catch_test_macros.hpp>
+#include <mata/nfa.hh>
 
 #include <smt/theory_str_noodler/inclusion_graph_node.h>
 
@@ -73,3 +74,16 @@ TEST_CASE("Conversion to strings", "[noodler]") {
           BasicTerm{ BasicTermType::Variable, "y_58" }
     } );
 }
+
+TEST_CASE("Mata integration") {
+    auto nfa = Mata::Nfa::Nfa(3);
+    nfa.initial_states = { 0, 1};
+    nfa.final_states = { 3, 1};
+    nfa.add_trans(0, 42, 1);
+    nfa.add_trans(1, 42, 2);
+    CHECK(nfa.has_final(1));
+    CHECK(!nfa.has_final(0));
+    CHECK(nfa.has_trans(0, 42, 1));
+    CHECK(!nfa.has_trans(1, 42, 1));
+    CHECK(!nfa.has_no_transitions());
+}