From f0a51ba85e1f4e748aece38639ce3c3070f87c0c Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sun, 24 Sep 2023 23:01:41 +0200 Subject: [PATCH] only one version --- include/mata/nfa/algorithms.hh | 12 --- include/mata/nfa/nfa.hh | 3 - src/nfa/intersection.cc | 150 ------------------------------ src/strings/nfa-noodlification.cc | 2 +- 4 files changed, 1 insertion(+), 166 deletions(-) diff --git a/include/mata/nfa/algorithms.hh b/include/mata/nfa/algorithms.hh index 0dc296db6..f4a9b3ecc 100644 --- a/include/mata/nfa/algorithms.hh +++ b/include/mata/nfa/algorithms.hh @@ -102,18 +102,6 @@ Simlib::Util::BinaryRelation compute_relation( const Nfa& aut, const ParameterMap& params = {{ "relation", "simulation"}, { "direction", "forward"}}); -/** - * @brief Compute intersection of two NFAs with a possibility of using multiple epsilons. - * - * @param[in] lhs First NFA to compute intersection for. - * @param[in] rhs Second NFA to compute intersection for. - * @param[in] preserve_epsilon Whether to compute intersection preserving epsilon transitions. - * @param[in] epsilons Set of symbols to be considered as epsilons - * @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_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, - std::unordered_map, State> *prod_map = nullptr); /** * @brief Concatenate two NFAs. diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 6ecf1c62c..3b41f756f 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -424,15 +424,12 @@ 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_old(const Nfa& lhs, const Nfa& rhs, - bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); Nfa intersection( const Nfa& lhs_nfa, const Nfa& rhs_nfa, std::unordered_map, State> *prod_map_ptr = nullptr, Symbol first_epsilon = Limits::max_symbol); - /** * @brief Concatenate two NFAs. * diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index b2cf97cd0..67971a381 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -33,22 +33,6 @@ 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, product_map_t& product_map, - const std::pair& pair_to_process, SymbolPost& intersection_transition) { - if (intersection_transition.empty()) { return; } - - StatePost& intersect_state_transitions{ product.delta.mutable_state_post(product_map[pair_to_process]) }; - auto intersection_move_iter{ intersect_state_transitions.find(intersection_transition) }; - if (intersection_move_iter == intersect_state_transitions.end()) { - intersect_state_transitions.insert(intersection_transition); - } else { - if (++intersection_move_iter != intersect_state_transitions.end()) - std::cout<<"fuck"; - // Product already has some target states for the given symbol from the current product state. - intersection_move_iter->insert(intersection_transition.targets); - } -} - void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, const State lhs, const State rhs, SymbolPost& intersection_transition) { if (intersection_transition.empty()) { return; } @@ -66,31 +50,6 @@ void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, * @param[in] rhs_state_to Target state in NFA @c rhs. * @param[out] intersect_transitions Transitions of the product state. */ -void create_product_state_and_trans( - Nfa& product, - product_map_t& product_map, - const Nfa& lhs, - const Nfa& rhs, - std::deque>& pairs_to_process, - const State lhs_state_to, - const State rhs_state_to, - SymbolPost& intersect_transitions -) { - const std::pair intersect_state_pair_to(lhs_state_to, rhs_state_to); - State intersect_state_to; - if (product_map.find(intersect_state_pair_to) == product_map.end()) { - intersect_state_to = product.add_state(); - product_map[intersect_state_pair_to] = intersect_state_to; - pairs_to_process.push_back(intersect_state_pair_to); - - if (lhs.final[lhs_state_to] && rhs.final[rhs_state_to]) { - product.final.insert(intersect_state_to); - } - } else { - intersect_state_to = product_map[intersect_state_pair_to]; - } - intersect_transitions.insert(intersect_state_to); -} void create_product_state_and_move2( Nfa& product_nfa, pair_to_state_t & pair_to_state, @@ -130,115 +89,6 @@ void create_product_state_and_move2( namespace mata::nfa { -Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - product_map_t *prod_map) { - - const std::set epsilons({EPSILON}); - return algorithms::intersection_eps(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& epsilons, - std::unordered_map, State> *prod_map) { - Nfa product{}; // Product of the intersection. - // Product map for the generated intersection mapping original state pairs to new product states. - product_map_t product_map{}; - std::pair pair_to_process{}; // State pair of original states currently being processed. - std::deque> pairs_to_process{}; // Set of state pairs of original states to process. - - // Initialize pairs to process with initial state pairs. - for (const State lhs_initial_state : lhs.initial) { - for (const State rhs_initial_state : rhs.initial) { - // Update product with initial state pairs. - const std::pair this_and_other_initial_state_pair(lhs_initial_state, rhs_initial_state); - const State new_intersection_state = product.add_state(); - - product_map[this_and_other_initial_state_pair] = new_intersection_state; - pairs_to_process.push_back(this_and_other_initial_state_pair); - - product.initial.insert(new_intersection_state); - if (lhs.final[lhs_initial_state] && rhs.final[rhs_initial_state]) { - product.final.insert(new_intersection_state); - } - } - } - - while (!pairs_to_process.empty()) { - pair_to_process = pairs_to_process.back(); - pairs_to_process.pop_back(); - // Compute classic product for current state pair. - - mata::utils::SynchronizedUniversalIterator::const_iterator> sync_iterator(2); - mata::utils::push_back(sync_iterator, lhs.delta[pair_to_process.first]); - mata::utils::push_back(sync_iterator, rhs.delta[pair_to_process.second]); - - while (sync_iterator.advance()) { - std::vector moves = sync_iterator.get_current(); - assert(moves.size() == 2); // One move per state in the pair. - - // Compute product for state transitions with same symbols. - // 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 intersection_transition{ moves[0]->symbol }; - for (const State this_state_to: moves[0]->targets) - { - for (const State other_state_to: moves[1]->targets) - { - create_product_state_and_trans( - product, product_map, lhs, rhs, pairs_to_process, - this_state_to, other_state_to, intersection_transition - ); - } - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - - if (preserve_epsilon) { - // Add transitions of the current state pair for an epsilon preserving product. - - // Check for lhs epsilon transitions. - const StatePost& lhs_post{ lhs.delta[pair_to_process.first] }; - if (!lhs_post.empty()) { - const auto& lhs_state_last_transitions{ lhs_post.back() }; - if (epsilons.find(lhs_state_last_transitions.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 intersection_transition{ lhs_state_last_transitions.symbol }; - for (const State lhs_state_to: lhs_state_last_transitions.targets) { - create_product_state_and_trans(product, product_map, lhs, rhs, pairs_to_process, - lhs_state_to, pair_to_process.second, - intersection_transition); - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - } - - // Check for rhs epsilon transitions in case only rhs has any transitions and add them. - const StatePost& rhs_post{ rhs.delta[pair_to_process.second]}; - 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_trans(product, product_map, lhs, rhs, pairs_to_process, - pair_to_process.first, rhs_state_to, - intersection_transition); - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - } - } - } - - if (prod_map != nullptr) { *prod_map = product_map; } - return product; -} // intersection(). - Nfa mata::nfa::intersection( const Nfa& lhs_nfa, const Nfa& rhs_nfa, std::unordered_map, State> *prod_map_ptr/* = nullptr*/, diff --git a/src/strings/nfa-noodlification.cc b/src/strings/nfa-noodlification.cc index 7ebdbcf22..e49de6e85 100644 --- a/src/strings/nfa-noodlification.cc +++ b/src/strings/nfa-noodlification.cc @@ -386,7 +386,7 @@ std::vector seg_nfa::noodlify_for_equation( const std::set epsilons({EPSILON, EPSILON-1}); auto product_pres_eps_trans{ - intersection_eps(concatenated_lhs, concatenated_rhs, true, epsilons).trim() }; + intersection(concatenated_lhs, concatenated_rhs, nullptr, EPSILON-1).trim() }; if (product_pres_eps_trans.is_lang_empty()) { return {};