10 #ifndef CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H 11 #define CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H 50 static std::string
bin_zero(
unsigned bits);
67 typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
73 #endif // CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H static typet gen_array_index_type()
The type of an expression.
void convert_as_bv(const exprt &expr)
void find_symbols(const exprt &expr)
virtual void convert_dplib_expr(const exprt &expr)
static std::string array_index_type()
void convert_array_value(const exprt &expr)
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
static std::string array_index(unsigned i)
static std::string bin_zero(unsigned bits)
static std::string dplib_pointer_type()
dplib_convt(const namespacet &_ns, std::ostream &_out)
pointer_logict pointer_logic
identifier_mapt identifier_map
virtual literalt convert_rest(const exprt &expr)
virtual void convert_dplib_type(const typet &type)
Base class for all expressions.
void convert_identifier(const std::string &identifier)
virtual void set_to(const exprt &expr, bool value)
virtual void convert_address_of_rec(const exprt &expr)
void convert_array_index(const exprt &expr)