1 /* Poly_Con_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_Con_Relation_defs_hh 25 #define PPL_Poly_Con_Relation_defs_hh 1 26 27 #include "Poly_Con_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_Con_Relation */ 37 bool operator==(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 38 39 //! True if and only if \p x and \p y are not logically equivalent. 40 /*! \relates Poly_Con_Relation */ 41 bool operator!=(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 42 43 //! Yields the logical conjunction of \p x and \p y. 44 /*! \relates Poly_Con_Relation */ 45 Poly_Con_Relation operator&&(const Poly_Con_Relation& x, 46 const Poly_Con_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_Con_Relation 53 */ 54 Poly_Con_Relation operator-(const Poly_Con_Relation& x, 55 const Poly_Con_Relation& y); 56 57 namespace IO_Operators { 58 59 //! Output operator. 60 /*! \relates Parma_Polyhedra_Library::Poly_Con_Relation */ 61 std::ostream& operator<<(std::ostream& s, const Poly_Con_Relation& r); 62 63 } // namespace IO_Operators 64 65 } // namespace Parma_Polyhedra_Library 66 67 68 //! The relation between a polyhedron and a constraint. 69 /*! \ingroup PPL_CXX_interface 70 This class implements conjunctions of assertions on the relation 71 between a polyhedron and a constraint. 72 */ 73 class Parma_Polyhedra_Library::Poly_Con_Relation { 74 private: 75 //! Poly_Con_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 IS_DISJOINT = 1U << 0; 82 static const flags_t STRICTLY_INTERSECTS = 1U << 1; 83 static const flags_t IS_INCLUDED = 1U << 2; 84 static const flags_t SATURATES = 1U << 3; 85 //@} // Bit-masks for the individual assertions 86 87 //! All assertions together. 88 static const flags_t EVERYTHING 89 = IS_DISJOINT 90 | STRICTLY_INTERSECTS 91 | IS_INCLUDED 92 | SATURATES; 93 94 //! This holds the current bitset. 95 flags_t flags; 96 97 //! True if and only if the conjunction \p x implies the conjunction \p y. 98 static bool implies(flags_t x, flags_t y); 99 100 //! Construct from a bit-mask. 101 Poly_Con_Relation(flags_t mask); 102 103 friend bool 104 operator==(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 105 friend bool 106 operator!=(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 107 108 friend Poly_Con_Relation 109 operator&&(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 110 111 friend Poly_Con_Relation 112 operator-(const Poly_Con_Relation& x, const Poly_Con_Relation& y); 113 114 friend std::ostream& 115 Parma_Polyhedra_Library:: 116 IO_Operators::operator<<(std::ostream& s, const Poly_Con_Relation& r); 117 118 public: 119 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 120 /*! \brief 121 Access the internal flags: this is needed for some language 122 interfaces. 123 */ 124 #endif 125 flags_t get_flags() const; 126 127 public: 128 //! The assertion that says nothing. 129 static Poly_Con_Relation nothing(); 130 131 /*! \brief 132 The polyhedron and the set of points satisfying 133 the constraint are disjoint. 134 */ 135 static Poly_Con_Relation is_disjoint(); 136 137 /*! \brief 138 The polyhedron intersects the set of points satisfying 139 the constraint, but it is not included in it. 140 */ 141 static Poly_Con_Relation strictly_intersects(); 142 143 /*! \brief 144 The polyhedron is included in the set of points satisfying 145 the constraint. 146 */ 147 static Poly_Con_Relation is_included(); 148 149 /*! \brief 150 The polyhedron is included in the set of points saturating 151 the constraint. 152 */ 153 static Poly_Con_Relation saturates(); 154 155 PPL_OUTPUT_DECLARATIONS 156 157 //! True if and only if \p *this implies \p y. 158 bool implies(const Poly_Con_Relation& y) const; 159 160 //! Checks if all the invariants are satisfied. 161 bool OK() const; 162 }; 163 164 #include "Poly_Con_Relation_inlines.hh" 165 166 #endif // !defined(PPL_Poly_Con_Relation_defs_hh) 167