12 #ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
13 #define CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
52 seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
55 template <
typename S,
typename T>
67 std::pair<unsigned int, const irept::dt *>,
69 pair_hash<unsigned int, const irept::dt *>>
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
static void hash_combine(std::size_t &seed, const T &v)
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
graphml_witnesst(const namespacet &_ns)
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Read/write graphs as GraphML.
std::size_t operator()(const std::pair< S, T > &v) const