From 4c94e14f867bf871a290f326d36ed749837a2b91 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Sep 2021 16:47:52 +0200 Subject: [PATCH] parseaut: replace std::map by robin_hood::unordered_flat_map This improves the parsing performance a bit more. * spot/parseaut/parsedecl.hh, spot/parseaut/parseaut.yy: Here. * tests/sanity/style.test: Handle parsedecl.hh as a private header. --- spot/parseaut/parseaut.yy | 3 ++- spot/parseaut/parsedecl.hh | 3 ++- tests/sanity/style.test | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 3efa85047..c71636bde 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -33,6 +33,7 @@ { #include "config.h" #include +#include #include #include #include @@ -64,7 +65,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); over and over, and to register all their atomic_propositions in the bdd_dict. Keep the bdd result around so we can reuse it. */ - typedef std::map formula_cache; + typedef robin_hood::unordered_flat_map formula_cache; typedef std::pair pair; typedef spot::twa_graph::namer named_tgba_t; diff --git a/spot/parseaut/parsedecl.hh b/spot/parseaut/parsedecl.hh index ad2d1ae78..14fcc9958 100644 --- a/spot/parseaut/parsedecl.hh +++ b/spot/parseaut/parsedecl.hh @@ -20,6 +20,7 @@ #pragma once #include +#include "spot/priv/robin_hood.hh" #include #include @@ -28,7 +29,7 @@ spot::location *yylloc, \ void* yyscanner, \ spot::parse_aut_error_list& error_list, \ - std::map& fmap) + robin_hood::unordered_flat_map& fmap) YY_DECL; namespace spot diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 29fe48aea..8f157014d 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -313,7 +313,7 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do # (in the latter case they do not have to specify the priv/ # directory, so they will not match this regex). case $file in - */priv/*|*/bin/*);; + */priv/*|*/bin/*|*/parsedecl.hh);; *) $GREP '#.*include.*priv/' $tmp && diag 'Do not include private headers in public headers.'