1 /* H79_Certificate class implementation
2 (non-inline member functions).
3 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
4 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
5
6 This file is part of the Parma Polyhedra Library (PPL).
7
8 The PPL is free software; you can redistribute it and/or modify it
9 under the terms of the GNU General Public License as published by the
10 Free Software Foundation; either version 3 of the License, or (at your
11 option) any later version.
12
13 The PPL is distributed in the hope that it will be useful, but WITHOUT
14 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
15 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
16 for more details.
17
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software Foundation,
20 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
21
22 For the most up-to-date information see the Parma Polyhedra Library
23 site: http://bugseng.com/products/ppl/ . */
24
25 #include "ppl-config.h"
26 #include "H79_Certificate_defs.hh"
27 #include "Polyhedron_defs.hh"
28 #include "assertions.hh"
29 #include <iostream>
30
31 namespace PPL = Parma_Polyhedra_Library;
32
H79_Certificate(const Polyhedron & ph)33 PPL::H79_Certificate::H79_Certificate(const Polyhedron& ph)
34 : affine_dim(0), num_constraints(0) {
35 // The affine dimension of the polyhedron is obtained by subtracting
36 // the number of equalities from the space dimension.
37 // When counting constraints, for a correct reasoning, we have
38 // to disregard the low-level constraints (i.e., the positivity
39 // constraint and epsilon bounds).
40 const dimension_type space_dim = ph.space_dimension();
41 affine_dim = space_dim;
42 const Constraint_System& cs = ph.minimized_constraints();
43 // It is assumed that `ph' is not an empty polyhedron.
44 PPL_ASSERT(!ph.marked_empty());
45 for (Constraint_System::const_iterator i = cs.begin(),
46 cs_end = cs.end(); i != cs_end; ++i) {
47 ++num_constraints;
48 if (i->is_equality()) {
49 --affine_dim;
50 }
51 }
52
53 // TODO: this is an inefficient workaround.
54 // For NNC polyhedra, generators might be no longer up-to-date
55 // (and hence, neither minimized) due to the strong minimization
56 // process applied to constraints when constructing the certificate.
57 // We have to reinforce the (normal) minimization of the generator
58 // system. The future, lazy implementation of the strong minimization
59 // process will solve this problem.
60 if (!ph.is_necessarily_closed()) {
61 ph.minimize();
62 }
63 }
64
65 int
compare(const H79_Certificate & y) const66 PPL::H79_Certificate::compare(const H79_Certificate& y) const {
67 if (affine_dim != y.affine_dim) {
68 return (affine_dim > y.affine_dim) ? 1 : -1;
69 }
70 if (num_constraints != y.num_constraints) {
71 return (num_constraints > y.num_constraints) ? 1 : -1;
72 }
73 // All components are equal.
74 return 0;
75 }
76
77 int
compare(const Polyhedron & ph) const78 PPL::H79_Certificate::compare(const Polyhedron& ph) const {
79 // The affine dimension of the polyhedron is obtained by subtracting
80 // the number of equalities from the space dimension.
81 // When counting constraints, for a correct reasoning, we have
82 // to disregard the low-level constraints (i.e., the positivity
83 // constraint and epsilon bounds).
84 const dimension_type space_dim = ph.space_dimension();
85 dimension_type ph_affine_dim = space_dim;
86 dimension_type ph_num_constraints = 0;
87 const Constraint_System& cs = ph.minimized_constraints();
88 // It is assumed that `ph' is a polyhedron containing the
89 // polyhedron described by `*this': hence, it cannot be empty.
90 PPL_ASSERT(!ph.marked_empty());
91 for (Constraint_System::const_iterator i = cs.begin(),
92 cs_end = cs.end(); i != cs_end; ++i) {
93 ++ph_num_constraints;
94 if (i->is_equality()) {
95 --ph_affine_dim;
96 }
97 }
98 // TODO: this is an inefficient workaround.
99 // For NNC polyhedra, generators might be no longer up-to-date
100 // (and hence, neither minimized) due to the strong minimization
101 // process applied to constraints when constructing the certificate.
102 // We have to reinforce the (normal) minimization of the generator
103 // system. The future, lazy implementation of the strong minimization
104 // process will solve this problem.
105 if (!ph.is_necessarily_closed()) {
106 ph.minimize();
107 }
108
109 // If the affine dimension of `ph' is increasing, the chain is stabilizing.
110 if (ph_affine_dim > affine_dim) {
111 return 1;
112 }
113
114 // At this point the two polyhedra must have the same affine dimension.
115 PPL_ASSERT(ph_affine_dim == affine_dim);
116
117 // If the number of constraints of `ph' is decreasing, then the chain
118 // is stabilizing. If it is increasing, the chain is not stabilizing.
119 if (ph_num_constraints != num_constraints) {
120 return (ph_num_constraints < num_constraints) ? 1 : -1;
121 }
122
123 // All components are equal.
124 return 0;
125 }
126