Merge pull request #394 from VeriFIT/nft-insert_word

Improve insert_word and insert_identity

include/mata/nfa/nfa.hh

@@ -104,14 +104,25 @@ public:
     State add_state(State state);
 
     /**
-     * Inserts a @p word into the NFA from a source state @p src to a target state @p tgt.
+     * Inserts a @p word into the NFA from a source state @p source to a target state @p target.
      * Creates new states along the path of the @p word.
      *
-     * @param src The source state where the word begins. It must already be a part of the automaton.
+     * @param source The source state where the word begins. It must already be a part of the automaton.
      * @param word The nonempty word to be inserted into the NFA.
-     * @param tgt The target state where the word ends. It must already be a part of the automaton.
+     * @param target The target state where the word ends.
+     * @return The state @p target where the inserted @p word ends.
      */
-    void insert_word(const State src, const Word &word, const State tgt);
+    State insert_word(State source, const Word& word, State target);
+
+    /**
+     * Inserts a @p word into the NFA from a source state @p source to a new target state.
+     * Creates new states along the path of the @p word.
+     *
+     * @param source The source state where the word begins. It must already be a part of the automaton.
+     * @param word The nonempty word to be inserted into the NFA.
+     * @return The newly created target state where the inserted @p word ends.
+     */
+    State insert_word(State source, const Word& word);
 
     /**
      * @brief Get the current number of states in the whole automaton.

include/mata/nft/nft.hh

@@ -143,33 +143,71 @@ public:
     State add_state_with_level(State state, Level level);
 
     /**
-     * Inserts a @p word into the NFT from a source state @p src to a target state @p tgt.
+     * Inserts a @p word into the NFT from a source state @p source to a target state @p target.
      * Creates new states along the path of the @p word.
      *
      * If the length of @p word is less than @c num_of_levels, then the last symbol of @p word
-     * will form a transition going directly from the last inner state to @p tgt. The level
-     * of the state @p tgt must be 0 or greater than the level of the last inner state.
+     * will form a transition going directly from the last inner state to @p target. The level
+     * of the state @p target must be 0 or greater than the level of the last inner state.
      *
-     * @param src The source state where the word begins. It must already be a part of the transducer.
+     * @param source The source state where the word begins. It must already be a part of the transducer.
      * @param word The nonempty word to be inserted into the NFA.
-     * @param tgt The target state where the word ends. It must already be a part of the transducer.
+     * @param target The target state where the word ends.
+     * @return The state @p target where the inserted @p word ends.
      */
-    void insert_word(const State src, const Word &word, const State tgt);
+    State insert_word(State source, const Word &word, State target);
 
     /**
-     * Inserts a word, which is created by interleaving parts from @p word_part_on_level, into the NFT
-     * from a source state @p src to a target state @p tgt, creating new states along its path.
+     * @brief Inserts a @p word into the NFT from a source state @p source to a newly created target state, creating
+     *  new states along the path of the @p word.
      *
-     * The length of the inserted word equals @c num_of_levels * the maximum word length in the vector @p word_part_on_level.
-     * At least one Word in @p word_part_on_level must be nonempty.
-     * The vector @p word_part_on_level must have a size equal to @c num_of_levels.
+     * If the length of @p word is less than @c num_of_levels, then the last symbol of @p word
+     *  will form a transition going directly from the last inner state to the newly created target.
+     *
+     * @param source The source state where the word begins. It must already be a part of the transducer.
+     * @param word The nonempty word to be inserted into the NFA.
+     * @return The newly created target where the inserted word ends.
+     */
+    State insert_word(State source, const Word &word);
+
+    /**
+     * @brief Inserts a word, which is created by interleaving parts from @p word_parts_on_levels, into the NFT
+     *  from a source state @p source to a target state @p target, creating new states along the path of @p word.
+     *
+     * The length of the inserted word equals @c num_of_levels * the maximum word length in the vector @p word_parts_on_levels.
+     * At least one Word in @p word_parts_on_levels must be nonempty.
+     * The vector @p word_parts_on_levels must have a size equal to @c num_of_levels.
+     * Words shorter than the maximum word length are interpreted as words followed by a sequence of epsilons to match the maximum length.
+     *
+     * @param source The source state where the word begins. This state must already exist in the transducer and must be of a level 0.
+     * @param word_parts_on_levels The vector of word parts, with each part corresponding to a different level.
+     * @param target The target state where the word ends.
+     * @return The state @p target where the inserted @p word_parts_on_levels ends.
+     */
+    State insert_word_by_parts(State source, const std::vector<Word>& word_parts_on_levels, State target);
+
+    /**
+     * @brief Inserts a word, which is created by interleaving parts from @p word_parts_on_levels, into the NFT
+     *  from a source state @p source to a target state @p target, creating new states along the path of @p word.
+     *
+     * The length of the inserted word equals @c num_of_levels * the maximum word length in the vector @p word_parts_on_levels.
+     * At least one Word in @p word_parts_on_levels must be nonempty.
+     * The vector @p word_parts_on_levels must have a size equal to @c num_of_levels.
      * Words shorter than the maximum word length are interpreted as words followed by a sequence of epsilons to match the maximum length.
      *
-     * @param src The source state where the word begins. This state must already exist in the transducer and must be of a level 0.
-     * @param word_part_on_level The vector of word parts, with each part corresponding to a different level.
-     * @param tgt The target state where the word ends. This state must already exist in the transducer and must be of a level 0.
+     * @param source The source state where the word begins. This state must already exist in the transducer and must be of a level 0.
+     * @param word_parts_on_levels The vector of word parts, with each part corresponding to a different level.
+     * @return The newly created target where the inserted @p word_parts_on_levels ends.
      */
-    void insert_word_by_parts(const State src, const std::vector<Word> &word_part_on_level, const State tgt);
+    State insert_word_by_parts(State source, const std::vector<Word>& word_parts_on_levels);
+
+    /**
+    * Inserts identity transitions into the NFT.
+    *
+    * @param state The state where the identity transition will be inserted. This serves as both the source and target state.
+    * @param symbol The vector of symbols used for the identity transition. Identity will be created for each symbol in the vector.
+    */
+    void insert_identity(State state, const std::vector<Symbol>& symbols);
 
     /**
     * Inserts an identity transition into the NFT.

src/nfa/nfa.cc

@@ -544,20 +544,21 @@ State Nfa::add_state(State state) {
     return state;
 }
 
-void Nfa::insert_word(const State src, const Word &word, const State tgt) {
+State Nfa::insert_word(const State source, const Word &word, const State target) {
     assert(!word.empty());
-    assert(src < num_of_states());
-    assert(tgt < num_of_states());
+    const size_t num_of_states_orig{ num_of_states() };
+    assert(source < num_of_states_orig);
+    assert(target < num_of_states_orig);
 
     const size_t word_len = word.size();
     if (word_len == 1) {
-        delta.add(src, word[0], tgt);
-        return;
+        delta.add(source, word[0], target);
+        return target;
     }
 
-    // Add transition src --> inner_state.
+    // Add transition source --> inner_state.
     State inner_state = add_state();
-    delta.add(src, word[0], inner_state);
+    delta.add(source, word[0], inner_state);
 
     // Add transitions inner_state --> inner_state
     State prev_state = inner_state;
@@ -567,10 +568,13 @@ void Nfa::insert_word(const State src, const Word &word, const State tgt) {
         prev_state = inner_state;
     }
 
-    // Add transition inner_state --> tgt
-    delta.add(prev_state, word[word_len - 1], tgt);
+    // Add transition inner_state --> target
+    delta.add(prev_state, word[word_len - 1], target);
+    return target;
 }
 
+State Nfa::insert_word(const State source, const Word &word) { return insert_word(source, word, add_state()); }
+
 size_t Nfa::num_of_states() const {
     return std::max({
         static_cast<size_t>(initial.domain_size()),

src/nft/nft.cc

@@ -305,65 +305,69 @@ State Nft::add_state_with_level(const State state, const Level level) {
     return Nfa::add_state(state);
 }
 
-void Nft::insert_word(const State src, const Word &word, const State tgt) {
+State Nft::insert_word(const State source, const Word &word, const State target) {
     assert(0 < num_of_levels);
+    const size_t num_of_states_orig{ num_of_states() };
+    assert(source < num_of_states_orig);
+    assert(target < num_of_states_orig);
 
-    const State first_new_state = num_of_states();
-    Nfa::insert_word(src, word, tgt);
+    const State first_new_state = num_of_states_orig;
+    const State word_tgt = Nfa::insert_word(source, word, target);
     const size_t num_of_states_after = num_of_states();
-    const Level src_lvl = levels[src];
+    const Level src_lvl = levels[source];
+
     Level lvl = (num_of_levels == 1 ) ? src_lvl : (src_lvl + 1);
     State state{ first_new_state };
     for (; state < num_of_states_after; state++, lvl = (lvl + 1) % static_cast<Level>(num_of_levels)){
         add_state_with_level(state, lvl);
     }
 
-    assert(levels[tgt] == 0 || levels[num_of_states_after - 1] < levels[tgt]);
-}
+    assert(levels[word_tgt] == 0 || levels[num_of_states_after - 1] < levels[word_tgt]);
 
-void Nft::insert_identity(const State state, const Symbol symbol) {
-    insert_word(state, Word(num_of_levels, symbol), state);
+    return word_tgt;
 }
 
-void Nft::insert_word_by_parts(const State src, const std::vector<Word> &word_part_on_level, const State tgt) {
+State Nft::insert_word(const State source, const Word &word) { return insert_word(source, word, add_state()); }
+
+State Nft::insert_word_by_parts(const State source, const std::vector<Word> &word_parts_on_levels, const State target) {
     assert(0 < num_of_levels);
-    assert(word_part_on_level.size() == num_of_levels);
-    assert(src < num_of_states());
-    assert(tgt < num_of_states());
-    assert(levels[src] == 0);
-    assert(levels[tgt] == 0);
+    assert(word_parts_on_levels.size() == num_of_levels);
+    const size_t num_of_states_orig{ num_of_states() };
+    assert(source < num_of_states_orig);
+    assert(target < num_of_states_orig);
+    assert(levels[source] == 0);
+    assert(levels[target] == 0);
 
     if (num_of_levels == 1) {
-        Nft::insert_word(src, word_part_on_level[0], tgt);
-        return;
+        return Nft::insert_word(source, word_parts_on_levels[0], target);
     }
 
     size_t max_word_part_len = std::max_element(
-        word_part_on_level.begin(),
-        word_part_on_level.end(),
+        word_parts_on_levels.begin(),
+        word_parts_on_levels.end(),
         [](const Word& a, const Word& b) { return a.size() < b.size(); }
     )->size();
     assert(0 < max_word_part_len);
     size_t word_total_len = num_of_levels * max_word_part_len;
 
     std::vector<mata::Word::const_iterator> word_part_it_v(num_of_levels);
     for (Level lvl{ 0 }; lvl < num_of_levels; lvl++) {
-        word_part_it_v[lvl] = word_part_on_level[lvl].begin();
+        word_part_it_v[lvl] = word_parts_on_levels[lvl].begin();
     }
 
     // This function retrieves the next symbol from a word part at a specified level and advances the corresponding iterator.
     // Returns EPSILON when the iterator reaches the end of the word part.
     auto get_next_symbol = [&](Level lvl) {
-        if (word_part_it_v[lvl] == word_part_on_level[lvl].end()) {
+        if (word_part_it_v[lvl] == word_parts_on_levels[lvl].end()) {
             return EPSILON;
         }
         return *(word_part_it_v[lvl]++);
     };
 
-    // Add transition src --> inner_state.
+    // Add transition source --> inner_state.
     Level inner_lvl = (num_of_levels == 1 ) ? 0 : 1;
     State inner_state = add_state_with_level(inner_lvl);
-    delta.add(src, get_next_symbol(0), inner_state);
+    delta.add(source, get_next_symbol(0), inner_state);
 
     // Add transition inner_state --> inner_state
     State prev_state = inner_state;
@@ -376,8 +380,23 @@ void Nft::insert_word_by_parts(const State src, const std::vector<Word> &word_pa
         prev_lvl = inner_lvl;
     }
 
-    // Add transition inner_state --> tgt.
-    delta.add(prev_state, get_next_symbol(prev_lvl), tgt);
+    // Add transition inner_state --> target.
+    delta.add(prev_state, get_next_symbol(prev_lvl), target);
+    return target;
+}
+
+State Nft::insert_word_by_parts(const State source, const std::vector<Word> &word_parts_on_levels) {
+   return insert_word_by_parts(source, word_parts_on_levels, add_state());
+}
+
+void Nft::insert_identity(const State state, const std::vector<Symbol> &symbols) {
+    for (const Symbol symbol : symbols) {
+        insert_identity(state, symbol);
+    }
+}
+
+void Nft::insert_identity(const State state, const Symbol symbol) {
+    insert_word(state, Word(num_of_levels, symbol), state);
 }
 
 void Nft::clear() {