mata as lib: integration

VeriFIT · Jan 18, 2023 · dd349d2 · dd349d2
1 parent 7f5f5b1
commit dd349d2
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 19 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -10,12 +10,6 @@ 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/smt/theory_str_noodler/aut_assignment.h b/src/smt/theory_str_noodler/aut_assignment.h
@@ -22,8 +22,8 @@ namespace smt::noodler {
 
         Mata::Nfa::Nfa eps_automaton() const {
             Mata::Nfa::Nfa nfa(1);
-            nfa.initial_states = {0};
-            nfa.final_states = {0};
+            nfa.initial = {0};
+            nfa.final = {0};
             return nfa;
         }
 
@@ -37,7 +37,7 @@ namespace smt::noodler {
 
         bool is_epsilon(const BasicTerm &t) const {
             Mata::Nfa::Nfa v = Mata::Nfa::minimize(Mata::Nfa::remove_epsilon(this->at(t))); // if we are sure that we have epsilon-free automata, we can skip remove_epsilon
-            return v.get_num_of_trans() == 0 && v.initial_states.size() == 1 && v.final_states.size();
+            return v.get_num_of_trans() == 0 && v.initial.size() == 1 && v.final.size();
         }
 
     };

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -94,15 +94,15 @@ TEST_CASE("Conversion to strings", "[noodler]") {
 
 TEST_CASE("Mata integration", "[noodler]") {
     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());
+    nfa.initial = { 0, 1};
+    nfa.final = { 3, 1};
+    nfa.delta.add(0, 42, 1);
+    nfa.delta.add(1, 42, 2);
+    CHECK(nfa.final[1]);
+    CHECK(!nfa.final[0]);
+    CHECK(nfa.delta.contains(0, 42, 1));
+    CHECK(!nfa.delta.contains(1, 42, 1));
+    CHECK(!nfa.delta.empty());
 }
 
 TEST_CASE("Graph::get_edges_to", "[noodler]") {