1 /* Multiplication_Floating_Point_Expression class implementation:
2 non-inline template functions.
3 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
4 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
5
6 This file is part of the Parma Polyhedra Library (PPL).
7
8 The PPL is free software; you can redistribute it and/or modify it
9 under the terms of the GNU General Public License as published by the
10 Free Software Foundation; either version 3 of the License, or (at your
11 option) any later version.
12
13 The PPL is distributed in the hope that it will be useful, but WITHOUT
14 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
15 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
16 for more details.
17
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software Foundation,
20 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
21
22 For the most up-to-date information see the Parma Polyhedra Library
23 site: http://bugseng.com/products/ppl/ . */
24
25 #ifndef PPL_Multiplication_Floating_Point_Expression_templates_hh
26 #define PPL_Multiplication_Floating_Point_Expression_templates_hh 1
27
28 namespace Parma_Polyhedra_Library {
29
30 template <typename FP_Interval_Type, typename FP_Format>
31 bool Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format>
linearize(const FP_Interval_Abstract_Store & int_store,const FP_Linear_Form_Abstract_Store & lf_store,FP_Linear_Form & result) const32 ::linearize(const FP_Interval_Abstract_Store& int_store,
33 const FP_Linear_Form_Abstract_Store& lf_store,
34 FP_Linear_Form& result) const {
35 /*
36 FIXME: We currently adopt the "Interval-Size Local" strategy in order to
37 decide which of the two linear forms must be intervalized, as described
38 in Section 6.2.4 ("Multiplication Strategies") of Antoine Mine's Ph.D.
39 thesis "Weakly Relational Numerical Abstract Domains".
40 In this Section are also described other multiplication strategies, such
41 as All-Cases, Relative-Size Local, Simplification-Driven Global and
42 Homogeneity Global.
43 */
44
45 // Here we choose which of the two linear forms must be intervalized.
46
47 // true if we intervalize the first form, false if we intervalize the second.
48 bool intervalize_first;
49 FP_Linear_Form linearized_first_operand;
50 if (!first_operand->linearize(int_store, lf_store,
51 linearized_first_operand)) {
52 return false;
53 }
54 FP_Interval_Type intervalized_first_operand;
55 this->intervalize(linearized_first_operand, int_store,
56 intervalized_first_operand);
57 FP_Linear_Form linearized_second_operand;
58 if (!second_operand->linearize(int_store, lf_store,
59 linearized_second_operand)) {
60 return false;
61 }
62 FP_Interval_Type intervalized_second_operand;
63 this->intervalize(linearized_second_operand, int_store,
64 intervalized_second_operand);
65
66 // FIXME: we are not sure that what we do here is policy-proof.
67 if (intervalized_first_operand.is_bounded()) {
68 if (intervalized_second_operand.is_bounded()) {
69 boundary_type first_interval_size
70 = intervalized_first_operand.upper()
71 - intervalized_first_operand.lower();
72 boundary_type second_interval_size
73 = intervalized_second_operand.upper()
74 - intervalized_second_operand.lower();
75 if (first_interval_size <= second_interval_size) {
76 intervalize_first = true;
77 }
78 else {
79 intervalize_first = false;
80 }
81 }
82 else {
83 intervalize_first = true;
84 }
85 }
86 else {
87 if (intervalized_second_operand.is_bounded()) {
88 intervalize_first = false;
89 }
90 else {
91 return false;
92 }
93 }
94
95 // Here we do the actual computation.
96 // For optimizing, we store the relative error directly into result.
97 if (intervalize_first) {
98 relative_error(linearized_second_operand, result);
99 linearized_second_operand *= intervalized_first_operand;
100 result *= intervalized_first_operand;
101 result += linearized_second_operand;
102 }
103 else {
104 relative_error(linearized_first_operand, result);
105 linearized_first_operand *= intervalized_second_operand;
106 result *= intervalized_second_operand;
107 result += linearized_first_operand;
108 }
109
110 result += this->absolute_error;
111 return !this->overflows(result);
112 }
113
114 } // namespace Parma_Polyhedra_Library
115
116 #endif // !defined(PPL_Multiplication_Floating_Point_Expression_templates_hh)
117