21 "types of expressions on each side of equality should match",
44 "sizes of lhs and rhs bitvectors should match",
46 "lhs size: " + std::to_string(
lhs_bv.size()),
48 "rhs size: " + std::to_string(
rhs_bv.size()));
68 "lhs and rhs types should match in verilog_case_equality",
77 "bitvector arguments to verilog_case_equality should have the same size",
79 "lhs size: " + std::to_string(
lhs_bv.size()),
81 "rhs size: " + std::to_string(
rhs_bv.size()));
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
literalt record_array_equality(const equal_exprt &expr)
A base class for relations, i.e., binary predicates whose two operands have the same type.
bool is_unbounded_array(const typet &type) const override
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
typet & type()
Return the type of the expression.
const irep_idt & id() const
virtual literalt new_variable()=0
std::vector< literalt > bvt
bool has_byte_operator(const exprt &src)
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
API to expression classes.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.