32 "Bool terms may only be used to construct bool typed expressions.");
39 false,
"Unexpected conversion of identifier to value expression.");
51 "Width of smt bit vector term must match the width of pointer type.");
52 if(bit_vector_constant.
value() == 0)
68 const auto bitvector_type =
72 bitvector_type->get_width() == sort_width,
73 "Width of smt bit vector term must match the width of bit vector "
79 const auto c_enum_tag_type =
86 "Width of smt bit vector term must match the width of bit vector "
87 "underlying type of the original c_enum type.");
95 "construct_value_expr_from_smt for bit vector should not be applied to "
105 "Unexpected conversion of function application to value expression.");
111 false,
"Unexpected conversion of forall quantifier to value expression.");
117 false,
"Unexpected conversion of exists quantifier to value expression.");
130 value_term.
accept(factory);
131 INVARIANT(factory.
result.has_value(),
"Factory must result in expr value.");
138 const typet &type_to_construct,
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
pointer_typet pointer_type(const typet &subtype)
std::size_t get_width() const
const typet & underlying_type() const
A constant literal expression.
Base class for all expressions.
The Boolean constant false.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
const smt_bit_vector_sortt & get_sort() const
std::size_t bit_width() const
Stores identifiers in unescaped and unquoted form.
void accept(smt_term_const_downcast_visitort &) const
The Boolean constant true.
The type of an expression, extends irept.
std::optional< exprt > result
void visit(const smt_bool_literal_termt &bool_literal) override
const typet & type_to_construct
void visit(const smt_function_application_termt &function_application) override
void visit(const smt_identifier_termt &identifier_term) override
static exprt make(const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
This function is complete the external interface to this class.
void visit(const smt_forall_termt &forall) override
void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
void visit(const smt_exists_termt &exists) override
value_expr_from_smt_factoryt(const typet &type_to_construct, const namespacet &ns)
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
mini_bddt exists(const mini_bddt &u, const unsigned var)
API to expression classes for Pointers.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
Defines typet, type_with_subtypet and type_with_subtypest.