Use std::forward_list instead of std::map in irept by default

src/util/irep.cpp

@@ -92,7 +92,7 @@ void irept::set(const irep_namet &name, const long long value)
 
 void irept::remove(const irep_namet &name)
 {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   return get_named_sub().remove(name);
 #else
   named_subt &s = get_named_sub();
@@ -120,7 +120,7 @@ irept &irept::add(const irep_namet &name, irept irep)
 {
   named_subt &s = get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   return s.add(name, std::move(irep));
 #else
   std::pair<named_subt::iterator, bool> entry = s.emplace(

src/util/irep.h

@@ -20,9 +20,14 @@ Author: Daniel Kroening, [email protected]
 #ifndef HASH_CODE
 #  define HASH_CODE 1
 #endif
-// #define NAMED_SUB_IS_FORWARD_LIST
+// use forward_list by default, unless _GLIBCXX_DEBUG is set as the debug
+// overhead is noticeably higher with the regression test suite taking four
+// times as long.
+#if !defined(NAMED_SUB_IS_FORWARD_LIST) && !defined(_GLIBCXX_DEBUG)
+#  define NAMED_SUB_IS_FORWARD_LIST 1
+#endif
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
 #  include "forward_list_as_map.h"
 #else
 #include <map>
@@ -386,7 +391,7 @@ class irept
   : public non_sharing_treet<
       irept,
 #endif
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
       forward_list_as_mapt<irep_namet, irept>>
 #else
       std::map<irep_namet, irept>>

src/util/irep_hash_container.cpp

@@ -55,7 +55,7 @@ void irep_hash_container_baset::pack(
   {
     // we pack: the irep id, the sub size, the subs, the named-sub size, and
     // each of the named subs with their ids
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     const std::size_t named_sub_size =
       std::distance(named_sub.begin(), named_sub.end());
 #else

src/util/irep_serialization.cpp

@@ -76,14 +76,14 @@ irept irep_serializationt::read_irep(std::istream &in)
     sub.push_back(reference_convert(in));
   }
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = named_sub.before_begin();
 #endif
   while(in.peek()=='N')
   {
     in.get();
     irep_idt id = read_string_ref(in);
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     named_sub.emplace_after(before, id, reference_convert(in));
     ++before;
 #else
@@ -95,7 +95,7 @@ irept irep_serializationt::read_irep(std::istream &in)
   {
     in.get();
     irep_idt id = read_string_ref(in);
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     named_sub.emplace_after(before, id, reference_convert(in));
     ++before;
 #else

src/util/lispirep.cpp

@@ -46,7 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value.clear();
   dest.type=lispexprt::List;
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   const std::size_t named_sub_size =
     std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
 #else

src/util/merge_irep.cpp

@@ -46,7 +46,7 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
 
   if(sub.size()!=o_sub.size())
     return false;
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   if(
     std::distance(named_sub.begin(), named_sub.end()) !=
     std::distance(o_named_sub.begin(), o_named_sub.end()))
@@ -105,12 +105,12 @@ const merged_irept &merged_irepst::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = dest_named_sub.before_begin();
 #endif
   forall_named_irep(it, src_named_sub)
   {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     dest_named_sub.emplace_after(
       before, it->first, merged(it->second)); // recursive call
     ++before;
@@ -209,12 +209,12 @@ const irept &merge_full_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = dest_named_sub.before_begin();
 #endif
   forall_named_irep(it, src_named_sub)
   {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     dest_named_sub.emplace_after(
       before, it->first, merged(it->second)); // recursive call
     ++before;

src/util/type.h

@@ -31,7 +31,8 @@ class typet:public irept
 
   explicit typet(const irep_idt &_id):irept(_id) { }
 
-#if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6
+  // the STL implementation shipped with GCC 5 is broken
+#if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
   typet(irep_idt _id, typet _subtype)
     : irept(std::move(_id), {}, {std::move(_subtype)})
   {

unit/util/irep.cpp

@@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       REQUIRE(sizeof(std::vector<int>) == 3 * sizeof(void *));
 #endif
 
-#ifndef NAMED_SUB_IS_FORWARD_LIST
+#if !NAMED_SUB_IS_FORWARD_LIST
       const std::size_t named_size = sizeof(std::map<int, int>);
 #  ifndef _GLIBCXX_DEBUG
 #    ifdef __APPLE__