CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
merge_irep.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_MERGE_IREP_H
11#define CPROVER_UTIL_MERGE_IREP_H
12
13#include <unordered_set>
14
15#include "irep.h"
16
17class merged_irept:public irept
18{
19public:
20 bool operator==(const merged_irept &other) const
21 {
22 // We assume that both are in the same container,
23 // which isn't checked.
24 return &read()==&other.read();
25 }
26
27 bool operator<(const merged_irept &other) const
28 {
29 // again, assumes that both are in the same container
30 return &read()<&other.read();
31 }
32
33 std::size_t hash() const
34 {
35 return reinterpret_cast<std::size_t>(&read());
36 }
37
38 // copy constructor: will only copy from other merged_irepts
42
43protected:
44 // more general one can only be used by merged_irepst
45 explicit merged_irept(const irept &src):irept(src)
46 {
47 }
48
49 friend class merged_irepst;
50};
51
52// NOLINTNEXTLINE(readability/identifiers)
54{
55 std::size_t operator()(const merged_irept &irep) const
56 { return irep.hash(); }
57};
58
59// internal, don't use me
61{
62public:
63 bool operator==(const to_be_merged_irept &other) const;
64 std::size_t hash() const;
65
66protected:
67 // can only be used by merged_irepst
68 explicit to_be_merged_irept(const irept &src):irept(src)
69 {
70 }
71
72 friend class merged_irepst;
73};
74
75// NOLINTNEXTLINE(readability/identifiers)
77{
78 std::size_t operator()(const to_be_merged_irept &irep) const
79 { return irep.hash(); }
80};
81
83{
84public:
85 const merged_irept &operator()(const irept &src)
86 {
87 return merged(src);
88 }
89
90protected:
91 typedef std::unordered_set<merged_irept, merged_irep_hash> merged_irep_storet;
93
94 typedef std::unordered_set<to_be_merged_irept, to_be_merged_irep_hash>
97
98 const merged_irept &merged(const irept &);
99};
100
101// Warning: the below uses irep_hash, as opposed to irep_full_hash,
102// i.e., any comments will be disregarded during merging. Use
103// merge_full_irept if any comments are of importance.
104
106{
107public:
108 void operator()(irept &);
109
110protected:
111 typedef std::unordered_set<irept, irep_hash> irep_storet;
113
114 const irept &merged(const irept &irep);
115};
116
118{
119public:
120 void operator()(irept &);
121
122protected:
123 typedef std::unordered_set<irept, irep_full_hash, irep_full_eq> irep_storet;
125
126 const irept &merged(const irept &irep);
127};
128
129#endif // CPROVER_UTIL_MERGE_IREP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
std::unordered_set< irept, irep_full_hash, irep_full_eq > irep_storet
Definition merge_irep.h:123
irep_storet irep_store
Definition merge_irep.h:124
const irept & merged(const irept &irep)
void operator()(irept &)
const irept & merged(const irept &irep)
std::unordered_set< irept, irep_hash > irep_storet
Definition merge_irep.h:111
void operator()(irept &)
irep_storet irep_store
Definition merge_irep.h:112
const merged_irept & operator()(const irept &src)
Definition merge_irep.h:85
std::unordered_set< merged_irept, merged_irep_hash > merged_irep_storet
Definition merge_irep.h:91
to_be_merged_irep_storet to_be_merged_irep_store
Definition merge_irep.h:96
const merged_irept & merged(const irept &)
std::unordered_set< to_be_merged_irept, to_be_merged_irep_hash > to_be_merged_irep_storet
Definition merge_irep.h:95
merged_irep_storet merged_irep_store
Definition merge_irep.h:92
merged_irept(const irept &src)
Definition merge_irep.h:45
merged_irept(const merged_irept &_src)
Definition merge_irep.h:39
bool operator<(const merged_irept &other) const
Definition merge_irep.h:27
std::size_t hash() const
Definition merge_irep.h:33
bool operator==(const merged_irept &other) const
Definition merge_irep.h:20
std::size_t hash() const
to_be_merged_irept(const irept &src)
Definition merge_irep.h:68
bool operator==(const to_be_merged_irept &other) const
std::size_t operator()(const merged_irept &irep) const
Definition merge_irep.h:55
std::size_t operator()(const to_be_merged_irept &irep) const
Definition merge_irep.h:78