cprover
boolbv_unary_minus.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
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 = to_type_with_subtype(type).subtype();
40
41 std::size_t sub_width=boolbv_width(subtype);
42
44 sub_width > 0,
45 "bitvector representation of type needs to have at least one bit");
46
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(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
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}
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
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
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:114
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
bvt negate(const bvt &op)
Definition: bv_utils.cpp:529
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bvt negate(const bvt &)
const irep_idt & id() const
Definition: irep.h:396
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
std::vector< literalt > bvt
Definition: literal.h:201
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177