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

Reuse Boolean->BDD translations performed during simplification.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
Use boolean_to_bdd()
This commit is contained in:
Alexandre Duret-Lutz 2011-11-11 15:53:05 +01:00
parent f590ca4e96
commit b67852a5ff
1 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1542,9 +1542,21 @@ namespace spot
if (i != m->end())
return i->second;
ltl_trad_visitor v(*this, mark_all, exprop);
f->accept(v);
translated t = { v.result(), v.has_rational(), v.has_marked() };
translated t;
if (f->is_boolean())
{
t.symbolic = boolean_to_bdd(f);
t.has_rational = false;
t.has_marked = false;
}
else
{
ltl_trad_visitor v(*this, mark_all, exprop);
f->accept(v);
t.symbolic = v.result();
t.has_rational = v.has_rational();
t.has_marked = v.has_marked();
}
return m->insert(std::make_pair(f->clone(), t)).first->second;
}