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: " +
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< 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< 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
Struct constructor from list of elements.
Expression to hold a symbol (variable)
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 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.
bool can_cast_expr< less_than_exprt >(const exprt &base)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool can_cast_expr< greater_than_exprt >(const exprt &base)
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
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