28 "Bool terms may only be used to construct bool typed expressions.");
35 false,
"Unexpected conversion of identifier to value expression.");
47 "Width of smt bit vector term must match the width of bit vector "
55 "construct_value_expr_from_smt for bit vector should not be applied to "
65 "Unexpected conversion of function application to value expression.");
76 INVARIANT(factory.result.has_value(),
"Factory must result in expr value.");
77 return *factory.result;
83 const typet &type_to_construct)
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
The Boolean constant false.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Stores identifiers in unescaped and unquoted form.
The Boolean constant true.
The type of an expression, extends irept.
value_expr_from_smt_factoryt(const typet &type_to_construct)
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
optionalt< exprt > result
void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
static exprt make(const smt_termt &value_term, const typet &type_to_construct)
This function is complete the external interface to this class.
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
#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.