cprover
Loading...
Searching...
No Matches
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).
 
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.
 
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 optionalt< smt_termttry_relational_conversion (const exprt &expr)
 
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).
 

Function Documentation

◆ convert_expr_to_smt() [1/63]

static smt_termt convert_expr_to_smt ( const abs_exprt absolute_value_of)
static

Definition at line 583 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [2/63]

static smt_termt convert_expr_to_smt ( const address_of_exprt address_of)
static

Definition at line 472 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [3/63]

static smt_termt convert_expr_to_smt ( const and_exprt and_expression)
static

Definition at line 222 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [4/63]

static smt_termt convert_expr_to_smt ( const array_comprehension_exprt array_comprehension)
static

Definition at line 486 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [5/63]

static smt_termt convert_expr_to_smt ( const array_exprt array_construction)
static

Definition at line 618 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [6/63]

static smt_termt convert_expr_to_smt ( const array_of_exprt array_of)
static

Definition at line 479 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [7/63]

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() [8/63]

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() [9/63]

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() [10/63]

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() [11/63]

static smt_termt convert_expr_to_smt ( const bswap_exprt byte_swap)
static

Definition at line 649 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [12/63]

static smt_termt convert_expr_to_smt ( const byte_extract_exprt byte_extraction)
static

Definition at line 569 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [13/63]

static smt_termt convert_expr_to_smt ( const byte_update_exprt byte_update)
static

Definition at line 576 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [14/63]

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() [15/63]

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() [16/63]

static smt_termt convert_expr_to_smt ( const count_leading_zeros_exprt count_leading_zeros)
static

Definition at line 664 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [17/63]

static smt_termt convert_expr_to_smt ( const count_trailing_zeros_exprt count_trailing_zeros)
static

Definition at line 672 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [18/63]

static smt_termt convert_expr_to_smt ( const div_exprt divide)
static

Definition at line 372 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [19/63]

static smt_termt convert_expr_to_smt ( const equal_exprt equal)
static

Definition at line 251 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [20/63]

static smt_termt convert_expr_to_smt ( const euclidean_mod_exprt euclidean_modulo)
static

Definition at line 445 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [21/63]

static smt_termt convert_expr_to_smt ( const exists_exprt exists)
static

Definition at line 637 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [22/63]

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

◆ convert_expr_to_smt() [23/63]

static smt_termt convert_expr_to_smt ( const extractbit_exprt extract_bit)
static

Definition at line 548 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [24/63]

static smt_termt convert_expr_to_smt ( const extractbits_exprt extract_bits)
static

Definition at line 555 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [25/63]

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() [26/63]

static smt_termt convert_expr_to_smt ( const forall_exprt for_all)
static

Definition at line 631 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [27/63]

static smt_termt convert_expr_to_smt ( const ieee_float_equal_exprt float_equal)
static

Definition at line 263 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [28/63]

static smt_termt convert_expr_to_smt ( const ieee_float_notequal_exprt float_not_equal)
static

Definition at line 271 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [29/63]

static smt_termt convert_expr_to_smt ( const ieee_float_op_exprt float_operation)
static

Definition at line 402 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [30/63]

static smt_termt convert_expr_to_smt ( const if_exprt if_expression)
static

Definition at line 186 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [31/63]

static smt_termt convert_expr_to_smt ( const implies_exprt implies)
static

Definition at line 240 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [32/63]

static smt_termt convert_expr_to_smt ( const index_exprt index)
static

Definition at line 493 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [33/63]

static smt_termt convert_expr_to_smt ( const is_dynamic_object_exprt is_dynamic_object)
static

Definition at line 526 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [34/63]

static smt_termt convert_expr_to_smt ( const is_invalid_pointer_exprt is_invalid_pointer)
static

Definition at line 534 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [35/63]

static smt_termt convert_expr_to_smt ( const isfinite_exprt is_finite_expr)
static

Definition at line 597 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [36/63]

static smt_termt convert_expr_to_smt ( const isinf_exprt is_infinite_expr)
static

Definition at line 604 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [37/63]

static smt_termt convert_expr_to_smt ( const isnan_exprt is_nan_expr)
static

Definition at line 590 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [38/63]

static smt_termt convert_expr_to_smt ( const isnormal_exprt is_normal_expr)
static

Definition at line 611 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [39/63]

static smt_termt convert_expr_to_smt ( const literal_exprt literal)
static

Definition at line 625 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [40/63]

static smt_termt convert_expr_to_smt ( const member_exprt member_extraction)
static

Definition at line 518 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [41/63]

static smt_termt convert_expr_to_smt ( const minus_exprt minus)
static

Definition at line 354 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [42/63]

static smt_termt convert_expr_to_smt ( const mod_exprt truncation_modulo)
static

Definition at line 411 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [43/63]

static smt_termt convert_expr_to_smt ( const mult_exprt multiply)
static

Definition at line 452 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [44/63]

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() [45/63]

static smt_termt convert_expr_to_smt ( const not_exprt logical_not)
static

Definition at line 246 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [46/63]

static smt_termt convert_expr_to_smt ( const notequal_exprt not_equal)
static

Definition at line 257 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [47/63]

static smt_termt convert_expr_to_smt ( const or_exprt or_expression)
static

Definition at line 228 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [48/63]

static smt_termt convert_expr_to_smt ( const plus_exprt plus)
static

Definition at line 337 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [49/63]

static smt_termt convert_expr_to_smt ( const popcount_exprt population_count)
static

Definition at line 656 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [50/63]

static smt_termt convert_expr_to_smt ( const replication_exprt replication)
static

Definition at line 562 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [51/63]

static smt_termt convert_expr_to_smt ( const shift_exprt shift)
static

Definition at line 499 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [52/63]

static smt_termt convert_expr_to_smt ( const sign_exprt is_negative)
static

Definition at line 179 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [53/63]

static smt_termt convert_expr_to_smt ( const string_constantt is_invalid_pointer)
static

Definition at line 541 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [54/63]

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() [55/63]

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() [56/63]

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() [57/63]

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() [58/63]

static smt_termt convert_expr_to_smt ( const unary_plus_exprt unary_plus)
static

Definition at line 172 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [59/63]

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() [60/63]

static smt_termt convert_expr_to_smt ( const update_exprt update)
static

Definition at line 512 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [61/63]

static smt_termt convert_expr_to_smt ( const vector_exprt vector)
static

Definition at line 643 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [62/63]

static smt_termt convert_expr_to_smt ( const with_exprt with)
static

Definition at line 506 of file convert_expr_to_smt.cpp.

◆ convert_expr_to_smt() [63/63]

static smt_termt convert_expr_to_smt ( const xor_exprt xor_expression)
static

Definition at line 234 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 206 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 279 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.

◆ try_relational_conversion()

static optionalt< smt_termt > try_relational_conversion ( const exprt expr)
static

Definition at line 300 of file convert_expr_to_smt.cpp.