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