13 #ifndef CPROVER_SOLVERS_SMT1_SMT1_CONV_H 14 #define CPROVER_SOLVERS_SMT1_SMT1_CONV_H 48 const std::string &_benchmark,
49 const std::string &_source,
50 const std::string &_logic,
157 const std::string &index,
158 const std::string &value)
161 if(tmp.
id()==
"array-list" && identifier.
value.
id()==
"array-list")
167 identifier.
value=tmp;
170 typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
191 const std::string &index,
192 const std::string &v,
193 bool in_struct)
const;
197 const std::string &binary)
const;
201 const std::string &binary)
const;
214 #endif // CPROVER_SOLVERS_SMT1_SMT1_CONV_H The type of an expression.
virtual void set_to(const exprt &expr, bool value)
void convert_overflow(const exprt &expr)
pointer_logict pointer_logic
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
void convert_type(const typet &type)
void convert_mult(const mult_exprt &expr)
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &expr, bool bool_as_bv)
void copy_to_operands(const exprt &expr)
void convert_floatbv_minus(const exprt &expr)
void set_value(identifiert &identifier, const std::string &index, const std::string &value)
smt1_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver, std::ostream &_out)
A constant literal expression.
std::map< exprt, irep_idt > array_expr_mapt
void convert_byte_extract(const byte_extract_exprt &expr, bool bool_as_bv)
virtual void print_assignment(std::ostream &out) const
void find_symbols(const exprt &expr)
Extract member of struct or union.
identifier_mapt identifier_map
virtual resultt dec_solve()
void convert_byte_update(const exprt &expr, bool bool_as_bv)
const irep_idt & id() const
void convert_div(const div_exprt &expr)
void convert_union(const exprt &expr)
division (integer and real)
virtual literalt convert(const exprt &expr)
void convert_update(const exprt &expr)
void convert_index(const index_exprt &expr, bool bool_as_bv)
typet array_index_type() const
API to expression classes.
unsigned array_index_bits
std::map< exprt, irep_idt > array_of_mapt
boolbv_widtht boolbv_width
unsigned no_boolean_variables
#define forall_operands(it, expr)
string2array_mapt string2array_map
std::map< exprt, exprt > string2array_mapt
void convert_struct(const exprt &expr)
std::vector< bool > boolean_assignment
void convert_plus(const plus_exprt &expr)
void convert_floatbv_plus(const exprt &expr)
virtual tvt l_get(literalt) const
void from_bool_end(const typet &type, bool bool_as_bv)
void from_bv_begin(const typet &type, bool bool_as_bv)
void convert_member(const member_exprt &expr, bool bool_as_bv)
void from_bool_begin(const typet &type, bool bool_as_bv)
array_of_mapt array_of_map
void convert_floatbv_mult(const exprt &expr)
virtual std::string decision_procedure_text() const
void convert_typecast(const typecast_exprt &expr, bool bool_as_bv)
void convert_constant(const constant_exprt &expr, bool bool_as_bv)
exprt ce_value(const typet &type, const std::string &index, const std::string &v, bool in_struct) const
Base class for all expressions.
void convert_nary(const exprt &expr, const irep_idt op_string, bool bool_as_bv)
void convert_literal(const literalt l)
void flatten_array(const exprt &op)
void convert_with(const exprt &expr)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
void convert_relation(const exprt &expr, bool bool_as_bv)
void convert_floatbv_div(const exprt &expr)
exprt binary2struct(const struct_typet &type, const std::string &binary) const
void convert_mod(const mod_exprt &expr)
exprt binary2union(const union_typet &type, const std::string &binary) const
void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv)
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void from_bv_end(const typet &type, bool bool_as_bv)
array_expr_mapt array_expr_map
std::string convert_identifier(const irep_idt &identifier)
void array_index(const exprt &expr)
std::set< irep_idt > quantified_symbols