10 #ifndef CPROVER_SOLVERS_CVC_CVC_CONV_H 11 #define CPROVER_SOLVERS_CVC_CVC_CONV_H 58 typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
83 static std::string
bin_zero(
unsigned bits);
89 #endif // CPROVER_SOLVERS_CVC_CVC_CONV_H cvc_convt(const namespacet &_ns, std::ostream &_out)
void convert_minus_expr(const exprt &expr)
The type of an expression.
void convert_comparison_expr(const exprt &expr)
void convert_binary_expr(const exprt &expr, const exprt &op)
void convert_plus_expr(const exprt &expr)
virtual void convert_address_of_rec(const exprt &expr)
static std::string array_index(unsigned i)
void convert_constant_expr(const exprt &expr)
static std::string bin_zero(unsigned bits)
virtual literalt convert(const exprt &expr)
void convert_literal(const literalt l)
identifier_mapt identifier_map
void convert_with_expr(const exprt &expr)
virtual void print_assignment(std::ostream &out) const
static typet gen_array_index_type()
static std::string cvc_pointer_type()
void convert_array_value(const exprt &expr)
void convert_as_bv(const exprt &expr)
void convert_identifier(const std::string &identifier)
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
void convert_equality_expr(const exprt &expr)
virtual void convert_type(const typet &type)
Base class for all expressions.
void convert_struct_expr(const exprt &expr)
virtual tvt l_get(literalt) const
std::vector< bool > boolean_assignment
unsigned no_boolean_variables
static std::string array_index_type()
void find_symbols(const exprt &expr)
void convert_typecast_expr(const exprt &expr)
pointer_logict pointer_logic
void convert_array_index(const exprt &expr)
virtual void set_to(const exprt &expr, bool value)
virtual void convert_expr(const exprt &expr)