20 for(
const auto &irep : sub)
26 for(
const auto &irep_entry : named_sub)
33 const std::size_t named_sub_size = named_sub.size();
49 if(sub.size()!=o_sub.size())
51 #if NAMED_SUB_IS_FORWARD_LIST
53 std::distance(named_sub.begin(), named_sub.end()) !=
54 std::distance(o_named_sub.begin(), o_named_sub.end()))
59 if(named_sub.size()!=o_named_sub.size())
64 irept::subt::const_iterator s_it=sub.begin();
65 irept::subt::const_iterator os_it=o_sub.begin();
67 for(; s_it!=sub.end(); s_it++, os_it++)
74 irept::named_subt::const_iterator s_it=named_sub.begin();
75 irept::named_subt::const_iterator os_it=o_named_sub.begin();
77 for(; s_it!=named_sub.end(); s_it++, os_it++)
78 if(s_it->first!=os_it->first ||
91 merged_irep_storet::const_iterator entry=
102 dest_sub.reserve(src_sub.size());
104 for(
const auto &sub_irep : src_sub)
105 dest_sub.push_back(
merged(sub_irep));
110 #if NAMED_SUB_IS_FORWARD_LIST
111 irept::named_subt::iterator before = dest_named_sub.before_begin();
113 for(
const auto &irep_entry : src_named_sub)
115 #if NAMED_SUB_IS_FORWARD_LIST
116 dest_named_sub.emplace_after(
117 before, irep_entry.first,
merged(irep_entry.second));
120 dest_named_sub[irep_entry.first] =
121 merged(irep_entry.second);
125 std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
133 static_cast<const irept &
>(*result.first));
153 std::size_t index = 0;
154 for(
const auto &sub_irep : src_sub)
157 if(&op.
read() != &(sub_irep.read()))
160 dest_sub_ptr = &(
const_cast<irept &
>(*entry.first)).get_sub();
161 (*dest_sub_ptr)[index] = op;
169 std::ptrdiff_t advance_by = 0;
170 for(
const auto &irep_entry : src_named_sub)
175 if(&op.
read() != &(irep_entry.second.read()))
177 if(!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;
199 irep_storet::const_iterator entry=
irep_store.find(irep);
207 dest_sub.reserve(src_sub.size());
209 for(
const auto &sub_irep : src_sub)
210 dest_sub.push_back(
merged(sub_irep));
215 #if NAMED_SUB_IS_FORWARD_LIST
216 irept::named_subt::iterator before = dest_named_sub.before_begin();
218 for(
const auto &irep_entry : src_named_sub)
220 #if NAMED_SUB_IS_FORWARD_LIST
221 dest_named_sub.emplace_after(
222 before, irep_entry.first,
merged(irep_entry.second));
225 dest_named_sub[irep_entry.first] =
226 merged(irep_entry.second);
230 return *
irep_store.insert(std::move(new_irep)).first;
There are a large number of kinds of tree structured or tree-like data in CPROVER.
named_subt & get_named_sub()
const irep_idt & id() const
static bool is_comment(const irep_idt &name)
const irept & merged(const irept &irep)
const irept & merged(const irept &irep)
to_be_merged_irep_storet to_be_merged_irep_store
const merged_irept & merged(const irept &)
merged_irep_storet merged_irep_store
typename dt::named_subt named_subt
bool operator==(const to_be_merged_irept &other) const
size_t hash_string(const dstringt &s)
#define hash_finalize(h1, len)
#define hash_combine(h1, h2)