Go to the documentation of this file.
53 std::pair<mappingt::iterator, bool> result=
54 mapping.insert(std::pair<irep_idt, map_entryt>(
69 "number of literals in the literal map shall equal the bitvector width");
76 for(mappingt::const_iterator it=
mapping.begin();
86 const std::size_t width,
94 "number of literals in the literal map shall equal the bitvector width");
99 const std::size_t bit=it-literals.begin();
102 bit < map_entry.
literal_map.size(),
"bit index shall be within bounds");
117 std::cout <<
"NEW: " << identifier <<
":" << bit
136 "variable number of non-constant literals shall be within bounds");
138 const std::size_t bit = it - literals.begin();
141 bit < map_entry.
literal_map.size(),
"bit index shall be within bounds");
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void erase_literals(const irep_idt &identifier, const typet &type)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
std::string get_value(const propt &) const
The type of an expression, extends irept.
std::vector< literalt > bvt
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
bvtypet get_bvtype(const typet &type)
virtual literalt new_variable()=0
virtual size_t no_variables() const =0
#define forall_literals(it, bv)
#define Forall_literals(it, bv)
#define PRECONDITION(CONDITION)
const boolbv_widtht & boolbv_width
virtual tvt l_get(literalt a) const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)