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

bdddict: remove dead code

Browse source 
* src/twa/bdddict.cc,
src/twa/bdddict.hh (unregister_all_typed_variables, oneacc_to_formula,
register_acceptance_variables): Remove these unused methods.
This commit is contained in:
Alexandre Duret-Lutz 2015-10-02 17:05:17 +02:00
parent 2fa9c27534
commit 24ef5a0b7f
2 changed files with 0 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/twa/bdddict.cc
View file

@ -155,43 +155,6 @@ namespace spot
return num;
}
void
bdd_dict::register_acceptance_variables(bdd f, const void* for_me)
{
if (f == bddtrue || f == bddfalse)
return;
int v = bdd_var(f);
assert(unsigned(v) < bdd_map.size());
bdd_info& i = bdd_map[v];
assert(i.type == acc);
i.refs.insert(for_me);
register_acceptance_variables(bdd_high(f), for_me);
register_acceptance_variables(bdd_low(f), for_me);
}
formula
bdd_dict::oneacc_to_formula(int var) const
{
assert(unsigned(var) < bdd_map.size());
const bdd_info& i = bdd_map[var];
assert(i.type == acc);
return i.f;
}
formula
bdd_dict::oneacc_to_formula(bdd oneacc) const
{
assert(oneacc != bddfalse);
while (bdd_high(oneacc) == bddfalse)
{
oneacc = bdd_low(oneacc);
assert(oneacc != bddfalse);
}
return oneacc_to_formula(bdd_var(oneacc));
}
int
bdd_dict::register_anonymous_variables(int n, const void* for_me)
{
@ -313,17 +276,6 @@ namespace spot
priv_->free_anonymous_list_of.erase(me);
}
void
bdd_dict::unregister_all_typed_variables(var_type type, const void* me)
{
unsigned s = bdd_map.size();
for (unsigned i = 0; i < s; ++i)
if (bdd_map[i].type == type)
unregister_variable(i, me);
if (type == anon)
priv_->free_anonymous_list_of.erase(me);
}
std::ostream&
bdd_dict::dump(std::ostream& os) const
{

50
src/twa/bdddict.hh
View file

@ -143,44 +143,6 @@ namespace spot
}
/// @}
/// \brief Register BDD variables as acceptance variables.
///
/// Register all variables occurring in \a f as acceptance variables
/// used by \a for_me. This assumes that these acceptance variables
/// are already known from the dictionary (i.e., they have already
/// been registered by register_acceptance_variable() for another
/// automaton).
/// @{
void register_acceptance_variables(bdd f, const void* for_me);
template <typename T>
void register_acceptance_variables(bdd f, std::shared_ptr<T> for_me)
{
register_acceptance_variables(f, for_me.get());
}
/// @}
/// \brief Convert one acceptance condition into the associated
/// formula.
///
/// This version accepts a conjunction of Acc variables, in which
/// only one must be positive. This positive variable will be
/// converted back into the associated formula.
///
/// The returned formula is not cloned, and is valid until the BDD
/// variable used in \a oneacc are unregistered.
formula oneacc_to_formula(bdd oneacc) const;
/// \brief Convert one acceptance condition into the associated
/// formula.
///
/// This version takes the number of a BDD variable that must has
/// been returned by a call to register_acceptance_variable().
///
/// The returned formula is not cloned, and is valid until the BDD
/// variable \a var is unregistered.
formula oneacc_to_formula(int var) const;
/// \brief Register anonymous BDD variables.
///
/// Return (and maybe allocate) \a n consecutive BDD variables which
@ -267,18 +229,6 @@ namespace spot
/// Usually called in the destructor if \a me.
void unregister_all_my_variables(const void* me);
/// \brief Release all variables of a given type, used by an
/// object.
/// @{
void unregister_all_typed_variables(var_type type, const void* me);
template <typename T>
void unregister_all_typed_variables(var_type type, std::shared_ptr<T> me)
{
unregister_all_typed_variables(type, me.get());
}
/// @}
/// \brief Release a variable used by \a me.
/// @{
void unregister_variable(int var, const void* me);