diff --git a/spot/misc/optionmap.cc b/spot/misc/optionmap.cc index 3349f0f0d..4db5235eb 100644 --- a/spot/misc/optionmap.cc +++ b/spot/misc/optionmap.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013-2016, 2018 Laboratoire de Recherche +// Copyright (C) 2008, 2013-2016, 2018, 2022 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -158,17 +158,39 @@ namespace spot int option_map::set(const char* option, int val, int def) { - int old = get(option, def); - set_(option, val); - return old; + if (auto [p, b] = options_.emplace(option, val); b) + { + unused_.insert(option); + return def; + } + else + { + int old = p->second; + p->second = val; + return old; + } + } + + void + option_map::set_if_unset(const char* option, int val) + { + if (options_.emplace(option, val).second) + unused_.insert(option); } std::string option_map::set_str(const char* option, std::string val, std::string def) { - std::string old = get_str(option, def); - set_str_(option, val); - return old; + if (auto [p, b] = options_str_.emplace(option, val); b) + { + unused_.insert(option); + return def; + } + else + { + std::swap(val, p->second); + return val; + } } void diff --git a/spot/misc/optionmap.hh b/spot/misc/optionmap.hh index ea06c62f9..229733a18 100644 --- a/spot/misc/optionmap.hh +++ b/spot/misc/optionmap.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015, 2016-2017 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) +// Copyright (C) 2013, 2015, 2016-2017, 2022 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE) // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -80,6 +80,9 @@ namespace spot /// or \a def otherwise. int set(const char* option, int val, int def = 0); + /// \brief Set the value of \a option to \a val if it is unset. + void set_if_unset(const char* option, int val); + /// \brief Set the value of a string \a option to \a val. /// /// \return The previous value associated to \a option if declared, diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 9025bb303..ec2defb4f 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2020, 2021 Laboratoire de Recherche et +// Copyright (C) 2020-2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -768,13 +768,9 @@ namespace spot auto sol = gi.s; const bdd_dict_ptr& dict = gi.dict; - for (auto&& p : std::vector> - {{"simul", 0}, - {"ba-simul", 0}, - {"det-simul", 0}, - {"tls-impl", 1}, - {"wdba-minimize", 2}}) - extra_options.set(p.first, extra_options.get(p.first, p.second)); + extra_options.set_if_unset("simul", 0); + extra_options.set_if_unset("tls-impl", 1); + extra_options.set_if_unset("wdba-minimize", 2); translator trans(dict, &extra_options); switch (sol)