acc: introduce inf_unit()

* spot/twa/acc.cc, spot/twa/acc.hh: Here.
* tests/python/setacc.py: Test it.

spot/twa/acc.cc

@@ -2825,6 +2825,37 @@ namespace spot
     return res;
   }
 
+  acc_cond::mark_t acc_cond::acc_code::inf_unit() const
+  {
+    mark_t res = {};
+    if (empty() || is_f())
+      return res;
+    const acc_cond::acc_word* pos = &back();
+    do
+      {
+        switch (pos->sub.op)
+          {
+          case acc_cond::acc_op::And:
+            --pos;
+            break;
+          case acc_cond::acc_op::Or:
+            pos -= pos->sub.size + 1;
+            break;
+          case acc_cond::acc_op::Fin:
+          case acc_cond::acc_op::InfNeg:
+          case acc_cond::acc_op::FinNeg:
+            pos -= 2;
+            break;
+          case acc_cond::acc_op::Inf:
+            res |= pos[-1].mark;
+            pos -= 2;
+            break;
+          }
+      }
+    while (pos >= &front());
+    return res;
+  }
+
   acc_cond::mark_t acc_cond::acc_code::used_once_sets() const
   {
     mark_t seen = {};

spot/twa/acc.hh

@@ -1257,6 +1257,19 @@ namespace spot
       /// Return -1 if no such set exist.
       int fin_one() const;
 
+      /// \brief Find a `Inf(i)` that is a unit clause.
+      ///
+      /// This return a mark_t `{i}` such that `Inf(i)` appears as a
+      /// unit clause in the acceptance condition.  I.e., either the
+      /// condition is exactly `Inf(i)`, or the condition has the form
+      /// `...&Inf(i)&...`.  If there is no such `Inf(i)`, an empty
+      /// mark_t is returned.
+      ///
+      /// If multiple unit-Inf appear as unit-clauses, the set of
+      /// those will be returned.  For instance applied to
+      /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
+      mark_t inf_unit() const;
+
       /// \brief Help closing accepting or rejecting cycle.
       ///
       /// Assuming you have a partial cycle visiting all acceptance
@@ -2153,6 +2166,22 @@ namespace spot
       return code_.fin_one();
     }
 
+    /// \brief Find a `Inf(i)` that is a unit clause.
+    ///
+    /// This return a mark_t `{i}` such that `Inf(i)` appears as a
+    /// unit clause in the acceptance condition.  I.e., either the
+    /// condition is exactly `Inf(i)`, or the condition has the form
+    /// `...&Inf(i)&...`.  If there is no such `Inf(i)`, an empty
+    /// mark_t is returned.
+    ///
+    /// If multiple unit-Inf appear as unit-clauses, the set of
+    /// those will be returned.  For instance applied to
+    /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
+    mark_t inf_unit() const
+    {
+      return code_.inf_unit();
+    }
+
     /// \brief Return the top-level disjuncts.
     ///
     /// For instance, if the formula is

tests/python/setacc.py

@@ -106,3 +106,20 @@ assert acc == spot.acc_cond('Inf(0)')
 acc = spot.translate('b').get_acceptance()
 collect()
 assert acc == spot.acc_code('Inf(0)')
+
+
+c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))')
+m1 = c.fin_unit()
+m2 = c.inf_unit()
+assert m1 == [0,1]
+assert m2 == []
+c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))')
+m1 = c.fin_unit()
+m2 = c.inf_unit()
+assert m1 == []
+assert m2 == [0,1]
+c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))')
+m1 = c.fin_unit()
+m2 = c.inf_unit()
+assert m1 == []
+assert m2 == []