From df73b84a4779a571c12299584e940e555ad2c52f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 5 Nov 2017 09:43:01 +0100 Subject: [PATCH] bdd_dict: remove register_all_propositions_of * spot/twa/bdddict.cc, spot/twa/bdddict.hh: Here. * NEWS: Mention this removal. --- NEWS | 8 ++++++-- spot/twa/bdddict.cc | 18 ++---------------- spot/twa/bdddict.hh | 37 ++----------------------------------- 3 files changed, 10 insertions(+), 53 deletions(-) diff --git a/NEWS b/NEWS index 15c1aba2d..229ac9476 100644 --- a/NEWS +++ b/NEWS @@ -173,14 +173,18 @@ New in spot 2.4.1.dev (not yet released) - The spot::closure(), spot::sl2(), spot::is_stutter_invariant() functions no longuer takes && arguments. The former two have - spot::closure_inplace() and spot::sl2_inplace() variant. These - function also do not take to list of atomic propositions as an + spot::closure_inplace() and spot::sl2_inplace() variants. These + functions also do not take a list of atomic propositions as an argument anymore. - The spot::bmrand() and spot::prand() functions have been removed. They were not used at all in Spot, and it's not Spot's objective to provide such random functions. + - The spot::bdd_dict::register_all_propositions_of() function has + been removed. It's a low-level function was not used anywhere in + Spot anymore, since it's better to use spot::twa::copy_ap_of(). + Bugs fixed: - Automata produced by "genaut --ks-nca=N" were incorrectly marked diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc index ef601ad70..58d7185c3 100644 --- a/spot/twa/bdddict.cc +++ b/spot/twa/bdddict.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2012-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -197,20 +197,6 @@ namespace spot } - void - bdd_dict::register_all_propositions_of(const void* from_other, - const void* for_me) - { - for (auto& i: bdd_map) - { - if (i.type != var_type::var) - continue; - ref_set& s = i.refs; - if (s.find(from_other) != s.end()) - s.insert(for_me); - } - } - void bdd_dict::unregister_variable(int v, const void* me) { diff --git a/spot/twa/bdddict.hh b/spot/twa/bdddict.hh index fafa4c214..c9b39d8a5 100644 --- a/spot/twa/bdddict.hh +++ b/spot/twa/bdddict.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2011-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -199,39 +199,6 @@ namespace spot } /// @} - /// \brief Register the same propositions as another object. - /// - /// This tells this dictionary that the \a for_me object will be - /// using the same BDD variable used for atomic propositions by - /// the \a from_other object. This ensures that the variables - /// won't be freed when \a from_other is deleted if \a from_other - /// is still alive. - /// @{ - void register_all_propositions_of(const void* from_other, - const void* for_me); - - template - void register_all_propositions_of(const void* from_other, - std::shared_ptr for_me) - { - register_all_propositions_of(from_other, for_me.get()); - } - - template - void register_all_propositions_of(std::shared_ptr from_other, - const void* for_me) - { - register_all_propositions_of(from_other.get(), for_me); - } - - template - void register_all_propositions_of(std::shared_ptr from_other, - std::shared_ptr for_me) - { - register_all_propositions_of(from_other.get(), for_me.get()); - } - /// @} - /// \brief Release all variables used by an object. /// /// Usually called in the destructor if \a me.