February 2011 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(ppl-0_11-branch): Fixed a bug in the simplification of the solution tree.
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 3992ea8c7b4688f53fd7c7b60a8bcc6a6bf97bf0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3992ea8c7b46… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 10:49:35 2011 +0100 Fixed a bug in the simplification of the solution tree. We were too eager in merging a single true child with its parent: if the true child happened to be a decision node with both childs, the merging was causing the violation of a PIP_Decision_Node invariant. --- src/PIP_Tree.cc | 53 ++++++++++++++++++++++++++++++++++++++++++++--------- 1 files changed, 44 insertions(+), 9 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 28cc5f8..c06545c 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2224,15 +2224,50 @@ PIP_Solution_Node::solve(const PIP_Problem& pip, } } else if (f_node == 0) { - // t_node feasible, f_node unfeasible: - // restore cs and aps into t_node. - t_node->constraints_.swap(cs); - t_node->artificial_parameters.swap(aps); - // Add t_test to t_nodes's constraints. - t_node->add_constraint(t_test, all_params); - // It is now safe to release previously wrapped t_node pointer - // and return it to caller. - return wrapped_node.release(); + // t_node feasible, f_node unfeasible. + // NOTE: in principle, we could merge t_node into its parent. + // However, if t_node is a decision node having both childs, + // then we would obtain a node violating the PIP_Decision_Node + // invariant saying that t_node should have a single constraint: + // it will have, at least, the two splitting constraints. + PIP_Decision_Node* dn = dynamic_cast<PIP_Decision_Node*>(t_node); + if (dn != 0 && dn->false_child != 0) { + // Do NOT merge: create a new decision node. + PIP_Tree_Node* parent + = new PIP_Decision_Node(t_node->get_owner(), 0, t_node); + // Previously wrapped 't_node' is now safe: release it + // and protect new 'parent' node from exception safety issues. + wrapped_node.release(); + wrapped_node.reset(parent); + // Restore into parent `cs' and `aps'. + parent->constraints_.swap(cs); + parent->artificial_parameters.swap(aps); + // Add t_test to parent's constraints. + parent->add_constraint(t_test, all_params); + // It is now safe to release previously wrapped parent pointer + // and return it to caller. + return wrapped_node.release(); + } + else { + // Merge t_node with its parent: + // a) append into `cs' the constraints of t_node; + for (Constraint_System::const_iterator + i = t_node->constraints_.begin(), + i_end = t_node->constraints_.end(); i != i_end; ++i) + cs.insert(*i); + // b) append into `aps' the parameters of t_node; + aps.insert(aps.end(), + t_node->artificial_parameters.begin(), + t_node->artificial_parameters.end()); + // c) swap the updated `cs' and `aps' into t_node. + cs.swap(t_node->constraints_); + aps.swap(t_node->artificial_parameters); + // d) add t_test to t_nodes's constraints. + t_node->add_constraint(t_test, all_params); + // It is now safe to release previously wrapped t_node pointer + // and return it to caller. + return wrapped_node.release(); + } } // Here both t_node and f_node are feasible:

1 0

[GIT] ppl/ppl(master): New commits
by Roberto Bagnara 11 Feb '11

11 Feb '11

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e42f8b60421c… Merge: 9d99c21af3e717056a34d4f67739afb375cabe94 22b1565be0efe35f86e6323180ff6de113b19b18 Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 10:17:30 2011 +0100 Merge branch 'master' into pip URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9d99c21af3e7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 08:50:37 2011 +0100 Minor readability improvements to PIP_Decision_Node::solve(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a5d400f674a9… Merge: 29201d2a5893bbe17744777de36e9a106ed8ea95 d0f6bd037c90676130e9547e5ed909cf6ba8eee9 Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 18:50:11 2011 +0100 Merge branch 'master' into pip URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=29201d2a5893… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 18:48:11 2011 +0100 For readability, separate the input operation from input stream status check. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bb08fb49f561… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 18:46:41 2011 +0100 Corrected expected results. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b86cb60dbf77… Merge: 3c8f16e240439811d501629660cedb8f99f0009a c23ded5ce0023a753fdd5da2dbbd99d1a084566c Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 10:49:20 2011 +0100 Merge branch 'master' into pip URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3c8f16e24043… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 10:47:59 2011 +0100 Corrected the expected result for test02 to match integral simplifications. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e4098c48d6f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Feb 10 10:46:03 2011 +0100 Exploit variable integrality when creating tautology constraints. Factored out helper function void integral_simplification(Row&); used when generating tautology and sign splitting constraints. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=caaa126b56cc… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 17:22:07 2011 +0100 Fixed a bug in the simplification of the solution tree. We were too eager in merging a single true child with its parent: if the true child happened to be a decision node with both childs, the merging was causing the violation of a PIP_Decision_Node invariant. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=20f99dbe73d5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 15:42:15 2011 +0100 Further improvement to debug output. Preprocessor flag NOISY_PIP_TREE_STRUCTURE only activate those debug print taht is useful to hightlight the solution tree construction process. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d6c61aaed265… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 14:21:07 2011 +0100 A minor improvement to the debug printing mechanism. Methods solve() and generate_cut() are now provided with additional argument indent_level, telling the amount of indentation for debug prints. Added several messages to debug prints so as to clarify the solution tree construction process. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=03f79f0649bf… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 11:22:41 2011 +0100 Exploit integrality when adding constraints for mixed parameter sign rows. Try to distinguish between NOISY and VERY_NOISY debugging output. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=35d2df08098d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 09:52:58 2011 +0100 Fully normalize artificial parameters on construction. When in noisy mode, print normalized parameters. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f551cfb8700… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 4 08:39:12 2011 +0100 Minor changes related to coding standards. Prefer initial capitalization for (user-defined) type names. Prefer function objects to function pointers. Avoid nesting an anonymous namespace into another anonymous namespace.

1 0

[GIT] ppl/ppl(pip): Merge branch 'master' into pip
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: pip Commit: e42f8b60421ca299d9a25d1d96f741a3a537e482 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e42f8b60421c… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 10:17:30 2011 +0100 Merge branch 'master' into pip ---

1 0

[GIT] ppl/ppl(pip): Mentioned the correction of a few problems.
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: pip Commit: 22b1565be0efe35f86e6323180ff6de113b19b18 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22b1565be0ef… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 09:53:50 2011 +0100 Mentioned the correction of a few problems. --- NEWS | 17 +++++++++++++++++ 1 files changed, 17 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index cc6146c..ebdbdb3 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,23 @@ o The input routine for PPL numeric datatypes has been extended to Bugfixes ======== +o Corrected a problem in the input method for checked integers whereby, + under specific conditions, the input stream state bits were not updated. + The bug was only affecting builds using checked integer coefficients. + +o Corrected a bug in the OCaml interface, which was affecting functions + + ppl_Pointset_Powerset_<INSTANCE>_get_disjunct. + +o Corrected a couple of resource (re-)allocation problems that, under + specific conditions, could affect the correctness of Grid constructor + + Grid::Grid(const Box<Interval>& box) + + and NNC_Polyhedron method + + Polyhedron::generalized_affine_image(). + o Corrected a precision bug in method Octagonal_Shape<T>::affine_image()

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Mentioned the correction of a few problems.
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: e6f401f5b70b979d06b16bba206f39bab5e04030 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e6f401f5b70b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 10:02:42 2011 +0100 Mentioned the correction of a few problems. --- NEWS | 17 +++++++++++++++++ 1 files changed, 17 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index 15dedc3..f831f02 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,23 @@ NEWS for version 0.11.1 (release date to be decided) Bugfixes ======== +o Corrected a problem in the input method for checked integers whereby, + under specific conditions, the input stream state bits were not updated. + The bug was only affecting builds using checked integer coefficients. + +o Corrected a bug in the OCaml interface, which was affecting functions + + ppl_Pointset_Powerset_<INSTANCE>_get_disjunct. + +o Corrected a couple of resource (re-)allocation problems that, under + specific conditions, could affect the correctness of Grid constructor + + Grid::Grid(const Box<Interval>& box) + + and NNC_Polyhedron method + + Polyhedron::generalized_affine_image(). + o Corrected an efficiency bug in the C language interface function ppl_Linear_Expression_add_to_coefficient().

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Fixed function ppl_Pointset_Powerset_*_get_disjunct in OCaml interface.
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: a9aaf385df4d3f1a4a4c78898afa9b707ac3d366 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a9aaf385df4d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 5 21:01:13 2011 +0100 Fixed function ppl_Pointset_Powerset_*_get_disjunct in OCaml interface. --- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 5 +++-- 1 files changed, 3 insertions(+), 2 deletions(-) diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 index fe0f213..4a829e7 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 @@ -984,9 +984,10 @@ ppl_@CLASS@_get_disjunct(value caml_it) try { CAMLparam1(caml_it); CAMLlocal1(caml_return_value); @CPP_CLASS@::iterator& cpp_it = *p_@CLASS@_iterator_val(caml_it); - @DISJUNCT_TOPOLOGY@@A_DISJUNCT@ disjunct = cpp_it->pointset(); + const @DISJUNCT_TOPOLOGY@@A_DISJUNCT@& disjunct = cpp_it->pointset(); caml_return_value = unregistered_value_p_@DISJUNCT@(disjunct); - actual_p_@DISJUNCT@_val(caml_return_value) = mark(&disjunct); + actual_p_@DISJUNCT@_val(caml_return_value) + = const_cast<@DISJUNCT_TOPOLOGY@@A_DISJUNCT@*>(mark(&disjunct)); CAMLreturn(caml_return_value); } CATCH_ALL

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Polyhedron: fix an invalid reference bug in generalized_affine_image().
by Marco Poletti 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: ec1bbda7096c881d72d7f26eabc9a992f09dcac0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ec1bbda7096c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Feb 5 16:09:47 2011 +0100 Polyhedron: fix an invalid reference bug in generalized_affine_image(). --- src/Polyhedron_public.cc | 9 ++++----- 1 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index 9c66a31..80c293b 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -2925,15 +2925,14 @@ generalized_affine_image(const Variable var, const dimension_type eps_index = space_dim + 1; for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) if (gen_sys[i].is_point()) { - Generator& g = gen_sys[i]; - // Add a `var'-displaced copy of `g' to the generator system. - gen_sys.add_row(g); + // Add a `var'-displaced copy of `gen_sys[i]' to the generator system. + gen_sys.add_row(gen_sys[i]); if (relsym == GREATER_THAN) ++gen_sys[gen_sys.num_rows()-1][var_space_dim]; else --gen_sys[gen_sys.num_rows()-1][var_space_dim]; - // Transform `g' into a closure point. - g[eps_index] = 0; + // Transform `gen_sys[i]' into a closure point. + gen_sys[i][eps_index] = 0; } clear_constraints_up_to_date(); clear_generators_minimized();

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Grid: avoid using an invalid reference in the constructor from a Box.
by Marco Poletti 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: dd1194cc4d67b72e97dd1d1497ac8df6162589db URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dd1194cc4d67… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Feb 5 09:58:54 2011 +0100 Grid: avoid using an invalid reference in the constructor from a Box. --- src/Grid.templates.hh | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) diff --git a/src/Grid.templates.hh b/src/Grid.templates.hh index d202f83..51b01a3 100644 --- a/src/Grid.templates.hh +++ b/src/Grid.templates.hh @@ -63,8 +63,10 @@ Grid::Grid(const Box<Interval>& box, PPL_DIRTY_TEMP_COEFFICIENT(u_n); PPL_DIRTY_TEMP_COEFFICIENT(u_d); gen_sys.insert(grid_point(0*Variable(space_dim-1))); - Grid_Generator& point = gen_sys[0]; for (dimension_type k = space_dim; k-- > 0; ) { + // This is declared here because it may be invalidated by the call to + // gen_sys.insert() at the end of the loop. + Grid_Generator& point = gen_sys[0]; bool closed = false; // TODO: Consider producing the system(s) in minimized form. if (box.get_lower_bound(k, closed, l_n, l_d)) {

1 0

[GIT] ppl/ppl(master): Mentioned the correction of a few problems.
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: master Commit: 22b1565be0efe35f86e6323180ff6de113b19b18 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22b1565be0ef… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 09:53:50 2011 +0100 Mentioned the correction of a few problems. --- NEWS | 17 +++++++++++++++++ 1 files changed, 17 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index cc6146c..ebdbdb3 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,23 @@ o The input routine for PPL numeric datatypes has been extended to Bugfixes ======== +o Corrected a problem in the input method for checked integers whereby, + under specific conditions, the input stream state bits were not updated. + The bug was only affecting builds using checked integer coefficients. + +o Corrected a bug in the OCaml interface, which was affecting functions + + ppl_Pointset_Powerset_<INSTANCE>_get_disjunct. + +o Corrected a couple of resource (re-)allocation problems that, under + specific conditions, could affect the correctness of Grid constructor + + Grid::Grid(const Box<Interval>& box) + + and NNC_Polyhedron method + + Polyhedron::generalized_affine_image(). + o Corrected a precision bug in method Octagonal_Shape<T>::affine_image()

1 0

[GIT] ppl/ppl(pip): Minor readability improvements to PIP_Decision_Node:: solve().
by Enea Zaffanella 11 Feb '11

11 Feb '11

Module: ppl/ppl Branch: pip Commit: 9d99c21af3e717056a34d4f67739afb375cabe94 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9d99c21af3e7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Feb 11 08:50:37 2011 +0100 Minor readability improvements to PIP_Decision_Node::solve(). --- src/PIP_Tree.cc | 38 ++++++++++++++++++++------------------ 1 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 38a30e5..f6ff537 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1321,8 +1321,8 @@ 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); + const bool has_false_child = (false_child != 0); + const bool has_true_child = (true_child != 0); #ifdef NOISY_PIP_TREE_STRUCTURE indent_and_print(std::cerr, indent_level, "=== DECISION: SOLVING THEN CHILD\n"); @@ -1357,7 +1357,6 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, return 0; } - 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 @@ -1368,11 +1367,13 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, indent_and_print(std::cerr, indent_level, "==> merge then branch with parent.\n"); #endif - true_child->parent_merge(); - true_child->set_parent(parent()); - node = true_child; + PIP_Tree_Node* node = true_child; + node->parent_merge(); + node->set_parent(parent()); true_child = 0; delete this; + PPL_ASSERT(node->OK()); + return node; } else if (has_true_child && true_child == 0) { // True child has become unfeasible: merge this node's artificials @@ -1383,11 +1384,13 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, indent_and_print(std::cerr, indent_level, "==> merge else branch with parent.\n"); #endif - false_child->parent_merge(); - false_child->set_parent(parent()); - node = false_child; + PIP_Tree_Node* node = false_child; + node->parent_merge(); + node->set_parent(parent()); false_child = 0; delete this; + PPL_ASSERT(node->OK()); + return node; } else if (check_feasible_context) { // Test all constraints for redundancy with the context, and eliminate @@ -1401,7 +1404,7 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, 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. + // The constraint is not redundant with the context: keep it. constraints_.insert(*ci); } } @@ -1413,16 +1416,17 @@ PIP_Decision_Node::solve(const PIP_Problem& pip, indent_and_print(std::cerr, indent_level, "==> merge then branch with parent.\n"); #endif - /* FIXME: shouldn't we delete the else branch? */ - true_child->parent_merge(); - true_child->set_parent(parent()); - node = true_child; + PIP_Tree_Node* node = true_child; + node->parent_merge(); + node->set_parent(parent()); true_child = 0; delete this; + PPL_ASSERT(node->OK()); + return node; } } - PPL_ASSERT(node->OK()); - return node; + PPL_ASSERT(OK()); + return this; } void @@ -2906,7 +2910,6 @@ PIP_Solution_Node::solve(const PIP_Problem& pip, // and protect new 'parent' node from exception safety issues. wrapped_node.release(); wrapped_node.reset(parent); - /* FIXME: delete this; */ // Restore into parent `cs' and `aps'. parent->constraints_.swap(cs); parent->artificial_parameters.swap(aps); @@ -2917,7 +2920,6 @@ PIP_Solution_Node::solve(const PIP_Problem& pip, return wrapped_node.release(); } else { - /* FIXME: delete this; */ // Merge t_node with its parent: // a) append into `cs' the constraints of t_node; for (Constraint_System::const_iterator

1 0