10 #ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H 11 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H 58 typedef std::unordered_map<irep_idt, map_entryt>
mappingt;
70 const std::size_t width,
88 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
The type of an expression, extends irept.
const boolbv_widtht & boolbv_width
boolbv_mapt(propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
std::string get_value(const propt &) const
void erase_literals(const irep_idt &identifier, const typet &type)
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< map_bitt > literal_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_map< irep_idt, map_entryt > mappingt
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
std::vector< literalt > bvt
Defines typet, type_with_subtypet and type_with_subtypest.