21 const bool is_base_type_eq =
25 "types of expressions on each side of equality should match",
47 lhs_bv.size() == rhs_bv.size(),
48 "sizes of lhs and rhs bitvectors should match",
70 const bool is_base_type_eq =
74 "lhs and rhs types should match in verilog_case_equality",
82 lhs_bv.size() == rhs_bv.size(),
83 "bitvector arguments to verilog_case_equality should have the same size",
89 if(expr.
id()==ID_verilog_case_inequality)
A base class for relations, i.e., binary predicates.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
const irep_idt & id() const
virtual literalt new_variable()=0
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Exceptions that can be raised in bv_conversion.
API to expression classes.
literalt record_array_equality(const equal_exprt &expr)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
bool has_byte_operator(const exprt &src)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
std::vector< literalt > bvt