cprover
Loading...
Searching...
No Matches
boolbv_bv_rel.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
12
13#include "boolbv_type.h"
14
16
19{
20 const irep_idt &rel=expr.id();
21
22 const exprt &lhs = expr.lhs();
23 const exprt &rhs = expr.rhs();
24
25 const bvt &bv_lhs = convert_bv(lhs);
26 const bvt &bv_rhs = convert_bv(rhs);
27
28 bvtypet bvtype_lhs = get_bvtype(lhs.type());
29 bvtypet bvtype_rhs = get_bvtype(rhs.type());
30
31 if(
32 bv_lhs.size() == bv_rhs.size() && !bv_lhs.empty() &&
33 bvtype_lhs == bvtype_rhs)
34 {
35 if(bvtype_lhs == bvtypet::IS_FLOAT)
36 {
37 float_utilst float_utils(prop, to_floatbv_type(lhs.type()));
38
39 if(rel == ID_le)
40 return float_utils.relation(bv_lhs, float_utilst::relt::LE, bv_rhs);
41 else if(rel == ID_lt)
42 return float_utils.relation(bv_lhs, float_utilst::relt::LT, bv_rhs);
43 else if(rel == ID_ge)
44 return float_utils.relation(bv_lhs, float_utilst::relt::GE, bv_rhs);
45 else if(rel == ID_gt)
46 return float_utils.relation(bv_lhs, float_utilst::relt::GT, bv_rhs);
47 else
48 return SUB::convert_rest(expr);
49 }
50 else if(
51 (lhs.type().id() == ID_range && rhs.type() == lhs.type()) ||
52 bvtype_lhs == bvtypet::IS_SIGNED || bvtype_lhs == bvtypet::IS_UNSIGNED ||
53 bvtype_lhs == bvtypet::IS_FIXED)
54 {
55 literalt literal;
56
57 bv_utilst::representationt rep = ((bvtype_lhs == bvtypet::IS_SIGNED) ||
58 (bvtype_lhs == bvtypet::IS_FIXED))
61
62#if 1
63
64 return bv_utils.rel(bv_lhs, expr.id(), bv_rhs, rep);
65
66#else
67 literalt literal = bv_utils.rel(bv_lhs, expr.id(), bv_rhs, rep);
68
69 if(prop.has_set_to())
70 {
71 // it's unclear if this helps
72 if(bv_lhs.size() > 8)
73 {
74 literalt equal_lit = equality(lhs, rhs);
75
76 if(or_equal)
77 prop.l_set_to_true(prop.limplies(equal_lit, literal));
78 else
79 prop.l_set_to_true(prop.limplies(equal_lit, !literal));
80 }
81 }
82
83 return literal;
84#endif
85 }
86 else if(
87 (bvtype_lhs == bvtypet::IS_VERILOG_SIGNED ||
88 bvtype_lhs == bvtypet::IS_VERILOG_UNSIGNED) &&
89 lhs.type() == rhs.type())
90 {
91 // extract number bits
92 bvt extract0, extract1;
93
94 extract0.resize(bv_lhs.size() / 2);
95 extract1.resize(bv_rhs.size() / 2);
96
97 for(std::size_t i = 0; i < extract0.size(); i++)
98 extract0[i] = bv_lhs[i * 2];
99
100 for(std::size_t i = 0; i < extract1.size(); i++)
101 extract1[i] = bv_rhs[i * 2];
102
104
105 // now compare
106 return bv_utils.rel(extract0, expr.id(), extract1, rep);
107 }
108 }
109
110 return SUB::convert_rest(expr);
111}
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:13
bvtypet
Definition: boolbv_type.h:17
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
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
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
bv_utilst bv_utils
Definition: boolbv.h:114
representationt
Definition: bv_utils.h:28
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1279
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
literalt relation(const bvt &src1, relt rel, const bvt &src2)
const irep_idt & id() const
Definition: irep.h:396
virtual literalt convert_rest(const exprt &expr)
void l_set_to_true(literalt a)
Definition: prop.h:51
virtual literalt limplies(literalt a, literalt b)=0
virtual bool has_set_to() const
Definition: prop.h:80
std::vector< literalt > bvt
Definition: literal.h:201