Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_IREP_H
11 #define CPROVER_UTIL_IREP_H
26 #if !defined(NAMED_SUB_IS_FORWARD_LIST) && !defined(_GLIBCXX_DEBUG)
27 # define NAMED_SUB_IS_FORWARD_LIST 1
30 #if NAMED_SUB_IS_FORWARD_LIST
77 template <
bool enabled>
85 unsigned ref_count = 1;
107 template <
typename treet,
typename named_subtreest,
bool sharing = true>
112 typedef std::vector<treet>
subt;
158 :
data(std::move(_data)),
166 template <
typename derivedt,
typename named_subtreest>
182 :
data(new
dt(std::move(_id), std::move(_named_sub), std::move(_sub)))
199 std::cout <<
"COPY " <<
data <<
" " <<
data->ref_count <<
'\n';
210 std::cout <<
"COPY MOVE\n";
218 std::cout <<
"ASSIGN\n";
238 std::cout <<
"ASSIGN MOVE\n";
241 std::swap(
data, irep.data);
275 template <
typename derivedt,
typename named_subtreest>
280 template <
typename derivedt,
typename named_subtreest>
296 :
data(std::move(_id), std::move(_named_sub), std::move(_sub))
375 : public non_sharing_treet<
378 #if NAMED_SUB_IS_FORWARD_LIST
379 forward_list_as_mapt<irep_namet, irept>>
381 std::map<irep_namet, irept>>
389 return id() == ID_nil;
393 return id() != ID_nil;
401 :
baset(_id, _named_sub, _sub)
437 add(name, std::move(irep));
450 return !(*
this==other);
472 std::size_t
hash()
const;
477 std::string
pretty(
unsigned indent=0,
unsigned max_indent=0)
const;
480 {
return !name.
empty() && name[0]==
'#'; }
528 template <
typename derivedt,
typename named_subtreest>
532 std::cout <<
"DETACH1: " <<
data <<
'\n';
540 std::cout <<
"ALLOCATED " <<
data <<
'\n';
543 else if(
data->ref_count > 1)
549 std::cout <<
"ALLOCATED " <<
data <<
'\n';
553 remove_ref(old_data);
559 std::cout <<
"DETACH2: " <<
data <<
'\n';
563 template <
typename derivedt,
typename named_subtreest>
566 if(old_data == &empty_d)
570 nonrecursive_destructor(old_data);
576 std::cout <<
"R: " << old_data <<
" " << old_data->
ref_count <<
'\n';
583 std::cout <<
"D: " << pretty() <<
'\n';
584 std::cout <<
"DELETING " << old_data->
data <<
" " << old_data <<
'\n';
586 std::cout <<
"DEALLOCATING " << old_data <<
"\n";
593 std::cout <<
"DONE\n";
601 template <
typename derivedt,
typename named_subtreest>
605 std::vector<dt *> stack(1, old_data);
607 while(!stack.empty())
609 dt *d = stack.back();
610 stack.erase(--stack.end());
623 for(
typename named_subt::iterator it = d->
named_sub.begin();
627 stack.push_back(it->second.data);
628 it->second.data = &empty_d;
631 for(
typename subt::iterator it = d->
sub.begin(); it != d->
sub.end(); it++)
633 stack.push_back(it->data);
643 #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)
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
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)
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
void set_size_t(const irep_namet &name, const std::size_t value)
named_subtreest named_subt
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
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