October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Added 2 more functions for the C interface to the PIP_Problem class.
by Patricia Hill 07 Oct '09

07 Oct '09

Module: ppl/ppl Branch: pip Commit: 57c81a9ac76f4ec249259a5216f24bc3529bfc30 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=57c81a9ac76f… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Wed Oct 7 16:00:42 2009 +0100 Added 2 more functions for the C interface to the PIP_Problem class. --- interfaces/C/ppl_c_header.h | 1 + interfaces/C/ppl_c_implementation_common.cc | 16 ++++++++++++++++ .../C/ppl_c_implementation_common.inlines.hh | 2 ++ 3 files changed, 19 insertions(+), 0 deletions(-) diff --git a/interfaces/C/ppl_c_header.h b/interfaces/C/ppl_c_header.h index 1bb8c4e..070f380 100644 --- a/interfaces/C/ppl_c_header.h +++ b/interfaces/C/ppl_c_header.h @@ -694,6 +694,7 @@ PPL_TYPE_DECLARATION(MIP_Problem) towards \extref{Parma_Polyhedra_Library::PIP_Problem, PIP_Problem}. */ PPL_TYPE_DECLARATION(PIP_Problem) +PPL_TYPE_DECLARATION(PIP_Tree_Node) #undef PPL_DECLARE_PRINT_FUNCTIONS diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index 875d4cd..f5c4a38 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2220,6 +2220,22 @@ ppl_PIP_Problem_solve(ppl_const_PIP_Problem_t mip) try { CATCH_ALL int +ppl_PIP_Problem_solution(ppl_const_PIP_Problem_t pip, + ppl_const_PIP_Tree_Node_t* ppip_tree) try { + *ppip_tree = to_const(to_const(pip)->solution()); + return 0; +} +CATCH_ALL + +int +ppl_PIP_Problem_optimizing_solution(ppl_const_PIP_Problem_t pip, + ppl_const_PIP_Tree_Node_t* ppip_tree) try { + *ppip_tree = to_const(to_const(pip)->optimizing_solution()); + return 0; +} +CATCH_ALL + +int ppl_PIP_Problem_OK(ppl_const_PIP_Problem_t mip) try { return to_const(mip)->OK() ? 1 : 0; } diff --git a/interfaces/C/ppl_c_implementation_common.inlines.hh b/interfaces/C/ppl_c_implementation_common.inlines.hh index 6137b23..2065879 100644 --- a/interfaces/C/ppl_c_implementation_common.inlines.hh +++ b/interfaces/C/ppl_c_implementation_common.inlines.hh @@ -79,6 +79,8 @@ DECLARE_CONVERSIONS(MIP_Problem, MIP_Problem) DECLARE_CONVERSIONS(PIP_Problem, PIP_Problem) +DECLARE_CONVERSIONS(PIP_Tree_Node, PIP_Tree_Node) + inline Relation_Symbol relation_symbol(enum ppl_enum_Constraint_Type t) { switch (t) {

1 0

[GIT] ppl/ppl(floating_point): Fixed test05.
by Roberto Amadini 07 Oct '09

07 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 10a020c1c5d8fe8cf02dbf61555ff773706e819d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=10a020c1c5d8… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Oct 7 16:19:27 2009 +0200 Fixed test05. --- tests/Floating_Point_Expression/digitalfilters1.cc | 25 +++++++++---------- 1 files changed, 12 insertions(+), 13 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 7d2a2f1..ae586bb 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -412,7 +412,6 @@ test04() { // tests rate limiter using octagons abstract domain and // linearization of floating point expressions. -// FIXME: not pass at the moment. bool test05() { // Input signal. @@ -430,6 +429,7 @@ test05() { FP_Linear_Form_Abstract_Store lf_abstract_store; FP_Octagonal_Shape oc(abstract_store); FP_Interval y(0); + FP_Interval y_begin(1); FP_Octagonal_Shape oc_begin; Con_FP_Expression con_y(0, 0); FP_Linear_Form lx; @@ -441,10 +441,11 @@ test05() { con_y.linearize(abstract_store, lf_abstract_store, lk); oc.affine_image(Y, lk); - for(unsigned short n = 0; oc_begin != oc; ++n) { + for(unsigned short n = 0; y_begin != y; ++n) { nout << "*** n = " << n << " ***" << endl; oc_begin = oc; + y_begin = y; Con_FP_Expression con_x(-128, 128); con_x.linearize(abstract_store, lf_abstract_store, lk); @@ -520,7 +521,7 @@ test05() { } nout << "*** Y in " << y << " ***" << endl; - return y.is_bounded(); + return !y.is_bounded(); } // tests rate limiter using polyhedra abstract domain and @@ -545,6 +546,8 @@ test06() { FP_Interval tmp(0); NNC_Polyhedron ph_begin; Con_FP_Expression con_y(0, 0); + FP_Interval y(0); + FP_Interval y_begin(1); FP_Linear_Form lx; FP_Linear_Form ly; FP_Linear_Form lr; @@ -554,32 +557,28 @@ test06() { con_y.linearize(abstract_store, lf_abstract_store, lk); ph.affine_image(Y, lk); - for(unsigned short n = 0; ph_begin != ph; ++n) { + for(unsigned short n = 0; y_begin != y && y.is_bounded(); ++n) { nout << "*** n = " << n << " ***" << endl; ph_begin = ph; - + y_begin = y; // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; Con_FP_Expression con_x(-128, 128); con_x.linearize(abstract_store, lf_abstract_store, lk); ph.affine_image(X, lk); - Con_FP_Expression con_d(0, 16); 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); @@ -637,11 +636,11 @@ test06() { ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); Box<FP_Interval> box(ph); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } - nout << "*** Y in " << tmp << " ***" << endl; - return tmp.is_bounded(); + nout << "*** Y in " << y << " ***" << endl; + return !y.is_bounded(); } } // namespace @@ -651,6 +650,6 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - //DO_TEST(test05); + DO_TEST(test05); //DO_TEST(test06); END_MAIN

1 0

[GIT] ppl/ppl(pip): Added a very basic interface for C to the PIP_Problem class.
by Patricia Hill 07 Oct '09

07 Oct '09

Module: ppl/ppl Branch: pip Commit: 518bf5b2eb2c508f19b6b2a7ab78ba085afe05b9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=518bf5b2eb2c… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Wed Oct 7 14:30:38 2009 +0100 Added a very basic interface for C to the PIP_Problem class. Note this is incomplete and does not support methods with PIP_Tree. --- interfaces/C/ppl_c_header.h | 295 ++++++++++++++++++++ interfaces/C/ppl_c_implementation_common.cc | 142 ++++++++++ .../C/ppl_c_implementation_common.inlines.hh | 2 + 3 files changed, 439 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=518bf5b2…

1 0

[GIT] ppl/ppl(floating_point): Using uint16_t instead of uint32_t in float_ieee754_half.
by Fabio Biselli 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 9c35b656767f36003e45c04094861a5f06140eb8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9c35b656767f… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Oct 6 19:15:32 2009 +0200 Using uint16_t instead of uint32_t in float_ieee754_half. Extended float_ibm_single. --- src/Float.defs.hh | 34 +++++++++-- src/Float.inlines.hh | 59 ++++++++++++++++++++ tests/Floating_Point_Expression/digitalfilters1.cc | 1 + 3 files changed, 87 insertions(+), 7 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 3f65b2b..303e988 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -42,13 +42,13 @@ namespace Parma_Polyhedra_Library { #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) struct float_ieee754_half { - uint32_t word; - static const uint32_t SGN_MASK = 0x8000; - static const uint32_t EXP_MASK = 0xfc00; - static const uint32_t POS_INF = 0xfc00; - static const uint32_t NEG_INF = 0x7c00; - static const uint32_t POS_ZERO = 0x0000; - static const uint32_t NEG_ZERO = 0x8000; + uint16_t word; + static const uint16_t SGN_MASK = 0x8000; + static const uint16_t EXP_MASK = 0xfc00; + static const uint16_t POS_INF = 0xfc00; + 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 EXPONENT_BITS = 5; static const unsigned int MANTISSA_BITS = 10; static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; @@ -147,9 +147,29 @@ struct float_ieee754_double { #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) struct float_ibm_single { + uint32_t word; + static const uint32_t SGN_MASK = 0x80000000; + static const uint32_t EXP_MASK = 0x7f000000; + static const uint32_t POS_INF = 0x7f000000; + 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 EXPONENT_BITS = 7; static const unsigned int MANTISSA_BITS = 24; static const int EXPONENT_BIAS = 64; + static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; + static const int EXPONENT_MIN = -EXPONENT_MAX + 1; + static const int EXPONENT_MIN_DENORM = EXPONENT_MIN + - static_cast<int>(MANTISSA_BITS); + int is_inf() const; + int is_nan() const; + int is_zero() const; + int sign_bit() const; + void negate(); + void dec(); + void inc(); + void set_max(bool negative); + void build(bool negative, mpz_t mantissa, int exponent); }; #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index dcbe93f..9b01fa5 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -228,6 +228,65 @@ float_ieee754_double::build(bool negative, mpz_t mantissa, int exponent) { } inline int +float_ibm_single::is_inf() const { + if (word == NEG_INF) + return -1; + if (word == POS_INF) + return 1; + return 0; +} + +inline int +float_ibm_single::is_nan() const { + return (word & ~SGN_MASK) > POS_INF; +} + +inline int +float_ibm_single::is_zero() const { + if (word == NEG_ZERO) + return -1; + if (word == POS_ZERO) + return 1; + return 0; +} + +inline void +float_ibm_single::negate() { + word ^= SGN_MASK; +} + +inline int +float_ibm_single::sign_bit() const { + return !!(word & SGN_MASK); +} + +inline void +float_ibm_single::dec() { + --word; +} + +inline void +float_ibm_single::inc() { + ++word; +} + +inline void +float_ibm_single::set_max(bool negative) { + word = 0x7f000000; + if (negative) + word |= SGN_MASK; +} + +inline void +float_ibm_single::build(bool negative, mpz_t mantissa, int exponent) { + word = mpz_get_ui(mantissa) & ((1UL << MANTISSA_BITS) - 1); + if (negative) + word |= SGN_MASK; + word |= static_cast<uint32_t>(exponent + EXPONENT_BIAS) << MANTISSA_BITS; +} + + ///asasdasda +inline int float_intel_double_extended::is_inf() const { if (lsp != LSP_INF) return 0; diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index acc28e6..7d2a2f1 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -86,6 +86,7 @@ test01() { abstract_store.affine_image(R, X - S); abstract_store.affine_image(Y, X); + // if (R <= -D) Y = S - D; FP_Interval_Abstract_Store as_then(abstract_store); as_then.refine_with_constraint(R <= -D);

1 0

[GIT] ppl/ppl(pip): Removed useless pointer to problem object in PIP_Tree_Node.
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: 99f2fbb392153b9ca8bd25b15e57a33211a25bc1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=99f2fbb39215… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 16:29:54 2009 +0200 Removed useless pointer to problem object in PIP_Tree_Node. --- src/PIP_Problem.cc | 2 +- src/PIP_Tree.cc | 24 ++++++++++-------------- src/PIP_Tree.defs.hh | 10 +++------- 3 files changed, 14 insertions(+), 22 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index 3e657f3..225372f 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -79,7 +79,7 @@ PPL::PIP_Problem::solve() const { PIP_Problem_Status return_value; if (current_solution == 0) - x.current_solution = new PIP_Solution_Node(&x); + x.current_solution = new PIP_Solution_Node(); if (input_cs.empty()) { // no constraints: solution = {0} return OPTIMIZED_PIP_PROBLEM; diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 2c9fe70..5e6bcd1 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -112,15 +112,13 @@ operator<<(std::ostream& os, const PIP_Tree_Node::Artificial_Parameter& x) { } // namespace IO_Operators -PIP_Tree_Node::PIP_Tree_Node(PIP_Problem* p) - : problem(p), - constraints_(), +PIP_Tree_Node::PIP_Tree_Node() + : constraints_(), artificial_parameters() { } PIP_Tree_Node::PIP_Tree_Node(const PIP_Tree_Node &x) - : problem(x.problem), - constraints_(x.constraints_), + : constraints_(x.constraints_), artificial_parameters(x.artificial_parameters) { } @@ -171,8 +169,8 @@ PIP_Decision_Node::~PIP_Decision_Node() { PIP_Solution_Node::~PIP_Solution_Node() { } -PIP_Solution_Node::PIP_Solution_Node(PIP_Problem* p) - : PIP_Tree_Node(p), +PIP_Solution_Node::PIP_Solution_Node() + : PIP_Tree_Node(), tableau(), basis(), mapping(), @@ -193,7 +191,7 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x) PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, bool empty_constraints) - : PIP_Tree_Node(x.problem), + : PIP_Tree_Node(), tableau(x.tableau), basis(x.basis), mapping(x.mapping), @@ -206,10 +204,9 @@ PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, } } -PIP_Decision_Node::PIP_Decision_Node(PIP_Problem* p, - PIP_Tree_Node* fcp, +PIP_Decision_Node::PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp) - : PIP_Tree_Node(p), + : PIP_Tree_Node(), true_child(tcp), false_child(fcp) { } @@ -1174,14 +1171,13 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, } /* Create a decision Node to become parent of current Node */ - PIP_Decision_Node* parent - = new PIP_Decision_Node(fals->problem, fals, tru); + PIP_Decision_Node* parent = new PIP_Decision_Node(fals, tru); parent->add_constraint(test, parameters); if (!cs.empty()) { /* If node to be solved had tautologies, store them in a new decision node */ - parent = new PIP_Decision_Node(fals->problem, 0, parent); + parent = new PIP_Decision_Node(0, parent); cs.swap(parent->constraints_); } aps.swap(parent->artificial_parameters); diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index e70f467..e4a7e8b 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -122,7 +122,7 @@ public: protected: //! Default constructor. - PIP_Tree_Node(PIP_Problem* p); + PIP_Tree_Node(); //! Copy constructor. PIP_Tree_Node(const PIP_Tree_Node &x); @@ -136,10 +136,6 @@ protected: friend class PIP_Decision_Node; friend class PIP_Solution_Node; - //FIXME - remove problem pointer - //! A pointer to the master problem object. - PIP_Problem* problem; - //! The local system of parameter constraints. Constraint_System constraints_; @@ -199,7 +195,7 @@ protected: class PIP_Solution_Node : public PIP_Tree_Node { public: //! Default constructor. - PIP_Solution_Node(PIP_Problem* p); + PIP_Solution_Node(); //! Destructor. ~PIP_Solution_Node(); @@ -447,7 +443,7 @@ private: \exception std::invalid_argument Thrown if \p cs contains strict inequalities. */ - PIP_Decision_Node(PIP_Problem* p, PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); + PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); protected: /*! \brief

1 0

[GIT] ppl/ppl(pip): Minor fixes in Doxygen documentation.
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: e0451215bb4b46c08a054a803850e841753722e3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e0451215bb4b… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 16:00:20 2009 +0200 Minor fixes in Doxygen documentation. --- src/PIP_Tree.defs.hh | 7 +++++-- 1 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 65f3a47..e70f467 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -107,10 +107,10 @@ public: \param params the Variables_Set to be updated - + \param space_dimension the space dimension for \p *this - + \return the number of inserted indices */ @@ -215,6 +215,9 @@ public: The returned linear expression only involves parameters. + \param v + the variable which is queried about + \param parameters a \c std::set of indices of the parameters in the constraints

1 0

[GIT] ppl/ppl(pip): Improved accuracy of context compatibility checks.
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: d876143defdad8b67abd6996277958241d6c9974 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d876143defda… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 12:48:18 2009 +0200 Improved accuracy of context compatibility checks. --- src/PIP_Tree.cc | 18 +++++++++--------- 1 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index e4ff584..2c9fe70 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -69,13 +69,13 @@ merge_assign(Matrix& x, } } -// Tranform expression "expr" into "-expr-1" +// Tranform expression "expr" into "-expr-1", using scaling void -negate_assign(Row& x, const Row& y) { +negate_assign(Row& x, const Row& y, const Coefficient& sc) { PPL_ASSERT(x.size() == y.size()); for (dimension_type i = x.size(); i-- > 0; ) x[i] = -y[i]; - x[0] -= 1; + x[0] -= sc; } // Update given context matrix using local artificials @@ -405,7 +405,7 @@ PIP_Decision_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& context, update_context(context_false, artificial_parameters); merge_assign(context_false, constraints_, parameters); Row &last = context_false[context_false.num_rows()-1]; - negate_assign(last, last); + negate_assign(last, last, 1); stf = false_child->solve(false_child, context_false, parameters, space_dimension); } @@ -664,11 +664,11 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { break; } // Perform a pivot operation on the matrix - const Coefficient& sij = p[j]; + const Coefficient sij = p[j]; for (j_=0; j_<num_cols; ++j_) { if (j_ == j) continue; - const Coefficient& sij_ = p[j_]; + const Coefficient sij_ = p[j_]; for (k=0; k<num_rows; ++k) { if (k == i) continue; @@ -856,7 +856,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, // constraint t_i(z) >= 0 is compatible with the context s = POSITIVE; Row c(num_params, Row::Flags()); - negate_assign(c, tableau.t[i]); + negate_assign(c, tableau.t[i], tableau.get_denominator()); if (compatibility_check(context, c)) { // constraint t_i(z) < 0 <=> -t_i(z)-1 >= 0 is compatible if (s == POSITIVE) @@ -897,7 +897,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, if (!found) continue; Row row(tableau.t[i]); - row[0] -= 1; + row[0] -= tableau.get_denominator(); if (compatibility_check(context, row)) { if (i__ == n_a_d) i__ = i; @@ -1152,7 +1152,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, aps.swap(artificial_parameters); PIP_Tree_Node *fals = this; Row &testf = context[context.num_rows()-1]; - negate_assign(testf, test); + negate_assign(testf, test, 1); PIP_Problem_Status status_f = solve(fals, context, parameters, space_dimension);

1 0

[GIT] ppl/ppl(floating_point): Changed loop-guards in the first four test of digitalfilters1.cc
by Roberto Amadini 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 4f3fe255850af214acc364daff87fbbec16fc8c0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4f3fe255850a… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Oct 6 12:31:55 2009 +0200 Changed loop-guards in the first four test of digitalfilters1.cc --- tests/Floating_Point_Expression/digitalfilters1.cc | 109 +++++++++++--------- 1 files changed, 58 insertions(+), 51 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 5c3a4fd..acc28e6 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -62,24 +62,26 @@ test01() { Variable R(4); FP_Interval_Abstract_Store abstract_store(5); - FP_Interval tmp(0); + FP_Interval y(0); + FP_Interval y_begin(1); FP_Interval_Abstract_Store as_begin; // Y = 0; - abstract_store.set_interval(Y, tmp); + abstract_store.set_interval(Y, y); - for(unsigned short n = 0; as_begin != abstract_store; ++n) { + for(unsigned short n = 0; y != y_begin; ++n) { nout << "*** n = " << n << " ***" << endl; as_begin = abstract_store; + y_begin = y; // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; - tmp.lower() = -128; - tmp.upper() = 128; - abstract_store.set_interval(X, tmp); - tmp.lower() = 0; - tmp.upper() = 16; - abstract_store.set_interval(D, tmp); + y.lower() = -128; + y.upper() = 128; + abstract_store.set_interval(X, y); + y.lower() = 0; + y.upper() = 16; + abstract_store.set_interval(D, y); abstract_store.affine_image(S, Y); abstract_store.affine_image(R, X - S); abstract_store.affine_image(Y, X); @@ -119,11 +121,11 @@ test01() { abstract_store.limited_CC76_extrapolation_assign(as_begin, cs); Box<FP_Interval> box(abstract_store); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } nout << "*** Y in [-128 - 16n, 128 + 16n] ***" << endl; - return !tmp.is_bounded(); + return !y.is_bounded(); } // tests rate limiter using bounded differences abstract domain @@ -143,24 +145,26 @@ test02() { FP_Interval_Abstract_Store abstract_store(5); FP_BD_Shape bd(abstract_store); - FP_Interval tmp(0); + FP_Interval y_begin(1); + FP_Interval y(0); FP_BD_Shape bd_begin; // Y = 0; - bd.affine_image(Y, FP_Linear_Form(tmp)); + bd.affine_image(Y, FP_Linear_Form(y)); - for(unsigned short n = 0; bd_begin != bd; ++n) { + for(unsigned short n = 0; y != y_begin; ++n) { nout << "*** n = " << n << " ***" << endl; bd_begin = bd; + y_begin = y; // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; - tmp.lower() = -128; - tmp.upper() = 128; - bd.affine_image(X, FP_Linear_Form(tmp)); - tmp.lower() = 0; - tmp.upper() = 16; - bd.affine_image(D, FP_Linear_Form(tmp)); + y.lower() = -128; + y.upper() = 128; + bd.affine_image(X, FP_Linear_Form(y)); + y.lower() = 0; + y.upper() = 16; + bd.affine_image(D, FP_Linear_Form(y)); bd.affine_image(S, FP_Linear_Form(Y)); bd.affine_image(R, FP_Linear_Form(X - S)); bd.affine_image(Y, FP_Linear_Form(X)); @@ -207,11 +211,11 @@ test02() { bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs); Box<FP_Interval> box(bd); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } nout << "*** Y in [-16 - 16n, 128 + 16n] ***" << endl; - return !tmp.is_bounded(); + return !y.is_bounded(); } // tests rate limiter using octagons abstract domain @@ -231,24 +235,26 @@ test03() { FP_Interval_Abstract_Store abstract_store(5); FP_Octagonal_Shape oc(abstract_store); - FP_Interval tmp(0); + FP_Interval y(0); + FP_Interval y_begin(1); FP_Octagonal_Shape oc_begin; // Y = 0; - oc.affine_image(Y, FP_Linear_Form(tmp)); + oc.affine_image(Y, FP_Linear_Form(y)); - for(unsigned short n = 0; oc_begin != oc; ++n) { + for(unsigned short n = 0; y_begin != y; ++n) { nout << "*** n = " << n << " ***" << endl; oc_begin = oc; + y_begin = y; //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; - tmp.lower() = -128; - tmp.upper() = 128; - oc.affine_image(X, FP_Linear_Form(tmp)); - tmp.lower() = 0; - tmp.upper() = 16; - oc.affine_image(D, FP_Linear_Form(tmp)); + y.lower() = -128; + y.upper() = 128; + oc.affine_image(X, FP_Linear_Form(y)); + y.lower() = 0; + y.upper() = 16; + oc.affine_image(D, FP_Linear_Form(y)); oc.affine_image(S, FP_Linear_Form(Y)); oc.affine_image(R, FP_Linear_Form(X - S)); oc.affine_image(Y, FP_Linear_Form(X)); @@ -301,11 +307,11 @@ test03() { oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } - nout << "*** Y in " << tmp << " ***" << endl; - return tmp.is_bounded(); + nout << "*** Y in " << y << " ***" << endl; + return y.is_bounded(); } // tests rate limiter using polyhedra abstract domain @@ -325,24 +331,25 @@ test04() { FP_Interval_Abstract_Store abstract_store(5); NNC_Polyhedron ph(abstract_store); - FP_Interval tmp(0); + FP_Interval y(0); + FP_Interval y_begin(1); NNC_Polyhedron ph_begin; // Y = 0; - ph.affine_image(Y, FP_Linear_Form(tmp)); + ph.affine_image(Y, FP_Linear_Form(y)); - for(unsigned short n = 0; ph_begin != ph; ++n) { + for(unsigned short n = 0; y_begin != y; ++n) { nout << "*** n = " << n << " ***" << endl; ph_begin = ph; - + y_begin = y; // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; - tmp.lower() = -128; - tmp.upper() = 128; - ph.affine_image(X, FP_Linear_Form(tmp)); - tmp.lower() = 0; - tmp.upper() = 16; - ph.affine_image(D, FP_Linear_Form(tmp)); + y.lower() = -128; + y.upper() = 128; + ph.affine_image(X, FP_Linear_Form(y)); + y.lower() = 0; + y.upper() = 16; + ph.affine_image(D, FP_Linear_Form(y)); abstract_store = Box<FP_Interval>(ph); ph.affine_image(S, FP_Linear_Form(Y)); abstract_store = Box<FP_Interval>(ph); @@ -395,11 +402,11 @@ test04() { ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); Box<FP_Interval> box(ph); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } - nout << "*** Y in " << tmp << " ***" << endl; - return tmp.is_bounded(); + nout << "*** Y in " << y << " ***" << endl; + return y.is_bounded(); } // tests rate limiter using octagons abstract domain and @@ -421,7 +428,7 @@ test05() { FP_Interval_Abstract_Store abstract_store(5); FP_Linear_Form_Abstract_Store lf_abstract_store; FP_Octagonal_Shape oc(abstract_store); - FP_Interval tmp(0); + FP_Interval y(0); FP_Octagonal_Shape oc_begin; Con_FP_Expression con_y(0, 0); FP_Linear_Form lx; @@ -508,11 +515,11 @@ test05() { oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); - tmp = box.get_interval(Y); + y = box.get_interval(Y); } - nout << "*** Y in " << tmp << " ***" << endl; - return tmp.is_bounded(); + nout << "*** Y in " << y << " ***" << endl; + return y.is_bounded(); } // tests rate limiter using polyhedra abstract domain and

1 0

[GIT] ppl/ppl(pip): Added generation of non-parametric cuts.
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: c38128604c574a12117776bfd5473d8aede752b3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c38128604c57… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 11:32:17 2009 +0200 Added generation of non-parametric cuts. --- src/PIP_Tree.cc | 121 ++++++++++++++++++++++++++++++------------------------- 1 files changed, 66 insertions(+), 55 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 31a0120..e4ff584 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1248,73 +1248,84 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, << "Cut generation required." << std::endl; #endif - - tableau.t.add_zero_columns(1); tableau.s.add_zero_rows(1, Row::Flags()); tableau.t.add_zero_rows(1, Row::Flags()); - context.add_zero_columns(1); - // Generate new artificial parameter + // Test if cut to be generated must be parametric or not + const Row& row_t1 = tableau.t[i]; + for (j=1; j<num_params; ++j) { + if (row_t1[j] % d != 0) { + tableau.t.add_zero_columns(1); + context.add_zero_columns(1); + break; + } + } + const Row& row_t = tableau.t[i]; - Linear_Expression e; - Variables_Set::const_iterator p; - mod_assign(mod, row_t[0], d); - if (mod != 0) - e += (d-mod); - for (p=parameters.begin(), j=1; j<num_params; ++j, ++p) { - mod_assign(mod, row_t[j], d); + Row& cut_s = tableau.s[num_rows]; + Row& cut_t = tableau.t[num_rows]; + + if (j < num_params) { + // Fractional parameter coefficient found: generate parametric cut + // Generate new artificial parameter + Linear_Expression e; + Variables_Set::const_iterator p; + mod_assign(mod, row_t[0], d); if (mod != 0) - e += (d-mod) * Variable(*p); - } - artificial_parameters.push_back(Artificial_Parameter(e, d)); - parameters.insert(space_dimension); + e += (d-mod); + for (p=parameters.begin(), j=1; j<num_params; ++j, ++p) { + mod_assign(mod, row_t[j], d); + if (mod != 0) + e += (d-mod) * Variable(*p); + } + artificial_parameters.push_back(Artificial_Parameter(e, d)); + parameters.insert(space_dimension); #ifdef NOISY_PIP - using namespace IO_Operators; - std::cout << "Creating new parameter " << Variable(space_dimension) - << " = (" << e << ")/" << d - << std::endl; + using namespace IO_Operators; + std::cout << "Creating new parameter " << Variable(space_dimension) + << " = (" << e << ")/" << d + << std::endl; #endif - ++space_dimension; - - // Update current context with constraints on the new parameter - Row ctx1(num_params+1, Row::Flags()); - Row ctx2(num_params+1, Row::Flags()); - for (j=0; j<num_params; ++j) { - mod_assign(mod, row_t[j], d); - if (mod != 0) { - ctx1[j] = d - mod; - ctx2[j] = -ctx1[j]; - } else { - ctx1[j] = 0; - ctx2[j] = 0; + ++space_dimension; + + // Update current context with constraints on the new parameter + Row ctx1(num_params+1, Row::Flags()); + Row ctx2(num_params+1, Row::Flags()); + for (j=0; j<num_params; ++j) { + mod_assign(mod, row_t[j], d); + if (mod != 0) { + ctx1[j] = d - mod; + ctx2[j] = -ctx1[j]; + } else { + ctx1[j] = 0; + ctx2[j] = 0; + } } - } - ctx1[num_params] = -d; - ctx2[num_params] = d; - ctx2[0] += d-1; + ctx1[num_params] = -d; + ctx2[num_params] = d; + ctx2[0] += d-1; #ifdef NOISY_PIP - { - Variables_Set::const_iterator p = parameters.begin(); - Linear_Expression e1; - Linear_Expression e2; - for (j=1; j<=num_params; ++j, ++p) { - e1 += ctx1[j] * Variable(*p); - e2 += ctx2[j] * Variable(*p); + { + Variables_Set::const_iterator p = parameters.begin(); + Linear_Expression e1; + Linear_Expression e2; + for (j=1; j<=num_params; ++j, ++p) { + e1 += ctx1[j] * Variable(*p); + e2 += ctx2[j] * Variable(*p); + } + e1 += ctx1[0]; + e2 += ctx2[0]; + std::cout << "Inserting into context: " + << Constraint(e1 >= 0) << " ; " + << Constraint(e2 >= 0) << std::endl; } - e1 += ctx1[0]; - e2 += ctx2[0]; - std::cout << "Inserting into context: " - << Constraint(e1 >= 0) << " ; " - << Constraint(e2 >= 0) << std::endl; - } #endif - context.add_row(ctx1); - context.add_row(ctx2); + context.add_row(ctx1); + context.add_row(ctx2); + cut_t[num_params] = d*d; + } // Generate new cut - Row& cut_s = tableau.s[num_rows]; - Row& cut_t = tableau.t[num_rows]; - //const Row& row_t = tableau.t[i]; const Row& row_s = tableau.s[i]; for (j=0; j<num_vars; ++j) { mod_assign(mod, row_s[j], d); @@ -1327,9 +1338,9 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, else cut_t[j] = 0; } - cut_t[num_params] = d*d; #ifdef NOISY_PIP { + using namespace IO_Operators; Linear_Expression e; dimension_type ti = 1; dimension_type si = 0;

1 0

[GIT] ppl/ppl(pip): Improved display in noisy mode.
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: 620039bd51f0e178511b097b5bfacfe4c49f903b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=620039bd51f0… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 10:54:18 2009 +0200 Improved display in noisy mode. --- src/PIP_Tree.cc | 21 +++++++++++++++++++++ src/PIP_Tree.defs.hh | 1 + 2 files changed, 22 insertions(+), 0 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index f2866e7..31a0120 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -824,6 +824,12 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, dimension_type num_params = tableau.t.num_columns(); Row_Sign s; +#ifdef NOISY_PIP + tableau.ascii_dump(std::cout); + std::cout << "context "; + context.ascii_dump(std::cout); +#endif + for (i=0; i<num_rows; ++i) { Row_Sign s = sign[i]; if (s == UNKNOWN) { @@ -1322,6 +1328,21 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, cut_t[j] = 0; } cut_t[num_params] = d*d; +#ifdef NOISY_PIP + { + Linear_Expression e; + dimension_type ti = 1; + dimension_type si = 0; + for (j=0; j<space_dimension; ++j) { + if (parameters.count(j) == 1) + e += cut_t[ti++] * Variable(j); + else + e += cut_s[si++] * Variable(j); + } + std::cout << "Adding cut: " << Constraint(e + cut_t[0] >= 0) + << std::endl; + } +#endif sign.push_back(NEGATIVE); } } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 6db48e9..65f3a47 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -136,6 +136,7 @@ protected: friend class PIP_Decision_Node; friend class PIP_Solution_Node; + //FIXME - remove problem pointer //! A pointer to the master problem object. PIP_Problem* problem;

1 0