CBMC
irep_hash_container.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Hashing IREPs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "irep_hash_container.h"
13 
14 #include "irep.h"
15 #include "irep_hash.h"
16 
18 {
19  // the ptr-hash provides a speedup of up to 3x
20 
21  ptr_hasht::const_iterator it=ptr_hash.find(&irep.read());
22 
23  if(it!=ptr_hash.end())
24  return it->second.number;
25 
26  packedt packed;
27  pack(irep, packed);
28  size_t id=numbering.number(packed);
29 
30  ptr_hash.emplace(
31  std::piecewise_construct,
32  std::forward_as_tuple(&irep.read()),
33  std::forward_as_tuple(id, irep));
34 
35  return id;
36 }
37 
39  const packedt &p) const
40 {
41  size_t result=p.size(); // seed
42  for(auto elem : p)
43  result=hash_combine(result, elem);
44  return result;
45 }
46 
48  const irept &irep,
49  packedt &packed)
50 {
51  const irept::subt &sub=irep.get_sub();
52  const irept::named_subt &named_sub=irep.get_named_sub();
53 
54  if(full)
55  {
56  // we pack: the irep id, the sub size, the subs, the named-sub size, and
57  // each of the named subs with their ids
58 #if NAMED_SUB_IS_FORWARD_LIST
59  const std::size_t named_sub_size =
60  std::distance(named_sub.begin(), named_sub.end());
61 #else
62  const std::size_t named_sub_size = named_sub.size();
63 #endif
64  packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);
65 
66  packed.push_back(irep_id_hash()(irep.id()));
67 
68  packed.push_back(sub.size());
69  for(const auto &sub_irep : sub)
70  packed.push_back(number(sub_irep));
71 
72  packed.push_back(named_sub_size);
73  for(const auto &sub_irep : named_sub)
74  {
75  packed.push_back(irep_id_hash()(sub_irep.first)); // id
76  packed.push_back(number(sub_irep.second)); // sub-irep
77  }
78  }
79  else
80  {
81  const std::size_t non_comment_count =
83 
84  // we pack: the irep id, the sub size, the subs, the named-sub size, and
85  // each of the non-comment named subs with their ids
86  packed.reserve(1 + 1 + sub.size() + 1 + non_comment_count * 2);
87 
88  packed.push_back(irep_id_hash()(irep.id()));
89 
90  packed.push_back(sub.size());
91  for(const auto &sub_irep : sub)
92  packed.push_back(number(sub_irep));
93 
94  packed.push_back(non_comment_count);
95  for(const auto &sub_irep : named_sub)
96  if(!irept::is_comment(sub_irep.first))
97  {
98  packed.push_back(irep_id_hash()(sub_irep.first)); // id
99  packed.push_back(number(sub_irep.second)); // sub-irep
100  }
101  }
102 }
irep_hash_container_baset::numbering
numberingt< packedt, vector_hasht > numbering
Definition: irep_hash_container.h:73
irep_hash_container_baset::pack
void pack(const irept &irep, packedt &)
Definition: irep_hash_container.cpp:47
irep_hash_container_baset::packedt
std::vector< std::size_t > packedt
Definition: irep_hash_container.h:66
irep_hash_container_baset::vector_hasht::operator()
std::size_t operator()(const packedt &p) const
Definition: irep_hash_container.cpp:38
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::named_subt
typename dt::named_subt named_subt
Definition: irep.h:161
irep_hash_container.h
irept::number_of_non_comments
static std::size_t number_of_non_comments(const named_subt &)
count the number of named_sub elements that are not comments
Definition: irep.cpp:417
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:458
sharing_treet::read
const dt & read() const
Definition: irep.h:248
hash_combine
#define hash_combine(h1, h2)
Definition: irep_hash.h:121
irept::id
const irep_idt & id() const
Definition: irep.h:396
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition: irep.h:160
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:39
irep_hash_container_baset::number
std::size_t number(const irept &irep)
Definition: irep_hash_container.cpp:17
irept::get_sub
subt & get_sub()
Definition: irep.h:456
irep_hash_container_baset::full
bool full
Definition: irep_hash_container.h:77
irep_hash.h
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
irept::is_comment
static bool is_comment(const irep_idt &name)
Definition: irep.h:468
irep.h
irep_hash_container_baset::ptr_hash
ptr_hasht ptr_hash
Definition: irep_hash_container.h:62