cprover
Loading...
Searching...
No Matches
boolbv_equality.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/std_expr.h>
12#include <util/invariant.h>
13
15
17{
18 const bool equality_types_match = expr.lhs().type() == expr.rhs().type();
20 equality_types_match,
21 "types of expressions on each side of equality should match",
24
25 // see if it is an unbounded array
26 if(is_unbounded_array(expr.lhs().type()))
27 {
28 // flatten byte_update/byte_extract operators if needed
29
30 if(has_byte_operator(expr))
31 {
34 }
35
36 return record_array_equality(expr);
37 }
38
39 const bvt &lhs_bv = convert_bv(expr.lhs());
40 const bvt &rhs_bv = convert_bv(expr.rhs());
41
43 lhs_bv.size() == rhs_bv.size(),
44 "sizes of lhs and rhs bitvectors should match",
45 irep_pretty_diagnosticst{expr.lhs()},
46 "lhs size: " + std::to_string(lhs_bv.size()),
47 irep_pretty_diagnosticst{expr.rhs()},
48 "rhs size: " + std::to_string(rhs_bv.size()));
49
50 if(lhs_bv.empty())
51 {
52 // An empty bit-vector comparison. It's not clear
53 // what this is meant to say.
54 return prop.new_variable();
55 }
56
57 return bv_utils.equal(lhs_bv, rhs_bv);
58}
59
61 const binary_relation_exprt &expr)
62{
63 // This is 4-valued comparison, i.e., z===z, x===x etc.
64 // The result is always Boolean.
65
67 expr.lhs().type() == expr.rhs().type(),
68 "lhs and rhs types should match in verilog_case_equality",
69 irep_pretty_diagnosticst{expr.lhs()},
70 irep_pretty_diagnosticst{expr.rhs()});
71
72 const bvt &lhs_bv = convert_bv(expr.lhs());
73 const bvt &rhs_bv = convert_bv(expr.rhs());
74
76 lhs_bv.size() == rhs_bv.size(),
77 "bitvector arguments to verilog_case_equality should have the same size",
78 irep_pretty_diagnosticst{expr.lhs()},
79 "lhs size: " + std::to_string(lhs_bv.size()),
80 irep_pretty_diagnosticst{expr.rhs()},
81 "rhs size: " + std::to_string(rhs_bv.size()));
82
83 if(expr.id()==ID_verilog_case_inequality)
84 return !bv_utils.equal(lhs_bv, rhs_bv);
85 else
86 return bv_utils.equal(lhs_bv, rhs_bv);
87}
const namespacet & ns
Definition: arrays.h:56
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:52
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:547
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...
Definition: boolbv.cpp:40
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:114
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.
Definition: bv_utils.cpp:1103
Equality.
Definition: std_expr.h:1225
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:396
virtual literalt new_variable()=0
std::vector< literalt > bvt
Definition: literal.h:201
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,...)
Definition: invariant.h:511
API to expression classes.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265