Go to the documentation of this file.
53 if(type.
id() == ID_symbol_type)
56 std::pair<mappingt::iterator, bool> result=
57 mapping.insert(std::pair<irep_idt, map_entryt>(
72 "number of literals in the literal map shall equal the bitvector width");
79 for(mappingt::const_iterator it=
mapping.begin();
89 const std::size_t width,
97 "number of literals in the literal map shall equal the bitvector width");
102 const std::size_t bit=it-literals.begin();
105 bit < map_entry.
literal_map.size(),
"bit index shall be within bounds");
120 std::cout <<
"NEW: " << identifier <<
":" << bit
139 "variable number of non-constant literals shall be within bounds");
141 const std::size_t bit = it - literals.begin();
144 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)
#define PRECONDITION(CONDITION)
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)
const irep_idt & id() const
const boolbv_widtht & boolbv_width
virtual tvt l_get(literalt a) const =0
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)