cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
merge_irep.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#include "
merge_irep.h
"
10
11
#include "
irep_hash.h
"
12
13
std::size_t
to_be_merged_irept::hash
()
const
14
{
15
std::size_t result=
hash_string
(
id
());
16
17
const
irept::subt
&sub=
get_sub
();
18
const
irept::named_subt
&named_sub=
get_named_sub
();
19
20
for
(
const
auto
&irep : sub)
21
{
22
result =
23
hash_combine
(result,
static_cast<
const
merged_irept
&
>
(irep).
hash
());
24
}
25
26
for
(
const
auto
&irep_entry : named_sub)
27
{
28
result =
hash_combine
(result,
hash_string
(irep_entry.first));
29
result =
hash_combine
(
30
result,
static_cast<
const
merged_irept
&
>
(irep_entry.second).
hash
());
31
}
32
33
const
std::size_t named_sub_size = named_sub.size();
34
result =
hash_finalize
(result, named_sub_size + sub.size());
35
36
return
result;
37
}
38
39
bool
to_be_merged_irept::operator ==
(
const
to_be_merged_irept
&other)
const
40
{
41
if
(
id
()!=other.
id
())
42
return
false
;
43
44
const
irept::subt
&sub=
get_sub
();
45
const
irept::subt
&o_sub=other.
get_sub
();
46
const
irept::named_subt
&named_sub=
get_named_sub
();
47
const
irept::named_subt
&o_named_sub=other.
get_named_sub
();
48
49
if
(sub.size()!=o_sub.size())
50
return
false
;
51
#if NAMED_SUB_IS_FORWARD_LIST
52
if
(
53
std::distance(named_sub.begin(), named_sub.end()) !=
54
std::distance(o_named_sub.begin(), o_named_sub.end()))
55
{
56
return
false
;
57
}
58
#else
59
if
(named_sub.size()!=o_named_sub.size())
60
return
false
;
61
#endif
62
63
{
64
irept::subt::const_iterator s_it=sub.begin();
65
irept::subt::const_iterator os_it=o_sub.begin();
66
67
for
(; s_it!=sub.end(); s_it++, os_it++)
68
if
(
static_cast<
const
merged_irept
&
>
(*s_it)!=
69
static_cast<
const
merged_irept
&
>
(*os_it))
70
return
false
;
71
}
72
73
{
74
irept::named_subt::const_iterator s_it=named_sub.begin();
75
irept::named_subt::const_iterator os_it=o_named_sub.begin();
76
77
for
(; s_it!=named_sub.end(); s_it++, os_it++)
78
if
(s_it->first!=os_it->first ||
79
static_cast<
const
merged_irept
&
>
(s_it->second)!=
80
static_cast<
const
merged_irept
&
>
(os_it->second))
81
return
false
;
82
}
83
84
return
true
;
85
}
86
87
const
merged_irept
&
merged_irepst::merged
(
const
irept
&irep)
88
{
89
// first see if it's already a merged_irep
90
91
merged_irep_storet::const_iterator entry=
92
merged_irep_store
.find(
merged_irept
(irep));
93
94
if
(entry!=
merged_irep_store
.end())
95
return
*entry;
// nothing to do
96
97
// need to build new irep that will be in the container
98
irept
new_irep(irep.
id
());
99
100
const
irept::subt
&src_sub=irep.
get_sub
();
101
irept::subt
&dest_sub=new_irep.
get_sub
();
102
dest_sub.reserve(src_sub.size());
103
104
for
(
const
auto
&sub_irep : src_sub)
105
dest_sub.push_back(
merged
(sub_irep));
// recursive call
106
107
const
irept::named_subt
&src_named_sub=irep.
get_named_sub
();
108
irept::named_subt
&dest_named_sub=new_irep.
get_named_sub
();
109
110
#if NAMED_SUB_IS_FORWARD_LIST
111
irept::named_subt::iterator before = dest_named_sub.before_begin();
112
#endif
113
for
(
const
auto
&irep_entry : src_named_sub)
114
{
115
#if NAMED_SUB_IS_FORWARD_LIST
116
dest_named_sub.emplace_after(
117
before, irep_entry.first,
merged
(irep_entry.second));
// recursive call
118
++before;
119
#else
120
dest_named_sub[irep_entry.first] =
121
merged
(irep_entry.second);
// recursive call
122
#endif
123
}
124
125
std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
126
to_be_merged_irep_store
.insert(
to_be_merged_irept
(new_irep));
127
128
if
(result.second)
// really new, record
129
merged_irep_store
.insert(
merged_irept
(new_irep));
130
131
return
132
static_cast<
const
merged_irept
&
>
(
133
static_cast<
const
irept
&
>
(*result.first));
134
}
135
136
void
merge_irept::operator()
(
irept
&irep)
137
{
138
// only useful if there is sharing
139
#ifdef SHARING
140
irep=
merged
(irep);
141
#endif
142
}
143
144
const
irept
&
merge_irept::merged
(
const
irept
&irep)
145
{
146
auto
entry =
irep_store
.insert(irep);
147
if
(!entry.second)
148
return
*entry.first;
149
150
const
irept::subt
&src_sub=irep.
get_sub
();
151
irept::subt
*dest_sub_ptr =
nullptr
;
152
153
std::size_t index = 0;
154
for
(
const
auto
&sub_irep : src_sub)
155
{
156
const
irept
&op =
merged
(sub_irep);
// recursive call
157
if
(&op.
read
() != &(sub_irep.read()))
158
{
159
if
(!dest_sub_ptr)
160
dest_sub_ptr = &(
const_cast<
irept
&
>
(*entry.first)).get_sub();
161
(*dest_sub_ptr)[index] = op;
162
}
163
++index;
164
}
165
166
const
irept::named_subt
&src_named_sub=irep.
get_named_sub
();
167
irept::named_subt
*dest_named_sub_ptr =
nullptr
;
168
169
std::ptrdiff_t advance_by = 0;
170
for
(
const
auto
&irep_entry : src_named_sub)
171
{
172
if
(!
irept::is_comment
(irep_entry.first))
173
{
174
const
irept
&op =
merged
(irep_entry.second);
// recursive call
175
if
(&op.
read
() != &(irep_entry.second.read()))
176
{
177
if
(!dest_named_sub_ptr)
178
dest_named_sub_ptr =
179
&(
const_cast<
irept
&
>
(*entry.first)).get_named_sub();
180
std::next(dest_named_sub_ptr->begin(), advance_by)->second = op;
181
}
182
}
183
++advance_by;
184
}
185
186
return
*entry.first;
187
}
188
189
void
merge_full_irept::operator()
(
irept
&irep)
190
{
191
// only useful if there is sharing
192
#ifdef SHARING
193
irep=
merged
(irep);
194
#endif
195
}
196
197
const
irept
&
merge_full_irept::merged
(
const
irept
&irep)
198
{
199
irep_storet::const_iterator entry=
irep_store
.find(irep);
200
if
(entry!=
irep_store
.end())
201
return
*entry;
202
203
irept
new_irep(irep.
id
());
204
205
const
irept::subt
&src_sub=irep.
get_sub
();
206
irept::subt
&dest_sub=new_irep.
get_sub
();
207
dest_sub.reserve(src_sub.size());
208
209
for
(
const
auto
&sub_irep : src_sub)
210
dest_sub.push_back(
merged
(sub_irep));
// recursive call
211
212
const
irept::named_subt
&src_named_sub=irep.
get_named_sub
();
213
irept::named_subt
&dest_named_sub=new_irep.
get_named_sub
();
214
215
#if NAMED_SUB_IS_FORWARD_LIST
216
irept::named_subt::iterator before = dest_named_sub.before_begin();
217
#endif
218
for
(
const
auto
&irep_entry : src_named_sub)
219
{
220
#if NAMED_SUB_IS_FORWARD_LIST
221
dest_named_sub.emplace_after(
222
before, irep_entry.first,
merged
(irep_entry.second));
// recursive call
223
++before;
224
#else
225
dest_named_sub[irep_entry.first] =
226
merged
(irep_entry.second);
// recursive call
227
#endif
228
}
229
230
return
*
irep_store
.insert(std::move(new_irep)).first;
231
}
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
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
merge_full_irept::irep_store
irep_storet irep_store
Definition
merge_irep.h:124
merge_full_irept::merged
const irept & merged(const irept &irep)
Definition
merge_irep.cpp:197
merge_full_irept::operator()
void operator()(irept &)
Definition
merge_irep.cpp:189
merge_irept::merged
const irept & merged(const irept &irep)
Definition
merge_irep.cpp:144
merge_irept::operator()
void operator()(irept &)
Definition
merge_irep.cpp:136
merge_irept::irep_store
irep_storet irep_store
Definition
merge_irep.h:112
merged_irepst::to_be_merged_irep_store
to_be_merged_irep_storet to_be_merged_irep_store
Definition
merge_irep.h:96
merged_irepst::merged
const merged_irept & merged(const irept &)
Definition
merge_irep.cpp:87
merged_irepst::merged_irep_store
merged_irep_storet merged_irep_store
Definition
merge_irep.h:92
merged_irept
Definition
merge_irep.h:18
merged_irept::hash
std::size_t hash() const
Definition
merge_irep.h:33
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
to_be_merged_irept
Definition
merge_irep.h:61
to_be_merged_irept::hash
std::size_t hash() const
Definition
merge_irep.cpp:13
to_be_merged_irept::to_be_merged_irept
to_be_merged_irept(const irept &src)
Definition
merge_irep.h:68
to_be_merged_irept::operator==
bool operator==(const to_be_merged_irept &other) const
Definition
merge_irep.cpp:39
hash_string
size_t hash_string(const dstringt &s)
Definition
dstring.h:228
irep_hash.h
irep hash functions
hash_finalize
#define hash_finalize(h1, len)
Definition
irep_hash.h:123
hash_combine
#define hash_combine(h1, h2)
Definition
irep_hash.h:121
merge_irep.h
util
merge_irep.cpp
Generated by
1.17.0