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  const std::size_t named_sub_size = named_sub.size();
59  packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);
60 
61  packed.push_back(irep_id_hash()(irep.id()));
62 
63  packed.push_back(sub.size());
64  for(const auto &sub_irep : sub)
65  packed.push_back(number(sub_irep));
66 
67  packed.push_back(named_sub_size);
68  for(const auto &sub_irep : named_sub)
69  {
70  packed.push_back(irep_id_hash()(sub_irep.first)); // id
71  packed.push_back(number(sub_irep.second)); // sub-irep
72  }
73  }
74  else
75  {
76  const std::size_t non_comment_count =
78 
79  // we pack: the irep id, the sub size, the subs, the named-sub size, and
80  // each of the non-comment named subs with their ids
81  packed.reserve(1 + 1 + sub.size() + 1 + non_comment_count * 2);
82 
83  packed.push_back(irep_id_hash()(irep.id()));
84 
85  packed.push_back(sub.size());
86  for(const auto &sub_irep : sub)
87  packed.push_back(number(sub_irep));
88 
89  packed.push_back(non_comment_count);
90  for(const auto &sub_irep : named_sub)
91  if(!irept::is_comment(sub_irep.first))
92  {
93  packed.push_back(irep_id_hash()(sub_irep.first)); // id
94  packed.push_back(number(sub_irep.second)); // sub-irep
95  }
96  }
97 }
std::vector< std::size_t > packedt
numberingt< packedt, vector_hasht > numbering
void pack(const irept &irep, packedt &)
std::size_t number(const irept &irep)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
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:404
subt & get_sub()
Definition: irep.h:444
named_subt & get_named_sub()
Definition: irep.h:446
const irep_idt & id() const
Definition: irep.h:384
static bool is_comment(const irep_idt &name)
Definition: irep.h:456
const dt & read() const
Definition: irep.h:236
dstring_hash irep_id_hash
Definition: irep.h:38
irep hash functions
#define hash_combine(h1, h2)
Definition: irep_hash.h:121
IREP Hash Container.
std::size_t operator()(const packedt &p) const