24 #ifndef PPL_Linear_Form_templates_hh
25 #define PPL_Linear_Form_templates_hh 1
41 throw std::length_error(
"Linear_Form<C>::"
43 "v exceeds the maximum allowed "
56 const dimension_type space_dim = std::max(v_space_dim, w_space_dim);
58 throw std::length_error(
"Linear_Form<C>::"
59 "Linear_Form(v, w):\n"
60 "v or w exceed the maximum allowed "
65 if (v_space_dim != w_space_dim) {
66 vec[v_space_dim] = C(
typename C::boundary_type(1));
67 vec[w_space_dim] = C(
typename C::boundary_type(-1));
76 throw std::length_error(
"Linear_Form<C>::"
78 "e exceeds the maximum allowed "
82 vec.resize(space_dim+1);
97 if (f1_size > f2_size) {
110 while (i > min_size) {
112 r[i] = p_e_max->
vec[i];
123 template <
typename C>
128 throw std::length_error(
"Linear_Form "
130 "v exceeds the maximum allowed "
137 r[v_space_dim] += C(
typename C::boundary_type(1));
142 template <
typename C>
151 template <
typename C>
156 r[i].neg_assign(r[i]);
162 template <
typename C>
167 if (f1_size > f2_size) {
170 while (i > f2_size) {
184 while (i > f1_size) {
186 r[i].neg_assign(f2[i]);
198 template <
typename C>
203 throw std::length_error(
"Linear_Form "
205 "v exceeds the maximum allowed "
213 r[i].neg_assign(r[i]);
215 r[v_space_dim] += C(
typename C::boundary_type(1));
220 template <
typename C>
225 throw std::length_error(
"Linear_Form "
227 "v exceeds the maximum allowed "
234 r[v_space_dim] -= C(
typename C::boundary_type(1));
239 template <
typename C>
244 r[i].neg_assign(r[i]);
251 template <
typename C>
262 template <
typename C>
267 if (f1_size < f2_size) {
277 template <
typename C>
282 throw std::length_error(
"Linear_Form<C>& "
283 "operator+=(e, v):\n"
284 "v exceeds the maximum allowed space dimension.");
289 f[v_space_dim] += C(
typename C::boundary_type(1));
294 template <
typename C>
299 if (f1_size < f2_size) {
309 template <
typename C>
314 throw std::length_error(
"Linear_Form<C>& "
315 "operator-=(e, v):\n"
316 "v exceeds the maximum allowed space dimension.");
321 f[v_space_dim] -= C(
typename C::boundary_type(1));
326 template <
typename C>
337 template <
typename C>
348 template <
typename C>
353 if (x_size >= y_size) {
360 if (x[i] != x.
zero) {
372 if (y[i] != x.
zero) {
382 template <
typename C>
386 vec[i].neg_assign(vec[i]);
391 template <
typename C>
396 n += vec[i].external_memory_in_bytes();
398 n += vec.capacity()*
sizeof(C);
402 template <
typename C>
414 template <
typename C>
419 typedef typename C::boundary_type analyzer_format;
423 unsigned int f_mantissa_bits;
424 switch (analyzed_format) {
456 unsigned int u_power =
msb_position(f_base) * f_mantissa_bits;
457 int neg_power = -
static_cast<int>(u_power);
458 analyzer_format lb =
static_cast<analyzer_format
>(ldexp(1.0, neg_power));
464 const C* current_term = &inhomogeneous_term();
465 assert(current_term->is_bounded());
467 C current_multiplier(std::max(std::abs(current_term->lower()),
468 std::abs(current_term->upper())));
469 Linear_Form current_result_term(current_multiplier);
470 current_result_term *= error_propagator;
476 current_term = &coefficient(
Variable(i));
477 assert(current_term->is_bounded());
478 current_multiplier = C(std::max(std::abs(current_term->lower()),
479 std::abs(current_term->upper())));
481 current_result_term *= current_multiplier;
482 current_result_term *= error_propagator;
483 result += current_result_term;
489 template <
typename C>
490 template <
typename Target>
494 result = C(inhomogeneous_term());
497 C current_addend = coefficient(
Variable(i));
502 current_addend *= curr_int;
503 result += current_addend;
510 template <
typename C>
512 IO_Operators::operator<<(std::ostream& s, const Linear_Form<C>& f) {
516 const C& fv = f[v+1];
517 if (fv !=
typename C::boundary_type(0)) {
519 if (fv ==
typename C::boundary_type(-1)) {
522 else if (fv !=
typename C::boundary_type(1)) {
528 if (fv ==
typename C::boundary_type(-1)) {
533 if (fv !=
typename C::boundary_type(1)) {
555 s << Linear_Form<C>::zero;
562 template <typename C>
563 C
Linear_Form<C>::zero(typename C::boundary_type(0));
567 #endif // !defined(PPL_Linear_Form_templates_hh)
static const unsigned int BASE
I_Constraint< T > i_constraint(I_Constraint_Rel rel, const T &v)
static const unsigned int BASE
static const unsigned int MANTISSA_BITS
virtual bool get_interval(dimension_type dim, FP_Interval_Type &result) const =0
Asks the external analyzer for an interval that correctly approximates the floating point entity refe...
An abstract class to be implemented by an external analyzer such as ECLAIR in order to provide to the...
size_t dimension_type
An unsigned integral type for representing space dimensions.
static const unsigned int MANTISSA_BITS
IEEE 754 half precision, 16 bits (5 exponent, 10 mantissa).
IEEE 754 quad precision, 128 bits (15 exponent, 112 mantissa).
Coefficient_traits::const_reference inhomogeneous_term() const
Returns the inhomogeneous term of *this.
IBM single precision, 32 bits (7 exponent, 24 mantissa).
static const unsigned int BASE
static const unsigned int BASE
static const unsigned int BASE
#define PPL_OUTPUT_TEMPLATE_DEFINITIONS(type_symbol, class_prefix)
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
unsigned int msb_position(unsigned long long v)
If v is nonzero, returns the position of the most significant bit in a.
Coefficient_traits::const_reference coefficient(Variable v) const
Returns the coefficient of v in *this.
A dimension of the vector space.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
dimension_type compute_capacity(dimension_type requested_size, dimension_type maximum_size)
Speculative allocation function.
Intel double extended precision, 80 bits (15 exponent, 64 mantissa)
Greater than or equal to.
static const unsigned int MANTISSA_BITS
static const unsigned int BASE
static const unsigned int MANTISSA_BITS
The entire library is confined to this namespace.
IEEE 754 double precision, 64 bits (11 exponent, 52 mantissa).
IEEE 754 single precision, 32 bits (8 exponent, 23 mantissa).
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
static const unsigned int MANTISSA_BITS
static const unsigned int MANTISSA_BITS