CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
irep_hash_container.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Hashing IREPs
4
5Author: 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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:364
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:448
static bool is_comment(const irep_idt &name)
Definition irep.h:460
const irep_idt & id() const
Definition irep.h:388
named_subt & get_named_sub()
Definition irep.h:450
const dt & read() const
Definition irep.h:240
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