segfaoult

include/mata/nfa/algorithms.hh

@@ -115,8 +115,6 @@ Simlib::Util::BinaryRelation compute_relation(
 Nfa intersection_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set<Symbol>& epsilons,
     std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
 
-Nfa intersection_eps2(const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set<Symbol>& epsilons,
-                      std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
 /**
  * @brief Concatenate two NFAs.
  *

include/mata/nfa/delta.hh

@@ -123,6 +123,8 @@ public:
     iterator find(const Symbol symbol) { return super::find({ symbol, {} }); }
     const_iterator find(const Symbol symbol) const { return super::find({ symbol, {} }); }
 
+    const_iterator first_epsilon_it(Symbol first_epsilon) const;
+
     /**
      * @brief Iterator over moves represented as @c Move instances.
      *

include/mata/nfa/nfa.hh

@@ -424,11 +424,13 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs);
  * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states.
  * @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved.
  */
-Nfa intersection(const Nfa& lhs, const Nfa& rhs,
+Nfa intersection_old(const Nfa& lhs, const Nfa& rhs,
                  bool preserve_epsilon = false, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr);
 
-Nfa intersection2(const Nfa& lhs, const Nfa& rhs,
-                 bool preserve_epsilon = false, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr);
+Nfa intersection(
+        const Nfa& lhs_nfa, const Nfa& rhs_nfa,
+        std::unordered_map<std::pair<State, State>, State> *prod_map_ptr = nullptr,
+        Symbol first_epsilon = Limits::max_symbol);
 
 
 /**

include/mata/nfa/plumbing.hh

@@ -88,7 +88,7 @@ inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAut
 inline void intersection(Nfa* res, const Nfa& lhs, const Nfa& rhs,
                   bool preserve_epsilon = false,
                   std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr) {
-    *res = intersection(lhs, rhs, preserve_epsilon, prod_map);
+    *res = intersection(lhs, rhs, prod_map);
 }
 
 /**

src/nfa/complement.cc

@@ -74,6 +74,7 @@ Nfa mata::nfa::complement(const Nfa& aut, const mata::utils::OrdVector<mata::Sym
                                  " received an unknown value of the \"algo\" key: " + str_algo);
     }
 
+    //TODO: what is this thing? Explain plz in a comment.
     bool minimize_during_determinization = false;
     if (params.find("minimize") != params.end()) {
         const std::string& minimize_arg = params.at("minimize");

src/nfa/delta.cc

@@ -469,6 +469,18 @@ StatePost::Moves StatePost::moves(
     return { *this, symbol_post_it, symbol_post_end };
 }
 
+//returns an iterator to the smallest epsilon, or end() if there is no epsilon
+StatePost::const_iterator StatePost::first_epsilon_it(Symbol first_epsilon) const {
+    for (auto it = end(); it != begin(); ) {
+        --it;
+        if (it->symbol < first_epsilon) {
+            ++it;
+            return it;
+        }
+    }
+    return end();
+}
+
 StatePost::Moves StatePost::moves_epsilons(const Symbol first_epsilon) const {
     const StatePost::const_iterator symbol_post_begin{ cbegin() };
     const StatePost::const_iterator symbol_post_end{ cend() };
@@ -479,6 +491,7 @@ StatePost::Moves StatePost::moves_epsilons(const Symbol first_epsilon) const {
         return { *this, symbol_post_begin, symbol_post_end };
     }
 
+    //TODO: some comments, my brain hurts. Can we use first_epsilon_it above (or rewrite its code as below)
     StatePost::const_iterator previous_symbol_post_it{ std::prev(symbol_post_end) };
     StatePost::const_iterator symbol_post_it{ previous_symbol_post_it };
     while (previous_symbol_post_it != symbol_post_begin && first_epsilon < previous_symbol_post_it->symbol) {

src/nfa/inclusion.cc

@@ -35,7 +35,7 @@ bool mata::nfa::algorithms::is_included_naive(
     } else {
         bigger_cmpl = complement(bigger, *alphabet);
     }
-    Nfa nfa_isect = intersection(smaller, bigger_cmpl, false, nullptr);
+    Nfa nfa_isect = intersection(smaller, bigger_cmpl);
 
     return nfa_isect.is_lang_empty(cex);
 } // is_included_naive }}}

src/nfa/intersection.cc

@@ -24,7 +24,7 @@ namespace {
 
     //using pair_to_state_t = std::vector<std::unordered_map<State,State>>;
     using pair_to_state_t = std::vector<std::vector<State>>;
-    using state_map_t = std::unordered_map<std::pair<State,State>,State>;
+    using product_map_t = std::unordered_map<std::pair<State,State>,State>;
 
 /**
  * Add transition to the product.
@@ -33,7 +33,7 @@ namespace {
  * @param[in] pair_to_process Currently processed pair of original states.
  * @param[in] intersection_transition State transitions to add to the product.
  */
-void add_product_transition(Nfa& product, state_map_t& product_map,
+void add_product_transition(Nfa& product, product_map_t& product_map,
                             const std::pair<State,State>& pair_to_process, SymbolPost& intersection_transition) {
     if (intersection_transition.empty()) { return; }
 
@@ -68,7 +68,7 @@ void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state,
  */
 void create_product_state_and_trans(
             Nfa& product,
-            state_map_t& product_map,
+            product_map_t& product_map,
             const Nfa& lhs,
             const Nfa& rhs,
             std::deque<std::pair<State,State>>& pairs_to_process,
@@ -91,9 +91,10 @@ void create_product_state_and_trans(
     }
     intersect_transitions.insert(intersect_state_to);
 }
-void create_product_state_and_transition2(
+void create_product_state_and_move2(
         Nfa& product_nfa,
         pair_to_state_t & pair_to_state,
+        product_map_t * prod_map,
         const Nfa& lhs_nfa,
         const Nfa& rhs_nfa,
         std::deque<State>& pairs_to_process,
@@ -102,12 +103,14 @@ void create_product_state_and_transition2(
         SymbolPost& product_symbol_post
 ) {
     State intersect_target;
-    if (pair_to_state[lhs_target][rhs_target] == 1000000) {
+    if (pair_to_state[lhs_target][rhs_target] == Limits::max_state) {
         //if (pair_to_state[intersect_state_pair_to.first].find(intersect_state_pair_to.second) == pair_to_state[intersect_state_pair_to.first].end()) {
         //if (product_map.find(intersect_state_pair_to) == product_map.end()) {
         intersect_target = product_nfa.add_state();
         //product_map[intersect_state_pair_to] = intersect_state_to;
         pair_to_state[lhs_target][rhs_target] = intersect_target;
+        if (prod_map != nullptr) //this is here to appease tests
+            (*prod_map)[std::pair(lhs_target,rhs_target)] = intersect_target;
         pairs_to_process.push_back(lhs_target);
         pairs_to_process.push_back(rhs_target);
 
@@ -127,27 +130,19 @@ void create_product_state_and_transition2(
 
 namespace mata::nfa {
 
-Nfa intersection(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon,
-                 state_map_t *prod_map) {
+Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon,
+                     product_map_t *prod_map) {
 
     const std::set<Symbol> epsilons({EPSILON});
     return algorithms::intersection_eps(lhs, rhs, preserve_epsilon, epsilons, prod_map);
 }
 
-Nfa intersection2(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon,
-                 state_map_t *prod_map) {
-
-    const std::set<Symbol> epsilons({EPSILON});
-    return algorithms::intersection_eps2(lhs, rhs, preserve_epsilon, epsilons, prod_map);
-}
-
-
 Nfa mata::nfa::algorithms::intersection_eps(
         const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set<Symbol>& epsilons,
         std::unordered_map<std::pair<State, State>, State> *prod_map) {
     Nfa product{}; // Product of the intersection.
     // Product map for the generated intersection mapping original state pairs to new product states.
-    state_map_t product_map{};
+    product_map_t product_map{};
     std::pair<State,State> pair_to_process{}; // State pair of original states currently being processed.
     std::deque<std::pair<State,State>> pairs_to_process{}; // Set of state pairs of original states to process.
 
@@ -244,29 +239,32 @@ Nfa mata::nfa::algorithms::intersection_eps(
     return product;
 } // intersection().
 
-Nfa mata::nfa::algorithms::intersection_eps2(
-        const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set<Symbol>& epsilons,
-        std::unordered_map<std::pair<State, State>, State> *prod_map) {
+Nfa mata::nfa::intersection(
+        const Nfa& lhs_nfa, const Nfa& rhs_nfa,
+        std::unordered_map<std::pair<State, State>, State> *prod_map_ptr/* = nullptr*/,
+        Symbol first_epsilon/* = Limits::max_symbol*/) {
+
     Nfa product_nfa{}; // Product of the intersection.
     // Product map for the generated intersection mapping original state pairs to new product states.
-    state_map_t product_map{};
     std::deque<State> pairs_to_process{}; // Set of state pairs of original states to process.
 
     //pair_to_state_t pair_to_state(lhs.num_of_states());
-    pair_to_state_t pair_to_state(lhs_nfa.num_of_states(), std::vector<State>(rhs_nfa.num_of_states(), 1000000));
+    pair_to_state_t pair_to_state(lhs_nfa.num_of_states(), std::vector<State>(rhs_nfa.num_of_states(), Limits::max_state/100));
 
     // Initialize pairs to process with initial state pairs.
     for (const State lhs_initial_state : lhs_nfa.initial) {
         for (const State rhs_initial_state : rhs_nfa.initial) {
             // Update product with initial state pairs.
-            const State new_intersection_state = product_nfa.add_state();
+            const State product_initial_state = product_nfa.add_state();
 
             //product_map[this_and_other_initial_state_pair] = new_intersection_state;
-            pair_to_state[lhs_initial_state][rhs_initial_state] = new_intersection_state;
+            pair_to_state[lhs_initial_state][rhs_initial_state] = product_initial_state;
+            if (prod_map_ptr != nullptr) //this is here to appease tests
+                (*prod_map_ptr)[std::pair(lhs_initial_state, rhs_initial_state)] = product_initial_state;
             pairs_to_process.push_back(lhs_initial_state);
             pairs_to_process.push_back(rhs_initial_state);
 
-            product_nfa.initial.insert(new_intersection_state);
+            product_nfa.initial.insert(product_initial_state);
         }
     }
 
@@ -289,67 +287,58 @@ Nfa mata::nfa::algorithms::intersection_eps2(
             // Find all transitions that have the same symbol for first and the second state in the pair_to_process.
             // Create transition from the pair_to_process to all pairs between states to which first transition goes
             //  and states to which second one goes.
-            SymbolPost product_symbol_post{same_symbol_posts[0]->symbol };
-            for (const State lhs_target: same_symbol_posts[0]->targets)
-            {
-                for (const State rhs_target: same_symbol_posts[1]->targets)
-                {
-                    create_product_state_and_transition2(
-                            product_nfa, pair_to_state, lhs_nfa, rhs_nfa, pairs_to_process,
-                            lhs_target, rhs_target, product_symbol_post
-                    );
+            Symbol symbol = same_symbol_posts[0]->symbol;
+            if (symbol < first_epsilon) {
+                SymbolPost product_symbol_post{symbol};
+                for (const State lhs_target: same_symbol_posts[0]->targets) {
+                    for (const State rhs_target: same_symbol_posts[1]->targets) {
+                        create_product_state_and_move2(
+                                product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa, pairs_to_process,
+                                lhs_target, rhs_target, product_symbol_post
+                        );
+                    }
                 }
+                add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, product_symbol_post);
             }
-            add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, product_symbol_post);
+            else
+                break;
         }
 
-        if (preserve_epsilon) {
-            // Add transitions of the current state pair for an epsilon preserving product.
-
-            // Check for lhs epsilon transitions.
-            const StatePost& lhs_state_post{lhs_nfa.delta[lhs_source] };
-            if (!lhs_state_post.empty()) {
-                //TODO: does this copy the symbol post?
-                const SymbolPost& lhs_last_symbol_post{lhs_state_post.back() };
-                if (epsilons.find(lhs_last_symbol_post.symbol) != epsilons.end()) {
-                    // Compute product for state transitions with lhs state epsilon transition.
-                    // Create transition from the pair_to_process to all pairs between states to which first transition
-                    //  goes and states to which second one goes.
-                    SymbolPost lhs_symbol_post{lhs_last_symbol_post.symbol };
-                    for (const State lhs_state_to: lhs_last_symbol_post.targets) {
-                        create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa,
-                                                             pairs_to_process,
-                                                             lhs_state_to, rhs_source,
-                                                             lhs_symbol_post);
-                    }
-                    add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source,
-                                             lhs_symbol_post);
+        // Add epsilon transitions, from lhs e-transitions.
+        const StatePost& lhs_state_post{lhs_nfa.delta[lhs_source] };
+        auto lhs_first_epsilon_it = lhs_state_post.first_epsilon_it(first_epsilon);
+        if (lhs_first_epsilon_it != lhs_state_post.end()) {
+            for (auto lhs_symbol_post = lhs_first_epsilon_it; lhs_symbol_post < lhs_state_post.end(); lhs_symbol_post++) {
+                SymbolPost prod_symbol_post{lhs_symbol_post->symbol };
+                for (const State lhs_target: lhs_symbol_post->targets) {
+                    create_product_state_and_move2(product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa,
+                                                   pairs_to_process,
+                                                   lhs_target, rhs_source,
+                                                   prod_symbol_post);
                 }
+                add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source,
+                                         prod_symbol_post);
             }
+        }
 
-            // Check for rhs epsilon transitions in case only rhs has any transitions and add them.
-            const StatePost& rhs_post{rhs_nfa.delta[rhs_source]};
-            if (!rhs_post.empty()) {
-                const auto& rhs_state_last_transitions{ rhs_post.back()};
-                if (epsilons.find(rhs_state_last_transitions.symbol) != epsilons.end()) {
-                    // Compute product for state transitions with rhs state epsilon transition.
-                    // Create transition from the pair_to_process to all pairs between states to which first transition
-                    //  goes and states to which second one goes.
-                    SymbolPost intersection_transition{ rhs_state_last_transitions.symbol };
-                    for (const State rhs_state_to: rhs_state_last_transitions.targets) {
-                        create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa,
-                                                             pairs_to_process,
-                                                             lhs_source, rhs_state_to,
-                                                             intersection_transition);
-                    }
-                    add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source,
-                                             intersection_transition);
+        // Add epsilon transitions, from rhs e-transitions.
+        const StatePost& rhs_state_post{rhs_nfa.delta[rhs_source] };
+        auto rhs_first_epsilon_it = rhs_state_post.first_epsilon_it(first_epsilon);
+        if (rhs_first_epsilon_it != rhs_state_post.end()) {
+            for (auto rhs_symbol_post = rhs_first_epsilon_it; rhs_symbol_post < rhs_state_post.end(); rhs_symbol_post++) {
+                SymbolPost prod_symbol_post{rhs_symbol_post->symbol };
+                for (const State rhs_target: rhs_symbol_post->targets) {
+                    create_product_state_and_move2(product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa,
+                                                   pairs_to_process,
+                                                   lhs_source, rhs_target,
+                                                   prod_symbol_post);
                 }
+                add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source,
+                                         prod_symbol_post);
             }
         }
     }
 
-    if (prod_map != nullptr) { *prod_map = product_map; }
     return product_nfa;
 } // intersection().
 

src/strings/nfa-noodlification.cc

@@ -279,7 +279,7 @@ std::vector<seg_nfa::Noodle> seg_nfa::noodlify_for_equation(
     }
 
     auto product_pres_eps_trans{
-            intersection(concatenated_lhs, rhs_automaton, true).trim() };
+            intersection(concatenated_lhs, rhs_automaton).trim() };
     if (product_pres_eps_trans.is_lang_empty()) {
         return {};
     }
@@ -328,7 +328,7 @@ std::vector<seg_nfa::Noodle> seg_nfa::noodlify_for_equation(
     }
 
     auto product_pres_eps_trans{
-            intersection(concatenated_lhs, rhs_automaton, true).trim() };
+            intersection(concatenated_lhs, rhs_automaton).trim() };
     if (product_pres_eps_trans.is_lang_empty()) {
         return {};
     }

tests-integration/src/bench-bool-comb-cox-inter.cc

@@ -37,7 +37,7 @@ int main(int argc, char *argv[]) {
  //   TIME_END(intersection);
 
     TIME_BEGIN(intersection2);
-    Nfa intersect_aut2 = intersection2(lhs, rhs);
+    Nfa intersect_aut2 = intersection(lhs, rhs);
     TIME_END(intersection2);
 
 //    TIME_BEGIN(emptiness_check);