Merge pull request #391 from VeriFIT/reluctant_replace

Implement NFT operations for solving string constraints `replace(_re)()` and `replace(_re)_all()`

include/mata/nfa/delta.hh

@@ -126,6 +126,7 @@ public:
     using super::back;
     using super::pop_back;
     using super::filter;
+    using super::clear;
 
     using super::erase;
 

include/mata/nfa/nfa.hh

@@ -428,7 +428,7 @@ public:
      * you can get all words by calling
      *      get_words(aut.num_of_states())
      */
-    std::set<Word> get_words(unsigned max_length) const;
+    std::set<Word> get_words(size_t max_length) const;
 
     /**
      * @brief Get any arbitrary accepted word in the language of the automaton.

include/mata/nfa/strings.hh

@@ -116,6 +116,15 @@ std::set<Symbol> get_accepted_symbols(const Nfa& nfa);
  */
 std::set<std::pair<int, int>> get_word_lengths(const Nfa& aut);
 
+/**
+ * @brief Modify @p nfa in-place to remove outgoing transitions from final states.
+ *
+ * If @p nfa accepts empty string, returned NFA will accept only the empty string.
+ * @param nfa NFA to modify.
+ * @return The reluctant version of @p nfa.
+ */
+Nfa reluctant_nfa(Nfa nfa);
+
 /**
  * @brief Checks if the automaton @p nfa accepts only a single word \eps.
  *

include/mata/nft/algorithms.hh

@@ -99,12 +99,14 @@ Simlib::Util::BinaryRelation compute_relation(
  * @param[out] prod_map Can be used to get the mapping of the pairs of the original states to product states.
  *   Mostly useless, it is only filled in and returned if !=nullptr, but the algorithm internally uses another data structures,
  *   because this one is too slow.
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
  * @param[in] lhs_first_aux_state The first auxiliary state in @p lhs. Two auxiliary states can not form a product state.
  * @param[in] rhs_first_aux_state The first auxiliary state in @p rhs. Two auxiliary states con not form a product state.
  * @return NFT as a product of NFTs @p lhs and @p rhs with ε handled as regular symbols.
  */
 Nft product(const Nft& lhs, const Nft& rhs, const std::function<bool(State,State)> && final_condition,
-            std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr,
+            std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr, const JumpMode jump_mode = JumpMode::RepeatSymbol,
             const State lhs_first_aux_state = Limits::max_state, const State rhs_first_aux_state = Limits::max_state);
 
 /**

include/mata/nft/builder.hh

@@ -6,6 +6,7 @@
 #include "mata/nfa/builder.hh"
 #include "nft.hh"
 
+#include <optional>
 #include <filesystem>
 
 /**
@@ -103,7 +104,7 @@ Nft parse_from_mata(const std::filesystem::path& nft_file);
  * @param epsilons Which symbols handle as epsilons.
  * @return NFT representing @p nfa_state with @p level_cnt number of levels.
  */
-Nft create_from_nfa(const mata::nfa::Nfa& nfa_state, Level level_cnt = 2, const std::set<Symbol>& epsilons = { EPSILON });
+Nft create_from_nfa(const mata::nfa::Nfa& nfa_state, Level level_cnt = 2, std::optional<Symbol> next_level_symbol = {}, const std::set<Symbol>& epsilons = { EPSILON });
 
 } // namespace mata::nft::builder.
 

include/mata/nft/nft.hh

@@ -320,6 +320,14 @@ public:
     /// Checks whether the prefix of a string is in the language of an automaton
     bool is_prfx_in_lang(const Run& word) const;
 
+    /**
+     * @brief Checks whether track words are in the language of the transducer.
+     *
+     * That is, the function checks whether a tuple @p track_words (word1, word2, word3, ..., wordn) is in the regular
+     *  relation accepted by the transducer with 'n' levels (tracks).
+     */
+    bool is_tuple_in_lang(const std::vector<Word>& track_words);
+
     std::pair<Run, bool> get_word_for_path(const Run& run) const;
 
     /**
@@ -329,7 +337,7 @@ public:
      * you can get all words by calling
      *      get_words(aut.num_of_states())
      */
-    std::set<Word> get_words(unsigned max_length);
+    std::set<Word> get_words(size_t max_length) const;
 
 }; // class Nft.
 
@@ -357,43 +365,54 @@ Nft uni(const Nft &lhs, const Nft &rhs);
  * @param[in] lhs First NFT to compute intersection for.
  * @param[in] rhs Second NFT to compute intersection for.
  * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
  * @param[in] lhs_first_aux_state The first auxiliary state in @p lhs. Two auxiliary states does not form a product state.
  * @param[in] rhs_first_aux_state The first auxiliary state in @p rhs. Two auxiliary states does not form a product state.
  * @return NFT as a product of NFTs @p lhs and @p rhs.
  */
-Nft intersection(const Nft& lhs, const Nft& rhs, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr,
+Nft intersection(const Nft& lhs, const Nft& rhs, std::unordered_map<std::pair<State, State>,
+                 State> *prod_map = nullptr, const JumpMode jump_mode = JumpMode::RepeatSymbol,
                  const State lhs_first_aux_state = Limits::max_state, const State rhs_first_aux_state = Limits::max_state);
 
 
 /**
  * @brief Composes two NFTs.
  *
- * Takes two NFTs and their corresponding synchronization levels as input,
- * and returns a new NFT that represents their composition.
+ * Takes two NFTs and their corresponding synchronization levels as input, and returns a new NFT that represents their
+ *  composition as `lhs || rhs` where `a || b` (read as "a pipe b", or "b after a") means apply `a` on input and then apply `b` on
+ *  output of `a`.
  *
  * Vectors of synchronization levels have to be non-empty and of the the same size.
  *
  * @param[in] lhs First transducer to compose.
  * @param[in] rhs Second transducer to compose.
  * @param[in] lhs_sync_levels Ordered vector of synchronization levels of the @p lhs.
  * @param[in] rhs_sync_levels Ordered vector of synchronization levels of the @p rhs.
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
  * @return A new NFT after the composition.
  */
-Nft compose(const Nft& lhs, const Nft& rhs, const utils::OrdVector<Level>& lhs_sync_levels, const utils::OrdVector<Level>& rhs_sync_levels);
+Nft compose(const Nft& lhs, const Nft& rhs,
+            const utils::OrdVector<Level>& lhs_sync_levels, const utils::OrdVector<Level>& rhs_sync_levels,
+            const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Composes two NFTs.
  *
- * Takes two NFTs and their corresponding synchronization levels as input,
- * and returns a new NFT that represents their composition.
+ * Takes two NFTs and their corresponding synchronization levels as input, and returns a new NFT that represents their
+ *  composition as `lhs || rhs` where `a || b` (read as "a pipe b", or "b after a") means apply `a` on input and then apply `b` on
+ *  output of `a`.
  *
  * @param[in] lhs First transducer to compose.
  * @param[in] rhs Second transducer to compose.
  * @param[in] lhs_sync_level The synchronization level of the @p lhs.
  * @param[in] rhs_sync_level The synchronization level of the @p rhs.
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
  * @return A new NFT after the composition.
  */
-Nft compose(const Nft& lhs, const Nft& rhs, const Level& lhs_sync_level = 1, const Level rhs_sync_level = 0);
+Nft compose(const Nft& lhs, const Nft& rhs, const Level lhs_sync_level = 1, const Level rhs_sync_level = 0, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Concatenate two NFTs.
@@ -562,51 +581,51 @@ Nft remove_epsilon(const Nft& aut, Symbol epsilon = EPSILON);
  * @param[in] nft The transducer for projection.
  * @param[in] levels_to_project A non-empty ordered vector of levels to be projected out from the transducer. It must
  *  contain only values that are greater than or equal to 0 and smaller than @c num_of_levels.
- * @param[in] repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @p DONT_CARE symbols.
  * @return A new projected transducer.
  */
-Nft project_out(const Nft& nft, const utils::OrdVector<Level>& levels_to_project, bool repeat_jump_symbol = true);
+Nft project_out(const Nft& nft, const utils::OrdVector<Level>& levels_to_project, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Projects out specified level @p level_to_project in the given transducer @p nft.
  *
  * @param[in] nft The transducer for projection.
  * @param[in] level_to_project A level that is going to be projected out from the transducer. It has to be greater than or
  *  equal to 0 and smaller than @c num_of_levels.
- * @param[in] repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @c DONT_CARE symbols.
  * @return A new projected transducer.
  */
-Nft project_out(const Nft& nft, Level level_to_project, bool repeat_jump_symbol = true);
+Nft project_out(const Nft& nft, Level level_to_project, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Projects to specified levels @p levels_to_project in the given transducer @p nft.
  *
  * @param[in] nft The transducer for projection.
  * @param[in] levels_to_project A non-empty ordered vector of levels the transducer is going to be projected to.
  *  It must contain only values greater than or equal to 0 and smaller than @c num_of_levels.
- * @param[in] repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @c DONT_CARE symbols.
  * @return A new projected transducer.
  */
-Nft project_to(const Nft& nft, const utils::OrdVector<Level>& levels_to_project, bool repeat_jump_symbol = true);
+Nft project_to(const Nft& nft, const utils::OrdVector<Level>& levels_to_project, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Projects to a specified level @p level_to_project in the given transducer @p nft.
  *
  * @param[in] nft The transducer for projection.
  * @param[in] level_to_project A level the transducer is going to be projected to. It has to be greater than or equal to 0
  *  and smaller than @c num_of_levels.
- * @param[in] repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @c DONT_CARE symbols.
  * @return A new projected transducer.
  */
-Nft project_to(const Nft& nft, Level level_to_project, bool repeat_jump_symbol = true);
+Nft project_to(const Nft& nft, Level level_to_project, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Inserts new levels, as specified by the mask @p new_levels_mask, into the given transducer @p nft.
@@ -619,11 +638,11 @@ Nft project_to(const Nft& nft, Level level_to_project, bool repeat_jump_symbol =
  * @param[in] new_levels_mask A mask representing the old and new levels. The vector {1, 0, 1, 1, 0} indicates
  *  that one level is inserted before level 0 and two levels are inserted before level 1.
  * @param[in] default_symbol The default symbol to be used for transitions at the inserted levels.
- * @param[in] repeat_jump_symbol Specifies whether the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies whether the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @c DONT_CARE symbols.
  */
-Nft insert_levels(const Nft& nft, const BoolVector& new_levels_mask, const Symbol default_symbol = DONT_CARE, bool repeat_jump_symbol = true);
+Nft insert_levels(const Nft& nft, const BoolVector& new_levels_mask, const Symbol default_symbol = DONT_CARE, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /**
  * @brief Inserts a new level @p new_level into the given transducer @p nft.
@@ -636,11 +655,11 @@ Nft insert_levels(const Nft& nft, const BoolVector& new_levels_mask, const Symbo
  *  If @p new_level is less than @c num_of_levels, then it is inserted before the level @c new_level-1.
  *  If @p new_level is greater than or equal to @c num_of_levels, then all levels from @c num_of_levels through @p new_level are appended after the last level.
  * @param[in] default_symbol The default symbol to be used for transitions at the inserted levels.
- * @param[in] repeat_jump_symbol Specifies whether the symbol on a jump transition (a transition with a length greater than 1)
+ * @param[in] jump_mode Specifies whether the symbol on a jump transition (a transition with a length greater than 1)
  *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
  *  of @c DONT_CARE symbols.
  */
-Nft insert_level(const Nft& nft, const Level new_level, const Symbol default_symbol = DONT_CARE, bool repeat_jump_symbol = true);
+Nft insert_level(const Nft& nft, const Level new_level, const Symbol default_symbol = DONT_CARE, const JumpMode jump_mode = JumpMode::RepeatSymbol);
 
 /** Encodes a vector of strings (each corresponding to one symbol) into a
  *  @c Word instance

include/mata/nft/plumbing.hh

@@ -75,14 +75,16 @@ inline void uni(Nft *unionAutomaton, const Nft &lhs, const Nft &rhs) { *unionAut
  * @param[in] lhs First NFT to compute intersection for.
  * @param[in] rhs Second NFT to compute intersection for.
  * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).
+ * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+ *  is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE
  * @param[in] lhs_first_aux_state The first auxiliary state in @p lhs. Two auxiliary states does not form a product state.
  * @param[in] rhs_first_aux_state The first auxiliary state in @p rhs. Two auxiliary states does not form a product state.
  * @return NFT as a product of NFTs @p lhs and @p rhs.
  */
 inline void intersection(Nft* res, const Nft& lhs, const Nft& rhs,
-                  std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr,
+                  std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr, const JumpMode jump_mode = JumpMode::RepeatSymbol,
                   const State lhs_first_aux_state = Limits::max_state, const State rhs_first_aux_state = Limits::max_state) {
-    *res = intersection(lhs, rhs, prod_map, lhs_first_aux_state, rhs_first_aux_state);
+    *res = intersection(lhs, rhs, prod_map, jump_mode, lhs_first_aux_state, rhs_first_aux_state);
 }
 
 /**