translate: add a new relabel-overlap option

Fixes issue #536.  Also a part of issue #500.

* spot/twaalgos/translate.hh, spot/twaalgos/translate.cc: Implement
this new option.
* bin/spot-x.cc, NEWS: Mention it.
* tests/core/ltl2tgba2.test: Add the test case from issue #536.

NEWS

@@ -37,6 +37,29 @@ New in spot 2.11.6.dev  (not yet released)
     replace boolean subformulas by fresh atomic propositions even if
     those subformulas share atomic propositions.
 
+  - spot::translate() has a new -x option "relabel-overlap=M" that
+    augments the existing "relabel-bool=N".  By default, N=4, M=8.
+    When the formula to translate has more than N atomic propositions,
+    relabel_bse() is first called to attempt to rename non-overlaping
+    boolean subexpressions (i.e., no shared atomic proposition) in
+    order to reduce the number of atomic proposition, a source of
+    explonential explosion in several places of the translation
+    pipeline.  This relabel-bool optimization exists since Spot 2.4.
+    The new feature is that if, after relabel-bool, the formula still
+    has more than M atomic propositions, then spot::translate() now
+    attempts to relabel boolean subexpressions even if they have
+    overlapping atomic propositions, in an attempt to reduce the
+    number of atomic proposition even more.  Doing so has the slightly
+    unfortunate side effect of hindering some simplifications (because
+    the new atomic propositions hide their interactions), but it
+    usually incures a large speedup.  (See Issue #500, Issue #536.)
+
+    For instance on Alexandre's laptop, running
+      'ltlsynt --tlsf SPIReadManag.tlsf --aiger'
+    with Spot 2.11.6 used to produce an AIG circuit with 48 nodes in
+    36 seconds; it now produce an AIG circuit with 53 nodes in only
+    0.1 second.
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:

bin/spot-x.cc

@@ -196,7 +196,16 @@ disabled, it is just an upper bound otherwise.") },
 with N atomic propositions or more will have its Boolean subformulas \
 abstracted as atomic propositions during the translation to automaton. \
 This relabeling can speeds the translation if a few Boolean subformulas \
-use a large number of atomic propositions.  By default N=4.  Setting \
+use a large number of atomic propositions.  This relabeling make sure \
+the subexpression that are replaced do not share atomic propositions.  \
+By default N=4.  Setting this value to 0 will disable the rewriting.") },
+    { DOC("relabel-overlap", "If set to a positive integer N, a formula \
+with N atomic propositions or more will have its Boolean subformulas \
+abstracted as atomic propositions during the translation to automaton. \
+This version does not care about overlapping atomic propositions, so \
+it can cause the created temporary automata to have incompatible \
+combinations of atomic propositions that will be eventually be removed. \
+This relabeling is attempted after relabel-bool.  By default N=8.  Setting \
 this value to 0 will disable the rewriting.") },
     { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization, to 1 to \
 always try it, or 2 to attempt it only on syntactic obligations or on automata \

spot/twaalgos/translate.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018, 2020-2022 Laboratoire de Recherche et
+// Copyright (C) 2013-2018, 2020-2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -38,6 +38,7 @@ namespace spot
   {
     comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
     relabel_bool_ = 4;
+    relabel_overlap_ = 8;
     tls_impl_ = -1;
     ltl_split_ = true;
     exprop_ = -1;
@@ -47,6 +48,7 @@ namespace spot
       return;
 
     relabel_bool_ = opt->get("relabel-bool", 4);
+    relabel_overlap_ = opt->get("relabel-overlap", 6);
     comp_susp_ = opt->get("comp-susp", 0);
     if (comp_susp_ == 1)
       {
@@ -480,15 +482,23 @@ namespace spot
     //  2) has some Boolean subformula
     //  3) relabel_bse() actually reduces the number of atomic
     //     propositions.
+    //
+    // If the formula still has more than relabel_overlap_ APs after
+    // the above, we try the more aggressive relabel_overlapping_bse()
+    // function.  However after applying this function, we might have
+    // false edges.
     relabeling_map m;
     formula to_work_on = *f;
-    if (relabel_bool_ > 0)
+    if (relabel_bool_ > 0 || relabel_overlap_ > 0)
       {
         std::set<formula> aps;
         atomic_prop_collect(to_work_on, &aps);
         unsigned atomic_props = aps.size();
 
-        if (atomic_props >= (unsigned) relabel_bool_)
+        if ((relabel_bool_
+             && atomic_props >= (unsigned) relabel_bool_)
+            || (relabel_overlap_
+                && atomic_props >= (unsigned) relabel_overlap_))
           {
             // Make a very quick simplification path before for
             // Boolean subformulas, only only syntactic rules.  This
@@ -507,14 +517,15 @@ namespace spot
             options.nenoform_stop_on_boolean = true;
             options.boolean_to_isop = false;
             tl_simplifier simpl(options, simpl_->get_dict());
-            to_work_on = simpl.simplify(to_work_on);
+            formula simplified = to_work_on = simpl.simplify(to_work_on);
 
             // Do we have Boolean subformulas that are not atomic
             // propositions?
             bool has_boolean_sub = false;
             to_work_on.traverse([&](const formula& f)
                                 {
-                                  if (f.is_boolean())
+                                  if (f.is_boolean()
+                                      && !f.is(op::ap, op::Not))
                                     {
                                       has_boolean_sub = true;
                                       return true;
@@ -524,11 +535,34 @@ namespace spot
 
             if (has_boolean_sub)
               {
-                formula relabeled = relabel_bse(to_work_on, Pnn, &m);
+                if (relabel_bool_
-                if (m.size() < atomic_props)
+                    && atomic_props >= (unsigned) relabel_bool_)
-                  to_work_on = relabeled;
+                  {
-                else
+                    formula relabeled = relabel_bse(to_work_on, Pnn, &m);
-                  m.clear();
+                    if (m.size() < atomic_props)
+                      {
+                        atomic_props = m.size();
+                        to_work_on = relabeled;
+                      }
+                    else
+                      {
+                        m.clear();
+                      }
+                  }
+                if (relabel_overlap_
+                    && atomic_props >= (unsigned) relabel_overlap_)
+                  {
+                    relabeling_map m2;
+                    formula relabeled =
+                      relabel_overlapping_bse(simplified, Pnn, &m2);
+                    if (m2.size() < atomic_props)
+                      {
+                        atomic_props = m2.size();
+                        to_work_on = relabeled;
+                        std::swap(m, m2);
+                      }
+                    m2.clear();
+                  }
               }
           }
       }

spot/twaalgos/translate.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018, 2020, 2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018, 2020, 2022, 2023 Laboratoire de Recherche
-// de l'Epita (LRDE).
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -150,6 +150,7 @@ namespace spot
     int skel_wdba_;
     int skel_simul_;
     int relabel_bool_;
+    int relabel_overlap_;
     int tls_impl_;
     bool gf_guarantee_ = true;
     bool gf_guarantee_set_ = false;

tests/core/ltl2tgba2.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009-2023 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
@@ -516,3 +516,14 @@ f='G((a -> X((!a U b) | G!a)) & (a -> X(G!a | (!a U c))) & (a -> X(G!a
 (a -> X(G!a | (!a U g))) & (a -> X(G!a | (!a U h)))) & (GFa <-> (GFb &
 GFc & GFd & GFe & GFf & GFg & GFh))'
 test 128 = `ltl2tgba -G -D "$f" --stats=%s`
+
+# This used to die from out of memory after 5 minutes.  See issue #536.
+f='(TRUE & (G F ~v21)& (( G  F v39 ->  G  F v23))) -> (TRUE &
+(G F (v1 -> (v41 & v29)))& (G F (v3 -> (v42 & v29)))& (G F (v5
+-> (v43 & v29)))& (G F (v7 -> (v44 & v29)))& (G F (v9 -> (v45 &
+v29)))& (G F (v11 -> (v46 & v29)))& (G F (v13 -> (v47 & v29)))&
+(G F (v15 -> (v48 & v29)))& (G F (v17 -> (v49 & v29)))& (G F (v19
+-> (v50 & v29)))& (G F (v41 | (v1 | (v3 | (v5 | (v7 | (v9 |
+(v11 | (v13 | (v15 | (v17 | v19))))))))))))'
+ltl2tgba -p'min even' -D -C "$f" --stats='%s %e'>out
+test '22 288' = "`cat out`"