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
66template <
bool enabled>
74 unsigned ref_count = 1;
96template <
typename treet,
typename named_subtreest,
bool sharing = true>
101 typedef std::vector<treet>
subt;
155template <
typename derivedt,
typename named_subtreest>
188 std::cout <<
"COPY " <<
data <<
" " <<
data->ref_count <<
'\n';
199 std::cout <<
"COPY MOVE\n";
207 std::cout <<
"ASSIGN\n";
214 irep_data->ref_count++;
227 std::cout <<
"ASSIGN MOVE\n";
230 std::swap(
data, irep.data);
264template <
typename derivedt,
typename named_subtreest>
269template <
typename derivedt,
typename named_subtreest>
285 :
data(
std::move(_id),
std::move(_named_sub),
std::move(_sub))
364 : public non_sharing_treet<
367#if NAMED_SUB_IS_FORWARD_LIST
368 forward_list_as_mapt<irep_idt, irept>>
370 std::map<irep_idt, irept>>
378 return id() == ID_nil;
382 return id() != ID_nil;
390 :
baset(_id, _named_sub, _sub)
426 add(name, std::move(irep));
428 void set(
const irep_idt &name,
const long long value);
439 return !(*
this==other);
461 std::size_t
hash()
const;
466 std::string
pretty(
unsigned indent=0,
unsigned max_indent=0)
const;
469 {
return !name.
empty() && name[0]==
'#'; }
517template <
typename derivedt,
typename named_subtreest>
521 std::cout <<
"DETACH1: " <<
data <<
'\n';
529 std::cout <<
"ALLOCATED " <<
data <<
'\n';
532 else if(
data->ref_count > 1)
538 std::cout <<
"ALLOCATED " <<
data <<
'\n';
542 remove_ref(old_data);
548 std::cout <<
"DETACH2: " <<
data <<
'\n';
552template <
typename derivedt,
typename named_subtreest>
555 if(old_data == &empty_d)
559 nonrecursive_destructor(old_data);
565 std::cout <<
"R: " << old_data <<
" " << old_data->ref_count <<
'\n';
568 old_data->ref_count--;
569 if(old_data->ref_count == 0)
572 std::cout <<
"D: " << pretty() <<
'\n';
573 std::cout <<
"DELETING " << old_data->
data <<
" " << old_data <<
'\n';
575 std::cout <<
"DEALLOCATING " << old_data <<
"\n";
582 std::cout <<
"DONE\n";
590template <
typename derivedt,
typename named_subtreest>
594 std::vector<dt *> stack(1, old_data);
596 while(!stack.empty())
598 dt *d = stack.back();
599 stack.erase(--stack.end());
603 INVARIANT(d->ref_count != 0,
"All contents of the stack must be in use");
606 if(d->ref_count == 0)
612 for(
typename named_subt::iterator it = d->
named_sub.begin();
616 stack.push_back(it->second.data);
617 it->second.
data = &empty_d;
620 for(
typename subt::iterator it = d->
sub.begin(); it != d->
sub.end(); it++)
622 stack.push_back(it->data);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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 get_bool(const irep_idt &name) const
bool operator==(const irept &other) const
void set(const irep_idt &name, irept irep)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void move_to_named_sub(const irep_idt &name, irept &irep)
std::size_t get_size_t(const irep_idt &name) const
bool operator!=(const irept &other) const
const subt & get_sub() const
const irept & find(const irep_idt &name) const
bool ordering(const irept &other) const
defines ordering on the internal representation
const irep_idt & get(const irep_idt &name) const
irept(const irep_idt &_id)
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
void set_size_t(const irep_idt &name, const std::size_t value)
irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
const named_subt & get_named_sub() const
const std::string & id_string() const
bool operator<(const irept &other) const
defines ordering on the internal representation
bool full_eq(const irept &other) const
long long get_long_long(const irep_idt &name) const
std::size_t full_hash() const
signed int get_int(const irep_idt &name) const
static bool is_comment(const irep_idt &name)
void move_to_sub(irept &irep)
const irep_idt & id() const
void id(const irep_idt &_data)
irept & add(const irep_idt &name)
named_subt & get_named_sub()
const std::string & get_string(const irep_idt &name) const
Base class for tree-like data structures without sharing.
non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
non_sharing_treet()=default
non_sharing_treet(irep_idt _id)
typename dt::named_subt named_subt
Base class for tree-like data structures with sharing.
sharing_treet & operator=(sharing_treet &&irep)
sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
sharing_treet(irep_idt _id)
static void remove_ref(dt *old_data)
typename dt::named_subt named_subt
sharing_treet tree_implementationt
Used to refer to this class from derived classes.
sharing_treet(const sharing_treet &irep)
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
sharing_treet(sharing_treet &&irep)
sharing_treet & operator=(const sharing_treet &irep)
A node with data in a tree, it contains:
named_subtreest named_subt
tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
std::vector< treet > subt
tree_nodet(irep_idt _data)
irep_idt data
This irep_idt is the only place to store data in an tree node.
dstring_hash irep_id_hash
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
Helper to give us some diagnostic in a usable form on assertion failure.
bool operator()(const irept &i1, const irept &i2) const
std::size_t operator()(const irept &irep) const
std::size_t operator()(const irept &irep) const
Used in tree_nodet for activating or not reference counting.