From 583ca38d91c92fc5201ddaf3b26d46cc41f42736 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 11 Oct 2022 10:43:27 +0200
Subject: [PATCH] replace bdd_relprod by bdd_restrict

* spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/toweak.cc: Here.
---
 spot/twaalgos/alternation.cc | 4 ++--
 spot/twaalgos/dualize.cc     | 2 +-
 spot/twaalgos/simulation.cc  | 4 ++--
 spot/twaalgos/toweak.cc      | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc
index 8370f395b..bdbe07982 100644
--- a/spot/twaalgos/alternation.cc
+++ b/spot/twaalgos/alternation.cc
@@ -457,7 +457,7 @@ namespace spot
             // First loop over all possible valuations atomic properties.
             for (bdd oneletter: minterms_of(all_letters, ap))
               {
-                minato_isop isop(bdd_relprod(bs, oneletter, ap));
+                minato_isop isop(bdd_restrict(bs, oneletter));
                 bdd dest;
                 while ((dest = isop.next()) != bddfalse)
                   {
@@ -636,7 +636,7 @@ namespace spot
               cond_ = oneletter;
               all_letters_ -= oneletter;
               // Get a sum of possible transitions matching this letter.
-              isop_ = minato_isop(bdd_relprod(transitions_, oneletter, ap_));
+              isop_ = minato_isop(bdd_restrict(transitions_, oneletter));
               dest_ = isop_.next();
             }
           std::set<unsigned> dest = bdd_to_state(dest_);
diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc
index 91498ce8d..1b60a0d17 100644
--- a/spot/twaalgos/dualize.cc
+++ b/spot/twaalgos/dualize.cc
@@ -155,7 +155,7 @@ namespace spot
 
             for (bdd oneletter: minterms_of(letters, ap))
               {
-                minato_isop isop(bdd_relprod(delta, oneletter, ap));
+                minato_isop isop(bdd_restrict(delta, oneletter));
                 bdd dest;
 
                 while ((dest = isop.next()) != bddfalse)
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index 58ebfd79d..ca8928888 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -590,7 +590,7 @@ namespace spot
                 // C1 then (!C1)C2, instead of C1 then C2.
                 // With minatop_isop, we ensure that the no negative
                 // class variable will be seen (likewise for promises).
-                minato_isop isop(bdd_relprod(sig, one, sup_all_atomic_prop));
+                minato_isop isop(bdd_restrict(sig, one));
 
                 ++nb_minterms;
 
diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc
index 543c7c9a1..ae7a0f58a 100644
--- a/spot/twaalgos/toweak.cc
+++ b/spot/twaalgos/toweak.cc
@@ -179,7 +179,7 @@ namespace spot
 
               for (bdd oneletter: minterms_of(letters, ap))
                 {
-                  minato_isop isop(bdd_relprod(delta, oneletter, ap));
+                  minato_isop isop(bdd_restrict(delta, oneletter));
                   bdd dest;
 
                   while ((dest = isop.next()) != bddfalse)