alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl2tgba_fm: simplify three bdd operations

Browse source 
* spot/twaalgos/ltl2tgba_fm.cc: Replace bdd_exists(a & b, c) by
bdd_appex(a, b, bddop_and, c).
This commit is contained in:
Alexandre Duret-Lutz 2016-11-09 07:29:59 +01:00
parent 84b16aa6bd
commit 2e6297c26a
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -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]);