diff --git a/CMakeLists.txt b/CMakeLists.txt index e61b668f8..d07bddd02 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -91,6 +91,11 @@ set(MATA_CLANG_WARNINGS -Wno-system-headers ) +# set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0") +# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0") +# add_compile_options(-fno-omit-frame-pointer -mno-omit-leaf-frame-pointer) +# add_compile_options(-DNDEBUG -g) + # Set whether to treat warnings as errors. if (MATA_WERROR) message("-- Treating warnings in mata as errors") 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/delta.hh b/include/mata/nfa/delta.hh index faa1ab316..8a3f74a59 100644 --- a/include/mata/nfa/delta.hh +++ b/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. * diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index b9962f846..3b41f756f 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -424,8 +424,11 @@ 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, - 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/include/mata/nfa/plumbing.hh b/include/mata/nfa/plumbing.hh index 200472028..1800d6404 100644 --- a/include/mata/nfa/plumbing.hh +++ b/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, State> *prod_map = nullptr) { - *res = intersection(lhs, rhs, preserve_epsilon, prod_map); + *res = intersection(lhs, rhs, prod_map); } /** diff --git a/src/nfa/complement.cc b/src/nfa/complement.cc index a8fc509d7..9b1b8415c 100644 --- a/src/nfa/complement.cc +++ b/src/nfa/complement.cc @@ -74,6 +74,7 @@ Nfa mata::nfa::complement(const Nfa& aut, const mata::utils::OrdVectorsymbol < 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() }; @@ -478,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) { diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 38f00774f..07e602103 100644 --- a/src/nfa/inclusion.cc +++ b/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 }}} diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index 8519a70be..67971a381 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -14,6 +14,7 @@ */ // MATA headers +#include #include "mata/nfa/nfa.hh" #include "mata/nfa/algorithms.hh" @@ -21,6 +22,10 @@ using namespace mata::nfa; namespace { + //using pair_to_state_t = std::vector>; + using pair_to_state_t = std::vector>; + using product_map_t = std::unordered_map,State>; + /** * Add transition to the product. * @param[out] product Created product automaton. @@ -28,18 +33,12 @@ 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, std::unordered_map, State>& product_map, - const std::pair& pair_to_process, SymbolPost& intersection_transition) { +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; } - auto& 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 { - // Product already has some target states for the given symbol from the current product state. - intersection_move_iter->insert(intersection_transition.targets); - } + StatePost& intersect_state_transitions{ product.delta.mutable_state_post(pair_to_state[lhs][rhs]) }; + intersect_state_transitions.push_back(std::move(intersection_transition)); } /** @@ -51,143 +50,147 @@ void add_product_transition(Nfa& product, std::unordered_map, State>& 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 +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& pairs_to_process, + const State lhs_target, + const State rhs_target, + SymbolPost& product_symbol_post ) { - 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); + State intersect_target; + 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); + + if (lhs_nfa.final[lhs_target] && rhs_nfa.final[rhs_target]) { + product_nfa.final.insert(intersect_target); } } else { - intersect_state_to = product_map[intersect_state_pair_to]; + //intersect_state_to = product_map[intersect_state_pair_to]; + intersect_target = pair_to_state[lhs_target][rhs_target]; } - intersect_transitions.insert(intersect_state_to); + //TODO: would push_back and sort at the end be faster? + product_symbol_post.insert(intersect_target); } + } // Anonymous namespace. namespace mata::nfa { -Nfa intersection(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - std::unordered_map, State> *prod_map) { +Nfa mata::nfa::intersection( + const Nfa& lhs_nfa, const Nfa& rhs_nfa, + std::unordered_map, State> *prod_map_ptr/* = nullptr*/, + Symbol first_epsilon/* = Limits::max_symbol*/) { - 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. + Nfa product_nfa{}; // Product of the intersection. // Product map for the generated intersection mapping original state pairs to new product states. - std::unordered_map, State> 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. + std::deque 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(rhs_nfa.num_of_states(), Limits::max_state/100)); // Initialize pairs to process with initial state pairs. - for (const State lhs_initial_state : lhs.initial) { - for (const State rhs_initial_state : rhs.initial) { + 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 std::pair this_and_other_initial_state_pair(lhs_initial_state, rhs_initial_state); - const State new_intersection_state = product.add_state(); + const State product_initial_state = product_nfa.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_map[this_and_other_initial_state_pair] = 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.initial.insert(new_intersection_state); - if (lhs.final[lhs_initial_state] && rhs.final[rhs_initial_state]) { - product.final.insert(new_intersection_state); - } + product_nfa.initial.insert(product_initial_state); } } while (!pairs_to_process.empty()) { - pair_to_process = pairs_to_process.back(); + State rhs_source = pairs_to_process.back();; + pairs_to_process.pop_back(); + State lhs_source = 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]); + mata::utils::push_back(sync_iterator, lhs_nfa.delta[lhs_source]); + mata::utils::push_back(sync_iterator, rhs_nfa.delta[rhs_source]); while (sync_iterator.advance()) { - std::vector moves = sync_iterator.get_current(); - assert(moves.size() == 2); // One move per state in the pair. + std::vector same_symbol_posts = sync_iterator.get_current(); + assert(same_symbol_posts.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 - ); + 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_transition(product, product_map, pair_to_process, intersection_transition); + 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_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); + // 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.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); + // 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; + return product_nfa; } // intersection(). + } // namespace mata::nfa. diff --git a/src/strings/nfa-noodlification.cc b/src/strings/nfa-noodlification.cc index 09820ac9b..e49de6e85 100644 --- a/src/strings/nfa-noodlification.cc +++ b/src/strings/nfa-noodlification.cc @@ -279,7 +279,7 @@ std::vector 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::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 {}; } @@ -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 {}; diff --git a/tests-integration/src/bench-bool-comb-cox-inter.cc b/tests-integration/src/bench-bool-comb-cox-inter.cc index 2118b8de8..b17d759b1 100644 --- a/tests-integration/src/bench-bool-comb-cox-inter.cc +++ b/tests-integration/src/bench-bool-comb-cox-inter.cc @@ -32,10 +32,17 @@ int main(int argc, char *argv[]) { // Setting precision of the times to fixed points and 4 decimal places std::cout << std::fixed << std::setprecision(4); - TIME_BEGIN(emptiness_check); - Nfa intersect_aut = intersection(lhs, rhs); - intersect_aut.is_lang_empty(); - TIME_END(emptiness_check); + // TIME_BEGIN(intersection); + // Nfa intersect_aut = intersection(lhs, rhs); + // TIME_END(intersection); + + TIME_BEGIN(intersection2); + Nfa intersect_aut2 = intersection(lhs, rhs); + TIME_END(intersection2); + +// TIME_BEGIN(emptiness_check); +// intersect_aut.is_lang_empty(); +// TIME_END(emptiness_check); return EXIT_SUCCESS; } diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index e85f8fd47..04ddce8f3 100644 --- a/tests-integration/src/utils/utils.cc +++ b/tests-integration/src/utils/utils.cc @@ -62,7 +62,7 @@ int load_automata( std::vector mintermized = mintermization.mintermize(inter_auts); TIME_END(mintermization); for (mata::IntermediateAut& inter_aut : mintermized) { - assert(inter_aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR); + //assert(inter_aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR); auts.push_back(mata::nfa::builder::construct(inter_aut, &alphabet)); } } diff --git a/tests/nfa/nfa-intersection.cc b/tests/nfa/nfa-intersection.cc index ffa35c1e5..2fa054216 100644 --- a/tests/nfa/nfa-intersection.cc +++ b/tests/nfa/nfa-intersection.cc @@ -75,7 +75,7 @@ TEST_CASE("mata::nfa::intersection()") SECTION("Intersection of empty automata") { - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial.empty()); REQUIRE(res.final.empty()); @@ -108,7 +108,7 @@ TEST_CASE("mata::nfa::intersection()") REQUIRE(!a.final.empty()); REQUIRE(!b.final.empty()); - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(!res.initial.empty()); REQUIRE(!res.final.empty()); @@ -127,7 +127,7 @@ TEST_CASE("mata::nfa::intersection()") FILL_WITH_AUT_A(a); FILL_WITH_AUT_B(b); - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial[prod_map[{1, 4}]]); REQUIRE(res.initial[prod_map[{3, 4}]]); @@ -178,7 +178,7 @@ TEST_CASE("mata::nfa::intersection()") FILL_WITH_AUT_B(b); b.final = {12}; - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial[prod_map[{1, 4}]]); REQUIRE(res.initial[prod_map[{3, 4}]]); @@ -215,7 +215,7 @@ TEST_CASE("mata::nfa::intersection() with preserving epsilon transitions") b.delta.add(6, 'a', 9); b.delta.add(6, 'b', 7); - Nfa result{intersection(a, b, true, &prod_map) }; + Nfa result{intersection(a, b, &prod_map) }; // Check states. CHECK(result.is_state(prod_map[{0, 0}])); @@ -315,7 +315,7 @@ TEST_CASE("mata::nfa::intersection() for profiling", "[.profiling],[intersection b.delta.add(6, 'b', 7); for (size_t i{ 0 }; i < 10000; ++i) { - Nfa result{intersection(a, b, true) }; + Nfa result{intersection(a, b) }; } } diff --git a/tests/strings/nfa-noodlification.cc b/tests/strings/nfa-noodlification.cc index c974bafb9..87ed8ea34 100644 --- a/tests/strings/nfa-noodlification.cc +++ b/tests/strings/nfa-noodlification.cc @@ -191,7 +191,7 @@ TEST_CASE("mata::nfa::SegNfa::noodlify_for_equation()") { noodle.delta.add(0, 0, 1); noodle.final.insert(1); auto result{ seg_nfa::noodlify_for_equation({ left1, left2 }, right) }; - REQUIRE(result.size() == 1); + REQUIRE(result.size() == 1); } SECTION("Larger automata") {