47 named_subt::const_iterator it=s.find(name);
54 return it->second.id();
82 add(name).
id(std::to_string(value));
91 add(name).
id(std::to_string(value));
104 auto it = s.find(name);
121#if NAMED_SUB_IS_FORWARD_LIST
122 return s.add(name, std::move(irep));
124 std::pair<named_subt::iterator, bool> entry = s.emplace(
125 std::piecewise_construct,
126 std::forward_as_tuple(name),
127 std::forward_as_tuple(irep));
130 entry.first->second = std::move(irep);
132 return entry.first->second;
136#ifdef IREP_HASH_STATS
143 #ifdef IREP_HASH_STATS
153 #ifdef IREP_HASH_STATS
186#ifdef IREP_HASH_STATS
222 for(std::size_t i=0; i<
i1_sub.size(); i++)
250 if(
X.sub.size()<
Y.sub.size())
252 if(
Y.sub.size()<
X.sub.size())
256 irept::subt::const_iterator
it1,
it2;
258 for(
it1=
X.sub.begin(),
260 it1!=
X.sub.end() &&
it2!=
Y.sub.end();
271 "Unequal lengths will return before this");
274 if(
X.named_sub.size()<
Y.named_sub.size())
276 if(
Y.named_sub.size()<
X.named_sub.size())
280 irept::named_subt::const_iterator
it1,
it2;
282 for(
it1=
X.named_sub.begin(),
283 it2=
Y.named_sub.begin();
284 it1!=
X.named_sub.end() &&
it2!=
Y.named_sub.end();
300 "Unequal lengths will return before this");
313 r=
id().compare(i.
id());
317 const subt::size_type size=
get_sub().size(),
326 irept::subt::const_iterator
it1,
it2;
340 "Unequal lengths will return before this");
352 irept::named_subt::const_iterator
it1,
it2;
381 r=
it1->first.compare(
it2->first);
385 r=
it1->second.compare(
it2->second);
395 "Unequal number of non-comments will return before this");
408#ifdef IREP_HASH_STATS
414 std::size_t result = 0;
416 for(
const auto &
n : named_sub)
426 if(
read().hash_code!=0)
427 return read().hash_code;
435 for(
const auto &irep : sub)
453 read().hash_code=result;
455#ifdef IREP_HASH_STATS
468 for(
const auto &irep : sub)
486 for(
unsigned i=0; i<indent; i++)
517 for(
const auto &irep :
get_sub())
522 result+=std::to_string(count++);
525 result += irep.pretty(indent + 2,
max_indent);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
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
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
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)
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
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
irept & add(const irep_idt &name)
named_subt & get_named_sub()
const std::string & get_string(const irep_idt &name) const
typename dt::named_subt named_subt
size_t hash_string(const dstringt &s)
static std::enable_if< std::is_integral< T >::value, dstringt >::type to_dstring(T value)
equivalent to dstringt(std::to_string(value)), i.e., produces a string from a number
static void indent_str(std::string &s, unsigned indent)
const irept & get_nil_irep()
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
#define hash_finalize(h1, len)
#define hash_combine(h1, h2)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
std::size_t unsafe_string2size_t(const std::string &str, int base)
int unsafe_string2int(const std::string &str, int base)
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
irep_pretty_diagnosticst(const irept &irep)