- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Simplify function names in PIP_Tree_Node, matching
by Patricia Hill 08 Apr '10

08 Apr '10

Module: ppl/ppl Branch: master Commit: 924d4fbdd9192a6b03c9fbea4c4e5f0d71411f96 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=924d4fbdd919… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu Apr 8 12:29:57 2010 +0100 Simplify function names in PIP_Tree_Node, matching corresponding predicate names in Prolog interface. --- interfaces/OCaml/ppl_ocaml_common.cc | 6 +++--- interfaces/OCaml/ppl_ocaml_globals.ml | 12 ++++++------ interfaces/OCaml/ppl_ocaml_globals.mli | 6 +++--- interfaces/OCaml/tests/test1.ml | 10 +++++----- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/interfaces/OCaml/ppl_ocaml_common.cc b/interfaces/OCaml/ppl_ocaml_common.cc index 9f3e8bf..291298b 100644 --- a/interfaces/OCaml/ppl_ocaml_common.cc +++ b/interfaces/OCaml/ppl_ocaml_common.cc @@ -1626,7 +1626,7 @@ CATCH_ALL extern "C" CAMLprim value -ppl_PIP_Tree_Node_get_parametric_values(value caml_node, +ppl_PIP_Tree_Node_parametric_values(value caml_node, value caml_dim) try { CAMLparam2(caml_node, caml_dim); const PIP_Tree_Node* ppl_node = p_PIP_Tree_Node_val(caml_node); @@ -1647,7 +1647,7 @@ CATCH_ALL extern "C" CAMLprim value -ppl_PIP_Tree_Node_get_true_child(value caml_node) try { +ppl_PIP_Tree_Node_true_child(value caml_node) try { CAMLparam1(caml_node); const PIP_Tree_Node* ppl_node = p_PIP_Tree_Node_val(caml_node); const PIP_Tree_Node* child = ppl_PIP_Tree_Node_get_child(ppl_node, true); @@ -1657,7 +1657,7 @@ CATCH_ALL extern "C" CAMLprim value -ppl_PIP_Tree_Node_get_false_child(value caml_node) try { +ppl_PIP_Tree_Node_false_child(value caml_node) try { CAMLparam1(caml_node); const PIP_Tree_Node* ppl_node = p_PIP_Tree_Node_val(caml_node); const PIP_Tree_Node* child = ppl_PIP_Tree_Node_get_child(ppl_node, false); diff --git a/interfaces/OCaml/ppl_ocaml_globals.ml b/interfaces/OCaml/ppl_ocaml_globals.ml index 5ce4c8f..3d1e7a4 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.ml +++ b/interfaces/OCaml/ppl_ocaml_globals.ml @@ -414,18 +414,18 @@ external ppl_PIP_Tree_Node_is_solution: pip_tree_node -> bool = "ppl_PIP_Tree_Node_is_solution" -external ppl_PIP_Tree_Node_get_parametric_values: +external ppl_PIP_Tree_Node_parametric_values: pip_tree_node -> int -> linear_expression - = "ppl_PIP_Tree_Node_get_parametric_values" + = "ppl_PIP_Tree_Node_parametric_values" external ppl_PIP_Tree_Node_is_decision: pip_tree_node -> bool = "ppl_PIP_Tree_Node_is_decision" -external ppl_PIP_Tree_Node_get_true_child: +external ppl_PIP_Tree_Node_true_child: pip_tree_node -> pip_tree_node - = "ppl_PIP_Tree_Node_get_true_child" + = "ppl_PIP_Tree_Node_true_child" -external ppl_PIP_Tree_Node_get_false_child: +external ppl_PIP_Tree_Node_false_child: pip_tree_node -> pip_tree_node - = "ppl_PIP_Tree_Node_get_false_child" + = "ppl_PIP_Tree_Node_false_child" diff --git a/interfaces/OCaml/ppl_ocaml_globals.mli b/interfaces/OCaml/ppl_ocaml_globals.mli index e43b10c..8ffb016 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.mli +++ b/interfaces/OCaml/ppl_ocaml_globals.mli @@ -356,14 +356,14 @@ val ppl_PIP_Tree_Node_is_bottom: val ppl_PIP_Tree_Node_is_solution: pip_tree_node -> bool -val ppl_PIP_Tree_Node_get_parametric_values: +val ppl_PIP_Tree_Node_parametric_values: pip_tree_node -> int -> linear_expression val ppl_PIP_Tree_Node_is_decision: pip_tree_node -> bool -val ppl_PIP_Tree_Node_get_true_child: +val ppl_PIP_Tree_Node_true_child: pip_tree_node -> pip_tree_node -val ppl_PIP_Tree_Node_get_false_child: +val ppl_PIP_Tree_Node_false_child: pip_tree_node -> pip_tree_node diff --git a/interfaces/OCaml/tests/test1.ml b/interfaces/OCaml/tests/test1.ml index dcf8ac4..66d6b8a 100644 --- a/interfaces/OCaml/tests/test1.ml +++ b/interfaces/OCaml/tests/test1.ml @@ -597,21 +597,21 @@ let out = if (ppl_PIP_Tree_Node_artificials node = []) in (print_string_if_noisy out);; print_string_if_noisy "\n";; let _node_cs = ppl_PIP_Tree_Node_constraints node;; -let tchild = ppl_PIP_Tree_Node_get_true_child node;; -let _fchild = ppl_PIP_Tree_Node_get_false_child node;; +let tchild = ppl_PIP_Tree_Node_true_child node;; +let _fchild = ppl_PIP_Tree_Node_false_child node;; let out = if (ppl_PIP_Tree_Node_is_decision tchild) then "ppl_PIP_Tree_Node_is_decision tchild test succeeded" else "ppl_PIP_Tree_Node_is_decision tchild test failed" in (print_string_if_noisy out);; print_string_if_noisy "\n";; -let ttchild = ppl_PIP_Tree_Node_get_true_child tchild;; -let ftchild = ppl_PIP_Tree_Node_get_false_child tchild;; +let ttchild = ppl_PIP_Tree_Node_true_child tchild;; +let ftchild = ppl_PIP_Tree_Node_false_child tchild;; let out = if (ppl_PIP_Tree_Node_is_solution ttchild) then "ppl_PIP_Tree_Node_is_decision ttchild test succeeded" else "ppl_PIP_Tree_Node_is_decision ttchild test failed" in (print_string_if_noisy out);; print_string_if_noisy "\n";; -let _par_vals = ppl_PIP_Tree_Node_get_parametric_values ttchild 0;; +let _par_vals = ppl_PIP_Tree_Node_parametric_values ttchild 0;; let _ftchild_arts = ppl_PIP_Tree_Node_artificials ftchild;; (* Pointset_Powerset_Grid is not enabled by default, the following code is *)

1 0

[GIT] ppl/ppl(master): Simplified Prolog interface for PIP_Tree_Node.
by Patricia Hill 08 Apr '10

08 Apr '10

Module: ppl/ppl Branch: master Commit: 97c151b721fbfa9963d9b873355b163181f0d07b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97c151b721fb… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu Apr 8 12:06:01 2010 +0100 Simplified Prolog interface for PIP_Tree_Node. --- ...erface_generator_prolog_procedure_generators.m4 | 11 +++-- interfaces/Prolog/ppl_prolog_common.cc | 46 ++++++++++---------- interfaces/Prolog/ppl_prolog_common.defs.hh | 23 +++++----- interfaces/Prolog/tests/pl_check.pl | 34 +++++++------- 4 files changed, 58 insertions(+), 56 deletions(-) diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 index 1d80e1c..cfd158b 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 @@ -107,13 +107,14 @@ ppl_PIP_Problem_optimizing_solution/2, ppl_PIP_Problem_OK/1, ppl_PIP_Problem_ascii_dump/1, ppl_PIP_Tree_Node_constraints/2, -ppl_PIP_Tree_Node_as_solution/2, -ppl_PIP_Tree_Node_as_decision/2, +ppl_PIP_Tree_Node_is_solution/1, +ppl_PIP_Tree_Node_is_decision/1, +ppl_PIP_Tree_Node_is_bottom/1, ppl_PIP_Tree_Node_artificials/2, ppl_PIP_Tree_Node_OK/1, -ppl_PIP_Solution_Node_get_parametric_values/3, -ppl_PIP_Decision_Node_get_true_child/2, -ppl_PIP_Decision_Node_get_false_child/2`'dnl +ppl_PIP_Tree_Node_parametric_values/3, +ppl_PIP_Tree_Node_true_child/2, +ppl_PIP_Tree_Node_false_child/2`'dnl ') m4_define(`m4_procedure_list', diff --git a/interfaces/Prolog/ppl_prolog_common.cc b/interfaces/Prolog/ppl_prolog_common.cc index fbb985d..cf55e9a 100644 --- a/interfaces/Prolog/ppl_prolog_common.cc +++ b/interfaces/Prolog/ppl_prolog_common.cc @@ -2996,43 +2996,43 @@ ppl_PIP_Tree_Node_constraints(Prolog_term_ref t_pip, } extern "C" Prolog_foreign_return_type -ppl_PIP_Tree_Node_as_solution(Prolog_term_ref t_pip, - Prolog_term_ref t_sol) { +ppl_PIP_Tree_Node_is_solution(Prolog_term_ref t_pip) { static const char* where = "ppl_PIP_Tree_Node_as_solution/2"; try { const PIP_Tree_Node* pip = term_to_handle<PIP_Tree_Node>(t_pip, where); PPL_CHECK(pip); - PIP_Solution_Node* sol = const_cast<PIP_Solution_Node*>(pip->as_solution()); - if (sol == 0) - return PROLOG_FAILURE; - Prolog_term_ref t_ppl_sol = Prolog_new_term_ref(); - Prolog_put_address(t_ppl_sol, sol); - if (Prolog_unify(t_sol, t_ppl_sol)) { - PPL_WEAK_REGISTER(sol); + if (pip != 0 && pip->as_solution() != 0) return PROLOG_SUCCESS; - } + return PROLOG_FAILURE; } CATCH_ALL; } extern "C" Prolog_foreign_return_type -ppl_PIP_Tree_Node_as_decision(Prolog_term_ref t_pip, - Prolog_term_ref t_dec) { +ppl_PIP_Tree_Node_is_decision(Prolog_term_ref t_pip) { static const char* where = "ppl_PIP_Tree_Node_as_decision/2"; try { const PIP_Tree_Node* pip = term_to_handle<PIP_Tree_Node>(t_pip, where); PPL_CHECK(pip); - PIP_Decision_Node* dec = const_cast<PIP_Decision_Node*>(pip->as_decision()); - if (dec == 0) - return PROLOG_FAILURE; - Prolog_term_ref t_ppl_dec = Prolog_new_term_ref(); - Prolog_put_address(t_ppl_dec, dec); - if (Prolog_unify(t_dec, t_ppl_dec)) { - PPL_WEAK_REGISTER(dec); + if (pip != 0 && pip->as_decision() != 0) return PROLOG_SUCCESS; - } + return PROLOG_FAILURE; + } + CATCH_ALL; +} + +extern "C" Prolog_foreign_return_type +ppl_PIP_Tree_Node_is_bottom(Prolog_term_ref t_pip) { + static const char* where = "ppl_PIP_Tree_Node_as_decision/2"; + try { + const PIP_Tree_Node* pip = term_to_handle<PIP_Tree_Node>(t_pip, where); + PPL_CHECK(pip); + + if (pip == 0) + return PROLOG_SUCCESS; + return PROLOG_FAILURE; } CATCH_ALL; } @@ -3060,7 +3060,7 @@ ppl_PIP_Tree_Node_artificials(Prolog_term_ref t_tree_node, } extern "C" Prolog_foreign_return_type -ppl_PIP_Solution_Node_get_parametric_values(Prolog_term_ref t_pip, +ppl_PIP_Tree_Node_parametric_values(Prolog_term_ref t_pip, Prolog_term_ref t_var, Prolog_term_ref t_le) { static const char* where = "ppl_PIP_Solution_Node_get_parametric_values/3"; @@ -3076,7 +3076,7 @@ ppl_PIP_Solution_Node_get_parametric_values(Prolog_term_ref t_pip, } extern "C" Prolog_foreign_return_type -ppl_PIP_Decision_Node_get_true_child(Prolog_term_ref t_pip, +ppl_PIP_Tree_Node_true_child(Prolog_term_ref t_pip, Prolog_term_ref t_ptree) { static const char* where = "ppl_PIP_Decision_Node_get_true_child/2"; try { @@ -3096,7 +3096,7 @@ ppl_PIP_Decision_Node_get_true_child(Prolog_term_ref t_pip, } extern "C" Prolog_foreign_return_type -ppl_PIP_Decision_Node_get_false_child(Prolog_term_ref t_pip, +ppl_PIP_Tree_Node_false_child(Prolog_term_ref t_pip, Prolog_term_ref t_ptree) { static const char* where = "ppl_PIP_Decision_Node_get_false_child/2"; try { diff --git a/interfaces/Prolog/ppl_prolog_common.defs.hh b/interfaces/Prolog/ppl_prolog_common.defs.hh index 337b9fc..53a9b63 100644 --- a/interfaces/Prolog/ppl_prolog_common.defs.hh +++ b/interfaces/Prolog/ppl_prolog_common.defs.hh @@ -1046,12 +1046,13 @@ ppl_PIP_Tree_Node_constraints(Prolog_term_ref t_tree_node, Prolog_term_ref t_clist); extern "C" Prolog_foreign_return_type -ppl_PIP_Tree_Node_as_solution(Prolog_term_ref t_tree_node, - Prolog_term_ref t_sol_node); +ppl_PIP_Tree_Node_is_solution(Prolog_term_ref t_tree_node); extern "C" Prolog_foreign_return_type -ppl_PIP_Tree_Node_as_decision(Prolog_term_ref t_tree_node, - Prolog_term_ref t_dec_node); +ppl_PIP_Tree_Node_is_decision(Prolog_term_ref t_tree_node); + +extern "C" Prolog_foreign_return_type +ppl_PIP_Tree_Node_is_bottom(Prolog_term_ref t_tree_node); extern "C" Prolog_foreign_return_type ppl_PIP_Tree_Node_artificials(Prolog_term_ref t_tree_node, @@ -1061,17 +1062,17 @@ extern "C" Prolog_foreign_return_type ppl_PIP_Tree_Node_OK(Prolog_term_ref t_pip_tree); extern "C" Prolog_foreign_return_type -ppl_PIP_Solution_Node_get_parametric_values(Prolog_term_ref t_pip_sol, - Prolog_term_ref t_var, - Prolog_term_ref t_pvalue_list); +ppl_PIP_Tree_Node_parametric_values(Prolog_term_ref t_pip_sol, + Prolog_term_ref t_var, + Prolog_term_ref t_pvalue_list); extern "C" Prolog_foreign_return_type -ppl_PIP_Decision_Node_get_true_child(Prolog_term_ref t_pip_dec, - Prolog_term_ref t_pip_tree); +ppl_PIP_Tree_Node_true_child(Prolog_term_ref t_pip_dec, + Prolog_term_ref t_pip_tree); extern "C" Prolog_foreign_return_type -ppl_PIP_Decision_Node_get_false_child(Prolog_term_ref t_pip_dec, - Prolog_term_ref t_pip_tree); +ppl_PIP_Tree_Node_false_child(Prolog_term_ref t_pip_dec, + Prolog_term_ref t_pip_tree); using namespace Parma_Polyhedra_Library; using namespace Parma_Polyhedra_Library::Interfaces::Prolog; diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index e70d85a..83d3e48 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -2464,29 +2464,29 @@ pip_solution :- make_vars(4, [I, J, M, N]), clean_ppl_new_PIP_Problem( 4, [3*J >= -2*I + 8, J =< 4*I - 4, J =< M, I =< N], [M,N], PIP), - ppl_PIP_Problem_solution(PIP, Tree_Node), - ppl_PIP_Tree_Node_artificials(Tree_Node, Artificials), + ppl_PIP_Problem_solution(PIP, Node), + ppl_PIP_Tree_Node_artificials(Node, Artificials), Artificials = [], - \+ ppl_PIP_Tree_Node_as_solution(Tree_Node, _Sol), - ppl_PIP_Tree_Node_constraints(Tree_Node, _CS), - ppl_PIP_Tree_Node_as_decision(Tree_Node, Dec), - ppl_PIP_Tree_Node_constraints(Dec, _CS1), - ppl_PIP_Decision_Node_get_true_child(Dec, TChild), - ppl_PIP_Decision_Node_get_false_child(Dec, _FChild), - ppl_PIP_Tree_Node_as_decision(TChild, TChild_Dec), - ppl_PIP_Decision_Node_get_true_child(TChild_Dec, TTChild), - \+ ppl_PIP_Tree_Node_as_decision(TTChild, _TTChild_Dec), - ppl_PIP_Tree_Node_as_solution(TTChild, TTChild_Sol), - ppl_PIP_Solution_Node_get_parametric_values(TTChild_Sol, I, _TPV), - ppl_PIP_Decision_Node_get_false_child(TChild_Dec, FTChild), + \+ ppl_PIP_Tree_Node_is_solution(Node), + ppl_PIP_Tree_Node_constraints(Node, _CS), + ppl_PIP_Tree_Node_is_decision(Node), + ppl_PIP_Tree_Node_constraints(Node, _CS1), + ppl_PIP_Tree_Node_true_child(Node, TChild), + ppl_PIP_Tree_Node_false_child(Node, _FChild), + ppl_PIP_Tree_Node_is_decision(TChild), + ppl_PIP_Tree_Node_true_child(TChild, TTChild), + \+ ppl_PIP_Tree_Node_is_decision(TTChild), + ppl_PIP_Tree_Node_is_solution(TTChild), + ppl_PIP_Tree_Node_parametric_values(TTChild, I, _TPV), + ppl_PIP_Tree_Node_false_child(TChild, FTChild), ppl_PIP_Tree_Node_artificials(FTChild, FTChild_Artificials), FTChild_Artificials = [Art_LinExpr/Art_Den], compare_lin_expressions(Art_LinExpr, M), Art_Den = 2, - ppl_PIP_Tree_Node_as_solution(FTChild, FTChild_Sol), - ppl_PIP_Solution_Node_get_parametric_values(FTChild_Sol, I, _FPV), + ppl_PIP_Tree_Node_is_solution(FTChild), + ppl_PIP_Tree_Node_parametric_values(FTChild, I, _FPV), ppl_PIP_Problem_OK(PIP), - ppl_PIP_Tree_Node_OK(Tree_Node), + ppl_PIP_Tree_Node_OK(Node), !, ppl_delete_PIP_Problem(PIP).

1 0

[GIT] ppl/ppl(master): Removed artificial_parameter_sequence type.
by Patricia Hill 08 Apr '10

08 Apr '10

Module: ppl/ppl Branch: master Commit: 46aa53b6bc9849ad622c1f0fcb6dbc763059af41 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=46aa53b6bc98… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu Apr 8 11:44:06 2010 +0100 Removed artificial_parameter_sequence type. Added to the PIP_Problem tests. --- interfaces/OCaml/ppl_ocaml_globals.ml | 4 +- interfaces/OCaml/ppl_ocaml_globals.mli | 4 +- interfaces/OCaml/tests/test1.ml | 172 +++++++++++++++++++++++--------- 3 files changed, 127 insertions(+), 53 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=46aa53b6…

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Patricia Hill 08 Apr '10

08 Apr '10

Module: ppl/ppl Branch: master Commit: 99f17d8aa4bd39d2dfb3b9404a73ea907f7d2698 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=99f17d8aa4bd… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu Apr 8 11:42:06 2010 +0100 Typo fixed. --- interfaces/Prolog/tests/pl_check.pl | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index d291960..e70d85a 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -2472,7 +2472,7 @@ pip_solution :- ppl_PIP_Tree_Node_as_decision(Tree_Node, Dec), ppl_PIP_Tree_Node_constraints(Dec, _CS1), ppl_PIP_Decision_Node_get_true_child(Dec, TChild), - ppl_PIP_Decision_Node_get_true_child(Dec, _FChild), + ppl_PIP_Decision_Node_get_false_child(Dec, _FChild), ppl_PIP_Tree_Node_as_decision(TChild, TChild_Dec), ppl_PIP_Decision_Node_get_true_child(TChild_Dec, TTChild), \+ ppl_PIP_Tree_Node_as_decision(TTChild, _TTChild_Dec),

1 0

[GIT] ppl/w3ppl(master): Added BagnaraMPZ10TR.
by Roberto Bagnara 07 Apr '10

07 Apr '10

Module: ppl/w3ppl Branch: master Commit: 77f2d0719a99cb91bbc7fb9156197a453ddb52d0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=77f2d0719a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Apr 7 21:28:33 2010 +0200 Added BagnaraMPZ10TR. --- htdocs/Documentation/ppl.bib | 34 ++++++++++++++++++++++++++++++++++ 1 files changed, 34 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index ee137a7..fe8ae8c 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -373,6 +373,40 @@ algorithm for the domain of \emph{octagonal shapes}.", } +@Techreport{BagnaraMPZ10TR, + Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella", + Title = "The Automatic Synthesis of Linear Ranking Functions: + The Complete Unabridged Version", + Number = 498, + Type = "Quaderno", + Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", + Year = 2010, + Note = "Available at \url{http://www.cs.unipr.it/Publications/}. + Also published as {\tt arXiv:cs.PL/1004.0944}, + available from \url{http://arxiv.org/}.", + Abstract = "The classical technique for proving termination of a + generic sequential computer program involves the + synthesis of a \emph{ranking function} for each loop of + the program. \emph{Linear} ranking functions are + particularly interesting because many terminating loops + admit one and algorithms exist to automatically + synthesize it. In this paper we present two such + algorithms: one based on work dated 1991 by Sohn and + Van~Gelder; the other, due to Podelski and Rybalchenko, + dated 2004. Remarkably, while the two algorithms will + synthesize a linear ranking function under exactly the + same set of conditions, the former is mostly unknown to + the community of termination analysis and its general + applicability has never been put forward before the + present paper. In this paper we thoroughly justify both + algorithms, we prove their correctness, we compare their + worst-case complexity and experimentally evaluate their + efficiency, and we present an open-source implementation + of them that will make it very easy to include + termination-analysis capabilities in automatic program + verifiers." +} + @InProceedings{BagnaraRZH02, Author = "R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill", Title = "Possibly Not Closed Convex Polyhedra

1 0

[GIT] ppl/ppl(master): Restructured the OCaml interface to PIP_Tree_Node C++ classes.
by Enea Zaffanella 07 Apr '10

07 Apr '10

Module: ppl/ppl Branch: master Commit: 6f92bdda48d52db1c27f36537b9af13f20b6c755 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6f92bdda48d5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Apr 7 17:37:14 2010 +0200 Restructured the OCaml interface to PIP_Tree_Node C++ classes. Also corrected several bugs related to object finalization. --- interfaces/OCaml/ppl_ocaml_common.cc | 238 ++++++++++++++------------------ interfaces/OCaml/ppl_ocaml_globals.ml | 46 +++---- interfaces/OCaml/ppl_ocaml_globals.mli | 34 ++--- 3 files changed, 141 insertions(+), 177 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=6f92bdda…

1 0

[GIT] ppl/ppl(master): Added a couple of entries.
by Enea Zaffanella 06 Apr '10

06 Apr '10

Module: ppl/ppl Branch: master Commit: f39f1ccdbe873dfac61fd101c1075f11678e98dc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f39f1ccdbe87… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 6 11:24:24 2010 +0200 Added a couple of entries. --- NEWS | 20 +++++++++++++++++--- 1 files changed, 17 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 835744d..74781bc 100644 --- a/NEWS +++ b/NEWS @@ -38,14 +38,28 @@ o The C and Java interfaces now support timeout computation facilities. o New configuration option `--with-gmp-build=DIR' allows to use a non-installed build of GMP in DIR. -o New methods +o New class PIP_Problem provides a Parametric Integer Programming (PIP) + problem solver mainly based on P. Feautrier's specification. + The implementation combines a parametric dual simplex algorithm using + exact arithmetic with Gomory's cut generation. + Still under beta testing. + +o New Linear_Expression methods - bool Linear_Expression::is_zero() const - bool Linear_Expression::all_homogeneous_terms_are_zero() const + bool is_zero() const + bool all_homogeneous_terms_are_zero() const return true if and only if `*this' is 0, and if and only if all the homogeneous terms of `*this' are 0, respectively. +o New Linear_Expression methods + + void add_mul_assign(Coefficient_traits::const_reference c, Variable v) + void sub_mul_assign(Coefficient_traits::const_reference c, Variable v) + + assign linear expression *this + c * v (resp., *this - c * v) to *this, + while avoiding the allocation of a temporary Linear_Expression. + o For the PPL semantic objects, other than the Pointset_Powerset and Partially_Reduced Product, there is a new method:

1 0

[GIT] ppl/ppl(master): ...get_big_parameter_dimension/2 changed to
by Patricia Hill 06 Apr '10

06 Apr '10

Module: ppl/ppl Branch: master Commit: 8354fb40ac3b479de4176560139e6daba5d46bc7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8354fb40ac3b… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Apr 6 09:52:31 2010 +0100 ..get_big_parameter_dimension/2 changed to ..has_big_parameter_dimension/2 and now this fails if the "big dimension" == not_a_dimension(). --- ...erface_generator_prolog_procedure_generators.m4 | 2 +- interfaces/Prolog/ppl_prolog_common.cc | 7 +++++-- interfaces/Prolog/ppl_prolog_common.defs.hh | 2 +- interfaces/Prolog/tests/pl_check.pl | 19 +++++++++++-------- 4 files changed, 18 insertions(+), 12 deletions(-) diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 index e29aeda..1d80e1c 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 @@ -98,7 +98,7 @@ ppl_PIP_Problem_add_constraint/2, ppl_PIP_Problem_add_constraints/2, ppl_PIP_Problem_set_control_parameter/2 *nofail, ppl_PIP_Problem_get_control_parameter/3, -ppl_PIP_Problem_get_big_parameter_dimension/2, +ppl_PIP_Problem_has_big_parameter_dimension/2, ppl_PIP_Problem_set_big_parameter_dimension/2, ppl_PIP_Problem_is_satisfiable/1, ppl_PIP_Problem_solve/2, diff --git a/interfaces/Prolog/ppl_prolog_common.cc b/interfaces/Prolog/ppl_prolog_common.cc index 1c945a2..fbb985d 100644 --- a/interfaces/Prolog/ppl_prolog_common.cc +++ b/interfaces/Prolog/ppl_prolog_common.cc @@ -2846,13 +2846,16 @@ ppl_PIP_Problem_set_control_parameter(Prolog_term_ref t_pip, } extern "C" Prolog_foreign_return_type -ppl_PIP_Problem_get_big_parameter_dimension(Prolog_term_ref t_pip, +ppl_PIP_Problem_has_big_parameter_dimension(Prolog_term_ref t_pip, Prolog_term_ref t_d) { static const char* where = "ppl_PIP_Problem_get_big_parameter_dimension/2"; try { PIP_Problem* pip = term_to_handle<PIP_Problem>(t_pip, where); PPL_CHECK(pip); - if (unify_ulong(t_d, pip->get_big_parameter_dimension())) + dimension_type dim = pip->get_big_parameter_dimension(); + if (dim == not_a_dimension()) + return PROLOG_FAILURE; + if (unify_ulong(t_d, dim)) return PROLOG_SUCCESS; } CATCH_ALL; diff --git a/interfaces/Prolog/ppl_prolog_common.defs.hh b/interfaces/Prolog/ppl_prolog_common.defs.hh index e1be161..337b9fc 100644 --- a/interfaces/Prolog/ppl_prolog_common.defs.hh +++ b/interfaces/Prolog/ppl_prolog_common.defs.hh @@ -1028,7 +1028,7 @@ ppl_PIP_Problem_optimizing_solution(Prolog_term_ref t_pip, Prolog_term_ref t_pip_tree); extern "C" Prolog_foreign_return_type -ppl_PIP_Problem_get_big_parameter_dimension(Prolog_term_ref t_pip, +ppl_PIP_Problem_has_big_parameter_dimension(Prolog_term_ref t_pip, Prolog_term_ref t_d); extern "C" Prolog_foreign_return_type diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index c3a29ad..d291960 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -2428,16 +2428,19 @@ pip_set :- make_vars(3, [A, B, C]), clean_ppl_new_PIP_Problem( 3, [A >= 0, A =< 3, A + B + C >= 9, B >= 5, C =< 5], [B], PIP), - pl_check_prolog_flag(bounded, Y), - (Y == false -> - ppl_PIP_Problem_get_big_parameter_dimension(PIP, _X) -% ppl_PIP_Problem_set_big_parameter_dimension(PIP, X), - ; - true - ), + \+ ppl_PIP_Problem_has_big_parameter_dimension(PIP, _X), ppl_PIP_Problem_solve(PIP, optimized), !, - ppl_delete_PIP_Problem(PIP). + ppl_delete_PIP_Problem(PIP), + + make_vars(4, [X, Y, P, M]), + clean_ppl_new_PIP_Problem( + 4, [Y - M >= -2*X + 2*M - 4, 2*Y - 2*M =< X - M + 2*P], [P, M], PIP1), + ppl_PIP_Problem_set_big_parameter_dimension(PIP1, 3), + ppl_PIP_Problem_has_big_parameter_dimension(PIP1, 3), + ppl_PIP_Problem_solve(PIP1, optimized), + !, + ppl_delete_PIP_Problem(PIP1). pip_solve :- make_vars(3, [A, B, C]),

1 0

[GIT] ppl/ppl(master): Solaris users should install GNU sed.
by Enea Zaffanella 06 Apr '10

06 Apr '10

Module: ppl/ppl Branch: master Commit: 5c4bc05adbdf6d6b2d853ad0ddb926c21695bc3a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c4bc05adbdf… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 6 10:18:29 2010 +0200 Solaris users should install GNU sed. --- README.Solaris | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/README.Solaris b/README.Solaris new file mode 100644 index 0000000..e454198 --- /dev/null +++ b/README.Solaris @@ -0,0 +1,8 @@ +Build problems have been reported for Solaris 10, affecting the build +of the Java language interface, which are due to the use of an +incompatible version of sed: + + https://www.cs.unipr.it/mantis/view.php?id=103 + +The solution is to install and use GNU sed. +This is recommended, even when only using the C++ language interface.

1 0

[GIT] ppl/ppl(master): Check if the Prolog system supports unbounded integers before
by Patricia Hill 06 Apr '10

06 Apr '10

Module: ppl/ppl Branch: master Commit: 087b4f0fa21c23ce4799ec96ad8108cb7911c40a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=087b4f0fa21c… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Apr 6 09:00:38 2010 +0100 Check if the Prolog system supports unbounded integers before testing the big_parameter for PIP_Problem. --- interfaces/Prolog/tests/pl_check.pl | 7 ++++++- 1 files changed, 6 insertions(+), 1 deletions(-) diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index 0db2379..c3a29ad 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -2428,8 +2428,13 @@ pip_set :- make_vars(3, [A, B, C]), clean_ppl_new_PIP_Problem( 3, [A >= 0, A =< 3, A + B + C >= 9, B >= 5, C =< 5], [B], PIP), - ppl_PIP_Problem_get_big_parameter_dimension(PIP, _X), + pl_check_prolog_flag(bounded, Y), + (Y == false -> + ppl_PIP_Problem_get_big_parameter_dimension(PIP, _X) % ppl_PIP_Problem_set_big_parameter_dimension(PIP, X), + ; + true + ), ppl_PIP_Problem_solve(PIP, optimized), !, ppl_delete_PIP_Problem(PIP).

1 0