1 /* Congruence class implementation (non-inline functions).
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 #include "ppl-config.h"
25 #include "Congruence_defs.hh"
26 #include "Variable_defs.hh"
27 #include "Constraint_defs.hh"
28 #include "assertions.hh"
29 #include <iostream>
30 #include <sstream>
31 #include <stdexcept>
32 #include <string>
33
34 namespace PPL = Parma_Polyhedra_Library;
35
Congruence(const Constraint & c,Representation r)36 PPL::Congruence::Congruence(const Constraint& c, Representation r)
37 : expr(c.expression(), c.space_dimension(), r),
38 modulus_(0) {
39 if (!c.is_equality()) {
40 throw_invalid_argument("Congruence(c, r)",
41 "constraint c must be an equality.");
42 }
43 }
44
Congruence(const Constraint & c,dimension_type new_space_dimension,Representation r)45 PPL::Congruence::Congruence(const Constraint& c,
46 dimension_type new_space_dimension,
47 Representation r)
48 : expr(c.expression(), new_space_dimension, r),
49 modulus_(0) {
50 if (!c.is_equality()) {
51 throw_invalid_argument("Congruence(c, space_dim, r)",
52 "constraint c must be an equality.");
53 }
54 }
55
56 void
sign_normalize()57 PPL::Congruence::sign_normalize() {
58 expr.sign_normalize();
59 }
60
61 void
normalize()62 PPL::Congruence::normalize() {
63 PPL_ASSERT(OK());
64 sign_normalize();
65
66 if (modulus_ == 0) {
67 return;
68 }
69
70 PPL_DIRTY_TEMP_COEFFICIENT(c);
71 c = expr.inhomogeneous_term();
72 // Factor the modulus out of the inhomogeneous term.
73 c %= modulus_;
74 if (c < 0) {
75 // Make inhomogeneous term positive.
76 c += modulus_;
77 }
78 expr.set_inhomogeneous_term(c);
79
80 PPL_ASSERT(OK());
81 }
82
83 void
strong_normalize()84 PPL::Congruence::strong_normalize() {
85 normalize();
86
87 Coefficient gcd = expr.gcd(0, expr.space_dimension() + 1);
88 if (gcd == 0) {
89 gcd = modulus_;
90 }
91 else {
92 gcd_assign(gcd, modulus_, gcd);
93 }
94
95 if (gcd != 0 && gcd != 1) {
96 expr /= gcd;
97 modulus_ /= gcd;
98 }
99 PPL_ASSERT(OK());
100 }
101
102 void
scale(Coefficient_traits::const_reference factor)103 PPL::Congruence::scale(Coefficient_traits::const_reference factor) {
104 if (factor == 1) {
105 // Nothing to do.
106 return;
107 }
108
109 expr *= factor;
110 modulus_ *= factor;
111 }
112
113 void
114 PPL::Congruence
affine_preimage(Variable v,const Linear_Expression & e,Coefficient_traits::const_reference denominator)115 ::affine_preimage(Variable v, const Linear_Expression& e,
116 Coefficient_traits::const_reference denominator) {
117 PPL_DIRTY_TEMP_COEFFICIENT(c);
118 c = expr.get(v);
119
120 if (c == 0) {
121 return;
122 }
123
124 scale(denominator);
125
126 expr.linear_combine(e, 1, c, 0, e.space_dimension() + 1);
127
128 if (v.space_dimension() > e.space_dimension() || e.get(v) == 0) {
129 // Not invertible
130 expr.set(v, Coefficient_zero());
131 }
132 else {
133 c *= e.get(v);
134 expr.set(v, c);
135 }
136 }
137
138 PPL::Congruence
create(const Linear_Expression & e1,const Linear_Expression & e2,Representation r)139 PPL::Congruence::create(const Linear_Expression& e1,
140 const Linear_Expression& e2,
141 Representation r) {
142 Linear_Expression e(e1,
143 std::max(e1.space_dimension(), e2.space_dimension()),
144 r);
145 e -= e2;
146 return Congruence(e, 1, Recycle_Input());
147 }
148
149 void
throw_invalid_argument(const char * method,const char * message) const150 PPL::Congruence::throw_invalid_argument(const char* method,
151 const char* message) const {
152 std::ostringstream s;
153 s << "PPL::Congruence::" << method << ":" << std::endl
154 << message;
155 throw std::invalid_argument(s.str());
156 }
157
158 void
throw_dimension_incompatible(const char * method,const char * v_name,const Variable v) const159 PPL::Congruence::throw_dimension_incompatible(const char* method,
160 const char* v_name,
161 const Variable v) const {
162 std::ostringstream s;
163 s << "this->space_dimension() == " << space_dimension() << ", "
164 << v_name << ".space_dimension() == " << v.space_dimension() << ".";
165 const std::string str = s.str();
166 throw_invalid_argument(method, str.c_str());
167 }
168
169 /*! \relates Parma_Polyhedra_Library::Congruence */
170 std::ostream&
operator <<(std::ostream & s,const Congruence & c)171 PPL::IO_Operators::operator<<(std::ostream& s, const Congruence& c) {
172 const dimension_type num_variables = c.space_dimension();
173 PPL_DIRTY_TEMP_COEFFICIENT(cv);
174 bool first = true;
175 const Congruence::expr_type c_e = c.expression();
176 for (Congruence::expr_type::const_iterator i = c_e.begin(),
177 i_end = c_e.lower_bound(Variable(num_variables)); i != i_end; ++i) {
178 cv = *i;
179 if (!first) {
180 if (cv > 0) {
181 s << " + ";
182 }
183 else {
184 s << " - ";
185 neg_assign(cv);
186 }
187 }
188 else {
189 first = false;
190 }
191 if (cv == -1) {
192 s << "-";
193 }
194 else if (cv != 1) {
195 s << cv << "*";
196 }
197 s << i.variable();
198 }
199 if (first) {
200 s << Coefficient_zero();
201 }
202 s << " = " << -c.inhomogeneous_term();
203 if (c.is_proper_congruence()) {
204 s << " (mod " << c.modulus() << ")";
205 }
206 return s;
207 }
208
209 bool
is_tautological() const210 PPL::Congruence::is_tautological() const {
211 if (is_equality()) {
212 return (inhomogeneous_term() == 0) && expr.all_homogeneous_terms_are_zero();
213 }
214 return (inhomogeneous_term() % modulus() == 0) && expr.all_homogeneous_terms_are_zero();
215 }
216
217 bool
is_inconsistent() const218 PPL::Congruence::is_inconsistent() const {
219 if (is_equality()) {
220 return (inhomogeneous_term() != 0) && expr.all_homogeneous_terms_are_zero();
221 }
222
223 return (inhomogeneous_term() % modulus() != 0) && expr.all_homogeneous_terms_are_zero();
224 }
225
226 void
ascii_dump(std::ostream & s) const227 PPL::Congruence::ascii_dump(std::ostream& s) const {
228 expr.ascii_dump(s);
229 s << " m " << modulus_ << std::endl;
230 }
231
PPL_OUTPUT_DEFINITIONS(Congruence)232 PPL_OUTPUT_DEFINITIONS(Congruence)
233
234 bool
235 PPL::Congruence::ascii_load(std::istream& s) {
236 expr.ascii_load(s);
237
238 std::string str;
239 if (!(s >> str) || str != "m") {
240 return false;
241 }
242
243 if (!(s >> modulus_)) {
244 return false;
245 }
246
247 PPL_ASSERT(OK());
248 return true;
249 }
250
251 bool
OK() const252 PPL::Congruence::OK() const {
253 // Modulus check.
254 if (modulus() < 0) {
255 #ifndef NDEBUG
256 std::cerr << "Congruence has a negative modulus " << modulus() << "."
257 << std::endl;
258 #endif
259 return false;
260 }
261
262 // All tests passed.
263 return true;
264 }
265
266 const PPL::Congruence* PPL::Congruence::zero_dim_false_p = 0;
267 const PPL::Congruence* PPL::Congruence::zero_dim_integrality_p = 0;
268
269 void
initialize()270 PPL::Congruence::initialize() {
271 PPL_ASSERT(zero_dim_false_p == 0);
272 zero_dim_false_p
273 = new Congruence((Linear_Expression::zero() %= Coefficient(-1)) / 0);
274
275 PPL_ASSERT(zero_dim_integrality_p == 0);
276 zero_dim_integrality_p
277 = new Congruence(Linear_Expression::zero() %= Coefficient(-1));
278 }
279
280 void
finalize()281 PPL::Congruence::finalize() {
282 PPL_ASSERT(zero_dim_false_p != 0);
283 delete zero_dim_false_p;
284 zero_dim_false_p = 0;
285
286 PPL_ASSERT(zero_dim_integrality_p != 0);
287 delete zero_dim_integrality_p;
288 zero_dim_integrality_p = 0;
289 }
290