CBMC
boolbv_bv_rel.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/bitvector_types.h>
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
@ IS_VERILOG_UNSIGNED
@ IS_VERILOG_SIGNED
exprt & lhs()
Definition: std_expr.h:668
exprt & rhs()
Definition: std_expr.h:678
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:37
bv_utilst bv_utils
Definition: boolbv.h:116
representationt
Definition: bv_utils.h:28
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1557
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
literalt relation(const bvt &src1, relt rel, const bvt &src2)
const irep_idt & id() const
Definition: irep.h:384
virtual literalt convert_rest(const exprt &expr)
void l_set_to_true(literalt a)
Definition: prop.h:52
virtual literalt limplies(literalt a, literalt b)=0
virtual bool has_set_to() const
Definition: prop.h:81
std::vector< literalt > bvt
Definition: literal.h:201