September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Pass variables to affine_image by copy.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d61e5566f5f6dadd4386bf7154772492fb910932 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d61e5566f5f6… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 11:58:55 2009 +0200 Pass variables to affine_image by copy. --- src/BD_Shape.defs.hh | 2 +- src/BD_Shape.templates.hh | 2 +- src/Octagonal_Shape.defs.hh | 2 +- src/Octagonal_Shape.templates.hh | 2 +- src/Polyhedron.defs.hh | 2 +- src/Polyhedron.templates.hh | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 3dc29bb..ece9b0d 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -1108,7 +1108,7 @@ public: is not a dimension of \p *this. */ template <typename Interval_Info> - void affine_image(const Variable& var, + void affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf); /*! \brief diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 8b5c49d..5275116 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4046,7 +4046,7 @@ BD_Shape<T>::affine_image(const Variable var, template <typename T> template <typename Interval_Info> void -BD_Shape<T>::affine_image(const Variable& var, +BD_Shape<T>::affine_image(const Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf) { // Check that T is a floating point type. diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index a893fb7..6f910d2 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1155,7 +1155,7 @@ public: floating point variable represented by \p var. */ template <typename Interval_Info> - void affine_image(const Variable& var, + void affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf); /*! \brief diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 4b491bf..e3ae567 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5056,7 +5056,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, template <typename T> template <typename Interval_Info> void -Octagonal_Shape<T>::affine_image(const Variable& var, +Octagonal_Shape<T>::affine_image(const Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf) { // Check that T is a floating point type. diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 87ece79..7f17172 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1213,7 +1213,7 @@ public: floating point variable represented by \p var. */ template <typename FP_Format, typename Interval_Info> - void affine_image(const Variable& var, + void affine_image(Variable var, const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 8f9be84..8ad8b01 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -345,7 +345,7 @@ Polyhedron::refine_with_linear_form_inequality( template <typename FP_Format, typename Interval_Info> void -Polyhedron::affine_image(const Variable& var, +Polyhedron::affine_image(const Variable var, const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) {

1 0

[GIT] ppl/ppl(floating_point): Written Polyhedron:: refine_fp_interval_abstract_store.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 0d9faf95e4bc2c1f7f52936c4db0291a57686d3d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0d9faf95e4bc… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 11:50:35 2009 +0200 Written Polyhedron::refine_fp_interval_abstract_store. Various other corrections. --- src/Octagonal_Shape.defs.hh | 3 +- src/Octagonal_Shape.templates.hh | 2 +- src/Polyhedron.defs.hh | 10 +++++++ src/Polyhedron.templates.hh | 51 ++++++++++++++++++++++++++++++++++++- 4 files changed, 62 insertions(+), 4 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 61aebe7..a893fb7 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1746,7 +1746,8 @@ public: */ template <typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store); + std::map< dimension_type, Interval<T, Interval_Info> >& store) + const; //@} // Member Functions that May Modify the Dimension of the Vector Space diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index f09d910..4b491bf 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5426,7 +5426,7 @@ template <typename Interval_Info> void Octagonal_Shape<T>:: refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) { + std::map< dimension_type, Interval<T, Interval_Info> >& store) const { // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 7ecc2cf..87ece79 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1011,6 +1011,16 @@ public: const Linear_Form< Interval<FP_Format, Interval_Info> >& right, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); + //! Refines \p store with the constraints defining \p *this. + /*! + \param store + The interval floating point abstract store to refine. + */ + template <typename FP_Format, typename Interval_Info> + void refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + const; + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 7adf015..8f9be84 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -441,7 +441,6 @@ Polyhedron::convert_to_integer_expression( result = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+1); std::vector<Coefficient> denominators(lf_dimension+1); @@ -488,7 +487,6 @@ Polyhedron::convert_to_integer_expressions( res = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+2); std::vector<Coefficient> denominators(lf_dimension+2); @@ -541,6 +539,55 @@ Polyhedron::convert_to_integer_expressions( res_hi_coeff = Coefficient(0); } +template <typename FP_Format, typename Interval_Info> +void +Polyhedron:: +refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + const { + + // Check that FP_Format is indeed a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, + "Polyhedron::refine_fp_interval_abstract_store:" + " T not a floating point type."); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef typename std::map<dimension_type, FP_Interval_Type>::iterator + Map_Iterator; + + // FIXME: there could be restrictions on Interval_Info. + Box<FP_Interval_Type> limits(*this); + PPL_DIRTY_TEMP_COEFFICIENT(numerator); + PPL_DIRTY_TEMP_COEFFICIENT(denominator); + Map_Iterator store_end = store.end(); + for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) { + dimension_type curr_var = ite->first; + PPL_ASSERT(curr_var < space_dim); + Variable var(curr_var); + Linear_Expression var_exp(var); + bool dummy; + FP_Interval_Type& curr_int = ite->second; + FP_Format& lb = curr_int.lower(); + FP_Format& ub = curr_int.upper(); + FP_Format comparison_term; + mpq_class tmp_rational; + if (limits.minimize(var_exp, numerator, denominator, dummy)) { + assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); + assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); + assign_r(comparison_term, tmp_rational, ROUND_DOWN); + if (comparison_term > lb) + lb = comparison_term; + } + if (limits.maximize(var_exp, numerator, denominator, dummy)) { + assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); + assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); + assign_r(comparison_term, tmp_rational, ROUND_UP); + if (comparison_term < ub) + ub = comparison_term; + } + } +} + template <typename C> void Polyhedron::throw_dimension_incompatible(const char* method,

1 0

[GIT] ppl/ppl(pip): Added mechanism for fetching parametric values for variables.
by François Galea 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: pip Commit: 5561eee98184efc4cd7be287411c9b00616b1c11 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5561eee98184… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Sep 22 09:31:27 2009 +0200 Added mechanism for fetching parametric values for variables. --- src/PIP_Tree.cc | 62 +++++++++++++++++++++++++++++++++++++++++++++++-- src/PIP_Tree.defs.hh | 9 +++++++ 2 files changed, 68 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index b81d10b..9d8197c 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -89,7 +89,9 @@ PIP_Solution_Node::PIP_Solution_Node(PIP_Problem* p) tableau(), basis(), mapping(), - sign() { + sign(), + solution(), + solution_valid(false) { } PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x) @@ -97,7 +99,9 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x) tableau(x.tableau), basis(x.basis), mapping(x.mapping), - sign(x.sign) { + sign(x.sign), + solution(x.solution), + solution_valid(x.solution_valid) { } PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, @@ -106,7 +110,9 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, tableau(x.tableau), basis(x.basis), mapping(x.mapping), - sign(x.sign) { + sign(x.sign), + solution(x.solution), + solution_valid(x.solution_valid) { if (!empty_constraints) constraints_ = x.constraints_; } @@ -407,10 +413,35 @@ PIP_Solution_Node::ascii_load(std::istream& s) { if (!tableau.t.ascii_load(s)) return false; + solution_valid = false; PPL_ASSERT(OK()); return true; } +const Linear_Expression& +PIP_Solution_Node::parametric_values(Variable v) { + update_solution(); + Variables_Set& parameters = problem->parameters; + dimension_type id = v.id(); + dimension_type j; + Variables_Set::iterator location = parameters.lower_bound(id); + if (location == parameters.end()) + j = id; + else { + if (*location == id) { +#ifndef NDEBUG + std::cerr << "PIP_Solution_Node::parametric_values(Variable): " + "Supplied Variable corresponds to a parameter" + << std::endl; +#endif + j = not_a_dimension(); + } else + j = id - std::distance(parameters.begin(),location) - 1; + } + + return solution[j]; +} + PIP_Solution_Node::Row_Sign PIP_Solution_Node::row_sign(const Row &x) { PIP_Solution_Node::Row_Sign sign = ZERO; @@ -581,6 +612,30 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, // FIXME: decide emptiness detection (and node removal) } +void +PIP_Solution_Node::update_solution() { + if (solution_valid) + return; + dimension_type num_vars = tableau.s.num_columns(); + if (solution.size() != num_vars) + solution.resize(num_vars); + for (dimension_type i = num_vars; i-- > 0; ) { + Linear_Expression &sol = solution[i]; + if (basis[i]) { + sol = Linear_Expression(0); + } else { + Row &row = tableau.t[mapping[i]]; + sol = Linear_Expression(row[0]); + dimension_type k; + Variables_Set::iterator j; + Variables_Set::iterator j_end = problem->parameters.end(); + for (j = problem->parameters.begin(), k = 1; j != j_end; ++j, ++k) + sol += row[k] * Variable(*j); + } + } + solution_valid = true; +} + PIP_Problem_Status PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx) { @@ -802,6 +857,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, } c /= sij; } + solution_valid = false; } /* Otherwise, we have found a row i__ with mixed parameter sign. */ diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index fcbd62e..238ef5b 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -276,6 +276,12 @@ private: //! A cache for computed sign values of constraint parametric RHS. std::vector<Row_Sign> sign; + //! Parametric values for the solution. + std::vector<Linear_Expression> solution; + + //! An indicator for solution validity. + bool solution_valid; + //! Determines the sign of given Row. static Row_Sign row_sign(const Row &x); @@ -322,6 +328,9 @@ protected: const Constraint_Sequence &input_cs, const Variables_Set &parameters); + //! Update the solution values. + virtual void update_solution(); + /*! \brief Execute a parametric simplex on the tableau, under specified context.

1 0

[GIT] ppl/ppl(pip): Added reference to the Problem object in solution tree Nodes.
by François Galea 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: pip Commit: a6ea14f4ac3f3c9d64b4f0d3db728cec03ff7c9c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a6ea14f4ac3f… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Sep 22 09:30:53 2009 +0200 Added reference to the Problem object in solution tree Nodes. --- src/PIP_Problem.cc | 2 +- src/PIP_Problem.defs.hh | 1 + src/PIP_Tree.cc | 25 +++++++++++++++---------- src/PIP_Tree.defs.hh | 9 ++++++--- 4 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index ec42436..6d651fa 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -77,7 +77,7 @@ PPL::PIP_Problem::solve() const { PIP_Problem_Status return_value; if (current_solution == 0) - x.current_solution = new PIP_Solution_Node(); + x.current_solution = new PIP_Solution_Node(&x); x.current_solution->update_tableau(&x.current_solution, external_space_dim, diff --git a/src/PIP_Problem.defs.hh b/src/PIP_Problem.defs.hh index 58ebff5..3accf0e 100644 --- a/src/PIP_Problem.defs.hh +++ b/src/PIP_Problem.defs.hh @@ -83,6 +83,7 @@ operator<<(std::ostream& s, const PIP_Problem& p); the change of objective function and the change of optimization mode. */ class Parma_Polyhedra_Library::PIP_Problem { + friend class PIP_Solution_Node; public: //! Builds a trivial PIP problem. /*! diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 45d25e1..b81d10b 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -22,6 +22,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <ppl-config.h> #include "PIP_Tree.defs.hh" +#include "PIP_Problem.defs.hh" #include <algorithm> @@ -64,12 +65,14 @@ negate_assign(Row& x, const Row& y) { } // namespace -PIP_Tree_Node::PIP_Tree_Node() - : constraints_() { +PIP_Tree_Node::PIP_Tree_Node(PIP_Problem* p) + : problem(p), + constraints_() { } PIP_Tree_Node::PIP_Tree_Node(const PIP_Tree_Node &x) - : constraints_(x.constraints_) { + : problem(x.problem), + constraints_(x.constraints_) { } PIP_Decision_Node::~PIP_Decision_Node() { @@ -81,8 +84,8 @@ PIP_Decision_Node::~PIP_Decision_Node() { PIP_Solution_Node::~PIP_Solution_Node() { } -PIP_Solution_Node::PIP_Solution_Node() - : PIP_Tree_Node(), +PIP_Solution_Node::PIP_Solution_Node(PIP_Problem* p) + : PIP_Tree_Node(p), tableau(), basis(), mapping(), @@ -99,7 +102,7 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x) PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, bool empty_constraints) - : PIP_Tree_Node(), + : PIP_Tree_Node(x.problem), tableau(x.tableau), basis(x.basis), mapping(x.mapping), @@ -108,8 +111,10 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, constraints_ = x.constraints_; } -PIP_Decision_Node::PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp) - : PIP_Tree_Node(), +PIP_Decision_Node::PIP_Decision_Node(PIP_Problem* p, + PIP_Tree_Node* fcp, + PIP_Tree_Node* tcp) + : PIP_Tree_Node(p), true_child(tcp), false_child(fcp) { } @@ -882,13 +887,13 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, } /* Create a decision Node to become parent of current Node */ - PIP_Decision_Node *parent = new PIP_Decision_Node(fals, tru); + PIP_Decision_Node *parent = new PIP_Decision_Node(problem, fals, tru); parent->add_constraint(test); if (!cs.empty()) { /* If node to be solved had tautologies, store them in a new decision node */ - parent = new PIP_Decision_Node(0, parent); + parent = new PIP_Decision_Node(problem, 0, parent); cs.swap(parent->constraints_); } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 7ac9ec2..fcbd62e 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -75,7 +75,7 @@ public: protected: //! Default constructor. - PIP_Tree_Node(); + PIP_Tree_Node(PIP_Problem* p); //! Copy constructor. PIP_Tree_Node(const PIP_Tree_Node &x); @@ -89,6 +89,9 @@ protected: friend class PIP_Decision_Node; friend class PIP_Solution_Node; + //! A pointer to the master problem object. + PIP_Problem* problem; + //! The local system of parameter constraints. Constraint_System constraints_; @@ -141,7 +144,7 @@ protected: class PIP_Solution_Node : public PIP_Tree_Node { public: //! Default constructor. - PIP_Solution_Node(); + PIP_Solution_Node(PIP_Problem* p); //! Destructor. ~PIP_Solution_Node(); @@ -383,7 +386,7 @@ private: \exception std::invalid_argument Thrown if \p cs contains strict inequalities. */ - PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); + PIP_Decision_Node(PIP_Problem* p, PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); protected: /*! \brief

1 0

[GIT] ppl/ppl(floating_point): Little correction in two_variables_affine_image method.
by Roberto Amadini 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1508fe8fbb7be516e7cebabb60d8fe30c1399407 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1508fe8fbb7b… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 22 10:55:49 2009 +0200 Little correction in two_variables_affine_image method. --- src/BD_Shape.templates.hh | 5 ++++- 1 files changed, 4 insertions(+), 1 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 08b1c5d..8b5c49d 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4237,7 +4237,10 @@ void BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& lf, const dimension_type& space_dim) { - reset_shortest_path_closed(); + // Shortest-path closure is preserved, but not reduction. + if (marked_shortest_path_reduced()) + reset_shortest_path_reduced(); + Linear_Form< Interval<T, Interval_Info> > minus_lf(lf); minus_lf.negate();

1 0

[GIT] ppl/ppl(floating_point): Fixed one cut-&-paste error.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c6e8ada743e7203512e9f830e052e52256458ac6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c6e8ada743e7… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 09:36:01 2009 +0200 Fixed one cut-&-paste error. Use a single call of bounded_affine_image instead of calling generalized_affine_image twice. Added two FIXME notes. --- src/Floating_Point_Expression.defs.hh | 6 ++++++ src/Octagonal_Shape.defs.hh | 2 +- src/Polyhedron.templates.hh | 9 ++------- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index ec21e1b..ffaf2b7 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -34,6 +34,12 @@ namespace Parma_Polyhedra_Library { //! Exception class indicating the failure of a linearization attempt. class Linearization_Failed {}; +/* + FIXME: considering adapting the whole code of Floating_Point_Expression + to use the policies defined in Float.defs.hh instead of the following + ones that contain duplicate information. +*/ + //! Policy class defining the IEEE754 half precision format. struct IEEE754_Half { static const unsigned short fraction_bits = 10; diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 111d2de..61aebe7 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1864,7 +1864,7 @@ private: const Linear_Form< Interval<T, Interval_Info> >& lf, N& result) const; - // FIXME: the name is questionable. + // FIXME: this function is currently not used. Consider removing it. static void interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, const N& int_ub, const N& int_lb, diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index a8e2a07..7adf015 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -305,7 +305,7 @@ Polyhedron::refine_with_linear_form_inequality( // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, - "Polyhedron::affine_image:" + "Polyhedron::refine_with_linear_form_inequality:" " FP_Format not a floating point type."); // Dimension compatibility checks. @@ -383,12 +383,7 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { lo_coeff, hi_coeff); // Finally, do the assignment. - PPL_DIRTY_TEMP_COEFFICIENT(one_coeff); - one_coeff = 1; - generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx_le + lo_coeff, - one_coeff); - generalized_affine_image(var, LESS_OR_EQUAL, lf_approx_le + hi_coeff, - one_coeff); + bounded_affine_image(var, lf_approx_le + lo_coeff, lf_approx_le + hi_coeff); }

1 0

[GIT] ppl/ppl(floating_point): Added another test for the general case of affine_image.
by Roberto Amadini 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 3e7c9713946e790f1894bc8d35c3ab97535fb7be URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e7c9713946e… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 21 19:23:37 2009 +0200 Added another test for the general case of affine_image. --- tests/Floating_Point_Expression/affineimage3.cc | 4 +- tests/Floating_Point_Expression/bdshape1.cc | 40 +++++++++++++++++++++++ 2 files changed, 42 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index f439275..5cd40be 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -287,7 +287,8 @@ bool test09() { } -// tests affine_image(A, i + i0*A + i1*B) +// tests affine_image(A, i + i0*A + i1*B) where +// i = [0, 2], i0 = [1, 1] and i1 = [1, 2]. bool test10() { Variable A(0); @@ -300,7 +301,6 @@ bool test10() { oc1.add_constraint(B <= 2); oc1.add_constraint(A - B >= 0); db_r_oc tmp(1); - tmp.join_assign(1); Linear_Form<db_r_oc> l(A); l *= tmp; tmp.lower() = 0; diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index 0c8e305..9d3053c 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -279,6 +279,45 @@ bool test09() { return ok; } +// tests affine_image(A, i + i0*A + i1*B) where +// i = [0, 2], i0 = [1, 1] and i1 = [1, 2]. +bool test10() { + + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(2); + bd1.add_constraint(A >= 0); + bd1.add_constraint(A <= 2); + bd1.add_constraint(B >= 0); + bd1.add_constraint(B <= 2); + bd1.add_constraint(A - B >= 0); + db_r_oc tmp(1); + Linear_Form<db_r_oc> l(A); + l *= tmp; + tmp.lower() = 0; + tmp.upper() = 2; + l += tmp; + tmp.lower() = 1; + tmp.upper() = 2; + l += tmp * Linear_Form<db_r_oc>(B); + bd1.affine_image(A,l); + print_constraints(bd1, "*** bd1.affine_image(A, i + i0*A + i1*B) ***"); + + BD_Shape<double> know_result(2); + know_result.add_constraint(A >= 0); + know_result.add_constraint(A <= 8); + know_result.add_constraint(B >= 0); + know_result.add_constraint(B <= 2); + know_result.add_constraint(A - B <= 6); + know_result.add_constraint(-A + B <= 0); + print_constraints(know_result, "*** know_result ***"); + + bool ok = (bd1 == know_result); + + return ok; +} + } // namespace BEGIN_MAIN @@ -291,4 +330,5 @@ BEGIN_MAIN DO_TEST(test07); DO_TEST(test08); DO_TEST(test09); + DO_TEST(test10); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in affine_image and modified one_variable_affine_image.
by Roberto Amadini 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: faefe0f0d2247dbd65bdd5aebade57a61b2e6a9b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=faefe0f0d224… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 21 18:45:29 2009 +0200 Fixed a bug in affine_image and modified one_variable_affine_image. Added a new test for the general case. --- src/BD_Shape.templates.hh | 130 +++++++++++++-------------- tests/Floating_Point_Expression/bdshape1.cc | 27 ++++++ 2 files changed, 90 insertions(+), 67 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 5cbf5a5..08b1c5d 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4103,11 +4103,12 @@ BD_Shape<T>::affine_image(const Variable& var, } else if (t == 1) { const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id - 1)); - one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim); - PPL_ASSERT(OK()); - return; + if(w_coeff == 1 || w_coeff == -1) { + one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim); + PPL_ASSERT(OK()); + return; + } } - two_variables_affine_image(var_id, lf, space_dim); PPL_ASSERT(OK()); } @@ -4154,76 +4155,71 @@ void BD_Shape<T> bool is_b_zero = (b_mlb == 0 && b_ub == 0); // true if w_coeff = [1;1] bool is_w_coeff_one = (w_coeff == 1); - // true if w_coeff = [-1;-1]. - bool is_w_coeff_minus_one = (w_coeff == -1); - if (is_w_coeff_one || is_w_coeff_minus_one) { - if (w_id == var_id) { - // Here `lf' is of the form: [+/-1;+/-1] * v + b. - if (is_w_coeff_one) { - if (is_b_zero) - // The transformation is the identity function. - return; - else { - // Translate all the constraints on `var' by adding the value - // `b_ub' or subtracting the value `b_lb'. - DB_Row<N>& dbm_v = dbm[var_id]; - for (dimension_type i = space_dim + 1; i-- > 0; ) { - N& dbm_vi = dbm_v[i]; - add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP); - N& dbm_iv = dbm[i][var_id]; - add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP); - } - // Both shortest-path closure and reduction are preserved. - } - } + if (w_id == var_id) { + // Here `lf' is of the form: [+/-1;+/-1] * v + b. + if (is_w_coeff_one) { + if (is_b_zero) + // The transformation is the identity function. + return; else { - // Here `w_coeff = [-1;-1]. - // Remove the binary constraints on `var'. - forget_binary_dbm_constraints(var_id); - std::swap(dbm[var_id][0], dbm[0][var_id]); - // Shortest-path closure is not preserved. - reset_shortest_path_closed(); - if (!is_b_zero) { - // Translate the unary constraints on `var' by adding the value - // `b_ub' or subtracting the value `b_lb'. - N& dbm_v0 = dbm[var_id][0]; - add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP); - N& dbm_0v = dbm[0][var_id]; - add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); + // Translate all the constraints on `var' by adding the value + // `b_ub' or subtracting the value `b_lb'. + DB_Row<N>& dbm_v = dbm[var_id]; + for (dimension_type i = space_dim + 1; i-- > 0; ) { + N& dbm_vi = dbm_v[i]; + add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP); + N& dbm_iv = dbm[i][var_id]; + add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP); } + // Both shortest-path closure and reduction are preserved. + } + } + else { + // Here `w_coeff = [-1;-1]. + // Remove the binary constraints on `var'. + forget_binary_dbm_constraints(var_id); + std::swap(dbm[var_id][0], dbm[0][var_id]); + // Shortest-path closure is not preserved. + reset_shortest_path_closed(); + if (!is_b_zero) { + // Translate the unary constraints on `var' by adding the value + // `b_ub' or subtracting the value `b_lb'. + N& dbm_v0 = dbm[var_id][0]; + add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP); + N& dbm_0v = dbm[0][var_id]; + add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); } } + } + else { + // Here `w != var', so that `lf' is of the form + // [+/-1;+/-1] * w + b. + // Remove all constraints on `var'. + forget_all_dbm_constraints(var_id); + // Shortest-path closure is preserved, but not reduction. + if (marked_shortest_path_reduced()) + reset_shortest_path_reduced(); + if (is_w_coeff_one) { + // Add the new constraints `var - w >= b_lb' + // `and var - w <= b_ub'. + add_dbm_constraint(w_id, var_id, b_ub); + add_dbm_constraint(var_id, w_id, b_mlb); + } else { - // Here `w != var', so that `lf' is of the form - // [+/-1;+/-1] * w + b. - // Remove all constraints on `var'. - forget_all_dbm_constraints(var_id); - // Shortest-path closure is preserved, but not reduction. - if (marked_shortest_path_reduced()) - reset_shortest_path_reduced(); - - if (is_w_coeff_one) { - // Add the new constraints `var - w >= b_lb' - // `and var - w <= b_ub'. - add_dbm_constraint(w_id, var_id, b_ub); - add_dbm_constraint(var_id, w_id, b_mlb); + // We have to add the constraint `v + w == b', over-approximating it + // by computing lower and upper bounds for `w'. + const N& mlb_w = dbm[w_id][0]; + if (!is_plus_infinity(mlb_w)) { + // Add the constraint `v <= ub - lb_w'. + add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP); + reset_shortest_path_closed(); } - else { - // We have to add the constraint `v + w == b', over-approximating it - // by computing lower and upper bounds for `w'. - const N& mlb_w = dbm[w_id][0]; - if (!is_plus_infinity(mlb_w)) { - // Add the constraint `v <= ub - lb_w'. - add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP); - reset_shortest_path_closed(); - } - const N& ub_w = dbm[0][w_id]; - if (!is_plus_infinity(ub_w)) { - // Add the constraint `v >= lb - ub_w'. - add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP); - reset_shortest_path_closed(); - } + const N& ub_w = dbm[0][w_id]; + if (!is_plus_infinity(ub_w)) { + // Add the constraint `v >= lb - ub_w'. + add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP); + reset_shortest_path_closed(); } } } diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index e5f06d1..0c8e305 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -253,6 +253,32 @@ bool test08() { return ok; } +// tests affine_image(B, [-0.5, 0.5]*A) +bool test09() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc coeff(-0.5); + coeff.join_assign(0.5); + Linear_Form<db_r_oc> l(A); + l *= coeff; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, [-0.5, 0.5]*A) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(A - B <= 3); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + } // namespace BEGIN_MAIN @@ -264,4 +290,5 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Implemented a preliminary (yet untested) version of methods
by Roberto Amadini 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 351e41c9b7853cd031d34ce681841b78ece3cab5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=351e41c9b785… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 21 18:02:31 2009 +0200 Implemented a preliminary (yet untested) version of methods BD_Shape::linear_form_upper_bound and BD_Shape::two_variables_affine_image. --- src/BD_Shape.defs.hh | 14 ++- src/BD_Shape.templates.hh | 119 ++++++++++++++++++++++++++- tests/Floating_Point_Expression/bdshape1.cc | 1 - 3 files changed, 125 insertions(+), 9 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 96a3fd7..3dc29bb 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -2088,15 +2088,21 @@ private: const Interval<T, Interval_Info>& w_coeff, const dimension_type& w_id, const dimension_type& space_dim); - + /* \brief Auxiliary function for \ref affine_relation "affine image" that handle the general case: \f$l \equal ax + by + c\f$ */ template <typename Interval_Info> - void two_variables_affine_image(const Variable& var, - const dimension_type& var_id, - const Linear_Form< Interval<T,Interval_Info> >& lf); + void two_variables_affine_image(const dimension_type& var_id, + const Linear_Form< Interval<T,Interval_Info> >& lf, + const dimension_type& space_dim); + + template <typename Interval_Info> + void linear_form_upper_bound( + const Linear_Form< Interval<T, Interval_Info> >& lf, + N& result, + const dimension_type& space_dim) const; //! An helper function for the computation of affine relations. /*! diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 734f503..5cbf5a5 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4108,7 +4108,7 @@ BD_Shape<T>::affine_image(const Variable& var, return; } - //two_variables_affine_image(var, var_id, lf); + two_variables_affine_image(var_id, lf, space_dim); PPL_ASSERT(OK()); } @@ -4237,11 +4237,122 @@ void BD_Shape<T> template <typename T> template <typename Interval_Info> void BD_Shape<T> -::two_variables_affine_image(const Variable& var, - const dimension_type& var_id, - const Linear_Form< Interval<T, Interval_Info> >& lf) { +::two_variables_affine_image(const dimension_type& var_id, + const Linear_Form< Interval<T, Interval_Info> >& lf, + const dimension_type& space_dim) { + + reset_shortest_path_closed(); + + Linear_Form< Interval<T, Interval_Info> > minus_lf(lf); + minus_lf.negate(); + + // Declare temporaries outside the loop. + PPL_DIRTY_TEMP(N, upper_bound); + + // Update binary constraints on var FIRST. + for (dimension_type curr_var = 1; curr_var < var_id; ++curr_var) { + Variable current(curr_var - 1); + linear_form_upper_bound(lf - current, upper_bound, space_dim); + assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); + } + for (dimension_type curr_var = var_id + 1; curr_var <= space_dim; + ++curr_var) { + Variable current(curr_var - 1); + linear_form_upper_bound(lf - current, upper_bound, space_dim); + assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); + } + // Finally, update unary constraints on var. + PPL_DIRTY_TEMP(N, lf_ub); + linear_form_upper_bound(lf, lf_ub, space_dim); + PPL_DIRTY_TEMP(N, minus_lf_ub); + linear_form_upper_bound(minus_lf, minus_lf_ub, space_dim); + assign_r(dbm[0][var_id], lf_ub, ROUND_NOT_NEEDED); + assign_r(dbm[var_id][0], minus_lf_ub, ROUND_NOT_NEEDED); } +template <typename T> +template <typename Interval_Info> +void +BD_Shape<T>:: +linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, + N& result, + const dimension_type& space_dim) const { + + // Check that T is a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "BD_Shape<T>::linear_form_upper_bound:" + " T not a floating point type."); + + const dimension_type lf_space_dimension = lf.space_dimension(); + PPL_ASSERT(lf_space_dimension <= space_dim); + + typedef Interval<T, Interval_Info> FP_Interval_Type; + + PPL_DIRTY_TEMP(N, curr_lb); + PPL_DIRTY_TEMP(N, curr_ub); + PPL_DIRTY_TEMP(N, curr_var_ub); + PPL_DIRTY_TEMP(N, curr_minus_var_ub); + + PPL_DIRTY_TEMP(N, first_comparison_term); + PPL_DIRTY_TEMP(N, second_comparison_term); + + PPL_DIRTY_TEMP(N, negator); + + assign_r(result, lf.inhomogeneous_term().upper(), ROUND_NOT_NEEDED); + + for (dimension_type curr_var = 0, n_var = 0; curr_var < lf_space_dimension; + ++curr_var) { + n_var = curr_var + 1; + const FP_Interval_Type& curr_coefficient = + lf.coefficient(Variable(curr_var)); + assign_r(curr_lb, curr_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(curr_ub, curr_coefficient.upper(), ROUND_NOT_NEEDED); + if (curr_lb != 0 || curr_ub != 0) { + assign_r(curr_var_ub, dbm[0][n_var], ROUND_NOT_NEEDED); + neg_assign_r(curr_minus_var_ub, dbm[n_var][0], ROUND_NOT_NEEDED); + // Optimize the most commons cases: curr = +/-[1;1] + if (curr_lb == 1 && curr_ub == 1) { + add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub), + ROUND_UP); + } + else if (curr_lb == -1 && curr_ub == -1) { + neg_assign_r(negator, std::min(curr_var_ub, curr_minus_var_ub), + ROUND_NOT_NEEDED); + add_assign_r(result, result, negator, ROUND_UP); + } + else { + // Next addend will be the maximum of four quantities. + assign_r(first_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(second_comparison_term, curr_var_ub, curr_lb, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_lb, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + + add_assign_r(result, result, first_comparison_term, ROUND_UP); + } + } + } +} template <typename T> void diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index a9886b4..e5f06d1 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -244,7 +244,6 @@ bool test08() { known_result.add_constraint(A <= 12); known_result.add_constraint(B <= 2); known_result.add_constraint(B >= -10); - //known_result.add_constraint(-B - A <= 0); known_result.add_constraint(-A + B <= 4); known_result.add_constraint(A - B <= 22); print_constraints(known_result, "*** known_result ***");

1 0

[GIT] ppl/ppl(floating_point): Added more floating point formats.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 7365b420d7ab0984de1d19f7764c24892d5dff38 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7365b420d7ab… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 16:59:22 2009 +0200 Added more floating point formats. Added some parametric typedefs for tests. --- src/Floating_Point_Expression.defs.hh | 28 ++++++++++++++++++ tests/ppl_test.hh | 50 +++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+), 0 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index 71b77ad..ec21e1b 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -34,6 +34,13 @@ namespace Parma_Polyhedra_Library { //! Exception class indicating the failure of a linearization attempt. class Linearization_Failed {}; +//! Policy class defining the IEEE754 half precision format. +struct IEEE754_Half { + static const unsigned short fraction_bits = 10; + static const unsigned short exponent_bits = 5; + static const unsigned short exponent_bias = 15; +}; + //! Policy class defining the IEEE754 single precision format. struct IEEE754_Single { static const unsigned short fraction_bits = 23; @@ -48,6 +55,27 @@ struct IEEE754_Double { static const unsigned short exponent_bias = 1023; }; +//! Policy class defining the IEEE754 quadruple precision format. +struct IEEE754_Quadruple { + static const unsigned short fraction_bits = 112; + static const unsigned short exponent_bits = 15; + static const unsigned short exponent_bias = 16383; +}; + +//! Policy class defining the IBM single precision format. +struct IBM_Single { + static const unsigned short fraction_bits = 24; + static const unsigned short exponent_bits = 7; + static const unsigned short exponent_bias = 64; +}; + +//! Policy class defining the IBM double precision format. +struct IBM_Double { + static const unsigned short fraction_bits = 56; + static const unsigned short exponent_bits = 7; + static const unsigned short exponent_bias = 64; +}; + /*! \brief \ingroup PPL_CXX_Interface A floating point expression on a given format. diff --git a/tests/ppl_test.hh b/tests/ppl_test.hh index ff7e1eb..628c3a0 100644 --- a/tests/ppl_test.hh +++ b/tests/ppl_test.hh @@ -29,6 +29,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <stdexcept> #include <sstream> #include <list> +#include <map> #include <iterator> #include <string> #include <iostream> @@ -513,6 +514,19 @@ struct Floating_Real_Open_Interval_Info_Policy { const_bool_nodef(check_inexact, false); }; +struct Floating_Real_Closed_Interval_Info_Policy { + const_bool_nodef(store_special, false); + const_bool_nodef(store_open, false); + const_bool_nodef(cache_empty, false); + const_bool_nodef(cache_singleton, true); + const_bool_nodef(cache_normalized, false); + const_int_nodef(next_bit, 0); + const_bool_nodef(may_be_empty, false); + const_bool_nodef(may_contain_infinity, false); + const_bool_nodef(check_empty_result, false); + const_bool_nodef(check_inexact, false); +}; + typedef Interval_Restriction_None <Interval_Info_Bitset<unsigned int, Floating_Real_Open_Interval_Info_Policy> > Floating_Real_Open_Interval_Info; @@ -549,6 +563,42 @@ typedef BD_Shape<BD_SHAPE_INSTANCE> TBD_Shape; //! The incarnation of Octagonal_Shape under test. typedef Octagonal_Shape<OCTAGONAL_SHAPE_INSTANCE> TOctagonal_Shape; +// For floating point analysis. +#ifdef ANALYZER_FP_FORMAT +#ifdef ANALYZED_FP_FORMAT +//! The type of an interval with floating point boundaries. +typedef Interval<ANALYZER_FP_FORMAT, + Floating_Real_Closed_Interval_Info_Policy> FP_Interval; + +//! The type of an interval linear form. +typedef Linear_Form<FP_Interval> FP_Linear_Form; + +//! The type of an interval abstract store. +typedef std::map<dimension_type, FP_Interval> FP_Interval_Abstract_Store; + +//! The type of a linear form abstract store. +typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; + +/*! \brief + The incarnation of Floating_Point_Expression under test for analyzing + floating point computations. +*/ +typedef Floating_Point_Expression<FP_Interval_Type, ANALYZED_FP_FORMAT> FP_Expression; + +/*! \brief + The incarnation of BD_Shape under test for analyzing + floating point computations. +*/ +typedef BD_Shape<ANALYZER_FP_FORMAT> FP_BD_Shape; + +/*! \brief + The incarnation of Octagon under test for analyzing + floating point computations. +*/ +typedef Octagon<ANALYZER_FP_FORMAT> FP_Octagon; +#endif +#endif + template <typename Shape> inline bool has_exact_coefficient_type(const Shape&) {

1 0