20 const bool is_base_type_eq =
24 const std::string error_msg =
25 std::string(
"equality without matching types:\n") +
"######### lhs: " +
48 bv0.size() == bv1.size(),
49 std::string(
"unexpected size mismatch on equality:\n") +
"lhs: " +
51 '\n' +
"rhs: " + expr.
rhs().
pretty() +
'\n' +
70 const bool is_base_type_eq =
74 std::string(
"verilog_case_equality without matching types:\n") +
75 "######### lhs: " + expr.
lhs().
pretty() +
'\n' +
82 bv0.size() == bv1.size(),
83 std::string(
"unexpected size mismatch on verilog_case_equality:\n") +
84 "lhs: " + expr.
lhs().
pretty() +
'\n' +
"lhs size: " +
88 if(expr.
id()==ID_verilog_case_inequality)
A generic base class for relations, i.e., binary predicates.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
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
const irep_idt & id() const
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
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 a generic exprt to an equal_exprt.
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool has_byte_operator(const exprt &src)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
std::vector< literalt > bvt