convert_expr_to_smt.cpp File Reference

#include <solvers/smt2_incremental/convert_expr_to_smt.h>
#include <solvers/prop/literal_expr.h>
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
#include <solvers/smt2_incremental/smt_core_theory.h>
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/expr.h>
#include <util/expr_cast.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 <functional>
#include <numeric>

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 optionalt< smt_termt >	try_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). More...

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

expr	The expression to convert.
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 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.