Go to the documentation of this file.
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))
50 "Generation of SMT formula for symbol expression: " + symbol_expr.
pretty());
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: " +
158 "Generation of SMT formula for unary minus expression: " +
165 "Generation of SMT formula for unary plus expression: " +
172 "Generation of SMT formula for \"is negative\" expression: " +
195 template <
typename factoryt>
198 const factoryt &factory)
201 const auto operand_terms =
205 return std::accumulate(
206 ++operand_terms.begin(),
208 *operand_terms.begin(),
256 "Generation of SMT formula for floating point equality expression: " +
264 "Generation of SMT formula for floating point not equal expression: " +
265 float_not_equal.
pretty());
268 template <
typename unsigned_factory_typet,
typename signed_factory_typet>
271 const unsigned_factory_typet &unsigned_factory,
272 const signed_factory_typet &signed_factory)
277 const typet operand_type = binary_relation.
lhs().
type();
281 return unsigned_factory(lhs, rhs);
283 return signed_factory(lhs, rhs);
286 "Generation of SMT formula for relational expression: " +
287 binary_relation.
pretty());
297 smt_bit_vector_theoryt::unsigned_greater_than,
298 smt_bit_vector_theoryt::signed_greater_than);
304 smt_bit_vector_theoryt::unsigned_greater_than_or_equal,
305 smt_bit_vector_theoryt::signed_greater_than_or_equal);
311 smt_bit_vector_theoryt::unsigned_less_than,
312 smt_bit_vector_theoryt::signed_less_than);
318 smt_bit_vector_theoryt::unsigned_less_than_or_equal,
319 smt_bit_vector_theoryt::signed_less_than_or_equal);
322 "Generation of SMT formula for binary relation expression: " +
323 binary_relation.
pretty());
329 "Generation of SMT formula for plus expression: " + plus.
pretty());
335 "Generation of SMT formula for minus expression: " + minus.
pretty());
341 "Generation of SMT formula for divide expression: " + divide.
pretty());
349 "Generation of SMT formula for floating point operation expression: " +
350 float_operation.
pretty());
356 "Generation of SMT formula for truncation modulo expression: " +
357 truncation_modulo.
pretty());
364 "Generation of SMT formula for euclidean modulo expression: " +
365 euclidean_modulo.
pretty());
371 "Generation of SMT formula for multiply expression: " + multiply.
pretty());
377 "Generation of SMT formula for address of expression: " +
384 "Generation of SMT formula for array of expression: " + array_of.
pretty());
391 "Generation of SMT formula for array comprehension expression: " +
392 array_comprehension.
pretty());
398 "Generation of SMT formula for index expression: " + index.
pretty());
405 "Generation of SMT formula for shift expression: " + shift.
pretty());
411 "Generation of SMT formula for with expression: " + with.
pretty());
417 "Generation of SMT formula for update expression: " + update.
pretty());
423 "Generation of SMT formula for member extraction expression: " +
424 member_extraction.
pretty());
431 "Generation of SMT formula for is dynamic object expression: " +
432 is_dynamic_object.
pretty());
439 "Generation of SMT formula for is invalid pointer expression: " +
440 is_invalid_pointer.
pretty());
446 "Generation of SMT formula for is invalid pointer expression: " +
447 is_invalid_pointer.
pretty());
453 "Generation of SMT formula for extract bit expression: " +
460 "Generation of SMT formula for extract bits expression: " +
467 "Generation of SMT formula for bit vector replication expression: " +
474 "Generation of SMT formula for byte extract expression: " +
475 byte_extraction.
pretty());
481 "Generation of SMT formula for byte update expression: " +
488 "Generation of SMT formula for absolute value of expression: " +
489 absolute_value_of.
pretty());
495 "Generation of SMT formula for is not a number expression: " +
502 "Generation of SMT formula for is finite expression: " +
509 "Generation of SMT formula for is infinite expression: " +
510 is_infinite_expr.
pretty());
516 "Generation of SMT formula for is infinite expression: " +
523 "Generation of SMT formula for array construction expression: " +
524 array_construction.
pretty());
530 "Generation of SMT formula for literal expression: " + literal.
pretty());
536 "Generation of SMT formula for for all expression: " + for_all.
pretty());
542 "Generation of SMT formula for exists expression: " +
exists.pretty());
548 "Generation of SMT formula for vector expression: " + vector.
pretty());
554 "Generation of SMT formula for byte swap expression: " +
561 "Generation of SMT formula for population count expression: " +
562 population_count.
pretty());
569 "Generation of SMT formula for count leading zeros expression: " +
570 count_leading_zeros.
pretty());
577 "Generation of SMT formula for byte swap expression: " +
578 count_trailing_zeros.
pretty());
583 if(
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
587 if(
const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
591 if(
const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
596 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
600 if(
const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
604 if(
const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
608 if(
const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
613 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
617 if(
const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
621 if(
const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
625 if(
const auto bitwise_xor = expr_try_dynamic_cast<bitxor_exprt>(expr))
629 if(
const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
633 if(
const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
637 if(
const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
641 if(
const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
645 if(
const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
649 if(
const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
653 if(
const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
657 if(
const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
661 if(
const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
665 if(
const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
669 if(
const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
673 if(
const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
678 const auto float_equal =
679 expr_try_dynamic_cast<ieee_float_equal_exprt>(expr))
684 const auto float_not_equal =
685 expr_try_dynamic_cast<ieee_float_notequal_exprt>(expr))
690 const auto binary_relation =
691 expr_try_dynamic_cast<binary_relation_exprt>(expr))
695 if(
const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
699 if(
const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
703 if(
const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
708 const auto float_operation =
709 expr_try_dynamic_cast<ieee_float_op_exprt>(expr))
713 if(
const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
718 const auto euclidean_modulo =
719 expr_try_dynamic_cast<euclidean_mod_exprt>(expr))
723 if(
const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
728 else if(expr.
id() == ID_floatbv_rem)
733 if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
737 if(
const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
742 const auto array_comprehension =
743 expr_try_dynamic_cast<array_comprehension_exprt>(expr))
747 if(
const auto index = expr_try_dynamic_cast<index_exprt>(expr))
751 if(
const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
755 if(
const auto with = expr_try_dynamic_cast<with_exprt>(expr))
759 if(
const auto update = expr_try_dynamic_cast<update_exprt>(expr))
763 if(
const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
768 else if(expr.
id()==ID_pointer_offset)
771 else if(expr.
id()==ID_pointer_object)
776 const auto is_dynamic_object =
777 expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
782 const auto is_invalid_pointer =
783 expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
787 if(
const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
791 if(
const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
795 if(
const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
799 if(
const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
804 const auto byte_extraction =
805 expr_try_dynamic_cast<byte_extract_exprt>(expr))
809 if(
const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
813 if(
const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
817 if(
const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
821 if(
const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
825 if(
const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
829 if(
const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
833 if(
const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
837 if(
const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
841 if(
const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
845 if(
const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
849 if(
const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
854 else if(expr.
id()==ID_object_size)
856 out <<
"|" << object_sizes[expr] <<
"|";
859 if(
const auto let = expr_try_dynamic_cast<let_exprt>(expr))
864 expr.
id() != ID_constraint_select_one,
865 "constraint_select_one is not expected in smt conversion: " +
867 if(
const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
871 if(
const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
876 const auto count_leading_zeros =
877 expr_try_dynamic_cast<count_leading_zeros_exprt>(expr))
882 const auto count_trailing_zeros =
883 expr_try_dynamic_cast<count_trailing_zeros_exprt>(expr))
889 "Generation of SMT formula for unknown kind of expression: " +
Operator to update elements in structs and arrays.
A base class for multi-ary expressions Associativity is not specified.
mini_bddt exists(const mini_bddt &u, const unsigned var)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Expression to hold a nondeterministic choice.
#define UNIMPLEMENTED_FEATURE(FEATURE)
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
static const smt_function_application_termt::factoryt< distinctt > distinct
The trinary if-then-else operator.
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Evaluates to true if the operand is a pointer to a dynamic object.
Various predicates over pointers in programs.
static const smt_function_application_termt::factoryt< ort > make_or
Union constructor from single element.
static const smt_function_application_termt::factoryt< xort > make_xor
The plus expression Associativity is not specified.
Base class for all expressions.
static const smt_function_application_termt::factoryt< nott > make_not
Sign of an expression Predicate is true if _op is negative, false otherwise.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
Concatenation of bit-vector operands.
Vector constructor from list of elements.
bool is_true() const
Return whether the expression is a constant representing true.
Expression to hold a symbol (variable)
optionalt< smt_termt > result
static const smt_function_application_termt::factoryt< impliest > implies
Evaluates to true if the operand is finite.
std::size_t bit_width() const
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Struct constructor from list of elements.
IEEE floating-point disequality.
typet & type()
Return the type of the expression.
Expression classes for byte-level operators.
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)
Semantic type conversion from/to floating-point formats.
#define PRECONDITION(CONDITION)
Array constructor from single element.
API to expression classes for Pointers.
Binary multiplication Associativity is not specified.
void visit(const smt_bool_sortt &) override
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
The unary minus expression.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
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...
API to expression classes for floating-point arithmetic.
The unary plus expression.
bool can_cast_expr< less_than_exprt >(const exprt &base)
nonstd::optional< T > optionalt
Operator to update elements in structs and arrays.
static const smt_function_application_termt::factoryt< andt > make_and
std::size_t get_width() const
Bit-wise negation of bit-vectors.
Extract member of struct or union.
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
A base class for shift and rotate operators.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
const constant_exprt & member_input
Base class of fixed-width bit-vector types.
Evaluates to true if the operand is infinite.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Templated functions to cast to specific exprt-derived classes.
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
static const smt_function_application_termt::factoryt< equalt > equal
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The byte swap expression.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
Expression to define a mapping from an argument (index) to elements.
A constant literal expression.
IEEE-floating-point equality.
bool can_cast_expr< greater_than_exprt >(const exprt &base)
API to expression classes.
const irep_idt & get_value() const
sort_based_literal_convertert(const constant_exprt &input)
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
Array constructor from list of elements.
ranget< iteratort > make_range(iteratort begin, iteratort end)
Evaluates to true if the operand is a normal number.
API to expression classes for bitvectors.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
Evaluates to true if the operand is NaN.
API to expression classes for 'mathematical' expressions.