24 std::cout <<
"######### lhs: " << expr.
lhs().
pretty() <<
'\n';
25 std::cout <<
"######### rhs: " << expr.
rhs().
pretty() <<
'\n';
26 throw "equality without matching types";
46 if(bv0.size()!=bv1.size())
48 std::cerr <<
"lhs: " << expr.
lhs().
pretty() <<
'\n';
49 std::cerr <<
"lhs size: " << bv0.size() <<
'\n';
50 std::cerr <<
"rhs: " << expr.
rhs().
pretty() <<
'\n';
51 std::cerr <<
"rhs size: " << bv1.size() <<
'\n';
52 throw "unexpected size mismatch on equality";
73 std::cout <<
"######### lhs: " << expr.
lhs().
pretty() <<
'\n';
74 std::cout <<
"######### rhs: " << expr.
rhs().
pretty() <<
'\n';
75 throw "verilog_case_equality without matching types";
81 if(bv0.size()!=bv1.size())
83 std::cerr <<
"lhs: " << expr.
lhs().
pretty() <<
'\n';
84 std::cerr <<
"lhs size: " << bv0.size() <<
'\n';
85 std::cerr <<
"rhs: " << expr.
rhs().
pretty() <<
'\n';
86 std::cerr <<
"rhs size: " << bv1.size() <<
'\n';
87 throw "unexpected size mismatch on verilog_case_equality";
90 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 equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
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)
API to expression classes.
literalt record_array_equality(const equal_exprt &expr)
Base class for all expressions.
bool has_byte_operator(const exprt &src)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
std::vector< literalt > bvt