cprover
convert_expr_to_smt.cpp File Reference
+ Include dependency graph for convert_expr_to_smt.cpp:

Go to the source code of this file.

Classes

struct  sort_based_literal_convertert
 

Functions

static smt_sortt convert_type_to_smt_sort (const bool_typet &type)
 
static smt_sortt convert_type_to_smt_sort (const bitvector_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)
 
static smt_termt convert_expr_to_smt (const typecast_exprt &cast)
 
static smt_termt convert_expr_to_smt (const floatbv_typecast_exprt &float_cast)
 
static smt_termt convert_expr_to_smt (const struct_exprt &struct_construction)
 
static smt_termt convert_expr_to_smt (const union_exprt &union_construction)
 
static smt_termt convert_expr_to_smt (const constant_exprt &constant_literal)
 
static smt_termt convert_expr_to_smt (const concatenation_exprt &concatenation)
 
static smt_termt convert_expr_to_smt (const bitand_exprt &bitwise_and_expr)
 
static smt_termt convert_expr_to_smt (const bitor_exprt &bitwise_or_expr)
 
static smt_termt convert_expr_to_smt (const bitxor_exprt &bitwise_xor)
 
static smt_termt convert_expr_to_smt (const bitnot_exprt &bitwise_not)
 
static smt_termt convert_expr_to_smt (const unary_minus_exprt &unary_minus)
 
static smt_termt convert_expr_to_smt (const unary_plus_exprt &unary_plus)
 
static smt_termt convert_expr_to_smt (const sign_exprt &is_negative)
 
static smt_termt convert_expr_to_smt (const if_exprt &if_expression)
 
template<typename factoryt >
static smt_termt convert_multiary_operator_to_terms (const multi_ary_exprt &expr, const factoryt &factory)
 Converts operator expressions with 2 or more operands to terms expressed as binary operator application. More...
 
static smt_termt convert_expr_to_smt (const and_exprt &and_expression)
 
static smt_termt convert_expr_to_smt (const or_exprt &or_expression)
 
static smt_termt convert_expr_to_smt (const xor_exprt &xor_expression)
 
static smt_termt convert_expr_to_smt (const implies_exprt &implies)
 
static smt_termt convert_expr_to_smt (const not_exprt &logical_not)
 
static smt_termt convert_expr_to_smt (const equal_exprt &equal)
 
static smt_termt convert_expr_to_smt (const notequal_exprt &not_equal)
 
static smt_termt convert_expr_to_smt (const ieee_float_equal_exprt &float_equal)
 
static smt_termt convert_expr_to_smt (const ieee_float_notequal_exprt &float_not_equal)
 
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)
 
static smt_termt convert_expr_to_smt (const binary_relation_exprt &binary_relation)
 
static smt_termt convert_expr_to_smt (const plus_exprt &plus)
 
static smt_termt convert_expr_to_smt (const minus_exprt &minus)
 
static smt_termt convert_expr_to_smt (const div_exprt &divide)
 
static smt_termt convert_expr_to_smt (const ieee_float_op_exprt &float_operation)
 
static smt_termt convert_expr_to_smt (const mod_exprt &truncation_modulo)
 
static smt_termt convert_expr_to_smt (const euclidean_mod_exprt &euclidean_modulo)
 
static smt_termt convert_expr_to_smt (const mult_exprt &multiply)
 
static smt_termt convert_expr_to_smt (const address_of_exprt &address_of)
 
static smt_termt convert_expr_to_smt (const array_of_exprt &array_of)
 
static smt_termt convert_expr_to_smt (const array_comprehension_exprt &array_comprehension)
 
static smt_termt convert_expr_to_smt (const index_exprt &index)
 
static smt_termt convert_expr_to_smt (const shift_exprt &shift)
 
static smt_termt convert_expr_to_smt (const with_exprt &with)
 
static smt_termt convert_expr_to_smt (const update_exprt &update)
 
static smt_termt convert_expr_to_smt (const member_exprt &member_extraction)
 
static smt_termt convert_expr_to_smt (const is_dynamic_object_exprt &is_dynamic_object)
 
static smt_termt convert_expr_to_smt (const is_invalid_pointer_exprt &is_invalid_pointer)
 
static smt_termt convert_expr_to_smt (const string_constantt &is_invalid_pointer)
 
static smt_termt convert_expr_to_smt (const extractbit_exprt &extract_bit)
 
static smt_termt convert_expr_to_smt (const extractbits_exprt &extract_bits)
 
static smt_termt convert_expr_to_smt (const replication_exprt &replication)
 
static smt_termt convert_expr_to_smt (const byte_extract_exprt &byte_extraction)
 
static smt_termt convert_expr_to_smt (const byte_update_exprt &byte_update)
 
static smt_termt convert_expr_to_smt (const abs_exprt &absolute_value_of)
 
static smt_termt convert_expr_to_smt (const isnan_exprt &is_nan_expr)
 
static smt_termt convert_expr_to_smt (const isfinite_exprt &is_finite_expr)
 
static smt_termt convert_expr_to_smt (const isinf_exprt &is_infinite_expr)
 
static smt_termt convert_expr_to_smt (const isnormal_exprt &is_normal_expr)
 
static smt_termt convert_expr_to_smt (const array_exprt &array_construction)
 
static smt_termt convert_expr_to_smt (const literal_exprt &literal)
 
static smt_termt convert_expr_to_smt (const forall_exprt &for_all)
 
static smt_termt convert_expr_to_smt (const exists_exprt &exists)
 
static smt_termt convert_expr_to_smt (const vector_exprt &vector)
 
static smt_termt convert_expr_to_smt (const bswap_exprt &byte_swap)
 
static smt_termt convert_expr_to_smt (const popcount_exprt &population_count)
 
static smt_termt convert_expr_to_smt (const count_leading_zeros_exprt &count_leading_zeros)
 
static smt_termt convert_expr_to_smt (const count_trailing_zeros_exprt &count_trailing_zeros)
 
smt_termt convert_expr_to_smt (const exprt &expr)
 Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree). More...
 

Function Documentation

◆ convert_expr_to_smt() [1/64]

static smt_termt convert_expr_to_smt ( const abs_exprt absolute_value_of)
static

Definition at line 485 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [2/64]

static smt_termt convert_expr_to_smt ( const address_of_exprt address_of)
static

Definition at line 374 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [3/64]

static smt_termt convert_expr_to_smt ( const and_exprt and_expression)
static

Definition at line 212 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [4/64]

static smt_termt convert_expr_to_smt ( const array_comprehension_exprt array_comprehension)
static

Definition at line 388 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [5/64]

static smt_termt convert_expr_to_smt ( const array_exprt array_construction)
static

Definition at line 520 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [6/64]

static smt_termt convert_expr_to_smt ( const array_of_exprt array_of)
static

Definition at line 381 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [7/64]

static smt_termt convert_expr_to_smt ( const binary_relation_exprt binary_relation)
static

Definition at line 291 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [8/64]

static smt_termt convert_expr_to_smt ( const bitand_exprt bitwise_and_expr)
static

Definition at line 127 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [9/64]

static smt_termt convert_expr_to_smt ( const bitnot_exprt bitwise_not)
static

Definition at line 148 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [10/64]

static smt_termt convert_expr_to_smt ( const bitor_exprt bitwise_or_expr)
static

Definition at line 134 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [11/64]

static smt_termt convert_expr_to_smt ( const bitxor_exprt bitwise_xor)
static

Definition at line 141 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [12/64]

static smt_termt convert_expr_to_smt ( const bswap_exprt byte_swap)
static

Definition at line 551 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [13/64]

static smt_termt convert_expr_to_smt ( const byte_extract_exprt byte_extraction)
static

Definition at line 471 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [14/64]

static smt_termt convert_expr_to_smt ( const byte_update_exprt byte_update)
static

Definition at line 478 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [15/64]

static smt_termt convert_expr_to_smt ( const concatenation_exprt concatenation)
static

Definition at line 120 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [16/64]

static smt_termt convert_expr_to_smt ( const constant_exprt constant_literal)
static

Definition at line 112 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [17/64]

static smt_termt convert_expr_to_smt ( const count_leading_zeros_exprt count_leading_zeros)
static

Definition at line 566 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [18/64]

static smt_termt convert_expr_to_smt ( const count_trailing_zeros_exprt count_trailing_zeros)
static

Definition at line 574 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [19/64]

static smt_termt convert_expr_to_smt ( const div_exprt divide)
static

Definition at line 338 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [20/64]

static smt_termt convert_expr_to_smt ( const equal_exprt equal)
static

Definition at line 241 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [21/64]

static smt_termt convert_expr_to_smt ( const euclidean_mod_exprt euclidean_modulo)
static

Definition at line 361 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [22/64]

static smt_termt convert_expr_to_smt ( const exists_exprt exists)
static

Definition at line 539 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [23/64]

smt_termt convert_expr_to_smt ( const exprt expr)

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

Definition at line 581 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [24/64]

static smt_termt convert_expr_to_smt ( const extractbit_exprt extract_bit)
static

Definition at line 450 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [25/64]

static smt_termt convert_expr_to_smt ( const extractbits_exprt extract_bits)
static

Definition at line 457 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [26/64]

static smt_termt convert_expr_to_smt ( const floatbv_typecast_exprt float_cast)
static

Definition at line 66 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [27/64]

static smt_termt convert_expr_to_smt ( const forall_exprt for_all)
static

Definition at line 533 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [28/64]

static smt_termt convert_expr_to_smt ( const ieee_float_equal_exprt float_equal)
static

Definition at line 253 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [29/64]

static smt_termt convert_expr_to_smt ( const ieee_float_notequal_exprt float_not_equal)
static

Definition at line 261 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [30/64]

static smt_termt convert_expr_to_smt ( const ieee_float_op_exprt float_operation)
static

Definition at line 344 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [31/64]

static smt_termt convert_expr_to_smt ( const if_exprt if_expression)
static

Definition at line 176 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [32/64]

static smt_termt convert_expr_to_smt ( const implies_exprt implies)
static

Definition at line 230 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [33/64]

static smt_termt convert_expr_to_smt ( const index_exprt index)
static

Definition at line 395 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [34/64]

static smt_termt convert_expr_to_smt ( const is_dynamic_object_exprt is_dynamic_object)
static

Definition at line 428 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [35/64]

static smt_termt convert_expr_to_smt ( const is_invalid_pointer_exprt is_invalid_pointer)
static

Definition at line 436 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [36/64]

static smt_termt convert_expr_to_smt ( const isfinite_exprt is_finite_expr)
static

Definition at line 499 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [37/64]

static smt_termt convert_expr_to_smt ( const isinf_exprt is_infinite_expr)
static

Definition at line 506 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [38/64]

static smt_termt convert_expr_to_smt ( const isnan_exprt is_nan_expr)
static

Definition at line 492 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [39/64]

static smt_termt convert_expr_to_smt ( const isnormal_exprt is_normal_expr)
static

Definition at line 513 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [40/64]

static smt_termt convert_expr_to_smt ( const literal_exprt literal)
static

Definition at line 527 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [41/64]

static smt_termt convert_expr_to_smt ( const member_exprt member_extraction)
static

Definition at line 420 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [42/64]

static smt_termt convert_expr_to_smt ( const minus_exprt minus)
static

Definition at line 332 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [43/64]

static smt_termt convert_expr_to_smt ( const mod_exprt truncation_modulo)
static

Definition at line 353 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [44/64]

static smt_termt convert_expr_to_smt ( const mult_exprt multiply)
static

Definition at line 368 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [45/64]

static smt_termt convert_expr_to_smt ( const nondet_symbol_exprt nondet_symbol)
static

Definition at line 53 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [46/64]

static smt_termt convert_expr_to_smt ( const not_exprt logical_not)
static

Definition at line 236 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [47/64]

static smt_termt convert_expr_to_smt ( const notequal_exprt not_equal)
static

Definition at line 247 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [48/64]

static smt_termt convert_expr_to_smt ( const or_exprt or_expression)
static

Definition at line 218 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [49/64]

static smt_termt convert_expr_to_smt ( const plus_exprt plus)
static

Definition at line 326 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [50/64]

static smt_termt convert_expr_to_smt ( const popcount_exprt population_count)
static

Definition at line 558 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [51/64]

static smt_termt convert_expr_to_smt ( const replication_exprt replication)
static

Definition at line 464 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [52/64]

static smt_termt convert_expr_to_smt ( const shift_exprt shift)
static

Definition at line 401 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [53/64]

static smt_termt convert_expr_to_smt ( const sign_exprt is_negative)
static

Definition at line 169 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [54/64]

static smt_termt convert_expr_to_smt ( const string_constantt is_invalid_pointer)
static

Definition at line 443 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [55/64]

static smt_termt convert_expr_to_smt ( const struct_exprt struct_construction)
static

Definition at line 73 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [56/64]

static smt_termt convert_expr_to_smt ( const symbol_exprt symbol_expr)
static

Definition at line 47 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [57/64]

static smt_termt convert_expr_to_smt ( const typecast_exprt cast)
static

Definition at line 60 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [58/64]

static smt_termt convert_expr_to_smt ( const unary_minus_exprt unary_minus)
static

Definition at line 155 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [59/64]

static smt_termt convert_expr_to_smt ( const unary_plus_exprt unary_plus)
static

Definition at line 162 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [60/64]

static smt_termt convert_expr_to_smt ( const union_exprt union_construction)
static

Definition at line 80 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [61/64]

static smt_termt convert_expr_to_smt ( const update_exprt update)
static

Definition at line 414 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [62/64]

static smt_termt convert_expr_to_smt ( const vector_exprt vector)
static

Definition at line 545 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [63/64]

static smt_termt convert_expr_to_smt ( const with_exprt with)
static

Definition at line 408 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [64/64]

static smt_termt convert_expr_to_smt ( const xor_exprt xor_expression)
static

Definition at line 224 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 factoryt &  factory 
)
static

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

Parameters
exprThe expression to convert.
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 196 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 
)
static

Definition at line 269 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [1/3]

static smt_sortt convert_type_to_smt_sort ( const bitvector_typet type)
static

Definition at line 29 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [2/3]

static smt_sortt convert_type_to_smt_sort ( const bool_typet type)
static

Definition at line 24 of file convert_expr_to_smt.cpp.

◆ convert_type_to_smt_sort() [3/3]

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