#include <util/arith_tools.h>#include <util/bitvector_expr.h>#include <util/byte_operators.h>#include <util/c_types.h>#include <util/config.h>#include <util/expr.h>#include <util/expr_cast.h>#include <util/expr_util.h>#include <util/floatbv_expr.h>#include <util/mathematical_expr.h>#include <util/pointer_expr.h>#include <util/pointer_predicates.h>#include <util/range.h>#include <util/std_expr.h>#include <util/string_constant.h>#include <solvers/prop/literal_expr.h>#include <solvers/smt2_incremental/convert_expr_to_smt.h>#include <solvers/smt2_incremental/theories/smt_array_theory.h>#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>#include <solvers/smt2_incremental/theories/smt_core_theory.h>#include <algorithm>#include <functional>#include <numeric>#include <stack>
Include dependency graph for convert_expr_to_smt.cpp:Go to the source code of this file.
Classes | |
| struct | sort_based_cast_to_bit_vector_convertert |
| struct | sort_based_literal_convertert |
| struct | at_scope_exitt< functiont > |
Typedefs | |
| using | sub_expression_mapt = std::unordered_map< exprt, smt_termt, irep_hash > |
Post order visitation is used in order to construct the the smt terms bottom upwards without using recursion to traverse the input exprt. More... | |
Functions | |
| 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. More... | |
| template<typename target_typet > | |
| static bool | operands_are_of_type (const exprt &expr) |
| Ensures that all operands of the argument expression have related types. More... | |
| 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) |
| 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). More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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 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. More... | |
| 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. More... | |
| 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). More... | |
Typedef Documentation
◆ sub_expression_mapt
| using sub_expression_mapt = std::unordered_map<exprt, smt_termt, irep_hash> |
Post order visitation is used in order to construct the the smt terms bottom upwards without using recursion to traverse the input exprt.
Therefore the convert_expr_to_smt overload for any given type of exprt, will be passed a sub_expression_map which already contains the result of converting that expressions operands to smt terms. This has the advantages of -
- avoiding the deeply nested call stacks associated with recursion.
- supporting wider scope for the conversion of specific types of
exprt, without inflating the parameter list / scope for all conversions.
Definition at line 38 of file convert_expr_to_smt.cpp.
Function Documentation
◆ at_scope_exit()
| at_scope_exitt<functiont> at_scope_exit | ( | functiont | exit_function | ) |
Definition at line 1856 of file convert_expr_to_smt.cpp.
◆ convert_array_update_to_smt()
|
static |
Definition at line 1006 of file convert_expr_to_smt.cpp.
◆ convert_bit_vector_cast()
|
static |
Definition at line 243 of file convert_expr_to_smt.cpp.
◆ convert_c_bool_cast()
|
static |
Returns a cast to C bool expressed in smt terms.
Definition at line 148 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [1/73]
|
static |
Definition at line 1150 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [2/73]
|
static |
This conversion constructs a bit vector representation of the memory address. This address is composed of 2 concatenated bit vector components. The first part is the base object's unique identifier. The second is the offset into that object. For address of symbols the offset will be 0. The offset may be non-zero for cases such as the address of a member field of a struct or a the address of a non-zero index into an array.
Definition at line 866 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [3/73]
|
static |
Definition at line 480 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [4/73]
|
static |
Definition at line 919 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [5/73]
|
static |
Definition at line 1368 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [6/73]
|
static |
Definition at line 909 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [7/73]
|
static |
Definition at line 370 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [8/73]
|
static |
Definition at line 421 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [9/73]
|
static |
Definition at line 387 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [10/73]
|
static |
Definition at line 404 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [11/73]
|
static |
Definition at line 1433 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [12/73]
|
static |
Definition at line 1132 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [13/73]
|
static |
Definition at line 1141 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [14/73]
|
static |
Definition at line 356 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [15/73]
|
static |
Definition at line 330 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [16/73]
|
static |
Definition at line 1451 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [17/73]
|
static |
Definition at line 1460 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [18/73]
|
static |
Definition at line 750 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [19/73]
|
static |
Definition at line 519 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [20/73]
|
static |
Definition at line 828 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [21/73]
|
static |
Definition at line 1394 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [22/73]
| 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).
Definition at line 1921 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [23/73]
|
static |
Definition at line 1100 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [24/73]
|
static |
Definition at line 1109 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [25/73]
|
static |
Definition at line 272 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [26/73]
|
static |
Definition at line 1386 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [27/73]
|
static |
Definition at line 535 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [28/73]
|
static |
Definition at line 544 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [29/73]
|
static |
Definition at line 783 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [30/73]
|
static |
Definition at line 470 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [31/73]
|
static |
Definition at line 504 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [32/73]
|
static |
Definition at line 928 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [33/73]
|
static |
Definition at line 1049 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [34/73]
|
static |
Definition at line 1065 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [35/73]
|
static |
Definition at line 1168 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [36/73]
|
static |
Definition at line 1177 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [37/73]
|
static |
Definition at line 1159 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [38/73]
|
static |
Definition at line 1186 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [39/73]
|
static |
Definition at line 1427 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [40/73]
|
static |
Definition at line 1378 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [41/73]
|
static |
Definition at line 1040 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [42/73]
|
static |
Definition at line 694 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [43/73]
|
static |
Definition at line 1240 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [44/73]
|
static |
Definition at line 794 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [45/73]
|
static |
Definition at line 837 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [46/73]
|
static |
Definition at line 1272 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [47/73]
|
static |
Definition at line 123 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [48/73]
|
static |
Definition at line 512 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [49/73]
|
static |
Definition at line 527 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [50/73]
|
static |
Definition at line 1410 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [51/73]
|
static |
Definition at line 488 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [52/73]
|
static |
Definition at line 637 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [53/73]
|
static |
Definition at line 1211 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [54/73]
|
static |
Definition at line 1315 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [55/73]
|
static |
Definition at line 1338 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [56/73]
|
static |
Definition at line 1442 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [57/73]
|
static |
Definition at line 1478 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [58/73]
|
static |
Definition at line 1469 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [59/73]
|
static |
Definition at line 1123 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [60/73]
|
static |
Definition at line 978 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [61/73]
|
static |
Definition at line 1359 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [62/73]
|
static |
Definition at line 461 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [63/73]
|
static |
Definition at line 1091 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [64/73]
|
static |
Definition at line 281 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [65/73]
|
static |
Definition at line 117 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [66/73]
|
static |
Definition at line 255 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [67/73]
|
static |
Definition at line 436 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [68/73]
|
static |
Definition at line 452 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [69/73]
|
static |
Definition at line 290 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [70/73]
|
static |
Definition at line 1032 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [71/73]
|
static |
Definition at line 1402 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [72/73]
|
static |
Definition at line 1020 of file convert_expr_to_smt.cpp.
◆ convert_expr_to_smt() [73/73]
|
static |
Definition at line 496 of file convert_expr_to_smt.cpp.
◆ convert_multiary_operator_to_terms()
|
static |
Converts operator expressions with 2 or more operands to terms expressed as binary operator application.
- Parameters
-
expr The expression to convert. converted Map for looking up previously converted sub expressions. factory The factory function which makes applications of the relevant smt term, when applied to the term operands.
The conversion used is left associative for instances with 3 or more operands. The SMT standard / core theory version 2.6 actually supports applying the and, or and xor to 3 or more operands. However our internal smt_core_theoryt does not support this currently and converting to binary application has the advantage of making the order of evaluation explicit.
Definition at line 53 of file convert_expr_to_smt.cpp.
◆ convert_relational_to_smt()
|
static |
Definition at line 554 of file convert_expr_to_smt.cpp.
◆ convert_to_smt_shift()
|
static |
Definition at line 938 of file convert_expr_to_smt.cpp.
◆ convert_type_to_smt_sort() [1/4]
|
static |
Definition at line 93 of file convert_expr_to_smt.cpp.
◆ convert_type_to_smt_sort() [2/4]
|
static |
Definition at line 88 of file convert_expr_to_smt.cpp.
◆ convert_type_to_smt_sort() [3/4]
|
static |
Definition at line 83 of file convert_expr_to_smt.cpp.
◆ convert_type_to_smt_sort() [4/4]
Converts the type to an smt encoding of the same expression stored as sort ast (abstract syntax tree).
Definition at line 100 of file convert_expr_to_smt.cpp.
◆ dispatch_expr_to_smt_conversion()
|
static |
Definition at line 1487 of file convert_expr_to_smt.cpp.
◆ extension_for_type()
|
static |
Definition at line 161 of file convert_expr_to_smt.cpp.
◆ filtered_visit_post()
| 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.
Note that this function is based on the visit_post_template function.
Definition at line 1884 of file convert_expr_to_smt.cpp.
◆ lower_address_of_array_index()
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.
Definition at line 1862 of file convert_expr_to_smt.cpp.
◆ make_bitvector_resize_cast()
|
static |
Definition at line 174 of file convert_expr_to_smt.cpp.
◆ make_not_zero()
Makes a term which is true if input is not 0 / false.
Definition at line 135 of file convert_expr_to_smt.cpp.
◆ most_significant_bit_is_set()
Constructs a term which is true if the most significant bit of input is set.
Definition at line 1198 of file convert_expr_to_smt.cpp.
◆ operands_are_of_type()
|
static |
Ensures that all operands of the argument expression have related types.
- Parameters
-
expr The expression of which the operands we evaluate for type equality.
Definition at line 75 of file convert_expr_to_smt.cpp.
◆ try_relational_conversion()
|
static |
Definition at line 594 of file convert_expr_to_smt.cpp.
