|
| template<typename factoryt > |
| static smt_termt | convert_multiary_operator_to_terms (const multi_ary_exprt &expr, const sub_expression_mapt &converted, const factoryt &factory) |
| | Converts operator expressions with 2 or more operands to terms expressed as binary operator application.
|
| |
| template<typename target_typet > |
| static bool | operands_are_of_type (const exprt &expr) |
| | Ensures that all operands of the argument expression have related types.
|
| |
| static smt_sortt | convert_type_to_smt_sort (const bool_typet &type) |
| |
| static smt_sortt | convert_type_to_smt_sort (const bitvector_typet &type) |
| |
| static smt_sortt | convert_type_to_smt_sort (const array_typet &type) |
| |
| static smt_sortt | convert_type_to_smt_sort (const floatbv_typet &type) |
| |
| smt_sortt | convert_type_to_smt_sort (const typet &type) |
| | Converts the type to an smt encoding of the same expression stored as sort ast (abstract syntax tree).
|
| |
| static smt_termt | convert_expr_to_smt (const symbol_exprt &symbol_expr) |
| |
| static smt_termt | convert_expr_to_smt (const nondet_symbol_exprt &nondet_symbol, const sub_expression_mapt &converted) |
| |
| static smt_termt | make_not_zero (const smt_termt &input, const typet &source_type) |
| | Makes a term which is true if input is not 0 / false.
|
| |
| static smt_termt | convert_c_bool_cast (const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type) |
| | Returns a cast to C bool expressed in smt terms.
|
| |
| static std::function< std::function< smt_termt(smt_termt)>(std::size_t)> | extension_for_type (const typet &type) |
| |
| static smt_termt | make_bitvector_resize_cast (const smt_termt &from_term, const bitvector_typet &from_type, const bitvector_typet &to_type) |
| |
| static smt_termt | convert_bit_vector_cast (const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type) |
| |
| static smt_termt | convert_expr_to_smt (const typecast_exprt &cast, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const floatbv_typecast_exprt &float_cast, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const struct_exprt &struct_construction, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const union_exprt &union_construction, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const constant_exprt &constant_literal) |
| |
| static smt_termt | convert_expr_to_smt (const concatenation_exprt &concatenation, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const bitand_exprt &bitwise_and_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const bitor_exprt &bitwise_or_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const bitxor_exprt &bitwise_xor, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const bitnot_exprt &bitwise_not, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const unary_minus_exprt &unary_minus, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const unary_plus_exprt &unary_plus, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const sign_exprt &is_negative, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const if_exprt &if_expression, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const and_exprt &and_expression, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const or_exprt &or_expression, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const xor_exprt &xor_expression, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const implies_exprt &implies, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const not_exprt &logical_not, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const equal_exprt &equal, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const notequal_exprt ¬_equal, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const ieee_float_equal_exprt &float_equal, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const ieee_float_notequal_exprt &float_not_equal, const sub_expression_mapt &converted) |
| |
| template<typename unsigned_factory_typet , typename signed_factory_typet > |
| static smt_termt | convert_relational_to_smt (const binary_relation_exprt &binary_relation, const unsigned_factory_typet &unsigned_factory, const signed_factory_typet &signed_factory, const sub_expression_mapt &converted) |
| |
| static std::optional< smt_termt > | try_relational_conversion (const exprt &expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const plus_exprt &plus, const sub_expression_mapt &converted, const type_size_mapt &pointer_sizes) |
| |
| static smt_termt | convert_expr_to_smt (const minus_exprt &minus, const sub_expression_mapt &converted, const type_size_mapt &pointer_sizes) |
| |
| static smt_termt | convert_expr_to_smt (const div_exprt ÷, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const ieee_float_op_exprt &float_operation, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const mod_exprt &truncation_modulo, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const euclidean_mod_exprt &euclidean_modulo, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const mult_exprt &multiply, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const address_of_exprt &address_of, const sub_expression_mapt &converted, const smt_object_mapt &object_map) |
| |
| static smt_termt | convert_expr_to_smt (const array_of_exprt &array_of, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const array_comprehension_exprt &array_comprehension, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const index_exprt &index_of, const sub_expression_mapt &converted) |
| |
| template<typename factoryt , typename shiftt > |
| static smt_termt | convert_to_smt_shift (const factoryt &factory, const shiftt &shift, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const shift_exprt &shift, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_array_update_to_smt (const with_exprt &with, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const with_exprt &with, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const update_exprt &update, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const member_exprt &member_extraction, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const is_dynamic_object_exprt &is_dynamic_object, const sub_expression_mapt &converted, const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object) |
| |
| static smt_termt | convert_expr_to_smt (const is_invalid_pointer_exprt &is_invalid_pointer, const smt_object_mapt &object_map, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const string_constantt &string_constant, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const extractbit_exprt &extract_bit, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const extractbits_exprt &extract_bits, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const replication_exprt &replication, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const byte_extract_exprt &byte_extraction, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const byte_update_exprt &byte_update, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const abs_exprt &absolute_value_of, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const isnan_exprt &is_nan_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const isfinite_exprt &is_finite_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const isinf_exprt &is_infinite_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const isnormal_exprt &is_normal_expr, const sub_expression_mapt &converted) |
| |
| static smt_termt | most_significant_bit_is_set (const smt_termt &input) |
| | Constructs a term which is true if the most significant bit of input is set.
|
| |
| static smt_termt | convert_expr_to_smt (const plus_overflow_exprt &plus_overflow, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const minus_overflow_exprt &minus_overflow, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const mult_overflow_exprt &mult_overflow, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const pointer_object_exprt &pointer_object, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const pointer_offset_exprt &pointer_offset, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const shl_overflow_exprt &shl_overflow, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const array_exprt &array_construction, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const literal_exprt &literal, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const forall_exprt &for_all, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const exists_exprt &exists, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const vector_exprt &vector, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const object_size_exprt &object_size, const sub_expression_mapt &converted, const smt_object_sizet::make_applicationt &call_object_size) |
| |
| static smt_termt | convert_expr_to_smt (const let_exprt &let, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const bswap_exprt &byte_swap, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const popcount_exprt &population_count, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const count_leading_zeros_exprt &count_leading_zeros, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const count_trailing_zeros_exprt &count_trailing_zeros, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const zero_extend_exprt &zero_extend, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok, const sub_expression_mapt &converted) |
| |
| static smt_termt | convert_expr_to_smt (const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range, const sub_expression_mapt &converted) |
| |
| static smt_termt | dispatch_expr_to_smt_conversion (const exprt &expr, const sub_expression_mapt &converted, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, const smt_object_sizet::make_applicationt &call_object_size, const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object) |
| |
| template<typename functiont > |
| at_scope_exitt< functiont > | at_scope_exit (functiont exit_function) |
| |
| exprt | lower_address_of_array_index (exprt expr) |
| | Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array), so that it can be fed to convert_expr_to_smt.
|
| |
| void | filtered_visit_post (const exprt &_expr, std::function< bool(const exprt &)> filter, std::function< void(const exprt &)> visitor) |
| | Post order traversal where the children of a node are only visited if applying the filter function to that node returns true.
|
| |
| smt_termt | convert_expr_to_smt (const exprt &expr, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, const smt_object_sizet::make_applicationt &object_size, const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object) |
| | Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree).
|
| |
Include dependency graph for convert_expr_to_smt.cpp: