cprover
float_approximation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
12{
13}
14
16{
17 // this thing is quadratic!
18 // returns 'zero' if fraction is zero
19 bvt new_fraction=prop.new_variables(fraction.size());
20 bvt new_exponent=prop.new_variables(exponent.size());
21
22 // i is the shift distance
23 for(unsigned i=0; i<fraction.size(); i++)
24 {
25 bvt equal;
26
27 // the bits above need to be zero
28 for(unsigned j=0; j<i; j++)
29 equal.push_back(
30 !fraction[fraction.size()-1-j]);
31
32 // this one needs to be one
33 equal.push_back(fraction[fraction.size()-1-i]);
34
35 // iff all of that holds, we shift here!
36 literalt shift=prop.land(equal);
37
38 // build shifted value
39 bvt shifted_fraction;
41 shifted_fraction=overapproximating_left_shift(fraction, i);
42 else
43 shifted_fraction=bv_utils.shift(
45
46 bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
47
48 // build new exponent
49 bvt adjustment =
50 bv_utils.build_constant(-static_cast<int>(i), exponent.size());
51 bvt added_exponent=bv_utils.add(exponent, adjustment);
52 bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
53 }
54
55 // fraction all zero? it stays zero
56 // the exponent is undefined in that case
57 literalt fraction_all_zero=bv_utils.is_zero(fraction);
58 bvt zero_fraction;
59 zero_fraction.resize(fraction.size(), const_literal(false));
60 bv_utils.cond_implies_equal(fraction_all_zero, zero_fraction, new_fraction);
61
62 fraction=new_fraction;
63 exponent=new_exponent;
64}
65
67 const bvt &src, unsigned dist)
68{
69 bvt result;
70 result.resize(src.size());
71
72 for(unsigned i=0; i<src.size(); i++)
73 {
74 literalt l;
75
76 l=(dist<=i?src[i-dist]:prop.new_variable());
77 result[i]=l;
78 }
79
80 return result;
81}
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:61
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
literalt is_zero(const bvt &op)
Definition: bv_utils.h:138
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1312
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:477
bvt overapproximating_left_shift(const bvt &src, unsigned dist)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bv_utilst bv_utils
Definition: float_utils.h:155
propt & prop
Definition: float_utils.h:154
virtual literalt land(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
virtual literalt new_variable()=0
Floating Point with under/over-approximation.
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188