cprover
|
#include <smt2_conv.h>
Classes | |
struct | identifiert |
struct | let_count_idt |
class | let_visitort |
class | smt2_symbolt |
Public Types | |
enum | solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 } |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Public Member Functions | |
smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out) | |
virtual | ~smt2_convt () |
virtual resultt | dec_solve () |
virtual literalt | convert (const exprt &expr) |
virtual void | set_frozen (literalt a) |
virtual void | set_to (const exprt &expr, bool value) |
virtual exprt | get (const exprt &expr) const |
virtual std::string | decision_procedure_text () const |
virtual void | print_assignment (std::ostream &out) const |
virtual tvt | l_get (literalt l) const |
virtual void | set_assumptions (const bvt &bv) |
void | convert_expr (const exprt &) |
void | convert_type (const typet &) |
void | convert_literal (const literalt) |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
virtual bool | has_set_assumptions () const |
virtual void | set_all_frozen () |
virtual bool | is_in_conflict (literalt l) const |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const |
virtual void | set_time_limit_seconds (uint32_t) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
Public Attributes | |
bool | use_FPA_theory |
bool | use_datatypes |
bool | use_array_of_bool |
bool | emit_set_logic |
Protected Types | |
enum | wheret { wheret::BEGIN, wheret::END } |
typedef irep_hash_mapt< exprt, let_count_idt > | seen_expressionst |
typedef std::unordered_map< irep_idt, identifiert > | identifier_mapt |
typedef std::map< typet, std::string > | datatype_mapt |
typedef std::map< exprt, irep_idt > | defined_expressionst |
typedef std::set< std::string > | smt2_identifierst |
Protected Member Functions | |
void | write_header () |
void | write_footer (std::ostream &) |
bool | use_array_theory (const exprt &) |
void | flatten_array (const exprt &) |
produce a flat bit-vector for a given array of fixed size More... | |
void | unflatten_array (const exprt &) |
void | convert_byte_update (const byte_update_exprt &expr) |
void | convert_byte_extract (const byte_extract_exprt &expr) |
void | convert_typecast (const typecast_exprt &expr) |
void | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
void | convert_struct (const struct_exprt &expr) |
void | convert_union (const union_exprt &expr) |
void | convert_constant (const constant_exprt &expr) |
void | convert_relation (const exprt &expr) |
void | convert_is_dynamic_object (const exprt &expr) |
void | convert_plus (const plus_exprt &expr) |
void | convert_minus (const minus_exprt &expr) |
void | convert_div (const div_exprt &expr) |
void | convert_mult (const mult_exprt &expr) |
void | convert_rounding_mode_FPA (const exprt &expr) |
Converting a constant or symbolic rounding mode to SMT-LIB. More... | |
void | convert_floatbv_plus (const ieee_float_op_exprt &expr) |
void | convert_floatbv_minus (const ieee_float_op_exprt &expr) |
void | convert_floatbv_div (const ieee_float_op_exprt &expr) |
void | convert_floatbv_mult (const ieee_float_op_exprt &expr) |
void | convert_mod (const mod_exprt &expr) |
void | convert_index (const index_exprt &expr) |
void | convert_member (const member_exprt &expr) |
void | convert_overflow (const exprt &expr) |
void | convert_with (const with_exprt &expr) |
void | convert_update (const exprt &expr) |
std::string | convert_identifier (const irep_idt &identifier) |
exprt | convert_operands (const exprt &) |
void | find_symbols (const exprt &expr) |
void | find_symbols (const typet &type) |
void | find_symbols_rec (const typet &type, std::set< irep_idt > &recstack) |
exprt | letify (exprt &expr) |
exprt | letify_rec (exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i) |
void | collect_bindings (exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order) |
exprt | substitute_let (exprt &expr, const seen_expressionst &map) |
constant_exprt | parse_literal (const irept &, const typet &type) |
exprt | parse_struct (const irept &s, const struct_typet &type) |
exprt | parse_union (const irept &s, const union_typet &type) |
exprt | parse_array (const irept &s, const array_typet &type) |
exprt | parse_rec (const irept &s, const typet &type) |
void | convert_floatbv (const exprt &expr) |
std::string | type2id (const typet &) const |
std::string | floatbv_suffix (const exprt &) const |
const smt2_symbolt & | to_smt2_symbol (const exprt &expr) |
void | flatten2bv (const exprt &) |
void | unflatten (wheret, const typet &, unsigned nesting=0) |
void | convert_address_of_rec (const exprt &expr, const pointer_typet &result_type) |
void | define_object_size (const irep_idt &id, const exprt &expr) |
Protected Attributes | |
std::ostream & | out |
std::string | benchmark |
std::string | notes |
std::string | logic |
solvert | solver |
bvt | assumptions |
boolbv_widtht | boolbv_width |
std::size_t | let_id_count |
std::set< irep_idt > | bvfp_set |
pointer_logict | pointer_logic |
identifier_mapt | identifier_map |
datatype_mapt | datatype_map |
defined_expressionst | defined_expressions |
defined_expressionst | object_sizes |
smt2_identifierst | smt2_identifiers |
std::size_t | no_boolean_variables |
std::vector< bool > | boolean_assignment |
![]() | |
const namespacet & | ns |
Static Protected Attributes | |
static const std::size_t | LET_COUNT = 2 |
Additional Inherited Members |
Definition at line 32 of file smt2_conv.h.
|
protected |
Definition at line 297 of file smt2_conv.h.
|
protected |
Definition at line 306 of file smt2_conv.h.
|
protected |
Definition at line 291 of file smt2_conv.h.
|
protected |
Definition at line 191 of file smt2_conv.h.
|
protected |
Definition at line 311 of file smt2_conv.h.
|
strong |
Enumerator | |
---|---|
GENERIC | |
BOOLECTOR | |
CVC3 | |
CVC4 | |
MATHSAT | |
YICES | |
Z3 |
Definition at line 35 of file smt2_conv.h.
|
strongprotected |
Enumerator | |
---|---|
BEGIN | |
END |
Definition at line 267 of file smt2_conv.h.
|
inline |
Definition at line 46 of file smt2_conv.h.
References BOOLECTOR, CVC3, CVC4, emit_set_logic, GENERIC, MATHSAT, solver, use_array_of_bool, use_datatypes, write_header(), YICES, and Z3.
|
inlinevirtual |
Definition at line 101 of file smt2_conv.h.
|
protected |
Definition at line 4774 of file smt2_conv.cpp.
References smt2_convt::let_count_idt::count, irep_hash_mapt< Key, T >::end(), irep_hash_mapt< Key, T >::find(), Forall_operands, irep_hash_mapt< Key, T >::insert(), let_id_count, exprt::operands(), to_string(), and exprt::type().
Referenced by letify().
Implements prop_convt.
Definition at line 710 of file smt2_conv.cpp.
References const_literal(), convert_expr(), convert_literal(), find_symbols(), literal_exprt::get_literal(), irept::id(), exprt::is_false(), exprt::is_true(), no_boolean_variables, out, to_literal_expr(), and exprt::type().
|
protected |
Definition at line 499 of file smt2_conv.cpp.
References pointer_logict::add_object(), index_exprt::array(), boolbv_width, configt::bv_encoding, config, convert_expr(), namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), irept::id_string(), index_exprt::index(), index_type(), INVALIDEXPR, exprt::is_zero(), member_offset(), decision_proceduret::ns, configt::bv_encodingt::object_bits, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, pointer_logic, pointer_type(), member_exprt::struct_op(), typet::subtype(), to_index_expr(), to_member_expr(), to_struct_type(), exprt::type(), and UNEXPECTEDCASE.
Referenced by convert_expr().
|
protected |
Definition at line 598 of file smt2_conv.cpp.
References BEGIN, convert_expr(), END, flatten_byte_extract(), decision_proceduret::ns, exprt::type(), and unflatten().
Referenced by convert_expr().
|
protected |
Definition at line 607 of file smt2_conv.cpp.
References BEGIN, BEGIN, boolbv_width, END, END, flatten2bv(), from_integer(), irept::id(), INVALIDEXPR, byte_update_exprt::offset(), byte_update_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, power(), to_integer(), exprt::type(), UNEXPECTEDCASE, unflatten(), and byte_update_exprt::value().
Referenced by convert_expr().
|
protected |
Definition at line 2653 of file smt2_conv.cpp.
References binary2integer(), boolbv_width, defined_expressions, irept::get(), floatbv_typet::get_e(), floatbv_typet::get_f(), ieee_floatt::get_sign(), constant_exprt::get_value(), irept::id(), id2string(), irept::id_string(), integer2binary(), exprt::is_false(), ieee_floatt::is_infinity(), ieee_floatt::is_NaN(), exprt::is_true(), out, ieee_floatt::pack(), pos(), ieee_floatt::spec, to_fixedbv_type(), to_floatbv_type(), exprt::type(), UNEXPECTEDCASE, use_FPA_theory, fixedbv_spect::width, and ieee_float_spect::width().
Referenced by convert_expr(), and convert_typecast().
|
protected |
Definition at line 3285 of file smt2_conv.cpp.
References convert_expr(), fixedbv_spect::get_fraction_bits(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, to_fixedbv_type(), exprt::type(), UNEXPECTEDCASE, UNREACHABLE, and fixedbv_spect::width.
Referenced by convert_expr().
void smt2_convt::convert_expr | ( | const exprt & | expr | ) |
Definition at line 866 of file smt2_conv.cpp.
References base_type_eq(), boolbv_width, configt::bv_encoding, config, convert_address_of_rec(), convert_byte_extract(), convert_byte_update(), convert_constant(), convert_div(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_identifier(), convert_index(), convert_is_dynamic_object(), convert_literal(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_plus(), convert_relation(), convert_struct(), convert_type(), convert_typecast(), convert_union(), convert_update(), convert_with(), DATA_INVARIANT, datatype_map, defined_expressions, flatten2bv(), forall_operands, from_integer(), irept::get(), symbol_exprt::get_identifier(), nondet_symbol_exprt::get_identifier(), pointer_logict::get_invalid_object(), bitvector_typet::get_width(), irept::id(), id2string(), irept::id_string(), index_type(), INVALIDEXPR, exprt::is_constant(), lower_popcount(), MATHSAT, decision_proceduret::ns, configt::bv_encodingt::object_bits, object_sizes, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, pointer_logic, power(), vector_typet::size(), SMT2_TODO, solver, let_exprt::symbol(), to_bitvector_type(), to_byte_extract_expr(), to_byte_update_expr(), to_constant_expr(), to_div_expr(), to_fixedbv_type(), to_floatbv_typecast_expr(), to_ieee_float_op_expr(), to_index_expr(), to_integer(), to_let_expr(), to_literal_expr(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_nondet_symbol_expr(), to_plus_expr(), to_pointer_type(), to_popcount_expr(), to_signedbv_type(), to_struct_expr(), to_symbol_expr(), to_typecast_expr(), to_union_expr(), to_vector_type(), to_with_expr(), exprt::type(), UNEXPECTEDCASE, use_datatypes, use_FPA_theory, let_exprt::value(), and let_exprt::where().
Referenced by convert(), convert_address_of_rec(), convert_byte_extract(), convert_div(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_index(), convert_is_dynamic_object(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_plus(), convert_relation(), convert_rounding_mode_FPA(), convert_struct(), convert_typecast(), convert_with(), define_object_size(), find_symbols(), flatten2bv(), flatten_array(), and set_to().
|
protected |
Definition at line 833 of file smt2_conv.cpp.
References convert_expr(), convert_identifier(), floatbv_suffix(), forall_operands, symbol_exprt::get_identifier(), smt2_convt::smt2_symbolt::get_identifier(), irept::id(), exprt::operands(), out, to_smt2_symbol(), to_symbol_expr(), and use_FPA_theory.
Referenced by convert_expr(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_relation(), and convert_typecast().
|
protected |
Definition at line 3331 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), convert_rounding_mode_FPA(), irept::id(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, exprt::type(), and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Definition at line 3266 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), convert_rounding_mode_FPA(), irept::id(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, exprt::type(), and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Definition at line 3425 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), convert_rounding_mode_FPA(), irept::id(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, exprt::type(), and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Definition at line 3128 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), convert_rounding_mode_FPA(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, SMT2_TODO, typet::subtype(), exprt::type(), UNEXPECTEDCASE, and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Definition at line 2377 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), convert_rounding_mode_FPA(), namespace_baset::follow_tag(), floatbv_typet::get_e(), floatbv_typet::get_f(), bitvector_typet::get_width(), irept::id(), irept::id_string(), decision_proceduret::ns, floatbv_typecast_exprt::op(), exprt::op1(), out, typet::subtype(), to_c_enum_tag_type(), to_floatbv_type(), to_signedbv_type(), to_unsignedbv_type(), exprt::type(), UNEXPECTEDCASE, and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Definition at line 762 of file smt2_conv.cpp.
References messaget::result(), dstringt::size(), and to_string().
Referenced by convert_expr(), convert_floatbv(), find_symbols(), smt2_dect::read_result(), and set_to().
|
protected |
Definition at line 3701 of file smt2_conv.cpp.
References index_exprt::array(), BEGIN, boolbv_width, convert_expr(), datatype_map, END, namespace_baset::follow(), index_exprt::index(), decision_proceduret::ns, exprt::operands(), out, array_typet::size(), SMT2_TODO, typet::subtype(), to_array_type(), to_integer(), to_vector_type(), exprt::type(), UNEXPECTEDCASE, unflatten(), use_array_of_bool, use_array_theory(), and use_datatypes.
Referenced by convert_expr().
|
protected |
Definition at line 2810 of file smt2_conv.cpp.
References boolbv_width, configt::bv_encoding, config, convert_expr(), pointer_logict::get_dynamic_objects(), configt::bv_encodingt::object_bits, exprt::op0(), exprt::operands(), out, pointer_logic, and exprt::type().
Referenced by convert_expr().
void smt2_convt::convert_literal | ( | const literalt | l | ) |
Definition at line 742 of file smt2_conv.cpp.
References const_literal(), out, literalt::sign(), smt2_identifiers, to_string(), and literalt::var_no().
Referenced by convert(), convert_expr(), and write_footer().
|
protected |
Definition at line 3803 of file smt2_conv.cpp.
References BEGIN, boolbv_width, convert_expr(), datatype_map, END, namespace_baset::follow(), struct_union_typet::get_component(), struct_union_typet::componentt::get_name(), struct_union_typet::has_component(), irept::id(), irept::id_string(), INVALIDEXPR, member_offset(), decision_proceduret::ns, exprt::operands(), out, to_member_expr(), to_struct_type(), exprt::type(), UNEXPECTEDCASE, unflatten(), and use_datatypes.
Referenced by convert_expr().
|
protected |
Definition at line 3164 of file smt2_conv.cpp.
References boolbv_width, convert_expr(), datatype_map, forall_operands, from_integer(), irept::id(), irept::id_string(), index_type(), INVALIDEXPR, decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), out, pointer_offset_size(), vector_typet::size(), SMT2_TODO, typet::subtype(), to_integer(), to_vector_type(), exprt::type(), UNEXPECTEDCASE, UNREACHABLE, and use_datatypes.
Referenced by convert_expr().
|
protected |
Definition at line 2789 of file smt2_conv.cpp.
References convert_expr(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, exprt::type(), and UNEXPECTEDCASE.
Referenced by convert_expr().
|
protected |
Definition at line 3350 of file smt2_conv.cpp.
References convert_expr(), forall_operands, fixedbv_spect::get_fraction_bits(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, to_fixedbv_type(), exprt::type(), UNEXPECTEDCASE, UNREACHABLE, and fixedbv_spect::width.
Referenced by convert_expr().
|
protected |
Definition at line 4079 of file smt2_conv.cpp.
References UNREACHABLE.
|
protected |
Definition at line 2934 of file smt2_conv.cpp.
References boolbv_width, CHECK_RETURN, convert_expr(), datatype_map, forall_operands, from_integer(), irept::id(), irept::id_string(), index_type(), INVALIDEXPR, make_binary(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), out, pointer_offset_size(), vector_typet::size(), typet::subtype(), irept::swap(), to_integer(), to_plus_expr(), to_vector_type(), exprt::type(), UNEXPECTEDCASE, UNREACHABLE, and use_datatypes.
Referenced by convert_expr().
|
protected |
Definition at line 2849 of file smt2_conv.cpp.
References convert_expr(), convert_floatbv(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, exprt::type(), UNEXPECTEDCASE, and use_FPA_theory.
Referenced by convert_expr().
|
protected |
Converting a constant or symbolic rounding mode to SMT-LIB.
Only called when use_FPA_theory is enabled
Definition at line 3072 of file smt2_conv.cpp.
References binary2integer(), convert_expr(), constant_exprt::get_value(), irept::id(), id2string(), INVALIDEXPR, out, to_bitvector_type(), to_constant_expr(), exprt::type(), and use_FPA_theory.
Referenced by convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), and convert_floatbv_typecast().
|
protected |
Definition at line 2523 of file smt2_conv.cpp.
References struct_union_typet::components(), convert_expr(), datatype_map, flatten_array(), namespace_baset::follow(), decision_proceduret::ns, exprt::op0(), exprt::operands(), out, to_struct_type(), exprt::type(), and use_datatypes.
Referenced by convert_expr().
void smt2_convt::convert_type | ( | const typet & | type | ) |
Definition at line 4387 of file smt2_conv.cpp.
References boolbv_width, c_bit_field_replacement_type(), datatype_map, namespace_baset::follow(), namespace_baset::follow_tag(), floatbv_typet::get_e(), floatbv_typet::get_f(), bitvector_typet::get_width(), irept::id(), irept::id_string(), INVALIDEXPR, irept::is_not_nil(), decision_proceduret::ns, out, array_typet::size(), typet::subtype(), to_array_type(), to_bitvector_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_floatbv_type(), exprt::type(), UNEXPECTEDCASE, use_array_of_bool, use_datatypes, and use_FPA_theory.
Referenced by convert_expr(), find_symbols(), find_symbols_rec(), and set_to().
|
protected |
Definition at line 1880 of file smt2_conv.cpp.
References boolbv_width, ieee_floatt::build(), c_bit_field_replacement_type(), convert_constant(), convert_expr(), convert_floatbv(), flatten2bv(), namespace_baset::follow(), namespace_baset::follow_tag(), format(), from_integer(), fixedbv_spect::get_fraction_bits(), fixedbv_typet::get_fraction_bits(), fixedbv_typet::get_integer_bits(), bitvector_typet::get_width(), irept::id(), irept::id_string(), integer2binary(), fixedbv_spect::integer_bits, decision_proceduret::ns, exprt::op0(), exprt::operands(), out, ieee_floatt::pack(), irept::set(), SMT2_TODO, ieee_floatt::spec, to_bitvector_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_fixedbv_type(), to_floatbv_type(), to_integer(), exprt::type(), UNEXPECTEDCASE, use_datatypes, use_FPA_theory, fixedbv_spect::width, and ieee_float_spect::width().
Referenced by convert_expr().
|
protected |
Definition at line 2620 of file smt2_conv.cpp.
References boolbv_width, flatten2bv(), INVALIDEXPR, decision_proceduret::ns, unary_exprt::op(), out, to_union_type(), and exprt::type().
Referenced by convert_expr().
|
protected |
Definition at line 3694 of file smt2_conv.cpp.
References exprt::operands(), and SMT2_TODO.
Referenced by convert_expr().
|
protected |
Definition at line 3444 of file smt2_conv.cpp.
References boolbv_width, convert_expr(), datatype_map, flatten2bv(), namespace_baset::follow(), irept::get(), boolbv_widtht::get_member(), struct_union_typet::has_component(), irept::id(), irept::id_string(), INVALIDEXPR, with_exprt::new_value(), decision_proceduret::ns, boolbv_widtht::membert::offset, with_exprt::old(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, power(), array_typet::size(), SMT2_TODO, typet::subtype(), to_array_type(), to_struct_type(), to_union_type(), exprt::type(), UNEXPECTEDCASE, use_array_theory(), use_datatypes, with_exprt::where(), and boolbv_widtht::membert::width.
Referenced by convert_expr().
|
virtual |
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 172 of file smt2_conv.cpp.
References decision_proceduret::D_ERROR, out, and write_footer().
|
inlinevirtual |
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 114 of file smt2_conv.h.
Definition at line 134 of file smt2_conv.cpp.
References boolbv_width, configt::bv_encoding, config, convert_expr(), namespace_baset::follow(), irept::id(), irept::is_nil(), decision_proceduret::ns, configt::bv_encodingt::object_bits, object_size(), pointer_logict::objects, exprt::op0(), out, pointer_logic, size_of_expr(), to_integer(), and exprt::type().
Referenced by write_footer().
|
protected |
Definition at line 4172 of file smt2_conv.cpp.
References bvfp_set, convert_expr(), convert_identifier(), convert_type(), defined_expressions, float_bv(), floatbv_suffix(), forall_operands, from_integer(), symbol_exprt::get_identifier(), irept::id(), id2string(), irept::id_string(), identifier_map, letify(), object_sizes, exprt::op0(), exprt::operands(), out, array_typet::size(), smt2_identifiers, string_constantt::to_array_expr(), to_array_type(), to_nondet_symbol_expr(), to_string(), to_string_constant(), to_symbol_expr(), exprt::type(), type2id(), and use_FPA_theory.
Referenced by convert(), find_symbols_rec(), and set_to().
|
protected |
Definition at line 4538 of file smt2_conv.cpp.
References find_symbols_rec().
Definition at line 4544 of file smt2_conv.cpp.
References struct_union_typet::components(), convert_type(), datatype_map, find_symbols(), namespace_baset::follow(), symbol_typet::get_identifier(), struct_union_typet::componentt::get_name(), irept::id(), INVALIDEXPR, decision_proceduret::ns, out, code_typet::parameters(), array_typet::size(), vector_typet::size(), typet::subtype(), to_array_type(), to_code_type(), to_integer(), to_string(), to_struct_type(), to_symbol_type(), to_union_type(), to_vector_type(), exprt::type(), and use_datatypes.
Referenced by find_symbols().
|
protected |
Definition at line 3868 of file smt2_conv.cpp.
References struct_union_typet::components(), convert_expr(), datatype_map, namespace_baset::follow(), irept::id(), INVALIDEXPR, decision_proceduret::ns, out, vector_typet::size(), to_integer(), to_struct_type(), to_vector_type(), exprt::type(), use_datatypes, and use_FPA_theory.
Referenced by convert_byte_update(), convert_expr(), convert_typecast(), convert_union(), and convert_with().
|
protected |
produce a flat bit-vector for a given array of fixed size
Definition at line 2586 of file smt2_conv.cpp.
References convert_expr(), namespace_baset::follow(), from_integer(), INVALIDEXPR, decision_proceduret::ns, out, array_typet::size(), to_array_type(), to_integer(), and exprt::type().
Referenced by convert_struct().
|
protected |
Definition at line 827 of file smt2_conv.cpp.
References exprt::op0(), exprt::operands(), exprt::type(), and type2id().
Referenced by convert_floatbv(), and find_symbols().
Implements decision_proceduret.
Definition at line 179 of file smt2_conv.cpp.
References member_exprt::get_component_name(), symbol_exprt::get_identifier(), nondet_symbol_exprt::get_identifier(), irept::id(), identifier_map, irept::is_nil(), member_exprt::struct_op(), to_member_expr(), to_nondet_symbol_expr(), to_symbol_expr(), and exprt::type().
Implements prop_convt.
Definition at line 61 of file smt2_conv.cpp.
References boolean_assignment, literalt::is_false(), literalt::is_true(), literalt::sign(), and literalt::var_no().
Definition at line 4740 of file smt2_conv.cpp.
References collect_bindings(), and letify_rec().
Referenced by find_symbols().
|
protected |
Definition at line 4750 of file smt2_conv.cpp.
References irep_hash_mapt< Key, T >::end(), irep_hash_mapt< Key, T >::find(), LET_COUNT, substitute_let(), let_exprt::symbol(), let_exprt::value(), and let_exprt::where().
Referenced by letify().
|
protected |
Definition at line 339 of file smt2_conv.cpp.
References irept::get_sub(), parse_rec(), array_typet::size(), typet::subtype(), and exprt::type().
Referenced by parse_rec().
|
protected |
Definition at line 211 of file smt2_conv.cpp.
References binary2integer(), boolbv_width, namespace_baset::follow_tag(), from_integer(), floatbv_typet::get_e(), floatbv_typet::get_f(), irept::get_sub(), constant_exprt::get_value(), irept::id(), id2string(), irept::id_string(), integer2binary(), ieee_floatt::minus_infinity(), ieee_floatt::NaN(), decision_proceduret::ns, ieee_floatt::plus_infinity(), string2integer(), to_c_enum_tag_type(), ieee_floatt::to_expr(), to_floatbv_type(), UNEXPECTEDCASE, and unsafe_string2size_t().
Referenced by parse_rec(), and parse_struct().
Definition at line 445 of file smt2_conv.cpp.
References boolbv_width, configt::bv_encoding, config, namespace_baset::follow(), irept::id(), integer2size_t(), decision_proceduret::ns, pointer_logict::pointert::object, configt::bv_encodingt::object_bits, pointer_logict::pointert::offset, parse_array(), parse_literal(), parse_struct(), parse_union(), pointer_logict::pointer_expr(), pointer_logic, power(), to_array_type(), to_integer(), to_pointer_type(), to_struct_type(), and to_union_type().
Referenced by parse_array(), parse_struct(), parse_union(), and smt2_dect::read_result().
|
protected |
Definition at line 384 of file smt2_conv.cpp.
References boolbv_width, struct_union_typet::components(), irept::get_sub(), constant_exprt::get_value(), id2string(), exprt::is_constant(), parse_literal(), parse_rec(), messaget::result(), dstringt::size(), to_constant_expr(), exprt::type(), and use_datatypes.
Referenced by parse_rec().
|
protected |
Definition at line 369 of file smt2_conv.cpp.
References boolbv_width, struct_union_typet::components(), irept::is_nil(), parse_rec(), and exprt::type().
Referenced by parse_rec().
|
virtual |
Implements decision_proceduret.
Definition at line 51 of file smt2_conv.cpp.
References boolean_assignment, and out.
|
inlinevirtual |
|
inlinevirtual |
Reimplemented from prop_convt.
Definition at line 111 of file smt2_conv.h.
|
virtual |
Implements decision_proceduret.
Definition at line 4084 of file smt2_conv.cpp.
References convert_expr(), convert_identifier(), convert_type(), find_symbols(), forall_operands, format(), irept::id(), identifier_map, binary_relation_exprt::lhs(), exprt::op0(), exprt::operands(), out, binary_relation_exprt::rhs(), smt2_identifiers, to_equal_expr(), to_symbol_expr(), and exprt::type().
|
protected |
Definition at line 4805 of file smt2_conv.cpp.
References Forall_operands, and exprt::operands().
Referenced by letify_rec().
|
inlineprotected |
Definition at line 257 of file smt2_conv.h.
References exprt::has_operands(), and irept::id().
Referenced by convert_floatbv().
|
protected |
Definition at line 793 of file smt2_conv.cpp.
References ieee_float_spect::f, namespace_baset::follow_tag(), irept::id(), decision_proceduret::ns, typet::subtype(), to_c_bool_type(), to_c_enum_tag_type(), to_floatbv_type(), to_signedbv_type(), to_string(), to_unsignedbv_type(), and ieee_float_spect::width().
Referenced by find_symbols(), and floatbv_suffix().
Definition at line 3964 of file smt2_conv.cpp.
References BEGIN, boolbv_width, struct_union_typet::components(), datatype_map, END, namespace_baset::follow(), irept::id(), INVALIDEXPR, decision_proceduret::ns, out, vector_typet::size(), typet::subtype(), to_integer(), to_struct_type(), to_vector_type(), and use_datatypes.
Referenced by convert_byte_extract(), convert_byte_update(), convert_index(), and convert_member().
|
protected |
|
protected |
Definition at line 4365 of file smt2_conv.cpp.
References namespace_baset::follow(), irept::id(), decision_proceduret::ns, with_exprt::old(), PRECONDITION, to_with_expr(), exprt::type(), and use_datatypes.
Referenced by convert_index(), and convert_with().
|
protected |
Definition at line 97 of file smt2_conv.cpp.
References assumptions, BOOLECTOR, convert_literal(), define_object_size(), forall_literals, object_sizes, out, smt2_identifiers, and solver.
Referenced by smt2_dect::dec_solve(), and dec_solve().
|
protected |
Definition at line 71 of file smt2_conv.cpp.
References BOOLECTOR, CVC3, CVC4, emit_set_logic, GENERIC, logic, MATHSAT, notes, out, solver, YICES, and Z3.
Referenced by smt2_convt().
|
protected |
Definition at line 129 of file smt2_conv.h.
Referenced by set_assumptions(), and write_footer().
|
protected |
Definition at line 126 of file smt2_conv.h.
|
protected |
Definition at line 130 of file smt2_conv.h.
Referenced by convert_address_of_rec(), convert_byte_update(), convert_constant(), convert_expr(), convert_index(), convert_is_dynamic_object(), convert_member(), convert_minus(), convert_plus(), convert_type(), convert_typecast(), convert_union(), convert_with(), define_object_size(), parse_literal(), parse_rec(), parse_struct(), parse_union(), and unflatten().
|
protected |
Definition at line 316 of file smt2_conv.h.
Referenced by l_get(), print_assignment(), and smt2_dect::read_result().
|
protected |
Definition at line 242 of file smt2_conv.h.
Referenced by find_symbols().
|
protected |
Definition at line 298 of file smt2_conv.h.
Referenced by convert_expr(), convert_index(), convert_member(), convert_minus(), convert_plus(), convert_struct(), convert_type(), convert_with(), find_symbols_rec(), flatten2bv(), and unflatten().
|
protected |
Definition at line 307 of file smt2_conv.h.
Referenced by convert_constant(), convert_expr(), and find_symbols().
bool smt2_convt::emit_set_logic |
Definition at line 107 of file smt2_conv.h.
Referenced by smt2_convt(), and write_header().
|
protected |
Definition at line 293 of file smt2_conv.h.
Referenced by find_symbols(), get(), smt2_dect::read_result(), and set_to().
|
staticprotected |
Definition at line 195 of file smt2_conv.h.
Referenced by letify_rec(), and smt2_convt::let_visitort::operator()().
|
protected |
Definition at line 194 of file smt2_conv.h.
Referenced by collect_bindings().
|
protected |
Definition at line 126 of file smt2_conv.h.
Referenced by smt2_dect::decision_procedure_text(), and write_header().
|
protected |
Definition at line 315 of file smt2_conv.h.
Referenced by convert(), and smt2_dect::read_result().
|
protected |
Definition at line 126 of file smt2_conv.h.
Referenced by write_header().
|
protected |
Definition at line 309 of file smt2_conv.h.
Referenced by convert_expr(), find_symbols(), and write_footer().
|
protected |
Definition at line 125 of file smt2_conv.h.
Referenced by convert(), convert_address_of_rec(), convert_byte_update(), convert_constant(), convert_div(), convert_expr(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_index(), convert_is_dynamic_object(), convert_literal(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_plus(), convert_relation(), convert_rounding_mode_FPA(), convert_struct(), convert_type(), convert_typecast(), convert_union(), convert_with(), dec_solve(), define_object_size(), find_symbols(), find_symbols_rec(), flatten2bv(), flatten_array(), print_assignment(), set_to(), unflatten(), write_footer(), and write_header().
|
protected |
Definition at line 272 of file smt2_conv.h.
Referenced by convert_address_of_rec(), convert_expr(), convert_is_dynamic_object(), define_object_size(), and parse_rec().
|
protected |
Definition at line 312 of file smt2_conv.h.
Referenced by convert_literal(), find_symbols(), set_to(), and write_footer().
|
protected |
Definition at line 127 of file smt2_conv.h.
Referenced by convert_expr(), smt2_dect::dec_solve(), smt2_dect::decision_procedure_text(), smt2_convt(), write_footer(), and write_header().
bool smt2_convt::use_array_of_bool |
Definition at line 106 of file smt2_conv.h.
Referenced by convert_index(), convert_type(), and smt2_convt().
bool smt2_convt::use_datatypes |
Definition at line 105 of file smt2_conv.h.
Referenced by convert_expr(), convert_index(), convert_member(), convert_minus(), convert_plus(), convert_struct(), convert_type(), convert_typecast(), convert_with(), find_symbols_rec(), flatten2bv(), parse_struct(), smt2_convt(), unflatten(), and use_array_theory().
bool smt2_convt::use_FPA_theory |
Definition at line 104 of file smt2_conv.h.
Referenced by convert_constant(), convert_expr(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_relation(), convert_rounding_mode_FPA(), convert_type(), convert_typecast(), smt2_dect::decision_procedure_text(), find_symbols(), and flatten2bv().