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

Generated by: LCOV version 1.12