From 2e6297c26afb116ffce4493978a9b2809b20961d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Nov 2016 07:29:59 +0100 Subject: [PATCH] ltl2tgba_fm: simplify three bdd operations * spot/twaalgos/ltl2tgba_fm.cc: Replace bdd_exists(a & b, c) by bdd_appex(a, b, bddop_and, c). --- spot/twaalgos/ltl2tgba_fm.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 5e779db1e..db276cf98 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -956,8 +956,8 @@ namespace spot all_props -= label; formula dest = - dict_.bdd_to_sere(bdd_exist(res & label, dict_.var_set)); - + 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; @@ -1421,7 +1421,7 @@ namespace spot all_props -= label; formula dest = - dict_.bdd_to_sere(bdd_exist(f1 & label, + dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, dict_.var_set)); formula dest2 = formula::binop(o, dest, node[1]); @@ -1505,7 +1505,8 @@ namespace spot all_props -= label; formula dest = - dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); + dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, + dict_.var_set)); formula dest2 = formula::binop(o, dest, node[1]);