Merge pull request #357 from VeriFIT/improve_intersection

Resolve discussions from previous PRs #patch

include/mata/nfa/nfa.hh

@@ -173,9 +173,12 @@ public:
      * @brief Get the useful states using a modified Tarjan's algorithm. A state
      * is useful if it is reachable from an initial state and can reach a final state.
      *
+     * @param state_at_first_useful_state Whether only the first found useful state is set to true. Useful when
+     *  checking whether the set of useful states is empty.
+     *
      * @return BoolVector Bool vector whose ith value is true iff the state i is useful.
      */
-    BoolVector get_useful_states(bool stop_at_first_useful_state = false) const;
+    BoolVector get_useful_states(const bool stop_at_first_useful_state = false) const;
 
     /**
      * @brief Remove inaccessible (unreachable) and not co-accessible (non-terminating) states in-place.

include/mata/nfa/plumbing.hh

@@ -90,7 +90,6 @@ inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAut
  */
 inline void intersection(Nfa* res, const Nfa& lhs, const Nfa& rhs, Symbol first_epsilon = EPSILON,
                   std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr) {
-    //TODO: first_epsilon should also be a parameter, optional parameter?
     *res = intersection(lhs, rhs, first_epsilon, prod_map);
 }
 

include/mata/parser/inter-aut.hh

@@ -124,13 +124,18 @@ public:
  * and q1 and s2 being children nodes of the root.
  */
 class FormulaGraph {
+private:
+    /// Maximal number of @c FormulaNode children in any @c FormulaGraph node (for AND, OR nodes). Only one (NOT node)
+    ///  or zero (@c FormulaNode node) children may be used. Used as an optimalization by preallocating @c children at
+    ///  node initialization.
+    static constexpr size_t MAX_NUM_OF_CHILDREN{ 2 };
 public:
     FormulaNode node{};
     std::vector<FormulaGraph> children{};
 
     FormulaGraph() = default;
-    explicit FormulaGraph(const FormulaNode& n) : node(n), children() { children.reserve(2); }
-    explicit FormulaGraph(FormulaNode&& n) : node(std::move(n)), children() { children.reserve(2); }
+    explicit FormulaGraph(const FormulaNode& n) : node(n), children() { children.reserve(MAX_NUM_OF_CHILDREN); }
+    explicit FormulaGraph(FormulaNode&& n) : node(std::move(n)), children() { children.reserve(MAX_NUM_OF_CHILDREN); }
     FormulaGraph(const FormulaGraph& g) : node(g.node), children(g.children) {}
     FormulaGraph(FormulaGraph&& g) noexcept : node(std::move(g.node)), children(std::move(g.children)) {}
 

include/mata/utils/utils.hh

@@ -68,13 +68,13 @@ class BoolVector : public std::vector<uint8_t> {
 public:
     BoolVector(size_t size, bool value) : std::vector<uint8_t>(size, value ? 1 : 0) {}
     BoolVector(const BoolVector&) = default;
-    BoolVector(BoolVector&&) = default;
+    BoolVector(BoolVector&&) noexcept = default;
     BoolVector() = default;
     BoolVector(std::initializer_list<uint8_t> uint8_ts): std::vector<uint8_t>(uint8_ts) {}
     explicit BoolVector(const std::vector<uint8_t>& uint8_ts): std::vector<uint8_t>(uint8_ts) {}
 
     BoolVector& operator=(const BoolVector&) = default;
-    BoolVector& operator=(BoolVector&&) = default;
+    BoolVector& operator=(BoolVector&&) noexcept = default;
 
     /// Count the number of set elements.
     size_t count() const {

src/nfa/delta.cc

@@ -488,48 +488,12 @@ StatePost::Moves StatePost::moves(
 }
 
 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() };
-    if (empty()) {
-        return { *this, symbol_post_end, symbol_post_end };
-    }
-    if (symbol_post_begin->symbol >= first_epsilon) {
-        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) {
-        symbol_post_it = previous_symbol_post_it;
-        --previous_symbol_post_it;
-    }
-    if (first_epsilon <= previous_symbol_post_it->symbol) {
-        return { *this, previous_symbol_post_it, symbol_post_end };
-    }
-    if (first_epsilon <= symbol_post_it->symbol) {
-        return { *this, symbol_post_it, symbol_post_end };
-    }
-    return { *this, symbol_post_end, symbol_post_end };
+    return { *this, first_epsilon_it(first_epsilon), cend() };
 }
 
 StatePost::Moves StatePost::moves_symbols(const Symbol last_symbol) const {
-    const StatePost::const_iterator symbol_post_end{ cend() };
-    const StatePost::const_iterator symbol_post_begin{ cbegin() };
-    if (empty() || symbol_post_begin->symbol > last_symbol) {
-        return { *this, symbol_post_end, symbol_post_end };
-    }
-
-    StatePost::const_iterator end_symbol_post_it { symbol_post_end };
-    StatePost::const_iterator previous_end_symbol_post_it{ std::prev(symbol_post_end) };
-    while (previous_end_symbol_post_it != symbol_post_begin && last_symbol < previous_end_symbol_post_it->symbol) {
-        end_symbol_post_it = previous_end_symbol_post_it;
-        --previous_end_symbol_post_it;
-    }
-    // Either previous_end_symbol_post_it is == symbol_post_begin, at which case we should iterate only over the first
-    //  symbol post (that is, end_symbol_post_it == symbol_post_begin + 1); or, previous_end_symbol_post_it jumped over
-    //  last_symbol and end_symbol_post_it is the first symbol post (or end()) after last symbol.
-    return { *this, symbol_post_begin, end_symbol_post_it };
+    if (last_symbol == EPSILON) { throw std::runtime_error("Using default epsilon as a last symbol to iterate over."); }
+    return { *this, cbegin(), first_epsilon_it(last_symbol + 1) };
 }
 
 StatePost::Moves::const_iterator StatePost::Moves::begin() const {

src/nfa/nfa.cc

@@ -243,14 +243,14 @@ namespace {
  *
  * @return BoolVector
  *
- * If stop_at_first_useful_state is true, then the algo stops at the first found useful state.
- * This is used at emptiness test.
+ * If @p stop_at_first_useful_state is true, then the algo stops at the first found useful state. This is used in an
+ *  emptiness test.
  */
-BoolVector Nfa::get_useful_states(bool stop_at_first_useful_state) const {
+BoolVector Nfa::get_useful_states(const bool stop_at_first_useful_state) const {
     BoolVector useful(this->num_of_states(),false);
     std::vector<TarjanNodeData> node_info(this->num_of_states());
-    std::deque<State> program_stack;
-    std::deque<State> tarjan_stack;
+    std::vector<State> program_stack;
+    std::vector<State> tarjan_stack;
     unsigned long index_cnt = 0;
 
     for(const State& q0 : initial) {
@@ -275,8 +275,7 @@ BoolVector Nfa::get_useful_states(bool stop_at_first_useful_state) const {
             tarjan_stack.push_back(act_state);
             if(this->final.contains(act_state)) {
                 useful[act_state] = true;
-                if (stop_at_first_useful_state)
-                    return useful;
+                if (stop_at_first_useful_state) { return useful; }
             }
         } else { // return from the recursive call
             State act_succ = act_state_data.get_curr_succ();
@@ -325,13 +324,13 @@ BoolVector Nfa::get_useful_states(bool stop_at_first_useful_state) const {
                 scc.push_back(st);
             } while(st != act_state);
             if(final_scc) {
-                // propagate usefulness to the closed SCC
-                for(const State& st : scc) useful[st] = true;
-                // propagate usefulness to predecessors in @p tarjan_stack
-                for (auto st = tarjan_stack.rbegin(); st != tarjan_stack.rend(); ++st) {
-                    if (useful[*st])
-                        break;
-                    useful[*st] = true;
+                // Propagate usefulness to the closed SCC.
+                for(const State& st: scc) { useful[st] = true; }
+                // Propagate usefulness to predecessors in @p tarjan_stack.
+                for (auto state_it{ tarjan_stack.rbegin() }, state_it_end{ tarjan_stack.rend() };
+                     state_it != state_it_end; ++state_it) {
+                    if (useful[*state_it]) { break; }
+                    useful[*state_it] = true;
                 }
             }
         }

src/strings/nfa-noodlification.cc

@@ -384,7 +384,6 @@ std::vector<seg_nfa::NoodleWithEpsilonsCounter> seg_nfa::noodlify_for_equation(
         concatenated_rhs = concatenate_eps(concatenated_rhs, **next_rhs_aut_it, EPSILON-1, true); // we use EPSILON-1
     }
 
-    const std::set<Symbol> epsilons({EPSILON, EPSILON-1});
     auto product_pres_eps_trans{
             intersection(concatenated_lhs, concatenated_rhs, EPSILON-1).trim() };
 
@@ -402,7 +401,7 @@ std::vector<seg_nfa::NoodleWithEpsilonsCounter> seg_nfa::noodlify_for_equation(
             product_pres_eps_trans = revert(product_pres_eps_trans);
         }
     }
-    return noodlify_mult_eps(product_pres_eps_trans, epsilons, include_empty);
+    return noodlify_mult_eps(product_pres_eps_trans, { EPSILON, EPSILON-1 }, include_empty);
 }
 
 seg_nfa::VisitedEpsilonsCounterVector seg_nfa::process_eps_map(const VisitedEpsilonsCounterMap& eps_cnt) {