#include <Powerset.defs.hh>
Public Types | |
typedef Sequence::size_type | size_type |
typedef Sequence::value_type | value_type |
typedef iterator_to_const < Sequence > | iterator |
Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element. | |
typedef const_iterator_to_const < Sequence > | const_iterator |
A bidirectional const_iterator on the disjuncts of a Powerset element. | |
typedef std::reverse_iterator < iterator > | reverse_iterator |
The reverse iterator type built from Powerset::iterator. | |
typedef std::reverse_iterator < const_iterator > | const_reverse_iterator |
The reverse iterator type built from Powerset::const_iterator. | |
Public Member Functions | |
Constructors and Destructor | |
Powerset () | |
Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset). | |
Powerset (const Powerset &y) | |
Copy constructor. | |
Powerset (const D &d) | |
If d is not bottom, builds a powerset containing only d . Builds the empty powerset otherwise. | |
~Powerset () | |
Destructor. | |
Member Functions that Do Not Modify the Powerset Object | |
bool | definitely_entails (const Powerset &y) const |
Returns true if *this definitely entails y . Returns false if *this may not entail y (i.e., if *this does not entail y or if entailment could not be decided). | |
bool | is_top () const |
Returns true if and only if *this is the top element of the powerset constraint system (i.e., it represents the universe). | |
bool | is_bottom () const |
Returns true if and only if *this is the bottom element of the powerset constraint system (i.e., it represents the empty set). | |
memory_size_type | total_memory_in_bytes () const |
Returns a lower bound to the total size in bytes of the memory occupied by *this . | |
memory_size_type | external_memory_in_bytes () const |
Returns a lower bound to the size in bytes of the memory managed by *this . | |
bool | OK (bool disallow_bottom=false) const |
Checks if all the invariants are satisfied. | |
Member Functions for the Direct Manipulation of Disjuncts | |
void | omega_reduce () const |
Drops from the sequence of disjuncts in *this all the non-maximal elements so that *this is non-redundant. | |
size_type | size () const |
Returns the number of disjuncts. | |
bool | empty () const |
Returns true if and only if there are no disjuncts in *this . | |
iterator | begin () |
Returns an iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end iterator. | |
iterator | end () |
Returns the past-the-end iterator. | |
const_iterator | begin () const |
Returns a const_iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end const_iterator. | |
const_iterator | end () const |
Returns the past-the-end const_iterator. | |
reverse_iterator | rbegin () |
Returns a reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start reverse_iterator. | |
reverse_iterator | rend () |
Returns the before-the-start reverse_iterator. | |
const_reverse_iterator | rbegin () const |
Returns a const_reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start const_reverse_iterator. | |
const_reverse_iterator | rend () const |
Returns the before-the-start const_reverse_iterator. | |
void | add_disjunct (const D &d) |
Adds to *this the disjunct d . | |
iterator | drop_disjunct (iterator position) |
Drops the disjunct in *this pointed to by position , returning an iterator to the disjunct following position . | |
void | drop_disjuncts (iterator first, iterator last) |
Drops all the disjuncts from first to last (excluded). | |
void | clear () |
Drops all the disjuncts, making *this an empty powerset. | |
Member Functions that May Modify the Powerset Object | |
Powerset & | operator= (const Powerset &y) |
The assignment operator. | |
void | swap (Powerset &y) |
Swaps *this with y . | |
void | least_upper_bound_assign (const Powerset &y) |
Assigns to *this the least upper bound of *this and y . | |
void | upper_bound_assign (const Powerset &y) |
Assigns to *this an upper bound of *this and y . | |
bool | upper_bound_assign_if_exact (const Powerset &y) |
Assigns to *this the least upper bound of *this and y and returns true . | |
void | meet_assign (const Powerset &y) |
Assigns to *this the meet of *this and y . | |
void | collapse () |
If *this is not empty (i.e., it is not the bottom element), it is reduced to a singleton obtained by computing an upper-bound of all the disjuncts. | |
Protected Types | |
typedef std::list< D > | Sequence |
A powerset is implemented as a sequence of elements. | |
typedef Sequence::iterator | Sequence_iterator |
Alias for the low-level iterator on the disjuncts. | |
typedef Sequence::const_iterator | Sequence_const_iterator |
Alias for the low-level const_iterator on the disjuncts. | |
Protected Member Functions | |
bool | is_omega_reduced () const |
Returns true if and only if *this does not contain non-maximal elements. | |
void | collapse (unsigned max_disjuncts) |
Upon return, *this will contain at most max_disjuncts elements; the set of disjuncts in positions greater than or equal to max_disjuncts , will be replaced at that position by their upper-bound. | |
iterator | add_non_bottom_disjunct_preserve_reduction (const D &d, iterator first, iterator last) |
Adds to *this the disjunct d , assuming d is not the bottom element and ensuring partial Omega-reduction. | |
void | add_non_bottom_disjunct_preserve_reduction (const D &d) |
Adds to *this the disjunct d , assuming d is not the bottom element and preserving Omega-reduction. | |
template<typename Binary_Operator_Assign> | |
void | pairwise_apply_assign (const Powerset &y, Binary_Operator_Assign op_assign) |
Assigns to *this the result of applying op_assign pairwise to the elements in *this and y . | |
Protected Attributes | |
Sequence | sequence |
The sequence container holding powerset's elements. | |
bool | reduced |
If true , *this is Omega-reduced. | |
Private Member Functions | |
bool | check_omega_reduced () const |
Does the hard work of checking whether *this contains non-maximal elements and returns true if and only if it does not. | |
void | collapse (Sequence_iterator sink) |
Replaces the disjunct *sink by an upper bound of itself and all the disjuncts following it. | |
Related Functions | |
(Note that these are not member functions.) | |
template<typename D> | |
bool | operator== (const Powerset< D > &x, const Powerset< D > &y) |
Returns true if and only if x and y are equivalent. | |
template<typename D> | |
bool | operator!= (const Powerset< D > &x, const Powerset< D > &y) |
Returns true if and only if x and y are not equivalent. | |
template<typename D> | |
std::ostream & | operator<< (std::ostream &s, const Powerset< D > &x) |
Output operator. | |
template<typename D> | |
void | swap (Parma_Polyhedra_Library::Powerset< D > &x, Parma_Polyhedra_Library::Powerset< D > &y) |
Specializes std::swap . |
This class offers a generic implementation of a powerset domain as defined in Section The Powerset Construction.
Besides invoking the available methods on the disjuncts of a Powerset, this class also provides bidirectional iterators that allow for a direct inspection of these disjuncts. For a consistent handling of Omega-reduction, all the iterators are read-only, meaning that the disjuncts cannot be overwritten. Rather, by using the class iterator
, it is possible to drop one or more disjuncts (possibly so as to later add back modified versions). As an example of iterator usage, the following template function drops from powerset ps
all the disjuncts that would have become redundant by the addition of an external element d
.
template <typename D> void drop_subsumed(Powerset<D>& ps, const D& d) { for (typename Powerset<D>::iterator i = ps.begin(), ps_end = ps.end(), i != ps_end; ) if (i->definitely_entails(d)) i = ps.drop_disjunct(i); else ++i; }
The template class D must provide the following methods.
Returns a lower bound on the total size in bytes of the memory occupied by the instance of D.bool is_top() const
true
if and only if the instance of D is the top element of the domain. bool is_bottom() const
true
if and only if the instance of D is the bottom element of the domain. bool definitely_entails(const D& y) const
true
if the instance of D definitely entails y
. Returns false
if the instance may not entail y
(i.e., if the instance does not entail y
or if entailment could not be decided). void upper_bound_assign(const D& y)
y
. void meet_assign(const D& y)
y
. bool OK() const
true
if the instance of D is in a consistent state, else returns false
.The following operators on the template class D must be defined.
operator<<(std::ostream& s, const D& x)
s
. operator==(const D& x, const D& y)
true
if and only if x
and y
are equivalent D's. operator!=(const D& x, const D& y)
true
if and only if x
and y
are different D's.
Definition at line 145 of file Powerset.defs.hh.
typedef std::list<D> Parma_Polyhedra_Library::Powerset< D >::Sequence [protected] |
A powerset is implemented as a sequence of elements.
The particular sequence employed must support efficient deletion in any position and efficient back insertion.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 219 of file Powerset.defs.hh.
typedef Sequence::iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_iterator [protected] |
Alias for the low-level iterator on the disjuncts.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 222 of file Powerset.defs.hh.
typedef Sequence::const_iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_const_iterator [protected] |
Alias for the low-level const_iterator on the disjuncts.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 225 of file Powerset.defs.hh.
typedef Sequence::size_type Parma_Polyhedra_Library::Powerset< D >::size_type |
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 235 of file Powerset.defs.hh.
typedef Sequence::value_type Parma_Polyhedra_Library::Powerset< D >::value_type |
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 236 of file Powerset.defs.hh.
typedef iterator_to_const<Sequence> Parma_Polyhedra_Library::Powerset< D >::iterator |
Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element.
By using this iterator type, the disjuncts cannot be overwritten, but they can be removed using methods drop_disjunct(iterator position)
and drop_disjuncts(iterator first, iterator last)
, while still ensuring a correct handling of Omega-reduction.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 248 of file Powerset.defs.hh.
typedef const_iterator_to_const<Sequence> Parma_Polyhedra_Library::Powerset< D >::const_iterator |
A bidirectional const_iterator on the disjuncts of a Powerset element.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 251 of file Powerset.defs.hh.
typedef std::reverse_iterator<iterator> Parma_Polyhedra_Library::Powerset< D >::reverse_iterator |
The reverse iterator type built from Powerset::iterator.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 254 of file Powerset.defs.hh.
typedef std::reverse_iterator<const_iterator> Parma_Polyhedra_Library::Powerset< D >::const_reverse_iterator |
The reverse iterator type built from Powerset::const_iterator.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 257 of file Powerset.defs.hh.
Parma_Polyhedra_Library::Powerset< D >::Powerset | ( | ) | [inline] |
Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset).
Definition at line 132 of file Powerset.inlines.hh.
Parma_Polyhedra_Library::Powerset< D >::Powerset | ( | const Powerset< D > & | y | ) | [inline] |
Parma_Polyhedra_Library::Powerset< D >::Powerset | ( | const D & | d | ) | [inline, explicit] |
If d
is not bottom, builds a powerset containing only d
. Builds the empty powerset otherwise.
Definition at line 138 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.
Parma_Polyhedra_Library::Powerset< D >::~Powerset | ( | ) | [inline] |
bool Parma_Polyhedra_Library::Powerset< D >::definitely_entails | ( | const Powerset< D > & | y | ) | const [inline] |
Returns true
if *this
definitely entails y
. Returns false
if *this
may not entail y
(i.e., if *this
does not entail y
or if entailment could not be decided).
Definition at line 172 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().
00172 { 00173 const Powerset<D>& x = *this; 00174 bool found = true; 00175 for (const_iterator xi = x.begin(), 00176 x_end = x.end(); found && xi != x_end; ++xi) { 00177 found = false; 00178 for (const_iterator yi = y.begin(), 00179 y_end = y.end(); !found && yi != y_end; ++yi) 00180 found = (*xi).definitely_entails(*yi); 00181 } 00182 return found; 00183 }
bool Parma_Polyhedra_Library::Powerset< D >::is_top | ( | ) | const [inline] |
Returns true
if and only if *this
is the top element of the powerset constraint system (i.e., it represents the universe).
Definition at line 172 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().
00172 { 00173 // Must perform omega-reduction for correctness. 00174 omega_reduce(); 00175 const_iterator xi = begin(); 00176 const_iterator x_end = end(); 00177 return xi != x_end && xi->is_top() && ++xi == x_end; 00178 }
bool Parma_Polyhedra_Library::Powerset< D >::is_bottom | ( | ) | const [inline] |
Returns true
if and only if *this
is the bottom element of the powerset constraint system (i.e., it represents the empty set).
Definition at line 182 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::empty(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::map_space_dimensions().
00182 { 00183 // Must perform omega-reduction for correctness. 00184 omega_reduce(); 00185 return empty(); 00186 }
memory_size_type Parma_Polyhedra_Library::Powerset< D >::total_memory_in_bytes | ( | ) | const [inline] |
Returns a lower bound to the total size in bytes of the memory occupied by *this
.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 216 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes().
00216 { 00217 return sizeof(*this) + external_memory_in_bytes(); 00218 }
memory_size_type Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes | ( | ) | const [inline] |
Returns a lower bound to the size in bytes of the memory managed by *this
.
Reimplemented in Parma_Polyhedra_Library::Pointset_Powerset< PS >.
Definition at line 270 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().
Referenced by Parma_Polyhedra_Library::Powerset< D >::total_memory_in_bytes().
00270 { 00271 memory_size_type bytes = 0; 00272 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) { 00273 bytes += xi->total_memory_in_bytes(); 00274 // We assume there is at least a forward and a backward link, and 00275 // that the pointers implementing them are at least the size of 00276 // pointers to `D'. 00277 bytes += 2*sizeof(D*); 00278 } 00279 return bytes; 00280 }
bool Parma_Polyhedra_Library::Powerset< D >::OK | ( | bool | disallow_bottom = false |
) | const [inline] |
Checks if all the invariants are satisfied.
Definition at line 284 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::reduced.
Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), and Parma_Polyhedra_Library::Powerset< D >::Powerset().
00284 { 00285 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) { 00286 if (!xi->OK()) 00287 return false; 00288 if (disallow_bottom && xi->is_bottom()) { 00289 #ifndef NDEBUG 00290 std::cerr << "Bottom element in powerset!" 00291 << std::endl; 00292 #endif 00293 return false; 00294 } 00295 } 00296 if (reduced && !check_omega_reduced()) { 00297 #ifndef NDEBUG 00298 std::cerr << "Powerset claims to be reduced, but it is not!" 00299 << std::endl; 00300 #endif 00301 return false; 00302 } 00303 return true; 00304 }
void Parma_Polyhedra_Library::Powerset< D >::omega_reduce | ( | ) | const [inline] |
Drops from the sequence of disjuncts in *this
all the non-maximal elements so that *this
is non-redundant.
This method is declared const
because, even though Omega-reduction may change the syntactic representation of *this
, its semantics will be unchanged.
Definition at line 58 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::abandon_expensive_computations, Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::reduced.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_above(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_below(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::constrains(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Powerset< D >::is_bottom(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_topologically_closed(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::maximize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::minimize(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::strictly_contains().
00058 { 00059 if (reduced) 00060 return; 00061 00062 Powerset& x = const_cast<Powerset&>(*this); 00063 // First remove all bottom elements. 00064 for (iterator xi = x.begin(), x_end = x.end(); xi != x_end; ) 00065 if (xi->is_bottom()) 00066 xi = x.drop_disjunct(xi); 00067 else 00068 ++xi; 00069 // Then remove non-maximal elements. 00070 for (iterator xi = x.begin(); xi != x.end(); ) { 00071 const D& xv = *xi; 00072 bool dropping_xi = false; 00073 for (iterator yi = x.begin(); yi != x.end(); ) 00074 if (xi == yi) 00075 ++yi; 00076 else { 00077 const D& yv = *yi; 00078 if (yv.definitely_entails(xv)) 00079 yi = x.drop_disjunct(yi); 00080 else if (xv.definitely_entails(yv)) { 00081 dropping_xi = true; 00082 break; 00083 } 00084 else 00085 ++yi; 00086 } 00087 if (dropping_xi) 00088 xi = x.drop_disjunct(xi); 00089 else 00090 ++xi; 00091 if (abandon_expensive_computations && xi != x.end()) { 00092 // Hurry up! 00093 x.collapse(xi.base); 00094 break; 00095 } 00096 } 00097 reduced = true; 00098 assert(OK()); 00099 }
Powerset< D >::size_type Parma_Polyhedra_Library::Powerset< D >::size | ( | ) | const [inline] |
Returns the number of disjuncts.
Definition at line 81 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_dump(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_universe(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign().
00081 { 00082 return sequence.size(); 00083 }
bool Parma_Polyhedra_Library::Powerset< D >::empty | ( | ) | const [inline] |
Returns true
if and only if there are no disjuncts in *this
.
Definition at line 87 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints_and_minimize(), Parma_Polyhedra_Library::Powerset< D >::collapse(), and Parma_Polyhedra_Library::Powerset< D >::is_bottom().
00087 { 00088 return sequence.empty(); 00089 }
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::begin | ( | ) | [inline] |
Returns an iterator pointing to the first disjunct, if *this
is not empty; otherwise, returns the past-the-end iterator.
Definition at line 33 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_dump(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::collect_certificates(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::constrains(), Parma_Polyhedra_Library::Powerset< D >::definitely_entails(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_universe(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), and Parma_Polyhedra_Library::Powerset< D >::rend().
00033 { 00034 return sequence.begin(); 00035 }
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::end | ( | ) | [inline] |
Returns the past-the-end iterator.
Definition at line 39 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_dump(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::collect_certificates(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::constrains(), Parma_Polyhedra_Library::Powerset< D >::definitely_entails(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_universe(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), and Parma_Polyhedra_Library::Powerset< D >::rbegin().
00039 { 00040 return sequence.end(); 00041 }
Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::begin | ( | ) | const [inline] |
Returns a const_iterator pointing to the first disjunct, if *this
is not empty; otherwise, returns the past-the-end const_iterator.
Definition at line 45 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
00045 { 00046 return sequence.begin(); 00047 }
Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::end | ( | ) | const [inline] |
Returns the past-the-end const_iterator.
Definition at line 51 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
00051 { 00052 return sequence.end(); 00053 }
Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin | ( | ) | [inline] |
Returns a reverse_iterator pointing to the last disjunct, if *this
is not empty; otherwise, returns the before-the-start reverse_iterator.
Definition at line 57 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::end().
00057 { 00058 return reverse_iterator(end()); 00059 }
Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend | ( | ) | [inline] |
Returns the before-the-start reverse_iterator.
Definition at line 63 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin().
00063 { 00064 return reverse_iterator(begin()); 00065 }
Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin | ( | ) | const [inline] |
Returns a const_reverse_iterator pointing to the last disjunct, if *this
is not empty; otherwise, returns the before-the-start const_reverse_iterator.
Definition at line 69 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::end().
00069 { 00070 return const_reverse_iterator(end()); 00071 }
Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend | ( | ) | const [inline] |
Returns the before-the-start const_reverse_iterator.
Definition at line 75 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin().
00075 { 00076 return const_reverse_iterator(begin()); 00077 }
void Parma_Polyhedra_Library::Powerset< D >::add_disjunct | ( | const D & | d | ) | [inline] |
Adds to *this
the disjunct d
.
Definition at line 158 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::drop_disjunct | ( | iterator | position | ) | [inline] |
Drops the disjunct in *this
pointed to by position
, returning an iterator to the disjunct following position
.
Definition at line 93 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::iterator_to_const< Container >::base, and Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::operator==().
00093 { 00094 return sequence.erase(position.base); 00095 }
void Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts | ( | iterator | first, | |
iterator | last | |||
) | [inline] |
Drops all the disjuncts from first
to last
(excluded).
Definition at line 99 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::iterator_to_const< Container >::base, and Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Powerset< D >::collapse().
00099 { 00100 sequence.erase(first.base, last.base); 00101 }
void Parma_Polyhedra_Library::Powerset< D >::clear | ( | ) | [inline] |
Drops all the disjuncts, making *this
an empty powerset.
Definition at line 105 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::sequence.
00105 { 00106 sequence.clear(); 00107 }
Powerset< D > & Parma_Polyhedra_Library::Powerset< D >::operator= | ( | const Powerset< D > & | y | ) | [inline] |
The assignment operator.
Definition at line 117 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.
void Parma_Polyhedra_Library::Powerset< D >::swap | ( | Powerset< D > & | y | ) | [inline] |
Swaps *this
with y
.
Definition at line 125 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Powerset< D >::swap().
void Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign | ( | const Powerset< D > & | y | ) | [inline] |
Assigns to *this
the least upper bound of *this
and y
.
Definition at line 233 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().
Referenced by Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign(), and Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign_if_exact().
00233 { 00234 // Ensure omega-reduction here, since what follows has quadratic complexity. 00235 omega_reduce(); 00236 y.omega_reduce(); 00237 iterator old_begin = begin(); 00238 iterator old_end = end(); 00239 for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i) 00240 old_begin = add_non_bottom_disjunct_preserve_reduction(*i, 00241 old_begin, 00242 old_end); 00243 assert(OK()); 00244 }
void Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign | ( | const Powerset< D > & | y | ) | [inline] |
Assigns to *this
an upper bound of *this
and y
.
The result will be the least upper bound of *this
and y
.
Definition at line 203 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign().
00203 { 00204 least_upper_bound_assign(y); 00205 }
bool Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign_if_exact | ( | const Powerset< D > & | y | ) | [inline] |
Assigns to *this
the least upper bound of *this
and y
and returns true
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 209 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign().
00209 { 00210 least_upper_bound_assign(y); 00211 return true; 00212 }
void Parma_Polyhedra_Library::Powerset< D >::meet_assign | ( | const Powerset< D > & | y | ) | [inline] |
Assigns to *this
the meet of *this
and y
.
Definition at line 197 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().
00197 { 00198 pairwise_apply_assign(y, std::mem_fun_ref(&D::meet_assign)); 00199 }
void Parma_Polyhedra_Library::Powerset< D >::collapse | ( | ) | [inline] |
If *this
is not empty (i.e., it is not the bottom element), it is reduced to a singleton obtained by computing an upper-bound of all the disjuncts.
Definition at line 190 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::empty(), and Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_extrapolation_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().
bool Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced | ( | ) | const [inline, protected] |
Returns true
if and only if *this
does not contain non-maximal elements.
Definition at line 141 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), and Parma_Polyhedra_Library::Powerset< D >::reduced.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::collect_certificates(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_universe().
00141 { 00142 if (!reduced && check_omega_reduced()) 00143 reduced = true; 00144 return reduced; 00145 }
void Parma_Polyhedra_Library::Powerset< D >::collapse | ( | unsigned | max_disjuncts | ) | [inline, protected] |
Upon return, *this
will contain at most max_disjuncts
elements; the set of disjuncts in positions greater than or equal to max_disjuncts
, will be replaced at that position by their upper-bound.
Definition at line 103 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::iterator_to_const< Container >::base, Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::size().
00103 { 00104 assert(max_disjuncts > 0); 00105 // Omega-reduce before counting the number of disjuncts. 00106 omega_reduce(); 00107 size_type n = size(); 00108 if (n > max_disjuncts) { 00109 // Let `i' point to the last disjunct that will survive. 00110 iterator i = begin(); 00111 std::advance(i, max_disjuncts-1); 00112 // This disjunct will be assigned an upper-bound of itself and of 00113 // all the disjuncts that follow. 00114 collapse(i.base); 00115 } 00116 assert(OK()); 00117 assert(is_omega_reduced()); 00118 }
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction | ( | const D & | d, | |
iterator | first, | |||
iterator | last | |||
) | [inline, protected] |
Adds to *this
the disjunct d
, assuming d
is not the bottom element and ensuring partial Omega-reduction.
If d
is not the bottom element and is not Omega-redundant with respect to elements in positions between first
and last
, all elements in these positions that would be made Omega-redundant by the addition of d
are dropped and d
is added to the reduced sequence. If *this
is reduced before an invocation of this method, it will be reduced upon successful return from the method.
Definition at line 149 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.
Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce().
00151 { 00152 assert(!d.is_bottom()); 00153 for (iterator xi = first; xi != last; ) { 00154 const D& xv = *xi; 00155 if (d.definitely_entails(xv)) 00156 return first; 00157 else if (xv.definitely_entails(d)) { 00158 if (xi == first) 00159 ++first; 00160 xi = drop_disjunct(xi); 00161 } 00162 else 00163 ++xi; 00164 } 00165 sequence.push_back(d); 00166 assert(OK()); 00167 return first; 00168 }
void Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction | ( | const D & | d | ) | [inline, protected] |
Adds to *this
the disjunct d
, assuming d
is not the bottom element and preserving Omega-reduction.
If *this
is reduced before an invocation of this method, it will be reduced upon successful return from the method.
Definition at line 151 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().
00151 { 00152 // !d.is_bottom() is asserted by the callee. 00153 add_non_bottom_disjunct_preserve_reduction(d, begin(), end()); 00154 }
void Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign | ( | const Powerset< D > & | y, | |
Binary_Operator_Assign | op_assign | |||
) | [inline, protected] |
Assigns to *this
the result of applying op_assign
pairwise to the elements in *this
and y
.
The elements of the powerset result are obtained by applying op_assign
to each pair of elements whose components are drawn from *this
and y
, respectively.
Definition at line 211 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign(), Parma_Polyhedra_Library::Powerset< D >::meet_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::time_elapse_assign().
00212 { 00213 // Ensure omega-reduction here, since what follows has quadratic complexity. 00214 omega_reduce(); 00215 y.omega_reduce(); 00216 Sequence new_sequence; 00217 for (const_iterator xi = begin(), x_end = end(), 00218 y_begin = y.begin(), y_end = y.end(); xi != x_end; ++xi) 00219 for (const_iterator yi = y_begin; yi != y_end; ++yi) { 00220 D zi = *xi; 00221 op_assign(zi, *yi); 00222 if (!zi.is_bottom()) 00223 new_sequence.push_back(zi); 00224 } 00225 // Put the new sequence in place. 00226 std::swap(sequence, new_sequence); 00227 reduced = false; 00228 assert(OK()); 00229 }
bool Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced | ( | ) | const [inline, private] |
Does the hard work of checking whether *this
contains non-maximal elements and returns true
if and only if it does not.
Definition at line 122 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().
Referenced by Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), and Parma_Polyhedra_Library::Powerset< D >::OK().
00122 { 00123 for (const_iterator x_begin = begin(), x_end = end(), 00124 xi = x_begin; xi != x_end; ++xi) { 00125 const D& xv = *xi; 00126 if (xv.is_bottom()) 00127 return false; 00128 for (const_iterator yi = x_begin; yi != x_end; ++yi) { 00129 if (xi == yi) 00130 continue; 00131 const D& yv = *yi; 00132 if (xv.definitely_entails(yv) || yv.definitely_entails(xv)) 00133 return false; 00134 } 00135 } 00136 return true; 00137 }
void Parma_Polyhedra_Library::Powerset< D >::collapse | ( | Sequence_iterator | sink | ) | [inline, private] |
Replaces the disjunct *sink
by an upper bound of itself and all the disjuncts following it.
Definition at line 34 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.
00034 { 00035 assert(sink != sequence.end()); 00036 D& d = *sink; 00037 iterator x_sink = sink; 00038 iterator next_x_sink = x_sink; 00039 ++next_x_sink; 00040 iterator x_end = end(); 00041 for (const_iterator xi = next_x_sink; xi != x_end; ++xi) 00042 d.upper_bound_assign(*xi); 00043 // Drop the surplus disjuncts. 00044 drop_disjuncts(next_x_sink, x_end); 00045 00046 // Ensure omega-reduction. 00047 for (iterator xi = begin(); xi != x_sink; ) 00048 if (xi->definitely_entails(d)) 00049 xi = drop_disjunct(xi); 00050 else 00051 ++xi; 00052 00053 assert(OK()); 00054 }
Returns true
if and only if x
and y
are equivalent.
Definition at line 188 of file Powerset.templates.hh.
References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::size().
00188 { 00189 x.omega_reduce(); 00190 y.omega_reduce(); 00191 if (x.size() != y.size()) 00192 return false; 00193 // Take a copy of `y' and work with it. 00194 Powerset<D> yy = y; 00195 for (typename Powerset<D>::const_iterator xi = x.begin(), 00196 x_end = x.end(); xi != x_end; ++xi) { 00197 typename Powerset<D>::iterator yyi = yy.begin(); 00198 typename Powerset<D>::iterator yy_end = yy.end(); 00199 yyi = std::find(yyi, yy_end, *xi); 00200 if (yyi == yy_end) 00201 return false; 00202 else 00203 yy.drop_disjunct(yyi); 00204 } 00205 return true; 00206 }
Returns true
if and only if x
and y
are not equivalent.
Definition at line 166 of file Powerset.inlines.hh.
std::ostream & operator<< | ( | std::ostream & | s, | |
const Powerset< D > & | x | |||
) | [related] |
Output operator.
Definition at line 251 of file Powerset.templates.hh.
00251 { 00252 if (x.is_bottom()) 00253 s << "false"; 00254 else if (x.is_top()) 00255 s << "true"; 00256 else 00257 for (typename Powerset<D>::const_iterator i = x.begin(), 00258 x_end = x.end(); i != x_end; ) { 00259 s << "{ " << *i++ << " }"; 00260 if (i != x_end) 00261 s << ", "; 00262 } 00263 return s; 00264 }
void swap | ( | Parma_Polyhedra_Library::Powerset< D > & | x, | |
Parma_Polyhedra_Library::Powerset< D > & | y | |||
) | [related] |
Specializes std::swap
.
Definition at line 228 of file Powerset.inlines.hh.
References Parma_Polyhedra_Library::Powerset< D >::swap().
00229 { 00230 x.swap(y); 00231 }
Sequence Parma_Polyhedra_Library::Powerset< D >::sequence [protected] |
The sequence container holding powerset's elements.
Definition at line 228 of file Powerset.defs.hh.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints_and_minimize(), Parma_Polyhedra_Library::Powerset< D >::add_disjunct(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_preimage(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_above(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_below(), Parma_Polyhedra_Library::Powerset< D >::clear(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::contains(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::contains_integer_point(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts(), Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::expand_space_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::fold_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_preserving_enlarge_element(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_bounded(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_discrete(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_disjoint_from(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_topologically_closed(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::map_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::maximize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::minimize(), Parma_Polyhedra_Library::Powerset< D >::operator=(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset(), Parma_Polyhedra_Library::Powerset< D >::Powerset(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::relation_with(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign(), Parma_Polyhedra_Library::Powerset< D >::size(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::strictly_contains(), Parma_Polyhedra_Library::Powerset< D >::swap(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::topological_closure_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::unconstrain().
bool Parma_Polyhedra_Library::Powerset< D >::reduced [mutable, protected] |
If true
, *this
is Omega-reduced.
Definition at line 231 of file Powerset.defs.hh.
Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints_and_minimize(), Parma_Polyhedra_Library::Powerset< D >::add_disjunct(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_preimage(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::map_space_dimensions(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::operator=(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign(), Parma_Polyhedra_Library::Powerset< D >::swap(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::unconstrain().