cprover
Loading...
Searching...
No Matches
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
35
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 {
64 tmp_op = float_utils.negate(tmp_op);
65 }
66 else
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 }
79 {
80 return bv_utils.negate(op_bv);
81 }
83 {
85 return float_utils.negate(op_bv);
86 }
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)
bvtypet
Definition boolbv_type.h:17
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177