36 static inline bool named_subt_order(
37 const std::pair<irep_namet, irept> &a,
43 static inline irept::named_subt::const_iterator named_subt_lower_bound(
46 return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
49 static inline irept::named_subt::iterator named_subt_lower_bound(
52 return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
67 std::cout <<
"DETACH1: " <<
data <<
'\n';
75 std::cout <<
"ALLOCATED " <<
data <<
'\n';
78 else if(
data->ref_count>1)
84 std::cout <<
"ALLOCATED " <<
data <<
'\n';
94 std::cout <<
"DETACH2: " <<
data <<
'\n';
112 std::cout <<
"R: " << old_data <<
" " << old_data->
ref_count <<
'\n';
119 std::cout <<
"D: " <<
pretty() <<
'\n';
120 std::cout <<
"DELETING " << old_data->
data 121 <<
" " << old_data <<
'\n';
123 std::cout <<
"DEALLOCATING " << old_data <<
"\n";
130 std::cout <<
"DONE\n";
142 std::vector<dt *>
stack(1, old_data);
144 while(!
stack.empty())
161 for(named_subt::iterator
166 stack.push_back(it->second.data);
170 for(named_subt::iterator
175 stack.push_back(it->second.data);
184 stack.push_back(it->data);
219 named_subt::const_iterator it=named_subt_lower_bound(s, name);
228 named_subt::const_iterator it=s.find(name);
237 return it->second.id();
242 return get(name)==ID_1;
276 named_subt::iterator it=named_subt_lower_bound(s, name);
278 if(it!=s.end() && it->first==name)
291 named_subt::const_iterator it=named_subt_lower_bound(s, name);
297 named_subt::const_iterator it=s.
find(name);
312 named_subt::iterator it=named_subt_lower_bound(s, name);
316 it=s.insert(it, std::make_pair(name,
irept()));
330 named_subt::iterator it=named_subt_lower_bound(s, name);
334 it=s.insert(it, std::make_pair(name, irep));
340 std::pair<named_subt::iterator, bool> entry=
341 s.insert(std::make_pair(name, irep));
344 entry.first->second=irep;
346 return entry.first->second;
350 #ifdef IREP_HASH_STATS 351 unsigned long long irep_cmp_cnt=0;
352 unsigned long long irep_cmp_ne_cnt=0;
357 #ifdef IREP_HASH_STATS 365 if(
id()!=other.
id() ||
369 #ifdef IREP_HASH_STATS 397 if(i1_sub.size()!=i2_sub.size() ||
398 i1_named_sub.size()!=i2_named_sub.size() ||
399 i1_comments.size()!=i2_comments.size())
402 for(std::size_t i=0; i<i1_sub.size(); i++)
403 if(!i1_sub[i].
full_eq(i2_sub[i]))
407 irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
408 irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
410 for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
411 if(i1_it->first!=i2_it->first ||
412 !i1_it->second.full_eq(i2_it->second))
417 irept::named_subt::const_iterator i1_it=i1_comments.begin();
418 irept::named_subt::const_iterator i2_it=i2_comments.begin();
420 for(; i1_it!=i1_comments.end(); i1_it++, i2_it++)
421 if(i1_it->first!=i2_it->first ||
422 !i1_it->second.full_eq(i2_it->second))
440 if(X.sub.size()<Y.sub.size())
442 if(Y.sub.size()<X.sub.size())
446 irept::subt::const_iterator it1, it2;
448 for(it1=X.sub.begin(),
450 it1!=X.sub.end() && it2!=Y.sub.end();
460 INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
461 "Unequal lengths will return before this");
464 if(X.named_sub.size()<Y.named_sub.size())
466 if(Y.named_sub.size()<X.named_sub.size())
470 irept::named_subt::const_iterator it1, it2;
472 for(it1=X.named_sub.begin(),
473 it2=Y.named_sub.begin();
474 it1!=X.named_sub.end() && it2!=Y.named_sub.end();
478 if(it1->first<it2->first)
480 if(it2->first<it1->first)
483 if(
ordering(it1->second, it2->second))
485 if(
ordering(it2->second, it1->second))
489 INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
490 "Unequal lengths will return before this");
514 irept::subt::const_iterator it1, it2;
522 r=it1->compare(*it2);
528 "Unequal lengths will return before this");
539 irept::named_subt::const_iterator it1, it2;
547 r=it1->first.compare(it2->first);
551 r=it1->second.compare(it2->second);
558 "Unequal lengths will return before this");
571 #ifdef IREP_HASH_STATS 572 unsigned long long irep_hash_cnt=0;
578 if(
read().hash_code!=0)
579 return read().hash_code;
598 read().hash_code=result;
600 #ifdef IREP_HASH_STATS 630 named_sub.size()+sub.size()+comments.size());
637 for(
unsigned i=0; i<indent; i++)
643 if(max_indent>0 && indent>max_indent)
663 result+=it->second.pretty(indent+2, max_indent);
675 result+=it->second.pretty(indent+2, max_indent);
688 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)
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)
#define INVARIANT(CONDITION, REASON)
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)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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)