1 /* H79_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_H79_Certificate_defs_hh 25 #define PPL_H79_Certificate_defs_hh 1 26 27 #include "H79_Certificate_types.hh" 28 #include "Polyhedron_types.hh" 29 #include "globals_types.hh" 30 #include <vector> 31 32 //! A convergence certificate for the H79 widening operator. 33 /*! \ingroup PPL_CXX_interface 34 Convergence certificates are used to instantiate the BHZ03 framework 35 so as to define widening operators for the finite powerset domain. 36 \note 37 The convergence of the H79 widening can also be certified by 38 BHRZ03_Certificate. 39 */ 40 class Parma_Polyhedra_Library::H79_Certificate { 41 public: 42 //! Default constructor. 43 H79_Certificate(); 44 45 //! Constructor: computes the certificate for \p ph. 46 template <typename PH> 47 H79_Certificate(const PH& ph); 48 49 //! Constructor: computes the certificate for \p ph. 50 H79_Certificate(const Polyhedron& ph); 51 52 //! Copy constructor. 53 H79_Certificate(const H79_Certificate& y); 54 55 //! Destructor. 56 ~H79_Certificate(); 57 58 //! The comparison function for certificates. 59 /*! 60 \return 61 \f$-1\f$, \f$0\f$ or \f$1\f$ depending on whether \p *this 62 is smaller than, equal to, or greater than \p y, respectively. 63 64 Compares \p *this with \p y, using a total ordering which is a 65 refinement of the limited growth ordering relation for the 66 H79 widening. 67 */ 68 int compare(const H79_Certificate& y) const; 69 70 //! Compares \p *this with the certificate for polyhedron \p ph. 71 template <typename PH> 72 int compare(const PH& ph) const; 73 74 //! Compares \p *this with the certificate for polyhedron \p ph. 75 int compare(const Polyhedron& ph) const; 76 77 //! A total ordering on H79 certificates. 78 /*! \ingroup PPL_CXX_interface 79 This binary predicate defines a total ordering on H79 certificates 80 which is used when storing information about sets of polyhedra. 81 */ 82 struct Compare { 83 //! Returns <CODE>true</CODE> if and only if \p x comes before \p y. 84 bool operator()(const H79_Certificate& x, 85 const H79_Certificate& y) const; 86 }; 87 88 private: 89 //! Affine dimension of the polyhedron. 90 dimension_type affine_dim; 91 //! Cardinality of a non-redundant constraint system for the polyhedron. 92 dimension_type num_constraints; 93 }; 94 95 #include "H79_Certificate_inlines.hh" 96 97 #endif // !defined(PPL_H79_Certificate_defs_hh) 98