1/* Source code for an implementation of the Omega test, an integer
2   programming algorithm for dependence analysis, by William Pugh,
3   appeared in Supercomputing '91 and CACM Aug 92.
4
5   This code has no license restrictions, and is considered public
6   domain.
7
8   Changes copyright (C) 2005-2015 Free Software Foundation, Inc.
9   Contributed by Sebastian Pop <sebastian.pop@inria.fr>
10
11This file is part of GCC.
12
13GCC is free software; you can redistribute it and/or modify it under
14the terms of the GNU General Public License as published by the Free
15Software Foundation; either version 3, or (at your option) any later
16version.
17
18GCC is distributed in the hope that it will be useful, but WITHOUT ANY
19WARRANTY; without even the implied warranty of MERCHANTABILITY or
20FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
21for more details.
22
23You should have received a copy of the GNU General Public License
24along with GCC; see the file COPYING3.  If not see
25<http://www.gnu.org/licenses/>.  */
26
27#include "config.h"
28#include "params.h"
29
30#ifndef GCC_OMEGA_H
31#define GCC_OMEGA_H
32
33#define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS)
34#define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS)
35#define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS)
36
37#define pos_infinity (0x7ffffff)
38#define neg_infinity (-0x7ffffff)
39
40/* Results of the Omega solver.  */
41enum omega_result {
42  omega_false = 0,
43  omega_true = 1,
44
45  /* Value returned when the solver is unable to determine an
46     answer.  */
47  omega_unknown = 2,
48
49  /* Value used for asking the solver to simplify the system.  */
50  omega_simplify = 3
51};
52
53/* Values used for labeling equations.  Private (not used outside the
54   solver).  */
55enum omega_eqn_color {
56  omega_black = 0,
57  omega_red = 1
58};
59
60/* Structure for equations.  */
61typedef struct eqn_d
62{
63  int key;
64  int touched;
65  enum omega_eqn_color color;
66
67  /* Array of coefficients for the equation.  The layout of the data
68     is as follows: coef[0] is the constant, coef[i] for 1 <= i <=
69     OMEGA_MAX_VARS, are the coefficients for each dimension.  Examples:
70     the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the
71     inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3].  */
72  int *coef;
73} *eqn;
74
75typedef struct omega_pb_d
76{
77  /* The number of variables in the system of equations.  */
78  int num_vars;
79
80  /* Safe variables are not eliminated during the Fourier-Motzkin
81     simplification of the system.  Safe variables are all those
82     variables that are placed at the beginning of the array of
83     variables: PB->var[1, ..., SAFE_VARS].  PB->var[0] is not used,
84     as PB->eqs[x]->coef[0] represents the constant of the equation.  */
85  int safe_vars;
86
87  /* Number of elements in eqs[].  */
88  int num_eqs;
89  /* Number of elements in geqs[].  */
90  int num_geqs;
91  /* Number of elements in subs[].  */
92  int num_subs;
93
94  int hash_version;
95  bool variables_initialized;
96  bool variables_freed;
97
98  /* Index or name of variables.  Negative integers are reserved for
99     wildcard variables.  Maps the index of variables in the original
100     problem to the new index of the variable.  The index for a
101     variable in the coef array of an equation can change as some
102     variables are eliminated.  */
103  int *var;
104
105  int *forwarding_address;
106
107  /* Inequalities in the system of constraints.  */
108  eqn geqs;
109
110  /* Equations in the system of constraints.  */
111  eqn eqs;
112
113  /* A map of substituted variables.  */
114  eqn subs;
115} *omega_pb;
116
117extern void omega_initialize (void);
118extern omega_pb omega_alloc_problem (int, int);
119extern enum omega_result omega_solve_problem (omega_pb, enum omega_result);
120extern enum omega_result omega_simplify_problem (omega_pb);
121extern enum omega_result omega_simplify_approximate (omega_pb);
122extern enum omega_result omega_constrain_variable_sign (omega_pb,
123							enum omega_eqn_color,
124							int, int);
125extern void debug (omega_pb_d &ref);
126extern void debug (omega_pb_d *ptr);
127extern void debug_omega_problem (omega_pb);
128extern void omega_print_problem (FILE *, omega_pb);
129extern void omega_print_red_equations (FILE *, omega_pb);
130extern int omega_count_red_equations (omega_pb);
131extern void omega_pretty_print_problem (FILE *, omega_pb);
132extern void omega_unprotect_variable (omega_pb, int var);
133extern void omega_negate_geq (omega_pb, int);
134extern void omega_convert_eq_to_geqs (omega_pb, int eq);
135extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int);
136extern bool omega_problem_has_red_equations (omega_pb);
137extern enum omega_result omega_eliminate_redundant (omega_pb, bool);
138extern void omega_eliminate_red (omega_pb, bool);
139extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color,
140					    int, int);
141extern bool omega_query_variable (omega_pb, int, int *, int *);
142extern int omega_query_variable_signs (omega_pb, int, int, int, int,
143				       int, int, bool *, int *);
144extern bool omega_query_variable_bounds (omega_pb, int, int *, int *);
145extern void (*omega_when_reduced) (omega_pb);
146extern void omega_no_procedure (omega_pb);
147
148/* Return true when variable I in problem PB is a wildcard.  */
149
150static inline bool
151omega_wildcard_p (omega_pb pb, int i)
152{
153  return (pb->var[i] < 0);
154}
155
156/* Return true when variable I in problem PB is a safe variable.  */
157
158static inline bool
159omega_safe_var_p (omega_pb pb, int i)
160{
161  /* The constant of an equation is not a variable.  */
162  gcc_assert (0 < i);
163  return (i <= pb->safe_vars);
164}
165
166/* Print to FILE equality E from PB.  */
167
168static inline void
169omega_print_eq (FILE *file, omega_pb pb, eqn e)
170{
171  omega_print_eqn (file, pb, e, false, 0);
172}
173
174/* Print to FILE inequality E from PB.  */
175
176static inline void
177omega_print_geq (FILE *file, omega_pb pb, eqn e)
178{
179  omega_print_eqn (file, pb, e, true, 0);
180}
181
182/* Print to FILE inequality E from PB.  */
183
184static inline void
185omega_print_geq_extra (FILE *file, omega_pb pb, eqn e)
186{
187  omega_print_eqn (file, pb, e, true, 1);
188}
189
190/* E1 = E2, make a copy of E2 into E1.  Equations contain S variables.  */
191
192static inline void
193omega_copy_eqn (eqn e1, eqn e2, int s)
194{
195  e1->key = e2->key;
196  e1->touched = e2->touched;
197  e1->color = e2->color;
198
199  memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int));
200}
201
202/* Initialize E = 0.  Equation E contains S variables.  */
203
204static inline void
205omega_init_eqn_zero (eqn e, int s)
206{
207  e->key = 0;
208  e->touched = 0;
209  e->color = omega_black;
210
211  memset (e->coef, 0, (s + 1) * sizeof (int));
212}
213
214/* Allocate N equations with S variables.  */
215
216static inline eqn
217omega_alloc_eqns (int s, int n)
218{
219  int i;
220  eqn res = (eqn) (xcalloc (n, sizeof (struct eqn_d)));
221
222  for (i = n - 1; i >= 0; i--)
223    {
224      res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int)));
225      omega_init_eqn_zero (&res[i], s);
226    }
227
228  return res;
229}
230
231/* Free N equations from array EQ.  */
232
233static inline void
234omega_free_eqns (eqn eq, int n)
235{
236  int i;
237
238  for (i = n - 1; i >= 0; i--)
239    free (eq[i].coef);
240
241  free (eq);
242}
243
244/* Returns true when E is an inequality with a single variable.  */
245
246static inline bool
247single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED)
248{
249  return (e->key != 0
250	  && -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS);
251}
252
253/* Allocate a new equality with all coefficients 0, and tagged with
254   COLOR.  Return the index of this equality in problem PB.  */
255
256static inline int
257omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color)
258{
259  int idx = pb->num_eqs++;
260
261  gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
262  omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars);
263  pb->eqs[idx].color = color;
264  return idx;
265}
266
267/* Allocate a new inequality with all coefficients 0, and tagged with
268   COLOR.  Return the index of this inequality in problem PB.  */
269
270static inline int
271omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color)
272{
273  int idx = pb->num_geqs;
274
275  pb->num_geqs++;
276  gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
277  omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars);
278  pb->geqs[idx].touched = 1;
279  pb->geqs[idx].color = color;
280  return idx;
281}
282
283/* Initialize variables for problem PB.  */
284
285static inline void
286omega_initialize_variables (omega_pb pb)
287{
288  int i;
289
290  for (i = pb->num_vars; i >= 0; i--)
291    pb->forwarding_address[i] = pb->var[i] = i;
292
293  pb->variables_initialized = true;
294}
295
296/* Free problem PB.  */
297
298static inline void
299omega_free_problem (omega_pb pb)
300{
301  free (pb->var);
302  free (pb->forwarding_address);
303  omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS);
304  omega_free_eqns (pb->eqs, OMEGA_MAX_EQS);
305  omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1);
306  free (pb);
307}
308
309/* Copy omega problems: P1 = P2.  */
310
311static inline void
312omega_copy_problem (omega_pb p1, omega_pb p2)
313{
314  int e, i;
315
316  p1->num_vars = p2->num_vars;
317  p1->hash_version = p2->hash_version;
318  p1->variables_initialized = p2->variables_initialized;
319  p1->variables_freed = p2->variables_freed;
320  p1->safe_vars = p2->safe_vars;
321  p1->num_eqs = p2->num_eqs;
322  p1->num_subs = p2->num_subs;
323  p1->num_geqs = p2->num_geqs;
324
325  for (e = p2->num_eqs - 1; e >= 0; e--)
326    omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars);
327
328  for (e = p2->num_geqs - 1; e >= 0; e--)
329    omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars);
330
331  for (e = p2->num_subs - 1; e >= 0; e--)
332    omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars);
333
334  for (i = p2->num_vars; i >= 0; i--)
335    p1->var[i] = p2->var[i];
336
337  for (i = OMEGA_MAX_VARS; i >= 0; i--)
338    p1->forwarding_address[i] = p2->forwarding_address[i];
339}
340
341#endif /* GCC_OMEGA_H */
342