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

bdddict: remove register_clone_acc

Browse source 
* src/twa/bdddict.cc, src/twa/bdddict.hh: Here.
This commit is contained in:
Alexandre Duret-Lutz 2015-08-14 15:16:26 +02:00
parent c50d5a82ac
commit 304f2496ea
2 changed files with 0 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/twa/bdddict.cc
View file

@ -189,24 +189,6 @@ namespace spot
register_acceptance_variables(bdd_low(f), for_me);
}
int
bdd_dict::register_clone_acc(int v, const void* for_me)
{
assert(unsigned(v) < bdd_map.size());
bdd_info& i = bdd_map[v];
assert(i.type == acc);
std::ostringstream s;
// FIXME: We could be smarter and reuse unused "$n" numbers.
ltl::print_psl(s, i.f) << '$' << ++i.clone_counts;
const ltl::formula* f =
ltl::atomic_prop::instance(s.str(),
ltl::default_environment::instance());
int res = register_acceptance_variable(f, for_me);
f->destroy();
return res;
}
const ltl::formula*
bdd_dict::oneacc_to_formula(int var) const
{

15
src/twa/bdddict.hh
View file

@ -163,21 +163,6 @@ namespace spot
}
/// @}
/// \brief Clone an acceptance variable VAR for FOR_ME.
///
/// This is used in products TGBAs when both operands share the
/// same acceptance variables but they need to be distinguished in
/// the result.
/// @{
int register_clone_acc(int var, const void* for_me);
template <typename T>
int register_clone_acc(int var, std::shared_ptr<T> for_me)
{
return register_clone_acc(var, for_me.get());
}
/// @}
/// \brief Register BDD variables as acceptance variables.
///
/// Register all variables occurring in \a f as acceptance variables