36 if(
const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
40 if(
const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
56 "Generation of SMT formula for nondet symbol expression: " +
63 "Generation of SMT formula for type cast expression: " + cast.
pretty());
69 "Generation of SMT formula for floating point type cast expression: " +
76 "Generation of SMT formula for struct construction expression: " +
77 struct_construction.
pretty());
83 "Generation of SMT formula for union construction expression: " +
84 union_construction.
pretty());
104 const auto &width = bit_vector_sort.
bit_width();
116 sort.accept(converter);
123 "Generation of SMT formula for concatenation expression: " +
130 "Generation of SMT formula for bitwise and expression: " +
131 bitwise_and_expr.
pretty());
137 "Generation of SMT formula for bitwise or expression: " +
138 bitwise_or_expr.
pretty());
144 "Generation of SMT formula for bitwise xor expression: " +
151 "Generation of SMT formula for bitwise not expression: " +
157 const bool operand_is_bitvector =
159 if(operand_is_bitvector)
167 "Generation of SMT formula for unary minus expression: " +
175 "Generation of SMT formula for unary plus expression: " +
182 "Generation of SMT formula for \"is negative\" expression: " +
205template <
typename factoryt>
208 const factoryt &factory)
211 const auto operand_terms =
215 return std::accumulate(
216 ++operand_terms.begin(),
218 *operand_terms.begin(),
266 "Generation of SMT formula for floating point equality expression: " +
274 "Generation of SMT formula for floating point not equal expression: " +
275 float_not_equal.
pretty());
278template <
typename unsigned_factory_typet,
typename signed_factory_typet>
281 const unsigned_factory_typet &unsigned_factory,
282 const signed_factory_typet &signed_factory)
287 const typet operand_type = binary_relation.
lhs().
type();
291 return unsigned_factory(lhs, rhs);
293 return signed_factory(lhs, rhs);
296 "Generation of SMT formula for relational expression: " +
297 binary_relation.
pretty());
302 if(
const auto greater_than = expr_try_dynamic_cast<greater_than_exprt>(expr))
310 const auto greater_than_or_equal =
311 expr_try_dynamic_cast<greater_than_or_equal_exprt>(expr))
314 *greater_than_or_equal,
318 if(
const auto less_than = expr_try_dynamic_cast<less_than_exprt>(expr))
326 const auto less_than_or_equal =
327 expr_try_dynamic_cast<less_than_or_equal_exprt>(expr))
341 return can_cast_type<integer_bitvector_typet>(operand.type());
350 "Generation of SMT formula for plus expression: " + plus.
pretty());
356 const bool both_operands_bitvector =
360 if(both_operands_bitvector)
368 "Generation of SMT formula for minus expression: " + minus.
pretty());
374 const bool both_operands_bitvector =
378 const bool both_operands_unsigned =
382 if(both_operands_bitvector)
384 if(both_operands_unsigned)
398 "Generation of SMT formula for divide expression: " + divide.
pretty());
407 "Generation of SMT formula for floating point operation expression: " +
408 float_operation.
pretty());
413 const bool both_operands_bitvector =
417 const bool both_operands_unsigned =
421 if(both_operands_bitvector)
423 if(both_operands_unsigned)
439 "Generation of SMT formula for remainder (modulus) expression: " +
440 truncation_modulo.
pretty());
448 "Generation of SMT formula for euclidean modulo expression: " +
449 euclidean_modulo.
pretty());
458 return can_cast_type<integer_bitvector_typet>(operand.type());
467 "Generation of SMT formula for multiply expression: " +
475 "Generation of SMT formula for address of expression: " +
482 "Generation of SMT formula for array of expression: " + array_of.
pretty());
489 "Generation of SMT formula for array comprehension expression: " +
490 array_comprehension.
pretty());
496 "Generation of SMT formula for index expression: " + index.
pretty());
503 "Generation of SMT formula for shift expression: " + shift.
pretty());
509 "Generation of SMT formula for with expression: " + with.
pretty());
515 "Generation of SMT formula for update expression: " + update.
pretty());
521 "Generation of SMT formula for member extraction expression: " +
522 member_extraction.
pretty());
529 "Generation of SMT formula for is dynamic object expression: " +
530 is_dynamic_object.
pretty());
537 "Generation of SMT formula for is invalid pointer expression: " +
538 is_invalid_pointer.
pretty());
544 "Generation of SMT formula for is invalid pointer expression: " +
545 is_invalid_pointer.
pretty());
551 "Generation of SMT formula for extract bit expression: " +
558 "Generation of SMT formula for extract bits expression: " +
565 "Generation of SMT formula for bit vector replication expression: " +
572 "Generation of SMT formula for byte extract expression: " +
573 byte_extraction.
pretty());
579 "Generation of SMT formula for byte update expression: " +
586 "Generation of SMT formula for absolute value of expression: " +
587 absolute_value_of.
pretty());
593 "Generation of SMT formula for is not a number expression: " +
600 "Generation of SMT formula for is finite expression: " +
607 "Generation of SMT formula for is infinite expression: " +
608 is_infinite_expr.
pretty());
614 "Generation of SMT formula for is infinite expression: " +
621 "Generation of SMT formula for array construction expression: " +
622 array_construction.
pretty());
628 "Generation of SMT formula for literal expression: " + literal.
pretty());
634 "Generation of SMT formula for for all expression: " + for_all.
pretty());
640 "Generation of SMT formula for exists expression: " +
exists.pretty());
646 "Generation of SMT formula for vector expression: " + vector.
pretty());
652 "Generation of SMT formula for byte swap expression: " +
659 "Generation of SMT formula for population count expression: " +
660 population_count.
pretty());
667 "Generation of SMT formula for count leading zeros expression: " +
668 count_leading_zeros.
pretty());
675 "Generation of SMT formula for byte swap expression: " +
676 count_trailing_zeros.
pretty());
681 if(
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
685 if(
const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
689 if(
const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
694 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
698 if(
const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
702 if(
const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
706 if(
const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
711 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
715 if(
const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
719 if(
const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
723 if(
const auto bitwise_xor = expr_try_dynamic_cast<bitxor_exprt>(expr))
727 if(
const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
731 if(
const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
735 if(
const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
739 if(
const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
743 if(
const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
747 if(
const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
751 if(
const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
755 if(
const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
759 if(
const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
763 if(
const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
767 if(
const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
771 if(
const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
776 const auto float_equal =
777 expr_try_dynamic_cast<ieee_float_equal_exprt>(expr))
782 const auto float_not_equal =
783 expr_try_dynamic_cast<ieee_float_notequal_exprt>(expr))
789 return *converted_relational;
791 if(
const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
795 if(
const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
799 if(
const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
804 const auto float_operation =
805 expr_try_dynamic_cast<ieee_float_op_exprt>(expr))
809 if(
const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
814 const auto euclidean_modulo =
815 expr_try_dynamic_cast<euclidean_mod_exprt>(expr))
819 if(
const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
824 else if(expr.
id() == ID_floatbv_rem)
829 if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
833 if(
const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
838 const auto array_comprehension =
839 expr_try_dynamic_cast<array_comprehension_exprt>(expr))
843 if(
const auto index = expr_try_dynamic_cast<index_exprt>(expr))
847 if(
const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
851 if(
const auto with = expr_try_dynamic_cast<with_exprt>(expr))
855 if(
const auto update = expr_try_dynamic_cast<update_exprt>(expr))
859 if(
const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
864 else if(expr.
id()==ID_pointer_offset)
867 else if(expr.
id()==ID_pointer_object)
872 const auto is_dynamic_object =
873 expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
878 const auto is_invalid_pointer =
879 expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
883 if(
const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
887 if(
const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
891 if(
const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
895 if(
const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
900 const auto byte_extraction =
901 expr_try_dynamic_cast<byte_extract_exprt>(expr))
905 if(
const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
909 if(
const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
913 if(
const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
917 if(
const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
921 if(
const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
925 if(
const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
929 if(
const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
933 if(
const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
937 if(
const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
941 if(
const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
945 if(
const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
950 else if(expr.
id()==ID_object_size)
952 out <<
"|" << object_sizes[expr] <<
"|";
955 if(
const auto let = expr_try_dynamic_cast<let_exprt>(expr))
960 expr.
id() != ID_constraint_select_one,
961 "constraint_select_one is not expected in smt conversion: " +
963 if(
const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
967 if(
const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
972 const auto count_leading_zeros =
973 expr_try_dynamic_cast<count_leading_zeros_exprt>(expr))
978 const auto count_trailing_zeros =
979 expr_try_dynamic_cast<count_trailing_zeros_exprt>(expr))
985 "Generation of SMT formula for unknown kind of expression: " +
API to expression classes for bitvectors.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Expression classes for byte-level operators.
Operator to return the address of an object.
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
Array constructor from single element.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
The byte swap expression.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Concatenation of bit-vector operands.
A constant literal expression.
const irep_idt & get_value() const
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
Semantic type conversion from/to floating-point formats.
IEEE-floating-point equality.
IEEE floating-point disequality.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The trinary if-then-else operator.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A base class for multi-ary expressions Associativity is not specified.
Expression to hold a nondeterministic choice.
The plus expression Associativity is not specified.
The popcount (counting the number of bits set to 1) expression.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
std::size_t bit_width() const
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
static const smt_function_application_termt::factoryt< distinctt > distinct
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
static const smt_function_application_termt::factoryt< impliest > implies
static const smt_function_application_termt::factoryt< ort > make_or
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< andt > make_and
static const smt_function_application_termt::factoryt< xort > make_xor
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
Struct constructor from list of elements.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
The unary plus expression.
Union constructor from single element.
Operator to update elements in structs and arrays.
Vector constructor from list of elements.
Operator to update elements in structs and arrays.
static optionalt< smt_termt > try_relational_conversion(const exprt &expr)
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_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 applicati...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Templated functions to cast to specific exprt-derived classes.
API to expression classes for floating-point arithmetic.
API to expression classes for 'mathematical' expressions.
mini_bddt exists(const mini_bddt &u, const unsigned var)
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
nonstd::optional< T > optionalt
API to expression classes for Pointers.
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNIMPLEMENTED_FEATURE(FEATURE)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
binary_relation_exprt less_than(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
const constant_exprt & member_input
void visit(const smt_bool_sortt &) override
sort_based_literal_convertert(const constant_exprt &input)
optionalt< smt_termt > result