October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Parameter compatibility check now applies a revised dual simplex method.
by François Galea 20 Oct '09

20 Oct '09

Module: ppl/ppl Branch: pip Commit: 9f62791f13a0de4decf334ca5b3d604207bac6f7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9f62791f13a0… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 20 18:18:19 2009 +0200 Parameter compatibility check now applies a revised dual simplex method. --- src/PIP_Tree.cc | 48 +++++++++++++++++++++++++++++++++++++++++------- src/PIP_Tree.defs.hh | 8 ++++---- 2 files changed, 45 insertions(+), 11 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index fff5599..355f8f1 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -688,14 +688,23 @@ bool PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { Matrix s(ctx); s.add_row(cnst); - dimension_type i, i_, j, k, j_, j__; + dimension_type i, i_, j, k, j_, j__, var_i, var_j; dimension_type num_rows = s.num_rows(); dimension_type num_cols = s.num_columns(); + dimension_type num_vars = num_cols-1; + const dimension_type n_a_d = not_a_dimension(); std::vector<Coefficient> scaling(num_rows, 1); PPL_DIRTY_TEMP_COEFFICIENT(sij); PPL_DIRTY_TEMP_COEFFICIENT(mult); PPL_DIRTY_TEMP_COEFFICIENT(gcd); PPL_DIRTY_TEMP_COEFFICIENT(scale_factor); + PPL_DIRTY_TEMP_COEFFICIENT(scaling_i); + std::vector<dimension_type> mapping; + std::vector<bool> basis(num_vars, true); + for (j=1; j<=num_vars; ++j) + mapping.push_back(j); + Row p(num_cols, compute_capacity(num_cols, Matrix::max_num_columns()), + Row::Flags()); /* Perform simplex pivots on the context until we find an empty solution * or an optimum */ @@ -726,9 +735,37 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { // No negative RHS: optimum found return true; } + // Now we have a positive s[i][j] pivot - const Row& p = s[i]; + var_j = n_a_d; + var_i = n_a_d; + for (j_=0; j_<num_vars; ++j_) { + if (basis[j_]) { + if (mapping[j_] == j) + var_j = j_; + } else { + if (mapping[j_] == i) + var_i = j_; + } + } + /* update basis */ + if (var_j != n_a_d) { + basis[var_j] = false; + mapping[var_j] = i; + } + if (var_i != n_a_d) { + basis[var_i] = true; + mapping[var_i] = j; + } + + /* create the identity matrix row corresponding to basic variable j */ + for (j_=0; j_<num_cols; ++j_) + p[j_]=0; + p[j] = 1; + p.swap(s[i]); sij = p[j]; + scaling_i = scaling[i]; + scaling[i] = 1; // Perform a pivot operation on the matrix for (j_=0; j_<num_cols; ++j_) { @@ -739,8 +776,6 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { // if element j of pivot row is zero, nothing to do for this column continue; for (k=0; k<num_rows; ++k) { - if (k == i) - continue; Row& row = s[k]; mult = row[j] * sij_; if (mult % sij != 0) { @@ -754,14 +789,13 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { } row[j_] -= mult / sij; } - s[i][j_] = 0; } - if (sij != scaling[i]) { + if (sij != scaling_i) { // Update column only if pivot != 1 for (k=0; k<num_rows; ++k) { Row& row = s[k]; Coefficient& skj = row[j]; - mult = skj*scaling[i]; + mult = skj*scaling_i; if (mult % sij != 0) { // as above, we must perform row scaling gcd_assign(gcd, mult, sij); diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 4141818..c2a8186 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -331,10 +331,10 @@ private: Checks whether a constraint is compatible with a context, ie. does not make the context empty. - The algorithm consists in performing simplex pivots on a Matrix consisting - in the original matrix with the constraint inserted. If the simplex - terminates with a solution, then the restrained context is not empty. - Otherwise, it is. + The method consists in applying the revised dual simplex algorithm on a + Matrix consisting in the original matrix with the constraint inserted. If + the simplex terminates with a feasible (optimal) solution, then the + restrained context is not empty. Otherwise, it is. */ static bool compatibility_check(const Matrix &ctx, const Row &cnst);

1 0

[GIT] ppl/ppl(pip): Added display of computed row parameter signs in noisy PIP mode.
by François Galea 20 Oct '09

20 Oct '09

Module: ppl/ppl Branch: pip Commit: 5050775875b58d48e5a74f172767149a81068b8a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5050775875b5… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 20 16:52:33 2009 +0200 Added display of computed row parameter signs in noisy PIP mode. --- src/PIP_Tree.cc | 7 +++++++ 1 files changed, 7 insertions(+), 0 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index f0ade33..fff5599 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -988,6 +988,13 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, } } +#ifdef NOISY_PIP + std::cout << "sign ="; + for (i=0; i<sign.size(); ++i) + std::cout << " " << "?0+-*"[sign[i]]; + std::cout << std::endl; +#endif + /* If we have found a row i_ with negative parameters : Either the problem is empty, or a pivoting step is required */

1 0

[GIT] ppl/ppl(pip): Added new test, which should return an empty solution.
by François Galea 20 Oct '09

20 Oct '09

Module: ppl/ppl Branch: pip Commit: 27de41218171b82dbbb767ccb88f37bf4c202064 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=27de41218171… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 20 16:10:26 2009 +0200 Added new test, which should return an empty solution. --- tests/PIP_Problem/pipproblem1.cc | 23 +++++++++++++++++++++++ 1 files changed, 23 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 5b436fe..65b58aa 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -229,6 +229,28 @@ test05() { return ok; } +bool +test06() { + Variable i(0); + Variable n(1); + Variables_Set params(n); + + Constraint_System cs; + cs.insert(4*i + 2*n >= 1); + cs.insert(4*i + 2*n <= 1); + + 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(); + display_solution(solution, params, Variables_Set(i), + cs.space_dimension()); + } + + return ok; +} + } // namespace BEGIN_MAIN @@ -237,4 +259,5 @@ BEGIN_MAIN DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); + DO_TEST(test06); END_MAIN

1 0

[GIT] ppl/ppl(pip): Always stop compatibility check at first negative row.
by François Galea 20 Oct '09

20 Oct '09

Module: ppl/ppl Branch: pip Commit: 5d5b77d7bd5b2faa5f6966fb43172bbcbac80cba URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d5b77d7bd5b… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 20 11:36:57 2009 +0200 Always stop compatibility check at first negative row. --- src/PIP_Tree.cc | 48 +++++++++++++++++++++++++++++------------------- 1 files changed, 29 insertions(+), 19 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index ff42e3b..f0ade33 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -688,11 +688,10 @@ bool PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { Matrix s(ctx); s.add_row(cnst); - dimension_type i, j, k, j_, j__; + dimension_type i, i_, j, k, j_, j__; dimension_type num_rows = s.num_rows(); dimension_type num_cols = s.num_columns(); std::vector<Coefficient> scaling(num_rows, 1); - bool result = false; PPL_DIRTY_TEMP_COEFFICIENT(sij); PPL_DIRTY_TEMP_COEFFICIENT(mult); PPL_DIRTY_TEMP_COEFFICIENT(gcd); @@ -702,26 +701,36 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { * or an optimum */ for (;;) { // Look for a negative RHS (=constant term, stored in matrix column 0) - i = 0; - while (i<num_rows && s[i][0] >= 0) - i++; - if (i == num_rows) { + i = num_rows; + j = 0; + for (i_=0; i_<num_rows; ++i_) { + const Row& rs = s[i_]; + if (rs[0] < 0) { + if (i == num_rows) + i = i_; + for (j_=1; j_<num_cols; ++j_) { + if (rs[j_] > 0) { + if(j == 0) + j = j_; + break; + } + } + if (j_==num_cols) { + // No positive pivot candidate: empty problem + return false; + } + } + } + + if (j == 0) { // No negative RHS: optimum found - result = true; - break; + return true; } - // Find a positive m[i][j] pivot - j = 1; + // Now we have a positive s[i][j] pivot const Row& p = s[i]; - while (j<num_cols && p[j] <= 0) - j++; - if (j == num_cols) { - // No positive pivot candidate: empty problem - result = false; - break; - } - // Perform a pivot operation on the matrix sij = p[j]; + + // Perform a pivot operation on the matrix for (j_=0; j_<num_cols; ++j_) { if (j_ == j) continue; @@ -767,7 +776,8 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { } } - return result; + // This point is never reached + return false; } void

1 0

[GIT] ppl/ppl(floating_point): Documentation updates.
by Fabio Biselli 20 Oct '09

20 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 391db98125e29e306ee1baf3342b82d6664f9f54 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=391db98125e2… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Oct 20 15:23:59 2009 +0200 Documentation updates. Fixed parenthesis in ppl.sty as suggested. Fixed few typos. --- doc/definitions.dox | 37 ++++++++-------- doc/ppl.sty | 5 +- src/Difference_Floating_Point_Expression.defs.hh | 24 +++++------ src/Division_Floating_Point_Expression.defs.hh | 35 +++++++-------- src/Floating_Point_Expression.defs.hh | 13 +++--- ...ultiplication_Floating_Point_Expression.defs.hh | 45 ++++++++----------- src/Opposite_Floating_Point_Expression.defs.hh | 12 +++--- src/Sum_Floating_Point_Expression.defs.hh | 30 +++++++------- src/Variable_Floating_Point_Expression.defs.hh | 7 +-- 9 files changed, 99 insertions(+), 109 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=391db981…

1 0

SWI Prolog support added to the Debian package
by Israel Herraiz 18 Oct '09

18 Oct '09

Hi all, a new version of the PPL Debian package has been uploaded to the FTP archive, including SWI Prolog support (new package called libppl-swi). The details are here: http://packages.qa.debian.org/p/ppl/news/20091018T181815Z.html Cheers, Israel

2 1

[GIT] ppl/ppl(floating_point): Added FIXME notes.
by Roberto Amadini 17 Oct '09

17 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 6da25c9734d4f9bb3eebd7d23ec85f14e2d6fe18 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6da25c9734d4… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Oct 17 12:43:04 2009 +0200 Added FIXME notes. --- tests/Floating_Point_Expression/digitalfilters1.cc | 3 +++ 1 files changed, 3 insertions(+), 0 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 8a40c4b..7e19652 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -512,6 +512,7 @@ test05() { std::numeric_limits<ANALYZER_FP_FORMAT>::max(); max_analyzer = std::min(max_analyzer, max_analyzed); assign_r(M, max_analyzer, ROUND_DOWN); + //FIXME: We could take any value of M >= 145. cs.insert(Y <= M); cs.insert(Y >= -M); FP_BD_Shape bd_wid(bd); @@ -633,6 +634,7 @@ test06() { // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf. // For a more precise analysis, it is better to insert the // constraints Y <= N and Y >= -N, where N = M / 2. + // However, we could take any value of N >= 145. cs.insert(Y <= N); cs.insert(Y >= -N); FP_Octagonal_Shape oc_wid(oc); @@ -750,6 +752,7 @@ test07() { std::numeric_limits<ANALYZER_FP_FORMAT>::max(); max_analyzer = std::min(max_analyzer, max_analyzed); assign_r(M, max_analyzer, ROUND_DOWN); + //FIXME: We could take any value of M >= 136. cs.insert(Y <= M); cs.insert(Y >= -M); NNC_Polyhedron ph_wid(ph);

1 0

[GIT] ppl/ppl(floating_point): Added a test on BD_Shape, improved a test on Polyhedra.
by Roberto Amadini 16 Oct '09

16 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 8801eb01b1d065c9aa0790d4292edb467a642e2c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8801eb01b1d0… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Oct 16 18:23:45 2009 +0200 Added a test on BD_Shape, improved a test on Polyhedra. --- tests/Floating_Point_Expression/digitalfilters1.cc | 127 ++++++++++++++++++- 1 files changed, 120 insertions(+), 7 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 4dabd47..8a40c4b 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -410,7 +410,7 @@ test04() { return y.is_bounded(); } -// Tests rate limiter using octagons abstract domain and +// Tests rate limiter using bounded differences abstract domain and // linearization of floating point expressions. bool test05() { @@ -427,6 +427,121 @@ test05() { FP_Interval_Abstract_Store abstract_store(5); FP_Linear_Form_Abstract_Store lf_abstract_store; + FP_BD_Shape bd(abstract_store); + FP_Interval y(0); + FP_Interval y_begin(1); + FP_BD_Shape bd_begin; + Con_FP_Expression con_y(0, 0); + FP_Linear_Form lx; + FP_Linear_Form ly; + FP_Linear_Form lr; + FP_Linear_Form lk; + + // Y = 0; + con_y.linearize(abstract_store, lf_abstract_store, lk); + bd.affine_image(Y, lk); + + for(unsigned short n = 0; y_begin != y; ++n) { + + nout << "*** n = " << n << " ***" << endl; + bd_begin = bd; + y_begin = y; + + Con_FP_Expression con_x(-128, 128); + con_x.linearize(abstract_store, lf_abstract_store, lk); + bd.affine_image(X, lk); + + Con_FP_Expression con_d(0, 16); + con_d.linearize(abstract_store, lf_abstract_store, lk); + bd.affine_image(D, lk); + + Var_FP_Expression var_y(2); + var_y.linearize(abstract_store, lf_abstract_store, ly); + bd.affine_image(S, ly); + + Var_FP_Expression* px = new Var_FP_Expression(0); + Var_FP_Expression* ps = new Var_FP_Expression(3); + Dif_FP_Expression x_dif_s(px, ps); + x_dif_s.linearize(abstract_store, lf_abstract_store, lr); + bd.affine_image(R, lr); + + Var_FP_Expression var_x(0); + var_x.linearize(abstract_store, lf_abstract_store, lx); + bd.affine_image(Y, lx); + + // if (R <= -D) Y = S - D; + FP_BD_Shape bd_then(bd); + bd_then.refine_with_linear_form_inequality(lr, -lk); + + Var_FP_Expression* pd = new Var_FP_Expression(1); + Var_FP_Expression* ps2 = new Var_FP_Expression(3); + Dif_FP_Expression s_dif_d(ps2, pd); + s_dif_d.linearize(abstract_store, lf_abstract_store, ly); + bd_then.affine_image(Y, ly); + + bd.refine_with_linear_form_inequality(-lk, lr); + + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd) , + "*** if (R <= -D) Y = S - D; ***"); + + // if (R >= D) Y = S + D; + bd_then = bd; + bd_then.refine_with_linear_form_inequality(lk, lr); + + Var_FP_Expression* pd1 = new Var_FP_Expression(1); + Var_FP_Expression* ps3 = new Var_FP_Expression(3); + Sum_FP_Expression s_sum_d(ps3, pd1); + s_sum_d.linearize(abstract_store, lf_abstract_store, ly); + bd_then.affine_image(Y, ly); + + bd.refine_with_linear_form_inequality(lr, lk); + + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd), "*** if (R >= D) Y = S + D; ***"); + + bd.upper_bound_assign(bd_begin); + Constraint_System cs; + PPL_DIRTY_TEMP_COEFFICIENT(M); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); + FP_BD_Shape bd_wid(bd); + bd_wid.limited_BHMZ05_extrapolation_assign(bd_begin, cs); + Box<FP_Interval> box(bd_wid); + print_constraints(box, "*** after widening ***"); + y = box.get_interval(Y); + } + + nout << "*** Y in " << y << " ***" << endl; + return y.is_bounded(); +} + +// Tests rate limiter using octagons abstract domain and +// linearization of floating point expressions. +bool +test06() { + // Input signal. + Variable X(0); + // Maximum allowed for |R|. + Variable D(1); + // Output signal. + Variable Y(2); + // Last output. + Variable S(3); + // Actual rate. + Variable R(4); + + FP_Interval_Abstract_Store abstract_store(5); + FP_Linear_Form_Abstract_Store lf_abstract_store; FP_Octagonal_Shape oc(abstract_store); FP_Interval y(0); FP_Interval y_begin(1); @@ -534,7 +649,7 @@ test05() { // Tests rate limiter using polyhedra abstract domain and // linearization of floating point expressions. bool -test06() { +test07() { // Input signal. Variable X(0); // Maximum allowed for |R|. @@ -577,17 +692,14 @@ test06() { con_d.linearize(abstract_store, lf_abstract_store, lk); ph.affine_image(D, lk); Var_FP_Expression var_y(2); - abstract_store = Box<FP_Interval>(ph); var_y.linearize(abstract_store, lf_abstract_store, ly); ph.affine_image(S, ly); Var_FP_Expression* px = new Var_FP_Expression(0); Var_FP_Expression* ps = new Var_FP_Expression(3); Dif_FP_Expression x_dif_s(px, ps); - abstract_store = Box<FP_Interval>(ph); x_dif_s.linearize(abstract_store, lf_abstract_store, lr); ph.affine_image(R, lr); Var_FP_Expression var_x(0); - abstract_store = Box<FP_Interval>(ph); var_x.linearize(abstract_store, lf_abstract_store, lx); ph.affine_image(Y, lx); @@ -653,11 +765,12 @@ test06() { } // namespace -BEGIN_MAIN /* +BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); - DO_TEST(test04); */ + DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added BASE field to floating point struct.
by Fabio Biselli 16 Oct '09

16 Oct '09

Module: ppl/ppl Branch: floating_point Commit: d8d6e899f5cac4d00d37c1ebfbeeb199cbbbb1bb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d8d6e899f5ca… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Fri Oct 16 11:53:37 2009 +0200 Added BASE field to floating point struct. Modified absolute/relative error definition using FP_Format::BASE. Modified tests using FP_Format::BASE. --- src/Float.defs.hh | 9 +++++++++ src/Floating_Point_Expression.defs.hh | 17 +++++++++++------ src/Floating_Point_Expression.templates.hh | 11 +++++++---- tests/Floating_Point_Expression/Makefile.am | 3 +-- .../floatingpointexpr1.cc | 10 +++++----- 5 files changed, 33 insertions(+), 17 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index f0eb5f8..2030f55 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -49,6 +49,7 @@ struct float_ieee754_half { static const uint16_t NEG_INF = 0x7c00; static const uint16_t POS_ZERO = 0x0000; static const uint16_t NEG_ZERO = 0x8000; + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 5; static const unsigned int MANTISSA_BITS = 10; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; @@ -80,6 +81,7 @@ struct float_ieee754_single { static const uint32_t NEG_INF = 0xff800000; static const uint32_t POS_ZERO = 0x00000000; static const uint32_t NEG_ZERO = 0x80000000; + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 8; static const unsigned int MANTISSA_BITS = 23; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; @@ -124,6 +126,7 @@ struct float_ieee754_double { static const uint32_t LSP_INF = 0; static const uint32_t LSP_ZERO = 0; static const uint32_t LSP_MAX = 0xffffffff; + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 11; static const unsigned int MANTISSA_BITS = 52; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; @@ -154,6 +157,7 @@ struct float_ibm_single { static const uint32_t NEG_INF = 0xff000000; static const uint32_t POS_ZERO = 0x00000000; static const uint32_t NEG_ZERO = 0x80000000; + static const unsigned int BASE = 16; static const unsigned int EXPONENT_BITS = 7; static const unsigned int MANTISSA_BITS = 24; static const int EXPONENT_BIAS = 64; @@ -177,6 +181,9 @@ struct float_ibm_single { #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) struct float_ibm_double { + // FIXME: BASE must be 16, 16^56 should return an overflow + // and absolute/relative error are not sound. + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 7; static const unsigned int MANTISSA_BITS = 56; static const int EXPONENT_BIAS = 64; @@ -203,6 +210,7 @@ struct float_intel_double_extended { static const uint64_t LSP_ZERO = 0; static const uint64_t LSP_DMAX = 0x7fffffffffffffffULL; static const uint64_t LSP_NMAX = 0xffffffffffffffffULL; + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 15; static const unsigned int MANTISSA_BITS = 63; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; @@ -241,6 +249,7 @@ struct float_ieee754_quad { static const uint64_t LSP_INF = 0; static const uint64_t LSP_ZERO = 0; static const uint64_t LSP_MAX = 0xffffffffffffffffULL; + static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 15; static const unsigned int MANTISSA_BITS = 112; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index fb94f2d..a66190d 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -190,12 +190,17 @@ public: template <typename FP_Interval_Type, typename FP_Format> typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type -Floating_Point_Expression<FP_Interval_Type, FP_Format>::absolute_error = - std::max( - static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type> - (pow(2, static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(1) - FP_Format::EXPONENT_BIAS - FP_Format::MANTISSA_BITS)) - , - std::numeric_limits<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>::denorm_min()); +Floating_Point_Expression<FP_Interval_Type, FP_Format>::absolute_error = +std::max( + static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format> + ::boundary_type>(pow(FP_Format::BASE, static_cast<typename + Floating_Point_Expression<FP_Interval_Type, FP_Format> + ::boundary_type>(1) - FP_Format + ::EXPONENT_BIAS - FP_Format + ::MANTISSA_BITS)), + std::numeric_limits<typename + Floating_Point_Expression<FP_Interval_Type, FP_Format> + ::boundary_type>::denorm_min()); } // namespace Parma_Polyhedra_Library diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 0343bff..11168e0 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -35,9 +35,12 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> ::relative_error(const FP_Linear_Form& lf, FP_Linear_Form& result) { /* FIXME: here we assume that boundary_type can represent (2)^(-FP_Format::MANTISSA_BITS) precisely. */ - FP_Interval_Type error_propagator(-pow(2, -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(FP_Format::MANTISSA_BITS))); - // FIXME: this may be incorrect for some policies. - error_propagator.join_assign(FP_Interval_Type(pow(2, -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(FP_Format::MANTISSA_BITS)))); + FP_Interval_Type error_propagator(-pow(FP_Format::BASE, + -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format> + ::boundary_type>(FP_Format::MANTISSA_BITS))); + error_propagator.join_assign(FP_Interval_Type(pow(FP_Format::BASE, + -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format> + ::boundary_type>(FP_Format::MANTISSA_BITS)))); // Handle the inhomogeneous term. const FP_Interval_Type* current_term = &lf.inhomogeneous_term(); @@ -52,7 +55,7 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> for (dimension_type i = 0; i < dimension; ++i) { current_term = &lf.coefficient(Variable(i)); current_multiplier = FP_Interval_Type(std::max(abs(current_term->lower()), - abs(current_term->upper()))); + abs(current_term->upper()))); current_result_term = FP_Linear_Form(Variable(i)); current_result_term *= current_multiplier; current_result_term *= error_propagator; diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 9755e4b..7096075 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -51,9 +51,8 @@ $(top_builddir)/src/libppl.la \ @extra_libraries@ ORIGINAL_TESTS = \ -digitalfilters1 +digitalfilters1 -#digitalfilters1 #bdshape2 \ #bdshape1 \ #floatingpointexpr1 \ diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index c4322eb..c8facf4 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -101,7 +101,7 @@ test04() { Variable A(0); Variable B(1); FP_Linear_Form known_result = FP_Linear_Form(A); - ANALYZER_FP_FORMAT exp = pow(2, + ANALYZER_FP_FORMAT exp = pow(ANALYZED_FP_FORMAT::BASE, -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)); tmp = FP_Interval(1); tmp -= exp; @@ -135,7 +135,7 @@ test05() { Variable A(0); Variable B(1); FP_Linear_Form known_result = FP_Linear_Form(A); - ANALYZER_FP_FORMAT exp = pow(2, + ANALYZER_FP_FORMAT exp = pow(ANALYZED_FP_FORMAT::BASE, -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)); tmp = FP_Interval(1); tmp -= exp; @@ -169,7 +169,7 @@ test06() { tmp = FP_Interval(-FP_Expression::absolute_error); tmp.join_assign(FP_Expression::absolute_error); - ANALYZER_FP_FORMAT exp = pow(2, + ANALYZER_FP_FORMAT exp = pow(ANALYZED_FP_FORMAT::BASE, -static_cast<ANALYZER_FP_FORMAT>((ANALYZED_FP_FORMAT::MANTISSA_BITS-1))); FP_Interval coeff = FP_Interval(2); coeff -= exp; @@ -202,7 +202,7 @@ test07() { tmp = FP_Interval(-FP_Expression::absolute_error); tmp.join_assign(FP_Expression::absolute_error); - ANALYZER_FP_FORMAT exp = pow(2, + ANALYZER_FP_FORMAT exp = pow(ANALYZED_FP_FORMAT::BASE, -static_cast<ANALYZER_FP_FORMAT>((ANALYZED_FP_FORMAT::MANTISSA_BITS+1))); FP_Interval coeff = FP_Interval(1 / 2.0); coeff -= exp; @@ -234,7 +234,7 @@ test08() { Variable A(0); FP_Linear_Form known_result = FP_Linear_Form(A); - ANALYZER_FP_FORMAT exp = pow(2, + ANALYZER_FP_FORMAT exp = pow(ANALYZED_FP_FORMAT::BASE, -static_cast<ANALYZER_FP_FORMAT>((ANALYZED_FP_FORMAT::MANTISSA_BITS+1))); tmp = FP_Interval(-1 / 2.0); tmp -= exp;

1 0

[GIT] ppl/ppl(pip): Improved the heuristic for the choice of the deepest cut.
by François Galea 16 Oct '09

16 Oct '09

Module: ppl/ppl Branch: pip Commit: b748415bdb69719db9fc2ed07cc253d5c71759f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b748415bdb69… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Oct 16 09:58:24 2009 +0200 Improved the heuristic for the choice of the deepest cut. --- src/PIP_Tree.cc | 23 +++++++++++++++++------ 1 files changed, 17 insertions(+), 6 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 9f09443..ff42e3b 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1323,19 +1323,30 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, } else { /* The solution is non-integer. We have to generate a cut. */ - Coefficient mod; + /* Look for row which will generate the "deepest" cut */ - Coefficient score; + PPL_DIRTY_TEMP_COEFFICIENT(score); + PPL_DIRTY_TEMP_COEFFICIENT(score1); + PPL_DIRTY_TEMP_COEFFICIENT(score2); + PPL_DIRTY_TEMP_COEFFICIENT(mod); Coefficient best = 0; dimension_type best_i = 0; for (i_ = 0; i_ < num_rows; ++i_) { - const Row& row = tableau.t[i_]; - score = 0; + const Row& row_t = tableau.t[i_]; + const Row& row_s = tableau.s[i_]; + score1 = 0; for (j = 0; j < num_params; ++j) { - mod_assign(mod, row[j], d); + mod_assign(mod, row_t[j], d); + if (mod != 0) + score1 += d - mod; + } + score2 = 0; + for (j = 0; j < num_vars; ++j) { + mod_assign(mod, row_s[j], d); if (mod != 0) - score += d - mod; + score2 += d - mod; } + score = score1*score2; if (score > best) { best = score; best_i = i_;

1 0