From ede95f2eabeab645352a36af072ee998c400bca1 Mon Sep 17 00:00:00 2001 From: Anas Nashif Date: Tue, 6 Nov 2012 07:10:54 -0800 Subject: Imported Upstream version 0.11.2 --- src/Determinate.defs.hh | 337 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 337 insertions(+) create mode 100644 src/Determinate.defs.hh (limited to 'src/Determinate.defs.hh') diff --git a/src/Determinate.defs.hh b/src/Determinate.defs.hh new file mode 100644 index 000000000..668f9e74c --- /dev/null +++ b/src/Determinate.defs.hh @@ -0,0 +1,337 @@ +/* Determinate class declaration. + Copyright (C) 2001-2010 Roberto Bagnara + Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com) + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#ifndef PPL_Determinate_defs_hh +#define PPL_Determinate_defs_hh + +#include "Determinate.types.hh" +#include "Constraint_System.types.hh" +#include "Congruence_System.types.hh" +#include "Variable.defs.hh" +#include "globals.types.hh" +#include +#include "assert.hh" + +namespace Parma_Polyhedra_Library { + +/*! \brief + Returns true if and only if \p x and \p y are the same + COW-wrapped pointset. + + \relates Determinate +*/ +template +bool operator==(const Determinate& x, const Determinate& y); + +/*! \brief + Returns true if and only if \p x and \p y are different + COW-wrapped pointsets. + + \relates Determinate +*/ +template +bool operator!=(const Determinate& x, const Determinate& y); + +namespace IO_Operators { + +//! Output operator. +/*! \relates Parma_Polyhedra_Library::Determinate */ +template +std::ostream& +operator<<(std::ostream&, const Determinate&); + +} // namespace IO_Operators + +} // namespace Parma_Polyhedra_Library + +/*! \brief + A wrapper for PPL pointsets, providing them with a + determinate constraint system interface, as defined + in \ref Bag98 "[Bag98]". + + The implementation uses a copy-on-write optimization, making the + class suitable for constructions, like the finite powerset + and ask-and-tell of \ref Bag98 "[Bag98]", that are likely + to perform many copies. + + \ingroup PPL_CXX_interface +*/ +template +class Parma_Polyhedra_Library::Determinate { +public: + //! \name Constructors and Destructor + //@{ + + /*! \brief + Constructs a COW-wrapped object corresponding to the pointset \p p. + */ + Determinate(const PSET& p); + + /*! \brief + Constructs a COW-wrapped object corresponding to the pointset + defined by \p cs. + */ + Determinate(const Constraint_System& cs); + + /*! \brief + Constructs a COW-wrapped object corresponding to the pointset + defined by \p cgs. + */ + Determinate(const Congruence_System& cgs); + + //! Copy constructor. + Determinate(const Determinate& y); + + //! Destructor. + ~Determinate(); + + //@} // Constructors and Destructor + + //! \name Member Functions that Do Not Modify the Domain Element + //@{ + + //! Returns a const reference to the embedded pointset. + const PSET& pointset() const; + + /*! \brief + Returns true if and only if \p *this embeds the universe + element \p PSET. + */ + bool is_top() const; + + /*! \brief + Returns true if and only if \p *this embeds the empty + element of \p PSET. + */ + bool is_bottom() const; + + //! Returns true if and only if \p *this entails \p y. + bool definitely_entails(const Determinate& y) const; + + /*! \brief + Returns true if and only if \p *this and \p y + are definitely equivalent. + */ + bool is_definitely_equivalent_to(const Determinate& y) const; + + /*! \brief + Returns a lower bound to the total size in bytes of the memory + occupied by \p *this. + */ + memory_size_type total_memory_in_bytes() const; + + /*! \brief + Returns a lower bound to the size in bytes of the memory + managed by \p *this. + */ + memory_size_type external_memory_in_bytes() const; + + /*! + Returns true if and only if this domain + has a nontrivial weakening operator. + */ + static bool has_nontrivial_weakening(); + + //! Checks if all the invariants are satisfied. + bool OK() const; + + //@} // Member Functions that Do Not Modify the Domain Element + + + //! \name Member Functions that May Modify the Domain Element + //@{ + + //! Assigns to \p *this the upper bound of \p *this and \p y. + void upper_bound_assign(const Determinate& y); + + //! Assigns to \p *this the meet of \p *this and \p y. + void meet_assign(const Determinate& y); + + //! Assigns to \p *this the result of weakening \p *this with \p y. + void weakening_assign(const Determinate& y); + + /*! \brief + Assigns to \p *this the \ref Concatenating_Polyhedra "concatenation" + of \p *this and \p y, taken in this order. + */ + void concatenate_assign(const Determinate& y); + + //! Returns a reference to the embedded element. + PSET& pointset(); + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS + /*! \brief + On return from this method, the representation of \p *this + is not shared by different Determinate objects. + */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + void mutate(); + + //! Assignment operator. + Determinate& operator=(const Determinate& y); + + //! Swaps \p *this with \p y. + void swap(Determinate& y); + + //@} // Member Functions that May Modify the Domain Element + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS + //! A function adapter for the Determinate class. + /*! \ingroup PPL_CXX_interface + It lifts a Binary_Operator_Assign function object, taking arguments + of type PSET, producing the corresponding function object taking + arguments of type Determinate. + + The template parameter Binary_Operator_Assign is supposed to + implement an apply and assign function, i.e., a function + having signature void foo(PSET& x, const PSET& y) that + applies an operator to \c x and \c y and assigns the result to \c x. + For instance, such a function object is obtained by + std::mem_fun_ref(&C_Polyhedron::intersection_assign). + */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + template + class Binary_Operator_Assign_Lifter { + public: + //! Explicit unary constructor. + explicit + Binary_Operator_Assign_Lifter(Binary_Operator_Assign op_assign); + + //! Function-application operator. + void operator()(Determinate& x, const Determinate& y) const; + + private: + //! The function object to be lifted. + Binary_Operator_Assign op_assign_; + }; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS + /*! \brief + Helper function returning a Binary_Operator_Assign_Lifter object, + also allowing for the deduction of template arguments. + */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + template + static Binary_Operator_Assign_Lifter + lift_op_assign(Binary_Operator_Assign op_assign); + +private: + //! The possibly shared representation of a Determinate object. + /*! \ingroup PPL_CXX_interface + By adopting the copy-on-write technique, a single + representation of the base-level object may be shared by more than + one object of the class Determinate. + */ + class Rep { + private: + /*! \brief + Count the number of references: + - 0: leaked, \p pset is non-const; + - 1: one reference, \p pset is non-const; + - > 1: more than one reference, \p pset is const. + */ + mutable unsigned long references; + + //! Private and unimplemented: assignment not allowed. + Rep& operator=(const Rep& y); + + //! Private and unimplemented: copies not allowed. + Rep(const Rep& y); + + //! Private and unimplemented: default construction not allowed. + Rep(); + + public: + //! The possibly shared, embedded pointset. + PSET pset; + + /*! \brief + Builds a new representation by creating a pointset + of the specified kind, in the specified vector space. + */ + Rep(dimension_type num_dimensions, Degenerate_Element kind); + + //! Builds a new representation by copying the pointset \p p. + Rep(const PSET& p); + + //! Builds a new representation by copying the constraints in \p cs. + Rep(const Constraint_System& cs); + + //! Builds a new representation by copying the constraints in \p cgs. + Rep(const Congruence_System& cgs); + + //! Destructor. + ~Rep(); + + //! Registers a new reference. + void new_reference() const; + + /*! \brief + Unregisters one reference; returns true if and only if + the representation has become unreferenced. + */ + bool del_reference() const; + + //! True if and only if this representation is currently shared. + bool is_shared() const; + + /*! \brief + Returns a lower bound to the total size in bytes of the memory + occupied by \p *this. + */ + memory_size_type total_memory_in_bytes() const; + + /*! \brief + Returns a lower bound to the size in bytes of the memory + managed by \p *this. + */ + memory_size_type external_memory_in_bytes() const; + }; + + /*! \brief + A pointer to the possibly shared representation of + the base-level domain element. + */ + Rep* prep; + + friend bool + operator==(const Determinate& x, const Determinate& y); + + friend bool + operator!=(const Determinate& x, const Determinate& y); +}; + + +namespace std { + +//! Specializes std::swap. +/*! \relates Parma_Polyhedra_Library::Determinate */ +template +void swap(Parma_Polyhedra_Library::Determinate& x, + Parma_Polyhedra_Library::Determinate& y); + +} // namespace std + +#include "Determinate.inlines.hh" + +#endif // !defined(PPL_Determinate_defs_hh) -- cgit v1.2.3