48 named_subt::const_iterator it=s.find(name);
55 return it->second.id();
60 return get(name)==ID_1;
98 #if NAMED_SUB_IS_FORWARD_LIST
109 auto it = s.find(name);
126 #if NAMED_SUB_IS_FORWARD_LIST
127 return s.add(name, std::move(irep));
129 std::pair<named_subt::iterator, bool> entry = s.emplace(
130 std::piecewise_construct,
131 std::forward_as_tuple(name),
132 std::forward_as_tuple(irep));
135 entry.first->second = std::move(irep);
137 return entry.first->second;
141 #ifdef IREP_HASH_STATS
142 unsigned long long irep_cmp_cnt=0;
143 unsigned long long irep_cmp_ne_cnt=0;
148 #ifdef IREP_HASH_STATS
158 #ifdef IREP_HASH_STATS
168 named_subt::const_iterator this_it = this_named_sub.begin();
169 named_subt::const_iterator other_it = other_named_sub.begin();
171 while(this_it != this_named_sub.end() || other_it != other_named_sub.end())
173 if(this_it != this_named_sub.end() &&
is_comment(this_it->first))
179 if(other_it != other_named_sub.end() &&
is_comment(other_it->first))
186 this_it == this_named_sub.end() ||
187 other_it == other_named_sub.end() ||
188 this_it->first != other_it->first ||
189 this_it->second != other_it->second)
191 #ifdef IREP_HASH_STATS
218 if(i1_sub.size() != i2_sub.size())
224 if(i1_named_sub.size() != i2_named_sub.size())
227 for(std::size_t i=0; i<i1_sub.size(); i++)
228 if(!i1_sub[i].
full_eq(i2_sub[i]))
232 irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
233 irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
235 for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
236 if(i1_it->first!=i2_it->first ||
237 !i1_it->second.full_eq(i2_it->second))
255 if(X.sub.size()<Y.sub.size())
257 if(Y.sub.size()<X.sub.size())
261 irept::subt::const_iterator it1, it2;
263 for(it1=X.sub.begin(),
265 it1!=X.sub.end() && it2!=Y.sub.end();
275 INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
276 "Unequal lengths will return before this");
279 if(X.named_sub.size()<Y.named_sub.size())
281 if(Y.named_sub.size()<X.named_sub.size())
285 irept::named_subt::const_iterator it1, it2;
287 for(it1=X.named_sub.begin(),
288 it2=Y.named_sub.begin();
289 it1!=X.named_sub.end() && it2!=Y.named_sub.end();
293 if(it1->first<it2->first)
295 if(it2->first<it1->first)
298 if(
ordering(it1->second, it2->second))
300 if(
ordering(it2->second, it1->second))
304 INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
305 "Unequal lengths will return before this");
331 irept::subt::const_iterator it1, it2;
339 r=it1->compare(*it2);
345 "Unequal lengths will return before this");
357 irept::named_subt::const_iterator it1, it2;
384 it2 != i.
get_named_sub().end(),
"not at end of i.get_named_sub()");
386 r=it1->first.compare(it2->first);
390 r=it1->second.compare(it2->second);
400 "Unequal number of non-comments will return before this");
413 #ifdef IREP_HASH_STATS
414 unsigned long long irep_hash_cnt=0;
419 std::size_t result = 0;
421 for(
const auto &n : named_sub)
431 if(
read().hash_code!=0)
440 for(
const auto &irep : sub)
443 std::size_t number_of_named_ireps = 0;
445 for(
const auto &irep_entry : named_sub)
450 result =
hash_combine(result, irep_entry.second.hash());
451 number_of_named_ireps++;
455 result =
hash_finalize(result, sub.size() + number_of_named_ireps);
460 #ifdef IREP_HASH_STATS
473 for(
const auto &irep : sub)
477 for(
const auto &irep_entry : named_sub)
480 result =
hash_combine(result, irep_entry.second.full_hash());
483 const std::size_t named_sub_size = named_sub.size();
491 for(
unsigned i=0; i<indent; i++)
497 if(max_indent>0 && indent>max_indent)
517 result += irep_entry.second.pretty(indent + 2, max_indent);
522 for(
const auto &irep :
get_sub())
530 result += irep.pretty(indent + 2, max_indent);
unsignedbv_typet size_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
int compare(const dstringt &b) const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
static std::size_t number_of_non_comments(const named_subt &)
count the number of named_sub elements that are not comments
bool operator==(const irept &other) const
irept & add(const irep_namet &name)
std::size_t get_size_t(const irep_namet &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_namet &name, const irep_idt &value)
void move_to_named_sub(const irep_namet &name, irept &irep)
const std::string & get_string(const irep_namet &name) const
void set_size_t(const irep_namet &name, const std::size_t value)
bool get_bool(const irep_namet &name) const
bool ordering(const irept &other) const
defines ordering on the internal representation
named_subt & get_named_sub()
static bool is_comment(const irep_namet &name)
const irept & find(const irep_namet &name) const
const std::string & id_string() const
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
bool operator<(const irept &other) const
defines ordering on the internal representation
const irep_idt & id() const
bool full_eq(const irept &other) const
std::size_t full_hash() const
long long get_long_long(const irep_namet &name) const
void move_to_sub(irept &irep)
void remove(const irep_namet &name)
signed int get_int(const irep_namet &name) const
const irep_idt & get(const irep_namet &name) const
typename dt::named_subt named_subt
size_t hash_string(const dstringt &s)
static std::enable_if< std::is_integral< T >::value, dstringt >::type to_dstring(T value)
equivalent to dstringt(std::to_string(value)), i.e., produces a string from a number
static void indent_str(std::string &s, unsigned indent)
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
#define hash_finalize(h1, len)
#define hash_combine(h1, h2)
std::size_t unsafe_string2size_t(const std::string &str, int base)
int unsafe_string2int(const std::string &str, int base)
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
irep_pretty_diagnosticst(const irept &irep)