use bdd_restrict more

Doing so reduced the number of GC passes tested in bdd.test, which is
good.

* spot/twaalgos/ltl2tgba_fm.cc: Simplify minato loops with
bdd_restrict.
* spot/twaalgos/synthesis.cc (split_2step): Use bdd_restrict instead
of bdd_appex.
* tests/core/bdd.test, tests/core/ltlf.test: Adjust test cases.

spot/twaalgos/ltl2tgba_fm.cc

@@ -900,8 +900,7 @@ namespace spot
               for (bdd label: minterms_of(all_props, var_set))
                 {
                   formula dest =
-                    dict_.bdd_to_sere(bdd_appex(res_ndet, label, bddop_and,
+                    dict_.bdd_to_sere(bdd_restrict(res_ndet, label));
-                                                dict_.var_set));
                   dest = formula::first_match(dest);
                   if (to_concat_)
                     dest = formula::Concat({dest, to_concat_});
@@ -995,9 +994,7 @@ namespace spot
           bdd all_props = bdd_existcomp(res, dict_.var_set);
           for (bdd label: minterms_of(all_props, var_set))
             {
-              formula dest =
+              formula dest = dict_.bdd_to_sere(bdd_restrict(res, label));
-                dict_.bdd_to_sere(bdd_appex(res, label, bddop_and,
-                                            dict_.var_set));
               f2a_t::const_iterator i = f2a_.find(dest);
               if (i != f2a_.end() && i->second.first == nullptr)
                 continue;
@@ -1471,9 +1468,7 @@ namespace spot
                   for (bdd label: minterms_of(all_props, var_set))
                     {
                       formula dest =
-                        dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and,
+                        dict_.bdd_to_sere(bdd_restrict(f1, label));
-                                                    dict_.var_set));
-
                       formula dest2 = formula::binop(o, dest, node[1]);
                       bool unamb = dict_.unambiguous;
                       if (!dest2.is_ff())
@@ -1552,9 +1547,7 @@ namespace spot
                   for (bdd label: minterms_of(all_props, var_set))
                     {
                       formula dest =
-                        dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and,
+                        dict_.bdd_to_sere(bdd_restrict(f1, label));
-                                                    dict_.var_set));
-
                       formula dest2 = formula::binop(o, dest, node[1]);
 
                       bdd udest =
@@ -1787,16 +1780,15 @@ namespace spot
                 var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set);
                 all_props = bdd_existcomp(t.symbolic, d_.var_set);
               }
-            for (bdd one_prop_set: minterms_of(all_props, var_set))
+            for (bdd label: minterms_of(all_props, var_set))
               {
-                minato_isop isop(t.symbolic & one_prop_set);
+                minato_isop isop(t.symbolic & label);
                 bdd cube;
                 while ((cube = isop.next()) != bddfalse)
                   {
                     bdd label = bdd_exist(cube, d_.next_set);
                     bdd dest_bdd = bdd_existcomp(cube, d_.next_set);
-                    formula dest =
+                    formula dest = d_.conj_bdd_to_formula(dest_bdd);
-                      d_.conj_bdd_to_formula(dest_bdd);
 
                     // Handle a Miyano-Hayashi style unrolling for
                     // rational operators.  Marked nodes correspond to
@@ -1818,8 +1810,7 @@ namespace spot
                         dest = d_.mt.mark_concat_ops(dest);
                       }
                     // Note that simplify_mark may have changed dest.
-                    dest_bdd = bdd_ithvar(d_.register_next_variable(dest));
+                    res |= label & bdd_ithvar(d_.register_next_variable(dest));
-                    res |= label & dest_bdd;
                   }
               }
             t.symbolic = res;
@@ -2120,16 +2111,15 @@ namespace spot
             //
             // FIXME: minato_isop is quite expensive, and I (=adl)
             // don't think we really care that much about getting the
-            // smalled sum of products that minato_isop strives to
+            // smallest sum of products that minato_isop strives to
             // compute.  Given that Next and Acc variables should
             // always be positive, maybe there is a faster way to
             // compute the successors?  E.g. using bdd_satone() and
             // ignoring negated Next and Acc variables.
-            minato_isop isop(res & one_prop_set);
+            minato_isop isop(bdd_restrict(res, one_prop_set));
             bdd cube;
             while ((cube = isop.next()) != bddfalse)
               {
-                bdd label = bdd_exist(cube, d.next_set);
                 bdd dest_bdd = bdd_existcomp(cube, d.next_set);
                 formula dest = d.conj_bdd_to_formula(dest_bdd);
 
@@ -2147,8 +2137,9 @@ namespace spot
                 if (symb_merge)
                   dest = fc.canonicalize(dest);
 
-                bdd conds = bdd_existcomp(label, d.var_set);
+                bdd conds =
-                bdd promises = bdd_existcomp(label, d.a_set);
+                  exprop ? one_prop_set : bdd_existcomp(cube, d.var_set);
+                bdd promises = bdd_existcomp(cube, d.a_set);
                 dests.emplace_back(transition(dest, conds, promises));
               }
           }

spot/twaalgos/synthesis.cc

@@ -574,9 +574,7 @@ namespace spot
               // implies is faster than and
               if (bdd_implies(one_letter, e_info.einsup.first))
                 {
-                  e_info.econdout =
+                  e_info.econdout = bdd_restrict(e_info.econd, one_letter);
-                      bdd_appex(e_info.econd, one_letter,
-                                bddop_and, input_bdd);
                   dests.push_back(&e_info);
                   assert(e_info.econdout != bddfalse);
                 }

tests/core/bdd.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de
+# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et
-# l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -23,7 +23,7 @@ set -e
 
 # Make sure that setting the SPOT_BDD_TRACE envvar actually does
 # something.
-genltl --kr-nlogn=2 |
+genltl --kr-n=3 |
     SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err
 cat err
 grep spot: out && exit 1
@@ -31,14 +31,14 @@ grep 'spot: BDD package initialized' err
 # This value below, which is the number of time we need to garbage
 # collect might change if we improve the tool or change the way BuDDy
 # is initialized.
-test 11 = `grep -c 'spot: BDD GC' err`
+test 2 = `grep -c 'spot: BDD GC' err`
 # Minimal size for this automaton.
 # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf
-test "147,207" = `autfilt --stats=%s,%e out`
+test "2240,4214" = `autfilt --stats=%s,%e out`
 
 # With the default value of tls-max-states, no GC is needed
-genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err
+genltl --kr-n=3 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err
 cat err
 grep 'spot: BDD package initialized' err
 test 0 = `grep -c 'spot: BDD GC' err`
-test "147,207" = `cat out`
+test "2240,4214" = `cat out`

tests/core/ltlf.test

@@ -57,7 +57,7 @@ State: 3
 HOA: v1
 name: "a & X(A & a) & (A U G!A)"
 States: 4
-Start: 2
+Start: 3
 AP: 2 "A" "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
@@ -70,9 +70,9 @@ State: 1
 [!0] 0
 [0] 1
 State: 2
-[0&1] 3
-State: 3
 [0&1] 1
+State: 3
+[0&1] 2
 --END--
 HOA: v1
 name: "(a U (A & b)) & (A U G!A) & F((A & c) | (A & d & X!A))"
@@ -124,7 +124,7 @@ State: 2 {0}
 --END--
 HOA: v1
 States: 3
-Start: 1
+Start: 2
 AP: 1 "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
@@ -133,9 +133,9 @@ properties: trans-labels explicit-labels state-acc deterministic
 State: 0 {0}
 [t] 0
 State: 1
-[0] 2
-State: 2
 [0] 0
+State: 2
+[0] 1
 --END--
 HOA: v1
 States: 5