Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Intersection speedup and refactor #344

Merged
merged 26 commits into from
Sep 28, 2023
Merged
Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
06b53a8
fucking works
kilohsakul Sep 25, 2023
72daba8
tests pass
kilohsakul Sep 25, 2023
6880f4f
done, but sigsegv
kilohsakul Sep 25, 2023
d5c7ce3
almost done, and tests pass with matrix as well as with limits!!!
kilohsakul Sep 25, 2023
1ffc102
done, olé!
kilohsakul Sep 25, 2023
574e0bb
disable the assert in parsing to run the test (cox inter in test inte…
kilohsakul Sep 25, 2023
bfae9a7
is_lang_empty via get_useful_states (much faster)
kilohsakul Sep 25, 2023
d2881a2
before removing ranges to optimize product storage
kilohsakul Sep 26, 2023
2ceecb1
removed ranges optimization and did some little things asked for in r…
kilohsakul Sep 26, 2023
b1a9d72
renamed some things
kilohsakul Sep 26, 2023
5a46057
fix binding
kilohsakul Sep 26, 2023
49d5d75
adding the reverse product to lhs/rhs map as vectors,
kilohsakul Sep 26, 2023
0f01d7c
Update src/nfa/intersection.cc
kilohsakul Sep 28, 2023
31fa23c
Update src/nfa/intersection.cc
kilohsakul Sep 28, 2023
10f110f
Update include/mata/nfa/algorithms.hh
kilohsakul Sep 28, 2023
a375fd1
tf's review
kilohsakul Sep 28, 2023
03e911d
tf's review
kilohsakul Sep 28, 2023
8959594
Update src/nfa/delta.cc
kilohsakul Sep 28, 2023
2960deb
Also optimized language emptiness check a bit (get_useful_states term…
kilohsakul Sep 28, 2023
4d54953
Update src/nfa/intersection.cc
kilohsakul Sep 28, 2023
12fc2d6
some smalll things?
kilohsakul Sep 28, 2023
993be81
Merge remote-tracking branch 'origin/intersection_faster' into inters…
kilohsakul Sep 28, 2023
261c4b7
some smalll things?
kilohsakul Sep 28, 2023
7c43663
some smalll things?
kilohsakul Sep 28, 2023
8025de5
comment
kilohsakul Sep 28, 2023
8614495
comment
kilohsakul Sep 28, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions include/mata/nfa/algorithms.hh
Original file line number Diff line number Diff line change
Expand Up @@ -105,15 +105,15 @@ Simlib::Util::BinaryRelation compute_relation(
/**
* @brief Compute intersection of two NFAs with a possibility of using multiple epsilons.
*
* @param[in] lhs First NFA to compute intersection for.
* @param[in] lhs_source First NFA to compute intersection for.
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved
* @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<Symbol>& epsilons,
std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
Nfa product(const Nfa& lhs_source, const Nfa& rhs, const std::function<bool(State,State)> && final_condition,
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved
const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved

/**
* @brief Concatenate two NFAs.
Expand Down
4 changes: 4 additions & 0 deletions include/mata/nfa/delta.hh
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,10 @@ public:
iterator find(const Symbol symbol) { return super::find({ symbol, {} }); }
const_iterator find(const Symbol symbol) const { return super::find({ symbol, {} }); }

//returns an iterator to the smallest epsilon, or end() if there is no epsilon
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved
const_iterator first_epsilon_it(Symbol first_epsilon) const;


/**
* @brief Iterator over moves represented as @c Move instances.
*
Expand Down
2 changes: 1 addition & 1 deletion include/mata/nfa/nfa.hh
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,7 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs);
* @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<std::pair<State, State>, State> *prod_map = nullptr);
const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr);
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved

/**
* @brief Concatenate two NFAs.
Expand Down
4 changes: 2 additions & 2 deletions include/mata/nfa/plumbing.hh
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,9 @@ inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAut
* Automata must share alphabets.
*/
inline void intersection(Nfa* res, const Nfa& lhs, const Nfa& rhs,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Update the method docstring. Mention that it can (and will?) produce epsilon transitions. Instruct the user to call .remove_epsilon() afterwards on the epsilons to remove them.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wrote something, except not about remove_epsilon(), that's redundant.

bool preserve_epsilon = false,
std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr) {
Adda0 marked this conversation as resolved.
Show resolved Hide resolved
*res = intersection(lhs, rhs, preserve_epsilon, prod_map);
//TODO: first_epsilon should also be a parameter, optional parameter?
Adda0 marked this conversation as resolved.
Show resolved Hide resolved
*res = intersection(lhs, rhs, EPSILON, prod_map);
}

/**
Expand Down
20 changes: 20 additions & 0 deletions src/nfa/delta.cc
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ void SymbolPost::insert(State s) {
}
}

//TODO: slow! This should be doing merge, not inserting one by one.
void SymbolPost::insert(const StateSet& states) {
for (State s : states) {
insert(s);
Expand Down Expand Up @@ -374,6 +375,24 @@ bool Delta::operator==(const Delta& other) const {
return other_transitions_it == other_transitions_end;
}

//Returns an iterator to the smallest epsilon, or end() if there is no epsilon
//Searches from the end of the vector of SymbolPosts, since epsilons are at the end and they are typically few, mostly 1.
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved
StatePost::const_iterator StatePost::first_epsilon_it(Symbol first_epsilon) const {
auto it = end();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Extract end() into a local const variable and use instead of calling end() repeatedly.

Copy link
Collaborator Author

@kilohsakul kilohsakul Sep 28, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am doing this to avoid duscussions,
but to be honest, it is slightly pissing me off, I think it is a premature optimization that makes code clumsy and has no impact on speed

while (it != begin()) {
--it;
if (it->symbol < first_epsilon) { //is it a normal symbol already?
++it; // go step back, to the smallest epsilon or end(), and return it
return it;
kilohsakul marked this conversation as resolved.
Show resolved Hide resolved
}
}

if (it != end() && it->symbol >= first_epsilon) //special case when begin is the smallest epsilon (since the while loop ended before the step back)
return it;

return end();
}

StatePost::Moves::const_iterator::const_iterator(
const StatePost& state_post, const StatePost::const_iterator symbol_post_it,
const StatePost::const_iterator symbol_post_end)
Expand Down Expand Up @@ -478,6 +497,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)
Adda0 marked this conversation as resolved.
Show resolved Hide resolved
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) {
Expand Down
2 changes: 1 addition & 1 deletion src/nfa/inclusion.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}}
Expand Down
Loading