1 /* Grid_Certificate 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_Grid_Certificate_defs_hh 25 #define PPL_Grid_Certificate_defs_hh 1 26 27 #include "Grid_Certificate_types.hh" 28 29 #include "Grid_types.hh" 30 #include "globals_defs.hh" 31 #include <vector> 32 33 //! The convergence certificate for the Grid widening operator. 34 /*! \ingroup PPL_CXX_interface 35 Convergence certificates are used to instantiate the BHZ03 framework 36 so as to define widening operators for the finite powerset domain. 37 38 \note 39 Each convergence certificate has to be used together with a 40 compatible widening operator. In particular, Grid_Certificate can 41 certify the Grid widening. 42 */ 43 class Parma_Polyhedra_Library::Grid_Certificate { 44 public: 45 //! Default constructor. 46 Grid_Certificate(); 47 48 //! Constructor: computes the certificate for \p gr. 49 Grid_Certificate(const Grid& gr); 50 51 //! Copy constructor. 52 Grid_Certificate(const Grid_Certificate& y); 53 54 //! Destructor. 55 ~Grid_Certificate(); 56 57 //! The comparison function for certificates. 58 /*! 59 \return 60 \f$-1\f$, \f$0\f$ or \f$1\f$ depending on whether \p *this 61 is smaller than, equal to, or greater than \p y, respectively. 62 */ 63 int compare(const Grid_Certificate& y) const; 64 65 //! Compares \p *this with the certificate for grid \p gr. 66 int compare(const Grid& gr) const; 67 68 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 69 /*! \brief 70 Returns <CODE>true</CODE> if and only if the certificate for grid 71 \p gr is strictly smaller than \p *this. 72 */ 73 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 74 bool is_stabilizing(const Grid& gr) const; 75 76 //! A total ordering on Grid certificates. 77 /*! 78 This binary predicate defines a total ordering on Grid certificates 79 which is used when storing information about sets of grids. 80 */ 81 struct Compare { 82 //! Returns <CODE>true</CODE> if and only if \p x comes before \p y. 83 bool operator()(const Grid_Certificate& x, 84 const Grid_Certificate& y) const; 85 }; 86 87 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 88 //! Check if gathered information is meaningful. 89 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 90 bool OK() const; 91 92 private: 93 //! Number of a equalities in a minimized congruence system for the 94 //! grid. 95 dimension_type num_equalities; 96 //! Number of a proper congruences in a minimized congruence system 97 //! for the grid. 98 dimension_type num_proper_congruences; 99 }; 100 101 #include "Grid_Certificate_inlines.hh" 102 103 #endif // !defined(PPL_Grid_Certificate_defs_hh) 104