diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index ccb635839..94bad76a6 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/spot/twaalgos/forq_contains.cc @@ -470,7 +470,6 @@ namespace spot::forq bool operator<=(context_set const& other) const override; void add(state initial, std::set> const& other); - bool relevance_test(state_set const& set) const; template void iterate(Callable callable) const @@ -605,8 +604,6 @@ namespace spot::forq for (auto& v_ptr : new_post_f[src]) { auto& [V, word_of_v] = *v_ptr; - if (!V.relevance_test(W)) - continue; auto counter_example = find_counter_example(src, W, word_of_v, setup); @@ -968,52 +965,18 @@ namespace spot::forq } } - static bool operator<=( - std::set> const& f, - std::set> const& s) + static bool operator<=(std::set> const& f, + std::set> const& s) { return std::includes(s.begin(), s.end(), f.begin(), f.end()); } - static bool operator<=( - std::set> const& f, - state_set const& set) - { - if (set.size() < f.size()) - return false; - auto first1 = set.begin(), last1 = set.end(); - auto first2 = f.begin(), last2 = f.begin(); - - for (; first2 != last2; ++first1) - { - if (first1 == last1 || first2->first < *first1) - { - return false; - } - if (first2->first == *first1) - { - ++first2; - } - } - return true; - } - void context_set::add(state initial, std::set> const& other) { states[initial].insert(other.begin(), other.end()); } - bool context_set::relevance_test(state_set const& W) const - { - for (auto& [s1, quazi] : states) - { - if (!(quazi <= W)) - return false; - } - return true; - } - bool context_set::operator<=(context_set const& other) const { for (auto& [s, set] : states) @@ -1022,24 +985,6 @@ namespace spot::forq return false; } return true; - - if (other.states.size() != states.size()) - return false; - auto first1 = other.states.begin(), last1 = other.states.end(); - auto first2 = states.begin(), last2 = states.begin(); - - for (; first2 != last2; ++first1) - { - if (first1 == last1 || first2->first < first1->first) - return false; - if (first2->first == first1->first) - { - if (!(first2->second <= first1->second)) - return false; - ++first2; - } - } - return true; } state_set::state_set(state single_state, bool reversed)