cprover
float_approximation.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Floating Point with under/over-approximation
4
5Author:
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_APPROXIMATION_H
13#define CPROVER_SOLVERS_FLOATBV_FLOAT_APPROXIMATION_H
14
15#include "float_utils.h"
16
18{
19public:
20 explicit float_approximationt(propt &_prop):
21 float_utilst(_prop),
22 over_approximate(false),
24 {
25 }
26
27 virtual ~float_approximationt();
28
31
32protected:
33 virtual void normalization_shift(bvt &fraction, bvt &exponent);
34 bvt overapproximating_left_shift(const bvt &src, unsigned dist);
35
36private:
37 // NOLINTNEXTLINE(readability/identifiers)
39};
40
41#endif // CPROVER_SOLVERS_FLOATBV_FLOAT_APPROXIMATION_H
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
float_approximationt(propt &_prop)
TO_BE_DOCUMENTED.
Definition: prop.h:23
std::vector< literalt > bvt
Definition: literal.h:201