LCOV - code coverage report
Current view: top level - lts/source - tree_set.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 87 105 82.9 %
Date: 2020-02-19 00:44:21 Functions: 15 16 93.8 %
Legend: Lines: hit not hit

          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             : using namespace std;
      26             : 
      27             : namespace mcrl2
      28             : {
      29             : namespace lts
      30             : {
      31             : 
      32          75 : tree_set_store::tree_set_store()
      33             : {
      34          75 :   buckets = nullptr;
      35          75 :   buckets_size = 0;
      36          75 :   buckets_next = 0;
      37             : 
      38          75 :   tags = nullptr;
      39          75 :   tags_size = 0;
      40          75 :   tags_next = 0;
      41             : 
      42          75 :   hashmask = (1 << HASH_CLASS) - 1;
      43          75 :   hashtable = (ptrdiff_t*)malloc((hashmask+1)*sizeof(ptrdiff_t));
      44          75 :   if (hashtable == nullptr)
      45             :   {
      46           0 :     throw mcrl2::runtime_error("Out of memory.");
      47             :   }
      48     4915275 :   for (ptrdiff_t i=0; i<=hashmask; ++i)
      49             :   {
      50     4915200 :     hashtable[i] = EMPTY_LIST;
      51             :   }
      52          75 : }
      53             : 
      54         150 : tree_set_store::~tree_set_store()
      55             : {
      56          75 :   if (tags != nullptr)
      57             :   {
      58          75 :     free(tags);
      59          75 :     tags = nullptr;
      60             :   }
      61          75 :   if (buckets != nullptr)
      62             :   {
      63          75 :     free(buckets);
      64          75 :     buckets = nullptr;
      65             :   }
      66          75 :   free(hashtable);
      67          75 :   hashtable = nullptr;
      68          75 : }
      69             : 
      70         372 : void tree_set_store::check_tags()
      71             : {
      72         372 :   if (tags_next >= tags_size)
      73             :   {
      74          75 :     tags_size += TAGS_BLOCK;
      75          75 :     tags = (ptrdiff_t*)realloc(tags,tags_size*sizeof(ptrdiff_t));
      76          75 :     if (tags == nullptr)
      77             :     {
      78           0 :       throw mcrl2::runtime_error("Out of memory.");
      79             :     }
      80             :   }
      81         372 : }
      82             : 
      83         515 : void tree_set_store::check_buckets()
      84             : {
      85         515 :   if (buckets_next >= buckets_size)
      86             :   {
      87          75 :     buckets_size += BUCKETS_BLOCK;
      88          75 :     buckets = (bucket*)realloc(buckets,buckets_size*sizeof(bucket));
      89          75 :     if (buckets == nullptr)
      90             :     {
      91           0 :       throw mcrl2::runtime_error("Out of memory.");
      92             :     }
      93             :   }
      94         515 :   if (buckets_next*4 >= hashmask*3)
      95             :   {
      96           0 :     hashmask = hashmask + hashmask + 1;
      97           0 :     hashtable = (ptrdiff_t*)realloc(hashtable,(hashmask+1)*sizeof(ptrdiff_t));
      98           0 :     if (hashtable == nullptr)
      99             :     {
     100           0 :       throw mcrl2::runtime_error("Out of memory.");
     101             :     }
     102             :     ptrdiff_t i,hc;
     103           0 :     for (i=0; i<=hashmask; ++i)
     104             :     {
     105           0 :       hashtable[i] = EMPTY_LIST;
     106             :     }
     107           0 :     for (i=0; i<buckets_next; ++i)
     108             :     {
     109           0 :       hc = hash(buckets[i].child_l,buckets[i].child_r,hashmask);
     110           0 :       buckets[i].next = hashtable[hc];
     111           0 :       hashtable[hc] = i;
     112             :     }
     113             :   }
     114         515 : }
     115             : 
     116         515 : ptrdiff_t tree_set_store::build_set(ptrdiff_t child_l,ptrdiff_t child_r)
     117             : {
     118         515 :   check_buckets();
     119         515 :   ptrdiff_t hc = hash(child_l,child_r,hashmask);
     120         515 :   buckets[buckets_next].child_l = child_l;
     121         515 :   buckets[buckets_next].child_r = child_r;
     122         515 :   buckets[buckets_next].tag     = EMPTY_TAG;
     123         515 :   buckets[buckets_next].next    = hashtable[hc];
     124         515 :   hashtable[hc] = buckets_next;
     125         515 :   return buckets_next++;
     126             : }
     127             : 
     128         749 : ptrdiff_t tree_set_store::find_set(ptrdiff_t child_l,ptrdiff_t child_r)
     129             : {
     130         749 :   ptrdiff_t hc = hash(child_l,child_r,hashmask);
     131         749 :   for (ptrdiff_t i=hashtable[hc]; i!=EMPTY_LIST; i=buckets[i].next)
     132             :   {
     133         234 :     if (buckets[i].child_l==child_l && buckets[i].child_r==child_r)
     134             :     {
     135         234 :       return i;
     136             :     }
     137             :   }
     138         515 :   return build_set(child_l,child_r);
     139             : }
     140             : 
     141        1966 : ptrdiff_t tree_set_store::create_set(vector<ptrdiff_t> &elems)
     142             : {
     143        1966 :   if (elems.size() == 0)
     144             :   {
     145        1421 :     return EMPTY_SET;
     146             :   }
     147             : 
     148         545 :   ptrdiff_t* nodes = MCRL2_SPECIFIC_STACK_ALLOCATOR(ptrdiff_t,elems.size());
     149         545 :   std::size_t node_size = 0;
     150             :   std::size_t i,j;
     151        1192 :   for (i=0; i < elems.size(); ++i)
     152             :   {
     153         647 :     nodes[i]=find_set(elems[i],EMPTY_SET);
     154             :   }
     155         545 :   node_size = i;
     156         749 :   while (node_size > 1)
     157             :   {
     158         102 :     j = 0;
     159         216 :     for (i=0; i<node_size; i+=2)
     160             :     {
     161         114 :       if (i == node_size-1)
     162             :       {
     163          12 :         nodes[j] = nodes[i];
     164             :       }
     165             :       else
     166             :       {
     167         102 :         nodes[j] = find_set(nodes[i],nodes[i+1]);
     168             :       }
     169         114 :       ++j;
     170             :     }
     171         102 :     node_size = j;
     172             :   }
     173         545 :   ptrdiff_t r = nodes[0];
     174         545 :   return r;
     175             : }
     176             : 
     177         447 : ptrdiff_t tree_set_store::get_next_tag()
     178             : {
     179         447 :   return tags_next;
     180             : }
     181             : 
     182         372 : ptrdiff_t tree_set_store::get_set(ptrdiff_t tag)
     183             : {
     184         372 :   return tags[tag];
     185             : }
     186             : 
     187         558 : ptrdiff_t tree_set_store::get_set_child_left(ptrdiff_t set)
     188             : {
     189         558 :   return buckets[set].child_l;
     190             : }
     191             : 
     192         651 : ptrdiff_t tree_set_store::get_set_child_right(ptrdiff_t set)
     193             : {
     194         651 :   return buckets[set].child_r;
     195             : }
     196             : 
     197           0 : ptrdiff_t tree_set_store::get_set_size(ptrdiff_t set)
     198             : {
     199           0 :   if (buckets[set].child_r == EMPTY_SET)
     200             :   {
     201           0 :     return 1;
     202             :   }
     203           0 :   return get_set_size(buckets[set].child_l) +
     204           0 :          get_set_size(buckets[set].child_r);
     205             : }
     206             : 
     207        3007 : bool tree_set_store::is_set_empty(ptrdiff_t set)
     208             : {
     209        3007 :   return (set == EMPTY_SET);
     210             : }
     211             : 
     212         545 : ptrdiff_t tree_set_store::set_set_tag(ptrdiff_t set)
     213             : {
     214         545 :   if (buckets[set].tag != EMPTY_TAG)
     215             :   {
     216         173 :     return buckets[set].tag;
     217             :   }
     218         372 :   check_tags();
     219         372 :   tags[tags_next] = set;
     220         372 :   buckets[set].tag = tags_next;
     221         372 :   return tags_next++;
     222             : }
     223             : 
     224             : }
     225          21 : }

Generated by: LCOV version 1.13