formula: new trivial simplifications

Add the following rules:
  - f|[+] = [+] if f rejects [*0]
  - f|[*] = [*] if f accepts [*0]
  - f&&[+] = f if f rejects [*0]
  - b:b[*i..j] = b[*max(i,1)..j]
  - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1,1), j+l-1]

* spot/tl/formula.cc: Implement the new rules.
* doc/tl/tl.tex: Document them.
* tests/core/equals.test: Test them.
* NEWS: Add them

NEWS

@@ -1,5 +1,14 @@
 New in spot 2.11.2.dev  (not yet released)
 
+  Library:
+
+  - The following new trivial simplifications have been implemented for SEREs:
+    - f|[+] = [+] if f rejects [*0]
+    - f|[*] = [*] if f accepts [*0]
+    - f&&[+] = f if f rejects [*0]
+    - b:b[*i..j] = b[*max(i,1)..j]
+    - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1,1), j+l-1]
+
   Bug fixes:
 
   - Automata-based implication checks, used to simplify formulas were

doc/tl/tl.tex

@@ -853,10 +853,18 @@ The following rules are all valid with the two arguments swapped.
   \1\OR b &\equiv \1 &
   \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
   &&
-  \STAR{} \AND f &\equiv f &
+  \STAR{} \ANDALT f &\equiv f &
-  \STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
+  \STAR{} \OR f &\equiv \mathrlap{\STAR{}} &
   &&
-  \STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
+  \STAR{} \CONCAT f &\equiv \STAR{}\text{~if~}\varepsilon\VDash f& \\
+  &&
+  \PLUS{} \ANDALT f &\equiv f \text{~if~}\varepsilon\nVDash f&
+  \PLUS{} \OR f &\equiv \begin{cases}
+    \mathrlap{\STAR{}\text{~if~} \varepsilon\VDash f} \\
+    \mathrlap{\PLUS{}\text{~if~} \varepsilon\nVDash f} \\
+  \end{cases} &
+  &&
+  && \\
   \eword\AND f &\equiv f &
   \eword\ANDALT f &\equiv
   \begin{cases}
@@ -880,7 +888,9 @@ The following rules are all valid with the two arguments swapped.
 f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}} &
 f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
 f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f&\equiv f\FSTAR{\mvar{i+1}..\mvar{j+1}} &
-f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}}
+f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}}\\
+b\STAR{\mvar{i}..\mvar{j}}\FUSION b &\equiv b\STAR{\mvar{\max(i,1)}..\mvar{j}} &
+b\STAR{\mvar{i}..\mvar{j}}\FUSION b\STAR{\mvar{k}..\mvar{l}} &\equiv b\mathrlap{\STAR{\mvar{\max(i,1)+\max(k,1)-1}..\mvar{j+l-1}}}
 \end{align*}
 \section{SERE-LTL Binding Operators}
 

spot/tl/formula.cc

@@ -307,11 +307,14 @@ namespace spot
 
     unsigned orig_size = v.size();
 
-    const fnode* neutral;
+    const fnode* neutral;       // neutral element
-    const fnode* neutral2;
+    const fnode* neutral2;      // second neutral element (if any)
-    const fnode* abs;
+    const fnode* abs;           // absorbent element
-    const fnode* abs2;
+    const fnode* abs2;          // second absorbent element (if any)
-    const fnode* weak_abs;
+    const fnode* weak_abs;      // almost absorbent element (if any)
+    // The notion of "almost absorbent" captures situation where the
+    // present of the element can be simplified in itself or another
+    // element depending on a condition on the rest of the formula.
     switch (o)
       {
       case op::And:
@@ -323,7 +326,17 @@ namespace spot
         break;
       case op::AndRat:
         neutral = one_star();
-        neutral2 = nullptr;
+        {
+          // If this AndRat contains an operand that does not accept
+          // the empty word, and that is not [+], then any [+] can be
+          // removed.
+          bool one_non_eword_non_plus =
+          std::find_if(v.begin(), v.end(),
+                       [o = one_plus()](const fnode* f) {
+                         return !f->accepts_eword() && f != o;
+                       }) != v.end();
+          neutral2 = one_non_eword_non_plus ? one_plus() : nullptr;
+        }
         abs = ff();
         abs2 = nullptr;
         weak_abs = eword();
@@ -349,7 +362,7 @@ namespace spot
         neutral2 = nullptr;
         abs = one_star();
         abs2 = nullptr;
-        weak_abs = nullptr;
+        weak_abs = one_plus();
         gather_bool(v, op::Or);
         break;
       case op::Concat:
@@ -506,11 +519,10 @@ namespace spot
               else
                 return abs;
             }
-          else
+          else if (o == op::AndNLM)
             {
               // Similarly,  a* & 1 & (c;d) = c;d
               //             a* & 1 & c* = 1
-              assert(o == op::AndNLM);
               vec tmp;
               for (auto i: v)
                 {
@@ -527,6 +539,27 @@ namespace spot
                 tmp.emplace_back(weak_abs);
               v.swap(tmp);
             }
+          else if (o == op::OrRat)
+            {
+              // We have    a[*] | [+] | c = [*]
+              //     and    a | [+] | c = [+]
+              // So if [+] has been seen, check if some term
+              // recognize the empty word.
+              bool acc_eword = false;
+              for (i = v.begin(); i != v.end(); ++i)
+                {
+                  acc_eword |= (*i)->accepts_eword();
+                  (*i)->destroy();
+                }
+              if (acc_eword)
+                return abs;
+              else
+                return weak_abs;
+            }
+          else
+            {
+              SPOT_UNREACHABLE();
+            }
         }
       else if (o == op::Concat || o == op::Fusion)
         {
@@ -613,6 +646,81 @@ namespace spot
                   *fpos = newfs;
                 }
             }
+          // also
+          //   b[*i..j]:b -> b[*max(1,i),j]
+          //   b:b[*i..j] -> b[*max(1,i),j]
+          //   b[*i..j]:b[*k..l] -> b[*max(i,1)+max(j,1)-1,j+l-1]
+          if (o == op::Fusion && v.size() > 1)
+            {
+              i = v.begin();
+              while (i != v.end())
+                {
+                  if (!(((*i)->is(op::Star) && (*i)->nth(0)->is_boolean())
+                        || (*i)->is_boolean()))
+                    {
+                      ++i;
+                      continue;
+                    }
+                  const fnode *b;
+                  unsigned min;
+                  unsigned max;
+                  if ((*i)->is_boolean())
+                    {
+                      min = max = 1;
+                      b = *i;
+                    }
+                  else
+                    {
+                      b = (*i)->nth(0);
+                      min = (*i)->min();
+                      max = (*i)->max();
+                    }
+                  vec::iterator prev = i;
+                  ++i;
+                  bool changed = false;
+                  while (i != v.end())
+                    {
+                      unsigned min2;
+                      unsigned max2;
+                      if ((*i)->is_boolean())
+                        {
+                          if (*i != b)
+                            break;
+                          min2 = max2 = 1;
+                        }
+                      else if ((*i)->is(op::Star) && (*i)->nth(0)->is_boolean())
+                        {
+                          if ((*i)->nth(0) != b)
+                            break;
+                          min2 = (*i)->min();
+                          max2 = (*i)->max();
+                        }
+                      else
+                        {
+                          break;
+                        }
+                      // Now we can merge prev and i.
+                      min = min + (min == 0) + min2 + (min2 == 0) - 1;
+                      assert(max != 0 && max2 != 0);
+                      if (max2 == unbounded() || max == unbounded())
+                        max = unbounded();
+                      else if (max + max2 < unbounded())
+                        max = max + max2 - 1;
+                      else
+                        break;
+                      changed = true;
+                      (*i)->destroy();
+                      i = v.erase(i);
+                    }
+                  if (changed)
+                    {
+                      const fnode* newf =
+                        fnode::bunop(op::Star, b->clone(), min, max);
+                      (*prev)->destroy();
+                      *prev = newf;
+                    }
+                }
+            }
         }
     }
 

tests/core/equals.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2012, 2014-2015, 2021 Laboratoire de Recherche et
+# Copyright (C) 2009-2012, 2014-2015, 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -196,6 +196,12 @@ G({1}<>->1), 1
 {(a*;b|c)[:*0]}, 1
 {(a*;b|c)[:*1]}, {(a*;b|c)}
 {(a;b):(a;b):(a;b)[:*2]:(a;b):b*:b*:(c;d)[:*1]}, {(a;b)[:*5]:b*[:*2]:(c;d)}
+{((a;b)|[+]|(c;d[*]));a}, {[+];a}
+{((a;b)|[+]|(d[*]));a}, {[*];a}
+{((a;b)&&[+]&&(d[*]));a}, {((a;b)&&(d[*]));a}
+{((a;b|[*0])&&[+]&&(d[*]));a}, {((a;b|[*0])&&[+]&&(d[*]));a}
+{(a;c):b[*3..5]:b[*10]:(a;c)}, {(a;c):b[*12..14]:(a;c)}
+{(a;c):b:b[*3..5]:b:b[*0..4]:(a;c)}, {(a;c):b[*3..8]:(a;c)}
 EOF