35 static inline bool named_subt_order(
36 const std::pair<irep_namet, irept> &a,
42 static inline irept::named_subt::const_iterator named_subt_lower_bound(
45 return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
48 static inline irept::named_subt::iterator named_subt_lower_bound(
51 return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
66 std::cout <<
"DETACH1: " <<
data <<
'\n';
74 std::cout <<
"ALLOCATED " <<
data <<
'\n';
77 else if(
data->ref_count>1)
83 std::cout <<
"ALLOCATED " <<
data <<
'\n';
93 std::cout <<
"DETACH2: " <<
data <<
'\n';
111 std::cout <<
"R: " << old_data <<
" " << old_data->
ref_count <<
'\n';
118 std::cout <<
"D: " <<
pretty() <<
'\n';
119 std::cout <<
"DELETING " << old_data->
data 120 <<
" " << old_data <<
'\n';
122 std::cout <<
"DEALLOCATING " << old_data <<
"\n";
129 std::cout <<
"DONE\n";
141 std::vector<dt *>
stack(1, old_data);
143 while(!
stack.empty())
160 for(named_subt::iterator
165 stack.push_back(it->second.data);
169 for(named_subt::iterator
174 stack.push_back(it->second.data);
183 stack.push_back(it->data);
218 named_subt::const_iterator it=named_subt_lower_bound(s, name);
227 named_subt::const_iterator it=s.find(name);
236 return it->second.id();
241 return get(name)==ID_1;
275 named_subt::iterator it=named_subt_lower_bound(s, name);
277 if(it!=s.end() && it->first==name)
290 named_subt::const_iterator it=named_subt_lower_bound(s, name);
296 named_subt::const_iterator it=s.
find(name);
311 named_subt::iterator it=named_subt_lower_bound(s, name);
315 it=s.insert(it, std::make_pair(name,
irept()));
329 named_subt::iterator it=named_subt_lower_bound(s, name);
333 it=s.insert(it, std::make_pair(name, irep));
339 std::pair<named_subt::iterator, bool> entry=
340 s.insert(std::make_pair(name, irep));
343 entry.first->second=irep;
345 return entry.first->second;
349 #ifdef IREP_HASH_STATS 350 unsigned long long irep_cmp_cnt=0;
351 unsigned long long irep_cmp_ne_cnt=0;
356 #ifdef IREP_HASH_STATS 364 if(
id()!=other.
id() ||
368 #ifdef IREP_HASH_STATS 396 if(i1_sub.size()!=i2_sub.size() ||
397 i1_named_sub.size()!=i2_named_sub.size() ||
398 i1_comments.size()!=i2_comments.size())
401 for(std::size_t i=0; i<i1_sub.size(); i++)
402 if(!i1_sub[i].
full_eq(i2_sub[i]))
406 irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
407 irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
409 for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
410 if(i1_it->first!=i2_it->first ||
411 !i1_it->second.full_eq(i2_it->second))
416 irept::named_subt::const_iterator i1_it=i1_comments.begin();
417 irept::named_subt::const_iterator i2_it=i2_comments.begin();
419 for(; i1_it!=i1_comments.end(); i1_it++, i2_it++)
420 if(i1_it->first!=i2_it->first ||
421 !i1_it->second.full_eq(i2_it->second))
439 if(X.sub.size()<Y.sub.size())
441 if(Y.sub.size()<X.sub.size())
445 irept::subt::const_iterator it1, it2;
447 for(it1=X.sub.begin(),
449 it1!=X.sub.end() && it2!=Y.sub.end();
459 INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
460 "Unequal lengths will return before this");
463 if(X.named_sub.size()<Y.named_sub.size())
465 if(Y.named_sub.size()<X.named_sub.size())
469 irept::named_subt::const_iterator it1, it2;
471 for(it1=X.named_sub.begin(),
472 it2=Y.named_sub.begin();
473 it1!=X.named_sub.end() && it2!=Y.named_sub.end();
477 if(it1->first<it2->first)
479 if(it2->first<it1->first)
482 if(
ordering(it1->second, it2->second))
484 if(
ordering(it2->second, it1->second))
488 INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
489 "Unequal lengths will return before this");
513 irept::subt::const_iterator it1, it2;
521 r=it1->compare(*it2);
527 "Unequal lengths will return before this");
538 irept::named_subt::const_iterator it1, it2;
546 r=it1->first.compare(it2->first);
550 r=it1->second.compare(it2->second);
557 "Unequal lengths will return before this");
570 #ifdef IREP_HASH_STATS 571 unsigned long long irep_hash_cnt=0;
577 if(
read().hash_code!=0)
578 return read().hash_code;
597 read().hash_code=result;
599 #ifdef IREP_HASH_STATS 629 named_sub.size()+sub.size()+comments.size());
636 for(
unsigned i=0; i<indent; i++)
642 if(max_indent>0 && indent>max_indent)
662 result+=it->second.pretty(indent+2, max_indent);
674 result+=it->second.pretty(indent+2, max_indent);
687 result+=it->pretty(indent+2, max_indent);
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
int compare(const irept &i) const
defines ordering on the internal representation
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
std::vector< irept > subt
void move_to_sub(irept &irep)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool full_eq(const irept &other) const
unsigned unsafe_string2unsigned(const std::string &str, int base)
signed int get_int(const irep_namet &name) const
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
unsignedbv_typet size_type()
bool get_bool(const irep_namet &name) const
#define POSTCONDITION(CONDITION)
#define forall_named_irep(it, irep)
irep_pretty_diagnosticst(const irept &irep)
const irep_idt & id() const
std::size_t unsafe_string2size_t(const std::string &str, int base)
static void indent_str(std::string &s, unsigned indent)
const irep_idt & get(const irep_namet &name) const
#define hash_finalize(h1, len)
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
#define PRECONDITION(CONDITION)
named_subt & get_comments()
Base class for tree-like data structures with sharing.
std::map< irep_namet, irept > named_subt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool operator<(const irept &other) const
defines ordering on the internal representation
static void remove_ref(dt *old_data)
named_subt & get_named_sub()
bool ordering(const irept &other) const
defines ordering on the internal representation
size_t hash_string(const dstringt &s)
static bool is_comment(const irep_namet &name)
irep_idt data
This irep_idt is the only place to store data in an irep, other than the mere nesting structure.
int compare(const dstringt &b) const
std::size_t full_hash() const
irept & add(const irep_namet &name)
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
unsigned int get_unsigned_int(const irep_namet &name) const
long long get_long_long(const irep_namet &name) const
#define hash_combine(h1, h2)
bool operator==(const irept &other) const
void remove(const irep_namet &name)
std::size_t get_size_t(const irep_namet &name) const
int unsafe_string2int(const std::string &str, int base)
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
void move_to_named_sub(const irep_namet &name, irept &irep)
#define forall_irep(it, irep)