cprover
boolbv_abs.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 "
boolbv_type.h
"
12
13
#include <
util/bitvector_types.h
>
14
15
#include <
solvers/floatbv/float_utils.h
>
16
17
bvt
boolbvt::convert_abs
(
const
abs_exprt
&expr)
18
{
19
const
std::size_t width =
boolbv_width
(expr.
type
());
20
21
if
(width==0)
22
return
conversion_failed
(expr);
23
24
const
bvt
&op_bv=
convert_bv
(expr.
op
());
25
26
if
(expr.
op
().
type
()!=expr.
type
())
27
return
conversion_failed
(expr);
28
29
const
bvtypet
bvtype =
get_bvtype
(expr.
type
());
30
31
if
(bvtype==bvtypet::IS_FIXED ||
32
bvtype==bvtypet::IS_SIGNED ||
33
bvtype==bvtypet::IS_UNSIGNED)
34
{
35
return
bv_utils
.
absolute_value
(op_bv);
36
}
37
else
if
(bvtype==bvtypet::IS_FLOAT)
38
{
39
float_utilst
float_utils(
prop
,
to_floatbv_type
(expr.
type
()));
40
return
float_utils.
abs
(op_bv);
41
}
42
43
return
conversion_failed
(expr);
44
}
float_utilst::abs
bvt abs(const bvt &)
Definition:
float_utils.cpp:563
float_utilst
Definition:
float_utils.h:18
float_utils.h
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition:
bitvector_types.h:367
boolbv_type.h
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition:
boolbv_type.cpp:12
boolbvt::convert_abs
virtual bvt convert_abs(const abs_exprt &expr)
Definition:
boolbv_abs.cpp:17
bv_utilst::absolute_value
bvt absolute_value(const bvt &op)
Definition:
bv_utils.cpp:773
bvtypet
bvtypet
Definition:
boolbv_type.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:82
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:126
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition:
boolbv.h:96
bitvector_types.h
Pre-defined bitvector types.
abs_exprt
Absolute value.
Definition:
std_expr.h:346
unary_exprt::op
const exprt & op() const
Definition:
std_expr.h:293
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:47
boolbvt::bv_utils
bv_utilst bv_utils
Definition:
boolbv.h:111
boolbv.h
prop_conv_solvert::prop
propt & prop
Definition:
prop_conv_solver.h:128
solvers
flattening
boolbv_abs.cpp
Generated by
1.8.20