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

FM: use a vector to store the Next BDD->formula map.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-13 16:21:27 +02:00
parent 191fa370e2
commit 8c454f9ddf
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -168,7 +168,7 @@ namespace spot
mark_tools mt; mark_tools mt;
typedef bdd_dict::fv_map fv_map; typedef bdd_dict::fv_map fv_map;
typedef bdd_dict::vf_map vf_map; typedef std::vector<const formula*> vf_map;
fv_map next_map; ///< Maps "Next" variables to BDD variables fv_map next_map; ///< Maps "Next" variables to BDD variables
vf_map next_formula_map; ///< Maps BDD variables to "Next" variables vf_map next_formula_map; ///< Maps BDD variables to "Next" variables
@ -256,6 +256,7 @@ namespace spot
f = f->clone(); f = f->clone();
num = dict->register_anonymous_variables(1, this); num = dict->register_anonymous_variables(1, this);
next_map[f] = num; next_map[f] = num;
next_formula_map.resize(bdd_varnum());
next_formula_map[num] = f; next_formula_map[num] = f;
} }
next_set &= bdd_ithvar(num); next_set &= bdd_ithvar(num);
@ -280,13 +281,16 @@ namespace spot
const formula* const formula*
var_to_formula(int var) const var_to_formula(int var) const
{ {
vf_map::const_iterator isi = next_formula_map.find(var);
if (isi != next_formula_map.end())
return isi->second->clone();
const bdd_dict::bdd_info& i = dict->bdd_map[var]; const bdd_dict::bdd_info& i = dict->bdd_map[var];
if (i.type != bdd_dict::anon)
{
assert(i.type == bdd_dict::acc || i.type == bdd_dict::var); assert(i.type == bdd_dict::acc || i.type == bdd_dict::var);
return i.f->clone(); return i.f->clone();
} }
const formula* f = next_formula_map[var];
assert(f);
return f->clone();
}
bdd bdd
boolean_to_bdd(const formula* f) boolean_to_bdd(const formula* f)