- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(sparse_matrices): Use itr->field instead of (*itr).field, many occurrencies fixed.
by Marco Poletti 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: e7dbab946365a7ccf612a2205b504b37a863cff1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e7dbab946365… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Apr 16 15:07:12 2010 +0200 Use itr->field instead of (*itr).field, many occurrencies fixed. --- src/Dense_Matrix.cc | 2 +- src/Dense_Row.inlines.hh | 10 +- src/MIP_Problem.cc | 44 ++-- src/PIP_Problem.cc | 4 +- src/PIP_Tree.cc | 292 ++++++++++---------- src/Sparse_Row.defs.hh | 4 +- ...ited_Sparse_Row_Custom_Slist_Backend.inlines.hh | 24 +- src/Unlimited_Sparse_Row_Over_CO_Tree.templates.hh | 88 +++--- src/Unlimited_Sparse_Row_Over_Linear_Sequence.cc | 2 +- ...ited_Sparse_Row_Over_Linear_Sequence.inlines.hh | 48 ++-- ...ed_Sparse_Row_Over_Linear_Sequence.templates.hh | 204 +++++++------- src/Unlimited_Sparse_Row_Std_List_Backend.cc | 2 +- ...nlimited_Sparse_Row_Std_List_Backend.inlines.hh | 24 +- ...imited_Sparse_Row_Std_Vector_Backend.inlines.hh | 30 +- 14 files changed, 389 insertions(+), 389 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e7dbab94…

1 0

[GIT] ppl/ppl(sparse_matrices): Dense_Row: implement operator->() for iterators and const iterators.
by Marco Poletti 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 23192afd0a9f4d4ae5064c908e334be2dc1b7b49 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=23192afd0a9f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Apr 16 15:05:10 2010 +0200 Dense_Row: implement operator->() for iterators and const iterators. --- src/Dense_Row.defs.hh | 48 +++++++++++++++++++++++++++++++++++++++- src/Dense_Row.inlines.hh | 55 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 102 insertions(+), 1 deletions(-) diff --git a/src/Dense_Row.defs.hh b/src/Dense_Row.defs.hh index 68b228a..673304a 100644 --- a/src/Dense_Row.defs.hh +++ b/src/Dense_Row.defs.hh @@ -359,14 +359,44 @@ private: class Parma_Polyhedra_Library::Dense_Row::iterator { public: + typedef std::pair<const dimension_type,Coefficient&> value_type; typedef std::pair<const dimension_type,const Coefficient&> const_type; +private: + + class Member_Access_Helper { + public: + + Member_Access_Helper(dimension_type index, Coefficient& data); + + value_type* operator->(); + + private: + value_type value; + }; + + class Const_Member_Access_Helper { + public: + + Const_Member_Access_Helper(dimension_type index, + const Coefficient& data); + + const const_type* operator->() const; + + private: + const_type value; + }; + +public: iterator(Dense_Row& row1, dimension_type i1); value_type operator*(); const_type operator*() const; + Member_Access_Helper operator->(); + Const_Member_Access_Helper operator->() const; + iterator& operator++(); iterator operator++(int); @@ -387,12 +417,28 @@ private: class Parma_Polyhedra_Library::Dense_Row::const_iterator { public: - typedef std::pair<const dimension_type, const Coefficient&> const_type; +private: + + class Const_Member_Access_Helper { + public: + + Const_Member_Access_Helper(dimension_type index, + const Coefficient& data); + + const const_type* operator->() const; + + private: + const_type value; + }; + +public: + const_iterator(const Dense_Row& row1, dimension_type i1); const_type operator*() const; + Const_Member_Access_Helper operator->() const; const_iterator& operator++(); const_iterator operator++(int); diff --git a/src/Dense_Row.inlines.hh b/src/Dense_Row.inlines.hh index 2c2982f..b7b85d9 100644 --- a/src/Dense_Row.inlines.hh +++ b/src/Dense_Row.inlines.hh @@ -383,6 +383,18 @@ Dense_Row::iterator::operator*() const { return const_type(i, (*row)[i]); } +inline Dense_Row::iterator::Member_Access_Helper +Dense_Row::iterator::operator->() { + PPL_ASSERT(i < row->size()); + return Member_Access_Helper(i, (*row)[i]); +} + +inline Dense_Row::iterator::Const_Member_Access_Helper +Dense_Row::iterator::operator->() const { + PPL_ASSERT(i < row->size()); + return Const_Member_Access_Helper(i, (*row)[i]); +} + inline Dense_Row::iterator& Dense_Row::iterator::operator++() { PPL_ASSERT(i < row->size()); @@ -436,6 +448,30 @@ Dense_Row::iterator::OK() const { inline +Dense_Row::iterator::Member_Access_Helper +::Member_Access_Helper(dimension_type index, Coefficient& data) + : value(index, data) { +} + +inline Dense_Row::iterator::value_type* +Dense_Row::iterator::Member_Access_Helper::operator->() { + return &value; +} + + +inline +Dense_Row::iterator::Const_Member_Access_Helper +::Const_Member_Access_Helper(dimension_type index, const Coefficient& data) + : value(index, data) { +} + +inline const Dense_Row::iterator::const_type* +Dense_Row::iterator::Const_Member_Access_Helper::operator->() const { + return &value; +} + + +inline Dense_Row::const_iterator::const_iterator(const Dense_Row& row1, dimension_type i1) : row(&row1), i(i1) { @@ -448,6 +484,12 @@ Dense_Row::const_iterator::operator*() const { return const_type(i, (*row)[i]); } +inline Dense_Row::const_iterator::Const_Member_Access_Helper +Dense_Row::const_iterator::operator->() const { + PPL_ASSERT(i < row->size()); + return Const_Member_Access_Helper(i, (*row)[i]); +} + inline Dense_Row::const_iterator& Dense_Row::const_iterator::operator++() { PPL_ASSERT(i < row->size()); @@ -494,6 +536,19 @@ Dense_Row::const_iterator::OK() const { return (i <= row->size()); } + + +inline +Dense_Row::const_iterator::Const_Member_Access_Helper +::Const_Member_Access_Helper(dimension_type index, const Coefficient& data) + : value(index, data) { +} + +inline const Dense_Row::const_iterator::const_type* +Dense_Row::const_iterator::Const_Member_Access_Helper::operator->() const { + return &value; +} + } // namespace Parma_Polyhedra_Library

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree: add a faster implementation for the get2() method.
by Marco Poletti 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 24a28f39e4f816435b88a159a0d10e6e586de7a3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=24a28f39e4f8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Apr 16 13:41:46 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: add a faster implementation for the get2() method. --- src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 17 ++++++++++++++--- 1 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh index 9c7385d..a2b8188 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh @@ -685,9 +685,20 @@ Unlimited_Sparse_Row_Over_CO_Tree::get2(const dimension_type c1, const dimension_type c2, const Coefficient*& p1, const Coefficient*& p2) const { - // TODO: consider a faster impementation. - p1 = &(get(c1)); - p2 = &(get(c2)); + const_iterator itr1; + const_iterator itr2; + + find2(c1, c2, itr1, itr2); + + if (itr1.itr.is_at_end()) + p1 = &Coefficient_zero(); + else + p1 = &(itr1->second); + + if (itr2.itr.is_at_end()) + p2 = &Coefficient_zero(); + else + p2 = &(itr2->second); }

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree: add a faster implementation for find2() and find2_dangerous() methods.
by Marco Poletti 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 89087edefda0ac6590079f71ac25dbef4743d90e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=89087edefda0… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Apr 16 13:41:17 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: add a faster implementation for find2() and find2_dangerous() methods. --- src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 126 ++++++++++++++++++++-- 1 files changed, 117 insertions(+), 9 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh index 6007cf0..9c7385d 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh @@ -310,18 +310,90 @@ inline void Unlimited_Sparse_Row_Over_CO_Tree ::find2_dangerous(const dimension_type c1, const dimension_type c2, dangerous_iterator& itr1, dangerous_iterator& itr2) { - // TODO: consider a faster implementation. - itr1 = find_dangerous(c1); - itr2 = find_dangerous(c2); + if (tree.empty()) { + itr1 = end_dangerous(); + itr2 = itr1; + return; + } + + itr1.itr = CO_Tree::inorder_iterator(&tree); + while (1) { + if (itr1.itr->first < c1) { + if (itr1.itr->first < c2) { + if (!itr1.itr.get_right_child_value()) { + ++(itr1.itr); + itr2.itr = itr1.itr; + break; + } + } else { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } + } else { + if (itr1.itr->first == c1 || itr1.itr->first <= c2) { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } else { + if (!itr1.itr.get_left_child_value()) { + itr2.itr = itr1.itr; + break; + } + } + } + } + if (itr1.itr->first != c1) + itr1 = end_dangerous(); + if (itr2.itr->first != c2) + itr2 = end_dangerous(); } inline void Unlimited_Sparse_Row_Over_CO_Tree::find2(const dimension_type c1, const dimension_type c2, iterator& itr1, iterator& itr2) { - // TODO: consider a faster implementation. - itr1 = find(c1); - itr2 = find(c2); + if (tree.empty()) { + itr1 = end(); + itr2 = itr1; + return; + } + + itr1.itr = CO_Tree::inorder_iterator(&tree); + while (1) { + if (itr1.itr->first < c1) { + if (itr1.itr->first < c2) { + if (!itr1.itr.get_right_child_value()) { + ++(itr1.itr); + itr2.itr = itr1.itr; + break; + } + } else { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } + } else { + if (itr1.itr->first == c1 || itr1.itr->first <= c2) { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } else { + if (!itr1.itr.get_left_child_value()) { + itr2.itr = itr1.itr; + break; + } + } + } + } + if (itr1.itr->first != c1) + itr1 = end(); + if (itr2.itr->first != c2) + itr2 = end(); } inline void @@ -329,9 +401,45 @@ Unlimited_Sparse_Row_Over_CO_Tree::find2(const dimension_type c1, const dimension_type c2, const_iterator& itr1, const_iterator& itr2) const { - // TODO: consider a faster implementation. - itr1 = find(c1); - itr2 = find(c2); + if (tree.empty()) { + itr1 = end(); + itr2 = itr1; + return; + } + + itr1.itr = CO_Tree::inorder_const_iterator(&tree); + while (1) { + if (itr1.itr->first < c1) { + if (itr1.itr->first < c2) { + if (!itr1.itr.get_right_child_value()) { + ++(itr1.itr); + itr2.itr = itr1.itr; + break; + } + } else { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } + } else { + if (itr1.itr->first == c1 || itr1.itr->first <= c2) { + itr2.itr = itr1.itr; + tree.lower_bound(itr1.itr, c1); + tree.lower_bound(itr2.itr, c2); + break; + } else { + if (!itr1.itr.get_left_child_value()) { + itr2.itr = itr1.itr; + break; + } + } + } + } + if (itr1.itr->first != c1) + itr1 = end(); + if (itr2.itr->first != c2) + itr2 = end(); } inline Unlimited_Sparse_Row_Over_CO_Tree::dangerous_iterator

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree: remove some TODOs.
by Marco Poletti 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: dc67686d3d77fca5c70d1b1947a5722e5022a6b8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dc67686d3d77… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Apr 16 13:40:00 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: remove some TODOs. --- src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 6 ------ 1 files changed, 0 insertions(+), 6 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh index 65a6020..6007cf0 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh @@ -248,7 +248,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::find_dangerous(const dimension_type c, #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return find_dangerous(c); } @@ -260,7 +259,6 @@ Unlimited_Sparse_Row_Over_CO_Tree #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return lower_bound_dangerous(c); } @@ -272,7 +270,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::find(const dimension_type c, #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return find(c); } @@ -284,7 +281,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::lower_bound(const dimension_type c, #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return lower_bound(c); } @@ -296,7 +292,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::find(const dimension_type c, #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return find(c); } @@ -308,7 +303,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::lower_bound(const dimension_type c, #ifdef NDEBUG (void) itr; #endif - // TODO: consider a faster implementation. return lower_bound(c); }

1 0

[GIT] ppl/ppl(master): Corrected a few typos.
by Enea Zaffanella 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: master Commit: 41926a747ca792393a6ea992f7234d24f980369a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41926a747ca7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 16 14:46:46 2010 +0200 Corrected a few typos. --- interfaces/Prolog/XSB/xsb_pl_check.P | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/interfaces/Prolog/XSB/xsb_pl_check.P b/interfaces/Prolog/XSB/xsb_pl_check.P index 1958f03..c0e773f 100644 --- a/interfaces/Prolog/XSB/xsb_pl_check.P +++ b/interfaces/Prolog/XSB/xsb_pl_check.P @@ -155,8 +155,8 @@ site: http://www.cs.unipr.it/ppl/ . */ ppl_new_PIP_Problem_from_space_dimension/2, ppl_new_PIP_Problem/4, ppl_new_PIP_Problem_from_PIP_Problem/2, - ppl_PIP_Problem_swap/2 *nofail, - ppl_delete_PIP_Problem/1 *nofail, + ppl_PIP_Problem_swap/2, + ppl_delete_PIP_Problem/1, ppl_PIP_Problem_space_dimension/2, ppl_PIP_Problem_parameter_space_dimensions/2, ppl_PIP_Problem_constraints/2, @@ -165,7 +165,7 @@ site: http://www.cs.unipr.it/ppl/ . */ ppl_PIP_Problem_add_to_parameter_space_dimensions/2, ppl_PIP_Problem_add_constraint/2, ppl_PIP_Problem_add_constraints/2, - ppl_PIP_Problem_set_control_parameter/2 *nofail, + ppl_PIP_Problem_set_control_parameter/2, ppl_PIP_Problem_get_control_parameter/3, ppl_PIP_Problem_has_big_parameter_dimension/2, ppl_PIP_Problem_set_big_parameter_dimension/2,

1 0

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

16 Apr '10

Module: ppl/w3ppl Branch: master Commit: 5b1155a6c45815f9ff288374ec00a23016169309 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=5b1155a6c4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 16 14:40:41 2010 +0200 Added BandaG10. --- htdocs/Documentation/ppl_citations.bib | 27 +++++++++++++++++++++++++++ 1 files changed, 27 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index e51ce00..8cc053d 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -1365,6 +1365,33 @@ procedure." } +@Inproceedings{BandaG10, + Author = "G. Banda and J. P. Gallagher", + Title = "Constraint-Based Abstraction of a Model Checker + for Infinite State Systems", + Booktitle = "Proceedings of the 23rd Workshop on (Constraint) + Logic Programming (WLP 2009)", + Editor = "U. Geske and A. Wolf", + Address = "Potsdam, Germany", + Publisher = "Potsdam Universit{\"a}tsverlag", + Year = 2010, + Pages = "109--124", + Abstract = "Abstract interpretation-based model checking provides an + approach to verifying properties of infinite-state + systems. In practice, most previous work on abstract + model checking is either restricted to verifying + universal properties, or develops special techniques for + temporal logics such as modal transition systems or + other dual transition systems. By contrast we apply + completely standard techniques for constructing abstract + interpretations to the abstraction of a CTL semantic + function, without restricting the kind of properties + that can be verified. Furthermore we show that this + leads directly to implementation of abstract model + checking algorithms for abstract domains based on + constraints, making use of an SMT solver." +} + @Inproceedings{GulavaniR06, Author = "B. S. Gulavani and S. K. Rajamani", Title = "Counterexample Driven Refinement for Abstract Interpretation",

1 0

[GIT] ppl/ppl(master): Corrected typo causing a bug in the XSB Prolog interface.
by Enea Zaffanella 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: master Commit: 39fd68769135cfa380fadefddfdede59609e2f9c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=39fd68769135… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 16 14:06:50 2010 +0200 Corrected typo causing a bug in the XSB Prolog interface. --- .../Prolog/XSB/ppl_interface_generator_xsb_cc.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/interfaces/Prolog/XSB/ppl_interface_generator_xsb_cc.m4 b/interfaces/Prolog/XSB/ppl_interface_generator_xsb_cc.m4 index 8202bb2..f7cb94b 100644 --- a/interfaces/Prolog/XSB/ppl_interface_generator_xsb_cc.m4 +++ b/interfaces/Prolog/XSB/ppl_interface_generator_xsb_cc.m4 @@ -120,7 +120,7 @@ name() { \ Prolog_term_ref arg5 = reg_term(5); \ Prolog_term_ref arg6 = reg_term(6); \ Prolog_term_ref arg7 = reg_term(7); \ - Prolog_term_ref arg7 = reg_term(8); \ + Prolog_term_ref arg8 = reg_term(8); \ return xsb_stub_##name(arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8); \ }

1 0

[GIT] ppl/ppl(master): Add method wrap_assign() to Pointset_Powerset.
by Enea Zaffanella 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: master Commit: 7db9d078f15311aaaeed57e0dae06c44e89dd329 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7db9d078f153… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 16 11:14:23 2010 +0200 Add method wrap_assign() to Pointset_Powerset. --- src/Pointset_Powerset.defs.hh | 54 ++++++++++++++++++++++++++++++++++++ src/Pointset_Powerset.templates.hh | 18 ++++++++++++ 2 files changed, 72 insertions(+), 0 deletions(-) diff --git a/src/Pointset_Powerset.defs.hh b/src/Pointset_Powerset.defs.hh index 849e971..0ae87f3 100644 --- a/src/Pointset_Powerset.defs.hh +++ b/src/Pointset_Powerset.defs.hh @@ -985,6 +985,60 @@ public: void time_elapse_assign(const Pointset_Powerset& y); /*! \brief + \ref Wrapping_Operator "Wraps" the specified dimensions of the + vector space. + + \param vars + The set of Variable objects corresponding to the space dimensions + to be wrapped. + + \param w + The width of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param r + The representation of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param o + The overflow behavior of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param pcs + Possibly null pointer to a constraint system whose variables + are contained in \p vars. If <CODE>*pcs</CODE> depends on + variables not in \p vars, the behavior is undefined. + When non-null, the pointed-to constraint system is assumed to + represent the conditional or looping construct guard with respect + to which wrapping is performed. Since wrapping requires the + computation of upper bounds and due to non-distributivity of + constraint refinement over upper bounds, passing a constraint + system in this way can be more precise than refining the result of + the wrapping operation with the constraints in <CODE>*pcs</CODE>. + + \param complexity_threshold + A precision parameter of the \ref Wrapping_Operator "wrapping operator": + higher values result in possibly improved precision. + + \param wrap_individually + <CODE>true</CODE> if the dimensions should be wrapped individually + (something that results in much greater efficiency to the detriment of + precision). + + \exception std::invalid_argument + Thrown if <CODE>*pcs</CODE> is dimension-incompatible with + \p vars, or if \p *this is dimension-incompatible \p vars or with + <CODE>*pcs</CODE>. + */ + void wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Representation r, + Bounded_Integer_Type_Overflow o, + const Constraint_System* pcs = 0, + unsigned complexity_threshold = 16, + bool wrap_individually = true); + + /*! \brief Assign to \p *this the result of (recursively) merging together the pairs of disjuncts whose upper-bound is the same as their set-theoretical union. diff --git a/src/Pointset_Powerset.templates.hh b/src/Pointset_Powerset.templates.hh index d759e7b..5391a4e 100644 --- a/src/Pointset_Powerset.templates.hh +++ b/src/Pointset_Powerset.templates.hh @@ -1155,6 +1155,24 @@ Pointset_Powerset<PSET>::contains_integer_point() const { template <typename PSET> void +Pointset_Powerset<PSET>::wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Representation r, + Bounded_Integer_Type_Overflow o, + const Constraint_System* pcs, + unsigned complexity_threshold, + bool wrap_individually) { + Pointset_Powerset& x = *this; + for (Sequence_iterator si = x.sequence.begin(), + s_end = x.sequence.end(); si != s_end; ++si) + si->pointset().wrap_assign(vars, w, r, o, pcs, + complexity_threshold, wrap_individually); + x.reduced = false; + PPL_ASSERT_HEAVY(x.OK()); +} + +template <typename PSET> +void Pointset_Powerset<PSET>::pairwise_reduce() { Pointset_Powerset& x = *this; // It is wise to omega-reduce before pairwise-reducing.

1 0

[GIT] ppl/ppl(master): A minor stylistic improvement and a typo corrected.
by Enea Zaffanella 16 Apr '10

16 Apr '10

Module: ppl/ppl Branch: master Commit: 89dc0e98630f7986a46283fb3fa47259f0e77b8f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=89dc0e98630f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 16 11:13:48 2010 +0200 A minor stylistic improvement and a typo corrected. --- src/Grid_public.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 6d17f57..fcf89c0 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2679,8 +2679,8 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, Bounded_Integer_Type_Representation r, Bounded_Integer_Type_Overflow o, const Constraint_System* pcs, - unsigned, - bool) { + unsigned /* complexity_threshold */, + bool /* wrap_individually */) { // Dimension-compatibility check of `*pcs', if any. if (pcs != 0) { @@ -2698,7 +2698,7 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, if (space_dim < min_space_dim) throw_dimension_incompatible("wrap_assign(vs, ...)", min_space_dim); - // Wrapping an empty polyhedron is a no-op. + // Wrapping an empty grid is a no-op. if (marked_empty()) return; if (!generators_are_minimized() && !minimize())

1 0