September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added several corrections in order to parametrize floatingpointexpr1.cc
by Roberto Amadini 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 43b5cb98ab200cabeb3c984baa6ad6bb99e764b3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=43b5cb98ab20… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 23 16:53:23 2009 +0200 Added several corrections in order to parametrize floatingpointexpr1.cc --- src/Floating_Point_Expression.defs.hh | 13 +- tests/Floating_Point_Expression/Makefile.am | 44 +++--- .../floatingpointexpr1.cc | 147 +++++++++++--------- tests/Floating_Point_Expression/octagonalshape2.cc | 15 +- tests/ppl_test.hh | 2 +- 5 files changed, 120 insertions(+), 101 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=43b5cb98…

1 0

[GIT] ppl/ppl(floating_point): Parametrized floatingpointexpr1.cc
by Roberto Amadini 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 9691bf1a68b4e732c1b5a01838cfa000eb7f49fb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9691bf1a68b4… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 23 11:36:58 2009 +0200 Parametrized floatingpointexpr1.cc --- .../floatingpointexpr1.cc | 355 ++++++++------------ tests/Floating_Point_Expression/octagonalshape1.cc | 2 +- tests/ppl_test.hh | 58 +++- 3 files changed, 202 insertions(+), 213 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=9691bf1a…

1 0

[GIT] ppl/ppl(floating_point): Made the refine_fp_interval_abstract_store methods inline.
by Fabio Bossi 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 8128edd2954e9c4f63f9fea8bce387a2310c1183 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8128edd2954e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 23 17:01:36 2009 +0200 Made the refine_fp_interval_abstract_store methods inline. --- src/Octagonal_Shape.inlines.hh | 17 +++++++++++++++++ src/Octagonal_Shape.templates.hh | 21 --------------------- src/Polyhedron.inlines.hh | 16 ++++++++++++++++ src/Polyhedron.templates.hh | 20 -------------------- 4 files changed, 33 insertions(+), 41 deletions(-) diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index b76c327..cee791c 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -612,6 +612,23 @@ Octagonal_Shape<T>::strictly_contains(const Octagonal_Shape& y) const { return x.contains(y) && !y.contains(x); } +template <typename T> +template <typename Interval_Info> +inline void +Octagonal_Shape<T>:: +refine_fp_interval_abstract_store( + Box< Interval<T, Interval_Info> >& store) const { + + // Check that T is a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::refine_fp_interval_abstract_store:" + " T not a floating point type."); + + typedef Interval<T, Interval_Info> FP_Interval_Type; + store.intersection_assign(Box<FP_Interval_Type>(*this)); + +} + /*! \relates Octagonal_Shape */ template <typename Temp, typename To, typename T> inline bool diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 628e791..92f93f6 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -30,7 +30,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.defs.hh" #include "Linear_Form.defs.hh" #include "meta_programming.hh" -#include "Box.defs.hh" #include "assert.hh" #include <vector> #include <deque> @@ -856,7 +855,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( } PPL_ASSERT(OK()); - } template <typename T> @@ -5303,7 +5301,6 @@ Octagonal_Shape<T>::affine_image(const Variable var, assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); PPL_ASSERT(OK()); - } template <typename T> @@ -5418,24 +5415,6 @@ interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, assign_r(result, std::max(result, second_comparison_term), ROUND_NOT_NEEDED); assign_r(result, std::max(result, third_comparison_term), ROUND_NOT_NEEDED); assign_r(result, std::max(result, fourth_comparison_term), ROUND_NOT_NEEDED); - -} - -template <typename T> -template <typename Interval_Info> -void -Octagonal_Shape<T>:: -refine_fp_interval_abstract_store( - Box< Interval<T, Interval_Info> >& store) const { - - // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, - "Octagonal_Shape<T>::refine_fp_interval_abstract_store:" - " T not a floating point type."); - - typedef Interval<T, Interval_Info> FP_Interval_Type; - store.intersection_assign(Box<FP_Interval_Type>(*this)); - } template <typename T> diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index d20eaf5..5de0af8 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -372,6 +372,22 @@ Polyhedron::add_recycled_congruences(Congruence_System& cgs) { add_congruences(cgs); } +template <typename FP_Format, typename Interval_Info> +inline void +Polyhedron:: +refine_fp_interval_abstract_store( + Box< 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; + store.intersection_assign(Box<FP_Interval_Type>(*this)); + +} + /*! \relates Polyhedron */ inline bool operator!=(const Polyhedron& x, const Polyhedron& y) { diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index ed58841..880d88b 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -339,7 +339,6 @@ Polyhedron::refine_with_linear_form_inequality( // Finally, do the refinement. refine_with_constraint(lf_approx_le <= 0); - } template <typename FP_Format, typename Interval_Info> @@ -383,7 +382,6 @@ const Box< Interval<FP_Format, Interval_Info> >& store) { // Finally, do the assignment. bounded_affine_image(var, lf_approx_le + lo_coeff, lf_approx_le + hi_coeff); - } template <typename FP_Format, typename Interval_Info> @@ -403,7 +401,6 @@ Polyhedron::overapproximate_linear_form( typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; - typedef Box<FP_Interval_Type> Interval_Abstract_Store; result = FP_Linear_Form(lf.inhomogeneous_term()); // FIXME: this may not be policy-neutral. @@ -429,7 +426,6 @@ Polyhedron::overapproximate_linear_form( result += curr_addend_lf; } } - } template <typename FP_Format, typename Interval_Info> @@ -539,22 +535,6 @@ Polyhedron::convert_to_integer_expressions( res_hi_coeff = Coefficient(0); } -template <typename FP_Format, typename Interval_Info> -void -Polyhedron:: -refine_fp_interval_abstract_store( - Box< 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; - store.intersection_assign(Box<FP_Interval_Type>(*this)); - -} - template <typename C> void Polyhedron::throw_dimension_incompatible(const char* method,

1 0

[GIT] ppl/ppl(pip): Removed useless parameter in PIP_Tree_Node:: update_tableau method.
by François Galea 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: pip Commit: 44241590e1fdc021d9d28236dfda1a97b20a6668 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=44241590e1fd… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 23 11:15:32 2009 +0200 Removed useless parameter in PIP_Tree_Node::update_tableau method. --- src/PIP_Problem.cc | 3 +-- src/PIP_Tree.cc | 12 ++++-------- src/PIP_Tree.defs.hh | 18 +++--------------- 3 files changed, 8 insertions(+), 25 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index a8925b5..ced38e3 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -79,8 +79,7 @@ PPL::PIP_Problem::solve() const { if (current_solution == 0) x.current_solution = new PIP_Solution_Node(&x); - x.current_solution->update_tableau(&x.current_solution, - external_space_dim, + x.current_solution->update_tableau(external_space_dim, first_pending_constraint, input_cs, parameters); diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 89f40f1..1f904eb 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -275,19 +275,16 @@ PIP_Decision_Node::OK() const { } void -PIP_Decision_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, - dimension_type external_space_dim, +PIP_Decision_Node::update_tableau(dimension_type external_space_dim, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters) { - true_child->update_tableau(&true_child, - external_space_dim, + true_child->update_tableau(external_space_dim, first_pending_constraint, input_cs, parameters); if (false_child) - false_child->update_tableau(&false_child, - external_space_dim, + false_child->update_tableau(external_space_dim, first_pending_constraint, input_cs, parameters); @@ -558,8 +555,7 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { } void -PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, - dimension_type external_space_dim, +PIP_Solution_Node::update_tableau(dimension_type external_space_dim, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters) { diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 1893dd6..5f409f3 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -97,9 +97,6 @@ protected: /*! \brief Populates the parametric simplex tableau using external data, if necessary - \param parent_ref - a pointer to the parent reference to \p this - \param external_space_dim size of constraints (variables and parameters added) @@ -113,8 +110,7 @@ protected: \param parameters a \c std::set of indices of the parameters in the constraints */ - virtual void update_tableau(PIP_Tree_Node **parent_ref, - dimension_type external_space_dim, + virtual void update_tableau(dimension_type external_space_dim, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters) = 0; @@ -305,9 +301,6 @@ protected: /*! \brief Populates the parametric simplex tableau using external data, if necessary - \param parent_ref - a pointer to the parent reference to \p this - \param external_space_dim size of constraints (variables and parameters added) @@ -321,8 +314,7 @@ protected: \param parameters a \c std::set of indices of the parameters in the constraints */ - virtual void update_tableau(PIP_Tree_Node **parent_ref, - dimension_type external_space_dim, + virtual void update_tableau(dimension_type external_space_dim, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters); @@ -400,9 +392,6 @@ protected: /*! \brief Populates the parametric simplex tableau using external data, if necessary - \param parent_ref - a pointer to the parent reference to \p this - \param external_space_dim size of constraints (variables and parameters added) @@ -416,8 +405,7 @@ protected: \param parameters a \c std::set of indices of the parameters in the constraints */ - virtual void update_tableau(PIP_Tree_Node **parent_ref, - dimension_type external_space_dim, + virtual void update_tableau(dimension_type external_space_dim, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters);

1 0

[GIT] ppl/ppl(pip): Implemented display of solution trees.
by François Galea 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: pip Commit: 4eb68b6e2a67c8e0ae368cfa66b3cb8c567b4a94 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4eb68b6e2a67… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 23 10:53:15 2009 +0200 Implemented display of solution trees. --- src/PIP_Problem.cc | 9 ++++++++ src/PIP_Tree.cc | 4 +- src/PIP_Tree.defs.hh | 2 +- tests/PIP_Problem/pipproblem.cc | 41 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 53 insertions(+), 3 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index 6d651fa..a8925b5 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -105,6 +105,15 @@ PPL::PIP_Problem::solve() const { throw std::runtime_error("PPL internal error"); } +PPL::PIP_Tree +PPL::PIP_Problem::solution() const { + return current_solution; +} + +PPL::PIP_Tree +PPL::PIP_Problem::optimizing_solution() const { + return current_solution; +} bool PPL::PIP_Problem::OK() const { diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index b8169b0..89f40f1 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -433,8 +433,8 @@ PIP_Solution_Node::ascii_load(std::istream& s) { } const Linear_Expression& -PIP_Solution_Node::parametric_values(Variable v) { - update_solution(); +PIP_Solution_Node::parametric_values(const Variable &v) const { + const_cast<PIP_Solution_Node&>(*this).update_solution(); Variables_Set& parameters = problem->parameters; dimension_type id = v.id(); dimension_type j; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 6e9a954..1893dd6 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -163,7 +163,7 @@ public: Thrown if \p v is dimension-incompatible with \p *this or if \p v is a parameter. */ - const Linear_Expression& parametric_values(Variable v); + const Linear_Expression& parametric_values(const Variable &v) const; void ascii_dump(std::ostream& s) const; bool ascii_load(std::istream& s); diff --git a/tests/PIP_Problem/pipproblem.cc b/tests/PIP_Problem/pipproblem.cc index df9f96f..8d84a95 100644 --- a/tests/PIP_Problem/pipproblem.cc +++ b/tests/PIP_Problem/pipproblem.cc @@ -24,6 +24,43 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace { +void +display_solution(const PIP_Tree pip, const Variables_Set &vars, int indent=0) { + using namespace std; + using namespace Parma_Polyhedra_Library::IO_Operators; + if (!pip) { + nout << setw(indent*2) << "" << "_|_" << endl; + } else { + const Constraint_System &constraints = pip->constraints(); + if (!constraints.empty()) { + nout << setw(indent*2) << "" << "if "; + Constraint_System::const_iterator begin = constraints.begin(); + Constraint_System::const_iterator end = constraints.end(); + Constraint_System::const_iterator i; + for (i = begin; i != end; ++i) + nout << ((i==begin)?"":" and ") << *i; + nout << " then" << endl; + } + const PIP_Decision_Node* dn = pip->as_decision(); + if (dn) { + display_solution(dn->child_node(true), vars, indent+1); + nout << setw(indent*2) << "" << "else" << endl; + display_solution(dn->child_node(false), vars, indent+1); + } else { + const PIP_Solution_Node* sn = pip->as_solution(); + Variables_Set::const_iterator begin = vars.begin(); + Variables_Set::const_iterator end = vars.end(); + Variables_Set::const_iterator i; + nout << setw(indent*2+2) << "" << "{"; + for (i=begin; i!=end; ++i) + nout << ((i==begin)?"":" ; ") << sn->parametric_values(Variable(*i)); + nout << "}" << endl; + nout << setw(indent*2) << "" << "else" << endl; + nout << setw(indent*2+2) << "" << "_|_" << endl; + } + } +} + bool test01() { Variable X1(0); @@ -43,6 +80,10 @@ test01() { PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); bool ok = (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + display_solution(solution, Variables_Set(X1, X2)); + } return ok; }

1 0

[GIT] ppl/ppl(pip): Fixed bugs.
by François Galea 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: pip Commit: 8663b34c028288e99f503e354eff5ccb88e9e707 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8663b34c0282… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 23 11:05:57 2009 +0200 Fixed bugs. --- src/PIP_Tree.cc | 8 +++++--- 1 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index ca6be54..b8169b0 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -450,7 +450,7 @@ PIP_Solution_Node::parametric_values(Variable v) { #endif j = not_a_dimension(); } else - j = id - std::distance(parameters.begin(),location) - 1; + j = id - std::distance(parameters.begin(),location); } return solution[j]; @@ -911,6 +911,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, Row &r = tableau.t[i]; context.add_row(r); add_constraint(r); + sign[i] = POSITIVE; #ifdef NOISY_PIP Constraint_System::const_iterator c = constraints_.begin(); Constraint_System::const_iterator c_end = constraints_.end(); @@ -958,13 +959,14 @@ 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(problem, fals, tru); + PIP_Decision_Node* parent + = new PIP_Decision_Node(fals->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(problem, 0, parent); + parent = new PIP_Decision_Node(fals->problem, 0, parent); cs.swap(parent->constraints_); }

1 0

[GIT] ppl/ppl(pip): Changed index ordering in parameter constraints.
by François Galea 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: pip Commit: 25bfa050fc1d099961022e665157af966c40069f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=25bfa050fc1d… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 23 10:37:14 2009 +0200 Changed index ordering in parameter constraints. --- src/PIP_Tree.cc | 31 +++++++++++++++++++++++-------- src/PIP_Tree.defs.hh | 7 +++---- 2 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 9d8197c..ca6be54 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -40,16 +40,22 @@ add_assign(Row& x, const Row& y, Coefficient_traits::const_reference c) { // Merge constraint system to a Matrix-form context such as x = x U y void -merge_assign(Matrix& x, const Constraint_System& y) { +merge_assign(Matrix& x, + const Constraint_System& y, + const Variables_Set &parameters) { dimension_type width = x.num_columns(); PPL_ASSERT(y.empty() || y.begin()->space_dimension() == width-1); Row row(width, Row::Flags()); + Variables_Set::iterator param_begin = parameters.begin(); + Variables_Set::iterator param_end = parameters.end(); + Variables_Set::iterator pi; + dimension_type j; for (Constraint_System::const_iterator y_i = y.begin(), y_end = y.end(); y_i != y_end; ++y_i) { PPL_ASSERT(y_i->is_nonstrict_inequality()); - for (dimension_type j=width-1; j-- > 0; ) - row[j+1] = y_i->coefficient(Variable(j)); row[0] = y_i->inhomogeneous_term(); + for (pi=param_begin, j=1; pi != param_end; ++pi, ++j) + row[j] = y_i->coefficient(Variable(*pi)); x.add_row(row); } } @@ -211,8 +217,15 @@ PIP_Tree_Node::OK() const { void PIP_Tree_Node::add_constraint(const Row &row) { Linear_Expression e; - for (dimension_type j=row.size(); j-- > 1; ) - e += row[j] * Variable(j-1); + const Variables_Set &parameters = problem->parameter_space_dimensions(); + Variables_Set::const_iterator param_begin = parameters.begin(); + Variables_Set::const_iterator param_end = parameters.end(); + Variables_Set::const_iterator pi; + dimension_type j; + PPL_ASSERT(dimension_type(std::distance(param_begin, param_end))+1 + == row.size()); + for (pi=param_begin, j=1; pi != param_end; ++pi, ++j) + e += row[j] * Variable(*pi); constraints_.insert(e + row[0] >= 0); } @@ -286,13 +299,14 @@ PIP_Decision_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& context) { PIP_Problem_Status stt; PIP_Problem_Status stf = UNFEASIBLE_PIP_PROBLEM; Matrix context_true(context); - merge_assign(context_true, constraints_); + const Variables_Set &parameters = problem->parameter_space_dimensions(); + merge_assign(context_true, constraints_, parameters); stt = true_child->solve(true_child, context_true); if (false_child) { // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); Matrix context_false(context); - merge_assign(context_false, constraints_); + merge_assign(context_false, constraints_, parameters); Row &last = context_false[context_false.num_rows()-1]; negate_assign(last, last); stf = false_child->solve(false_child, context_false); @@ -640,7 +654,8 @@ PIP_Problem_Status PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx) { Matrix context(ctx); - merge_assign(context, constraints_); + const Variables_Set &parameters = problem->parameter_space_dimensions(); + merge_assign(context, constraints_, parameters); const dimension_type n_a_d = not_a_dimension(); Coefficient gcd; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 238ef5b..6e9a954 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -63,10 +63,9 @@ public: /*! \brief Returns the system of parameter constraints controlling \p *this. - The column indices in the constraints are numbered from \c 0 to - <tt>np-1</tt>, where \c np is the total number of parameters. They are - ordered with the same order as the parameter indices in the original - problem. + The indices in the constraints are the same as the original variables and + parameters. Coefficients in indices corresponding to variables always are + zero. */ const Constraint_System& constraints() const;

1 0

[GIT] ppl/ppl(floating_point): Always use Box instead of map for interval abstract stores.
by Fabio Bossi 23 Sep '09

23 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 230e752faf022e041afa79aa1e7f1a4250a3e0bb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=230e752faf02… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 23 12:24:25 2009 +0200 Always use Box instead of map for interval abstract stores. --- src/Octagonal_Shape.defs.hh | 1 - src/Octagonal_Shape.templates.hh | 1 - src/Polyhedron.defs.hh | 7 +++---- src/Polyhedron.templates.hh | 16 ++++++++-------- 4 files changed, 11 insertions(+), 14 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 81ddf92..42166af 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -47,7 +47,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.types.hh" #include "Linear_Form.types.hh" #include <vector> -#include <map> #include <cstddef> #include <climits> #include <iosfwd> diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 04906d6..628e791 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -33,7 +33,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Box.defs.hh" #include "assert.hh" #include <vector> -#include <map> #include <deque> #include <string> #include <iostream> diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index b402794..f2854b4 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -50,7 +50,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.types.hh" #include "Linear_Form.types.hh" #include <vector> -#include <map> #include <iosfwd> namespace Parma_Polyhedra_Library { @@ -1009,7 +1008,7 @@ public: void refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, - const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); + const Box< Interval<FP_Format, Interval_Info> >& store); //! Refines \p store with the constraints defining \p *this. /*! @@ -1215,7 +1214,7 @@ public: template <typename FP_Format, typename Interval_Info> 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); + const Box< Interval<FP_Format, Interval_Info> >& store); /*! \brief Assigns to \p *this the @@ -2661,7 +2660,7 @@ protected: static void overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, - const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, + const Box< Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result); /*! \brief diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index c312028..ed58841 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -28,7 +28,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.defs.hh" #include "Linear_Form.defs.hh" #include <algorithm> -#include <map> #include <deque> namespace Parma_Polyhedra_Library { @@ -301,7 +300,7 @@ void Polyhedron::refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, - const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { + const Box< Interval<FP_Format, Interval_Info> >& store) { // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, @@ -347,7 +346,7 @@ template <typename FP_Format, typename Interval_Info> void 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) { +const Box< Interval<FP_Format, Interval_Info> >& store) { // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, @@ -392,7 +391,7 @@ void Polyhedron::overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, - const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, + const Box< Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result) { // Check that FP_Format is indeed a floating point type. @@ -400,9 +399,11 @@ Polyhedron::overapproximate_linear_form( "Polyhedron::overapproximate_linear_form:" " FP_Format not a floating point type."); + PPL_ASSERT(lf_dimension <= store.space_dimension()); + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; - typedef std::map<dimension_type, FP_Interval_Type> Interval_Abstract_Store; + typedef Box<FP_Interval_Type> Interval_Abstract_Store; result = FP_Linear_Form(lf.inhomogeneous_term()); // FIXME: this may not be policy-neutral. @@ -416,11 +417,10 @@ Polyhedron::overapproximate_linear_form( FP_Format curr_lb = curr_coeff.lower(); FP_Format curr_ub = curr_coeff.upper(); if (curr_lb != 0 || curr_ub != 0) { - typename Interval_Abstract_Store::const_iterator i_ite = store.find(i); - PPL_ASSERT(i_ite != store.end()); + const FP_Interval_Type& curr_int = store.get_iterval(Variable(i)); FP_Interval_Type curr_addend(curr_ub - curr_lb); curr_addend *= aux_divisor2; - curr_addend *= i_ite->second; + curr_addend *= curr_int; result += curr_addend; curr_addend = FP_Interval_Type(curr_lb + curr_ub); curr_addend *= aux_divisor1;

1 0

[GIT] ppl/ppl(floating_point): Fixed another typo that prevented compilation of tests.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 15ed9f61cf8f2bd88b13226ff73b56a07ce1cffd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=15ed9f61cf8f… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 18:23:51 2009 +0200 Fixed another typo that prevented compilation of tests. --- tests/ppl_test.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/ppl_test.hh b/tests/ppl_test.hh index 6e99efe..6e13fdf 100644 --- a/tests/ppl_test.hh +++ b/tests/ppl_test.hh @@ -595,7 +595,7 @@ typedef BD_Shape<ANALYZER_FP_FORMAT> FP_BD_Shape; The incarnation of Octagon under test for analyzing floating point computations. */ -typedef Octagon<ANALYZER_FP_FORMAT> FP_Octagon; +typedef Octagonal_Shape<ANALYZER_FP_FORMAT> FP_Octagonal_Shape; #endif #endif

1 0

[GIT] ppl/ppl(floating_point): Fixed a typo that prevented compilation of tests.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d14d0775d881de693ce17e4f938cf9d0fe3e5450 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d14d0775d881… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 18:12:13 2009 +0200 Fixed a typo that prevented compilation of tests. --- tests/ppl_test.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/ppl_test.hh b/tests/ppl_test.hh index 628c3a0..6e99efe 100644 --- a/tests/ppl_test.hh +++ b/tests/ppl_test.hh @@ -583,7 +583,7 @@ typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; 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; +typedef Floating_Point_Expression<FP_Interval, ANALYZED_FP_FORMAT> FP_Expression; /*! \brief The incarnation of BD_Shape under test for analyzing

1 0