1 /* Poly_Gen_Relation class declaration. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_Poly_Gen_Relation_defs_hh 25 #define PPL_Poly_Gen_Relation_defs_hh 1 26 27 #include "Poly_Gen_Relation_types.hh" 28 #include "globals_defs.hh" 29 #include <iosfwd> 30 31 namespace Parma_Polyhedra_Library { 32 33 // Put them in the namespace here to declare them friend later. 34 35 //! True if and only if \p x and \p y are logically equivalent. 36 /*! \relates Poly_Gen_Relation */ 37 bool operator==(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 38 39 //! True if and only if \p x and \p y are not logically equivalent. 40 /*! \relates Poly_Gen_Relation */ 41 bool operator!=(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 42 43 //! Yields the logical conjunction of \p x and \p y. 44 /*! \relates Poly_Gen_Relation */ 45 Poly_Gen_Relation operator&&(const Poly_Gen_Relation& x, 46 const Poly_Gen_Relation& y); 47 48 /*! \brief 49 Yields the assertion with all the conjuncts of \p x 50 that are not in \p y. 51 52 \relates Poly_Gen_Relation 53 */ 54 Poly_Gen_Relation operator-(const Poly_Gen_Relation& x, 55 const Poly_Gen_Relation& y); 56 57 namespace IO_Operators { 58 59 //! Output operator. 60 /*! \relates Parma_Polyhedra_Library::Poly_Gen_Relation */ 61 std::ostream& operator<<(std::ostream& s, const Poly_Gen_Relation& r); 62 63 } // namespace IO_Operators 64 65 } // namespace Parma_Polyhedra_Library 66 67 68 //! The relation between a polyhedron and a generator 69 /*! \ingroup PPL_CXX_interface 70 This class implements conjunctions of assertions on the relation 71 between a polyhedron and a generator. 72 */ 73 class Parma_Polyhedra_Library::Poly_Gen_Relation { 74 private: 75 //! Poly_Gen_Relation is implemented by means of a finite bitset. 76 typedef unsigned int flags_t; 77 78 //! \name Bit-masks for the individual assertions 79 //@{ 80 static const flags_t NOTHING = 0U; 81 static const flags_t SUBSUMES = 1U << 0; 82 //@} // Bit-masks for the individual assertions 83 84 //! All assertions together. 85 static const flags_t EVERYTHING 86 = SUBSUMES; 87 88 //! This holds the current bitset. 89 flags_t flags; 90 91 //! True if and only if the conjunction \p x implies the conjunction \p y. 92 static bool implies(flags_t x, flags_t y); 93 94 //! Construct from a bit-mask. 95 Poly_Gen_Relation(flags_t mask); 96 97 friend bool 98 operator==(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 99 friend bool 100 operator!=(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 101 102 friend Poly_Gen_Relation 103 operator&&(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 104 105 friend Poly_Gen_Relation 106 operator-(const Poly_Gen_Relation& x, const Poly_Gen_Relation& y); 107 108 friend std::ostream& 109 Parma_Polyhedra_Library:: 110 IO_Operators::operator<<(std::ostream& s, const Poly_Gen_Relation& r); 111 112 public: 113 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 114 /*! \brief 115 Access the internal flags: this is needed for some language 116 interfaces. 117 */ 118 #endif 119 flags_t get_flags() const; 120 121 public: 122 //! The assertion that says nothing. 123 static Poly_Gen_Relation nothing(); 124 125 //! Adding the generator would not change the polyhedron. 126 static Poly_Gen_Relation subsumes(); 127 128 PPL_OUTPUT_DECLARATIONS 129 130 //! True if and only if \p *this implies \p y. 131 bool implies(const Poly_Gen_Relation& y) const; 132 133 //! Checks if all the invariants are satisfied. 134 bool OK() const; 135 }; 136 137 #include "Poly_Gen_Relation_inlines.hh" 138 139 #endif // !defined(PPL_Poly_Gen_Relation_defs_hh) 140