53 if(type.
id()==ID_symbol)
56 std::pair<mappingt::iterator, bool> result=
57 mapping.insert(std::pair<irep_idt, map_entryt>(
77 for(mappingt::const_iterator it=
mapping.begin();
87 const std::size_t width,
92 assert(literals.size()==width);
98 const std::size_t bit=it-literals.begin();
115 std::cout <<
"NEW: " << identifier <<
":" << bit
131 const std::size_t bit=it-literals.begin();
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
The type of an expression.
#define forall_literals(it, bv)
const boolbv_widtht & boolbv_width
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
const irep_idt & id() const
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
std::string get_value(const propt &) const
void erase_literals(const irep_idt &identifier, const typet &type)
virtual size_t no_variables() const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bvtypet get_bvtype(const typet &type)
virtual tvt l_get(literalt a) const =0
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
std::vector< literalt > bvt