Fix reluctant leftmost nft creation

VeriFIT · Apr 17, 2024 · d657670 · d657670
1 parent 756090f
commit d657670
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 12 deletions.
diff --git a/src/nft/strings.cc b/src/nft/strings.cc
@@ -408,16 +408,11 @@ Nft ReluctantReplace::reluctant_leftmost_nft(nfa::Nfa nfa, Alphabet* alphabet, S
 
     // Create self-loop on the new initial state.
     const State initial{ nft_reluctant_leftmost.add_state_with_level(0) };
-    State curr_state{ regex_num_of_states + 1 };
-    StatePost& initial_state_post{ nft_reluctant_leftmost.delta.mutable_state_post(initial) };
-    for (const Symbol symbol: alphabet_symbols) {
-        initial_state_post.push_back({ symbol, curr_state });
-        nft_reluctant_leftmost.delta.add(curr_state, symbol, initial);
-        nft_reluctant_leftmost.levels[curr_state] = 1;
-        ++curr_state;
-    }
+    nft_reluctant_leftmost.insert_identity(initial, alphabet_symbols.ToVector());
+
     // Move to replace mode when begin marker is encountered.
-    initial_state_post.insert({ begin_marker, curr_state });
+    State curr_state{ nft_reluctant_leftmost.num_of_states() };
+    nft_reluctant_leftmost.delta.add(initial, begin_marker, curr_state);
     nft_reluctant_leftmost.delta.mutable_state_post(curr_state).push_back(
         SymbolPost{ EPSILON, StateSet{ nft_reluctant_leftmost.initial } }
     );
@@ -436,11 +431,11 @@ Nft ReluctantReplace::reluctant_leftmost_nft(nfa::Nfa nfa, Alphabet* alphabet, S
     nft_reluctant_leftmost.final.insert(next_state);
     nft_reluctant_leftmost.final.clear();
     switch (replace_mode) {
-        case ReplaceMode::All: {
-            nft_reluctant_leftmost.delta.add(next_state, EPSILON, initial);
+        case ReplaceMode::All: { // Return to beginning to possibly repeat replacement.
+            nft_reluctant_leftmost.insert_word_by_parts(next_state, { { EPSILON }, { EPSILON } }, initial);
             break;
         };
-        case ReplaceMode::Single: {
+        case ReplaceMode::Single: { // End the replacement mode.
             nft_reluctant_leftmost.levels.resize(nft_reluctant_leftmost.levels.size() + alphabet_symbols.size() + 1);
             const State final{ next_state };
             nft_reluctant_leftmost.final.insert(final);

diff --git a/tests/nft/strings.cc b/tests/nft/strings.cc
@@ -925,4 +925,26 @@ TEST_CASE("mata::nft::strings::replace_reluctant_regex()") {
 //        ));
 //        CHECK(nft::are_equivalent(nft, expected));
     }
+
+    SECTION("bugfix: replace from Noodler") {
+        nfa::Nfa regex = nfa::builder::parse_from_mata(std::string(
+            "@NFA-explicit\n%Alphabet-auto\n%Initial q0\n%Final q7\nq0 60 q1\nq1 83 q2\nq2 67 q3\nq3 82 q4\nq4 73 q5\nq5 80 q6\nq6 84 q7\nq7 48 q7\nq7 49 q7\nq7 50 q7\nq7 51 q7\nq7 52 q7\nq7 53 q7\nq7 54 q7\nq7 55 q7\nq7 56 q7\nq7 57 q7\nq7 60 q7\nq7 66 q7\nq7 67 q7\nq7 68 q7\nq7 69 q7\nq7 70 q7\nq7 71 q7\nq7 72 q7\nq7 73 q7\nq7 74 q7\nq7 75 q7\nq7 76 q7\nq7 78 q7\nq7 79 q7\nq7 80 q7\nq7 82 q7\nq7 83 q7\nq7 84 q7\nq7 86 q7\nq7 87 q7\nq7 92 q7\nq7 97 q7\nq7 98 q7\nq7 99 q7\nq7 100 q7\nq7 101 q7\nq7 102 q7\nq7 103 q7\nq7 104 q7\nq7 105 q7\nq7 106 q7\nq7 107 q7\nq7 108 q7\nq7 109 q7\nq7 110 q7\nq7 112 q7\nq7 114 q7\nq7 115 q7\nq7 116 q7\nq7 119 q7\nq7 120 q7\nq7 121 q7\nq7 196608 q7\n"
+        ));
+        mata::Word replacement{ 66, 76, 79, 67, 75, 69, 68 };
+        alphabet = mata::EnumAlphabet{ 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 60, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 78, 79, 80, 82, 83, 84, 86, 87, 92, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 112, 114, 115, 116, 119, 120, 121, 196608 };
+        nft = nft::strings::replace_reluctant_regex(regex, replacement, &alphabet, ReplaceMode::All);
+
+        CHECK(nft.is_tuple_in_lang({ { '<', 'S', 'C', 'R', 'I', 'P', 'T', '<', '<', '<', '<' },
+                                     { 'B', 'L', 'O', 'C', 'K', 'E', 'D', '<', '<', '<', '<' } }));
+        CHECK(nft.is_tuple_in_lang({ { '<', '<', 'S', 'C', 'R', 'I', 'P', 'T', '<', '<', '<', '<' },
+                                     { '<', 'B', 'L', 'O', 'C', 'K', 'E', 'D', '<', '<', '<', '<' } }));
+        CHECK(nft.is_tuple_in_lang({ { '<', 'S', '<', 'S', 'C', 'R', 'I', 'P', 'T', '<', '<', '<', '<' },
+                                     { '<', 'S', 'B', 'L', 'O', 'C', 'K', 'E', 'D', '<', '<', '<', '<' } }));
+        CHECK(nft.is_tuple_in_lang({ { '<', 'S', '<', 'S', 'C', 'R', 'I', 'P', 'T', 'T', 'T', '<', '<' },
+                                     { '<', 'S', 'B', 'L', 'O', 'C', 'K', 'E', 'D', 'T', 'T', '<', '<' } }));
+        CHECK(!nft.is_tuple_in_lang({ { '<', 'S', '<', 'S', 'C', 'R', 'I', 'P', 'T', 'T', 'T', '<', '<' },
+                                     { '<', 'S', 'B', 'L', 'O', 'C', 'K', 'E', 'D', 'T', '<', '<' } }));
+        CHECK(!nft.is_tuple_in_lang({ { '<', 's', '<', 's', 'c', 'r', 'i', 'p', 't', 't', 't', '<', '<' },
+                                     { '<', 's', 'B', 'L', 'O', 'C', 'K', 'E', 'D', 't', 't', '<', '<' } }));
+    }
 }