From 803a966ffeca9c7a16f3f104c6b0616274f1713e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 Oct 2019 15:49:43 +0100 Subject: [PATCH] contain: some micro-optimizations * spot/tl/contain.cc, spot/tl/contain.hh: Use a pimp idiom to hide the hash tables, use robin_hood hash, and strip common Xs to save some cache lookups. * spot/tl/simplify.cc: Adjust to change of #include in contain.hh. --- spot/tl/contain.cc | 84 ++++++++++++++++++++++++++++++--------------- spot/tl/contain.hh | 20 +++++------ spot/tl/simplify.cc | 1 + 3 files changed, 65 insertions(+), 40 deletions(-) diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc index 19c3b7158..a6cb12806 100644 --- a/spot/tl/contain.cc +++ b/spot/tl/contain.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2012, 2014-2016, 2018 Laboratoire de Recherche +// Copyright (C) 2009-2012, 2014-2016, 2018, 2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -26,27 +26,50 @@ #include #include #include +#include +#include +#include namespace spot { + struct language_containment_checker::record_ + { + const_twa_graph_ptr translation; + typedef robin_hood::unordered_flat_map incomp_map; + incomp_map incompatible; + + record_(const_twa_graph_ptr&& trans) noexcept + : translation(std::move(trans)) + { + } + }; + + struct language_containment_checker::trans_map_ : + robin_hood::unordered_node_map + { + }; + language_containment_checker::language_containment_checker (bdd_dict_ptr dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx) : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), branching_postponement_(branching_postponement), - fair_loop_approx_(fair_loop_approx) + fair_loop_approx_(fair_loop_approx), + translated_(new trans_map_) { } language_containment_checker::~language_containment_checker() { clear(); + delete translated_; } void language_containment_checker::clear() { - translated_.clear(); + translated_->clear(); } bool @@ -57,11 +80,34 @@ namespace spot return i->second; bool res = product(l->translation, g->translation)->is_empty(); + // bool res = !l->translation->intersects(g->translation); l->incompatible[g] = res; g->incompatible[l] = res; return res; } + static void trim_common_Xs(formula& l, formula& r) + { + while (l.is(op::X) && r.is(op::X)) + { + l = l[0]; + r = r[0]; + } + } + + // Check whether L(l) is a subset of L(!g). + bool + language_containment_checker::contained_neg(formula l, + formula g) + { + if (l == g) + return false; + trim_common_Xs(l, g); + record_* rl = register_formula_(l); + record_* rg = register_formula_(g); + return incompatible_(rl, rg); + } + // Check whether L(l) is a subset of L(g). bool @@ -70,11 +116,10 @@ namespace spot { if (l == g) return true; - record_* rl = register_formula_(l); - record_* rng = register_formula_(formula::Not(g)); - return incompatible_(rl, rng); + return contained_neg(l, formula::Not(g)); } + // Check whether L(!l) is a subset of L(g). bool language_containment_checker::neg_contained(formula l, @@ -83,29 +128,14 @@ namespace spot if (l == g) return false; formula nl = formula::Not(l); - record_* rnl = register_formula_(nl); - record_* rng = register_formula_(formula::Not(g)); - if (nl == g) - return true; - return incompatible_(rnl, rng); - } - - // Check whether L(l) is a subset of L(!g). - bool - language_containment_checker::contained_neg(formula l, - formula g) - { - if (l == g) - return false; - record_* rl = register_formula_(l); - record_* rg = register_formula_(g); - return incompatible_(rl, rg); + return contained_neg(nl, formula::Not(g)); } // Check whether L(l) = L(g). bool language_containment_checker::equal(formula l, formula g) { + trim_common_Xs(l, g); if (l == g) return true; record_* rl = register_formula_(l); @@ -118,14 +148,12 @@ namespace spot language_containment_checker::record_* language_containment_checker::register_formula_(formula f) { - trans_map::iterator i = translated_.find(f); - if (i != translated_.end()) + auto i = translated_->find(f); + if (i != translated_->end()) return &i->second; auto e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, branching_postponement_, fair_loop_approx_); - record_& r = translated_[f]; - r.translation = e; - return &r; + return &translated_->emplace(f, std::move(e)).first->second; } } diff --git a/spot/tl/contain.hh b/spot/tl/contain.hh index f26ca5a9a..20fa714fd 100644 --- a/spot/tl/contain.hh +++ b/spot/tl/contain.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2011-2016, 2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -23,22 +23,17 @@ #pragma once #include -#include -#include -#include +#include namespace spot { + class tl_simplifier_cache; + /// Check containment between LTL formulae. class SPOT_API language_containment_checker { - struct record_ - { - const_twa_graph_ptr translation; - typedef std::map incomp_map; - incomp_map incompatible; - }; - typedef std::unordered_map trans_map; + struct record_; + struct trans_map_; public: /// This class uses spot::ltl_to_tgba_fm to translate LTL /// formulae. See that function for the meaning of these options. @@ -75,6 +70,7 @@ namespace spot bool branching_postponement_; bool fair_loop_approx_; /* Translation Maps */ - trans_map translated_; + trans_map_* translated_; + tl_simplifier_cache* c_; }; } diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 8b22dd601..5196f5b3d 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -36,6 +36,7 @@ #include #include #include +#include namespace spot {