optionmap: set_if_unset and simplifications

* spot/misc/optionmap.hh (set_if_unset): New method.
* spot/misc/optionmap.cc (set_if_unset, set, set_str): Implement
set_if_unset, and simplify set and set_str to not perform two lookups.
* spot/twaalgos/synthesis.cc (create_translator): Use set_if_unset
to simplify the code.

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);
+    if (auto [p, b] = options_.emplace(option, val); b)
-    set_(option, val);
+      {
-    return old;
+        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);
+    if (auto [p, b] = options_str_.emplace(option, val); b)
-    set_str_(option, val);
+      {
-    return old;
+        unused_.insert(option);
+        return def;
+      }
+    else
+      {
+        std::swap(val, p->second);
+        return val;
+      }
   }
 
   void

spot/misc/optionmap.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2015, 2016-2017 Laboratoire de Recherche et
+// Copyright (C) 2013, 2015, 2016-2017, 2022 Laboratoire de Recherche
-// Developpement de l'Epita (LRDE)
+// 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,

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<std::pair<const char*, int>>
+      extra_options.set_if_unset("simul", 0);
-                        {{"simul", 0},
+      extra_options.set_if_unset("tls-impl", 1);
-                         {"ba-simul", 0},
+      extra_options.set_if_unset("wdba-minimize", 2);
-                         {"det-simul", 0},
-                         {"tls-impl", 1},
-                         {"wdba-minimize", 2}})
-        extra_options.set(p.first, extra_options.get(p.first, p.second));
 
       translator trans(dict, &extra_options);
       switch (sol)