cprover
boolbv_ieee_float_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  bvtypet bvtype0=get_bvtype(op0.type());
28  bvtypet bvtype1=get_bvtype(op1.type());
29 
30  const bvt &bv0=convert_bv(op0);
31  const bvt &bv1=convert_bv(op1);
32 
33  if(bv0.size()==bv1.size() && !bv0.empty() &&
34  bvtype0==bvtypet::IS_FLOAT && bvtype1==bvtypet::IS_FLOAT)
35  {
36  float_utilst float_utils(prop, to_floatbv_type(op0.type()));
37 
38  if(rel==ID_ieee_float_equal)
39  return float_utils.relation(bv0, float_utilst::relt::EQ, bv1);
40  else if(rel==ID_ieee_float_notequal)
41  return !float_utils.relation(bv0, float_utilst::relt::EQ, bv1);
42  else
43  return SUB::convert_rest(expr);
44  }
45  }
46 
47  return SUB::convert_rest(expr);
48 }
virtual literalt convert_ieee_float_rel(const exprt &expr)
exprt & op0()
Definition: expr.h:72
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
exprt & op1()
Definition: expr.h:75
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
bvtypet
Definition: boolbv_type.h:16
std::vector< exprt > operandst
Definition: expr.h:45
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
Base class for all expressions.
Definition: expr.h:42
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200
literalt relation(const bvt &src1, relt rel, const bvt &src2)