Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_IREP_H
11 #define CPROVER_UTIL_IREP_H
25 #ifdef NAMED_SUB_IS_FORWARD_LIST
62 #define forall_irep(it, irep) \
63 for(irept::subt::const_iterator it=(irep).begin(); \
64 it!=(irep).end(); ++it)
66 #define Forall_irep(it, irep) \
67 for(irept::subt::iterator it=(irep).begin(); \
68 it!=(irep).end(); ++it)
70 #define forall_named_irep(it, irep) \
71 for(irept::named_subt::const_iterator it=(irep).begin(); \
72 it!=(irep).end(); ++it)
74 #define Forall_named_irep(it, irep) \
75 for(irept::named_subt::iterator it=(irep).begin(); \
76 it!=(irep).end(); ++it)
88 template <
bool enabled>
96 unsigned ref_count = 1;
118 template <
typename treet,
typename named_subtreest,
bool sharing = true>
123 typedef std::vector<treet>
subt;
169 :
data(std::move(_data)),
177 template <
typename derivedt,
typename named_subtreest>
193 :
data(new
dt(std::move(_id), std::move(_named_sub), std::move(_sub)))
210 std::cout <<
"COPY " <<
data <<
" " <<
data->ref_count <<
'\n';
221 std::cout <<
"COPY MOVE\n";
229 std::cout <<
"ASSIGN\n";
249 std::cout <<
"ASSIGN MOVE\n";
252 std::swap(
data, irep.data);
286 template <
typename derivedt,
typename named_subtreest>
291 template <
typename derivedt,
typename named_subtreest>
307 :
data(std::move(_id), std::move(_named_sub), std::move(_sub))
386 : public non_sharing_treet<
389 #ifdef NAMED_SUB_IS_FORWARD_LIST
390 forward_list_as_mapt<irep_namet, irept>>
392 std::map<irep_namet, irept>>
400 return id() == ID_nil;
404 return id() != ID_nil;
412 :
baset(_id, _named_sub, _sub)
448 add(name, std::move(irep));
460 return !(*
this==other);
482 std::size_t
hash()
const;
487 std::string
pretty(
unsigned indent=0,
unsigned max_indent=0)
const;
490 {
return !name.
empty() && name[0]==
'#'; }
538 template <
typename derivedt,
typename named_subtreest>
542 std::cout <<
"DETACH1: " <<
data <<
'\n';
550 std::cout <<
"ALLOCATED " <<
data <<
'\n';
553 else if(
data->ref_count > 1)
559 std::cout <<
"ALLOCATED " <<
data <<
'\n';
563 remove_ref(old_data);
569 std::cout <<
"DETACH2: " <<
data <<
'\n';
573 template <
typename derivedt,
typename named_subtreest>
576 if(old_data == &empty_d)
580 nonrecursive_destructor(old_data);
586 std::cout <<
"R: " << old_data <<
" " << old_data->
ref_count <<
'\n';
593 std::cout <<
"D: " << pretty() <<
'\n';
594 std::cout <<
"DELETING " << old_data->
data <<
" " << old_data <<
'\n';
596 std::cout <<
"DEALLOCATING " << old_data <<
"\n";
603 std::cout <<
"DONE\n";
611 template <
typename derivedt,
typename named_subtreest>
615 std::vector<dt *> stack(1, old_data);
617 while(!stack.empty())
619 dt *d = stack.back();
620 stack.erase(--stack.end());
633 for(
typename named_subt::iterator it = d->
named_sub.begin();
637 stack.push_back(it->second.data);
638 it->second.data = &empty_d;
641 for(
typename subt::iterator it = d->
sub.begin(); it != d->
sub.end(); it++)
643 stack.push_back(it->data);
653 #endif // CPROVER_UTIL_IREP_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::vector< treet > subt
static bool is_comment(const irep_namet &name)
static void remove_ref(dt *old_data)
signed int get_int(const irep_namet &name) const
void move_to_sub(irept &irep)
bool operator()(const irept &i1, const irept &i2) const
bool full_eq(const irept &other) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
sharing_treet tree_implementationt
Used to refer to this class from derived classes.
irept & add(const irep_namet &name)
irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, irept irep)
long long get_long_long(const irep_namet &name) const
typename dt::named_subt named_subt
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
sharing_treet(const sharing_treet &irep)
static std::size_t number_of_non_comments(const named_subt &)
count the number of named_sub elements that are not comments
bool get_bool(const irep_namet &name) const
Used in tree_nodet for activating or not reference counting.
void move_to_named_sub(const irep_namet &name, irept &irep)
non_sharing_treet(irep_idt _id)
std::size_t operator()(const irept &irep) const
const std::string & id2string(const irep_idt &d)
named_subt & get_named_sub()
std::size_t operator()(const irept &irep) const
void id(const irep_idt &_data)
tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
#define PRECONDITION(CONDITION)
bool operator!=(const irept &other) const
const std::string & id_string() const
const irept & get_nil_irep()
tree_nodet(irep_idt _data)
sharing_treet & operator=(const sharing_treet &irep)
sharing_treet(sharing_treet &&irep)
const irep_idt & id() const
const named_subt & get_named_sub() const
sharing_treet & operator=(sharing_treet &&irep)
void remove(const irep_namet &name)
Helper to give us some diagnostic in a usable form on assertion failure.
dstring_hash irep_id_hash
bool operator==(const irept &other) const
irept(const irep_idt &_id)
const std::string & get_string(const irep_namet &name) const
Base class for tree-like data structures without sharing.
sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
#define POSTCONDITION(CONDITION)
bool ordering(const irept &other) const
defines ordering on the internal representation
std::size_t get_size_t(const irep_namet &name) const
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const subt & get_sub() const
sharing_treet(irep_idt _id)
A node with data in a tree, it contains:
const std::string & name2string(const irep_namet &n)
std::string as_string(resultt result)
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
named_subtreest named_subt
There are a large number of kinds of tree structured or tree-like data in CPROVER.
irep_pretty_diagnosticst(const irept &irep)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
irep_idt data
This irep_idt is the only place to store data in an tree node.
bool operator<(const irept &other) const
defines ordering on the internal representation
non_sharing_treet()=default
typename dt::named_subt named_subt
non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
Base class for tree-like data structures with sharing.
std::size_t full_hash() const