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.
5 This code has no license restrictions, and is considered public
8 Changes copyright (C) 2005, 2006, 2007, 2008, 2009 Free Software Foundation,
10 Contributed by Sebastian Pop <sebastian.pop@inria.fr>
12 This file is part of GCC.
14 GCC is free software; you can redistribute it and/or modify it under
15 the terms of the GNU General Public License as published by the Free
16 Software Foundation; either version 3, or (at your option) any later
19 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
20 WARRANTY; without even the implied warranty of MERCHANTABILITY or
21 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
24 You should have received a copy of the GNU General Public License
25 along with GCC; see the file COPYING3. If not see
26 <http://www.gnu.org/licenses/>. */
28 /* For a detailed description, see "Constraint-Based Array Dependence
29 Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
31 ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
36 #include "coretypes.h"
40 #include "diagnostic.h"
42 #include "tree-pass.h"
45 /* When set to true, keep substitution variables. When set to false,
46 resurrect substitution variables (convert substitutions back to EQs). */
47 static bool omega_reduce_with_subs
= true;
49 /* When set to true, omega_simplify_problem checks for problem with no
50 solutions, calling verify_omega_pb. */
51 static bool omega_verify_simplification
= false;
53 /* When set to true, only produce a single simplified result. */
54 static bool omega_single_result
= false;
56 /* Set return_single_result to 1 when omega_single_result is true. */
57 static int return_single_result
= 0;
59 /* Hash table for equations generated by the solver. */
60 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
61 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
62 static eqn hash_master
;
64 static int hash_version
= 0;
66 /* Set to true for making the solver enter in approximation mode. */
67 static bool in_approximate_mode
= false;
69 /* When set to zero, the solver is allowed to add new equalities to
70 the problem to be solved. */
71 static int conservative
= 0;
73 /* Set to omega_true when the problem was successfully reduced, set to
74 omega_unknown when the solver is unable to determine an answer. */
75 static enum omega_result omega_found_reduction
;
77 /* Set to true when the solver is allowed to add omega_red equations. */
78 static bool create_color
= false;
80 /* Set to nonzero when the problem to be solved can be reduced. */
81 static int may_be_red
= 0;
83 /* When false, there should be no substitution equations in the
84 simplified problem. */
85 static int please_no_equalities_in_simplified_problems
= 0;
87 /* Variables names for pretty printing. */
88 static char wild_name
[200][40];
90 /* Pointer to the void problem. */
91 static omega_pb no_problem
= (omega_pb
) 0;
93 /* Pointer to the problem to be solved. */
94 static omega_pb original_problem
= (omega_pb
) 0;
97 /* Return the integer A divided by B. */
100 int_div (int a
, int b
)
105 return -((-a
+ b
- 1)/b
);
108 /* Return the integer A modulo B. */
111 int_mod (int a
, int b
)
113 return a
- b
* int_div (a
, b
);
116 /* For X and Y positive integers, return X multiplied by Y and check
117 that the result does not overflow. */
120 check_pos_mul (int x
, int y
)
123 gcc_assert ((INT_MAX
) / x
> y
);
128 /* Return X multiplied by Y and check that the result does not
132 check_mul (int x
, int y
)
137 return check_pos_mul (x
, y
);
139 return -check_pos_mul (x
, -y
);
142 return -check_pos_mul (-x
, y
);
144 return check_pos_mul (-x
, -y
);
147 /* Test whether equation E is red. */
150 omega_eqn_is_red (eqn e
, int desired_res
)
152 return (desired_res
== omega_simplify
&& e
->color
== omega_red
);
155 /* Return a string for VARIABLE. */
158 omega_var_to_str (int variable
)
160 if (0 <= variable
&& variable
<= 20)
161 return wild_name
[variable
];
163 if (-20 < variable
&& variable
< 0)
164 return wild_name
[40 + variable
];
166 /* Collapse all the entries that would have overflowed. */
167 return wild_name
[21];
170 /* Return a string for variable I in problem PB. */
173 omega_variable_to_str (omega_pb pb
, int i
)
175 return omega_var_to_str (pb
->var
[i
]);
178 /* Do nothing function: used for default initializations. */
181 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED
)
185 void (*omega_when_reduced
) (omega_pb
) = omega_no_procedure
;
187 /* Compute the greatest common divisor of A and B. */
205 /* Print to FILE from PB equation E with all its coefficients
209 omega_print_term (FILE *file
, omega_pb pb
, eqn e
, int c
)
213 int n
= pb
->num_vars
;
216 for (i
= 1; i
<= n
; i
++)
217 if (c
* e
->coef
[i
] > 0)
222 if (c
* e
->coef
[i
] == 1)
223 fprintf (file
, "%s", omega_variable_to_str (pb
, i
));
225 fprintf (file
, "%d * %s", c
* e
->coef
[i
],
226 omega_variable_to_str (pb
, i
));
230 for (i
= 1; i
<= n
; i
++)
231 if (i
!= went_first
&& c
* e
->coef
[i
] != 0)
233 if (!first
&& c
* e
->coef
[i
] > 0)
234 fprintf (file
, " + ");
238 if (c
* e
->coef
[i
] == 1)
239 fprintf (file
, "%s", omega_variable_to_str (pb
, i
));
240 else if (c
* e
->coef
[i
] == -1)
241 fprintf (file
, " - %s", omega_variable_to_str (pb
, i
));
243 fprintf (file
, "%d * %s", c
* e
->coef
[i
],
244 omega_variable_to_str (pb
, i
));
247 if (!first
&& c
* e
->coef
[0] > 0)
248 fprintf (file
, " + ");
250 if (first
|| c
* e
->coef
[0] != 0)
251 fprintf (file
, "%d", c
* e
->coef
[0]);
254 /* Print to FILE the equation E of problem PB. */
257 omega_print_eqn (FILE *file
, omega_pb pb
, eqn e
, bool test
, int extra
)
260 int n
= pb
->num_vars
+ extra
;
261 bool is_lt
= test
&& e
->coef
[0] == -1;
269 else if (e
->key
!= 0)
270 fprintf (file
, "%d: ", e
->key
);
273 if (e
->color
== omega_red
)
278 for (i
= is_lt
? 1 : 0; i
<= n
; i
++)
282 fprintf (file
, " + ");
287 fprintf (file
, "%d", -e
->coef
[i
]);
288 else if (e
->coef
[i
] == -1)
289 fprintf (file
, "%s", omega_variable_to_str (pb
, i
));
291 fprintf (file
, "%d * %s", -e
->coef
[i
],
292 omega_variable_to_str (pb
, i
));
307 fprintf (file
, " = ");
309 fprintf (file
, " < ");
311 fprintf (file
, " <= ");
315 for (i
= 0; i
<= n
; i
++)
319 fprintf (file
, " + ");
324 fprintf (file
, "%d", e
->coef
[i
]);
325 else if (e
->coef
[i
] == 1)
326 fprintf (file
, "%s", omega_variable_to_str (pb
, i
));
328 fprintf (file
, "%d * %s", e
->coef
[i
],
329 omega_variable_to_str (pb
, i
));
335 if (e
->color
== omega_red
)
339 /* Print to FILE all the variables of problem PB. */
342 omega_print_vars (FILE *file
, omega_pb pb
)
346 fprintf (file
, "variables = ");
348 if (pb
->safe_vars
> 0)
349 fprintf (file
, "protected (");
351 for (i
= 1; i
<= pb
->num_vars
; i
++)
353 fprintf (file
, "%s", omega_variable_to_str (pb
, i
));
355 if (i
== pb
->safe_vars
)
358 if (i
< pb
->num_vars
)
359 fprintf (file
, ", ");
362 fprintf (file
, "\n");
365 /* Debug problem PB. */
368 debug_omega_problem (omega_pb pb
)
370 omega_print_problem (stderr
, pb
);
373 /* Print to FILE problem PB. */
376 omega_print_problem (FILE *file
, omega_pb pb
)
380 if (!pb
->variables_initialized
)
381 omega_initialize_variables (pb
);
383 omega_print_vars (file
, pb
);
385 for (e
= 0; e
< pb
->num_eqs
; e
++)
387 omega_print_eq (file
, pb
, &pb
->eqs
[e
]);
388 fprintf (file
, "\n");
391 fprintf (file
, "Done with EQ\n");
393 for (e
= 0; e
< pb
->num_geqs
; e
++)
395 omega_print_geq (file
, pb
, &pb
->geqs
[e
]);
396 fprintf (file
, "\n");
399 fprintf (file
, "Done with GEQ\n");
401 for (e
= 0; e
< pb
->num_subs
; e
++)
403 eqn eq
= &pb
->subs
[e
];
405 if (eq
->color
== omega_red
)
409 fprintf (file
, "%s := ", omega_var_to_str (eq
->key
));
411 fprintf (file
, "#%d := ", eq
->key
);
413 omega_print_term (file
, pb
, eq
, 1);
415 if (eq
->color
== omega_red
)
418 fprintf (file
, "\n");
422 /* Return the number of equations in PB tagged omega_red. */
425 omega_count_red_equations (omega_pb pb
)
430 for (e
= 0; e
< pb
->num_eqs
; e
++)
431 if (pb
->eqs
[e
].color
== omega_red
)
433 for (i
= pb
->num_vars
; i
> 0; i
--)
434 if (pb
->geqs
[e
].coef
[i
])
437 if (i
== 0 && pb
->geqs
[e
].coef
[0] == 1)
443 for (e
= 0; e
< pb
->num_geqs
; e
++)
444 if (pb
->geqs
[e
].color
== omega_red
)
447 for (e
= 0; e
< pb
->num_subs
; e
++)
448 if (pb
->subs
[e
].color
== omega_red
)
454 /* Print to FILE all the equations in PB that are tagged omega_red. */
457 omega_print_red_equations (FILE *file
, omega_pb pb
)
461 if (!pb
->variables_initialized
)
462 omega_initialize_variables (pb
);
464 omega_print_vars (file
, pb
);
466 for (e
= 0; e
< pb
->num_eqs
; e
++)
467 if (pb
->eqs
[e
].color
== omega_red
)
469 omega_print_eq (file
, pb
, &pb
->eqs
[e
]);
470 fprintf (file
, "\n");
473 for (e
= 0; e
< pb
->num_geqs
; e
++)
474 if (pb
->geqs
[e
].color
== omega_red
)
476 omega_print_geq (file
, pb
, &pb
->geqs
[e
]);
477 fprintf (file
, "\n");
480 for (e
= 0; e
< pb
->num_subs
; e
++)
481 if (pb
->subs
[e
].color
== omega_red
)
483 eqn eq
= &pb
->subs
[e
];
487 fprintf (file
, "%s := ", omega_var_to_str (eq
->key
));
489 fprintf (file
, "#%d := ", eq
->key
);
491 omega_print_term (file
, pb
, eq
, 1);
492 fprintf (file
, "]\n");
496 /* Pretty print PB to FILE. */
499 omega_pretty_print_problem (FILE *file
, omega_pb pb
)
501 int e
, v
, v1
, v2
, v3
, t
;
502 bool *live
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
503 int stuffPrinted
= 0;
508 } partial_order_type
;
510 partial_order_type
**po
= XNEWVEC (partial_order_type
*,
511 OMEGA_MAX_VARS
* OMEGA_MAX_VARS
);
512 int **po_eq
= XNEWVEC (int *, OMEGA_MAX_VARS
* OMEGA_MAX_VARS
);
513 int *last_links
= XNEWVEC (int, OMEGA_MAX_VARS
);
514 int *first_links
= XNEWVEC (int, OMEGA_MAX_VARS
);
515 int *chain_length
= XNEWVEC (int, OMEGA_MAX_VARS
);
516 int *chain
= XNEWVEC (int, OMEGA_MAX_VARS
);
520 if (!pb
->variables_initialized
)
521 omega_initialize_variables (pb
);
523 if (pb
->num_vars
> 0)
525 omega_eliminate_redundant (pb
, false);
527 for (e
= 0; e
< pb
->num_eqs
; e
++)
530 fprintf (file
, "; ");
533 omega_print_eq (file
, pb
, &pb
->eqs
[e
]);
536 for (e
= 0; e
< pb
->num_geqs
; e
++)
541 for (v
= 1; v
<= pb
->num_vars
; v
++)
543 last_links
[v
] = first_links
[v
] = 0;
546 for (v2
= 1; v2
<= pb
->num_vars
; v2
++)
550 for (e
= 0; e
< pb
->num_geqs
; e
++)
553 for (v
= 1; v
<= pb
->num_vars
; v
++)
554 if (pb
->geqs
[e
].coef
[v
] == 1)
556 else if (pb
->geqs
[e
].coef
[v
] == -1)
561 while (v1
> 0 && pb
->geqs
[e
].coef
[v1
] == 0)
566 while (v2
> 0 && pb
->geqs
[e
].coef
[v2
] == 0)
571 while (v3
> 0 && pb
->geqs
[e
].coef
[v3
] == 0)
574 if (pb
->geqs
[e
].coef
[0] > 0 || pb
->geqs
[e
].coef
[0] < -1
576 || pb
->geqs
[e
].coef
[v1
] * pb
->geqs
[e
].coef
[v2
] != -1)
578 /* Not a partial order relation. */
582 if (pb
->geqs
[e
].coef
[v1
] == 1)
589 /* Relation is v1 <= v2 or v1 < v2. */
590 po
[v1
][v2
] = ((pb
->geqs
[e
].coef
[0] == 0) ? le
: lt
);
594 for (v
= 1; v
<= pb
->num_vars
; v
++)
595 chain_length
[v
] = last_links
[v
];
597 /* Just in case pb->num_vars <= 0. */
599 for (t
= 0; t
< pb
->num_vars
; t
++)
603 for (v1
= 1; v1
<= pb
->num_vars
; v1
++)
604 for (v2
= 1; v2
<= pb
->num_vars
; v2
++)
605 if (po
[v1
][v2
] != none
&&
606 chain_length
[v1
] <= chain_length
[v2
])
608 chain_length
[v1
] = chain_length
[v2
] + 1;
613 /* Caught in cycle. */
614 gcc_assert (!change
);
616 for (v1
= 1; v1
<= pb
->num_vars
; v1
++)
617 if (chain_length
[v1
] == 0)
622 for (v1
= 2; v1
<= pb
->num_vars
; v1
++)
623 if (chain_length
[v1
] + first_links
[v1
] >
624 chain_length
[v
] + first_links
[v
])
627 if (chain_length
[v
] + first_links
[v
] == 0)
631 fprintf (file
, "; ");
635 /* Chain starts at v. */
640 for (e
= 0; e
< pb
->num_geqs
; e
++)
641 if (live
[e
] && pb
->geqs
[e
].coef
[v
] == 1)
644 fprintf (file
, ", ");
646 tmp
= pb
->geqs
[e
].coef
[v
];
647 pb
->geqs
[e
].coef
[v
] = 0;
648 omega_print_term (file
, pb
, &pb
->geqs
[e
], -1);
649 pb
->geqs
[e
].coef
[v
] = tmp
;
655 fprintf (file
, " <= ");
664 for (v2
= 1; v2
<= pb
->num_vars
; v2
++)
665 if (po
[v
][v2
] && chain_length
[v
] == 1 + chain_length
[v2
])
668 if (v2
> pb
->num_vars
)
675 fprintf (file
, "%s", omega_variable_to_str (pb
, chain
[0]));
677 for (multiprint
= false, i
= 1; i
< m
; i
++)
683 fprintf (file
, " <= ");
685 fprintf (file
, " < ");
687 fprintf (file
, "%s", omega_variable_to_str (pb
, v2
));
688 live
[po_eq
[v
][v2
]] = false;
690 if (!multiprint
&& i
< m
- 1)
691 for (v3
= 1; v3
<= pb
->num_vars
; v3
++)
693 if (v
== v3
|| v2
== v3
694 || po
[v
][v2
] != po
[v
][v3
]
695 || po
[v2
][chain
[i
+ 1]] != po
[v3
][chain
[i
+ 1]])
698 fprintf (file
, ",%s", omega_variable_to_str (pb
, v3
));
699 live
[po_eq
[v
][v3
]] = false;
700 live
[po_eq
[v3
][chain
[i
+ 1]]] = false;
708 /* Print last_links. */
713 for (e
= 0; e
< pb
->num_geqs
; e
++)
714 if (live
[e
] && pb
->geqs
[e
].coef
[v
] == -1)
717 fprintf (file
, ", ");
719 fprintf (file
, " <= ");
721 tmp
= pb
->geqs
[e
].coef
[v
];
722 pb
->geqs
[e
].coef
[v
] = 0;
723 omega_print_term (file
, pb
, &pb
->geqs
[e
], 1);
724 pb
->geqs
[e
].coef
[v
] = tmp
;
731 for (e
= 0; e
< pb
->num_geqs
; e
++)
735 fprintf (file
, "; ");
737 omega_print_geq (file
, pb
, &pb
->geqs
[e
]);
740 for (e
= 0; e
< pb
->num_subs
; e
++)
742 eqn eq
= &pb
->subs
[e
];
745 fprintf (file
, "; ");
750 fprintf (file
, "%s := ", omega_var_to_str (eq
->key
));
752 fprintf (file
, "#%d := ", eq
->key
);
754 omega_print_term (file
, pb
, eq
, 1);
767 /* Assign to variable I in PB the next wildcard name. The name of a
768 wildcard is a negative number. */
769 static int next_wild_card
= 0;
772 omega_name_wild_card (omega_pb pb
, int i
)
775 if (next_wild_card
< -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS
))
777 pb
->var
[i
] = next_wild_card
;
780 /* Return the index of the last protected (or safe) variable in PB,
781 after having added a new wildcard variable. */
784 omega_add_new_wild_card (omega_pb pb
)
787 int i
= ++pb
->safe_vars
;
790 /* Make a free place in the protected (safe) variables, by moving
791 the non protected variable pointed by "I" at the end, ie. at
792 offset pb->num_vars. */
793 if (pb
->num_vars
!= i
)
795 /* Move "I" for all the inequalities. */
796 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
798 if (pb
->geqs
[e
].coef
[i
])
799 pb
->geqs
[e
].touched
= 1;
801 pb
->geqs
[e
].coef
[pb
->num_vars
] = pb
->geqs
[e
].coef
[i
];
804 /* Move "I" for all the equalities. */
805 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
806 pb
->eqs
[e
].coef
[pb
->num_vars
] = pb
->eqs
[e
].coef
[i
];
808 /* Move "I" for all the substitutions. */
809 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
810 pb
->subs
[e
].coef
[pb
->num_vars
] = pb
->subs
[e
].coef
[i
];
812 /* Move the identifier. */
813 pb
->var
[pb
->num_vars
] = pb
->var
[i
];
816 /* Initialize at zero all the coefficients */
817 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
818 pb
->geqs
[e
].coef
[i
] = 0;
820 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
821 pb
->eqs
[e
].coef
[i
] = 0;
823 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
824 pb
->subs
[e
].coef
[i
] = 0;
826 /* And give it a name. */
827 omega_name_wild_card (pb
, i
);
831 /* Delete inequality E from problem PB that has N_VARS variables. */
834 omega_delete_geq (omega_pb pb
, int e
, int n_vars
)
836 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
838 fprintf (dump_file
, "Deleting %d (last:%d): ", e
, pb
->num_geqs
- 1);
839 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
840 fprintf (dump_file
, "\n");
843 if (e
< pb
->num_geqs
- 1)
844 omega_copy_eqn (&pb
->geqs
[e
], &pb
->geqs
[pb
->num_geqs
- 1], n_vars
);
849 /* Delete extra inequality E from problem PB that has N_VARS
853 omega_delete_geq_extra (omega_pb pb
, int e
, int n_vars
)
855 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
857 fprintf (dump_file
, "Deleting %d: ",e
);
858 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[e
]);
859 fprintf (dump_file
, "\n");
862 if (e
< pb
->num_geqs
- 1)
863 omega_copy_eqn (&pb
->geqs
[e
], &pb
->geqs
[pb
->num_geqs
- 1], n_vars
);
869 /* Remove variable I from problem PB. */
872 omega_delete_variable (omega_pb pb
, int i
)
874 int n_vars
= pb
->num_vars
;
877 if (omega_safe_var_p (pb
, i
))
879 int j
= pb
->safe_vars
;
881 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
883 pb
->geqs
[e
].touched
= 1;
884 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[j
];
885 pb
->geqs
[e
].coef
[j
] = pb
->geqs
[e
].coef
[n_vars
];
888 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
890 pb
->eqs
[e
].coef
[i
] = pb
->eqs
[e
].coef
[j
];
891 pb
->eqs
[e
].coef
[j
] = pb
->eqs
[e
].coef
[n_vars
];
894 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
896 pb
->subs
[e
].coef
[i
] = pb
->subs
[e
].coef
[j
];
897 pb
->subs
[e
].coef
[j
] = pb
->subs
[e
].coef
[n_vars
];
900 pb
->var
[i
] = pb
->var
[j
];
901 pb
->var
[j
] = pb
->var
[n_vars
];
905 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
906 if (pb
->geqs
[e
].coef
[n_vars
])
908 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[n_vars
];
909 pb
->geqs
[e
].touched
= 1;
912 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
913 pb
->eqs
[e
].coef
[i
] = pb
->eqs
[e
].coef
[n_vars
];
915 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
916 pb
->subs
[e
].coef
[i
] = pb
->subs
[e
].coef
[n_vars
];
918 pb
->var
[i
] = pb
->var
[n_vars
];
921 if (omega_safe_var_p (pb
, i
))
927 /* Because the coefficients of an equation are sparse, PACKING records
928 indices for non null coefficients. */
931 /* Set up the coefficients of PACKING, following the coefficients of
932 equation EQN that has NUM_VARS variables. */
935 setup_packing (eqn eqn
, int num_vars
)
940 for (k
= num_vars
; k
>= 0; k
--)
947 /* Computes a linear combination of EQ and SUB at VAR with coefficient
948 C, such that EQ->coef[VAR] is set to 0. TOP_VAR is the number of
949 non null indices of SUB stored in PACKING. */
952 omega_substitute_red_1 (eqn eq
, eqn sub
, int var
, int c
, bool *found_black
,
955 if (eq
->coef
[var
] != 0)
957 if (eq
->color
== omega_black
)
961 int j
, k
= eq
->coef
[var
];
965 for (j
= top_var
; j
>= 0; j
--)
966 eq
->coef
[packing
[j
]] -= sub
->coef
[packing
[j
]] * k
* c
;
971 /* Substitute in PB variable VAR with "C * SUB". */
974 omega_substitute_red (omega_pb pb
, eqn sub
, int var
, int c
, bool *found_black
)
976 int e
, top_var
= setup_packing (sub
, pb
->num_vars
);
978 *found_black
= false;
980 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
982 if (sub
->color
== omega_red
)
983 fprintf (dump_file
, "[");
985 fprintf (dump_file
, "substituting using %s := ",
986 omega_variable_to_str (pb
, var
));
987 omega_print_term (dump_file
, pb
, sub
, -c
);
989 if (sub
->color
== omega_red
)
990 fprintf (dump_file
, "]");
992 fprintf (dump_file
, "\n");
993 omega_print_vars (dump_file
, pb
);
996 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
998 eqn eqn
= &(pb
->eqs
[e
]);
1000 omega_substitute_red_1 (eqn
, sub
, var
, c
, found_black
, top_var
);
1002 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1004 omega_print_eq (dump_file
, pb
, eqn
);
1005 fprintf (dump_file
, "\n");
1009 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1011 eqn eqn
= &(pb
->geqs
[e
]);
1013 omega_substitute_red_1 (eqn
, sub
, var
, c
, found_black
, top_var
);
1015 if (eqn
->coef
[var
] && eqn
->color
== omega_red
)
1018 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1020 omega_print_geq (dump_file
, pb
, eqn
);
1021 fprintf (dump_file
, "\n");
1025 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
1027 eqn eqn
= &(pb
->subs
[e
]);
1029 omega_substitute_red_1 (eqn
, sub
, var
, c
, found_black
, top_var
);
1031 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1033 fprintf (dump_file
, "%s := ", omega_var_to_str (eqn
->key
));
1034 omega_print_term (dump_file
, pb
, eqn
, 1);
1035 fprintf (dump_file
, "\n");
1039 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1040 fprintf (dump_file
, "---\n\n");
1042 if (omega_safe_var_p (pb
, var
) && !omega_wildcard_p (pb
, var
))
1043 *found_black
= true;
1046 /* Substitute in PB variable VAR with "C * SUB". */
1049 omega_substitute (omega_pb pb
, eqn sub
, int var
, int c
)
1052 int top_var
= setup_packing (sub
, pb
->num_vars
);
1054 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1056 fprintf (dump_file
, "substituting using %s := ",
1057 omega_variable_to_str (pb
, var
));
1058 omega_print_term (dump_file
, pb
, sub
, -c
);
1059 fprintf (dump_file
, "\n");
1060 omega_print_vars (dump_file
, pb
);
1065 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
1066 pb
->eqs
[e
].coef
[var
] = 0;
1068 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1069 if (pb
->geqs
[e
].coef
[var
] != 0)
1071 pb
->geqs
[e
].touched
= 1;
1072 pb
->geqs
[e
].coef
[var
] = 0;
1075 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
1076 pb
->subs
[e
].coef
[var
] = 0;
1078 if (omega_safe_var_p (pb
, var
) && !omega_wildcard_p (pb
, var
))
1081 eqn eqn
= &(pb
->subs
[pb
->num_subs
++]);
1083 for (k
= pb
->num_vars
; k
>= 0; k
--)
1086 eqn
->key
= pb
->var
[var
];
1087 eqn
->color
= omega_black
;
1090 else if (top_var
== 0 && packing
[0] == 0)
1092 c
= -sub
->coef
[0] * c
;
1094 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
1096 pb
->eqs
[e
].coef
[0] += pb
->eqs
[e
].coef
[var
] * c
;
1097 pb
->eqs
[e
].coef
[var
] = 0;
1100 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1101 if (pb
->geqs
[e
].coef
[var
] != 0)
1103 pb
->geqs
[e
].coef
[0] += pb
->geqs
[e
].coef
[var
] * c
;
1104 pb
->geqs
[e
].coef
[var
] = 0;
1105 pb
->geqs
[e
].touched
= 1;
1108 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
1110 pb
->subs
[e
].coef
[0] += pb
->subs
[e
].coef
[var
] * c
;
1111 pb
->subs
[e
].coef
[var
] = 0;
1114 if (omega_safe_var_p (pb
, var
) && !omega_wildcard_p (pb
, var
))
1117 eqn eqn
= &(pb
->subs
[pb
->num_subs
++]);
1119 for (k
= pb
->num_vars
; k
>= 1; k
--)
1123 eqn
->key
= pb
->var
[var
];
1124 eqn
->color
= omega_black
;
1127 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1129 fprintf (dump_file
, "---\n\n");
1130 omega_print_problem (dump_file
, pb
);
1131 fprintf (dump_file
, "===\n\n");
1136 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
1138 eqn eqn
= &(pb
->eqs
[e
]);
1139 int k
= eqn
->coef
[var
];
1146 for (j
= top_var
; j
>= 0; j
--)
1149 eqn
->coef
[j0
] -= sub
->coef
[j0
] * k
;
1153 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1155 omega_print_eq (dump_file
, pb
, eqn
);
1156 fprintf (dump_file
, "\n");
1160 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1162 eqn eqn
= &(pb
->geqs
[e
]);
1163 int k
= eqn
->coef
[var
];
1171 for (j
= top_var
; j
>= 0; j
--)
1174 eqn
->coef
[j0
] -= sub
->coef
[j0
] * k
;
1178 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1180 omega_print_geq (dump_file
, pb
, eqn
);
1181 fprintf (dump_file
, "\n");
1185 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
1187 eqn eqn
= &(pb
->subs
[e
]);
1188 int k
= eqn
->coef
[var
];
1195 for (j
= top_var
; j
>= 0; j
--)
1198 eqn
->coef
[j0
] -= sub
->coef
[j0
] * k
;
1202 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1204 fprintf (dump_file
, "%s := ", omega_var_to_str (eqn
->key
));
1205 omega_print_term (dump_file
, pb
, eqn
, 1);
1206 fprintf (dump_file
, "\n");
1210 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1212 fprintf (dump_file
, "---\n\n");
1213 omega_print_problem (dump_file
, pb
);
1214 fprintf (dump_file
, "===\n\n");
1217 if (omega_safe_var_p (pb
, var
) && !omega_wildcard_p (pb
, var
))
1220 eqn eqn
= &(pb
->subs
[pb
->num_subs
++]);
1223 for (k
= pb
->num_vars
; k
>= 0; k
--)
1224 eqn
->coef
[k
] = c
* (sub
->coef
[k
]);
1226 eqn
->key
= pb
->var
[var
];
1227 eqn
->color
= sub
->color
;
1232 /* Solve e = factor alpha for x_j and substitute. */
1235 omega_do_mod (omega_pb pb
, int factor
, int e
, int j
)
1238 eqn eq
= omega_alloc_eqns (0, 1);
1240 bool kill_j
= false;
1242 omega_copy_eqn (eq
, &pb
->eqs
[e
], pb
->num_vars
);
1244 for (k
= pb
->num_vars
; k
>= 0; k
--)
1246 eq
->coef
[k
] = int_mod (eq
->coef
[k
], factor
);
1248 if (2 * eq
->coef
[k
] >= factor
)
1249 eq
->coef
[k
] -= factor
;
1252 nfactor
= eq
->coef
[j
];
1254 if (omega_safe_var_p (pb
, j
) && !omega_wildcard_p (pb
, j
))
1256 i
= omega_add_new_wild_card (pb
);
1257 eq
->coef
[pb
->num_vars
] = eq
->coef
[i
];
1259 eq
->coef
[i
] = -factor
;
1264 eq
->coef
[j
] = -factor
;
1265 if (!omega_wildcard_p (pb
, j
))
1266 omega_name_wild_card (pb
, j
);
1269 omega_substitute (pb
, eq
, j
, nfactor
);
1271 for (k
= pb
->num_vars
; k
>= 0; k
--)
1272 pb
->eqs
[e
].coef
[k
] = pb
->eqs
[e
].coef
[k
] / factor
;
1275 omega_delete_variable (pb
, j
);
1277 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1279 fprintf (dump_file
, "Mod-ing and normalizing produces:\n");
1280 omega_print_problem (dump_file
, pb
);
1283 omega_free_eqns (eq
, 1);
1286 /* Multiplies by -1 inequality E. */
1289 omega_negate_geq (omega_pb pb
, int e
)
1293 for (i
= pb
->num_vars
; i
>= 0; i
--)
1294 pb
->geqs
[e
].coef
[i
] *= -1;
1296 pb
->geqs
[e
].coef
[0]--;
1297 pb
->geqs
[e
].touched
= 1;
1300 /* Returns OMEGA_TRUE when problem PB has a solution. */
1302 static enum omega_result
1303 verify_omega_pb (omega_pb pb
)
1305 enum omega_result result
;
1307 bool any_color
= false;
1308 omega_pb tmp_problem
= XNEW (struct omega_pb
);
1310 omega_copy_problem (tmp_problem
, pb
);
1311 tmp_problem
->safe_vars
= 0;
1312 tmp_problem
->num_subs
= 0;
1314 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1315 if (pb
->geqs
[e
].color
== omega_red
)
1321 if (please_no_equalities_in_simplified_problems
)
1325 original_problem
= no_problem
;
1327 original_problem
= pb
;
1329 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1331 fprintf (dump_file
, "verifying problem");
1334 fprintf (dump_file
, " (color mode)");
1336 fprintf (dump_file
, " :\n");
1337 omega_print_problem (dump_file
, pb
);
1340 result
= omega_solve_problem (tmp_problem
, omega_unknown
);
1341 original_problem
= no_problem
;
1344 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1346 if (result
!= omega_false
)
1347 fprintf (dump_file
, "verified problem\n");
1349 fprintf (dump_file
, "disproved problem\n");
1350 omega_print_problem (dump_file
, pb
);
1356 /* Add a new equality to problem PB at last position E. */
1359 adding_equality_constraint (omega_pb pb
, int e
)
1361 if (original_problem
!= no_problem
1362 && original_problem
!= pb
1366 int e2
= original_problem
->num_eqs
++;
1368 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1370 "adding equality constraint %d to outer problem\n", e2
);
1371 omega_init_eqn_zero (&original_problem
->eqs
[e2
],
1372 original_problem
->num_vars
);
1374 for (i
= pb
->num_vars
; i
>= 1; i
--)
1376 for (j
= original_problem
->num_vars
; j
>= 1; j
--)
1377 if (original_problem
->var
[j
] == pb
->var
[i
])
1382 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1383 fprintf (dump_file
, "retracting\n");
1384 original_problem
->num_eqs
--;
1387 original_problem
->eqs
[e2
].coef
[j
] = pb
->eqs
[e
].coef
[i
];
1390 original_problem
->eqs
[e2
].coef
[0] = pb
->eqs
[e
].coef
[0];
1392 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1393 omega_print_problem (dump_file
, original_problem
);
1397 static int *fast_lookup
;
1398 static int *fast_lookup_red
;
1402 normalize_uncoupled
,
1404 } normalize_return_type
;
1406 /* Normalizes PB by removing redundant constraints. Returns
1407 normalize_false when the constraints system has no solution,
1408 otherwise returns normalize_coupled or normalize_uncoupled. */
1410 static normalize_return_type
1411 normalize_omega_problem (omega_pb pb
)
1413 int e
, i
, j
, k
, n_vars
;
1414 int coupled_subscripts
= 0;
1416 n_vars
= pb
->num_vars
;
1418 for (e
= 0; e
< pb
->num_geqs
; e
++)
1420 if (!pb
->geqs
[e
].touched
)
1422 if (!single_var_geq (&pb
->geqs
[e
], n_vars
))
1423 coupled_subscripts
= 1;
1427 int g
, top_var
, i0
, hashCode
;
1428 int *p
= &packing
[0];
1430 for (k
= 1; k
<= n_vars
; k
++)
1431 if (pb
->geqs
[e
].coef
[k
])
1434 top_var
= (p
- &packing
[0]) - 1;
1438 if (pb
->geqs
[e
].coef
[0] < 0)
1440 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1442 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
1443 fprintf (dump_file
, "\nequations have no solution \n");
1445 return normalize_false
;
1448 omega_delete_geq (pb
, e
, n_vars
);
1452 else if (top_var
== 0)
1454 int singlevar
= packing
[0];
1456 g
= pb
->geqs
[e
].coef
[singlevar
];
1460 pb
->geqs
[e
].coef
[singlevar
] = 1;
1461 pb
->geqs
[e
].key
= singlevar
;
1466 pb
->geqs
[e
].coef
[singlevar
] = -1;
1467 pb
->geqs
[e
].key
= -singlevar
;
1471 pb
->geqs
[e
].coef
[0] = int_div (pb
->geqs
[e
].coef
[0], g
);
1476 int hash_key_multiplier
= 31;
1478 coupled_subscripts
= 1;
1481 g
= pb
->geqs
[e
].coef
[i
];
1482 hashCode
= g
* (i
+ 3);
1487 for (; i0
>= 0; i0
--)
1492 x
= pb
->geqs
[e
].coef
[i
];
1493 hashCode
= hashCode
* hash_key_multiplier
* (i
+ 3) + x
;
1508 for (; i0
>= 0; i0
--)
1512 x
= pb
->geqs
[e
].coef
[i
];
1513 hashCode
= hashCode
* hash_key_multiplier
* (i
+ 3) + x
;
1518 pb
->geqs
[e
].coef
[0] = int_div (pb
->geqs
[e
].coef
[0], g
);
1521 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[i
] / g
;
1522 hashCode
= pb
->geqs
[e
].coef
[i
] * (i
+ 3);
1524 for (; i0
>= 0; i0
--)
1527 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[i
] / g
;
1528 hashCode
= hashCode
* hash_key_multiplier
* (i
+ 3)
1529 + pb
->geqs
[e
].coef
[i
];
1533 g2
= abs (hashCode
);
1535 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1537 fprintf (dump_file
, "Hash code = %d, eqn = ", hashCode
);
1538 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
1539 fprintf (dump_file
, "\n");
1542 j
= g2
% HASH_TABLE_SIZE
;
1545 eqn proto
= &(hash_master
[j
]);
1547 if (proto
->touched
== g2
)
1549 if (proto
->coef
[0] == top_var
)
1552 for (i0
= top_var
; i0
>= 0; i0
--)
1556 if (pb
->geqs
[e
].coef
[i
] != proto
->coef
[i
])
1560 for (i0
= top_var
; i0
>= 0; i0
--)
1564 if (pb
->geqs
[e
].coef
[i
] != -proto
->coef
[i
])
1571 pb
->geqs
[e
].key
= proto
->key
;
1573 pb
->geqs
[e
].key
= -proto
->key
;
1578 else if (proto
->touched
< 0)
1580 omega_init_eqn_zero (proto
, pb
->num_vars
);
1582 for (i0
= top_var
; i0
>= 0; i0
--)
1585 proto
->coef
[i
] = pb
->geqs
[e
].coef
[i
];
1588 for (i0
= top_var
; i0
>= 0; i0
--)
1591 proto
->coef
[i
] = -pb
->geqs
[e
].coef
[i
];
1594 proto
->coef
[0] = top_var
;
1595 proto
->touched
= g2
;
1597 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1598 fprintf (dump_file
, " constraint key = %d\n",
1601 proto
->key
= next_key
++;
1603 /* Too many hash keys generated. */
1604 gcc_assert (proto
->key
<= MAX_KEYS
);
1607 pb
->geqs
[e
].key
= proto
->key
;
1609 pb
->geqs
[e
].key
= -proto
->key
;
1614 j
= (j
+ 1) % HASH_TABLE_SIZE
;
1618 pb
->geqs
[e
].touched
= 0;
1622 int eKey
= pb
->geqs
[e
].key
;
1626 int cTerm
= pb
->geqs
[e
].coef
[0];
1627 e2
= fast_lookup
[MAX_KEYS
- eKey
];
1629 if (e2
< e
&& pb
->geqs
[e2
].key
== -eKey
1630 && pb
->geqs
[e2
].color
== omega_black
)
1632 if (pb
->geqs
[e2
].coef
[0] < -cTerm
)
1634 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1636 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
1637 fprintf (dump_file
, "\n");
1638 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e2
]);
1640 "\nequations have no solution \n");
1642 return normalize_false
;
1645 if (pb
->geqs
[e2
].coef
[0] == -cTerm
1647 || pb
->geqs
[e
].color
== omega_black
))
1649 omega_copy_eqn (&pb
->eqs
[pb
->num_eqs
], &pb
->geqs
[e
],
1651 if (pb
->geqs
[e
].color
== omega_black
)
1652 adding_equality_constraint (pb
, pb
->num_eqs
);
1654 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
1658 e2
= fast_lookup_red
[MAX_KEYS
- eKey
];
1660 if (e2
< e
&& pb
->geqs
[e2
].key
== -eKey
1661 && pb
->geqs
[e2
].color
== omega_red
)
1663 if (pb
->geqs
[e2
].coef
[0] < -cTerm
)
1665 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1667 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
1668 fprintf (dump_file
, "\n");
1669 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e2
]);
1671 "\nequations have no solution \n");
1673 return normalize_false
;
1676 if (pb
->geqs
[e2
].coef
[0] == -cTerm
&& create_color
)
1678 omega_copy_eqn (&pb
->eqs
[pb
->num_eqs
], &pb
->geqs
[e
],
1680 pb
->eqs
[pb
->num_eqs
].color
= omega_red
;
1682 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
1686 e2
= fast_lookup
[MAX_KEYS
+ eKey
];
1688 if (e2
< e
&& pb
->geqs
[e2
].key
== eKey
1689 && pb
->geqs
[e2
].color
== omega_black
)
1691 if (pb
->geqs
[e2
].coef
[0] > cTerm
)
1693 if (pb
->geqs
[e
].color
== omega_black
)
1695 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1698 "Removing Redundant Equation: ");
1699 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
1700 fprintf (dump_file
, "\n");
1702 "[a] Made Redundant by: ");
1703 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
1704 fprintf (dump_file
, "\n");
1706 pb
->geqs
[e2
].coef
[0] = cTerm
;
1707 omega_delete_geq (pb
, e
, n_vars
);
1714 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1716 fprintf (dump_file
, "Removing Redundant Equation: ");
1717 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
1718 fprintf (dump_file
, "\n");
1719 fprintf (dump_file
, "[b] Made Redundant by: ");
1720 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
1721 fprintf (dump_file
, "\n");
1723 omega_delete_geq (pb
, e
, n_vars
);
1729 e2
= fast_lookup_red
[MAX_KEYS
+ eKey
];
1731 if (e2
< e
&& pb
->geqs
[e2
].key
== eKey
1732 && pb
->geqs
[e2
].color
== omega_red
)
1734 if (pb
->geqs
[e2
].coef
[0] >= cTerm
)
1736 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1738 fprintf (dump_file
, "Removing Redundant Equation: ");
1739 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
1740 fprintf (dump_file
, "\n");
1741 fprintf (dump_file
, "[c] Made Redundant by: ");
1742 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
1743 fprintf (dump_file
, "\n");
1745 pb
->geqs
[e2
].coef
[0] = cTerm
;
1746 pb
->geqs
[e2
].color
= pb
->geqs
[e
].color
;
1748 else if (pb
->geqs
[e
].color
== omega_red
)
1750 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1752 fprintf (dump_file
, "Removing Redundant Equation: ");
1753 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
1754 fprintf (dump_file
, "\n");
1755 fprintf (dump_file
, "[d] Made Redundant by: ");
1756 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
1757 fprintf (dump_file
, "\n");
1760 omega_delete_geq (pb
, e
, n_vars
);
1767 if (pb
->geqs
[e
].color
== omega_red
)
1768 fast_lookup_red
[MAX_KEYS
+ eKey
] = e
;
1770 fast_lookup
[MAX_KEYS
+ eKey
] = e
;
1774 create_color
= false;
1775 return coupled_subscripts
? normalize_coupled
: normalize_uncoupled
;
1778 /* Divide the coefficients of EQN by their gcd. N_VARS is the number
1779 of variables in EQN. */
1782 divide_eqn_by_gcd (eqn eqn
, int n_vars
)
1786 for (var
= n_vars
; var
>= 0; var
--)
1787 g
= gcd (abs (eqn
->coef
[var
]), g
);
1790 for (var
= n_vars
; var
>= 0; var
--)
1791 eqn
->coef
[var
] = eqn
->coef
[var
] / g
;
1794 /* Rewrite some non-safe variables in function of protected
1795 wildcard variables. */
1798 cleanout_wildcards (omega_pb pb
)
1801 int n_vars
= pb
->num_vars
;
1802 bool renormalize
= false;
1804 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
1805 for (i
= n_vars
; !omega_safe_var_p (pb
, i
); i
--)
1806 if (pb
->eqs
[e
].coef
[i
] != 0)
1808 /* i is the last nonzero non-safe variable. */
1810 for (j
= i
- 1; !omega_safe_var_p (pb
, j
); j
--)
1811 if (pb
->eqs
[e
].coef
[j
] != 0)
1814 /* j is the next nonzero non-safe variable, or points
1815 to a safe variable: it is then a wildcard variable. */
1818 if (omega_safe_var_p (pb
, j
))
1820 eqn sub
= &(pb
->eqs
[e
]);
1821 int c
= pb
->eqs
[e
].coef
[i
];
1825 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1828 "Found a single wild card equality: ");
1829 omega_print_eq (dump_file
, pb
, &pb
->eqs
[e
]);
1830 fprintf (dump_file
, "\n");
1831 omega_print_problem (dump_file
, pb
);
1834 for (e2
= pb
->num_eqs
- 1; e2
>= 0; e2
--)
1835 if (e
!= e2
&& pb
->eqs
[e2
].coef
[i
]
1836 && (pb
->eqs
[e2
].color
== omega_red
1837 || (pb
->eqs
[e2
].color
== omega_black
1838 && pb
->eqs
[e
].color
== omega_black
)))
1840 eqn eqn
= &(pb
->eqs
[e2
]);
1843 for (var
= n_vars
; var
>= 0; var
--)
1844 eqn
->coef
[var
] *= a
;
1848 for (var
= n_vars
; var
>= 0; var
--)
1849 eqn
->coef
[var
] -= sub
->coef
[var
] * k
/ c
;
1852 divide_eqn_by_gcd (eqn
, n_vars
);
1855 for (e2
= pb
->num_geqs
- 1; e2
>= 0; e2
--)
1856 if (pb
->geqs
[e2
].coef
[i
]
1857 && (pb
->geqs
[e2
].color
== omega_red
1858 || (pb
->eqs
[e
].color
== omega_black
1859 && pb
->geqs
[e2
].color
== omega_black
)))
1861 eqn eqn
= &(pb
->geqs
[e2
]);
1864 for (var
= n_vars
; var
>= 0; var
--)
1865 eqn
->coef
[var
] *= a
;
1869 for (var
= n_vars
; var
>= 0; var
--)
1870 eqn
->coef
[var
] -= sub
->coef
[var
] * k
/ c
;
1877 for (e2
= pb
->num_subs
- 1; e2
>= 0; e2
--)
1878 if (pb
->subs
[e2
].coef
[i
]
1879 && (pb
->subs
[e2
].color
== omega_red
1880 || (pb
->subs
[e2
].color
== omega_black
1881 && pb
->eqs
[e
].color
== omega_black
)))
1883 eqn eqn
= &(pb
->subs
[e2
]);
1886 for (var
= n_vars
; var
>= 0; var
--)
1887 eqn
->coef
[var
] *= a
;
1891 for (var
= n_vars
; var
>= 0; var
--)
1892 eqn
->coef
[var
] -= sub
->coef
[var
] * k
/ c
;
1895 divide_eqn_by_gcd (eqn
, n_vars
);
1898 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1900 fprintf (dump_file
, "cleaned-out wildcard: ");
1901 omega_print_problem (dump_file
, pb
);
1908 normalize_omega_problem (pb
);
1911 /* Swap values contained in I and J. */
1914 swap (int *i
, int *j
)
1922 /* Swap values contained in I and J. */
1925 bswap (bool *i
, bool *j
)
1933 /* Make variable IDX unprotected in PB, by swapping its index at the
1934 PB->safe_vars rank. */
1937 omega_unprotect_1 (omega_pb pb
, int *idx
, bool *unprotect
)
1939 /* If IDX is protected... */
1940 if (*idx
< pb
->safe_vars
)
1942 /* ... swap its index with the last non protected index. */
1943 int j
= pb
->safe_vars
;
1946 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1948 pb
->geqs
[e
].touched
= 1;
1949 swap (&pb
->geqs
[e
].coef
[*idx
], &pb
->geqs
[e
].coef
[j
]);
1952 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
1953 swap (&pb
->eqs
[e
].coef
[*idx
], &pb
->eqs
[e
].coef
[j
]);
1955 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
1956 swap (&pb
->subs
[e
].coef
[*idx
], &pb
->subs
[e
].coef
[j
]);
1959 bswap (&unprotect
[*idx
], &unprotect
[j
]);
1961 swap (&pb
->var
[*idx
], &pb
->var
[j
]);
1962 pb
->forwarding_address
[pb
->var
[*idx
]] = *idx
;
1963 pb
->forwarding_address
[pb
->var
[j
]] = j
;
1967 /* The variable at pb->safe_vars is also unprotected now. */
1971 /* During the Fourier-Motzkin elimination some variables are
1972 substituted with other variables. This function resurrects the
1973 substituted variables in PB. */
1976 resurrect_subs (omega_pb pb
)
1978 if (pb
->num_subs
> 0
1979 && please_no_equalities_in_simplified_problems
== 0)
1983 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
1986 "problem reduced, bringing variables back to life\n");
1987 omega_print_problem (dump_file
, pb
);
1990 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
1991 if (omega_wildcard_p (pb
, i
))
1992 omega_unprotect_1 (pb
, &i
, NULL
);
1995 n
= MAX (pb
->num_vars
, pb
->safe_vars
+ m
);
1997 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
1998 if (single_var_geq (&pb
->geqs
[e
], pb
->num_vars
))
2000 if (!omega_safe_var_p (pb
, abs (pb
->geqs
[e
].key
)))
2001 pb
->geqs
[e
].key
+= (pb
->geqs
[e
].key
> 0 ? m
: -m
);
2005 pb
->geqs
[e
].touched
= 1;
2006 pb
->geqs
[e
].key
= 0;
2009 for (i
= pb
->num_vars
; !omega_safe_var_p (pb
, i
); i
--)
2011 pb
->var
[i
+ m
] = pb
->var
[i
];
2013 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2014 pb
->geqs
[e
].coef
[i
+ m
] = pb
->geqs
[e
].coef
[i
];
2016 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
2017 pb
->eqs
[e
].coef
[i
+ m
] = pb
->eqs
[e
].coef
[i
];
2019 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
2020 pb
->subs
[e
].coef
[i
+ m
] = pb
->subs
[e
].coef
[i
];
2023 for (i
= pb
->safe_vars
+ m
; !omega_safe_var_p (pb
, i
); i
--)
2025 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2026 pb
->geqs
[e
].coef
[i
] = 0;
2028 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
2029 pb
->eqs
[e
].coef
[i
] = 0;
2031 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
2032 pb
->subs
[e
].coef
[i
] = 0;
2037 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
2039 pb
->var
[pb
->safe_vars
+ 1 + e
] = pb
->subs
[e
].key
;
2040 omega_copy_eqn (&(pb
->eqs
[pb
->num_eqs
]), &(pb
->subs
[e
]),
2042 pb
->eqs
[pb
->num_eqs
].coef
[pb
->safe_vars
+ 1 + e
] = -1;
2043 pb
->eqs
[pb
->num_eqs
].color
= omega_black
;
2045 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2047 fprintf (dump_file
, "brought back: ");
2048 omega_print_eq (dump_file
, pb
, &pb
->eqs
[pb
->num_eqs
]);
2049 fprintf (dump_file
, "\n");
2053 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
2059 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2061 fprintf (dump_file
, "variables brought back to life\n");
2062 omega_print_problem (dump_file
, pb
);
2065 cleanout_wildcards (pb
);
2070 implies (unsigned int a
, unsigned int b
)
2072 return (a
== (a
& b
));
2075 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an
2076 extra step is performed. Returns omega_false when there exist no
2077 solution, omega_true otherwise. */
2080 omega_eliminate_redundant (omega_pb pb
, bool expensive
)
2082 int c
, e
, e1
, e2
, e3
, p
, q
, i
, k
, alpha
, alpha1
, alpha2
, alpha3
;
2083 bool *is_dead
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
2084 omega_pb tmp_problem
;
2086 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */
2087 unsigned int *peqs
= XNEWVEC (unsigned int, OMEGA_MAX_GEQS
);
2088 unsigned int *zeqs
= XNEWVEC (unsigned int, OMEGA_MAX_GEQS
);
2089 unsigned int *neqs
= XNEWVEC (unsigned int, OMEGA_MAX_GEQS
);
2091 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2092 unsigned int pp
, pz
, pn
;
2094 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2096 fprintf (dump_file
, "in eliminate Redundant:\n");
2097 omega_print_problem (dump_file
, pb
);
2100 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2105 peqs
[e
] = zeqs
[e
] = neqs
[e
] = 0;
2107 for (i
= pb
->num_vars
; i
>= 1; i
--)
2109 if (pb
->geqs
[e
].coef
[i
] > 0)
2111 else if (pb
->geqs
[e
].coef
[i
] < 0)
2121 for (e1
= pb
->num_geqs
- 1; e1
>= 0; e1
--)
2123 for (e2
= e1
- 1; e2
>= 0; e2
--)
2126 for (p
= pb
->num_vars
; p
> 1; p
--)
2127 for (q
= p
- 1; q
> 0; q
--)
2128 if ((alpha
= pb
->geqs
[e1
].coef
[p
] * pb
->geqs
[e2
].coef
[q
]
2129 - pb
->geqs
[e2
].coef
[p
] * pb
->geqs
[e1
].coef
[q
]) != 0)
2135 pz
= ((zeqs
[e1
] & zeqs
[e2
]) | (peqs
[e1
] & neqs
[e2
])
2136 | (neqs
[e1
] & peqs
[e2
]));
2137 pp
= peqs
[e1
] | peqs
[e2
];
2138 pn
= neqs
[e1
] | neqs
[e2
];
2140 for (e3
= pb
->num_geqs
- 1; e3
>= 0; e3
--)
2141 if (e3
!= e1
&& e3
!= e2
)
2143 if (!implies (zeqs
[e3
], pz
))
2146 alpha1
= (pb
->geqs
[e2
].coef
[q
] * pb
->geqs
[e3
].coef
[p
]
2147 - pb
->geqs
[e2
].coef
[p
] * pb
->geqs
[e3
].coef
[q
]);
2148 alpha2
= -(pb
->geqs
[e1
].coef
[q
] * pb
->geqs
[e3
].coef
[p
]
2149 - pb
->geqs
[e1
].coef
[p
] * pb
->geqs
[e3
].coef
[q
]);
2152 if (alpha1
* alpha2
<= 0)
2164 /* Trying to prove e3 is redundant. */
2165 if (!implies (peqs
[e3
], pp
)
2166 || !implies (neqs
[e3
], pn
))
2169 if (pb
->geqs
[e3
].color
== omega_black
2170 && (pb
->geqs
[e1
].color
== omega_red
2171 || pb
->geqs
[e2
].color
== omega_red
))
2174 for (k
= pb
->num_vars
; k
>= 1; k
--)
2175 if (alpha3
* pb
->geqs
[e3
].coef
[k
]
2176 != (alpha1
* pb
->geqs
[e1
].coef
[k
]
2177 + alpha2
* pb
->geqs
[e2
].coef
[k
]))
2180 c
= (alpha1
* pb
->geqs
[e1
].coef
[0]
2181 + alpha2
* pb
->geqs
[e2
].coef
[0]);
2183 if (c
< alpha3
* (pb
->geqs
[e3
].coef
[0] + 1))
2185 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2188 "found redundant inequality\n");
2190 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2191 alpha1
, alpha2
, alpha3
);
2193 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e1
]));
2194 fprintf (dump_file
, "\n");
2195 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
2196 fprintf (dump_file
, "\n=> ");
2197 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e3
]));
2198 fprintf (dump_file
, "\n\n");
2206 /* Trying to prove e3 <= 0 and therefore e3 = 0,
2207 or trying to prove e3 < 0, and therefore the
2208 problem has no solutions. */
2209 if (!implies (peqs
[e3
], pn
)
2210 || !implies (neqs
[e3
], pp
))
2213 if (pb
->geqs
[e1
].color
== omega_red
2214 || pb
->geqs
[e2
].color
== omega_red
2215 || pb
->geqs
[e3
].color
== omega_red
)
2219 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2220 for (k
= pb
->num_vars
; k
>= 1; k
--)
2221 if (alpha3
* pb
->geqs
[e3
].coef
[k
]
2222 != (alpha1
* pb
->geqs
[e1
].coef
[k
]
2223 + alpha2
* pb
->geqs
[e2
].coef
[k
]))
2226 c
= (alpha1
* pb
->geqs
[e1
].coef
[0]
2227 + alpha2
* pb
->geqs
[e2
].coef
[0]);
2229 if (c
< alpha3
* (pb
->geqs
[e3
].coef
[0]))
2231 /* We just proved e3 < 0, so no solutions exist. */
2232 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2235 "found implied over tight inequality\n");
2237 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2238 alpha1
, alpha2
, -alpha3
);
2239 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e1
]));
2240 fprintf (dump_file
, "\n");
2241 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
2242 fprintf (dump_file
, "\n=> not ");
2243 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e3
]));
2244 fprintf (dump_file
, "\n\n");
2252 else if (c
< alpha3
* (pb
->geqs
[e3
].coef
[0] - 1))
2254 /* We just proved that e3 <=0, so e3 = 0. */
2255 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2258 "found implied tight inequality\n");
2260 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2261 alpha1
, alpha2
, -alpha3
);
2262 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e1
]));
2263 fprintf (dump_file
, "\n");
2264 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
2265 fprintf (dump_file
, "\n=> inverse ");
2266 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e3
]));
2267 fprintf (dump_file
, "\n\n");
2270 omega_copy_eqn (&pb
->eqs
[pb
->num_eqs
++],
2271 &pb
->geqs
[e3
], pb
->num_vars
);
2272 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
2273 adding_equality_constraint (pb
, pb
->num_eqs
- 1);
2281 /* Delete the inequalities that were marked as dead. */
2282 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2284 omega_delete_geq (pb
, e
, pb
->num_vars
);
2287 goto eliminate_redundant_done
;
2289 tmp_problem
= XNEW (struct omega_pb
);
2292 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2294 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2297 "checking equation %d to see if it is redundant: ", e
);
2298 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
2299 fprintf (dump_file
, "\n");
2302 omega_copy_problem (tmp_problem
, pb
);
2303 omega_negate_geq (tmp_problem
, e
);
2304 tmp_problem
->safe_vars
= 0;
2305 tmp_problem
->variables_freed
= false;
2307 if (omega_solve_problem (tmp_problem
, omega_false
) == omega_false
)
2308 omega_delete_geq (pb
, e
, pb
->num_vars
);
2314 if (!omega_reduce_with_subs
)
2316 resurrect_subs (pb
);
2317 gcc_assert (please_no_equalities_in_simplified_problems
2318 || pb
->num_subs
== 0);
2321 eliminate_redundant_done
:
2329 /* For each inequality that has coefficients bigger than 20, try to
2330 create a new constraint that cannot be derived from the original
2331 constraint and that has smaller coefficients. Add the new
2332 constraint at the end of geqs. Return the number of inequalities
2333 that have been added to PB. */
2336 smooth_weird_equations (omega_pb pb
)
2338 int e1
, e2
, e3
, p
, q
, k
, alpha
, alpha1
, alpha2
, alpha3
;
2343 for (e1
= pb
->num_geqs
- 1; e1
>= 0; e1
--)
2344 if (pb
->geqs
[e1
].color
== omega_black
)
2348 for (v
= pb
->num_vars
; v
>= 1; v
--)
2349 if (pb
->geqs
[e1
].coef
[v
] != 0 && abs (pb
->geqs
[e1
].coef
[v
]) < g
)
2350 g
= abs (pb
->geqs
[e1
].coef
[v
]);
2357 for (v
= pb
->num_vars
; v
>= 1; v
--)
2358 pb
->geqs
[e3
].coef
[v
] = int_div (6 * pb
->geqs
[e1
].coef
[v
] + g
/ 2,
2361 pb
->geqs
[e3
].color
= omega_black
;
2362 pb
->geqs
[e3
].touched
= 1;
2364 pb
->geqs
[e3
].coef
[0] = 9997;
2366 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2368 fprintf (dump_file
, "Checking to see if we can derive: ");
2369 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e3
]);
2370 fprintf (dump_file
, "\n from: ");
2371 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e1
]);
2372 fprintf (dump_file
, "\n");
2375 for (e2
= pb
->num_geqs
- 1; e2
>= 0; e2
--)
2376 if (e1
!= e2
&& pb
->geqs
[e2
].color
== omega_black
)
2378 for (p
= pb
->num_vars
; p
> 1; p
--)
2380 for (q
= p
- 1; q
> 0; q
--)
2383 (pb
->geqs
[e1
].coef
[p
] * pb
->geqs
[e2
].coef
[q
] -
2384 pb
->geqs
[e2
].coef
[p
] * pb
->geqs
[e1
].coef
[q
]);
2393 alpha1
= (pb
->geqs
[e2
].coef
[q
] * pb
->geqs
[e3
].coef
[p
]
2394 - pb
->geqs
[e2
].coef
[p
] * pb
->geqs
[e3
].coef
[q
]);
2395 alpha2
= -(pb
->geqs
[e1
].coef
[q
] * pb
->geqs
[e3
].coef
[p
]
2396 - pb
->geqs
[e1
].coef
[p
] * pb
->geqs
[e3
].coef
[q
]);
2399 if (alpha1
* alpha2
<= 0)
2411 /* Try to prove e3 is redundant: verify
2412 alpha1*v1 + alpha2*v2 = alpha3*v3. */
2413 for (k
= pb
->num_vars
; k
>= 1; k
--)
2414 if (alpha3
* pb
->geqs
[e3
].coef
[k
]
2415 != (alpha1
* pb
->geqs
[e1
].coef
[k
]
2416 + alpha2
* pb
->geqs
[e2
].coef
[k
]))
2419 c
= alpha1
* pb
->geqs
[e1
].coef
[0]
2420 + alpha2
* pb
->geqs
[e2
].coef
[0];
2422 if (c
< alpha3
* (pb
->geqs
[e3
].coef
[0] + 1))
2423 pb
->geqs
[e3
].coef
[0] = int_div (c
, alpha3
);
2428 if (pb
->geqs
[e3
].coef
[0] < 9997)
2433 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2436 "Smoothing weird equations; adding:\n");
2437 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e3
]);
2438 fprintf (dump_file
, "\nto:\n");
2439 omega_print_problem (dump_file
, pb
);
2440 fprintf (dump_file
, "\n\n");
2448 /* Replace tuples of inequalities, that define upper and lower half
2449 spaces, with an equation. */
2452 coalesce (omega_pb pb
)
2457 int found_something
= 0;
2459 for (e
= 0; e
< pb
->num_geqs
; e
++)
2460 if (pb
->geqs
[e
].color
== omega_red
)
2466 is_dead
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
2468 for (e
= 0; e
< pb
->num_geqs
; e
++)
2471 for (e
= 0; e
< pb
->num_geqs
; e
++)
2472 if (pb
->geqs
[e
].color
== omega_red
2473 && !pb
->geqs
[e
].touched
)
2474 for (e2
= e
+ 1; e2
< pb
->num_geqs
; e2
++)
2475 if (!pb
->geqs
[e2
].touched
2476 && pb
->geqs
[e
].key
== -pb
->geqs
[e2
].key
2477 && pb
->geqs
[e
].coef
[0] == -pb
->geqs
[e2
].coef
[0]
2478 && pb
->geqs
[e2
].color
== omega_red
)
2480 omega_copy_eqn (&pb
->eqs
[pb
->num_eqs
++], &pb
->geqs
[e
],
2482 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
2488 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2490 omega_delete_geq (pb
, e
, pb
->num_vars
);
2492 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && found_something
)
2494 fprintf (dump_file
, "Coalesced pb->geqs into %d EQ's:\n",
2496 omega_print_problem (dump_file
, pb
);
2502 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2503 true, continue to eliminate all the red inequalities. */
2506 omega_eliminate_red (omega_pb pb
, bool eliminate_all
)
2508 int e
, e2
, e3
, i
, j
, k
, a
, alpha1
, alpha2
;
2510 bool *is_dead
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
2513 omega_pb tmp_problem
;
2515 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2517 fprintf (dump_file
, "in eliminate RED:\n");
2518 omega_print_problem (dump_file
, pb
);
2521 if (pb
->num_eqs
> 0)
2522 omega_simplify_problem (pb
);
2524 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2527 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2528 if (pb
->geqs
[e
].color
== omega_black
&& !is_dead
[e
])
2529 for (e2
= e
- 1; e2
>= 0; e2
--)
2530 if (pb
->geqs
[e2
].color
== omega_black
2535 for (i
= pb
->num_vars
; i
> 1; i
--)
2536 for (j
= i
- 1; j
> 0; j
--)
2537 if ((a
= (pb
->geqs
[e
].coef
[i
] * pb
->geqs
[e2
].coef
[j
]
2538 - pb
->geqs
[e2
].coef
[i
] * pb
->geqs
[e
].coef
[j
])) != 0)
2544 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2547 "found two equations to combine, i = %s, ",
2548 omega_variable_to_str (pb
, i
));
2549 fprintf (dump_file
, "j = %s, alpha = %d\n",
2550 omega_variable_to_str (pb
, j
), a
);
2551 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
2552 fprintf (dump_file
, "\n");
2553 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
2554 fprintf (dump_file
, "\n");
2557 for (e3
= pb
->num_geqs
- 1; e3
>= 0; e3
--)
2558 if (pb
->geqs
[e3
].color
== omega_red
)
2560 alpha1
= (pb
->geqs
[e2
].coef
[j
] * pb
->geqs
[e3
].coef
[i
]
2561 - pb
->geqs
[e2
].coef
[i
] * pb
->geqs
[e3
].coef
[j
]);
2562 alpha2
= -(pb
->geqs
[e
].coef
[j
] * pb
->geqs
[e3
].coef
[i
]
2563 - pb
->geqs
[e
].coef
[i
] * pb
->geqs
[e3
].coef
[j
]);
2565 if ((a
> 0 && alpha1
> 0 && alpha2
> 0)
2566 || (a
< 0 && alpha1
< 0 && alpha2
< 0))
2568 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2571 "alpha1 = %d, alpha2 = %d;"
2572 "comparing against: ",
2574 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e3
]));
2575 fprintf (dump_file
, "\n");
2578 for (k
= pb
->num_vars
; k
>= 0; k
--)
2580 c
= (alpha1
* pb
->geqs
[e
].coef
[k
]
2581 + alpha2
* pb
->geqs
[e2
].coef
[k
]);
2583 if (c
!= a
* pb
->geqs
[e3
].coef
[k
])
2586 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && k
> 0)
2587 fprintf (dump_file
, " %s: %d, %d\n",
2588 omega_variable_to_str (pb
, k
), c
,
2589 a
* pb
->geqs
[e3
].coef
[k
]);
2594 ((a
> 0 && c
< a
* pb
->geqs
[e3
].coef
[k
])
2595 || (a
< 0 && c
> a
* pb
->geqs
[e3
].coef
[k
]))))
2597 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2601 "red equation#%d is dead "
2602 "(%d dead so far, %d remain)\n",
2604 pb
->num_geqs
- dead_count
);
2605 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
2606 fprintf (dump_file
, "\n");
2607 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e2
]));
2608 fprintf (dump_file
, "\n");
2609 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e3
]));
2610 fprintf (dump_file
, "\n");
2618 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2620 omega_delete_geq (pb
, e
, pb
->num_vars
);
2624 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2626 fprintf (dump_file
, "in eliminate RED, easy tests done:\n");
2627 omega_print_problem (dump_file
, pb
);
2630 for (red_found
= 0, e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2631 if (pb
->geqs
[e
].color
== omega_red
)
2636 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2637 fprintf (dump_file
, "fast checks worked\n");
2639 if (!omega_reduce_with_subs
)
2640 gcc_assert (please_no_equalities_in_simplified_problems
2641 || pb
->num_subs
== 0);
2646 if (!omega_verify_simplification
2647 && verify_omega_pb (pb
) == omega_false
)
2651 tmp_problem
= XNEW (struct omega_pb
);
2653 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2654 if (pb
->geqs
[e
].color
== omega_red
)
2656 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2659 "checking equation %d to see if it is redundant: ", e
);
2660 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[e
]));
2661 fprintf (dump_file
, "\n");
2664 omega_copy_problem (tmp_problem
, pb
);
2665 omega_negate_geq (tmp_problem
, e
);
2666 tmp_problem
->safe_vars
= 0;
2667 tmp_problem
->variables_freed
= false;
2668 tmp_problem
->num_subs
= 0;
2670 if (omega_solve_problem (tmp_problem
, omega_false
) == omega_false
)
2672 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2673 fprintf (dump_file
, "it is redundant\n");
2674 omega_delete_geq (pb
, e
, pb
->num_vars
);
2678 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2679 fprintf (dump_file
, "it is not redundant\n");
2683 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2684 fprintf (dump_file
, "no need to check other red equations\n");
2692 /* omega_simplify_problem (pb); */
2694 if (!omega_reduce_with_subs
)
2695 gcc_assert (please_no_equalities_in_simplified_problems
2696 || pb
->num_subs
== 0);
2699 /* Transform some wildcard variables to non-safe variables. */
2702 chain_unprotect (omega_pb pb
)
2705 bool *unprotect
= XNEWVEC (bool, OMEGA_MAX_VARS
);
2707 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
2709 unprotect
[i
] = omega_wildcard_p (pb
, i
);
2711 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
2712 if (pb
->subs
[e
].coef
[i
])
2713 unprotect
[i
] = false;
2716 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2718 fprintf (dump_file
, "Doing chain reaction unprotection\n");
2719 omega_print_problem (dump_file
, pb
);
2721 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
2723 fprintf (dump_file
, "unprotecting %s\n",
2724 omega_variable_to_str (pb
, i
));
2727 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
2729 omega_unprotect_1 (pb
, &i
, unprotect
);
2731 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2733 fprintf (dump_file
, "After chain reactions\n");
2734 omega_print_problem (dump_file
, pb
);
2740 /* Reduce problem PB. */
2743 omega_problem_reduced (omega_pb pb
)
2745 if (omega_verify_simplification
2746 && !in_approximate_mode
2747 && verify_omega_pb (pb
) == omega_false
)
2750 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS
)
2751 && !omega_eliminate_redundant (pb
, true))
2754 omega_found_reduction
= omega_true
;
2756 if (!please_no_equalities_in_simplified_problems
)
2759 if (omega_reduce_with_subs
2760 || please_no_equalities_in_simplified_problems
)
2761 chain_unprotect (pb
);
2763 resurrect_subs (pb
);
2765 if (!return_single_result
)
2769 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
2770 pb
->forwarding_address
[pb
->var
[i
]] = i
;
2772 for (i
= 0; i
< pb
->num_subs
; i
++)
2773 pb
->forwarding_address
[pb
->subs
[i
].key
] = -i
- 1;
2775 (*omega_when_reduced
) (pb
);
2778 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2780 fprintf (dump_file
, "-------------------------------------------\n");
2781 fprintf (dump_file
, "problem reduced:\n");
2782 omega_print_problem (dump_file
, pb
);
2783 fprintf (dump_file
, "-------------------------------------------\n");
2787 /* Eliminates all the free variables for problem PB, that is all the
2788 variables from FV to PB->NUM_VARS. */
2791 omega_free_eliminations (omega_pb pb
, int fv
)
2793 bool try_again
= true;
2795 int n_vars
= pb
->num_vars
;
2801 for (i
= n_vars
; i
> fv
; i
--)
2803 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2804 if (pb
->geqs
[e
].coef
[i
])
2809 else if (pb
->geqs
[e
].coef
[i
] > 0)
2811 for (e2
= e
- 1; e2
>= 0; e2
--)
2812 if (pb
->geqs
[e2
].coef
[i
] < 0)
2817 for (e2
= e
- 1; e2
>= 0; e2
--)
2818 if (pb
->geqs
[e2
].coef
[i
] > 0)
2825 for (e3
= pb
->num_subs
- 1; e3
>= 0; e3
--)
2826 if (pb
->subs
[e3
].coef
[i
])
2832 for (e3
= pb
->num_eqs
- 1; e3
>= 0; e3
--)
2833 if (pb
->eqs
[e3
].coef
[i
])
2839 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2840 fprintf (dump_file
, "a free elimination of %s\n",
2841 omega_variable_to_str (pb
, i
));
2845 omega_delete_geq (pb
, e
, n_vars
);
2847 for (e
--; e
>= 0; e
--)
2848 if (pb
->geqs
[e
].coef
[i
])
2849 omega_delete_geq (pb
, e
, n_vars
);
2851 try_again
= (i
< n_vars
);
2854 omega_delete_variable (pb
, i
);
2855 n_vars
= pb
->num_vars
;
2860 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2862 fprintf (dump_file
, "\nafter free eliminations:\n");
2863 omega_print_problem (dump_file
, pb
);
2864 fprintf (dump_file
, "\n");
2868 /* Do free red eliminations. */
2871 free_red_eliminations (omega_pb pb
)
2873 bool try_again
= true;
2875 int n_vars
= pb
->num_vars
;
2876 bool *is_red_var
= XNEWVEC (bool, OMEGA_MAX_VARS
);
2877 bool *is_dead_var
= XNEWVEC (bool, OMEGA_MAX_VARS
);
2878 bool *is_dead_geq
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
2880 for (i
= n_vars
; i
> 0; i
--)
2882 is_red_var
[i
] = false;
2883 is_dead_var
[i
] = false;
2886 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2888 is_dead_geq
[e
] = false;
2890 if (pb
->geqs
[e
].color
== omega_red
)
2891 for (i
= n_vars
; i
> 0; i
--)
2892 if (pb
->geqs
[e
].coef
[i
] != 0)
2893 is_red_var
[i
] = true;
2899 for (i
= n_vars
; i
> 0; i
--)
2900 if (!is_red_var
[i
] && !is_dead_var
[i
])
2902 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2903 if (!is_dead_geq
[e
] && pb
->geqs
[e
].coef
[i
])
2908 else if (pb
->geqs
[e
].coef
[i
] > 0)
2910 for (e2
= e
- 1; e2
>= 0; e2
--)
2911 if (!is_dead_geq
[e2
] && pb
->geqs
[e2
].coef
[i
] < 0)
2916 for (e2
= e
- 1; e2
>= 0; e2
--)
2917 if (!is_dead_geq
[e2
] && pb
->geqs
[e2
].coef
[i
] > 0)
2924 for (e3
= pb
->num_subs
- 1; e3
>= 0; e3
--)
2925 if (pb
->subs
[e3
].coef
[i
])
2931 for (e3
= pb
->num_eqs
- 1; e3
>= 0; e3
--)
2932 if (pb
->eqs
[e3
].coef
[i
])
2938 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2939 fprintf (dump_file
, "a free red elimination of %s\n",
2940 omega_variable_to_str (pb
, i
));
2943 if (pb
->geqs
[e
].coef
[i
])
2944 is_dead_geq
[e
] = true;
2947 is_dead_var
[i
] = true;
2952 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
2954 omega_delete_geq (pb
, e
, n_vars
);
2956 for (i
= n_vars
; i
> 0; i
--)
2958 omega_delete_variable (pb
, i
);
2960 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2962 fprintf (dump_file
, "\nafter free red eliminations:\n");
2963 omega_print_problem (dump_file
, pb
);
2964 fprintf (dump_file
, "\n");
2972 /* For equation EQ of the form "0 = EQN", insert in PB two
2973 inequalities "0 <= EQN" and "0 <= -EQN". */
2976 omega_convert_eq_to_geqs (omega_pb pb
, int eq
)
2980 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2981 fprintf (dump_file
, "Converting Eq to Geqs\n");
2983 /* Insert "0 <= EQN". */
2984 omega_copy_eqn (&pb
->geqs
[pb
->num_geqs
], &pb
->eqs
[eq
], pb
->num_vars
);
2985 pb
->geqs
[pb
->num_geqs
].touched
= 1;
2988 /* Insert "0 <= -EQN". */
2989 omega_copy_eqn (&pb
->geqs
[pb
->num_geqs
], &pb
->eqs
[eq
], pb
->num_vars
);
2990 pb
->geqs
[pb
->num_geqs
].touched
= 1;
2992 for (i
= 0; i
<= pb
->num_vars
; i
++)
2993 pb
->geqs
[pb
->num_geqs
].coef
[i
] *= -1;
2997 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
2998 omega_print_problem (dump_file
, pb
);
3001 /* Eliminates variable I from PB. */
3004 omega_do_elimination (omega_pb pb
, int e
, int i
)
3006 eqn sub
= omega_alloc_eqns (0, 1);
3008 int n_vars
= pb
->num_vars
;
3010 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3011 fprintf (dump_file
, "eliminating variable %s\n",
3012 omega_variable_to_str (pb
, i
));
3014 omega_copy_eqn (sub
, &pb
->eqs
[e
], pb
->num_vars
);
3017 if (c
== 1 || c
== -1)
3019 if (pb
->eqs
[e
].color
== omega_red
)
3022 omega_substitute_red (pb
, sub
, i
, c
, &fB
);
3024 omega_convert_eq_to_geqs (pb
, e
);
3026 omega_delete_variable (pb
, i
);
3030 omega_substitute (pb
, sub
, i
, c
);
3031 omega_delete_variable (pb
, i
);
3039 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3040 fprintf (dump_file
, "performing non-exact elimination, c = %d\n", c
);
3042 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
3043 if (pb
->eqs
[e
].coef
[i
])
3045 eqn eqn
= &(pb
->eqs
[e
]);
3047 for (j
= n_vars
; j
>= 0; j
--)
3051 if (sub
->color
== omega_red
)
3052 eqn
->color
= omega_red
;
3053 for (j
= n_vars
; j
>= 0; j
--)
3054 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3057 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3058 if (pb
->geqs
[e
].coef
[i
])
3060 eqn eqn
= &(pb
->geqs
[e
]);
3063 if (sub
->color
== omega_red
)
3064 eqn
->color
= omega_red
;
3066 for (j
= n_vars
; j
>= 0; j
--)
3073 for (j
= n_vars
; j
>= 0; j
--)
3074 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3078 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
3079 if (pb
->subs
[e
].coef
[i
])
3081 eqn eqn
= &(pb
->subs
[e
]);
3084 gcc_assert (sub
->color
== omega_black
);
3085 for (j
= n_vars
; j
>= 0; j
--)
3089 for (j
= n_vars
; j
>= 0; j
--)
3090 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3093 if (in_approximate_mode
)
3094 omega_delete_variable (pb
, i
);
3096 omega_convert_eq_to_geqs (pb
, e2
);
3099 omega_free_eqns (sub
, 1);
3102 /* Helper function for printing "sorry, no solution". */
3104 static inline enum omega_result
3105 omega_problem_has_no_solution (void)
3107 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3108 fprintf (dump_file
, "\nequations have no solution \n");
3113 /* Helper function: solve equations in PB one at a time, following the
3114 DESIRED_RES result. */
3116 static enum omega_result
3117 omega_solve_eq (omega_pb pb
, enum omega_result desired_res
)
3124 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && pb
->num_eqs
> 0)
3126 fprintf (dump_file
, "\nomega_solve_eq (%d, %d)\n",
3127 desired_res
, may_be_red
);
3128 omega_print_problem (dump_file
, pb
);
3129 fprintf (dump_file
, "\n");
3135 j
= pb
->num_eqs
- 1;
3141 while (i
<= j
&& pb
->eqs
[i
].color
== omega_red
)
3144 while (i
<= j
&& pb
->eqs
[j
].color
== omega_black
)
3150 eq
= omega_alloc_eqns (0, 1);
3151 omega_copy_eqn (eq
, &pb
->eqs
[i
], pb
->num_vars
);
3152 omega_copy_eqn (&pb
->eqs
[i
], &pb
->eqs
[j
], pb
->num_vars
);
3153 omega_copy_eqn (&pb
->eqs
[j
], eq
, pb
->num_vars
);
3154 omega_free_eqns (eq
, 1);
3160 /* Eliminate all EQ equations */
3161 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
3163 eqn eqn
= &(pb
->eqs
[e
]);
3166 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3167 fprintf (dump_file
, "----\n");
3169 for (i
= pb
->num_vars
; i
> 0; i
--)
3175 for (j
= i
- 1; j
> 0; j
--)
3179 /* i is the position of last nonzero coefficient,
3180 g is the coefficient of i,
3181 j is the position of next nonzero coefficient. */
3185 if (eqn
->coef
[0] % g
!= 0)
3186 return omega_problem_has_no_solution ();
3188 eqn
->coef
[0] = eqn
->coef
[0] / g
;
3191 omega_do_elimination (pb
, e
, i
);
3197 if (eqn
->coef
[0] != 0)
3198 return omega_problem_has_no_solution ();
3210 omega_do_elimination (pb
, e
, i
);
3216 bool promotion_possible
=
3217 (omega_safe_var_p (pb
, j
)
3218 && pb
->safe_vars
+ 1 == i
3219 && !omega_eqn_is_red (eqn
, desired_res
)
3220 && !in_approximate_mode
);
3222 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && promotion_possible
)
3223 fprintf (dump_file
, " Promotion possible\n");
3226 if (!omega_safe_var_p (pb
, j
))
3228 for (; g
!= 1 && !omega_safe_var_p (pb
, j
); j
--)
3229 g
= gcd (abs (eqn
->coef
[j
]), g
);
3232 else if (!omega_safe_var_p (pb
, i
))
3237 for (; g
!= 1 && j
> 0; j
--)
3238 g
= gcd (abs (eqn
->coef
[j
]), g
);
3242 if (eqn
->coef
[0] % g
!= 0)
3243 return omega_problem_has_no_solution ();
3245 for (j
= 0; j
<= pb
->num_vars
; j
++)
3255 for (e2
= e
- 1; e2
>= 0; e2
--)
3256 if (pb
->eqs
[e2
].coef
[i
])
3260 for (e2
= pb
->num_geqs
- 1; e2
>= 0; e2
--)
3261 if (pb
->geqs
[e2
].coef
[i
])
3265 for (e2
= pb
->num_subs
- 1; e2
>= 0; e2
--)
3266 if (pb
->subs
[e2
].coef
[i
])
3271 bool change
= false;
3273 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3275 fprintf (dump_file
, "Ha! We own it! \n");
3276 omega_print_eq (dump_file
, pb
, eqn
);
3277 fprintf (dump_file
, " \n");
3283 for (j
= i
- 1; j
>= 0; j
--)
3285 int t
= int_mod (eqn
->coef
[j
], g
);
3290 if (t
!= eqn
->coef
[j
])
3299 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3300 fprintf (dump_file
, "So what?\n");
3305 omega_name_wild_card (pb
, i
);
3307 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3309 omega_print_eq (dump_file
, pb
, eqn
);
3310 fprintf (dump_file
, " \n");
3319 if (promotion_possible
)
3321 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3323 fprintf (dump_file
, "promoting %s to safety\n",
3324 omega_variable_to_str (pb
, i
));
3325 omega_print_vars (dump_file
, pb
);
3330 if (!omega_wildcard_p (pb
, i
))
3331 omega_name_wild_card (pb
, i
);
3333 promotion_possible
= false;
3338 if (g2
> 1 && !in_approximate_mode
)
3340 if (pb
->eqs
[e
].color
== omega_red
)
3342 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3343 fprintf (dump_file
, "handling red equality\n");
3346 omega_do_elimination (pb
, e
, i
);
3350 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3353 "adding equation to handle safe variable \n");
3354 omega_print_eq (dump_file
, pb
, eqn
);
3355 fprintf (dump_file
, "\n----\n");
3356 omega_print_problem (dump_file
, pb
);
3357 fprintf (dump_file
, "\n----\n");
3358 fprintf (dump_file
, "\n----\n");
3361 i
= omega_add_new_wild_card (pb
);
3363 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
3364 omega_init_eqn_zero (&pb
->eqs
[e
+ 1], pb
->num_vars
);
3365 omega_copy_eqn (&pb
->eqs
[e
+ 1], eqn
, pb
->safe_vars
);
3367 for (j
= pb
->num_vars
; j
>= 0; j
--)
3369 pb
->eqs
[e
+ 1].coef
[j
] = int_mod (pb
->eqs
[e
+ 1].coef
[j
], g2
);
3371 if (2 * pb
->eqs
[e
+ 1].coef
[j
] >= g2
)
3372 pb
->eqs
[e
+ 1].coef
[j
] -= g2
;
3375 pb
->eqs
[e
+ 1].coef
[i
] = g2
;
3378 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3379 omega_print_problem (dump_file
, pb
);
3388 /* Find variable to eliminate. */
3391 gcc_assert (in_approximate_mode
);
3393 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3395 fprintf (dump_file
, "non-exact elimination: ");
3396 omega_print_eq (dump_file
, pb
, eqn
);
3397 fprintf (dump_file
, "\n");
3398 omega_print_problem (dump_file
, pb
);
3401 for (i
= pb
->num_vars
; i
> sv
; i
--)
3402 if (pb
->eqs
[e
].coef
[i
] != 0)
3406 for (i
= pb
->num_vars
; i
> sv
; i
--)
3407 if (pb
->eqs
[e
].coef
[i
] == 1 || pb
->eqs
[e
].coef
[i
] == -1)
3413 omega_do_elimination (pb
, e
, i
);
3415 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && g2
> 1)
3417 fprintf (dump_file
, "result of non-exact elimination:\n");
3418 omega_print_problem (dump_file
, pb
);
3423 int factor
= (INT_MAX
);
3426 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3427 fprintf (dump_file
, "doing moding\n");
3429 for (i
= pb
->num_vars
; i
!= sv
; i
--)
3430 if ((pb
->eqs
[e
].coef
[i
] & 1) != 0)
3435 for (; i
!= sv
; i
--)
3436 if ((pb
->eqs
[e
].coef
[i
] & 1) != 0)
3442 if (j
!= 0 && i
== sv
)
3444 omega_do_mod (pb
, 2, e
, j
);
3450 for (i
= pb
->num_vars
; i
!= sv
; i
--)
3451 if (pb
->eqs
[e
].coef
[i
] != 0
3452 && factor
> abs (pb
->eqs
[e
].coef
[i
]) + 1)
3454 factor
= abs (pb
->eqs
[e
].coef
[i
]) + 1;
3460 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3461 fprintf (dump_file
, "should not have happened\n");
3465 omega_do_mod (pb
, factor
, e
, j
);
3466 /* Go back and try this equation again. */
3473 return omega_unknown
;
3476 /* Transform an inequation E to an equality, then solve DIFF problems
3477 based on PB, and only differing by the constant part that is
3478 diminished by one, trying to figure out which of the constants
3481 static enum omega_result
3482 parallel_splinter (omega_pb pb
, int e
, int diff
,
3483 enum omega_result desired_res
)
3485 omega_pb tmp_problem
;
3488 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3490 fprintf (dump_file
, "Using parallel splintering\n");
3491 omega_print_problem (dump_file
, pb
);
3494 tmp_problem
= XNEW (struct omega_pb
);
3495 omega_copy_eqn (&pb
->eqs
[0], &pb
->geqs
[e
], pb
->num_vars
);
3498 for (i
= 0; i
<= diff
; i
++)
3500 omega_copy_problem (tmp_problem
, pb
);
3502 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3504 fprintf (dump_file
, "Splinter # %i\n", i
);
3505 omega_print_problem (dump_file
, pb
);
3508 if (omega_solve_problem (tmp_problem
, desired_res
) == omega_true
)
3514 pb
->eqs
[0].coef
[0]--;
3521 /* Helper function: solve equations one at a time. */
3523 static enum omega_result
3524 omega_solve_geq (omega_pb pb
, enum omega_result desired_res
)
3528 enum omega_result result
;
3529 bool coupled_subscripts
= false;
3530 bool smoothed
= false;
3531 bool eliminate_again
;
3532 bool tried_eliminating_redundant
= false;
3534 if (desired_res
!= omega_simplify
)
3542 gcc_assert (desired_res
== omega_simplify
|| pb
->num_subs
== 0);
3544 /* Verify that there are not too many inequalities. */
3545 gcc_assert (pb
->num_geqs
<= OMEGA_MAX_GEQS
);
3547 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3549 fprintf (dump_file
, "\nomega_solve_geq (%d,%d):\n",
3550 desired_res
, please_no_equalities_in_simplified_problems
);
3551 omega_print_problem (dump_file
, pb
);
3552 fprintf (dump_file
, "\n");
3555 n_vars
= pb
->num_vars
;
3559 enum omega_eqn_color u_color
= omega_black
;
3560 enum omega_eqn_color l_color
= omega_black
;
3561 int upper_bound
= pos_infinity
;
3562 int lower_bound
= neg_infinity
;
3564 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3566 int a
= pb
->geqs
[e
].coef
[1];
3567 int c
= pb
->geqs
[e
].coef
[0];
3569 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3573 return omega_problem_has_no_solution ();
3580 if (lower_bound
< -c
3581 || (lower_bound
== -c
3582 && !omega_eqn_is_red (&pb
->geqs
[e
], desired_res
)))
3585 l_color
= pb
->geqs
[e
].color
;
3591 c
= int_div (c
, -a
);
3594 || (upper_bound
== c
3595 && !omega_eqn_is_red (&pb
->geqs
[e
], desired_res
)))
3598 u_color
= pb
->geqs
[e
].color
;
3603 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3605 fprintf (dump_file
, "upper bound = %d\n", upper_bound
);
3606 fprintf (dump_file
, "lower bound = %d\n", lower_bound
);
3609 if (lower_bound
> upper_bound
)
3610 return omega_problem_has_no_solution ();
3612 if (desired_res
== omega_simplify
)
3615 if (pb
->safe_vars
== 1)
3618 if (lower_bound
== upper_bound
3619 && u_color
== omega_black
3620 && l_color
== omega_black
)
3622 pb
->eqs
[0].coef
[0] = -lower_bound
;
3623 pb
->eqs
[0].coef
[1] = 1;
3624 pb
->eqs
[0].color
= omega_black
;
3626 return omega_solve_problem (pb
, desired_res
);
3630 if (lower_bound
> neg_infinity
)
3632 pb
->geqs
[0].coef
[0] = -lower_bound
;
3633 pb
->geqs
[0].coef
[1] = 1;
3634 pb
->geqs
[0].key
= 1;
3635 pb
->geqs
[0].color
= l_color
;
3636 pb
->geqs
[0].touched
= 0;
3640 if (upper_bound
< pos_infinity
)
3642 pb
->geqs
[pb
->num_geqs
].coef
[0] = upper_bound
;
3643 pb
->geqs
[pb
->num_geqs
].coef
[1] = -1;
3644 pb
->geqs
[pb
->num_geqs
].key
= -1;
3645 pb
->geqs
[pb
->num_geqs
].color
= u_color
;
3646 pb
->geqs
[pb
->num_geqs
].touched
= 0;
3654 omega_problem_reduced (pb
);
3658 if (original_problem
!= no_problem
3659 && l_color
== omega_black
3660 && u_color
== omega_black
3662 && lower_bound
== upper_bound
)
3664 pb
->eqs
[0].coef
[0] = -lower_bound
;
3665 pb
->eqs
[0].coef
[1] = 1;
3667 adding_equality_constraint (pb
, 0);
3673 if (!pb
->variables_freed
)
3675 pb
->variables_freed
= true;
3677 if (desired_res
!= omega_simplify
)
3678 omega_free_eliminations (pb
, 0);
3680 omega_free_eliminations (pb
, pb
->safe_vars
);
3682 n_vars
= pb
->num_vars
;
3688 switch (normalize_omega_problem (pb
))
3690 case normalize_false
:
3694 case normalize_coupled
:
3695 coupled_subscripts
= true;
3698 case normalize_uncoupled
:
3699 coupled_subscripts
= false;
3706 n_vars
= pb
->num_vars
;
3708 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3710 fprintf (dump_file
, "\nafter normalization:\n");
3711 omega_print_problem (dump_file
, pb
);
3712 fprintf (dump_file
, "\n");
3713 fprintf (dump_file
, "eliminating variable using Fourier-Motzkin.\n");
3717 int parallel_difference
= INT_MAX
;
3718 int best_parallel_eqn
= -1;
3719 int minC
, maxC
, minCj
= 0;
3720 int lower_bound_count
= 0;
3722 bool possible_easy_int_solution
;
3723 int max_splinters
= 1;
3725 bool lucky_exact
= false;
3727 int best
= (INT_MAX
);
3728 int j
= 0, jLe
= 0, jLowerBoundCount
= 0;
3731 eliminate_again
= false;
3733 if (pb
->num_eqs
> 0)
3734 return omega_solve_problem (pb
, desired_res
);
3736 if (!coupled_subscripts
)
3738 if (pb
->safe_vars
== 0)
3741 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3742 if (!omega_safe_var_p (pb
, abs (pb
->geqs
[e
].key
)))
3743 omega_delete_geq (pb
, e
, n_vars
);
3745 pb
->num_vars
= pb
->safe_vars
;
3747 if (desired_res
== omega_simplify
)
3749 omega_problem_reduced (pb
);
3756 if (desired_res
!= omega_simplify
)
3761 if (pb
->num_geqs
== 0)
3763 if (desired_res
== omega_simplify
)
3765 pb
->num_vars
= pb
->safe_vars
;
3766 omega_problem_reduced (pb
);
3772 if (desired_res
== omega_simplify
&& n_vars
== pb
->safe_vars
)
3774 omega_problem_reduced (pb
);
3778 if (pb
->num_geqs
> OMEGA_MAX_GEQS
- 30
3779 || pb
->num_geqs
> 2 * n_vars
* n_vars
+ 4 * n_vars
+ 10)
3781 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3783 "TOO MANY EQUATIONS; "
3784 "%d equations, %d variables, "
3785 "ELIMINATING REDUNDANT ONES\n",
3786 pb
->num_geqs
, n_vars
);
3788 if (!omega_eliminate_redundant (pb
, false))
3791 n_vars
= pb
->num_vars
;
3793 if (pb
->num_eqs
> 0)
3794 return omega_solve_problem (pb
, desired_res
);
3796 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3797 fprintf (dump_file
, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3800 if (desired_res
!= omega_simplify
)
3805 for (i
= n_vars
; i
!= fv
; i
--)
3811 int upper_bound_count
= 0;
3813 lower_bound_count
= 0;
3816 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3817 if (pb
->geqs
[e
].coef
[i
] < 0)
3819 minC
= MIN (minC
, pb
->geqs
[e
].coef
[i
]);
3820 upper_bound_count
++;
3821 if (pb
->geqs
[e
].coef
[i
] < -1)
3829 else if (pb
->geqs
[e
].coef
[i
] > 0)
3831 maxC
= MAX (maxC
, pb
->geqs
[e
].coef
[i
]);
3832 lower_bound_count
++;
3834 if (pb
->geqs
[e
].coef
[i
] > 1)
3843 if (lower_bound_count
== 0
3844 || upper_bound_count
== 0)
3846 lower_bound_count
= 0;
3850 if (ub
>= 0 && lb
>= 0
3851 && pb
->geqs
[lb
].key
== -pb
->geqs
[ub
].key
)
3853 int Lc
= pb
->geqs
[lb
].coef
[i
];
3854 int Uc
= -pb
->geqs
[ub
].coef
[i
];
3856 Lc
* pb
->geqs
[ub
].coef
[0] + Uc
* pb
->geqs
[lb
].coef
[0];
3857 lucky
= (diff
>= (Uc
- 1) * (Lc
- 1));
3863 || in_approximate_mode
)
3865 neweqns
= score
= upper_bound_count
* lower_bound_count
;
3867 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3869 "For %s, exact, score = %d*%d, range = %d ... %d,"
3870 "\nlucky = %d, in_approximate_mode=%d \n",
3871 omega_variable_to_str (pb
, i
),
3873 lower_bound_count
, minC
, maxC
, lucky
,
3874 in_approximate_mode
);
3884 jLowerBoundCount
= lower_bound_count
;
3886 lucky_exact
= lucky
;
3893 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3895 "For %s, non-exact, score = %d*%d,"
3896 "range = %d ... %d \n",
3897 omega_variable_to_str (pb
, i
),
3899 lower_bound_count
, minC
, maxC
);
3901 neweqns
= upper_bound_count
* lower_bound_count
;
3902 score
= maxC
- minC
;
3910 jLowerBoundCount
= lower_bound_count
;
3915 if (lower_bound_count
== 0)
3917 omega_free_eliminations (pb
, pb
->safe_vars
);
3918 n_vars
= pb
->num_vars
;
3919 eliminate_again
= true;
3926 lower_bound_count
= jLowerBoundCount
;
3928 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3929 if (pb
->geqs
[e
].coef
[i
] > 0)
3931 if (pb
->geqs
[e
].coef
[i
] == -minC
)
3932 max_splinters
+= -minC
- 1;
3935 check_pos_mul ((pb
->geqs
[e
].coef
[i
] - 1),
3936 (-minC
- 1)) / (-minC
) + 1;
3940 /* Trying to produce exact elimination by finding redundant
3942 if (!exact
&& !tried_eliminating_redundant
)
3944 omega_eliminate_redundant (pb
, false);
3945 tried_eliminating_redundant
= true;
3946 eliminate_again
= true;
3949 tried_eliminating_redundant
= false;
3952 if (return_single_result
&& desired_res
== omega_simplify
&& !exact
)
3954 omega_problem_reduced (pb
);
3958 /* #ifndef Omega3 */
3959 /* Trying to produce exact elimination by finding redundant
3961 if (!exact
&& !tried_eliminating_redundant
)
3963 omega_eliminate_redundant (pb
, false);
3964 tried_eliminating_redundant
= true;
3967 tried_eliminating_redundant
= false;
3974 for (e1
= pb
->num_geqs
- 1; e1
>= 0; e1
--)
3975 if (pb
->geqs
[e1
].color
== omega_black
)
3976 for (e2
= e1
- 1; e2
>= 0; e2
--)
3977 if (pb
->geqs
[e2
].color
== omega_black
3978 && pb
->geqs
[e1
].key
== -pb
->geqs
[e2
].key
3979 && ((pb
->geqs
[e1
].coef
[0] + pb
->geqs
[e2
].coef
[0])
3980 * (3 - single_var_geq (&pb
->geqs
[e1
], pb
->num_vars
))
3981 / 2 < parallel_difference
))
3983 parallel_difference
=
3984 (pb
->geqs
[e1
].coef
[0] + pb
->geqs
[e2
].coef
[0])
3985 * (3 - single_var_geq (&pb
->geqs
[e1
], pb
->num_vars
))
3987 best_parallel_eqn
= e1
;
3990 if (dump_file
&& (dump_flags
& TDF_DETAILS
)
3991 && best_parallel_eqn
>= 0)
3994 "Possible parallel projection, diff = %d, in ",
3995 parallel_difference
);
3996 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[best_parallel_eqn
]));
3997 fprintf (dump_file
, "\n");
3998 omega_print_problem (dump_file
, pb
);
4002 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4004 fprintf (dump_file
, "going to eliminate %s, (%d,%d,%d)\n",
4005 omega_variable_to_str (pb
, i
), i
, minC
,
4007 omega_print_problem (dump_file
, pb
);
4010 fprintf (dump_file
, "(a lucky exact elimination)\n");
4013 fprintf (dump_file
, "(an exact elimination)\n");
4015 fprintf (dump_file
, "Max # of splinters = %d\n", max_splinters
);
4018 gcc_assert (max_splinters
>= 1);
4020 if (!exact
&& desired_res
== omega_simplify
&& best_parallel_eqn
>= 0
4021 && parallel_difference
<= max_splinters
)
4022 return parallel_splinter (pb
, best_parallel_eqn
, parallel_difference
,
4030 int j
= pb
->num_vars
;
4032 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4034 fprintf (dump_file
, "Swapping %d and %d\n", i
, j
);
4035 omega_print_problem (dump_file
, pb
);
4038 swap (&pb
->var
[i
], &pb
->var
[j
]);
4040 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4041 if (pb
->geqs
[e
].coef
[i
] != pb
->geqs
[e
].coef
[j
])
4043 pb
->geqs
[e
].touched
= 1;
4044 t
= pb
->geqs
[e
].coef
[i
];
4045 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[j
];
4046 pb
->geqs
[e
].coef
[j
] = t
;
4049 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
4050 if (pb
->subs
[e
].coef
[i
] != pb
->subs
[e
].coef
[j
])
4052 t
= pb
->subs
[e
].coef
[i
];
4053 pb
->subs
[e
].coef
[i
] = pb
->subs
[e
].coef
[j
];
4054 pb
->subs
[e
].coef
[j
] = t
;
4057 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4059 fprintf (dump_file
, "Swapping complete \n");
4060 omega_print_problem (dump_file
, pb
);
4061 fprintf (dump_file
, "\n");
4067 else if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4069 fprintf (dump_file
, "No swap needed\n");
4070 omega_print_problem (dump_file
, pb
);
4074 n_vars
= pb
->num_vars
;
4080 int upper_bound
= pos_infinity
;
4081 int lower_bound
= neg_infinity
;
4082 enum omega_eqn_color ub_color
= omega_black
;
4083 enum omega_eqn_color lb_color
= omega_black
;
4084 int topeqn
= pb
->num_geqs
- 1;
4085 int Lc
= pb
->geqs
[Le
].coef
[i
];
4087 for (Le
= topeqn
; Le
>= 0; Le
--)
4088 if ((Lc
= pb
->geqs
[Le
].coef
[i
]) == 0)
4090 if (pb
->geqs
[Le
].coef
[1] == 1)
4092 int constantTerm
= -pb
->geqs
[Le
].coef
[0];
4094 if (constantTerm
> lower_bound
||
4095 (constantTerm
== lower_bound
&&
4096 !omega_eqn_is_red (&pb
->geqs
[Le
], desired_res
)))
4098 lower_bound
= constantTerm
;
4099 lb_color
= pb
->geqs
[Le
].color
;
4102 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4104 if (pb
->geqs
[Le
].color
== omega_black
)
4105 fprintf (dump_file
, " :::=> %s >= %d\n",
4106 omega_variable_to_str (pb
, 1),
4110 " :::=> [%s >= %d]\n",
4111 omega_variable_to_str (pb
, 1),
4117 int constantTerm
= pb
->geqs
[Le
].coef
[0];
4118 if (constantTerm
< upper_bound
||
4119 (constantTerm
== upper_bound
4120 && !omega_eqn_is_red (&pb
->geqs
[Le
],
4123 upper_bound
= constantTerm
;
4124 ub_color
= pb
->geqs
[Le
].color
;
4127 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4129 if (pb
->geqs
[Le
].color
== omega_black
)
4130 fprintf (dump_file
, " :::=> %s <= %d\n",
4131 omega_variable_to_str (pb
, 1),
4135 " :::=> [%s <= %d]\n",
4136 omega_variable_to_str (pb
, 1),
4142 for (Ue
= topeqn
; Ue
>= 0; Ue
--)
4143 if (pb
->geqs
[Ue
].coef
[i
] < 0
4144 && pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4146 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4147 int coefficient
= pb
->geqs
[Ue
].coef
[1] * Lc
4148 + pb
->geqs
[Le
].coef
[1] * Uc
;
4149 int constantTerm
= pb
->geqs
[Ue
].coef
[0] * Lc
4150 + pb
->geqs
[Le
].coef
[0] * Uc
;
4152 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4154 omega_print_geq_extra (dump_file
, pb
,
4156 fprintf (dump_file
, "\n");
4157 omega_print_geq_extra (dump_file
, pb
,
4159 fprintf (dump_file
, "\n");
4162 if (coefficient
> 0)
4164 constantTerm
= -int_div (constantTerm
, coefficient
);
4166 if (constantTerm
> lower_bound
4167 || (constantTerm
== lower_bound
4168 && (desired_res
!= omega_simplify
4169 || (pb
->geqs
[Ue
].color
== omega_black
4170 && pb
->geqs
[Le
].color
== omega_black
))))
4172 lower_bound
= constantTerm
;
4173 lb_color
= (pb
->geqs
[Ue
].color
== omega_red
4174 || pb
->geqs
[Le
].color
== omega_red
)
4175 ? omega_red
: omega_black
;
4178 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4180 if (pb
->geqs
[Ue
].color
== omega_red
4181 || pb
->geqs
[Le
].color
== omega_red
)
4183 " ::=> [%s >= %d]\n",
4184 omega_variable_to_str (pb
, 1),
4189 omega_variable_to_str (pb
, 1),
4195 constantTerm
= int_div (constantTerm
, -coefficient
);
4196 if (constantTerm
< upper_bound
4197 || (constantTerm
== upper_bound
4198 && pb
->geqs
[Ue
].color
== omega_black
4199 && pb
->geqs
[Le
].color
== omega_black
))
4201 upper_bound
= constantTerm
;
4202 ub_color
= (pb
->geqs
[Ue
].color
== omega_red
4203 || pb
->geqs
[Le
].color
== omega_red
)
4204 ? omega_red
: omega_black
;
4208 && (dump_flags
& TDF_DETAILS
))
4210 if (pb
->geqs
[Ue
].color
== omega_red
4211 || pb
->geqs
[Le
].color
== omega_red
)
4213 " ::=> [%s <= %d]\n",
4214 omega_variable_to_str (pb
, 1),
4219 omega_variable_to_str (pb
, 1),
4227 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4229 " therefore, %c%d <= %c%s%c <= %d%c\n",
4230 lb_color
== omega_red
? '[' : ' ', lower_bound
,
4231 (lb_color
== omega_red
&& ub_color
== omega_black
)
4233 omega_variable_to_str (pb
, 1),
4234 (lb_color
== omega_black
&& ub_color
== omega_red
)
4236 upper_bound
, ub_color
== omega_red
? ']' : ' ');
4238 if (lower_bound
> upper_bound
)
4241 if (pb
->safe_vars
== 1)
4243 if (upper_bound
== lower_bound
4244 && !(ub_color
== omega_red
|| lb_color
== omega_red
)
4245 && !please_no_equalities_in_simplified_problems
)
4248 pb
->eqs
[0].coef
[1] = -1;
4249 pb
->eqs
[0].coef
[0] = upper_bound
;
4251 if (ub_color
== omega_red
4252 || lb_color
== omega_red
)
4253 pb
->eqs
[0].color
= omega_red
;
4255 if (desired_res
== omega_simplify
4256 && pb
->eqs
[0].color
== omega_black
)
4257 return omega_solve_problem (pb
, desired_res
);
4260 if (upper_bound
!= pos_infinity
)
4262 pb
->geqs
[0].coef
[1] = -1;
4263 pb
->geqs
[0].coef
[0] = upper_bound
;
4264 pb
->geqs
[0].color
= ub_color
;
4265 pb
->geqs
[0].key
= -1;
4266 pb
->geqs
[0].touched
= 0;
4270 if (lower_bound
!= neg_infinity
)
4272 pb
->geqs
[pb
->num_geqs
].coef
[1] = 1;
4273 pb
->geqs
[pb
->num_geqs
].coef
[0] = -lower_bound
;
4274 pb
->geqs
[pb
->num_geqs
].color
= lb_color
;
4275 pb
->geqs
[pb
->num_geqs
].key
= 1;
4276 pb
->geqs
[pb
->num_geqs
].touched
= 0;
4281 if (desired_res
== omega_simplify
)
4283 omega_problem_reduced (pb
);
4289 && (desired_res
!= omega_simplify
4290 || (lb_color
== omega_black
4291 && ub_color
== omega_black
))
4292 && original_problem
!= no_problem
4293 && lower_bound
== upper_bound
)
4295 for (i
= original_problem
->num_vars
; i
>= 0; i
--)
4296 if (original_problem
->var
[i
] == pb
->var
[1])
4302 e
= original_problem
->num_eqs
++;
4303 omega_init_eqn_zero (&original_problem
->eqs
[e
],
4304 original_problem
->num_vars
);
4305 original_problem
->eqs
[e
].coef
[i
] = -1;
4306 original_problem
->eqs
[e
].coef
[0] = upper_bound
;
4308 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4311 "adding equality %d to outer problem\n", e
);
4312 omega_print_problem (dump_file
, original_problem
);
4319 eliminate_again
= true;
4321 if (lower_bound_count
== 1)
4323 eqn lbeqn
= omega_alloc_eqns (0, 1);
4324 int Lc
= pb
->geqs
[Le
].coef
[i
];
4326 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4327 fprintf (dump_file
, "an inplace elimination\n");
4329 omega_copy_eqn (lbeqn
, &pb
->geqs
[Le
], (n_vars
+ 1));
4330 omega_delete_geq_extra (pb
, Le
, n_vars
+ 1);
4332 for (Ue
= pb
->num_geqs
- 1; Ue
>= 0; Ue
--)
4333 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4335 if (lbeqn
->key
== -pb
->geqs
[Ue
].key
)
4336 omega_delete_geq_extra (pb
, Ue
, n_vars
+ 1);
4340 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4341 pb
->geqs
[Ue
].touched
= 1;
4342 eliminate_again
= false;
4344 if (lbeqn
->color
== omega_red
)
4345 pb
->geqs
[Ue
].color
= omega_red
;
4347 for (k
= 0; k
<= n_vars
; k
++)
4348 pb
->geqs
[Ue
].coef
[k
] =
4349 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4350 check_mul (lbeqn
->coef
[k
], Uc
);
4352 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4354 omega_print_geq (dump_file
, pb
,
4356 fprintf (dump_file
, "\n");
4361 omega_free_eqns (lbeqn
, 1);
4366 int *dead_eqns
= XNEWVEC (int, OMEGA_MAX_GEQS
);
4367 bool *is_dead
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
4369 int top_eqn
= pb
->num_geqs
- 1;
4370 lower_bound_count
--;
4372 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4373 fprintf (dump_file
, "lower bound count = %d\n",
4376 for (Le
= top_eqn
; Le
>= 0; Le
--)
4377 if (pb
->geqs
[Le
].coef
[i
] > 0)
4379 int Lc
= pb
->geqs
[Le
].coef
[i
];
4380 for (Ue
= top_eqn
; Ue
>= 0; Ue
--)
4381 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4383 if (pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4386 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4389 e2
= pb
->num_geqs
++;
4391 e2
= dead_eqns
[--num_dead
];
4393 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4395 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4398 "Le = %d, Ue = %d, gen = %d\n",
4400 omega_print_geq_extra (dump_file
, pb
,
4402 fprintf (dump_file
, "\n");
4403 omega_print_geq_extra (dump_file
, pb
,
4405 fprintf (dump_file
, "\n");
4408 eliminate_again
= false;
4410 for (k
= n_vars
; k
>= 0; k
--)
4411 pb
->geqs
[e2
].coef
[k
] =
4412 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4413 check_mul (pb
->geqs
[Le
].coef
[k
], Uc
);
4415 pb
->geqs
[e2
].coef
[n_vars
+ 1] = 0;
4416 pb
->geqs
[e2
].touched
= 1;
4418 if (pb
->geqs
[Ue
].color
== omega_red
4419 || pb
->geqs
[Le
].color
== omega_red
)
4420 pb
->geqs
[e2
].color
= omega_red
;
4422 pb
->geqs
[e2
].color
= omega_black
;
4424 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4426 omega_print_geq (dump_file
, pb
,
4428 fprintf (dump_file
, "\n");
4432 if (lower_bound_count
== 0)
4434 dead_eqns
[num_dead
++] = Ue
;
4436 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4437 fprintf (dump_file
, "Killed %d\n", Ue
);
4441 lower_bound_count
--;
4442 dead_eqns
[num_dead
++] = Le
;
4444 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4445 fprintf (dump_file
, "Killed %d\n", Le
);
4448 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4451 while (num_dead
> 0)
4452 is_dead
[dead_eqns
[--num_dead
]] = true;
4454 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4456 omega_delete_geq_extra (pb
, e
, n_vars
+ 1);
4467 rS
= omega_alloc_problem (0, 0);
4468 iS
= omega_alloc_problem (0, 0);
4470 possible_easy_int_solution
= true;
4472 for (e
= 0; e
< pb
->num_geqs
; e
++)
4473 if (pb
->geqs
[e
].coef
[i
] == 0)
4475 omega_copy_eqn (&(rS
->geqs
[e2
]), &pb
->geqs
[e
],
4477 omega_copy_eqn (&(iS
->geqs
[e2
]), &pb
->geqs
[e
],
4480 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4483 fprintf (dump_file
, "Copying (%d, %d): ", i
,
4484 pb
->geqs
[e
].coef
[i
]);
4485 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[e
]);
4486 fprintf (dump_file
, "\n");
4487 for (t
= 0; t
<= n_vars
+ 1; t
++)
4488 fprintf (dump_file
, "%d ", pb
->geqs
[e
].coef
[t
]);
4489 fprintf (dump_file
, "\n");
4493 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4496 for (Le
= pb
->num_geqs
- 1; Le
>= 0; Le
--)
4497 if (pb
->geqs
[Le
].coef
[i
] > 0)
4498 for (Ue
= pb
->num_geqs
- 1; Ue
>= 0; Ue
--)
4499 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4502 int Lc
= pb
->geqs
[Le
].coef
[i
];
4503 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4505 if (pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4508 rS
->geqs
[e2
].touched
= iS
->geqs
[e2
].touched
= 1;
4510 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4512 fprintf (dump_file
, "---\n");
4514 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4515 Le
, Lc
, Ue
, Uc
, e2
);
4516 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[Le
]);
4517 fprintf (dump_file
, "\n");
4518 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[Ue
]);
4519 fprintf (dump_file
, "\n");
4524 for (k
= n_vars
; k
>= 0; k
--)
4525 iS
->geqs
[e2
].coef
[k
] = rS
->geqs
[e2
].coef
[k
] =
4526 pb
->geqs
[Ue
].coef
[k
] + pb
->geqs
[Le
].coef
[k
];
4528 iS
->geqs
[e2
].coef
[0] -= (Uc
- 1);
4532 for (k
= n_vars
; k
>= 0; k
--)
4533 iS
->geqs
[e2
].coef
[k
] = rS
->geqs
[e2
].coef
[k
] =
4534 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4535 check_mul (pb
->geqs
[Le
].coef
[k
], Uc
);
4537 iS
->geqs
[e2
].coef
[0] -= (Uc
- 1) * (Lc
- 1);
4540 if (pb
->geqs
[Ue
].color
== omega_red
4541 || pb
->geqs
[Le
].color
== omega_red
)
4542 iS
->geqs
[e2
].color
= rS
->geqs
[e2
].color
= omega_red
;
4544 iS
->geqs
[e2
].color
= rS
->geqs
[e2
].color
= omega_black
;
4546 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4548 omega_print_geq (dump_file
, pb
, &(rS
->geqs
[e2
]));
4549 fprintf (dump_file
, "\n");
4553 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4555 else if (pb
->geqs
[Ue
].coef
[0] * Lc
+
4556 pb
->geqs
[Le
].coef
[0] * Uc
-
4557 (Uc
- 1) * (Lc
- 1) < 0)
4558 possible_easy_int_solution
= false;
4561 iS
->variables_initialized
= rS
->variables_initialized
= true;
4562 iS
->num_vars
= rS
->num_vars
= pb
->num_vars
;
4563 iS
->num_geqs
= rS
->num_geqs
= e2
;
4564 iS
->num_eqs
= rS
->num_eqs
= 0;
4565 iS
->num_subs
= rS
->num_subs
= pb
->num_subs
;
4566 iS
->safe_vars
= rS
->safe_vars
= pb
->safe_vars
;
4568 for (e
= n_vars
; e
>= 0; e
--)
4569 rS
->var
[e
] = pb
->var
[e
];
4571 for (e
= n_vars
; e
>= 0; e
--)
4572 iS
->var
[e
] = pb
->var
[e
];
4574 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
4576 omega_copy_eqn (&(rS
->subs
[e
]), &(pb
->subs
[e
]), pb
->num_vars
);
4577 omega_copy_eqn (&(iS
->subs
[e
]), &(pb
->subs
[e
]), pb
->num_vars
);
4581 n_vars
= pb
->num_vars
;
4583 if (desired_res
!= omega_true
)
4585 if (original_problem
== no_problem
)
4587 original_problem
= pb
;
4588 result
= omega_solve_geq (rS
, omega_false
);
4589 original_problem
= no_problem
;
4592 result
= omega_solve_geq (rS
, omega_false
);
4594 if (result
== omega_false
)
4601 if (pb
->num_eqs
> 0)
4603 /* An equality constraint must have been found */
4606 return omega_solve_problem (pb
, desired_res
);
4610 if (desired_res
!= omega_false
)
4613 int lower_bounds
= 0;
4614 int *lower_bound
= XNEWVEC (int, OMEGA_MAX_GEQS
);
4616 if (possible_easy_int_solution
)
4619 result
= omega_solve_geq (iS
, desired_res
);
4622 if (result
!= omega_false
)
4631 if (!exact
&& best_parallel_eqn
>= 0
4632 && parallel_difference
<= max_splinters
)
4637 return parallel_splinter (pb
, best_parallel_eqn
,
4638 parallel_difference
,
4642 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4643 fprintf (dump_file
, "have to do exact analysis\n");
4647 for (e
= 0; e
< pb
->num_geqs
; e
++)
4648 if (pb
->geqs
[e
].coef
[i
] > 1)
4649 lower_bound
[lower_bounds
++] = e
;
4651 /* Sort array LOWER_BOUND. */
4652 for (j
= 0; j
< lower_bounds
; j
++)
4654 int k
, smallest
= j
;
4656 for (k
= j
+ 1; k
< lower_bounds
; k
++)
4657 if (pb
->geqs
[lower_bound
[smallest
]].coef
[i
] >
4658 pb
->geqs
[lower_bound
[k
]].coef
[i
])
4661 k
= lower_bound
[smallest
];
4662 lower_bound
[smallest
] = lower_bound
[j
];
4666 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4668 fprintf (dump_file
, "lower bound coefficients = ");
4670 for (j
= 0; j
< lower_bounds
; j
++)
4671 fprintf (dump_file
, " %d",
4672 pb
->geqs
[lower_bound
[j
]].coef
[i
]);
4674 fprintf (dump_file
, "\n");
4677 for (j
= 0; j
< lower_bounds
; j
++)
4681 int worst_lower_bound_constant
= -minC
;
4684 max_incr
= (((pb
->geqs
[e
].coef
[i
] - 1) *
4685 (worst_lower_bound_constant
- 1) - 1)
4686 / worst_lower_bound_constant
);
4687 /* max_incr += 2; */
4689 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4691 fprintf (dump_file
, "for equation ");
4692 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
4694 "\ntry decrements from 0 to %d\n",
4696 omega_print_problem (dump_file
, pb
);
4699 if (max_incr
> 50 && !smoothed
4700 && smooth_weird_equations (pb
))
4706 goto solve_geq_start
;
4709 omega_copy_eqn (&pb
->eqs
[0], &pb
->geqs
[e
],
4711 pb
->eqs
[0].color
= omega_black
;
4712 omega_init_eqn_zero (&pb
->geqs
[e
], pb
->num_vars
);
4713 pb
->geqs
[e
].touched
= 1;
4716 for (c
= max_incr
; c
>= 0; c
--)
4718 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4721 "trying next decrement of %d\n",
4723 omega_print_problem (dump_file
, pb
);
4726 omega_copy_problem (rS
, pb
);
4728 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4729 omega_print_problem (dump_file
, rS
);
4731 result
= omega_solve_problem (rS
, desired_res
);
4733 if (result
== omega_true
)
4742 pb
->eqs
[0].coef
[0]--;
4745 if (j
+ 1 < lower_bounds
)
4748 omega_copy_eqn (&pb
->geqs
[e
], &pb
->eqs
[0],
4750 pb
->geqs
[e
].touched
= 1;
4751 pb
->geqs
[e
].color
= omega_black
;
4752 omega_copy_problem (rS
, pb
);
4754 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4756 "exhausted lower bound, "
4757 "checking if still feasible ");
4759 result
= omega_solve_problem (rS
, omega_false
);
4761 if (result
== omega_false
)
4766 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4767 fprintf (dump_file
, "fall-off the end\n");
4779 return omega_unknown
;
4780 } while (eliminate_again
);
4784 /* Because the omega solver is recursive, this counter limits the
4786 static int omega_solve_depth
= 0;
4788 /* Return omega_true when the problem PB has a solution following the
4792 omega_solve_problem (omega_pb pb
, enum omega_result desired_res
)
4794 enum omega_result result
;
4796 gcc_assert (pb
->num_vars
>= pb
->safe_vars
);
4797 omega_solve_depth
++;
4799 if (desired_res
!= omega_simplify
)
4802 if (omega_solve_depth
> 50)
4804 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4807 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4808 omega_solve_depth
, in_approximate_mode
);
4809 omega_print_problem (dump_file
, pb
);
4814 if (omega_solve_eq (pb
, desired_res
) == omega_false
)
4816 omega_solve_depth
--;
4820 if (in_approximate_mode
&& !pb
->num_geqs
)
4822 result
= omega_true
;
4823 pb
->num_vars
= pb
->safe_vars
;
4824 omega_problem_reduced (pb
);
4827 result
= omega_solve_geq (pb
, desired_res
);
4829 omega_solve_depth
--;
4831 if (!omega_reduce_with_subs
)
4833 resurrect_subs (pb
);
4834 gcc_assert (please_no_equalities_in_simplified_problems
4835 || !result
|| pb
->num_subs
== 0);
4841 /* Return true if red equations constrain the set of possible solutions.
4842 We assume that there are solutions to the black equations by
4843 themselves, so if there is no solution to the combined problem, we
4847 omega_problem_has_red_equations (omega_pb pb
)
4853 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4855 fprintf (dump_file
, "Checking for red equations:\n");
4856 omega_print_problem (dump_file
, pb
);
4859 please_no_equalities_in_simplified_problems
++;
4862 if (omega_single_result
)
4863 return_single_result
++;
4865 create_color
= true;
4866 result
= (omega_simplify_problem (pb
) == omega_false
);
4868 if (omega_single_result
)
4869 return_single_result
--;
4872 please_no_equalities_in_simplified_problems
--;
4876 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4877 fprintf (dump_file
, "Gist is FALSE\n");
4882 pb
->eqs
[0].color
= omega_red
;
4884 for (i
= pb
->num_vars
; i
> 0; i
--)
4885 pb
->eqs
[0].coef
[i
] = 0;
4887 pb
->eqs
[0].coef
[0] = 1;
4891 free_red_eliminations (pb
);
4892 gcc_assert (pb
->num_eqs
== 0);
4894 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4895 if (pb
->geqs
[e
].color
== omega_red
)
4901 for (i
= pb
->safe_vars
; i
>= 1; i
--)
4906 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4908 if (pb
->geqs
[e
].coef
[i
])
4910 if (pb
->geqs
[e
].coef
[i
] > 0)
4911 lb
|= (1 + (pb
->geqs
[e
].color
== omega_red
? 1 : 0));
4914 ub
|= (1 + (pb
->geqs
[e
].color
== omega_red
? 1 : 0));
4918 if (ub
== 2 || lb
== 2)
4921 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4922 fprintf (dump_file
, "checks for upper/lower bounds worked!\n");
4924 if (!omega_reduce_with_subs
)
4926 resurrect_subs (pb
);
4927 gcc_assert (pb
->num_subs
== 0);
4935 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4937 "*** Doing potentially expensive elimination tests "
4938 "for red equations\n");
4940 please_no_equalities_in_simplified_problems
++;
4941 omega_eliminate_red (pb
, true);
4942 please_no_equalities_in_simplified_problems
--;
4945 gcc_assert (pb
->num_eqs
== 0);
4947 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4948 if (pb
->geqs
[e
].color
== omega_red
)
4951 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4955 "******************** Redundant Red Equations eliminated!!\n");
4958 "******************** Red Equations remain\n");
4960 omega_print_problem (dump_file
, pb
);
4963 if (!omega_reduce_with_subs
)
4965 normalize_return_type r
;
4967 resurrect_subs (pb
);
4968 r
= normalize_omega_problem (pb
);
4969 gcc_assert (r
!= normalize_false
);
4972 cleanout_wildcards (pb
);
4973 gcc_assert (pb
->num_subs
== 0);
4979 /* Calls omega_simplify_problem in approximate mode. */
4982 omega_simplify_approximate (omega_pb pb
)
4984 enum omega_result result
;
4986 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4987 fprintf (dump_file
, "(Entering approximate mode\n");
4989 in_approximate_mode
= true;
4990 result
= omega_simplify_problem (pb
);
4991 in_approximate_mode
= false;
4993 gcc_assert (pb
->num_vars
== pb
->safe_vars
);
4994 if (!omega_reduce_with_subs
)
4995 gcc_assert (pb
->num_subs
== 0);
4997 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4998 fprintf (dump_file
, "Leaving approximate mode)\n");
5004 /* Simplifies problem PB by eliminating redundant constraints and
5005 reducing the constraints system to a minimal form. Returns
5006 omega_true when the problem was successfully reduced, omega_unknown
5007 when the solver is unable to determine an answer. */
5010 omega_simplify_problem (omega_pb pb
)
5014 omega_found_reduction
= omega_false
;
5016 if (!pb
->variables_initialized
)
5017 omega_initialize_variables (pb
);
5019 if (next_key
* 3 > MAX_KEYS
)
5024 next_key
= OMEGA_MAX_VARS
+ 1;
5026 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5027 pb
->geqs
[e
].touched
= 1;
5029 for (i
= 0; i
< HASH_TABLE_SIZE
; i
++)
5030 hash_master
[i
].touched
= -1;
5032 pb
->hash_version
= hash_version
;
5035 else if (pb
->hash_version
!= hash_version
)
5039 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5040 pb
->geqs
[e
].touched
= 1;
5042 pb
->hash_version
= hash_version
;
5045 if (pb
->num_vars
> pb
->num_eqs
+ 3 * pb
->safe_vars
)
5046 omega_free_eliminations (pb
, pb
->safe_vars
);
5048 if (!may_be_red
&& pb
->num_subs
== 0 && pb
->safe_vars
== 0)
5050 omega_found_reduction
= omega_solve_problem (pb
, omega_unknown
);
5052 if (omega_found_reduction
!= omega_false
5053 && !return_single_result
)
5057 (*omega_when_reduced
) (pb
);
5060 return omega_found_reduction
;
5063 omega_solve_problem (pb
, omega_simplify
);
5065 if (omega_found_reduction
!= omega_false
)
5067 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
5068 pb
->forwarding_address
[pb
->var
[i
]] = i
;
5070 for (i
= 0; i
< pb
->num_subs
; i
++)
5071 pb
->forwarding_address
[pb
->subs
[i
].key
] = -i
- 1;
5074 if (!omega_reduce_with_subs
)
5075 gcc_assert (please_no_equalities_in_simplified_problems
5076 || omega_found_reduction
== omega_false
5077 || pb
->num_subs
== 0);
5079 return omega_found_reduction
;
5082 /* Make variable VAR unprotected: it then can be eliminated. */
5085 omega_unprotect_variable (omega_pb pb
, int var
)
5088 idx
= pb
->forwarding_address
[var
];
5095 if (idx
< pb
->num_subs
)
5097 omega_copy_eqn (&pb
->subs
[idx
], &pb
->subs
[pb
->num_subs
],
5099 pb
->forwarding_address
[pb
->subs
[idx
].key
] = -idx
- 1;
5104 int *bring_to_life
= XNEWVEC (int, OMEGA_MAX_VARS
);
5107 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5108 bring_to_life
[e
] = (pb
->subs
[e
].coef
[idx
] != 0);
5110 for (e2
= pb
->num_subs
- 1; e2
>= 0; e2
--)
5111 if (bring_to_life
[e2
])
5116 if (pb
->safe_vars
< pb
->num_vars
)
5118 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5120 pb
->geqs
[e
].coef
[pb
->num_vars
] =
5121 pb
->geqs
[e
].coef
[pb
->safe_vars
];
5123 pb
->geqs
[e
].coef
[pb
->safe_vars
] = 0;
5126 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5128 pb
->eqs
[e
].coef
[pb
->num_vars
] =
5129 pb
->eqs
[e
].coef
[pb
->safe_vars
];
5131 pb
->eqs
[e
].coef
[pb
->safe_vars
] = 0;
5134 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5136 pb
->subs
[e
].coef
[pb
->num_vars
] =
5137 pb
->subs
[e
].coef
[pb
->safe_vars
];
5139 pb
->subs
[e
].coef
[pb
->safe_vars
] = 0;
5142 pb
->var
[pb
->num_vars
] = pb
->var
[pb
->safe_vars
];
5143 pb
->forwarding_address
[pb
->var
[pb
->num_vars
]] =
5148 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5149 pb
->geqs
[e
].coef
[pb
->safe_vars
] = 0;
5151 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5152 pb
->eqs
[e
].coef
[pb
->safe_vars
] = 0;
5154 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5155 pb
->subs
[e
].coef
[pb
->safe_vars
] = 0;
5158 pb
->var
[pb
->safe_vars
] = pb
->subs
[e2
].key
;
5159 pb
->forwarding_address
[pb
->subs
[e2
].key
] = pb
->safe_vars
;
5161 omega_copy_eqn (&(pb
->eqs
[pb
->num_eqs
]), &(pb
->subs
[e2
]),
5163 pb
->eqs
[pb
->num_eqs
++].coef
[pb
->safe_vars
] = -1;
5164 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5166 if (e2
< pb
->num_subs
- 1)
5167 omega_copy_eqn (&(pb
->subs
[e2
]), &(pb
->subs
[pb
->num_subs
- 1]),
5173 omega_unprotect_1 (pb
, &idx
, NULL
);
5174 free (bring_to_life
);
5177 chain_unprotect (pb
);
5180 /* Unprotects VAR and simplifies PB. */
5183 omega_constrain_variable_sign (omega_pb pb
, enum omega_eqn_color color
,
5186 int n_vars
= pb
->num_vars
;
5188 int k
= pb
->forwarding_address
[var
];
5197 omega_copy_eqn (&pb
->geqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5199 for (j
= 0; j
<= n_vars
; j
++)
5200 pb
->geqs
[e
].coef
[j
] *= sign
;
5202 pb
->geqs
[e
].coef
[0]--;
5203 pb
->geqs
[e
].touched
= 1;
5204 pb
->geqs
[e
].color
= color
;
5209 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5210 omega_copy_eqn (&pb
->eqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5211 pb
->eqs
[e
].color
= color
;
5217 omega_init_eqn_zero (&pb
->geqs
[e
], pb
->num_vars
);
5218 pb
->geqs
[e
].coef
[k
] = sign
;
5219 pb
->geqs
[e
].coef
[0] = -1;
5220 pb
->geqs
[e
].touched
= 1;
5221 pb
->geqs
[e
].color
= color
;
5226 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5227 omega_init_eqn_zero (&pb
->eqs
[e
], pb
->num_vars
);
5228 pb
->eqs
[e
].coef
[k
] = 1;
5229 pb
->eqs
[e
].color
= color
;
5232 omega_unprotect_variable (pb
, var
);
5233 return omega_simplify_problem (pb
);
5236 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5239 omega_constrain_variable_value (omega_pb pb
, enum omega_eqn_color color
,
5243 int k
= pb
->forwarding_address
[var
];
5249 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5250 omega_copy_eqn (&pb
->eqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5251 pb
->eqs
[e
].coef
[0] -= value
;
5256 omega_init_eqn_zero (&pb
->eqs
[e
], pb
->num_vars
);
5257 pb
->eqs
[e
].coef
[k
] = 1;
5258 pb
->eqs
[e
].coef
[0] = -value
;
5261 pb
->eqs
[e
].color
= color
;
5264 /* Return false when the upper and lower bounds are not coupled.
5265 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5269 omega_query_variable (omega_pb pb
, int i
, int *lower_bound
, int *upper_bound
)
5271 int n_vars
= pb
->num_vars
;
5274 bool coupled
= false;
5276 *lower_bound
= neg_infinity
;
5277 *upper_bound
= pos_infinity
;
5278 i
= pb
->forwarding_address
[i
];
5284 for (j
= 1; j
<= n_vars
; j
++)
5285 if (pb
->subs
[i
].coef
[j
] != 0)
5288 *upper_bound
= *lower_bound
= pb
->subs
[i
].coef
[0];
5292 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5293 if (pb
->subs
[e
].coef
[i
] != 0)
5296 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5297 if (pb
->eqs
[e
].coef
[i
] != 0)
5301 for (j
= 1; j
<= n_vars
; j
++)
5302 if (i
!= j
&& pb
->eqs
[e
].coef
[j
] != 0)
5313 *lower_bound
= *upper_bound
=
5314 -pb
->eqs
[e
].coef
[i
] * pb
->eqs
[e
].coef
[0];
5319 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5320 if (pb
->geqs
[e
].coef
[i
] != 0)
5322 if (pb
->geqs
[e
].key
== i
)
5323 *lower_bound
= MAX (*lower_bound
, -pb
->geqs
[e
].coef
[0]);
5325 else if (pb
->geqs
[e
].key
== -i
)
5326 *upper_bound
= MIN (*upper_bound
, pb
->geqs
[e
].coef
[0]);
5335 /* Sets the lower bound L and upper bound U for the values of variable
5336 I, and sets COULD_BE_ZERO to true if variable I might take value
5337 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5341 query_coupled_variable (omega_pb pb
, int i
, int *l
, int *u
,
5342 bool *could_be_zero
, int lower_bound
, int upper_bound
)
5349 /* Preconditions. */
5350 gcc_assert (abs (pb
->forwarding_address
[i
]) == 1
5351 && pb
->num_vars
+ pb
->num_subs
== 2
5352 && pb
->num_eqs
+ pb
->num_subs
== 1);
5354 /* Define variable I in terms of variable V. */
5355 if (pb
->forwarding_address
[i
] == -1)
5364 sign
= -eqn
->coef
[1];
5368 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5369 if (pb
->geqs
[e
].coef
[v
] != 0)
5371 if (pb
->geqs
[e
].coef
[v
] == 1)
5372 lower_bound
= MAX (lower_bound
, -pb
->geqs
[e
].coef
[0]);
5375 upper_bound
= MIN (upper_bound
, pb
->geqs
[e
].coef
[0]);
5378 if (lower_bound
> upper_bound
)
5386 if (lower_bound
== neg_infinity
)
5388 if (eqn
->coef
[v
] > 0)
5389 b1
= sign
* neg_infinity
;
5392 b1
= -sign
* neg_infinity
;
5395 b1
= sign
* (eqn
->coef
[0] + eqn
->coef
[v
] * lower_bound
);
5397 if (upper_bound
== pos_infinity
)
5399 if (eqn
->coef
[v
] > 0)
5400 b2
= sign
* pos_infinity
;
5403 b2
= -sign
* pos_infinity
;
5406 b2
= sign
* (eqn
->coef
[0] + eqn
->coef
[v
] * upper_bound
);
5408 *l
= MAX (*l
, b1
<= b2
? b1
: b2
);
5409 *u
= MIN (*u
, b1
<= b2
? b2
: b1
);
5411 *could_be_zero
= (*l
<= 0 && 0 <= *u
5412 && int_mod (eqn
->coef
[0], abs (eqn
->coef
[v
])) == 0);
5415 /* Return false when a lower bound L and an upper bound U for variable
5416 I in problem PB have been initialized. */
5419 omega_query_variable_bounds (omega_pb pb
, int i
, int *l
, int *u
)
5424 if (!omega_query_variable (pb
, i
, l
, u
)
5425 || (pb
->num_vars
== 1 && pb
->forwarding_address
[i
] == 1))
5428 if (abs (pb
->forwarding_address
[i
]) == 1
5429 && pb
->num_vars
+ pb
->num_subs
== 2
5430 && pb
->num_eqs
+ pb
->num_subs
== 1)
5433 query_coupled_variable (pb
, i
, l
, u
, &could_be_zero
, neg_infinity
,
5441 /* For problem PB, return an integer that represents the classic data
5442 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5443 masks that are added to the result. When DIST_KNOWN is true, DIST
5444 is set to the classic data dependence distance. LOWER_BOUND and
5445 UPPER_BOUND are bounds on the value of variable I, for example, it
5446 is possible to narrow the iteration domain with safe approximations
5447 of loop counts, and thus discard some data dependences that cannot
5451 omega_query_variable_signs (omega_pb pb
, int i
, int dd_lt
,
5452 int dd_eq
, int dd_gt
, int lower_bound
,
5453 int upper_bound
, bool *dist_known
, int *dist
)
5462 omega_query_variable (pb
, i
, &l
, &u
);
5463 query_coupled_variable (pb
, i
, &l
, &u
, &could_be_zero
, lower_bound
,
5482 *dist_known
= false;
5487 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5488 safe variables. Safe variables are not eliminated during the
5489 Fourier-Motzkin elimination. Safe variables are all those
5490 variables that are placed at the beginning of the array of
5491 variables: P->var[0, ..., NPROT - 1]. */
5494 omega_alloc_problem (int nvars
, int nprot
)
5498 gcc_assert (nvars
<= OMEGA_MAX_VARS
);
5499 omega_initialize ();
5501 /* Allocate and initialize PB. */
5502 pb
= XCNEW (struct omega_pb
);
5503 pb
->var
= XCNEWVEC (int, OMEGA_MAX_VARS
+ 2);
5504 pb
->forwarding_address
= XCNEWVEC (int, OMEGA_MAX_VARS
+ 2);
5505 pb
->geqs
= omega_alloc_eqns (0, OMEGA_MAX_GEQS
);
5506 pb
->eqs
= omega_alloc_eqns (0, OMEGA_MAX_EQS
);
5507 pb
->subs
= omega_alloc_eqns (0, OMEGA_MAX_VARS
+ 1);
5509 pb
->hash_version
= hash_version
;
5510 pb
->num_vars
= nvars
;
5511 pb
->safe_vars
= nprot
;
5512 pb
->variables_initialized
= false;
5513 pb
->variables_freed
= false;
5520 /* Keeps the state of the initialization. */
5521 static bool omega_initialized
= false;
5523 /* Initialization of the Omega solver. */
5526 omega_initialize (void)
5530 if (omega_initialized
)
5534 next_key
= OMEGA_MAX_VARS
+ 1;
5535 packing
= XCNEWVEC (int, OMEGA_MAX_VARS
);
5536 fast_lookup
= XCNEWVEC (int, MAX_KEYS
* 2);
5537 fast_lookup_red
= XCNEWVEC (int, MAX_KEYS
* 2);
5538 hash_master
= omega_alloc_eqns (0, HASH_TABLE_SIZE
);
5540 for (i
= 0; i
< HASH_TABLE_SIZE
; i
++)
5541 hash_master
[i
].touched
= -1;
5543 sprintf (wild_name
[0], "1");
5544 sprintf (wild_name
[1], "a");
5545 sprintf (wild_name
[2], "b");
5546 sprintf (wild_name
[3], "c");
5547 sprintf (wild_name
[4], "d");
5548 sprintf (wild_name
[5], "e");
5549 sprintf (wild_name
[6], "f");
5550 sprintf (wild_name
[7], "g");
5551 sprintf (wild_name
[8], "h");
5552 sprintf (wild_name
[9], "i");
5553 sprintf (wild_name
[10], "j");
5554 sprintf (wild_name
[11], "k");
5555 sprintf (wild_name
[12], "l");
5556 sprintf (wild_name
[13], "m");
5557 sprintf (wild_name
[14], "n");
5558 sprintf (wild_name
[15], "o");
5559 sprintf (wild_name
[16], "p");
5560 sprintf (wild_name
[17], "q");
5561 sprintf (wild_name
[18], "r");
5562 sprintf (wild_name
[19], "s");
5563 sprintf (wild_name
[20], "t");
5564 sprintf (wild_name
[40 - 1], "alpha");
5565 sprintf (wild_name
[40 - 2], "beta");
5566 sprintf (wild_name
[40 - 3], "gamma");
5567 sprintf (wild_name
[40 - 4], "delta");
5568 sprintf (wild_name
[40 - 5], "tau");
5569 sprintf (wild_name
[40 - 6], "sigma");
5570 sprintf (wild_name
[40 - 7], "chi");
5571 sprintf (wild_name
[40 - 8], "omega");
5572 sprintf (wild_name
[40 - 9], "pi");
5573 sprintf (wild_name
[40 - 10], "ni");
5574 sprintf (wild_name
[40 - 11], "Alpha");
5575 sprintf (wild_name
[40 - 12], "Beta");
5576 sprintf (wild_name
[40 - 13], "Gamma");
5577 sprintf (wild_name
[40 - 14], "Delta");
5578 sprintf (wild_name
[40 - 15], "Tau");
5579 sprintf (wild_name
[40 - 16], "Sigma");
5580 sprintf (wild_name
[40 - 17], "Chi");
5581 sprintf (wild_name
[40 - 18], "Omega");
5582 sprintf (wild_name
[40 - 19], "xxx");
5584 omega_initialized
= true;