diff --git a/src/twa/bdddict.cc b/src/twa/bdddict.cc index 0f23a6d5e..6cc9e63ae 100644 --- a/src/twa/bdddict.cc +++ b/src/twa/bdddict.cc @@ -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 { diff --git a/src/twa/bdddict.hh b/src/twa/bdddict.hh index 53ccc94a4..39f741e8a 100644 --- a/src/twa/bdddict.hh +++ b/src/twa/bdddict.hh @@ -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 - void register_acceptance_variables(bdd f, std::shared_ptr 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 - void unregister_all_typed_variables(var_type type, std::shared_ptr me) - { - unregister_all_typed_variables(type, me.get()); - } - /// @} - /// \brief Release a variable used by \a me. /// @{ void unregister_variable(int var, const void* me);