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(
46  fraction, bv_utilst::shiftt::SHIFT_LEFT, i);
47 
48  bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
49 
50  // build new exponent
51  bvt adjustment=bv_utils.build_constant(-i, exponent.size());
52  bvt added_exponent=bv_utils.add(exponent, adjustment);
53  bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
54  }
55 
56  // fraction all zero? it stays zero
57  // the exponent is undefined in that case
58  literalt fraction_all_zero=bv_utils.is_zero(fraction);
59  bvt zero_fraction;
60  zero_fraction.resize(fraction.size(), const_literal(false));
61  bv_utils.cond_implies_equal(fraction_all_zero, zero_fraction, new_fraction);
62 
63  fraction=new_fraction;
64  exponent=new_exponent;
65 }
66 
68  const bvt &src, unsigned dist)
69 {
70  bvt result;
71  result.resize(src.size());
72 
73  for(unsigned i=0; i<src.size(); i++)
74  {
75  literalt l;
76 
77  l=(dist<=i?src[i-dist]:prop.new_variable());
78  result[i]=l;
79  }
80 
81  return result;
82 }
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:141
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:1312
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15