From 6eff384fca3a1b32711384b53f590508e1eba01c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 Sep 2023 11:23:57 +0200
Subject: [PATCH] forq: remove the relevance test

Looks like the comparison operator between std::set<std::pair<state,
bool>> and std::set<state> had a few issue.  This is part of an
optimization that Pierre Ganty prefers to see removed, so I'm just
removing that code.

For reference, changing the removed operator<= to the following
also seem to fix all tests.

  static bool operator<=(std::set<std::pair<state, bool>> const& f,
                         state_set const& set)
  {
    auto first1 = set.begin(), last1 = set.end();
    auto first2 = f.begin(), last2 = f.end();
    for (; first2 != last2; ++first1)
      if (first1 == last1 || first2->first < *first1)
        {
          return false;
        }
      else if (first2->first == *first1)
        {
          ++first2;
          // Some states of f may appear twice because of the attached
          // Boolean.
          if (first2 != last2 && first2->first == *first1)
            ++first2;
        }
    return true;
  }

* spot/twaalgos/forq_contains.cc: Remove relevance-based optimization.
---
 spot/twaalgos/forq_contains.cc | 59 ++--------------------------------
 1 file changed, 2 insertions(+), 57 deletions(-)

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<std::pair<state, bool>> const& other);
-      bool relevance_test(state_set const& set) const;
 
       template<typename Callable>
       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<std::pair<state, bool>> const& f,
-    std::set<std::pair<state, bool>> const& s)
+  static bool operator<=(std::set<std::pair<state, bool>> const& f,
+                         std::set<std::pair<state, bool>> const& s)
   {
     return std::includes(s.begin(), s.end(), f.begin(), f.end());
   }
 
-  static bool operator<=(
-    std::set<std::pair<state, bool>> 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<std::pair<state, bool>> 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)