cprover
boolbv_unary_minus.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 
14 
15 #include <algorithm>
16 #include <iterator>
17 
18 #include "boolbv_type.h"
19 
21 {
22  const typet &type = expr.type();
23 
24  std::size_t width=boolbv_width(type);
25 
26  if(width==0)
27  return conversion_failed(expr);
28 
29  const exprt &op = expr.op();
30 
31  const bvt &op_bv = convert_bv(op, width);
32 
33  bvtypet bvtype=get_bvtype(type);
34  bvtypet op_bvtype = get_bvtype(op.type());
35 
36  if(bvtype==bvtypet::IS_UNKNOWN &&
37  (type.id()==ID_vector || type.id()==ID_complex))
38  {
39  const typet &subtype = type.subtype();
40 
41  std::size_t sub_width=boolbv_width(subtype);
42 
43  INVARIANT(
44  sub_width > 0,
45  "bitvector representation of type needs to have at least one bit");
46 
47  INVARIANT(
48  width % sub_width == 0,
49  "total bitvector width needs to be a multiple of the component bitvector "
50  "widths");
51 
52  bvt bv;
53 
54  for(std::size_t sub_idx = 0; sub_idx < width; sub_idx += sub_width)
55  {
56  bvt tmp_op;
57 
58  const auto sub_it = std::next(op_bv.begin(), sub_idx);
59  std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op));
60 
61  if(type.subtype().id() == ID_floatbv)
62  {
63  float_utilst float_utils(prop, to_floatbv_type(subtype));
64  tmp_op = float_utils.negate(tmp_op);
65  }
66  else
67  tmp_op = bv_utils.negate(tmp_op);
68 
69  INVARIANT(
70  tmp_op.size() == sub_width,
71  "bitvector after negation shall have same bit width");
72 
73  std::copy(tmp_op.begin(), tmp_op.end(), std::back_inserter(bv));
74  }
75 
76  return bv;
77  }
78  else if(bvtype==bvtypet::IS_FIXED && op_bvtype==bvtypet::IS_FIXED)
79  {
80  return bv_utils.negate(op_bv);
81  }
82  else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
83  {
84  float_utilst float_utils(prop, to_floatbv_type(expr.type()));
85  return float_utils.negate(op_bv);
86  }
87  else if((op_bvtype==bvtypet::IS_SIGNED || op_bvtype==bvtypet::IS_UNSIGNED) &&
88  (bvtype==bvtypet::IS_SIGNED || bvtype==bvtypet::IS_UNSIGNED))
89  {
90  return bv_utils.negate(op_bv);
91  }
92 
93  return conversion_failed(expr);
94 }
bvtypet::IS_SIGNED
@ IS_SIGNED
typet::subtype
const typet & subtype() const
Definition: type.h:47
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:29
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bvtypet::IS_FIXED
@ IS_FIXED
boolbv_type.h
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
exprt
Base class for all expressions.
Definition: expr.h:53
bvtypet::IS_UNSIGNED
@ IS_UNSIGNED
bvtypet
bvtypet
Definition: boolbv_type.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
bvtypet::IS_FLOAT
@ IS_FLOAT
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
std_types.h
Pre-defined types.
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
irept::id
const irep_idt & id() const
Definition: irep.h:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
boolbvt::convert_bv
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:119
bv_utilst::negate
bvt negate(const bvt &op)
Definition: bv_utils.cpp:533
float_utilst::negate
bvt negate(const bvt &)
Definition: float_utils.cpp:554
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
boolbvt::convert_unary_minus
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
Definition: boolbv_unary_minus.cpp:20
boolbv.h
bvtypet::IS_UNKNOWN
@ IS_UNKNOWN
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131