cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
17
size_t
irep_hash_container_baset::number
(
const
irept
&irep)
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
38
size_t
irep_hash_container_baset::vector_hasht::operator()
(
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
47
void
irep_hash_container_baset::pack
(
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 =
77
irept::number_of_non_comments
(named_sub);
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
}
irep_hash_container_baset::packedt
std::vector< std::size_t > packedt
Definition
irep_hash_container.h:66
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::number
std::size_t number(const irept &irep)
Definition
irep_hash_container.cpp:17
irep_hash_container_baset::full
bool full
Definition
irep_hash_container.h:77
irep_hash_container_baset::ptr_hash
ptr_hasht ptr_hash
Definition
irep_hash_container.h:62
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
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:404
irept::get_sub
subt & get_sub()
Definition
irep.h:448
irept::is_comment
static bool is_comment(const irep_idt &name)
Definition
irep.h:460
irept::id
const irep_idt & id() const
Definition
irep.h:388
irept::get_named_sub
named_subt & get_named_sub()
Definition
irep.h:450
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::named_subt
typename dt::named_subt named_subt
Definition
irep.h:153
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition
irep.h:152
sharing_treet::read
const dt & read() const
Definition
irep.h:240
irep.h
irep_id_hash
dstring_hash irep_id_hash
Definition
irep.h:38
irep_hash.h
irep hash functions
hash_combine
#define hash_combine(h1, h2)
Definition
irep_hash.h:121
irep_hash_container.h
IREP Hash Container.
irep_hash_container_baset::vector_hasht::operator()
std::size_t operator()(const packedt &p) const
Definition
irep_hash_container.cpp:38
util
irep_hash_container.cpp
Generated by
1.17.0