March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(termination): Corrected an invalid reference bug in PIP_Solution_Node::update_tableau().
by Enea Zaffanella 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: d054a83797b9b861addd7cdc5abac091edaf5865 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d054a83797b9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Mar 7 11:36:11 2010 +0100 Corrected an invalid reference bug in PIP_Solution_Node::update_tableau(). The addition of tableau rows invalidates previously computed references. Thanks to Marco Poletti for reporting this. --- src/PIP_Tree.cc | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index d970067..79d254e 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1644,8 +1644,10 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& pip, // This might be faster however. tableau.s.add_zero_rows(1, Row::Flags()); tableau.t.add_zero_rows(1, Row::Flags()); - neg_assign_row(tableau.s[1 + row_id], v_row); - neg_assign_row(tableau.t[1 + row_id], p_row); + // NOTE: addition of rows invalidates references v_row and p_row + // due to possible matrix reallocations: recompute them. + neg_assign_row(tableau.s[1 + row_id], tableau.s[row_id]); + neg_assign_row(tableau.t[1 + row_id], tableau.t[row_id]); sign.push_back(row_sign(tableau.t[1 + row_id], big_dimension)); special_equality_row = mapping.size(); basis.push_back(false);

1 0

[GIT] ppl/ppl(termination): Eventually perform solution tree simplifications after incremental addition of parameter constraints .
by François Galea 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 2fad4a9428627c5d0ca8142567ac754ceab0e855 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fad4a942862… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 21:13:37 2010 +0100 Eventually perform solution tree simplifications after incremental addition of parameter constraints. --- src/PIP_Tree.cc | 65 +++++++++++++++++++++++++++++++++++++++++++++++-- src/PIP_Tree.defs.hh | 3 ++ 2 files changed, 65 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index a5a7915..d970067 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -557,6 +557,18 @@ PIP_Tree_Node constraints_.insert(expr >= 0); } +void +PIP_Tree_Node::parent_merge() { + const PIP_Decision_Node& parent = *parent_; + + // Merge the parent's artificial parameters. + artificial_parameters.insert(artificial_parameters.begin(), + parent.art_parameter_begin(), + parent.art_parameter_end()); + + PPL_ASSERT(OK()); +} + bool PIP_Solution_Node::OK() const { #ifndef NDEBUG @@ -689,10 +701,12 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, add_artificial_parameters(context_true, all_params, space_dim, num_art_params); merge_assign(context_true, constraints_, all_params); + bool has_false_child = (false_child != 0); + bool has_true_child = (true_child != 0); true_child = true_child->solve(pip, check_feasible_context, context_true, all_params, space_dim); - if (false_child) { + if (has_false_child) { // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); // NOTE: modify context_true in place, complementing its last constraint. @@ -704,8 +718,53 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, } if (true_child != 0 || false_child != 0) { - PPL_ASSERT(OK()); - return this; + PIP_Tree_Node* node = this; + if (has_false_child && false_child == 0) { + // False child has become unfeasible: merge this node's artificials with + // the true child, while removing the local parameter constraints, which + // are no longer discriminative. + true_child->parent_merge(); + true_child->set_parent(parent()); + node = true_child; + true_child = 0; + delete this; + } + else if (has_true_child && true_child == 0) { + // True child has become unfeasible: merge this node's artificials + // with the false child. + false_child->parent_merge(); + false_child->set_parent(parent()); + node = false_child; + false_child = 0; + delete this; + } + else if (check_feasible_context) { + // Test all constraints for redundancy with the context, and eliminate + // them if not necessary. + Constraint_System cs; + cs.swap(constraints_); + const Constraint_System::const_iterator end = cs.end(); + for (Constraint_System::const_iterator ci = cs.begin(); ci != end; ++ci) { + Matrix ctx_copy(context); + merge_assign(ctx_copy, Constraint_System(*ci), all_params); + Row& last = ctx_copy[ctx_copy.num_rows()-1]; + complement_assign(last, last, 1); + if (compatibility_check(ctx_copy)) { + // The constraint is not redundant with the context: we must keep it. + constraints_.insert(*ci); + } + } + // If the constraints set has become empty, only keep the true child. + if (constraints_.empty()) { + true_child->parent_merge(); + true_child->set_parent(parent()); + node = true_child; + true_child = 0; + delete this; + } + } + PPL_ASSERT(node->OK()); + return node; } else { delete this; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index ada4280..2d94c5f 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -212,6 +212,9 @@ protected: //! Inserts a new parametric constraint in internal Row format void add_constraint(const Row& x, const Variables_Set& parameters); + //! Merges parent's artificial parameters into \p *this. + void parent_merge(); + //! Prints on \p s the tree rooted in \p *this. /*! \param s

1 0

[GIT] ppl/ppl(termination): Moved the compatibility_check static methods to PIP_Tree_Node.
by François Galea 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: f010ef5edd820af3fb4589c75c8c9be73b2930ac URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f010ef5edd82… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:27:09 2010 +0100 Moved the compatibility_check static methods to PIP_Tree_Node. --- src/PIP_Tree.cc | 4 ++-- src/PIP_Tree.defs.hh | 34 ++++++++++++++++------------------ 2 files changed, 18 insertions(+), 20 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 45427ae..a5a7915 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1230,7 +1230,7 @@ PIP_Solution_Node::row_sign(const Row& x, } bool -PIP_Solution_Node::compatibility_check(const Matrix& context, const Row& row) { +PIP_Tree_Node::compatibility_check(const Matrix& context, const Row& row) { // CHECKME: do `context' and `row' have compatible (row) capacity? Matrix s(context); s.add_row(row); @@ -1238,7 +1238,7 @@ PIP_Solution_Node::compatibility_check(const Matrix& context, const Row& row) { } bool -PIP_Solution_Node::compatibility_check(Matrix& s) { +PIP_Tree_Node::compatibility_check(Matrix& s) { PPL_ASSERT(s.OK()); // Note: num_rows may increase. dimension_type num_rows = s.num_rows(); diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index ef6e23a..ada4280 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -238,6 +238,22 @@ protected: static void indent_and_print(std::ostream& s, unsigned indent, const char* str); + /*! \brief + Checks whether a context matrix is satisfiable. + + The satisfiability check is implemented by the revised dual simplex + algorithm on the context matrix. The algorithm ensures the feasible + solution is integer by applying a cut generation method when + intermediate non-integer solutions are found. + */ + static bool compatibility_check(Matrix& s); + + /*! \brief + Helper method: checks for satisfiability of the restricted context + obtained by adding \p row to \p context. + */ + static bool compatibility_check(const Matrix& context, const Row& row); + }; // class PIP_Tree_Node @@ -571,22 +587,6 @@ private: //! Returns the sign of row \p x. static Row_Sign row_sign(const Row& x, dimension_type big_dimension); - /*! \brief - Checks whether a context matrix is satisfiable. - - The satisfiability check is implemented by the revised dual simplex - algorithm on the context matrix. The algorithm ensures the feasible - solution is integer by applying a cut generation method when - intermediate non-integer solutions are found. - */ - static bool compatibility_check(Matrix& s); - - /*! \brief - Helper method: checks for satisfiability of the restricted context - obtained by adding \p row to \p context. - */ - static bool compatibility_check(const Matrix& context, const Row& row); - protected: //! Copy constructor. PIP_Solution_Node(const PIP_Solution_Node& y); @@ -603,8 +603,6 @@ protected: // PIP_Problem::ascii load() method needs access set_owner(). friend bool PIP_Problem::ascii_load(std::istream& s); - // PIP_Problem::solve() method needs access compatibility_check(). - friend PIP_Problem_Status PIP_Problem::solve() const; //! Sets the pointer to the PIP_Problem owning object. virtual void set_owner(const PIP_Problem* owner);

1 0

[GIT] ppl/ppl(termination): Added one more test for incremental solving.
by François Galea 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: a7af846ade60e2c4e9bdd7595b80abd5776d4704 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7af846ade60… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:25:00 2010 +0100 Added one more test for incremental solving. --- tests/PIP_Problem/pipproblem1.cc | 37 +++++++++++++++++++++++++++++++++++++ 1 files changed, 37 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 4c7568b..e361a7b 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -666,6 +666,42 @@ test22() { return ok; } +bool +test23() { + // Same problem as test02, but incrementally adding a parameter constraint + // removing one level in the decision tree. + Variable i(0); + Variable j(1); + Variable n(2); + Variable m(3); + Variables_Set params(n, m); + + Constraint_System cs; + cs.insert(3*j >= -2*i+8); + cs.insert(j <= 4*i - 4); + cs.insert(j <= m); + cs.insert(i <= n); + + 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(); + ok &= solution->OK(); + pip.print_solution(nout); + } + + pip.add_constraint(7*n >= 10); + ok &= (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + ok &= solution->OK(); + pip.print_solution(nout); + } + + return ok; +} + } // namespace BEGIN_MAIN @@ -691,4 +727,5 @@ BEGIN_MAIN DO_TEST_F8(test20); DO_TEST_F8(test21); DO_TEST_F8(test22); + DO_TEST_F8(test23); END_MAIN

1 0

[GIT] ppl/ppl(termination): Documentation improved.
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 4684207ce34a88f9552f450faa6e019e475e4027 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4684207ce34a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 13:35:33 2010 +0400 Documentation improved. --- src/termination.defs.hh | 17 ++++++++++------- 1 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/termination.defs.hh b/src/termination.defs.hh index cab4eec..59b0028 100644 --- a/src/termination.defs.hh +++ b/src/termination.defs.hh @@ -29,11 +29,12 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { /*! \brief - Termination test using an improvement of the method by Serebrenik - and Mesnard. + Termination test using an improvement of the method by Mesnard and + Serebrenik. \tparam PSET - Any pointset supported by the PPL. + Any pointset supported by the PPL that provides the + <CODE>minimized_constraints()</CODE> method. \param pset A pointset approximating the behavior of a loop whose termination @@ -62,10 +63,11 @@ termination_test_MS(const PSET& pset); /*! \brief Termination test with witness ranking function using an improvement - of the method by Serebrenik and Mesnard. + of the method by Mesnard and Serebrenik. \tparam PSET - Any pointset supported by the PPL. + Any pointset supported by the PPL that provides the + <CODE>minimized_constraints()</CODE> method. \param pset A pointset approximating the behavior of a loop whose termination @@ -103,10 +105,11 @@ one_affine_ranking_function_MS(const PSET& pset, Generator& mu); /*! \brief Termination test with ranking function space using an improvement - of the method by Serebrenik and Mesnard. + of the method by Mesnard and Serebrenik. \tparam PSET - Any pointset supported by the PPL. + Any pointset supported by the PPL that provides the + <CODE>minimized_constraints()</CODE> method. \param pset A pointset approximating the behavior of a loop whose termination

1 0

[GIT] ppl/ppl(master): Corrected an invalid reference bug in PIP_Solution_Node::update_tableau().
by Enea Zaffanella 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: master Commit: d054a83797b9b861addd7cdc5abac091edaf5865 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d054a83797b9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Mar 7 11:36:11 2010 +0100 Corrected an invalid reference bug in PIP_Solution_Node::update_tableau(). The addition of tableau rows invalidates previously computed references. Thanks to Marco Poletti for reporting this. --- src/PIP_Tree.cc | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index d970067..79d254e 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1644,8 +1644,10 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& pip, // This might be faster however. tableau.s.add_zero_rows(1, Row::Flags()); tableau.t.add_zero_rows(1, Row::Flags()); - neg_assign_row(tableau.s[1 + row_id], v_row); - neg_assign_row(tableau.t[1 + row_id], p_row); + // NOTE: addition of rows invalidates references v_row and p_row + // due to possible matrix reallocations: recompute them. + neg_assign_row(tableau.s[1 + row_id], tableau.s[row_id]); + neg_assign_row(tableau.t[1 + row_id], tableau.t[row_id]); sign.push_back(row_sign(tableau.t[1 + row_id], big_dimension)); special_equality_row = mapping.size(); basis.push_back(false);

1 0

[GIT] ppl/ppl(master): Eventually perform solution tree simplifications after incremental addition of parameter constraints .
by François Galea 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: master Commit: 2fad4a9428627c5d0ca8142567ac754ceab0e855 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fad4a942862… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 21:13:37 2010 +0100 Eventually perform solution tree simplifications after incremental addition of parameter constraints. --- src/PIP_Tree.cc | 65 +++++++++++++++++++++++++++++++++++++++++++++++-- src/PIP_Tree.defs.hh | 3 ++ 2 files changed, 65 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index a5a7915..d970067 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -557,6 +557,18 @@ PIP_Tree_Node constraints_.insert(expr >= 0); } +void +PIP_Tree_Node::parent_merge() { + const PIP_Decision_Node& parent = *parent_; + + // Merge the parent's artificial parameters. + artificial_parameters.insert(artificial_parameters.begin(), + parent.art_parameter_begin(), + parent.art_parameter_end()); + + PPL_ASSERT(OK()); +} + bool PIP_Solution_Node::OK() const { #ifndef NDEBUG @@ -689,10 +701,12 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, add_artificial_parameters(context_true, all_params, space_dim, num_art_params); merge_assign(context_true, constraints_, all_params); + bool has_false_child = (false_child != 0); + bool has_true_child = (true_child != 0); true_child = true_child->solve(pip, check_feasible_context, context_true, all_params, space_dim); - if (false_child) { + if (has_false_child) { // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); // NOTE: modify context_true in place, complementing its last constraint. @@ -704,8 +718,53 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, } if (true_child != 0 || false_child != 0) { - PPL_ASSERT(OK()); - return this; + PIP_Tree_Node* node = this; + if (has_false_child && false_child == 0) { + // False child has become unfeasible: merge this node's artificials with + // the true child, while removing the local parameter constraints, which + // are no longer discriminative. + true_child->parent_merge(); + true_child->set_parent(parent()); + node = true_child; + true_child = 0; + delete this; + } + else if (has_true_child && true_child == 0) { + // True child has become unfeasible: merge this node's artificials + // with the false child. + false_child->parent_merge(); + false_child->set_parent(parent()); + node = false_child; + false_child = 0; + delete this; + } + else if (check_feasible_context) { + // Test all constraints for redundancy with the context, and eliminate + // them if not necessary. + Constraint_System cs; + cs.swap(constraints_); + const Constraint_System::const_iterator end = cs.end(); + for (Constraint_System::const_iterator ci = cs.begin(); ci != end; ++ci) { + Matrix ctx_copy(context); + merge_assign(ctx_copy, Constraint_System(*ci), all_params); + Row& last = ctx_copy[ctx_copy.num_rows()-1]; + complement_assign(last, last, 1); + if (compatibility_check(ctx_copy)) { + // The constraint is not redundant with the context: we must keep it. + constraints_.insert(*ci); + } + } + // If the constraints set has become empty, only keep the true child. + if (constraints_.empty()) { + true_child->parent_merge(); + true_child->set_parent(parent()); + node = true_child; + true_child = 0; + delete this; + } + } + PPL_ASSERT(node->OK()); + return node; } else { delete this; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index ada4280..2d94c5f 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -212,6 +212,9 @@ protected: //! Inserts a new parametric constraint in internal Row format void add_constraint(const Row& x, const Variables_Set& parameters); + //! Merges parent's artificial parameters into \p *this. + void parent_merge(); + //! Prints on \p s the tree rooted in \p *this. /*! \param s

1 0

[GIT] ppl/ppl(master): Moved the compatibility_check static methods to PIP_Tree_Node.
by François Galea 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: master Commit: f010ef5edd820af3fb4589c75c8c9be73b2930ac URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f010ef5edd82… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:27:09 2010 +0100 Moved the compatibility_check static methods to PIP_Tree_Node. --- src/PIP_Tree.cc | 4 ++-- src/PIP_Tree.defs.hh | 34 ++++++++++++++++------------------ 2 files changed, 18 insertions(+), 20 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 45427ae..a5a7915 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1230,7 +1230,7 @@ PIP_Solution_Node::row_sign(const Row& x, } bool -PIP_Solution_Node::compatibility_check(const Matrix& context, const Row& row) { +PIP_Tree_Node::compatibility_check(const Matrix& context, const Row& row) { // CHECKME: do `context' and `row' have compatible (row) capacity? Matrix s(context); s.add_row(row); @@ -1238,7 +1238,7 @@ PIP_Solution_Node::compatibility_check(const Matrix& context, const Row& row) { } bool -PIP_Solution_Node::compatibility_check(Matrix& s) { +PIP_Tree_Node::compatibility_check(Matrix& s) { PPL_ASSERT(s.OK()); // Note: num_rows may increase. dimension_type num_rows = s.num_rows(); diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index ef6e23a..ada4280 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -238,6 +238,22 @@ protected: static void indent_and_print(std::ostream& s, unsigned indent, const char* str); + /*! \brief + Checks whether a context matrix is satisfiable. + + The satisfiability check is implemented by the revised dual simplex + algorithm on the context matrix. The algorithm ensures the feasible + solution is integer by applying a cut generation method when + intermediate non-integer solutions are found. + */ + static bool compatibility_check(Matrix& s); + + /*! \brief + Helper method: checks for satisfiability of the restricted context + obtained by adding \p row to \p context. + */ + static bool compatibility_check(const Matrix& context, const Row& row); + }; // class PIP_Tree_Node @@ -571,22 +587,6 @@ private: //! Returns the sign of row \p x. static Row_Sign row_sign(const Row& x, dimension_type big_dimension); - /*! \brief - Checks whether a context matrix is satisfiable. - - The satisfiability check is implemented by the revised dual simplex - algorithm on the context matrix. The algorithm ensures the feasible - solution is integer by applying a cut generation method when - intermediate non-integer solutions are found. - */ - static bool compatibility_check(Matrix& s); - - /*! \brief - Helper method: checks for satisfiability of the restricted context - obtained by adding \p row to \p context. - */ - static bool compatibility_check(const Matrix& context, const Row& row); - protected: //! Copy constructor. PIP_Solution_Node(const PIP_Solution_Node& y); @@ -603,8 +603,6 @@ protected: // PIP_Problem::ascii load() method needs access set_owner(). friend bool PIP_Problem::ascii_load(std::istream& s); - // PIP_Problem::solve() method needs access compatibility_check(). - friend PIP_Problem_Status PIP_Problem::solve() const; //! Sets the pointer to the PIP_Problem owning object. virtual void set_owner(const PIP_Problem* owner);

1 0

[GIT] ppl/ppl(master): Added one more test for incremental solving.
by François Galea 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: master Commit: a7af846ade60e2c4e9bdd7595b80abd5776d4704 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7af846ade60… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:25:00 2010 +0100 Added one more test for incremental solving. --- tests/PIP_Problem/pipproblem1.cc | 37 +++++++++++++++++++++++++++++++++++++ 1 files changed, 37 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 4c7568b..e361a7b 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -666,6 +666,42 @@ test22() { return ok; } +bool +test23() { + // Same problem as test02, but incrementally adding a parameter constraint + // removing one level in the decision tree. + Variable i(0); + Variable j(1); + Variable n(2); + Variable m(3); + Variables_Set params(n, m); + + Constraint_System cs; + cs.insert(3*j >= -2*i+8); + cs.insert(j <= 4*i - 4); + cs.insert(j <= m); + cs.insert(i <= n); + + 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(); + ok &= solution->OK(); + pip.print_solution(nout); + } + + pip.add_constraint(7*n >= 10); + ok &= (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + ok &= solution->OK(); + pip.print_solution(nout); + } + + return ok; +} + } // namespace BEGIN_MAIN @@ -691,4 +727,5 @@ BEGIN_MAIN DO_TEST_F8(test20); DO_TEST_F8(test21); DO_TEST_F8(test22); + DO_TEST_F8(test23); END_MAIN

1 0

[GIT] ppl/ppl(termination): Still working on specifications.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: 37d7226faeb9e32cd096748616b822fbc39c00e3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=37d7226faeb9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 22:09:59 2010 +0400 Still working on specifications. --- src/termination.cc | 17 +++++++++++------ 1 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 47314e7..d0d1909 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -81,7 +81,7 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph, The allocation of variable indices in the output constraint systems \p cs_out1 and \p cs_out2 is as follows: - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu 0\f$ goes onto \f$ n \f$; + - \f$ \mu_0\f$ goes onto \f$ n \f$; - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; if we use the same constraint system, that is @@ -170,7 +170,7 @@ fill_constraint_systems_MS(const Constraint_System& cs, The output constraint system, where variables indices are allocated as follows: - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu 0\f$ goes onto \f$ n \f$; + - \f$ \mu_0\f$ goes onto \f$ n \f$; - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto \f$ n+m+1, ..., n+2*m+2 \f$. @@ -211,8 +211,6 @@ fill_constraint_systems_MS(const Constraint_System& cs, The space of ranking functions is then spanned by \f$ \vect{v}_3^\transpose A_C' \vect x \f$. - The ranking functions are expressed by L2 * A' * x, - In contrast, our encoding is of the form \f[ \begin{pmatrix} @@ -241,7 +239,7 @@ fill_constraint_systems_MS(const Constraint_System& cs, \vect{u}_2^\transpose E_B + \vect{u}_3^\transpose (E_C+E_C') &= \vect{0}^\transpose, \\ - \vect{u}_2 \vect{b}_B + \vect{u}_3 \vect{b}_C + \vect{u}_2 \vect{d}_B + \vect{u}_3 \vect{d}_C &> 0, \end{aligned} \f] @@ -249,6 +247,12 @@ fill_constraint_systems_MS(const Constraint_System& cs, are constrained to be nonpositive. The space of ranking functions is then spanned by \f$ \vect{u}_3^\transpose E_C' \vect x \f$. + + The allocation of variable indices in the output constraint + system \p cs_out is as follows: + - \f$ u_3 \f$ goes onto \f$ 0, \ldots, s-1 \f$; + - \f$ u_2 \f$ goes onto \f$ s, \ldots, s+r-1 \f$; + - \f$ u_1 \f$ goes onto \f$ s+r, \ldots, s+2r-1 \f$. */ void fill_constraint_systems_PR(const Constraint_System& cs, @@ -256,7 +260,7 @@ fill_constraint_systems_PR(const Constraint_System& cs, const dimension_type m, Constraint_System& cs_out) { // Determine the partitioning of the m rows into the r rows - // of E_B and the s rows of E_C|E'_C. + // of E_B and the s rows of E'_C|E_C. std::deque<bool> in_A_B(m, true); dimension_type r = m; for (Constraint_System::const_iterator i = cs.begin(), @@ -270,6 +274,7 @@ fill_constraint_systems_PR(const Constraint_System& cs, } } dimension_type s = m - r; + }

1 0