Composition without epsilon self-loops

examples/nft.cc

@@ -37,7 +37,7 @@ int main() {
     Nfa nfa = nfa::builder::create_from_regex("ABCDEFggg");
 
     // Compute the pre-image of an NFA (applies NFA to the image tape, i.e., tape 1)
-    Nft backward_applied_nft = nft.apply(nfa, 1);
+    Nft backward_applied_nft = nft.apply(nfa, 1, true, mata::nft::JumpMode::NoJump);
     // Extract a pre-image NFA.
     Nfa nfa_pre_image{ backward_applied_nft.to_nfa_move() };
     // Minimize the result pre-image using hopcroft minimization.

include/mata/nft/algorithms.hh

@@ -132,6 +132,47 @@ Nft product(const Nft& lhs, const Nft& rhs, const std::function<bool(State,State
 Nft concatenate_eps(const Nft& lhs, const Nft& rhs, const Symbol& epsilon, bool use_epsilon = false,
                     StateRenaming* lhs_state_renaming = nullptr, StateRenaming* rhs_state_renaming = nullptr);
 
+/**
+ * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs").
+ *
+ * This function computes the composition of two NFTs, `lhs` and `rhs`, by aligning their synchronization levels.
+ * Transitions between two synchronization levels are ordered as follows: first the transitions of `lhs`, then
+ * the transitions of `rhs` followed by next synchronization level (if exists). By default, synchronization
+ * levels are projected out from the resulting NFT.
+ *
+ * Vectors of synchronization levels have to be non-empty and of the same size.
+ *
+ * NOTE: If you have only a single synchronization level per NFT and don't use jump transitions, consider using
+ *       no-jump varsion of the composition for better performance.
+ *
+ * @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] project_out_sync_levels Whether we want to project out the synchronization levels.
+ * @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_general(const Nft& lhs, const Nft& rhs,
+            const utils::OrdVector<Level>& lhs_sync_levels, const utils::OrdVector<Level>& rhs_sync_levels,
+            bool project_out_sync_levels = true,
+            JumpMode jump_mode = JumpMode::RepeatSymbol);
+
+/**
+ * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs") with a single synchronization level and no jumps.
+ *
+ * @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] project_out_sync_levels Whether we wont to project out the synchronization levels.
+ *
+ * @return A new NFT after the composition.
+ */
+Nft compose_fast_no_jump(const Nft& lhs, const Nft& rhs, Level lhs_sync_level = 1, Level rhs_sync_level = 0, bool project_out_sync_levels = true);
+
 }
 
 #endif

include/mata/nft/nft.hh

@@ -340,6 +340,45 @@ public:
      */
     State add_transition(State source, const std::vector<Symbol>& symbols);
 
+    /**
+     * @brief Add a single NFT transition with a length @p length from a source state @p source
+     * to a newly created target state, creating as many inner states as needed for the transition
+     * @p length and the jump mode.
+     *
+     * @param source The source state where the transition begins. @p source must already exist.
+     * @param symbol The symbol used for the transition.
+     * @param length The length of the transition.
+     * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1).
+     */
+    State add_transition_with_length(State source, Symbol symbol, size_t length, JumpMode jump_mode = JumpMode::RepeatSymbol);
+
+    /**
+     * @brief Add a single NFT transition from a source state @p source to a target state @p target
+     * creating as many inner states as needed for the transition length and the jump mode.
+     *
+     * @param source The source state where the transition begins. @p source must already exist.
+     * @param symbol The symbol used for the transition.
+     * @param target The target state where the transition ends. @p target must already exist.
+     * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1).
+     */
+    void add_transition_with_target(const State source, const Symbol symbol, const State target, const JumpMode jump_mode = JumpMode::RepeatSymbol) {
+        add_transition_with_same_level_targets(source, symbol, { target }, jump_mode);
+    }
+
+    /**
+     * @brief Add a NFT transition from a source state @p source to a set of target states @p targets
+     * creating as many inner states as needed for the transition length and the jump mode.
+     *
+     * For transitions with a length `l` greater than 1, the common part (before the `l`-th symbol) of the
+     * is shared for all targets and only at the `l`-th symbol the transition branches to each target.
+     *
+     * @param source The source state where the transition begins. @p source must already exist.
+     * @param symbol The symbol used for the transition.
+     * @param targets The set of target states where the transition ends. Each target must already exist.
+     * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1).
+     */
+    void add_transition_with_same_level_targets(State source, Symbol symbol, const StateSet& targets, JumpMode jump_mode = JumpMode::RepeatSymbol);
+
     /**
      * @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.
@@ -913,45 +952,56 @@ Nft intersection(const Nft& lhs, const Nft& rhs,
 /**
  * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs").
  *
- * This function computes the composition of two NFTs, `lhs` and `rhs`, by aligning their synchronization levels.
- * Transitions between two synchronization levels are ordered as follows: first the transitions of `lhs`, then
- * the transitions of `rhs` followed by next synchronization level (if exists). By default, synchronization
- * levels are projected out from the resulting NFT.
- *
- * Vectors of synchronization levels have to be non-empty and of 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] project_out_sync_levels Whether we want to project out the synchronization levels.
  * @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] composition_mode Mode of composition to use. Default is Auto, which selects the best mode based
+ *                             on the presence of jump transitions. General mode supports all NFTs, while FastNoJump
+ *                             mode is optimized for NFTs without jump transitions and with only one synchronization level.
+ *
  * @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,
             bool project_out_sync_levels = true,
-            JumpMode jump_mode = JumpMode::RepeatSymbol);
+            JumpMode jump_mode = JumpMode::RepeatSymbol,
+            CompositionMode composition_mode = CompositionMode::Auto);
 
 /**
  * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs").
  *
- * This function computes the composition of two NFTs, `lhs` and `rhs`, by aligning their synchronization levels.
- * Transitions between two synchronization levels are ordered as follows: first the transitions of `lhs`, then
- * the transitions of `rhs` followed by next synchronization level (if exists). By default, synchronization
- * levels are projected out from the resulting NFT.
- *
  * @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] project_out_sync_levels Whether we wont to project out the synchronization levels.
+ * @param[in] project_out_sync_levels Whether we want to project out the synchronization levels.
  * @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] composition_mode Mode of composition to use. Default is Auto, which selects the best mode based
+ *                             on the presence of jump transitions. General mode supports all NFTs, while FastNoJump
+ *                             mode is optimized for NFTs without jump transitions and with only one synchronization level.
+ *
  * @return A new NFT after the composition.
  */
-Nft compose(const Nft& lhs, const Nft& rhs, Level lhs_sync_level = 1, Level rhs_sync_level = 0, bool project_out_sync_levels = true, JumpMode jump_mode = JumpMode::RepeatSymbol);
+inline Nft compose(const Nft& lhs, const Nft& rhs,
+                   const Level lhs_sync_level = 1, const Level rhs_sync_level = 0,
+                   const bool project_out_sync_levels = true,
+                   const JumpMode jump_mode = JumpMode::RepeatSymbol,
+                   const CompositionMode composition_mode = CompositionMode::Auto)
+{
+    return compose(
+        lhs, rhs,
+        utils::OrdVector<Level>{ lhs_sync_level },
+        utils::OrdVector<Level>{ rhs_sync_level },
+        project_out_sync_levels,
+        jump_mode,
+        composition_mode
+    );
+}
 
 /**
  * @brief Concatenate two NFTs.

include/mata/nft/types.hh

@@ -56,7 +56,14 @@ class Nft; ///< A non-deterministic finite transducer.
 
 enum class JumpMode {
     RepeatSymbol, ///< Repeat the symbol on the jump.
-    AppendDontCares ///< Append a sequence of DONT_CAREs to the symbol on the jump.
+    AppendDontCares, ///< Append a sequence of DONT_CAREs to the symbol on the jump.
+    NoJump ///< No jumps are allowed.
+};
+
+enum class CompositionMode {
+    General, ///< General composition mode for arbitrary number or synchronization levels and jump modes.
+    FastNoJump, ///< Fast composition mode for a single synchronization level and no jumps.
+    Auto ///< Automatically select the best composition mode based on the parameters.
 };
 
 using ProductFinalStateCondition = mata::nfa::ProductFinalStateCondition;
@@ -99,8 +106,9 @@ public:
      */
     size_t num_of_levels{ DEFAULT_NUM_OF_LEVELS };
 
-    // explicit Levels(const std::vector<Level>& levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {}
-    // explicit Levels(std::vector<Level>&& levels): super{ std::move(levels) } { num_of_levels = num_of_levels_of(*this).value_or(DEFAULT_NUM_OF_LEVELS); }
+    // explicit Levels(std::initializer_list<Level> levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {}
+    explicit Levels(const std::vector<Level>& levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {}
+    explicit Levels(std::vector<Level>&& levels): super{ std::move(levels) } { num_of_levels = num_of_levels_of(*this).value_or(DEFAULT_NUM_OF_LEVELS); }
     explicit Levels(const size_t num_of_levels, std::vector<Level> levels = {}): super{ std::move(levels) }, num_of_levels{ num_of_levels } {}
     Levels() = default;
     Levels(size_t num_of_levels, size_t count, Level value = DEFAULT_LEVEL);

src/applications/strings/noodlification.cc

@@ -469,9 +469,9 @@ std::vector<seg_nfa::TransducerNoodle> seg_nfa::noodlify_for_transducer(
         // we can do the following optimization. Let I1, ..., In be the input automata. Because T is homomorphic,
         // we can take the concatenation T(I1).T(I2)...T(In) connected with INPUT_DELIMITER instead of computing
         // the composition with concatenated_input_nft.
-        mata::nft::Nft concatenation{ mata::nft::compose(mata::nft::Nft(*input_automata[0]), *nft, 0, 0, false) };
+        mata::nft::Nft concatenation{ mata::nft::compose(mata::nft::Nft(*input_automata[0]), *nft, 0, 0, false, mata::nft::JumpMode::NoJump) };
         for (size_t i = 1; i < input_automata.size(); ++i) {
-            mata::nft::Nft composition = mata::nft::compose(mata::nft::Nft(*input_automata[i]), *nft, 0, 0, false);
+            mata::nft::Nft composition = mata::nft::compose(mata::nft::Nft(*input_automata[i]), *nft, 0, 0, false, mata::nft::JumpMode::NoJump);
             concatenation = mata::nft::algorithms::concatenate_eps(concatenation, composition, input_delimiter, true);
         }
         intersection = std::move(concatenation);
@@ -480,7 +480,7 @@ std::vector<seg_nfa::TransducerNoodle> seg_nfa::noodlify_for_transducer(
         // we intersect input nfa with nft on the input track, but we need to add INPUT_DELIMITER as an "epsilon transition" of nft
         add_self_loop_for_every_default_state(intersection, input_delimiter);
 
-        intersection = mata::nft::compose(concatenated_input_nft, intersection, 0, 0, false);
+        intersection = mata::nft::compose(concatenated_input_nft, intersection, 0, 0, false, mata::nft::JumpMode::NoJump);
     }
     intersection.trim();
 
@@ -491,7 +491,7 @@ std::vector<seg_nfa::TransducerNoodle> seg_nfa::noodlify_for_transducer(
     // We also need to INPUT_DELIMITER as "epsilon transition" of the output nfa, so that we do not lose it.
     add_self_loop_for_every_default_state(concatenated_output_nft, input_delimiter);
     add_self_loop_for_every_default_state(intersection, output_delimiter);
-    intersection = mata::nft::compose(concatenated_output_nft, intersection, 0, 1, false);
+    intersection = mata::nft::compose(concatenated_output_nft, intersection, 0, 1, false, mata::nft::JumpMode::NoJump);
     intersection.trim();
 
     if (intersection.final.empty()) { return {}; }

src/applications/strings/replace.cc

@@ -516,7 +516,7 @@ Nft ReluctantReplace::replace_regex(nfa::Nfa aut, const Word& replacement, Alpha
     const Nft dft_begin_marker{ begin_marker_nft(begin_marker_nfa(aut, alphabet), begin_marker) };
     const Nft nft_reluctant_replace{
         reluctant_leftmost_nft(std::move(aut), alphabet, begin_marker, replacement, replace_mode) };
-    return compose(dft_begin_marker, nft_reluctant_replace);
+    return compose(dft_begin_marker, nft_reluctant_replace, 1, 0, true, mata::nft::JumpMode::NoJump);
 }
 
 Nft ReluctantReplace::replace_literal(const Word& literal, const Word& replacement, Alphabet const* const alphabet,
@@ -551,7 +551,7 @@ Nft ReluctantReplace::replace_literal(const Word& literal, const Word& replaceme
     const Nft nft_literal_replace{
         replace_literal_nft(literal, replacement, alphabet, end_marker, replace_mode)
     };
-    return compose(nft_end_marker, nft_literal_replace);
+    return compose(nft_end_marker, nft_literal_replace, 1, 0, true, mata::nft::JumpMode::NoJump);
 }
 
 Nft ReluctantReplace::replace_symbol(