cprover
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  auto &irep_entry = ptr_hash[&irep.read()];
31  irep_entry.number = id;
32  irep_entry.irep = irep;
33 
34  return id;
35 }
36 
38  const packedt &p) const
39 {
40  size_t result=p.size(); // seed
41  for(auto elem : p)
42  result=hash_combine(result, elem);
43  return result;
44 }
45 
47  const irept &irep,
48  packedt &packed)
49 {
50  const irept::subt &sub=irep.get_sub();
51  const irept::named_subt &named_sub=irep.get_named_sub();
52  const irept::named_subt &comments=irep.get_comments();
53 
54  packed.reserve(
55  1+1+sub.size()+named_sub.size()*2+
56  (full?comments.size()*2:0));
57 
58  packed.push_back(irep_id_hash()(irep.id()));
59 
60  packed.push_back(sub.size());
61  forall_irep(it, sub)
62  packed.push_back(number(*it));
63 
64  packed.push_back(named_sub.size());
65  forall_named_irep(it, named_sub)
66  {
67  packed.push_back(irep_id_hash()(it->first)); // id
68  packed.push_back(number(it->second)); // sub-irep
69  }
70 
71  if(full)
72  {
73  packed.push_back(comments.size());
74  forall_named_irep(it, comments)
75  {
76  packed.push_back(irep_id_hash()(it->first)); // id
77  packed.push_back(number(it->second)); // sub-irep
78  }
79  }
80 }
irep_hash_container_baset::pack
void pack(const irept &irep, packedt &)
Definition: irep_hash_container.cpp:46
irep_hash_container_baset::packedt
std::vector< std::size_t > packedt
Definition: irep_hash_container.h:60
irept::named_subt
std::map< irep_namet, irept > named_subt
Definition: irep.h:169
template_numberingt
Definition: numbering.h:21
irep_hash_container_baset::vector_hasht::operator()
std::size_t operator()(const packedt &p) const
Definition: irep_hash_container.cpp:37
irep_hash_container.h
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
irept::read
const dt & read() const
Definition: irep.h:406
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:319
forall_named_irep
#define forall_named_irep(it, irep)
Definition: irep.h:70
hash_combine
#define hash_combine(h1, h2)
Definition: irep_hash.h:120
irept::id
const irep_idt & id() const
Definition: irep.h:259
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:35
forall_irep
#define forall_irep(it, irep)
Definition: irep.h:62
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:317
irep_hash_container_baset::full
bool full
Definition: irep_hash_container.h:72
irep_hash.h
irept::get_comments
named_subt & get_comments()
Definition: irep.h:321
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
irept::subt
std::vector< irept > subt
Definition: irep.h:160
irep.h
irep_hash_container_baset::ptr_hash
ptr_hasht ptr_hash
Definition: irep_hash_container.h:56