March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Wrong latex fixed.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 706a703a5546abc8c54fc35ad2c2574429aadc40 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=706a703a5546… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 16:49:55 2010 +0000 Wrong latex fixed. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 469ce91..403cf99 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2214,7 +2214,7 @@ where \f$\vect{w} \in \cL\f$ and |\mathrm{val}| = \min\Bigl\{ \big|\langle \vect{a}, \vect{v} \rangle + b - \big| \Big| \vect{v} \in \cL + \bigm| \Big| \vect{v} \in \cL \Bigr\}. \f]

1 0

[GIT] ppl/ppl(master): Added two new tests.
by Roberto Bagnara 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 418e4ff3dc14d5c18445ca52c0668c8eb2d68289 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=418e4ff3dc14… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Mar 23 20:01:58 2010 +0400 Added two new tests. --- tests/Polyhedron/termination1.cc | 68 ++++++++++++++++++++++++++++++++++++++ 1 files changed, 68 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index b17af5b..0d86c03 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -425,6 +425,72 @@ test18() { return !termination_test_PR(ph); } +bool +test19() { + Variable D(0); + Variable E(1); + Variable F(2); + Variable A(3); + Variable B(4); + Variable C(5); + C_Polyhedron ph(6); + + ph.add_constraint(A == D); + ph.add_constraint(B == E); + ph.add_constraint(B - F >= 0); + ph.add_constraint(A - F >= 0); + ph.add_constraint(C >=0); + ph.add_constraint(C - F <= -1); + + Generator witness(point()); + one_affine_ranking_function_PR(ph, witness); + + print_generator(witness, "*** witness ***"); + + Variable mu1(0); + Variable mu2(1); + Variable mu3(2); + Variable mu0(3); + Generator known_result(point(0*mu0 + 1*mu1 - 1*mu3)); + + print_generator(known_result, "*** known_result ***"); + + return known_result == witness; +} + +bool +test20() { + Variable D(0); + Variable E(1); + Variable F(2); + Variable A(3); + Variable B(4); + Variable C(5); + C_Polyhedron ph(6); + + ph.add_constraint(A == D); + ph.add_constraint(B == E); + ph.add_constraint(B - F >= 0); + ph.add_constraint(A - F >= 0); + ph.add_constraint(C >=0); + ph.add_constraint(C - F <= -1); + + Generator witness(point()); + one_affine_ranking_function_MS(ph, witness); + + print_generator(witness, "*** witness ***"); + + Variable mu1(0); + Variable mu2(1); + Variable mu3(2); + Variable mu0(3); + Generator known_result(point(-1*mu0 + 1*mu1 - 1*mu3)); + + print_generator(known_result, "*** known_result ***"); + + return known_result == witness; +} + } // namespace BEGIN_MAIN @@ -446,4 +512,6 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); + DO_TEST(test20); END_MAIN

1 0

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 23 Mar '10

23 Mar '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fa2e479513ed… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 16:00:22 2010 +0100 PIP_Solution_Node: use two-argument add_zero_columns() in update_tableau() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=372e574ca99b… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:59:29 2010 +0100 Dense_Matrix: add two-argument add_zero_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a9eb5d2e74da… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:59:06 2010 +0100 Dense_Matrix: fix assertion in permute_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c9300432feb8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:57:16 2010 +0100 Sparse_Matrix: add two-argument add_zero_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=52721116a3dd… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:56:34 2010 +0100 Unlimited_Sparse_Row: add method add_zeroes_and_shift(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7e8eabade51c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:08:28 2010 +0100 PIP_Tree_Node: use the newer find_create() versions in compatibility_check(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d67a9ccb10f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:07:46 2010 +0100 Dense_Row: add other versions of find_create().

1 0

[GIT] ppl/ppl(master): Several errors in the documentation for frequency fixed.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: e47ae35e17b0f82f3efd533085ea826db9cf86f3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e47ae35e17b0… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 14:24:19 2010 +0000 Several errors in the documentation for frequency fixed. --- doc/definitions.dox | 14 +++++++------- 1 files changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index a0f8782..469ce91 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2201,8 +2201,8 @@ affine expression \f$\mathrm{rhs}\f$. Let \f$\cL \in \Gset_n\f$ be any non-empty grid and \f$\mathrm{expr} = \bigl(\langle \vect{a}, \vect{x} \rangle + b\bigr)\f$ be a linear expression. Then if, for -some \f$b, f \in \Rset\f$, all the points in \f$\cL\f$ satisfy the -congruence \f$\cg = ( \mathrm{expr} \equiv_f b )\f$, then the maximum +some \f$c, f \in \Rset\f$, all the points in \f$\cL\f$ satisfy the +congruence \f$\cg = ( \mathrm{expr} \equiv_f c )\f$, then the maximum \f$f\f$ such that this holds is called the <EM>frequency</EM> of \f$\cL\f$ with respect to \f$\mathrm{expr}\f$. @@ -2213,8 +2213,8 @@ where \f$\vect{w} \in \cL\f$ and \f[ |\mathrm{val}| = \min\Bigl\{ - \bigl|\langle \vect{a}, \vect{v} \rangle + b - \bigr| \st \vect{v} \in \cL + \big|\langle \vect{a}, \vect{v} \rangle + b + \big| \Big| \vect{v} \in \cL \Bigr\}. \f] @@ -2222,9 +2222,9 @@ Observe that the above definition is also applied to other simple objects in the library like polyhedra, octagonal shapes, bd-shapes and boxes and in such cases the definition of frequency can be simplified. For instance, the frequency for an object \f$\cP \in \Pset_n\f$ is -defined if and only if there is a unique value \f$b\f$ such that -\f$\cP\f$ saturates the equality \f$( \mathrm{expr} = b )\f$; -in this case the frequency is \f$0\f$ and the value returned is \f$b\f$. +defined if and only if there is a unique value \f$c\f$ such that +\f$\cP\f$ saturates the equality \f$( \mathrm{expr} = c )\f$; +in this case the frequency is \f$0\f$ and the value returned is \f$c\f$. \subsection Grid_Time_Elapse Time-Elapse Operator

1 0

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 23 Mar '10

23 Mar '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cf2b4f20ebd8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 14:11:30 2010 +0100 PIP_Solution_Node::Tableau: optimize is_better_pivot() method for sparse matrices. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e4dfda7d485… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:55:32 2010 +0100 PIP_Solution_Node::Tableau: simplify code in scale(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=497150235901… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:49:03 2010 +0100 PIP_Tree.cc: use PPL_DIRTY_TEMP_COEFFICIENT in compatibility_check_find_pivot(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b24c684cdc51… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:46:29 2010 +0100 PIP_Tree.cc: compare signs before computing and comparing actual values, in compatibility_check_find_pivot(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=abd61b2c9f60… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:42:42 2010 +0100 PIP_Tree.cc: little optimizations in compatibility_check_find_pivot(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4491a380bf5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:34:14 2010 +0100 PIP_Tree.cc: don't compute the sign of always-positive coefficients, in compatibility_check_find_pivot_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c1078ddc5e23… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:28:56 2010 +0100 PIP_Tree.cc: don't compute the sign of always-positive coefficients, in compatibility_check_find_pivot_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8181979ac0f5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:25:22 2010 +0100 PIP_Tree.cc: use const_iterator instead of iterator in compatibility_check_find_pivot_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ded1053dc79e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:21:31 2010 +0100 PIP_Tree.cc: compare signs before computing and comparing actual values, in find_lexico_minimum_column_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f916a1a97a5c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:14:16 2010 +0100 PIP_Tree.cc: little optimization in find_lexico_minimum_column_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=85e0dbf07d2d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:11:25 2010 +0100 PIP_Tree.cc: remove unreachable code paths from find_lexico_minimum_column_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=80f3e3f8058e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 13:05:58 2010 +0100 PIP_Tree.cc: use const_iterator instead of iterator in find_lexico_minimum_column_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=47ce3d8281e9… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 12:09:23 2010 +0100 PIP_Tree.cc: little optimization in find_lexico_minimum_column_in_set(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bc885cfd1161… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 12:03:58 2010 +0100 PIP_Tree.cc: optimize column_lower() for sparse matrices.

1 0

[GIT] ppl/ppl(master): Fixed ill-positioned \f$.
by Roberto Bagnara 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 0b97d0055b7b169b8e958f87a6f1fe03f4b44b85 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0b97d0055b7b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Mar 23 17:06:04 2010 +0400 Fixed ill-positioned \f$. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 6725233..a0f8782 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2199,7 +2199,7 @@ affine expression \f$\mathrm{rhs}\f$. \subsection Grid_Frequency Frequency Operator Let \f$\cL \in \Gset_n\f$ be any non-empty grid and -\f$\mathrm{expr} = \bigl(\langle \vect{a}, \vect{x} \rangle + b\f$\bigr) +\f$\mathrm{expr} = \bigl(\langle \vect{a}, \vect{x} \rangle + b\bigr)\f$ be a linear expression. Then if, for some \f$b, f \in \Rset\f$, all the points in \f$\cL\f$ satisfy the congruence \f$\cg = ( \mathrm{expr} \equiv_f b )\f$, then the maximum

1 0

[GIT] ppl/ppl(master): Added interface code for wrap_assign().
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 2c22a25b340549e57e511f8961204ed546da541a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2c22a25b3405… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 11:08:20 2010 +0000 Added interface code for wrap_assign(). --- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 44 ++++++++++++++++- .../OCaml/ppl_interface_generator_ocaml_ml_code.m4 | 13 +++++ .../ppl_interface_generator_ocaml_mli_code.m4 | 9 +++ ...terface_generator_ocaml_procedure_generators.m4 | 1 + interfaces/OCaml/ppl_ocaml_common.cc | 53 ++++++++++++++++++++ interfaces/OCaml/ppl_ocaml_common.defs.hh | 9 +++ interfaces/OCaml/ppl_ocaml_globals.ml | 13 +++++ interfaces/OCaml/ppl_ocaml_globals.mli | 13 +++++ 8 files changed, 154 insertions(+), 1 deletions(-) diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 index 3900367..5ec23cd 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 @@ -625,7 +625,6 @@ CATCH_ALL ') - m4_define(`ppl_@CLASS@_widening_assign_with_tokens_code', `dnl extern "C" @@ -1325,3 +1324,46 @@ CAMLprim value CATCH_ALL ') + +m4_define(`ppl_@CLASS@_wrap_assign_code', +`dnl +extern "C" +CAMLprim value +ppl_@CLASS@_wrap_assign_native + (value ph, value caml_vset, value width, value rep, value oflow, + value cs, value complexity, value wrap_ind) try { + CAMLparam5(ph, caml_vset, width, rep, oflow); + CAMLxparam3(cs, complexity, wrap_ind); + @CPP_CLASS@& pph = *p_@CLASS@_val(ph); + Variables_Set ppl_vset; + if (Int_val(caml_vset) == 0) + CAMLreturn(Val_unit); + while (true) { + ppl_vset.insert(Int_val(Field(caml_vset, 0))); + if (Int_val(Field(caml_vset, 1)) == 0) + break; + caml_vset = Field(caml_vset, 1); + } + build_ppl_bounded_integer_type_representation(rep); + build_ppl_bounded_integer_type_overflow(oflow); + Constraint_System ppl_cs = build_ppl_Constraint_System(cs); + unsigned ppl_complexity = value_to_unsigned<unsigned>(complexity); + bool ppl_wrap_ind = Int_val(wrap_ind); + pph.wrap_assign(ppl_vset, + build_ppl_bounded_integer_type_width(width), + build_ppl_bounded_integer_type_representation(rep), + build_ppl_bounded_integer_type_overflow(oflow), + &ppl_cs, ppl_complexity, ppl_wrap_ind); + CAMLreturn(Val_unit); +} +CATCH_ALL + +CAMLprim value +ppl_@CLASS@_wrap_assign_bytecode(value * argv, int) +{ + return ppl_@CLASS@_wrap_assign_native(argv[0], argv[1], argv[2], argv[3], + argv[4], argv[5], argv[6], argv[7]); +} + +') + diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 index 0642842..aa3fd70 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 @@ -593,3 +593,16 @@ external ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2: = "ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2" ') + +m4_define(`ppl_@CLASS@_wrap_assign_code', +`dnl +external ppl_@CLASS@_wrap_assign: @!CLASS@ + -> bounded_integer_type_width + -> bounded_integer_type_representation + -> bounded_integer_type_overflow + -> constraint_system + -> int list -> int -> int -> unit + = "ppl_@CLASS@_wrap_assign_bytecode" + "ppl_@CLASS@_wrap_assign_native" + +') diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 index acb05a4..6f6125a 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 @@ -515,3 +515,12 @@ val ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2: @!CLASS@ -> @!CLASS@ -> polyhedron ') + +val ppl_@CLASS@_wrap_assign: @!CLASS@ + -> bounded_integer_type_width + -> bounded_integer_type_representation + -> bounded_integer_type_overflow + -> constraint_system + -> int list -> int -> int -> unit + +') diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_procedure_generators.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_procedure_generators.m4 index 8b8ff38..fad79c8 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_procedure_generators.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_procedure_generators.m4 @@ -43,6 +43,7 @@ dnl m4_define(`m4_procedure_list', `m4_echo_unquoted(ppl_new_@CLASS@_iterator +pointset_powerset, `m4_common_procedure_list', +ppl_@CLASS@_wrap_assign +simple, ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ +simple, ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ +simple, ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ +simple, diff --git a/interfaces/OCaml/ppl_ocaml_common.cc b/interfaces/OCaml/ppl_ocaml_common.cc index 8592046..ca1a1ef 100644 --- a/interfaces/OCaml/ppl_ocaml_common.cc +++ b/interfaces/OCaml/ppl_ocaml_common.cc @@ -209,6 +209,59 @@ build_ppl_relsym(value caml_relsym) { } } +Bounded_Integer_Type_Width +build_ppl_bounded_integer_type_width(value caml_width) { + assert(Is_long(caml_width)); + switch (Int_val(caml_width)) { + case 0: + return BITS_8; + case 1: + return BITS_16; + case 2: + return BITS_32; + case 3: + return BITS_64; + case 4: + return BITS_128; + default: + // We should not be here! + throw std::runtime_error("PPL OCaml interface internal error\n:" + "build_ppl_bounded_integer_type_width(width)"); + } +} + +Bounded_Integer_Type_Representation +build_ppl_bounded_integer_type_representation(value caml_rep) { + assert(Is_long(caml_rep)); + switch (Int_val(caml_rep)) { + case 0: + return UNSIGNED; + case 1: + return SIGNED_2_COMPLEMENT; + default: + // We should not be here! + throw std::runtime_error("PPL OCaml interface internal error\n:" + "build_ppl_bounded_integer_type_representation(rep)"); + } +} + +Bounded_Integer_Type_Overflow +build_ppl_bounded_integer_type_overflow(value caml_oflow) { + assert(Is_long(caml_oflow)); + switch (Int_val(caml_oflow)) { + case 0: + return OVERFLOW_WRAPS; + case 1: + return OVERFLOW_UNDEFINED; + case 2: + return OVERFLOW_IMPOSSIBLE; + default: + // We should not be here! + throw std::runtime_error("PPL OCaml interface internal error\n:" + "build_ppl_bounded_integer_type_overflow(oflow)"); + } +} + Optimization_Mode build_ppl_opt_mode(value caml_opt_mode) { assert(Is_long(caml_opt_mode)); diff --git a/interfaces/OCaml/ppl_ocaml_common.defs.hh b/interfaces/OCaml/ppl_ocaml_common.defs.hh index 21e64f9..ee31a6f 100644 --- a/interfaces/OCaml/ppl_ocaml_common.defs.hh +++ b/interfaces/OCaml/ppl_ocaml_common.defs.hh @@ -71,6 +71,15 @@ build_ppl_Complexity_Class(value cc); Relation_Symbol build_ppl_relsym(value caml_relsym); +Bounded_Integer_Type_Overflow +build_ppl_bounded_integer_type_overflow(value caml_oflow); + +Bounded_Integer_Type_Representation +build_ppl_bounded_integer_type_representation(value caml_rep); + +Bounded_Integer_Type_Width +build_ppl_bounded_integer_type_width(value caml_width); + Coefficient build_ppl_Coefficient(value coeff); diff --git a/interfaces/OCaml/ppl_ocaml_globals.ml b/interfaces/OCaml/ppl_ocaml_globals.ml index cd263d5..9868e7b 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.ml +++ b/interfaces/OCaml/ppl_ocaml_globals.ml @@ -102,6 +102,19 @@ type congruence_system = linear_congruence list type relation_symbol = Less_Than_RS | Less_Or_Equal_RS | Equal_RS | Greater_Than_RS | Greater_Or_Equal_RS +type bounded_integer_type_overflow = Overflow_Wraps + | Overflow_Undefined + | Overflow_Impossible + +type bounded_integer_type_representation = Unsigned + | Signed_2_Complement + +type bounded_integer_type_width = Bits_8 + | Bits_16 + | Bits_32 + | Bits_64 + | Bits_128 + type complexity_class = Polynomial_Complexity | Simplex_Complexity | Any_Complexity diff --git a/interfaces/OCaml/ppl_ocaml_globals.mli b/interfaces/OCaml/ppl_ocaml_globals.mli index f806f0d..e0d9c69 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.mli +++ b/interfaces/OCaml/ppl_ocaml_globals.mli @@ -88,6 +88,19 @@ type congruence_system = linear_congruence list type relation_symbol = Less_Than_RS | Less_Or_Equal_RS | Equal_RS | Greater_Than_RS | Greater_Or_Equal_RS +type bounded_integer_type_overflow = Overflow_Wraps + | Overflow_Undefined + | Overflow_Impossible + +type bounded_integer_type_representation = Unsigned + | Signed_2_Complement + +type bounded_integer_type_width = Bits_8 + | Bits_16 + | Bits_32 + | Bits_64 + | Bits_128 + type complexity_class = Polynomial_Complexity | Simplex_Complexity | Any_Complexity

1 0

[GIT] ppl/ppl(sparse_matrices): MIP_Problem: fix regression in process_pending_constraints(), introduced in commit beb4f18.
by Marco Poletti 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: 37d46822458f23ac7bb7ef5843d6a62f386978c4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=37d46822458f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 11:05:52 2010 +0100 MIP_Problem: fix regression in process_pending_constraints(), introduced in commit beb4f18. --- src/MIP_Problem.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index 6c97648..8f73dea 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -818,8 +818,8 @@ PPL::MIP_Problem::process_pending_constraints() { // linear_combine() invalidates itr and itr_end. itr = tableau_k.lower_bound(j->first); itr_end = tableau_k.end(); - } - ++itr; + } else + ++itr; ++j; } }

1 0

[GIT] ppl/ppl(sparse_matrices): Merge branch 'master' into sparse_matrices
by Roberto Bagnara 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: c19c3efac649aea0d15078e3ee3b13a5caf2d8eb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c19c3efac649… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Mar 23 10:28:00 2010 +0100 Merge branch 'master' into sparse_matrices ---

1 0

[GIT] ppl/ppl(sparse_matrices): Fixed the expected result for test04().
by Roberto Bagnara 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: f491feddb41d60b7ecef4c297ce9880bc245b953 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f491feddb41d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Mar 23 10:26:43 2010 +0100 Fixed the expected result for test04(). --- tests/Polyhedron/termination1.cc | 7 +------ 1 files changed, 1 insertions(+), 6 deletions(-) diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index 90ca22b..b17af5b 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -121,16 +121,11 @@ test04() { Variable mu2(1); Variable mu0(2); NNC_Polyhedron known_result(3); - known_result.add_constraint(mu1 - mu2 >= 1); - known_result.add_constraint(mu0 + 2*mu1 >= 0); + known_result.add_constraint(mu1 - mu2 > 0); known_result.add_constraint(mu2 >= 0); print_constraints(known_result, "*** known_result ***"); - if (known_result.contains(mu_space)) - std::cout << "->" << endl; - if (mu_space.contains(known_result)) - std::cout << "<-" << endl; return known_result == mu_space; }

1 0