cprover
float_approximation.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 "float_approximation.h"
10 
11 #include <cassert>
12 
14 {
15 }
16 
18 {
19  // this thing is quadratic!
20  // returns 'zero' if fraction is zero
21  bvt new_fraction=prop.new_variables(fraction.size());
22  bvt new_exponent=prop.new_variables(exponent.size());
23 
24  // i is the shift distance
25  for(unsigned i=0; i<fraction.size(); i++)
26  {
27  bvt equal;
28 
29  // the bits above need to be zero
30  for(unsigned j=0; j<i; j++)
31  equal.push_back(
32  !fraction[fraction.size()-1-j]);
33 
34  // this one needs to be one
35  equal.push_back(fraction[fraction.size()-1-i]);
36 
37  // iff all of that holds, we shift here!
38  literalt shift=prop.land(equal);
39 
40  // build shifted value
41  bvt shifted_fraction;
43  shifted_fraction=overapproximating_left_shift(fraction, i);
44  else
45  shifted_fraction=bv_utils.shift(fraction, bv_utilst::LEFT, i);
46 
47  bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
48 
49  // build new exponent
50  bvt adjustment=bv_utils.build_constant(-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 overapproximating_left_shift(const bvt &src, unsigned dist)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
literalt is_zero(const bvt &op)
Definition: bv_utils.h:137
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
Floating Point with under/over-approximation.
propt & prop
Definition: float_utils.h:152
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
literalt const_literal(bool value)
Definition: literal.h:187
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
bv_utilst bv_utils
Definition: float_utils.h:153
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1293
std::vector< literalt > bvt
Definition: literal.h:197
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15