Line data    Source code

       1             : // Author(s): Bas Ploeger
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file tree_set.cpp
      10             : 
      11             : #include "mcrl2/utilities/detail/memory_utility.h"
      12             : #include "mcrl2/utilities/logger.h"
      13             : #include "mcrl2/lts/detail/tree_set.h"
      14             : #include "mcrl2/utilities/exception.h"
      15             : 
      16             : #define EMPTY_SET (-1)
      17             : #define EMPTY_LIST (-1)
      18             : #define EMPTY_TAG (-1)
      19             : #define HASH_CLASS 16
      20             : #define TAGS_BLOCK 15000
      21             : #define BUCKETS_BLOCK 25000
      22             : // simple hash function; uses two large primes
      23             : #define hash(l,r,m) (36425657*l + 77673689*r) & m
      24             : 
      25             : namespace mcrl2
      26             : {
      27             : namespace lts
      28             : {
      29             : 
      30          75 : tree_set_store::tree_set_store()
      31             : {
      32          75 :   buckets = nullptr;
      33          75 :   buckets_size = 0;
      34          75 :   buckets_next = 0;
      35             : 
      36          75 :   tags = nullptr;
      37          75 :   tags_size = 0;
      38          75 :   tags_next = 0;
      39             : 
      40          75 :   hashmask = (1 << HASH_CLASS) - 1;
      41          75 :   hashtable = (ptrdiff_t*)malloc((hashmask+1)*sizeof(ptrdiff_t));
      42          75 :   if (hashtable == nullptr)
      43             :   {
      44           0 :     throw mcrl2::runtime_error("Out of memory.");
      45             :   }
      46     4915275 :   for (ptrdiff_t i=0; i<=hashmask; ++i)
      47             :   {
      48     4915200 :     hashtable[i] = EMPTY_LIST;
      49             :   }
      50          75 : }
      51             : 
      52          75 : tree_set_store::~tree_set_store()
      53             : {
      54          75 :   if (tags != nullptr)
      55             :   {
      56          75 :     free(tags);
      57          75 :     tags = nullptr;
      58             :   }
      59          75 :   if (buckets != nullptr)
      60             :   {
      61          75 :     free(buckets);
      62          75 :     buckets = nullptr;
      63             :   }
      64          75 :   free(hashtable);
      65          75 :   hashtable = nullptr;
      66          75 : }
      67             : 
      68         372 : void tree_set_store::check_tags()
      69             : {
      70         372 :   if (tags_next >= tags_size)
      71             :   {
      72          75 :     tags_size += TAGS_BLOCK;
      73          75 :     tags = (ptrdiff_t*)realloc(tags,tags_size*sizeof(ptrdiff_t));
      74          75 :     if (tags == nullptr)
      75             :     {
      76           0 :       throw mcrl2::runtime_error("Out of memory.");
      77             :     }
      78             :   }
      79         372 : }
      80             : 
      81         515 : void tree_set_store::check_buckets()
      82             : {
      83         515 :   if (buckets_next >= buckets_size)
      84             :   {
      85          75 :     buckets_size += BUCKETS_BLOCK;
      86          75 :     buckets = (bucket*)realloc(buckets,buckets_size*sizeof(bucket));
      87          75 :     if (buckets == nullptr)
      88             :     {
      89           0 :       throw mcrl2::runtime_error("Out of memory.");
      90             :     }
      91             :   }
      92         515 :   if (buckets_next*4 >= hashmask*3)
      93             :   {
      94           0 :     hashmask = hashmask + hashmask + 1;
      95           0 :     hashtable = (ptrdiff_t*)realloc(hashtable,(hashmask+1)*sizeof(ptrdiff_t));
      96           0 :     if (hashtable == nullptr)
      97             :     {
      98           0 :       throw mcrl2::runtime_error("Out of memory.");
      99             :     }
     100             :     ptrdiff_t i,hc;
     101           0 :     for (i=0; i<=hashmask; ++i)
     102             :     {
     103           0 :       hashtable[i] = EMPTY_LIST;
     104             :     }
     105           0 :     for (i=0; i<buckets_next; ++i)
     106             :     {
     107           0 :       hc = hash(buckets[i].child_l,buckets[i].child_r,hashmask);
     108           0 :       buckets[i].next = hashtable[hc];
     109           0 :       hashtable[hc] = i;
     110             :     }
     111             :   }
     112         515 : }
     113             : 
     114         515 : ptrdiff_t tree_set_store::build_set(ptrdiff_t child_l,ptrdiff_t child_r)
     115             : {
     116         515 :   check_buckets();
     117         515 :   ptrdiff_t hc = hash(child_l,child_r,hashmask);
     118         515 :   buckets[buckets_next].child_l = child_l;
     119         515 :   buckets[buckets_next].child_r = child_r;
     120         515 :   buckets[buckets_next].tag     = EMPTY_TAG;
     121         515 :   buckets[buckets_next].next    = hashtable[hc];
     122         515 :   hashtable[hc] = buckets_next;
     123         515 :   return buckets_next++;
     124             : }
     125             : 
     126         749 : ptrdiff_t tree_set_store::find_set(ptrdiff_t child_l,ptrdiff_t child_r)
     127             : {
     128         749 :   ptrdiff_t hc = hash(child_l,child_r,hashmask);
     129         749 :   for (ptrdiff_t i=hashtable[hc]; i!=EMPTY_LIST; i=buckets[i].next)
     130             :   {
     131         234 :     if (buckets[i].child_l==child_l && buckets[i].child_r==child_r)
     132             :     {
     133         234 :       return i;
     134             :     }
     135             :   }
     136         515 :   return build_set(child_l,child_r);
     137             : }
     138             : 
     139        1966 : ptrdiff_t tree_set_store::create_set(std::vector<ptrdiff_t> &elems)
     140             : {
     141        1966 :   if (elems.size() == 0)
     142             :   {
     143        1421 :     return EMPTY_SET;
     144             :   }
     145             : 
     146         545 :   ptrdiff_t* nodes = MCRL2_SPECIFIC_STACK_ALLOCATOR(ptrdiff_t,elems.size());
     147         545 :   std::size_t node_size = 0;
     148             :   std::size_t i,j;
     149        1192 :   for (i=0; i < elems.size(); ++i)
     150             :   {
     151         647 :     nodes[i]=find_set(elems[i],EMPTY_SET);
     152             :   }
     153         545 :   node_size = i;
     154         647 :   while (node_size > 1)
     155             :   {
     156         102 :     j = 0;
     157         216 :     for (i=0; i<node_size; i+=2)
     158             :     {
     159         114 :       if (i == node_size-1)
     160             :       {
     161          12 :         nodes[j] = nodes[i];
     162             :       }
     163             :       else
     164             :       {
     165         102 :         nodes[j] = find_set(nodes[i],nodes[i+1]);
     166             :       }
     167         114 :       ++j;
     168             :     }
     169         102 :     node_size = j;
     170             :   }
     171         545 :   ptrdiff_t r = nodes[0];
     172         545 :   return r;
     173             : }
     174             : 
     175         447 : ptrdiff_t tree_set_store::get_next_tag()
     176             : {
     177         447 :   return tags_next;
     178             : }
     179             : 
     180         372 : ptrdiff_t tree_set_store::get_set(ptrdiff_t tag)
     181             : {
     182         372 :   return tags[tag];
     183             : }
     184             : 
     185         558 : ptrdiff_t tree_set_store::get_set_child_left(ptrdiff_t set)
     186             : {
     187         558 :   return buckets[set].child_l;
     188             : }
     189             : 
     190         651 : ptrdiff_t tree_set_store::get_set_child_right(ptrdiff_t set)
     191             : {
     192         651 :   return buckets[set].child_r;
     193             : }
     194             : 
     195           0 : ptrdiff_t tree_set_store::get_set_size(ptrdiff_t set)
     196             : {
     197           0 :   if (buckets[set].child_r == EMPTY_SET)
     198             :   {
     199           0 :     return 1;
     200             :   }
     201           0 :   return get_set_size(buckets[set].child_l) +
     202           0 :          get_set_size(buckets[set].child_r);
     203             : }
     204             : 
     205        3007 : bool tree_set_store::is_set_empty(ptrdiff_t set)
     206             : {
     207        3007 :   return (set == EMPTY_SET);
     208             : }
     209             : 
     210         545 : ptrdiff_t tree_set_store::set_set_tag(ptrdiff_t set)
     211             : {
     212         545 :   if (buckets[set].tag != EMPTY_TAG)
     213             :   {
     214         173 :     return buckets[set].tag;
     215             :   }
     216         372 :   check_tags();
     217         372 :   tags[tags_next] = set;
     218         372 :   buckets[set].tag = tags_next;
     219         372 :   return tags_next++;
     220             : }
     221             : 
     222             : }
     223             : }