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

@@ -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 <spot/tl/formula.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
+#include <spot/misc/hash.hh>
+#include <spot/priv/robin_hood.hh>
+#include <spot/twaalgos/ltl2tgba_fm.hh>
 
 namespace spot
 {
+  struct language_containment_checker::record_
+  {
+    const_twa_graph_ptr translation;
+    typedef robin_hood::unordered_flat_map<const record_*, bool> 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<formula,
+                                   language_containment_checker::record_>
+  {
+  };
+
   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);
+    return contained_neg(l, formula::Not(g));
-    record_* rng = register_formula_(formula::Not(g));
-    return incompatible_(rl, rng);
   }
 
+
   // 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);
+    return contained_neg(nl, formula::Not(g));
-    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);
   }
 
   // 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);
+    auto i = translated_->find(f);
-    if (i != translated_.end())
+    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];
+    return &translated_->emplace(f, std::move(e)).first->second;
-    r.translation = e;
-    return &r;
   }
 }

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 <spot/tl/formula.hh>
-#include <spot/twaalgos/ltl2tgba_fm.hh>
+#include <spot/twa/bdddict.hh>
-#include <spot/misc/hash.hh>
-#include <map>
 
 namespace spot
 {
+  class tl_simplifier_cache;
+
   /// Check containment between LTL formulae.
   class SPOT_API language_containment_checker
   {
-    struct record_
+    struct record_;
-    {
+    struct trans_map_;
-      const_twa_graph_ptr translation;
-      typedef std::map<const record_*, bool> incomp_map;
-      incomp_map incompatible;
-    };
-    typedef std::unordered_map<formula, record_> 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_;
   };
 }

spot/tl/simplify.cc

@@ -36,6 +36,7 @@
 #include <spot/misc/minato.hh>
 #include <cassert>
 #include <memory>
+#include <unordered_set>
 
 namespace spot
 {