CBMC
Classes | Typedefs | Functions
convert_expr_to_smt.cpp File Reference
#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/smt_array_theory.h>
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
#include <solvers/smt2_incremental/smt_core_theory.h>
#include <functional>
#include <numeric>
+ 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_full_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 &not_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 optionalt< 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 &divide, 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 mp_integer power2 (unsigned exponent)
 
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 exprt &old, const exprt &index, const exprt &new_value, 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)
 
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 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)
 
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...
 
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)
 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_full_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()

template<typename functiont >
at_scope_exitt<functiont> at_scope_exit ( functiont  exit_function)

Definition at line 1812 of file convert_expr_to_smt.cpp.

◆ convert_array_update_to_smt()

static smt_termt convert_array_update_to_smt ( const exprt &  old,
const exprt &  index,
const exprt &  new_value,
const sub_expression_mapt &  converted 
)
static

Definition at line 1000 of file convert_expr_to_smt.cpp.

◆ convert_bit_vector_cast()

static smt_termt convert_bit_vector_cast ( const smt_termt &  from_term,
const typet &  from_type,
const bitvector_typet &  to_type 
)
static

Definition at line 239 of file convert_expr_to_smt.cpp.

◆ convert_c_bool_cast()

static smt_termt convert_c_bool_cast ( const smt_termt &  from_term,
const typet &  from_type,
const bitvector_typet &  to_type 
)
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/71]

static smt_termt convert_expr_to_smt ( const abs_exprt &  absolute_value_of,
const sub_expression_mapt &  converted 
)
static

Definition at line 1138 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [2/71]

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

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 871 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [3/71]

static smt_termt convert_expr_to_smt ( const and_exprt &  and_expression,
const sub_expression_mapt &  converted 
)
static

Definition at line 476 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [4/71]

static smt_termt convert_expr_to_smt ( const array_comprehension_exprt &  array_comprehension,
const sub_expression_mapt &  converted 
)
static

Definition at line 917 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [5/71]

static smt_termt convert_expr_to_smt ( const array_exprt &  array_construction,
const sub_expression_mapt &  converted 
)
static

Definition at line 1356 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [6/71]

static smt_termt convert_expr_to_smt ( const array_of_exprt &  array_of,
const sub_expression_mapt &  converted 
)
static

Definition at line 907 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [7/71]

static smt_termt convert_expr_to_smt ( const bitand_exprt &  bitwise_and_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 361 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [8/71]

static smt_termt convert_expr_to_smt ( const bitnot_exprt &  bitwise_not,
const sub_expression_mapt &  converted 
)
static

Definition at line 412 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [9/71]

static smt_termt convert_expr_to_smt ( const bitor_exprt &  bitwise_or_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 378 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [10/71]

static smt_termt convert_expr_to_smt ( const bitxor_exprt &  bitwise_xor,
const sub_expression_mapt &  converted 
)
static

Definition at line 395 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [11/71]

static smt_termt convert_expr_to_smt ( const bswap_exprt &  byte_swap,
const sub_expression_mapt &  converted 
)
static

Definition at line 1421 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [12/71]

static smt_termt convert_expr_to_smt ( const byte_extract_exprt &  byte_extraction,
const sub_expression_mapt &  converted 
)
static

Definition at line 1120 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [13/71]

static smt_termt convert_expr_to_smt ( const byte_update_exprt &  byte_update,
const sub_expression_mapt &  converted 
)
static

Definition at line 1129 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [14/71]

static smt_termt convert_expr_to_smt ( const concatenation_exprt &  concatenation,
const sub_expression_mapt &  converted 
)
static

Definition at line 352 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [15/71]

static smt_termt convert_expr_to_smt ( const constant_exprt &  constant_literal)
static

Definition at line 326 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [16/71]

static smt_termt convert_expr_to_smt ( const count_leading_zeros_exprt &  count_leading_zeros,
const sub_expression_mapt &  converted 
)
static

Definition at line 1439 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [17/71]

static smt_termt convert_expr_to_smt ( const count_trailing_zeros_exprt &  count_trailing_zeros,
const sub_expression_mapt &  converted 
)
static

Definition at line 1448 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [18/71]

static smt_termt convert_expr_to_smt ( const div_exprt &  divide,
const sub_expression_mapt &  converted 
)
static

Definition at line 746 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [19/71]

static smt_termt convert_expr_to_smt ( const equal_exprt &  equal,
const sub_expression_mapt &  converted 
)
static

Definition at line 515 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [20/71]

static smt_termt convert_expr_to_smt ( const euclidean_mod_exprt &  euclidean_modulo,
const sub_expression_mapt &  converted 
)
static

Definition at line 824 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [21/71]

static smt_termt convert_expr_to_smt ( const exists_exprt &  exists,
const sub_expression_mapt &  converted 
)
static

Definition at line 1382 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [22/71]

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 
)

Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree).

Definition at line 1837 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [23/71]

static smt_termt convert_expr_to_smt ( const extractbit_exprt &  extract_bit,
const sub_expression_mapt &  converted 
)
static

Definition at line 1088 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [24/71]

static smt_termt convert_expr_to_smt ( const extractbits_exprt &  extract_bits,
const sub_expression_mapt &  converted 
)
static

Definition at line 1097 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [25/71]

static smt_termt convert_expr_to_smt ( const floatbv_typecast_exprt &  float_cast,
const sub_expression_mapt &  converted 
)
static

Definition at line 268 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [26/71]

static smt_termt convert_expr_to_smt ( const forall_exprt &  for_all,
const sub_expression_mapt &  converted 
)
static

Definition at line 1374 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [27/71]

static smt_termt convert_expr_to_smt ( const ieee_float_equal_exprt &  float_equal,
const sub_expression_mapt &  converted 
)
static

Definition at line 531 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [28/71]

static smt_termt convert_expr_to_smt ( const ieee_float_notequal_exprt &  float_not_equal,
const sub_expression_mapt &  converted 
)
static

Definition at line 540 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [29/71]

static smt_termt convert_expr_to_smt ( const ieee_float_op_exprt &  float_operation,
const sub_expression_mapt &  converted 
)
static

Definition at line 779 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [30/71]

static smt_termt convert_expr_to_smt ( const if_exprt &  if_expression,
const sub_expression_mapt &  converted 
)
static

Definition at line 466 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [31/71]

static smt_termt convert_expr_to_smt ( const implies_exprt &  implies,
const sub_expression_mapt &  converted 
)
static

Definition at line 500 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [32/71]

static smt_termt convert_expr_to_smt ( const index_exprt &  index_of,
const sub_expression_mapt &  converted 
)
static

Definition at line 926 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [33/71]

static smt_termt convert_expr_to_smt ( const is_dynamic_object_exprt &  is_dynamic_object,
const sub_expression_mapt &  converted 
)
static

Definition at line 1044 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [34/71]

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

Definition at line 1053 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [35/71]

static smt_termt convert_expr_to_smt ( const isfinite_exprt &  is_finite_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 1156 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [36/71]

static smt_termt convert_expr_to_smt ( const isinf_exprt &  is_infinite_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 1165 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [37/71]

static smt_termt convert_expr_to_smt ( const isnan_exprt &  is_nan_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 1147 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [38/71]

static smt_termt convert_expr_to_smt ( const isnormal_exprt &  is_normal_expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 1174 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [39/71]

static smt_termt convert_expr_to_smt ( const let_exprt &  let,
const sub_expression_mapt &  converted 
)
static

Definition at line 1415 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [40/71]

static smt_termt convert_expr_to_smt ( const literal_exprt &  literal,
const sub_expression_mapt &  converted 
)
static

Definition at line 1366 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [41/71]

static smt_termt convert_expr_to_smt ( const member_exprt &  member_extraction,
const sub_expression_mapt &  converted 
)
static

Definition at line 1035 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [42/71]

static smt_termt convert_expr_to_smt ( const minus_exprt &  minus,
const sub_expression_mapt &  converted,
const type_size_mapt &  pointer_sizes 
)
static

Definition at line 690 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [43/71]

static smt_termt convert_expr_to_smt ( const minus_overflow_exprt &  minus_overflow,
const sub_expression_mapt &  converted 
)
static

Definition at line 1228 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [44/71]

static smt_termt convert_expr_to_smt ( const mod_exprt &  truncation_modulo,
const sub_expression_mapt &  converted 
)
static

Definition at line 790 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [45/71]

static smt_termt convert_expr_to_smt ( const mult_exprt &  multiply,
const sub_expression_mapt &  converted 
)
static

Definition at line 833 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [46/71]

static smt_termt convert_expr_to_smt ( const mult_overflow_exprt &  mult_overflow,
const sub_expression_mapt &  converted 
)
static

Definition at line 1260 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [47/71]

static smt_termt convert_expr_to_smt ( const nondet_symbol_exprt &  nondet_symbol,
const sub_expression_mapt &  converted 
)
static

Definition at line 123 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [48/71]

static smt_termt convert_expr_to_smt ( const not_exprt &  logical_not,
const sub_expression_mapt &  converted 
)
static

Definition at line 508 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [49/71]

static smt_termt convert_expr_to_smt ( const notequal_exprt &  not_equal,
const sub_expression_mapt &  converted 
)
static

Definition at line 523 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [50/71]

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

Definition at line 1398 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [51/71]

static smt_termt convert_expr_to_smt ( const or_exprt &  or_expression,
const sub_expression_mapt &  converted 
)
static

Definition at line 484 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [52/71]

static smt_termt convert_expr_to_smt ( const plus_exprt &  plus,
const sub_expression_mapt &  converted,
const type_size_mapt &  pointer_sizes 
)
static

Definition at line 633 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [53/71]

static smt_termt convert_expr_to_smt ( const plus_overflow_exprt &  plus_overflow,
const sub_expression_mapt &  converted 
)
static

Definition at line 1199 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [54/71]

static smt_termt convert_expr_to_smt ( const pointer_object_exprt &  pointer_object,
const sub_expression_mapt &  converted 
)
static

Definition at line 1303 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [55/71]

static smt_termt convert_expr_to_smt ( const pointer_offset_exprt &  pointer_offset,
const sub_expression_mapt &  converted 
)
static

Definition at line 1326 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [56/71]

static smt_termt convert_expr_to_smt ( const popcount_exprt &  population_count,
const sub_expression_mapt &  converted 
)
static

Definition at line 1430 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [57/71]

static smt_termt convert_expr_to_smt ( const replication_exprt &  replication,
const sub_expression_mapt &  converted 
)
static

Definition at line 1111 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [58/71]

static smt_termt convert_expr_to_smt ( const shift_exprt &  shift,
const sub_expression_mapt &  converted 
)
static

Definition at line 972 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [59/71]

static smt_termt convert_expr_to_smt ( const shl_overflow_exprt &  shl_overflow,
const sub_expression_mapt &  converted 
)
static

Definition at line 1347 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [60/71]

static smt_termt convert_expr_to_smt ( const sign_exprt &  is_negative,
const sub_expression_mapt &  converted 
)
static

Definition at line 457 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [61/71]

static smt_termt convert_expr_to_smt ( const string_constantt &  string_constant,
const sub_expression_mapt &  converted 
)
static

Definition at line 1079 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [62/71]

static smt_termt convert_expr_to_smt ( const struct_exprt &  struct_construction,
const sub_expression_mapt &  converted 
)
static

Definition at line 277 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [63/71]

static smt_termt convert_expr_to_smt ( const symbol_exprt &  symbol_expr)
static

Definition at line 117 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [64/71]

static smt_termt convert_expr_to_smt ( const typecast_exprt &  cast,
const sub_expression_mapt &  converted 
)
static

Definition at line 251 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [65/71]

static smt_termt convert_expr_to_smt ( const unary_minus_exprt &  unary_minus,
const sub_expression_mapt &  converted 
)
static

Definition at line 430 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [66/71]

static smt_termt convert_expr_to_smt ( const unary_plus_exprt &  unary_plus,
const sub_expression_mapt &  converted 
)
static

Definition at line 448 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [67/71]

static smt_termt convert_expr_to_smt ( const union_exprt &  union_construction,
const sub_expression_mapt &  converted 
)
static

Definition at line 286 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [68/71]

static smt_termt convert_expr_to_smt ( const update_exprt &  update,
const sub_expression_mapt &  converted 
)
static

Definition at line 1027 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [69/71]

static smt_termt convert_expr_to_smt ( const vector_exprt &  vector,
const sub_expression_mapt &  converted 
)
static

Definition at line 1390 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [70/71]

static smt_termt convert_expr_to_smt ( const with_exprt &  with,
const sub_expression_mapt &  converted 
)
static

Definition at line 1012 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [71/71]

static smt_termt convert_expr_to_smt ( const xor_exprt &  xor_expression,
const sub_expression_mapt &  converted 
)
static

Definition at line 492 of file convert_expr_to_smt.cpp.

◆ convert_multiary_operator_to_terms()

template<typename factoryt >
static smt_termt convert_multiary_operator_to_terms ( const multi_ary_exprt &  expr,
const sub_expression_mapt &  converted,
const factoryt &  factory 
)
static

Converts operator expressions with 2 or more operands to terms expressed as binary operator application.

Parameters
exprThe expression to convert.
convertedMap for looking up previously converted sub expressions.
factoryThe 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()

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

Definition at line 550 of file convert_expr_to_smt.cpp.

◆ convert_to_smt_shift()

template<typename factoryt , typename shiftt >
static smt_termt convert_to_smt_shift ( const factoryt &  factory,
const shiftt &  shift,
const sub_expression_mapt &  converted 
)
static

Definition at line 936 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [1/4]

static smt_sortt convert_type_to_smt_sort ( const array_typet &  type)
static

Definition at line 93 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [2/4]

static smt_sortt convert_type_to_smt_sort ( const bitvector_typet &  type)
static

Definition at line 88 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [3/4]

static smt_sortt convert_type_to_smt_sort ( const bool_typet &  type)
static

Definition at line 83 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [4/4]

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).

Definition at line 100 of file convert_expr_to_smt.cpp.

◆ dispatch_expr_to_smt_conversion()

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 
)
static

Definition at line 1457 of file convert_expr_to_smt.cpp.

◆ extension_for_type()

static std::function<std::function<smt_termt(smt_termt)>std::size_t)> extension_for_type ( const typet &  type)
static

Definition at line 161 of file convert_expr_to_smt.cpp.

◆ lower_address_of_array_index()

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.

Definition at line 1818 of file convert_expr_to_smt.cpp.

◆ make_bitvector_resize_cast()

static smt_termt make_bitvector_resize_cast ( const smt_termt &  from_term,
const bitvector_typet &  from_type,
const bitvector_typet &  to_type 
)
static

Definition at line 170 of file convert_expr_to_smt.cpp.

◆ make_not_zero()

static smt_termt make_not_zero ( const smt_termt &  input,
const typet &  source_type 
)
static

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()

static smt_termt most_significant_bit_is_set ( const smt_termt &  input)
static

Constructs a term which is true if the most significant bit of input is set.

Definition at line 1186 of file convert_expr_to_smt.cpp.

◆ operands_are_of_type()

template<typename target_typet >
static bool operands_are_of_type ( const exprt &  expr)
static

Ensures that all operands of the argument expression have related types.

Parameters
exprThe expression of which the operands we evaluate for type equality.

Definition at line 75 of file convert_expr_to_smt.cpp.

◆ power2()

static mp_integer power2 ( unsigned  exponent)
static

Definition at line 856 of file convert_expr_to_smt.cpp.

◆ try_relational_conversion()

static optionalt<smt_termt> try_relational_conversion ( const exprt &  expr,
const sub_expression_mapt &  converted 
)
static

Definition at line 590 of file convert_expr_to_smt.cpp.