25 #include <spot/misc/common.hh> 52 const char* parse_options(
const char* options);
62 int get(
const char* option,
int def = 0)
const;
69 std::string get_str(
const char* option, std::string def = {})
const;
75 int operator[](
const char* option)
const;
81 int set(
const char* option,
int val,
int def = 0);
87 std::string set_str(
const char* option,
88 std::string val, std::string def = {});
91 void report_unused_options()
const;
97 int& operator[](
const char* option);
100 friend SPOT_API std::ostream&
101 operator<<(std::ostream& os,
const option_map& m);
104 std::map<std::string, int> options_;
105 std::map<std::string, std::string> options_str_;
109 mutable std::set<std::string> unused_;
111 void set_(
const std::string&,
int val);
112 void set_str_(
const std::string&,
const std::string& val);
Manage a map of options.
Definition: optionmap.hh:37