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: " +
83 "Generation of SMT formula for union construction expression: " +
116 sort.accept(converter);
123 "Generation of SMT formula for concatenation expression: " +
130 "Generation of SMT formula for bitwise and expression: " +
137 "Generation of SMT formula for bitwise or expression: " +
144 "Generation of SMT formula for bitwise xor expression: " +
151 "Generation of SMT formula for bitwise not expression: " +
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)
215 return std::accumulate(
266 "Generation of SMT formula for floating point equality expression: " +
274 "Generation of SMT formula for floating point not equal expression: " +
278template <
typename unsigned_factory_typet,
typename signed_factory_typet>
296 "Generation of SMT formula for relational expression: " +
310 const auto greater_than_or_equal =
314 *greater_than_or_equal,
326 const auto less_than_or_equal =
341 return can_cast_type<integer_bitvector_typet>(operand.type());
350 "Generation of SMT formula for plus expression: " + plus.
pretty());
368 "Generation of SMT formula for minus expression: " + minus.
pretty());
398 "Generation of SMT formula for divide expression: " + divide.
pretty());
407 "Generation of SMT formula for floating point operation expression: " +
439 "Generation of SMT formula for remainder (modulus) expression: " +
448 "Generation of SMT formula for euclidean modulo expression: " +
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: " +
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: " +
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: " +
544 "Generation of SMT formula for is invalid pointer expression: " +
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: " +
579 "Generation of SMT formula for byte update expression: " +
586 "Generation of SMT formula for absolute value of expression: " +
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: " +
614 "Generation of SMT formula for is infinite expression: " +
621 "Generation of SMT formula for array construction expression: " +
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: " +
667 "Generation of SMT formula for count leading zeros expression: " +
675 "Generation of SMT formula for byte swap expression: " +
872 const auto is_dynamic_object =
952 out <<
"|" << object_sizes[expr] <<
"|";
961 "constraint_select_one is not expected in smt conversion: " +
985 "Generation of SMT formula for unknown kind of expression: " +
API to expression classes for bitvectors.
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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
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