September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Make sure uintptr_t is defined, if at all possible.
by Roberto Bagnara 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: master Commit: 2e103e539bb6f64b214ee11c40dfcb6fe1b81d30 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2e103e539bb6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 11 22:27:40 2009 +0200 Make sure uintptr_t is defined, if at all possible. --- configure.ac | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/configure.ac b/configure.ac index ba08ec1..8a661eb 100644 --- a/configure.ac +++ b/configure.ac @@ -716,6 +716,10 @@ AC_CHECK_DECLS([fma,fmaf,fmal,rintf,rintl], , , [#include <cmath>]) # Checks for the availability of "fast" integral types. AC_CHECK_TYPES([int_fast16_t,int_fast32_t,int_fast64_t,uint_fast16_t,uint_fast32_t,uint_fast64_t]) +# Make sure uintptr_t is defined to an unsigned integer type wide enough +# to hold a pointer, if such a type exists. +AC_TYPE_UINTPTR_T + # Checks on the GMP library.

1 0

[GIT] ppl/ppl(pip): Moved the constraint() method to PIP_Tree_Node class.
by François Galea 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: pip Commit: 92c85879ea35c25a53e3dae171d34a8ac1ad4b14 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=92c85879ea35… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 11 17:09:21 2009 +0200 Moved the constraint() method to PIP_Tree_Node class. --- src/PIP_Tree.defs.hh | 30 ++++++++++-------------------- src/PIP_Tree.inlines.hh | 5 +++++ 2 files changed, 15 insertions(+), 20 deletions(-) diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index acb8b2a..5393c02 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -60,6 +60,16 @@ public: //! Returns \c true if and only if \p *this is well formed. bool OK() const; + /*! \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. + */ + const Constraint_System& constraints() const; + protected: //! A type alias for a sequence of constraints. typedef std::vector<Constraint> Constraint_Sequence; @@ -137,16 +147,6 @@ public: */ const Linear_Expression& parametric_values(Variable v); - /*! \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. - */ - const Constraint_System& constraints(); - void ascii_dump(std::ostream& s) const; bool ascii_load(std::istream& s); @@ -330,16 +330,6 @@ public: //! Returns a pointer to the \p v (true or false) branch of \p *this. PIP_Tree_Node* child_node(bool v); - /*! \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. - */ - const Constraint_System& constraints(); - bool OK() const; private: diff --git a/src/PIP_Tree.inlines.hh b/src/PIP_Tree.inlines.hh index c3b23bc..c7f66bb 100644 --- a/src/PIP_Tree.inlines.hh +++ b/src/PIP_Tree.inlines.hh @@ -64,6 +64,11 @@ inline PIP_Tree_Node::~PIP_Tree_Node() { } +inline const Constraint_System& +PIP_Tree_Node::constraints() const { + return constraints_; +} + inline const PIP_Tree_Node* PIP_Decision_Node::child_node(bool v) const {

1 0

[GIT] ppl/ppl(floating_point): Removed outdated FIXME note.
by Fabio Bossi 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 688061869b0f3c16ba299fd49ccaab8fa6039c15 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=688061869b0f… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 11 17:05:06 2009 +0200 Removed outdated FIXME note. --- src/Octagonal_Shape.templates.hh | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index a36f67c..fa61f15 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4798,7 +4798,6 @@ Octagonal_Shape<T>::affine_image(Variable var, add_assign_r(m_i_cv, m_i_cv, b_mlb, ROUND_UP); } // Now update unary constraints on var. - // FIXME: are we sure that ROUND_IGNORE is good? mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE); N& m_cv_v = m_cv[n_var]; add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP);

1 0

[GIT] ppl/ppl(floating_point): Added other simple cases of affine_image.
by Fabio Bossi 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 762b048f813652e5bfb4e27032c8a4494563da95 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=762b048f8136… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 11 17:04:11 2009 +0200 Added other simple cases of affine_image. --- src/Octagonal_Shape.templates.hh | 77 ++++++++++++++++++++++++++++++------- 1 files changed, 62 insertions(+), 15 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 0d6b04a..a36f67c 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4731,26 +4731,26 @@ Octagonal_Shape<T>::affine_image(Variable var, // variable; // - If t == 2, the `lf' is of the general form. + PPL_DIRTY_TEMP(N, b_ub); + assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, b_lb); + assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, b_mlb); + neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED); + if (t == 0) { // Case 1: lf = [lb;ub]; forget_all_octagonal_constraints(var_id); - PPL_DIRTY_TEMP(N, two_mlb); - neg_assign_r(two_mlb, b.lower(), ROUND_NOT_NEEDED); - mul_2exp_assign_r(two_mlb, two_mlb, 1, ROUND_UP); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); PPL_DIRTY_TEMP(N, two_ub); - mul_2exp_assign_r(two_ub, b.upper(), 1, ROUND_UP); + mul_2exp_assign_r(two_ub, b_ub, 1, ROUND_UP); // Add the constraint `var >= lb && var <= ub'. add_octagonal_constraint(n_var+1, n_var, two_ub); - add_octagonal_constraint(n_var, n_var+1, two_mlb); + add_octagonal_constraint(n_var, n_var+1, b_mlb); PPL_ASSERT(OK()); return; } - PPL_DIRTY_TEMP(N, b_ub); - assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); - PPL_DIRTY_TEMP(N, b_lb); - assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED); - // true if b = [0;0]. bool is_b_zero = (b_lb == 0 && b_ub == 0); @@ -4776,8 +4776,6 @@ Octagonal_Shape<T>::affine_image(Variable var, else { // Translate all the constraints on `var' by adding the value // `b_ub' or subtracting the value `b_lb'. - PPL_DIRTY_TEMP(N, b_mlb); - neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED); const Row_Iterator m_begin = matrix.row_begin(); const Row_Iterator m_end = matrix.row_end(); Row_Iterator m_iter = m_begin + n_var; @@ -4807,16 +4805,65 @@ Octagonal_Shape<T>::affine_image(Variable var, mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE); N& m_v_cv = m_v[n_var+1]; add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); + reset_strongly_closed(); } - // FIXME: can't we put it above? - reset_strongly_closed(); } - // Here `w_coeff = [-1;-1]. + else { + // Here `w_coeff = [-1;-1]. + // Remove the binary constraints on `var'. + forget_binary_octagonal_constraints(var_id); + const Row_Iterator m_begin = matrix.row_begin(); + Row_Iterator m_iter = m_begin + n_var; + N& m_v_cv = (*m_iter)[n_var+1]; + ++m_iter; + N& m_cv_v = (*m_iter)[n_var]; + // Swap the unary constraints on `var'. + std::swap(m_v_cv, m_cv_v); + // Strong closure is not preserved. + reset_strongly_closed(); + if (b != 0) { + // Translate the unary constraints on `var' by adding the value + // `b_ub' or subtracting the value `b_lb'. + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE); + add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); + add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); + } + incremental_strong_closure_assign(var); + } } else { // Here `w != var', so that `lf' is of the form // [+/-1;+/-1] * w + b. + // Remove all constraints on `var'. + forget_all_octagonal_constraints(var_id); + const dimension_type n_w = 2*w_id; + if (is_w_coeff_one) + // Add the new constraints `var - w >= b_lb' + // `and var - w <= b_ub'. + if (var_id < w_id) { + add_octagonal_constraint(n_w, n_var, b_ub); + add_octagonal_constraint(n_w+1, n_var+1, b_mlb); + } + else { + add_octagonal_constraint(n_var+1, n_w+1, b_ub); + add_octagonal_constraint(n_var, n_w, b_mlb); + } + else + // Add the new constraints `var + w >= b_lb' + // `and var + w <= b_ub'. + if (var_id < w_id) { + add_octagonal_constraint(n_w+1, n_var, b_ub); + add_octagonal_constraint(n_w, n_var+1, b_mlb); + } + else { + add_octagonal_constraint(n_var+1, n_w, b_ub); + add_octagonal_constraint(n_var, n_w+1, b_mlb); + } + incremental_strong_closure_assign(var); } + PPL_ASSERT(OK()); + return; } }

1 0

[GIT] ppl/ppl(floating_point): Implemented another case for affine_image.
by Fabio Bossi 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e86a215e5bf18ca9785be5d79e199fe170bccd28 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e86a215e5bf1… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 11 14:12:30 2009 +0200 Implemented another case for affine_image. --- src/Octagonal_Shape.templates.hh | 53 ++++++++++++++++++++++++++++++------- 1 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 69f876d..0d6b04a 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4724,11 +4724,6 @@ Octagonal_Shape<T>::affine_image(Variable var, const dimension_type n_var = 2*var_id; const FP_Interval_Type& b = lf.inhomogeneous_term(); - PPL_DIRTY_TEMP(N, b_lb); - PPL_DIRTY_TEMP(N, b_ub); - assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED); - assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); - // `w' is the variable with index `w_id'. // Now we know the form of `lf': // - If t == 0, then lf == [lb;ub]; @@ -4740,11 +4735,10 @@ Octagonal_Shape<T>::affine_image(Variable var, // Case 1: lf = [lb;ub]; forget_all_octagonal_constraints(var_id); PPL_DIRTY_TEMP(N, two_mlb); + neg_assign_r(two_mlb, b.lower(), ROUND_NOT_NEEDED); + mul_2exp_assign_r(two_mlb, two_mlb, 1, ROUND_UP); PPL_DIRTY_TEMP(N, two_ub); - neg_assign_r(two_mlb, b_lb, ROUND_NOT_NEEDED); - assign_r(two_ub, b_ub, ROUND_NOT_NEEDED); - add_assign_r(two_mlb, two_mlb, two_mlb, ROUND_UP); - add_assign_r(two_ub, two_ub, two_ub, ROUND_UP); + mul_2exp_assign_r(two_ub, b.upper(), 1, ROUND_UP); // Add the constraint `var >= lb && var <= ub'. add_octagonal_constraint(n_var+1, n_var, two_ub); add_octagonal_constraint(n_var, n_var+1, two_mlb); @@ -4752,6 +4746,11 @@ Octagonal_Shape<T>::affine_image(Variable var, return; } + PPL_DIRTY_TEMP(N, b_ub); + assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, b_lb); + assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED); + // true if b = [0;0]. bool is_b_zero = (b_lb == 0 && b_ub == 0); @@ -4775,8 +4774,42 @@ Octagonal_Shape<T>::affine_image(Variable var, // 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'. + PPL_DIRTY_TEMP(N, b_mlb); + neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED); + const Row_Iterator m_begin = matrix.row_begin(); + const Row_Iterator m_end = matrix.row_end(); + Row_Iterator m_iter = m_begin + n_var; + Row_Reference m_v = *m_iter; + ++m_iter; + Row_Reference m_cv = *m_iter; + ++m_iter; + // NOTE: delay update of unary constraints on `var' + for (dimension_type j = n_var; j-- > 0; ) { + N& m_v_j = m_v[j]; + add_assign_r(m_v_j, m_v_j, b_mlb, ROUND_UP); + N& m_cv_j = m_cv[j]; + add_assign_r(m_cv_j, m_cv_j, b_ub, ROUND_UP); + } + for ( ; m_iter != m_end; ++m_iter) { + Row_Reference m_i = *m_iter; + N& m_i_v = m_i[n_var]; + add_assign_r(m_i_v, m_i_v, b_ub, ROUND_UP); + N& m_i_cv = m_i[n_var+1]; + add_assign_r(m_i_cv, m_i_cv, b_mlb, ROUND_UP); + } + // Now update unary constraints on var. + // FIXME: are we sure that ROUND_IGNORE is good? + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE); + N& m_cv_v = m_cv[n_var]; + add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE); + N& m_v_cv = m_v[n_var+1]; + add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); } + // FIXME: can't we put it above? + reset_strongly_closed(); } // Here `w_coeff = [-1;-1]. }

1 0

[GIT] ppl/ppl(pip): Added first tests in OK() methods of PIP_Tree classes.
by François Galea 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: pip Commit: 0c02e3b5a945d83ad4760bb4e014614442769464 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0c02e3b5a945… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 11 16:24:49 2009 +0200 Added first tests in OK() methods of PIP_Tree classes. --- src/PIP_Tree.cc | 80 ++++++++++++++++++++++++++++++++++++++++++++++++- src/PIP_Tree.defs.hh | 13 ++++---- 2 files changed, 84 insertions(+), 9 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 9a768c9..b7948f5 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -97,14 +97,90 @@ PIP_Decision_Node::as_decision() { } bool +PIP_Solution_Node::Tableau::OK() const { +#ifndef NDEBUG + using std::endl; + using std::cerr; +#endif + + const dimension_type num_rows = s.num_rows(); + if (num_rows != t.num_rows()) { +#ifndef NDEBUG + cerr << "The PIP_Solution_Node::Tableau matrices do not have the " + << "same number of rows." + << endl; +#endif + return false; + } + return true; +} + +bool +PIP_Tree_Node::OK() const { +#ifndef NDEBUG + using std::endl; + using std::cerr; +#endif + Constraint_System::const_iterator begin = constraints_.begin(); + Constraint_System::const_iterator end = constraints_.end(); + + // Parameter constraint system should contain no strict inequalities. + for (Constraint_System::const_iterator c = begin; c != end; c++) + if (c->is_strict_inequality()) { +#ifndef NDEBUG + cerr << "The feasible region of the PIP_Problem parameter context" + << "is defined by a constraint system containing strict " + << "inequalities." + << endl; + ascii_dump(cerr); +#endif + return false; + } + return true; +} + +bool PIP_Solution_Node::OK() const { - /* FIXME: write me! */ + /* FIXME: finish me! */ +#ifndef NDEBUG + using std::endl; + using std::cerr; +#endif + if (!PIP_Tree_Node::OK()) + return false; + + // Check that every member used is OK. + + if (!tableau.OK()) + return false; + return true; } bool PIP_Decision_Node::OK() const { - /* FIXME: write me! */ + /* FIXME: finish me! */ +#ifndef NDEBUG + using std::endl; + using std::cerr; +#endif + if (!PIP_Tree_Node::OK()) + return false; + + // Decision nodes with false child must have exactly one constraint + if (false_child) { + dimension_type + dist = std::distance(constraints_.begin(), constraints_.end()); + if (dist != 1) { +#ifndef NDEBUG + cerr << "The PIP_Decision_Node has a 'false' child but does not " + << "have exactly one parametric constraint. (" << dist << ")" + << endl; +#endif + return false; + } + } + return true; } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 5a3f476..acb8b2a 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -58,7 +58,7 @@ public: virtual ~PIP_Tree_Node(); //! Returns \c true if and only if \p *this is well formed. - virtual bool OK() const = 0; + bool OK() const; protected: //! A type alias for a sequence of constraints. @@ -69,6 +69,9 @@ protected: friend class PIP_Problem; friend class PIP_Decision_Node; + //! The local system of parameter constraints. + Constraint_System constraints_; + /*! \brief Populates the parametric simplex tableau using external data, if necessary @@ -206,6 +209,8 @@ private: Rational_Matrix s; //! The matrix of parameter coefficients. Rational_Matrix t; + //! Returns \c true if and only if \p *this is well formed. + bool OK() const; }; //! The parametric simplex tableau. @@ -249,9 +254,6 @@ private: //! A cache for computed sign values of constraint parametric RHS. std::vector<Row_Sign> sign; - //! The local system of parameter constraints. - Constraint_System constraints_; - //! Determines the sign of given Row. static Row_Sign row_sign(const Row &x); @@ -347,9 +349,6 @@ private: //! Pointer to the "false" child of \p *this. PIP_Tree_Node* false_child; - //! The local system of parameter constraints - Constraint_System constraints_; - /*! \brief Constructs if \p cs then \p tcp \p else \p fcp.

1 0

[GIT] ppl/ppl(pip): Implemented integer context compatibility check.
by François Galea 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: pip Commit: 400f860377c15c874ef1625070c2a23c8ec061e2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=400f860377c1… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 11 15:40:34 2009 +0200 Implemented integer context compatibility check. --- src/PIP_Tree.cc | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/PIP_Tree.defs.hh | 17 ++++++++++-- 2 files changed, 81 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index b552c72..9a768c9 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -241,6 +241,73 @@ PIP_Solution_Node::row_sign(const Row &x) { return sign; } +bool +PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { + Matrix s(ctx); + s.add_row(cnst); + dimension_type i, j, k, j_; + dimension_type num_rows = s.num_rows(); + dimension_type num_cols = s.num_columns(); + bool result = false; + + /* Perform nonparametric simplex pivots until we find an empty solution + * or an optimum */ + for(;;) { + // Look for a negative RHS (=constant term, stored in matrix column 0) + i = 0; + while (i<num_rows && s[i][0] >= 0) + i++; + if (i == num_rows) { + // No negative RHS: optimum found + result = true; + break; + } + // Find a positive m[i][j] pivot + j = 1; + Row &p = s[i]; + while (j<num_cols && p[j] <= 0) + j++; + if (j == num_cols) { + // No positive pivot candidate: empty problem + result = false; + break; + } + // Perform a pivot operation on the matrix + Coefficient sij = p[j]; + for (j_=0; j_<num_cols; ++j_) { + if (j_ == j) + continue; + Coefficient sij_ = p[j_]; + for (k=0; k<num_rows; ++k) { + Coefficient mult = s[k][j] * sij_; + if (mult % sij != 0) { + // Must scale row to stay in integer case + Coefficient gcd; + gcd_assign(gcd, mult, sij); + Coefficient scale_factor = sij/gcd; + add_assign(s[k], s[k], scale_factor); + mult *= scale_factor; + } + s[k][j_] -= mult / sij; + } + } + for (k=0; k<num_rows; ++k) { + Coefficient skj = s[k][j]; + if (skj % sij != 0) { + // as above, we must perform row scaling + Coefficient gcd; + gcd_assign(gcd, skj, sij); + Coefficient scale_factor = sij/gcd; + add_assign(s[k], s[k], scale_factor); + skj *= scale_factor; + } + s[k][j_] = skj/sij; + } + } + + return result; +} + void PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, dimension_type external_space_dim, diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index e0ce99c..5a3f476 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -246,15 +246,26 @@ private: MIXED }; - //! A cache for computed sign values of constraint parametric RHS + //! A cache for computed sign values of constraint parametric RHS. std::vector<Row_Sign> sign; - //! The local system of parameter constraints + //! The local system of parameter constraints. Constraint_System constraints_; - //! Determines the sign of given Row + //! Determines the sign of given Row. static Row_Sign row_sign(const Row &x); + /*! \brief + Checks whether a constraint is compatible with a context, ie. does not + make the context empty. + + The algorithm consists in performing simplex pivots on a Matrix consisting + in the original matrix with the constraint inserted. If the simplex + terminates with a solution, then the restrained context is not empty. + Otherwise, it is. + */ + static bool compatibility_check(const Matrix &ctx, const Row &cnst); + protected: /*! \brief Populates the parametric simplex tableau using external data, if necessary

1 0

[GIT] ppl/ppl(pip): Implemented row sign detection.
by François Galea 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: pip Commit: 9ce39ca898aa35e1639b768a5d7c92e987a9d3d2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9ce39ca898aa… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 11 13:16:08 2009 +0200 Implemented row sign detection. --- src/PIP_Tree.cc | 33 +++++++++++++++++++++++++++++++++ src/PIP_Tree.defs.hh | 20 ++++++++++++++++++++ 2 files changed, 53 insertions(+), 0 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 2f1afe0..b552c72 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -209,6 +209,38 @@ PIP_Solution_Node::ascii_load(std::istream& s) { return true; } +PIP_Solution_Node::Row_Sign +PIP_Solution_Node::row_sign(const Row &x) { + PIP_Solution_Node::Row_Sign sign = ZERO; + Coefficient c; + for (int i = x.size(); i-- > 0; ) { + c = x[i]; + switch (sign) { + case UNKNOWN: + // cannot happen + break; + case ZERO: + if (c < 0) + sign = NEGATIVE; + else if (c > 0) + sign = POSITIVE; + break; + case NEGATIVE: + if (c > 0) + return MIXED; + break; + case POSITIVE: + if (c < 0) + return MIXED; + break; + case MIXED: + // cannot happen + break; + } + } + return sign; +} + void PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, dimension_type external_space_dim, @@ -273,6 +305,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, // FIXME: must handle equality constraints tableau.s.add_row(var); tableau.t.add_row(param); + sign.push_back(row_sign(param)); } // FIXME: decide emptiness detection (and node removal) } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 13dc12b..e0ce99c 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -232,9 +232,29 @@ private: */ std::vector<dimension_type> mapping; + //! The possible values for the sign of a parametric linear expression. + enum Row_Sign { + //! Not computed yet (default) + UNKNOWN, + //! All row coefficients are zero. + ZERO, + //! All nonzero row coefficients are positive. + POSITIVE, + //! All nonzero row coefficients are negative. + NEGATIVE, + //! The row contains positive and negative coefficients. + MIXED + }; + + //! A cache for computed sign values of constraint parametric RHS + std::vector<Row_Sign> sign; + //! The local system of parameter constraints Constraint_System constraints_; + //! Determines the sign of given Row + static Row_Sign row_sign(const Row &x); + protected: /*! \brief Populates the parametric simplex tableau using external data, if necessary

1 0

[GIT] ppl/ppl(pip): Implemented constraint negation, plus minor fixes.
by François Galea 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: pip Commit: 33905b7bf1a3383376e5186937f7505308a5c2c9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=33905b7bf1a3… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 11 13:08:53 2009 +0200 Implemented constraint negation, plus minor fixes. --- src/PIP_Tree.cc | 22 ++++++++++------------ src/PIP_Tree.defs.hh | 2 +- src/PIP_Tree.inlines.hh | 5 +++++ 3 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 041184e..2f1afe0 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -37,7 +37,7 @@ add_assign(Row& x, const Row& y, Coefficient_traits::const_reference c) { add_mul_assign(x[i], c, y[i]); } -// Merge constraint systems such as x = x U z +// Merge constraint systems such as x = x U y void merge_assign(Constraint_System& x, const Constraint_System& y) { for (Constraint_System::const_iterator y_i = y.begin(), @@ -140,8 +140,12 @@ PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); Constraint_System context_false(context); - //FIXME: not implemented yet (constraint negation) - //context_false.insert(!constraints_[0]); + Constraint_System::const_iterator ci = constraints_.begin(); + PPL_ASSERT(ci->is_nonstrict_inequality()); + Linear_Expression expr = Linear_Expression(*ci); + expr += 1; + Constraint c(expr <= 0); + context_false.insert(c); stf = false_child->solve(&false_child, context_false); } @@ -149,9 +153,9 @@ PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, return_status = UNFEASIBLE_PIP_PROBLEM; *parent_ref = 0; delete this; - return UNFEASIBLE_PIP_PROBLEM; - } - return OPTIMIZED_PIP_PROBLEM; + } else + return_status = OPTIMIZED_PIP_PROBLEM; + return return_status; } void @@ -159,12 +163,6 @@ PIP_Solution_Node::Rational_Matrix::normalize() { //FIXME } -//! Returns the allocated capacity of each Row of the Matrix. -dimension_type -PIP_Solution_Node::Rational_Matrix::capacity() { - return row_capacity; -} - void PIP_Solution_Node::Rational_Matrix::ascii_dump(std::ostream& s) const { s << "denominator " << denominator << "\n"; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index c3c1b4b..13dc12b 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -185,7 +185,7 @@ private: void normalize(); //! Returns the allocated capacity of each Row of the Matrix. - dimension_type capacity(); + dimension_type capacity() const; //! Tests whether the matrix is integer, \e ie. the denominator is 1. bool is_integer() const; diff --git a/src/PIP_Tree.inlines.hh b/src/PIP_Tree.inlines.hh index 87f2a22..c3b23bc 100644 --- a/src/PIP_Tree.inlines.hh +++ b/src/PIP_Tree.inlines.hh @@ -55,6 +55,11 @@ PIP_Solution_Node::Rational_Matrix::get_denominator() const { return denominator; } +inline dimension_type +PIP_Solution_Node::Rational_Matrix::capacity() const { + return row_capacity; +} + inline PIP_Tree_Node::~PIP_Tree_Node() { }

1 0

[GIT] ppl/ppl(floating_point): Added a skeleton for the rest of the affine_image implementation.
by Fabio Bossi 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1bd882f4961087d6686bda5676bd1ba5908dd681 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1bd882f49610… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 11 10:50:42 2009 +0200 Added a skeleton for the rest of the affine_image implementation. --- src/Octagonal_Shape.templates.hh | 36 +++++++++++++++++++++++++++++++++++- 1 files changed, 35 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index b891006..69f876d 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4752,12 +4752,46 @@ Octagonal_Shape<T>::affine_image(Variable var, return; } + // true if b = [0;0]. bool is_b_zero = (b_lb == 0 && b_ub == 0); if (t == 1) { - + // The one and only non-zero homogeneous coefficient in `lf'. + const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id)); + PPL_DIRTY_TEMP(N, w_coeff_lb); + PPL_DIRTY_TEMP(N, w_coeff_ub); + assign_r(w_coeff_lb, w_coeff.lower(), ROUND_NOT_NEEDED); + assign_r(w_coeff_ub, w_coeff.upper(), ROUND_NOT_NEEDED); + // true if w_coeff = [1;1]. + bool is_w_coeff_one = (w_coeff_lb == 1 && w_coeff_ub == 1); + // true if w_coeff = [-1;-1]. + bool is_w_coeff_minus_one = (w_coeff_lb == -1 && w_coeff_ub == -1); + if (is_w_coeff_one || is_w_coeff_minus_one) { + // Case 2: lf = w_coeff*w + b, with w_coeff = [+/-1;+/-1]. + 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]. + } + else { + // Here `w != var', so that `lf' is of the form + // [+/-1;+/-1] * w + b. + } + } } + // General case. + // Either t == 2, so that + // expr == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, + // or t == 1, expr == i*w + b, but i <> [+/-1;+/-1]. + // FIXME: complete the implementation. }

1 0