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 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 eqn
->color
|= sub
->color
;
3052 for (j
= n_vars
; j
>= 0; j
--)
3053 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3056 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3057 if (pb
->geqs
[e
].coef
[i
])
3059 eqn eqn
= &(pb
->geqs
[e
]);
3062 if (sub
->color
== omega_red
)
3063 eqn
->color
= omega_red
;
3065 for (j
= n_vars
; j
>= 0; j
--)
3072 for (j
= n_vars
; j
>= 0; j
--)
3073 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3077 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
3078 if (pb
->subs
[e
].coef
[i
])
3080 eqn eqn
= &(pb
->subs
[e
]);
3083 gcc_assert (sub
->color
== omega_black
);
3084 for (j
= n_vars
; j
>= 0; j
--)
3088 for (j
= n_vars
; j
>= 0; j
--)
3089 eqn
->coef
[j
] -= sub
->coef
[j
] * k
/ c
;
3092 if (in_approximate_mode
)
3093 omega_delete_variable (pb
, i
);
3095 omega_convert_eq_to_geqs (pb
, e2
);
3098 omega_free_eqns (sub
, 1);
3101 /* Helper function for printing "sorry, no solution". */
3103 static inline enum omega_result
3104 omega_problem_has_no_solution (void)
3106 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3107 fprintf (dump_file
, "\nequations have no solution \n");
3112 /* Helper function: solve equations in PB one at a time, following the
3113 DESIRED_RES result. */
3115 static enum omega_result
3116 omega_solve_eq (omega_pb pb
, enum omega_result desired_res
)
3123 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && pb
->num_eqs
> 0)
3125 fprintf (dump_file
, "\nomega_solve_eq (%d, %d)\n",
3126 desired_res
, may_be_red
);
3127 omega_print_problem (dump_file
, pb
);
3128 fprintf (dump_file
, "\n");
3134 j
= pb
->num_eqs
- 1;
3140 while (i
<= j
&& pb
->eqs
[i
].color
== omega_red
)
3143 while (i
<= j
&& pb
->eqs
[j
].color
== omega_black
)
3149 eq
= omega_alloc_eqns (0, 1);
3150 omega_copy_eqn (eq
, &pb
->eqs
[i
], pb
->num_vars
);
3151 omega_copy_eqn (&pb
->eqs
[i
], &pb
->eqs
[j
], pb
->num_vars
);
3152 omega_copy_eqn (&pb
->eqs
[j
], eq
, pb
->num_vars
);
3153 omega_free_eqns (eq
, 1);
3159 /* Eliminate all EQ equations */
3160 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
3162 eqn eqn
= &(pb
->eqs
[e
]);
3165 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3166 fprintf (dump_file
, "----\n");
3168 for (i
= pb
->num_vars
; i
> 0; i
--)
3174 for (j
= i
- 1; j
> 0; j
--)
3178 /* i is the position of last nonzero coefficient,
3179 g is the coefficient of i,
3180 j is the position of next nonzero coefficient. */
3184 if (eqn
->coef
[0] % g
!= 0)
3185 return omega_problem_has_no_solution ();
3187 eqn
->coef
[0] = eqn
->coef
[0] / g
;
3190 omega_do_elimination (pb
, e
, i
);
3196 if (eqn
->coef
[0] != 0)
3197 return omega_problem_has_no_solution ();
3209 omega_do_elimination (pb
, e
, i
);
3215 bool promotion_possible
=
3216 (omega_safe_var_p (pb
, j
)
3217 && pb
->safe_vars
+ 1 == i
3218 && !omega_eqn_is_red (eqn
, desired_res
)
3219 && !in_approximate_mode
);
3221 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && promotion_possible
)
3222 fprintf (dump_file
, " Promotion possible\n");
3225 if (!omega_safe_var_p (pb
, j
))
3227 for (; g
!= 1 && !omega_safe_var_p (pb
, j
); j
--)
3228 g
= gcd (abs (eqn
->coef
[j
]), g
);
3231 else if (!omega_safe_var_p (pb
, i
))
3236 for (; g
!= 1 && j
> 0; j
--)
3237 g
= gcd (abs (eqn
->coef
[j
]), g
);
3241 if (eqn
->coef
[0] % g
!= 0)
3242 return omega_problem_has_no_solution ();
3244 for (j
= 0; j
<= pb
->num_vars
; j
++)
3254 for (e2
= e
- 1; e2
>= 0; e2
--)
3255 if (pb
->eqs
[e2
].coef
[i
])
3259 for (e2
= pb
->num_geqs
- 1; e2
>= 0; e2
--)
3260 if (pb
->geqs
[e2
].coef
[i
])
3264 for (e2
= pb
->num_subs
- 1; e2
>= 0; e2
--)
3265 if (pb
->subs
[e2
].coef
[i
])
3270 bool change
= false;
3272 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3274 fprintf (dump_file
, "Ha! We own it! \n");
3275 omega_print_eq (dump_file
, pb
, eqn
);
3276 fprintf (dump_file
, " \n");
3282 for (j
= i
- 1; j
>= 0; j
--)
3284 int t
= int_mod (eqn
->coef
[j
], g
);
3289 if (t
!= eqn
->coef
[j
])
3298 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3299 fprintf (dump_file
, "So what?\n");
3304 omega_name_wild_card (pb
, i
);
3306 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3308 omega_print_eq (dump_file
, pb
, eqn
);
3309 fprintf (dump_file
, " \n");
3318 if (promotion_possible
)
3320 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3322 fprintf (dump_file
, "promoting %s to safety\n",
3323 omega_variable_to_str (pb
, i
));
3324 omega_print_vars (dump_file
, pb
);
3329 if (!omega_wildcard_p (pb
, i
))
3330 omega_name_wild_card (pb
, i
);
3332 promotion_possible
= false;
3337 if (g2
> 1 && !in_approximate_mode
)
3339 if (pb
->eqs
[e
].color
== omega_red
)
3341 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3342 fprintf (dump_file
, "handling red equality\n");
3345 omega_do_elimination (pb
, e
, i
);
3349 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3352 "adding equation to handle safe variable \n");
3353 omega_print_eq (dump_file
, pb
, eqn
);
3354 fprintf (dump_file
, "\n----\n");
3355 omega_print_problem (dump_file
, pb
);
3356 fprintf (dump_file
, "\n----\n");
3357 fprintf (dump_file
, "\n----\n");
3360 i
= omega_add_new_wild_card (pb
);
3362 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
3363 omega_init_eqn_zero (&pb
->eqs
[e
+ 1], pb
->num_vars
);
3364 omega_copy_eqn (&pb
->eqs
[e
+ 1], eqn
, pb
->safe_vars
);
3366 for (j
= pb
->num_vars
; j
>= 0; j
--)
3368 pb
->eqs
[e
+ 1].coef
[j
] = int_mod (pb
->eqs
[e
+ 1].coef
[j
], g2
);
3370 if (2 * pb
->eqs
[e
+ 1].coef
[j
] >= g2
)
3371 pb
->eqs
[e
+ 1].coef
[j
] -= g2
;
3374 pb
->eqs
[e
+ 1].coef
[i
] = g2
;
3377 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3378 omega_print_problem (dump_file
, pb
);
3387 /* Find variable to eliminate. */
3390 gcc_assert (in_approximate_mode
);
3392 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3394 fprintf (dump_file
, "non-exact elimination: ");
3395 omega_print_eq (dump_file
, pb
, eqn
);
3396 fprintf (dump_file
, "\n");
3397 omega_print_problem (dump_file
, pb
);
3400 for (i
= pb
->num_vars
; i
> sv
; i
--)
3401 if (pb
->eqs
[e
].coef
[i
] != 0)
3405 for (i
= pb
->num_vars
; i
> sv
; i
--)
3406 if (pb
->eqs
[e
].coef
[i
] == 1 || pb
->eqs
[e
].coef
[i
] == -1)
3412 omega_do_elimination (pb
, e
, i
);
3414 if (dump_file
&& (dump_flags
& TDF_DETAILS
) && g2
> 1)
3416 fprintf (dump_file
, "result of non-exact elimination:\n");
3417 omega_print_problem (dump_file
, pb
);
3422 int factor
= (INT_MAX
);
3425 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3426 fprintf (dump_file
, "doing moding\n");
3428 for (i
= pb
->num_vars
; i
!= sv
; i
--)
3429 if ((pb
->eqs
[e
].coef
[i
] & 1) != 0)
3434 for (; i
!= sv
; i
--)
3435 if ((pb
->eqs
[e
].coef
[i
] & 1) != 0)
3441 if (j
!= 0 && i
== sv
)
3443 omega_do_mod (pb
, 2, e
, j
);
3449 for (i
= pb
->num_vars
; i
!= sv
; i
--)
3450 if (pb
->eqs
[e
].coef
[i
] != 0
3451 && factor
> abs (pb
->eqs
[e
].coef
[i
]) + 1)
3453 factor
= abs (pb
->eqs
[e
].coef
[i
]) + 1;
3459 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3460 fprintf (dump_file
, "should not have happened\n");
3464 omega_do_mod (pb
, factor
, e
, j
);
3465 /* Go back and try this equation again. */
3472 return omega_unknown
;
3475 /* Transform an inequation E to an equality, then solve DIFF problems
3476 based on PB, and only differing by the constant part that is
3477 diminished by one, trying to figure out which of the constants
3480 static enum omega_result
3481 parallel_splinter (omega_pb pb
, int e
, int diff
,
3482 enum omega_result desired_res
)
3484 omega_pb tmp_problem
;
3487 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3489 fprintf (dump_file
, "Using parallel splintering\n");
3490 omega_print_problem (dump_file
, pb
);
3493 tmp_problem
= XNEW (struct omega_pb
);
3494 omega_copy_eqn (&pb
->eqs
[0], &pb
->geqs
[e
], pb
->num_vars
);
3497 for (i
= 0; i
<= diff
; i
++)
3499 omega_copy_problem (tmp_problem
, pb
);
3501 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3503 fprintf (dump_file
, "Splinter # %i\n", i
);
3504 omega_print_problem (dump_file
, pb
);
3507 if (omega_solve_problem (tmp_problem
, desired_res
) == omega_true
)
3513 pb
->eqs
[0].coef
[0]--;
3520 /* Helper function: solve equations one at a time. */
3522 static enum omega_result
3523 omega_solve_geq (omega_pb pb
, enum omega_result desired_res
)
3527 enum omega_result result
;
3528 bool coupled_subscripts
= false;
3529 bool smoothed
= false;
3530 bool eliminate_again
;
3531 bool tried_eliminating_redundant
= false;
3533 if (desired_res
!= omega_simplify
)
3541 gcc_assert (desired_res
== omega_simplify
|| pb
->num_subs
== 0);
3543 /* Verify that there are not too many inequalities. */
3544 gcc_assert (pb
->num_geqs
<= OMEGA_MAX_GEQS
);
3546 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3548 fprintf (dump_file
, "\nomega_solve_geq (%d,%d):\n",
3549 desired_res
, please_no_equalities_in_simplified_problems
);
3550 omega_print_problem (dump_file
, pb
);
3551 fprintf (dump_file
, "\n");
3554 n_vars
= pb
->num_vars
;
3558 enum omega_eqn_color u_color
= omega_black
;
3559 enum omega_eqn_color l_color
= omega_black
;
3560 int upper_bound
= pos_infinity
;
3561 int lower_bound
= neg_infinity
;
3563 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3565 int a
= pb
->geqs
[e
].coef
[1];
3566 int c
= pb
->geqs
[e
].coef
[0];
3568 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3572 return omega_problem_has_no_solution ();
3579 if (lower_bound
< -c
3580 || (lower_bound
== -c
3581 && !omega_eqn_is_red (&pb
->geqs
[e
], desired_res
)))
3584 l_color
= pb
->geqs
[e
].color
;
3590 c
= int_div (c
, -a
);
3593 || (upper_bound
== c
3594 && !omega_eqn_is_red (&pb
->geqs
[e
], desired_res
)))
3597 u_color
= pb
->geqs
[e
].color
;
3602 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3604 fprintf (dump_file
, "upper bound = %d\n", upper_bound
);
3605 fprintf (dump_file
, "lower bound = %d\n", lower_bound
);
3608 if (lower_bound
> upper_bound
)
3609 return omega_problem_has_no_solution ();
3611 if (desired_res
== omega_simplify
)
3614 if (pb
->safe_vars
== 1)
3617 if (lower_bound
== upper_bound
3618 && u_color
== omega_black
3619 && l_color
== omega_black
)
3621 pb
->eqs
[0].coef
[0] = -lower_bound
;
3622 pb
->eqs
[0].coef
[1] = 1;
3623 pb
->eqs
[0].color
= omega_black
;
3625 return omega_solve_problem (pb
, desired_res
);
3629 if (lower_bound
> neg_infinity
)
3631 pb
->geqs
[0].coef
[0] = -lower_bound
;
3632 pb
->geqs
[0].coef
[1] = 1;
3633 pb
->geqs
[0].key
= 1;
3634 pb
->geqs
[0].color
= l_color
;
3635 pb
->geqs
[0].touched
= 0;
3639 if (upper_bound
< pos_infinity
)
3641 pb
->geqs
[pb
->num_geqs
].coef
[0] = upper_bound
;
3642 pb
->geqs
[pb
->num_geqs
].coef
[1] = -1;
3643 pb
->geqs
[pb
->num_geqs
].key
= -1;
3644 pb
->geqs
[pb
->num_geqs
].color
= u_color
;
3645 pb
->geqs
[pb
->num_geqs
].touched
= 0;
3653 omega_problem_reduced (pb
);
3657 if (original_problem
!= no_problem
3658 && l_color
== omega_black
3659 && u_color
== omega_black
3661 && lower_bound
== upper_bound
)
3663 pb
->eqs
[0].coef
[0] = -lower_bound
;
3664 pb
->eqs
[0].coef
[1] = 1;
3666 adding_equality_constraint (pb
, 0);
3672 if (!pb
->variables_freed
)
3674 pb
->variables_freed
= true;
3676 if (desired_res
!= omega_simplify
)
3677 omega_free_eliminations (pb
, 0);
3679 omega_free_eliminations (pb
, pb
->safe_vars
);
3681 n_vars
= pb
->num_vars
;
3687 switch (normalize_omega_problem (pb
))
3689 case normalize_false
:
3693 case normalize_coupled
:
3694 coupled_subscripts
= true;
3697 case normalize_uncoupled
:
3698 coupled_subscripts
= false;
3705 n_vars
= pb
->num_vars
;
3707 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3709 fprintf (dump_file
, "\nafter normalization:\n");
3710 omega_print_problem (dump_file
, pb
);
3711 fprintf (dump_file
, "\n");
3712 fprintf (dump_file
, "eliminating variable using Fourier-Motzkin.\n");
3716 int parallel_difference
= INT_MAX
;
3717 int best_parallel_eqn
= -1;
3718 int minC
, maxC
, minCj
= 0;
3719 int lower_bound_count
= 0;
3721 bool possible_easy_int_solution
;
3722 int max_splinters
= 1;
3724 bool lucky_exact
= false;
3726 int best
= (INT_MAX
);
3727 int j
= 0, jLe
= 0, jLowerBoundCount
= 0;
3730 eliminate_again
= false;
3732 if (pb
->num_eqs
> 0)
3733 return omega_solve_problem (pb
, desired_res
);
3735 if (!coupled_subscripts
)
3737 if (pb
->safe_vars
== 0)
3740 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3741 if (!omega_safe_var_p (pb
, abs (pb
->geqs
[e
].key
)))
3742 omega_delete_geq (pb
, e
, n_vars
);
3744 pb
->num_vars
= pb
->safe_vars
;
3746 if (desired_res
== omega_simplify
)
3748 omega_problem_reduced (pb
);
3755 if (desired_res
!= omega_simplify
)
3760 if (pb
->num_geqs
== 0)
3762 if (desired_res
== omega_simplify
)
3764 pb
->num_vars
= pb
->safe_vars
;
3765 omega_problem_reduced (pb
);
3771 if (desired_res
== omega_simplify
&& n_vars
== pb
->safe_vars
)
3773 omega_problem_reduced (pb
);
3777 if (pb
->num_geqs
> OMEGA_MAX_GEQS
- 30
3778 || pb
->num_geqs
> 2 * n_vars
* n_vars
+ 4 * n_vars
+ 10)
3780 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3782 "TOO MANY EQUATIONS; "
3783 "%d equations, %d variables, "
3784 "ELIMINATING REDUNDANT ONES\n",
3785 pb
->num_geqs
, n_vars
);
3787 if (!omega_eliminate_redundant (pb
, false))
3790 n_vars
= pb
->num_vars
;
3792 if (pb
->num_eqs
> 0)
3793 return omega_solve_problem (pb
, desired_res
);
3795 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3796 fprintf (dump_file
, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3799 if (desired_res
!= omega_simplify
)
3804 for (i
= n_vars
; i
!= fv
; i
--)
3810 int upper_bound_count
= 0;
3812 lower_bound_count
= 0;
3815 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3816 if (pb
->geqs
[e
].coef
[i
] < 0)
3818 minC
= MIN (minC
, pb
->geqs
[e
].coef
[i
]);
3819 upper_bound_count
++;
3820 if (pb
->geqs
[e
].coef
[i
] < -1)
3828 else if (pb
->geqs
[e
].coef
[i
] > 0)
3830 maxC
= MAX (maxC
, pb
->geqs
[e
].coef
[i
]);
3831 lower_bound_count
++;
3833 if (pb
->geqs
[e
].coef
[i
] > 1)
3842 if (lower_bound_count
== 0
3843 || upper_bound_count
== 0)
3845 lower_bound_count
= 0;
3849 if (ub
>= 0 && lb
>= 0
3850 && pb
->geqs
[lb
].key
== -pb
->geqs
[ub
].key
)
3852 int Lc
= pb
->geqs
[lb
].coef
[i
];
3853 int Uc
= -pb
->geqs
[ub
].coef
[i
];
3855 Lc
* pb
->geqs
[ub
].coef
[0] + Uc
* pb
->geqs
[lb
].coef
[0];
3856 lucky
= (diff
>= (Uc
- 1) * (Lc
- 1));
3862 || in_approximate_mode
)
3864 neweqns
= score
= upper_bound_count
* lower_bound_count
;
3866 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3868 "For %s, exact, score = %d*%d, range = %d ... %d,"
3869 "\nlucky = %d, in_approximate_mode=%d \n",
3870 omega_variable_to_str (pb
, i
),
3872 lower_bound_count
, minC
, maxC
, lucky
,
3873 in_approximate_mode
);
3883 jLowerBoundCount
= lower_bound_count
;
3885 lucky_exact
= lucky
;
3892 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
3894 "For %s, non-exact, score = %d*%d,"
3895 "range = %d ... %d \n",
3896 omega_variable_to_str (pb
, i
),
3898 lower_bound_count
, minC
, maxC
);
3900 neweqns
= upper_bound_count
* lower_bound_count
;
3901 score
= maxC
- minC
;
3909 jLowerBoundCount
= lower_bound_count
;
3914 if (lower_bound_count
== 0)
3916 omega_free_eliminations (pb
, pb
->safe_vars
);
3917 n_vars
= pb
->num_vars
;
3918 eliminate_again
= true;
3925 lower_bound_count
= jLowerBoundCount
;
3927 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
3928 if (pb
->geqs
[e
].coef
[i
] > 0)
3930 if (pb
->geqs
[e
].coef
[i
] == -minC
)
3931 max_splinters
+= -minC
- 1;
3934 check_pos_mul ((pb
->geqs
[e
].coef
[i
] - 1),
3935 (-minC
- 1)) / (-minC
) + 1;
3939 /* Trying to produce exact elimination by finding redundant
3941 if (!exact
&& !tried_eliminating_redundant
)
3943 omega_eliminate_redundant (pb
, false);
3944 tried_eliminating_redundant
= true;
3945 eliminate_again
= true;
3948 tried_eliminating_redundant
= false;
3951 if (return_single_result
&& desired_res
== omega_simplify
&& !exact
)
3953 omega_problem_reduced (pb
);
3957 /* #ifndef Omega3 */
3958 /* Trying to produce exact elimination by finding redundant
3960 if (!exact
&& !tried_eliminating_redundant
)
3962 omega_eliminate_redundant (pb
, false);
3963 tried_eliminating_redundant
= true;
3966 tried_eliminating_redundant
= false;
3973 for (e1
= pb
->num_geqs
- 1; e1
>= 0; e1
--)
3974 if (pb
->geqs
[e1
].color
== omega_black
)
3975 for (e2
= e1
- 1; e2
>= 0; e2
--)
3976 if (pb
->geqs
[e2
].color
== omega_black
3977 && pb
->geqs
[e1
].key
== -pb
->geqs
[e2
].key
3978 && ((pb
->geqs
[e1
].coef
[0] + pb
->geqs
[e2
].coef
[0])
3979 * (3 - single_var_geq (&pb
->geqs
[e1
], pb
->num_vars
))
3980 / 2 < parallel_difference
))
3982 parallel_difference
=
3983 (pb
->geqs
[e1
].coef
[0] + pb
->geqs
[e2
].coef
[0])
3984 * (3 - single_var_geq (&pb
->geqs
[e1
], pb
->num_vars
))
3986 best_parallel_eqn
= e1
;
3989 if (dump_file
&& (dump_flags
& TDF_DETAILS
)
3990 && best_parallel_eqn
>= 0)
3993 "Possible parallel projection, diff = %d, in ",
3994 parallel_difference
);
3995 omega_print_geq (dump_file
, pb
, &(pb
->geqs
[best_parallel_eqn
]));
3996 fprintf (dump_file
, "\n");
3997 omega_print_problem (dump_file
, pb
);
4001 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4003 fprintf (dump_file
, "going to eliminate %s, (%d,%d,%d)\n",
4004 omega_variable_to_str (pb
, i
), i
, minC
,
4006 omega_print_problem (dump_file
, pb
);
4009 fprintf (dump_file
, "(a lucky exact elimination)\n");
4012 fprintf (dump_file
, "(an exact elimination)\n");
4014 fprintf (dump_file
, "Max # of splinters = %d\n", max_splinters
);
4017 gcc_assert (max_splinters
>= 1);
4019 if (!exact
&& desired_res
== omega_simplify
&& best_parallel_eqn
>= 0
4020 && parallel_difference
<= max_splinters
)
4021 return parallel_splinter (pb
, best_parallel_eqn
, parallel_difference
,
4029 int j
= pb
->num_vars
;
4031 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4033 fprintf (dump_file
, "Swapping %d and %d\n", i
, j
);
4034 omega_print_problem (dump_file
, pb
);
4037 swap (&pb
->var
[i
], &pb
->var
[j
]);
4039 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4040 if (pb
->geqs
[e
].coef
[i
] != pb
->geqs
[e
].coef
[j
])
4042 pb
->geqs
[e
].touched
= 1;
4043 t
= pb
->geqs
[e
].coef
[i
];
4044 pb
->geqs
[e
].coef
[i
] = pb
->geqs
[e
].coef
[j
];
4045 pb
->geqs
[e
].coef
[j
] = t
;
4048 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
4049 if (pb
->subs
[e
].coef
[i
] != pb
->subs
[e
].coef
[j
])
4051 t
= pb
->subs
[e
].coef
[i
];
4052 pb
->subs
[e
].coef
[i
] = pb
->subs
[e
].coef
[j
];
4053 pb
->subs
[e
].coef
[j
] = t
;
4056 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4058 fprintf (dump_file
, "Swapping complete \n");
4059 omega_print_problem (dump_file
, pb
);
4060 fprintf (dump_file
, "\n");
4066 else if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4068 fprintf (dump_file
, "No swap needed\n");
4069 omega_print_problem (dump_file
, pb
);
4073 n_vars
= pb
->num_vars
;
4079 int upper_bound
= pos_infinity
;
4080 int lower_bound
= neg_infinity
;
4081 enum omega_eqn_color ub_color
= omega_black
;
4082 enum omega_eqn_color lb_color
= omega_black
;
4083 int topeqn
= pb
->num_geqs
- 1;
4084 int Lc
= pb
->geqs
[Le
].coef
[i
];
4086 for (Le
= topeqn
; Le
>= 0; Le
--)
4087 if ((Lc
= pb
->geqs
[Le
].coef
[i
]) == 0)
4089 if (pb
->geqs
[Le
].coef
[1] == 1)
4091 int constantTerm
= -pb
->geqs
[Le
].coef
[0];
4093 if (constantTerm
> lower_bound
||
4094 (constantTerm
== lower_bound
&&
4095 !omega_eqn_is_red (&pb
->geqs
[Le
], desired_res
)))
4097 lower_bound
= constantTerm
;
4098 lb_color
= pb
->geqs
[Le
].color
;
4101 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4103 if (pb
->geqs
[Le
].color
== omega_black
)
4104 fprintf (dump_file
, " :::=> %s >= %d\n",
4105 omega_variable_to_str (pb
, 1),
4109 " :::=> [%s >= %d]\n",
4110 omega_variable_to_str (pb
, 1),
4116 int constantTerm
= pb
->geqs
[Le
].coef
[0];
4117 if (constantTerm
< upper_bound
||
4118 (constantTerm
== upper_bound
4119 && !omega_eqn_is_red (&pb
->geqs
[Le
],
4122 upper_bound
= constantTerm
;
4123 ub_color
= pb
->geqs
[Le
].color
;
4126 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4128 if (pb
->geqs
[Le
].color
== omega_black
)
4129 fprintf (dump_file
, " :::=> %s <= %d\n",
4130 omega_variable_to_str (pb
, 1),
4134 " :::=> [%s <= %d]\n",
4135 omega_variable_to_str (pb
, 1),
4141 for (Ue
= topeqn
; Ue
>= 0; Ue
--)
4142 if (pb
->geqs
[Ue
].coef
[i
] < 0
4143 && pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4145 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4146 int coefficient
= pb
->geqs
[Ue
].coef
[1] * Lc
4147 + pb
->geqs
[Le
].coef
[1] * Uc
;
4148 int constantTerm
= pb
->geqs
[Ue
].coef
[0] * Lc
4149 + pb
->geqs
[Le
].coef
[0] * Uc
;
4151 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4153 omega_print_geq_extra (dump_file
, pb
,
4155 fprintf (dump_file
, "\n");
4156 omega_print_geq_extra (dump_file
, pb
,
4158 fprintf (dump_file
, "\n");
4161 if (coefficient
> 0)
4163 constantTerm
= -int_div (constantTerm
, coefficient
);
4165 if (constantTerm
> lower_bound
4166 || (constantTerm
== lower_bound
4167 && (desired_res
!= omega_simplify
4168 || (pb
->geqs
[Ue
].color
== omega_black
4169 && pb
->geqs
[Le
].color
== omega_black
))))
4171 lower_bound
= constantTerm
;
4172 lb_color
= (pb
->geqs
[Ue
].color
== omega_red
4173 || pb
->geqs
[Le
].color
== omega_red
)
4174 ? omega_red
: omega_black
;
4177 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4179 if (pb
->geqs
[Ue
].color
== omega_red
4180 || pb
->geqs
[Le
].color
== omega_red
)
4182 " ::=> [%s >= %d]\n",
4183 omega_variable_to_str (pb
, 1),
4188 omega_variable_to_str (pb
, 1),
4194 constantTerm
= int_div (constantTerm
, -coefficient
);
4195 if (constantTerm
< upper_bound
4196 || (constantTerm
== upper_bound
4197 && pb
->geqs
[Ue
].color
== omega_black
4198 && pb
->geqs
[Le
].color
== omega_black
))
4200 upper_bound
= constantTerm
;
4201 ub_color
= (pb
->geqs
[Ue
].color
== omega_red
4202 || pb
->geqs
[Le
].color
== omega_red
)
4203 ? omega_red
: omega_black
;
4207 && (dump_flags
& TDF_DETAILS
))
4209 if (pb
->geqs
[Ue
].color
== omega_red
4210 || pb
->geqs
[Le
].color
== omega_red
)
4212 " ::=> [%s <= %d]\n",
4213 omega_variable_to_str (pb
, 1),
4218 omega_variable_to_str (pb
, 1),
4226 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4228 " therefore, %c%d <= %c%s%c <= %d%c\n",
4229 lb_color
== omega_red
? '[' : ' ', lower_bound
,
4230 (lb_color
== omega_red
&& ub_color
== omega_black
)
4232 omega_variable_to_str (pb
, 1),
4233 (lb_color
== omega_black
&& ub_color
== omega_red
)
4235 upper_bound
, ub_color
== omega_red
? ']' : ' ');
4237 if (lower_bound
> upper_bound
)
4240 if (pb
->safe_vars
== 1)
4242 if (upper_bound
== lower_bound
4243 && !(ub_color
== omega_red
|| lb_color
== omega_red
)
4244 && !please_no_equalities_in_simplified_problems
)
4247 pb
->eqs
[0].coef
[1] = -1;
4248 pb
->eqs
[0].coef
[0] = upper_bound
;
4250 if (ub_color
== omega_red
4251 || lb_color
== omega_red
)
4252 pb
->eqs
[0].color
= omega_red
;
4254 if (desired_res
== omega_simplify
4255 && pb
->eqs
[0].color
== omega_black
)
4256 return omega_solve_problem (pb
, desired_res
);
4259 if (upper_bound
!= pos_infinity
)
4261 pb
->geqs
[0].coef
[1] = -1;
4262 pb
->geqs
[0].coef
[0] = upper_bound
;
4263 pb
->geqs
[0].color
= ub_color
;
4264 pb
->geqs
[0].key
= -1;
4265 pb
->geqs
[0].touched
= 0;
4269 if (lower_bound
!= neg_infinity
)
4271 pb
->geqs
[pb
->num_geqs
].coef
[1] = 1;
4272 pb
->geqs
[pb
->num_geqs
].coef
[0] = -lower_bound
;
4273 pb
->geqs
[pb
->num_geqs
].color
= lb_color
;
4274 pb
->geqs
[pb
->num_geqs
].key
= 1;
4275 pb
->geqs
[pb
->num_geqs
].touched
= 0;
4280 if (desired_res
== omega_simplify
)
4282 omega_problem_reduced (pb
);
4288 && (desired_res
!= omega_simplify
4289 || (lb_color
== omega_black
4290 && ub_color
== omega_black
))
4291 && original_problem
!= no_problem
4292 && lower_bound
== upper_bound
)
4294 for (i
= original_problem
->num_vars
; i
>= 0; i
--)
4295 if (original_problem
->var
[i
] == pb
->var
[1])
4301 e
= original_problem
->num_eqs
++;
4302 omega_init_eqn_zero (&original_problem
->eqs
[e
],
4303 original_problem
->num_vars
);
4304 original_problem
->eqs
[e
].coef
[i
] = -1;
4305 original_problem
->eqs
[e
].coef
[0] = upper_bound
;
4307 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4310 "adding equality %d to outer problem\n", e
);
4311 omega_print_problem (dump_file
, original_problem
);
4318 eliminate_again
= true;
4320 if (lower_bound_count
== 1)
4322 eqn lbeqn
= omega_alloc_eqns (0, 1);
4323 int Lc
= pb
->geqs
[Le
].coef
[i
];
4325 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4326 fprintf (dump_file
, "an inplace elimination\n");
4328 omega_copy_eqn (lbeqn
, &pb
->geqs
[Le
], (n_vars
+ 1));
4329 omega_delete_geq_extra (pb
, Le
, n_vars
+ 1);
4331 for (Ue
= pb
->num_geqs
- 1; Ue
>= 0; Ue
--)
4332 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4334 if (lbeqn
->key
== -pb
->geqs
[Ue
].key
)
4335 omega_delete_geq_extra (pb
, Ue
, n_vars
+ 1);
4339 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4340 pb
->geqs
[Ue
].touched
= 1;
4341 eliminate_again
= false;
4343 if (lbeqn
->color
== omega_red
)
4344 pb
->geqs
[Ue
].color
= omega_red
;
4346 for (k
= 0; k
<= n_vars
; k
++)
4347 pb
->geqs
[Ue
].coef
[k
] =
4348 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4349 check_mul (lbeqn
->coef
[k
], Uc
);
4351 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4353 omega_print_geq (dump_file
, pb
,
4355 fprintf (dump_file
, "\n");
4360 omega_free_eqns (lbeqn
, 1);
4365 int *dead_eqns
= XNEWVEC (int, OMEGA_MAX_GEQS
);
4366 bool *is_dead
= XNEWVEC (bool, OMEGA_MAX_GEQS
);
4368 int top_eqn
= pb
->num_geqs
- 1;
4369 lower_bound_count
--;
4371 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4372 fprintf (dump_file
, "lower bound count = %d\n",
4375 for (Le
= top_eqn
; Le
>= 0; Le
--)
4376 if (pb
->geqs
[Le
].coef
[i
] > 0)
4378 int Lc
= pb
->geqs
[Le
].coef
[i
];
4379 for (Ue
= top_eqn
; Ue
>= 0; Ue
--)
4380 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4382 if (pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4385 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4388 e2
= pb
->num_geqs
++;
4390 e2
= dead_eqns
[--num_dead
];
4392 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4394 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4397 "Le = %d, Ue = %d, gen = %d\n",
4399 omega_print_geq_extra (dump_file
, pb
,
4401 fprintf (dump_file
, "\n");
4402 omega_print_geq_extra (dump_file
, pb
,
4404 fprintf (dump_file
, "\n");
4407 eliminate_again
= false;
4409 for (k
= n_vars
; k
>= 0; k
--)
4410 pb
->geqs
[e2
].coef
[k
] =
4411 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4412 check_mul (pb
->geqs
[Le
].coef
[k
], Uc
);
4414 pb
->geqs
[e2
].coef
[n_vars
+ 1] = 0;
4415 pb
->geqs
[e2
].touched
= 1;
4417 if (pb
->geqs
[Ue
].color
== omega_red
4418 || pb
->geqs
[Le
].color
== omega_red
)
4419 pb
->geqs
[e2
].color
= omega_red
;
4421 pb
->geqs
[e2
].color
= omega_black
;
4423 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4425 omega_print_geq (dump_file
, pb
,
4427 fprintf (dump_file
, "\n");
4431 if (lower_bound_count
== 0)
4433 dead_eqns
[num_dead
++] = Ue
;
4435 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4436 fprintf (dump_file
, "Killed %d\n", Ue
);
4440 lower_bound_count
--;
4441 dead_eqns
[num_dead
++] = Le
;
4443 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4444 fprintf (dump_file
, "Killed %d\n", Le
);
4447 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4450 while (num_dead
> 0)
4451 is_dead
[dead_eqns
[--num_dead
]] = true;
4453 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4455 omega_delete_geq_extra (pb
, e
, n_vars
+ 1);
4466 rS
= omega_alloc_problem (0, 0);
4467 iS
= omega_alloc_problem (0, 0);
4469 possible_easy_int_solution
= true;
4471 for (e
= 0; e
< pb
->num_geqs
; e
++)
4472 if (pb
->geqs
[e
].coef
[i
] == 0)
4474 omega_copy_eqn (&(rS
->geqs
[e2
]), &pb
->geqs
[e
],
4476 omega_copy_eqn (&(iS
->geqs
[e2
]), &pb
->geqs
[e
],
4479 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4482 fprintf (dump_file
, "Copying (%d, %d): ", i
,
4483 pb
->geqs
[e
].coef
[i
]);
4484 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[e
]);
4485 fprintf (dump_file
, "\n");
4486 for (t
= 0; t
<= n_vars
+ 1; t
++)
4487 fprintf (dump_file
, "%d ", pb
->geqs
[e
].coef
[t
]);
4488 fprintf (dump_file
, "\n");
4492 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4495 for (Le
= pb
->num_geqs
- 1; Le
>= 0; Le
--)
4496 if (pb
->geqs
[Le
].coef
[i
] > 0)
4497 for (Ue
= pb
->num_geqs
- 1; Ue
>= 0; Ue
--)
4498 if (pb
->geqs
[Ue
].coef
[i
] < 0)
4501 int Lc
= pb
->geqs
[Le
].coef
[i
];
4502 int Uc
= -pb
->geqs
[Ue
].coef
[i
];
4504 if (pb
->geqs
[Le
].key
!= -pb
->geqs
[Ue
].key
)
4507 rS
->geqs
[e2
].touched
= iS
->geqs
[e2
].touched
= 1;
4509 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4511 fprintf (dump_file
, "---\n");
4513 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4514 Le
, Lc
, Ue
, Uc
, e2
);
4515 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[Le
]);
4516 fprintf (dump_file
, "\n");
4517 omega_print_geq_extra (dump_file
, pb
, &pb
->geqs
[Ue
]);
4518 fprintf (dump_file
, "\n");
4523 for (k
= n_vars
; k
>= 0; k
--)
4524 iS
->geqs
[e2
].coef
[k
] = rS
->geqs
[e2
].coef
[k
] =
4525 pb
->geqs
[Ue
].coef
[k
] + pb
->geqs
[Le
].coef
[k
];
4527 iS
->geqs
[e2
].coef
[0] -= (Uc
- 1);
4531 for (k
= n_vars
; k
>= 0; k
--)
4532 iS
->geqs
[e2
].coef
[k
] = rS
->geqs
[e2
].coef
[k
] =
4533 check_mul (pb
->geqs
[Ue
].coef
[k
], Lc
) +
4534 check_mul (pb
->geqs
[Le
].coef
[k
], Uc
);
4536 iS
->geqs
[e2
].coef
[0] -= (Uc
- 1) * (Lc
- 1);
4539 if (pb
->geqs
[Ue
].color
== omega_red
4540 || pb
->geqs
[Le
].color
== omega_red
)
4541 iS
->geqs
[e2
].color
= rS
->geqs
[e2
].color
= omega_red
;
4543 iS
->geqs
[e2
].color
= rS
->geqs
[e2
].color
= omega_black
;
4545 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4547 omega_print_geq (dump_file
, pb
, &(rS
->geqs
[e2
]));
4548 fprintf (dump_file
, "\n");
4552 gcc_assert (e2
< OMEGA_MAX_GEQS
);
4554 else if (pb
->geqs
[Ue
].coef
[0] * Lc
+
4555 pb
->geqs
[Le
].coef
[0] * Uc
-
4556 (Uc
- 1) * (Lc
- 1) < 0)
4557 possible_easy_int_solution
= false;
4560 iS
->variables_initialized
= rS
->variables_initialized
= true;
4561 iS
->num_vars
= rS
->num_vars
= pb
->num_vars
;
4562 iS
->num_geqs
= rS
->num_geqs
= e2
;
4563 iS
->num_eqs
= rS
->num_eqs
= 0;
4564 iS
->num_subs
= rS
->num_subs
= pb
->num_subs
;
4565 iS
->safe_vars
= rS
->safe_vars
= pb
->safe_vars
;
4567 for (e
= n_vars
; e
>= 0; e
--)
4568 rS
->var
[e
] = pb
->var
[e
];
4570 for (e
= n_vars
; e
>= 0; e
--)
4571 iS
->var
[e
] = pb
->var
[e
];
4573 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
4575 omega_copy_eqn (&(rS
->subs
[e
]), &(pb
->subs
[e
]), pb
->num_vars
);
4576 omega_copy_eqn (&(iS
->subs
[e
]), &(pb
->subs
[e
]), pb
->num_vars
);
4580 n_vars
= pb
->num_vars
;
4582 if (desired_res
!= omega_true
)
4584 if (original_problem
== no_problem
)
4586 original_problem
= pb
;
4587 result
= omega_solve_geq (rS
, omega_false
);
4588 original_problem
= no_problem
;
4591 result
= omega_solve_geq (rS
, omega_false
);
4593 if (result
== omega_false
)
4600 if (pb
->num_eqs
> 0)
4602 /* An equality constraint must have been found */
4605 return omega_solve_problem (pb
, desired_res
);
4609 if (desired_res
!= omega_false
)
4612 int lower_bounds
= 0;
4613 int *lower_bound
= XNEWVEC (int, OMEGA_MAX_GEQS
);
4615 if (possible_easy_int_solution
)
4618 result
= omega_solve_geq (iS
, desired_res
);
4621 if (result
!= omega_false
)
4630 if (!exact
&& best_parallel_eqn
>= 0
4631 && parallel_difference
<= max_splinters
)
4636 return parallel_splinter (pb
, best_parallel_eqn
,
4637 parallel_difference
,
4641 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4642 fprintf (dump_file
, "have to do exact analysis\n");
4646 for (e
= 0; e
< pb
->num_geqs
; e
++)
4647 if (pb
->geqs
[e
].coef
[i
] > 1)
4648 lower_bound
[lower_bounds
++] = e
;
4650 /* Sort array LOWER_BOUND. */
4651 for (j
= 0; j
< lower_bounds
; j
++)
4653 int k
, smallest
= j
;
4655 for (k
= j
+ 1; k
< lower_bounds
; k
++)
4656 if (pb
->geqs
[lower_bound
[smallest
]].coef
[i
] >
4657 pb
->geqs
[lower_bound
[k
]].coef
[i
])
4660 k
= lower_bound
[smallest
];
4661 lower_bound
[smallest
] = lower_bound
[j
];
4665 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4667 fprintf (dump_file
, "lower bound coefficients = ");
4669 for (j
= 0; j
< lower_bounds
; j
++)
4670 fprintf (dump_file
, " %d",
4671 pb
->geqs
[lower_bound
[j
]].coef
[i
]);
4673 fprintf (dump_file
, "\n");
4676 for (j
= 0; j
< lower_bounds
; j
++)
4680 int worst_lower_bound_constant
= -minC
;
4683 max_incr
= (((pb
->geqs
[e
].coef
[i
] - 1) *
4684 (worst_lower_bound_constant
- 1) - 1)
4685 / worst_lower_bound_constant
);
4686 /* max_incr += 2; */
4688 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4690 fprintf (dump_file
, "for equation ");
4691 omega_print_geq (dump_file
, pb
, &pb
->geqs
[e
]);
4693 "\ntry decrements from 0 to %d\n",
4695 omega_print_problem (dump_file
, pb
);
4698 if (max_incr
> 50 && !smoothed
4699 && smooth_weird_equations (pb
))
4705 goto solve_geq_start
;
4708 omega_copy_eqn (&pb
->eqs
[0], &pb
->geqs
[e
],
4710 pb
->eqs
[0].color
= omega_black
;
4711 omega_init_eqn_zero (&pb
->geqs
[e
], pb
->num_vars
);
4712 pb
->geqs
[e
].touched
= 1;
4715 for (c
= max_incr
; c
>= 0; c
--)
4717 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4720 "trying next decrement of %d\n",
4722 omega_print_problem (dump_file
, pb
);
4725 omega_copy_problem (rS
, pb
);
4727 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4728 omega_print_problem (dump_file
, rS
);
4730 result
= omega_solve_problem (rS
, desired_res
);
4732 if (result
== omega_true
)
4741 pb
->eqs
[0].coef
[0]--;
4744 if (j
+ 1 < lower_bounds
)
4747 omega_copy_eqn (&pb
->geqs
[e
], &pb
->eqs
[0],
4749 pb
->geqs
[e
].touched
= 1;
4750 pb
->geqs
[e
].color
= omega_black
;
4751 omega_copy_problem (rS
, pb
);
4753 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4755 "exhausted lower bound, "
4756 "checking if still feasible ");
4758 result
= omega_solve_problem (rS
, omega_false
);
4760 if (result
== omega_false
)
4765 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4766 fprintf (dump_file
, "fall-off the end\n");
4778 return omega_unknown
;
4779 } while (eliminate_again
);
4783 /* Because the omega solver is recursive, this counter limits the
4785 static int omega_solve_depth
= 0;
4787 /* Return omega_true when the problem PB has a solution following the
4791 omega_solve_problem (omega_pb pb
, enum omega_result desired_res
)
4793 enum omega_result result
;
4795 gcc_assert (pb
->num_vars
>= pb
->safe_vars
);
4796 omega_solve_depth
++;
4798 if (desired_res
!= omega_simplify
)
4801 if (omega_solve_depth
> 50)
4803 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4806 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4807 omega_solve_depth
, in_approximate_mode
);
4808 omega_print_problem (dump_file
, pb
);
4813 if (omega_solve_eq (pb
, desired_res
) == omega_false
)
4815 omega_solve_depth
--;
4819 if (in_approximate_mode
&& !pb
->num_geqs
)
4821 result
= omega_true
;
4822 pb
->num_vars
= pb
->safe_vars
;
4823 omega_problem_reduced (pb
);
4826 result
= omega_solve_geq (pb
, desired_res
);
4828 omega_solve_depth
--;
4830 if (!omega_reduce_with_subs
)
4832 resurrect_subs (pb
);
4833 gcc_assert (please_no_equalities_in_simplified_problems
4834 || !result
|| pb
->num_subs
== 0);
4840 /* Return true if red equations constrain the set of possible solutions.
4841 We assume that there are solutions to the black equations by
4842 themselves, so if there is no solution to the combined problem, we
4846 omega_problem_has_red_equations (omega_pb pb
)
4852 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4854 fprintf (dump_file
, "Checking for red equations:\n");
4855 omega_print_problem (dump_file
, pb
);
4858 please_no_equalities_in_simplified_problems
++;
4861 if (omega_single_result
)
4862 return_single_result
++;
4864 create_color
= true;
4865 result
= (omega_simplify_problem (pb
) == omega_false
);
4867 if (omega_single_result
)
4868 return_single_result
--;
4871 please_no_equalities_in_simplified_problems
--;
4875 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4876 fprintf (dump_file
, "Gist is FALSE\n");
4881 pb
->eqs
[0].color
= omega_red
;
4883 for (i
= pb
->num_vars
; i
> 0; i
--)
4884 pb
->eqs
[0].coef
[i
] = 0;
4886 pb
->eqs
[0].coef
[0] = 1;
4890 free_red_eliminations (pb
);
4891 gcc_assert (pb
->num_eqs
== 0);
4893 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4894 if (pb
->geqs
[e
].color
== omega_red
)
4900 for (i
= pb
->safe_vars
; i
>= 1; i
--)
4905 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4907 if (pb
->geqs
[e
].coef
[i
])
4909 if (pb
->geqs
[e
].coef
[i
] > 0)
4910 lb
|= (1 + (pb
->geqs
[e
].color
== omega_red
? 1 : 0));
4913 ub
|= (1 + (pb
->geqs
[e
].color
== omega_red
? 1 : 0));
4917 if (ub
== 2 || lb
== 2)
4920 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4921 fprintf (dump_file
, "checks for upper/lower bounds worked!\n");
4923 if (!omega_reduce_with_subs
)
4925 resurrect_subs (pb
);
4926 gcc_assert (pb
->num_subs
== 0);
4934 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4936 "*** Doing potentially expensive elimination tests "
4937 "for red equations\n");
4939 please_no_equalities_in_simplified_problems
++;
4940 omega_eliminate_red (pb
, true);
4941 please_no_equalities_in_simplified_problems
--;
4944 gcc_assert (pb
->num_eqs
== 0);
4946 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
4947 if (pb
->geqs
[e
].color
== omega_red
)
4950 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4954 "******************** Redundant Red Equations eliminated!!\n");
4957 "******************** Red Equations remain\n");
4959 omega_print_problem (dump_file
, pb
);
4962 if (!omega_reduce_with_subs
)
4964 normalize_return_type r
;
4966 resurrect_subs (pb
);
4967 r
= normalize_omega_problem (pb
);
4968 gcc_assert (r
!= normalize_false
);
4971 cleanout_wildcards (pb
);
4972 gcc_assert (pb
->num_subs
== 0);
4978 /* Calls omega_simplify_problem in approximate mode. */
4981 omega_simplify_approximate (omega_pb pb
)
4983 enum omega_result result
;
4985 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4986 fprintf (dump_file
, "(Entering approximate mode\n");
4988 in_approximate_mode
= true;
4989 result
= omega_simplify_problem (pb
);
4990 in_approximate_mode
= false;
4992 gcc_assert (pb
->num_vars
== pb
->safe_vars
);
4993 if (!omega_reduce_with_subs
)
4994 gcc_assert (pb
->num_subs
== 0);
4996 if (dump_file
&& (dump_flags
& TDF_DETAILS
))
4997 fprintf (dump_file
, "Leaving approximate mode)\n");
5003 /* Simplifies problem PB by eliminating redundant constraints and
5004 reducing the constraints system to a minimal form. Returns
5005 omega_true when the problem was successfully reduced, omega_unknown
5006 when the solver is unable to determine an answer. */
5009 omega_simplify_problem (omega_pb pb
)
5013 omega_found_reduction
= omega_false
;
5015 if (!pb
->variables_initialized
)
5016 omega_initialize_variables (pb
);
5018 if (next_key
* 3 > MAX_KEYS
)
5023 next_key
= OMEGA_MAX_VARS
+ 1;
5025 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5026 pb
->geqs
[e
].touched
= 1;
5028 for (i
= 0; i
< HASH_TABLE_SIZE
; i
++)
5029 hash_master
[i
].touched
= -1;
5031 pb
->hash_version
= hash_version
;
5034 else if (pb
->hash_version
!= hash_version
)
5038 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5039 pb
->geqs
[e
].touched
= 1;
5041 pb
->hash_version
= hash_version
;
5044 if (pb
->num_vars
> pb
->num_eqs
+ 3 * pb
->safe_vars
)
5045 omega_free_eliminations (pb
, pb
->safe_vars
);
5047 if (!may_be_red
&& pb
->num_subs
== 0 && pb
->safe_vars
== 0)
5049 omega_found_reduction
= omega_solve_problem (pb
, omega_unknown
);
5051 if (omega_found_reduction
!= omega_false
5052 && !return_single_result
)
5056 (*omega_when_reduced
) (pb
);
5059 return omega_found_reduction
;
5062 omega_solve_problem (pb
, omega_simplify
);
5064 if (omega_found_reduction
!= omega_false
)
5066 for (i
= 1; omega_safe_var_p (pb
, i
); i
++)
5067 pb
->forwarding_address
[pb
->var
[i
]] = i
;
5069 for (i
= 0; i
< pb
->num_subs
; i
++)
5070 pb
->forwarding_address
[pb
->subs
[i
].key
] = -i
- 1;
5073 if (!omega_reduce_with_subs
)
5074 gcc_assert (please_no_equalities_in_simplified_problems
5075 || omega_found_reduction
== omega_false
5076 || pb
->num_subs
== 0);
5078 return omega_found_reduction
;
5081 /* Make variable VAR unprotected: it then can be eliminated. */
5084 omega_unprotect_variable (omega_pb pb
, int var
)
5087 idx
= pb
->forwarding_address
[var
];
5094 if (idx
< pb
->num_subs
)
5096 omega_copy_eqn (&pb
->subs
[idx
], &pb
->subs
[pb
->num_subs
],
5098 pb
->forwarding_address
[pb
->subs
[idx
].key
] = -idx
- 1;
5103 int *bring_to_life
= XNEWVEC (int, OMEGA_MAX_VARS
);
5106 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5107 bring_to_life
[e
] = (pb
->subs
[e
].coef
[idx
] != 0);
5109 for (e2
= pb
->num_subs
- 1; e2
>= 0; e2
--)
5110 if (bring_to_life
[e2
])
5115 if (pb
->safe_vars
< pb
->num_vars
)
5117 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5119 pb
->geqs
[e
].coef
[pb
->num_vars
] =
5120 pb
->geqs
[e
].coef
[pb
->safe_vars
];
5122 pb
->geqs
[e
].coef
[pb
->safe_vars
] = 0;
5125 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5127 pb
->eqs
[e
].coef
[pb
->num_vars
] =
5128 pb
->eqs
[e
].coef
[pb
->safe_vars
];
5130 pb
->eqs
[e
].coef
[pb
->safe_vars
] = 0;
5133 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5135 pb
->subs
[e
].coef
[pb
->num_vars
] =
5136 pb
->subs
[e
].coef
[pb
->safe_vars
];
5138 pb
->subs
[e
].coef
[pb
->safe_vars
] = 0;
5141 pb
->var
[pb
->num_vars
] = pb
->var
[pb
->safe_vars
];
5142 pb
->forwarding_address
[pb
->var
[pb
->num_vars
]] =
5147 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5148 pb
->geqs
[e
].coef
[pb
->safe_vars
] = 0;
5150 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5151 pb
->eqs
[e
].coef
[pb
->safe_vars
] = 0;
5153 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5154 pb
->subs
[e
].coef
[pb
->safe_vars
] = 0;
5157 pb
->var
[pb
->safe_vars
] = pb
->subs
[e2
].key
;
5158 pb
->forwarding_address
[pb
->subs
[e2
].key
] = pb
->safe_vars
;
5160 omega_copy_eqn (&(pb
->eqs
[pb
->num_eqs
]), &(pb
->subs
[e2
]),
5162 pb
->eqs
[pb
->num_eqs
++].coef
[pb
->safe_vars
] = -1;
5163 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5165 if (e2
< pb
->num_subs
- 1)
5166 omega_copy_eqn (&(pb
->subs
[e2
]), &(pb
->subs
[pb
->num_subs
- 1]),
5172 omega_unprotect_1 (pb
, &idx
, NULL
);
5173 free (bring_to_life
);
5176 chain_unprotect (pb
);
5179 /* Unprotects VAR and simplifies PB. */
5182 omega_constrain_variable_sign (omega_pb pb
, enum omega_eqn_color color
,
5185 int n_vars
= pb
->num_vars
;
5187 int k
= pb
->forwarding_address
[var
];
5196 omega_copy_eqn (&pb
->geqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5198 for (j
= 0; j
<= n_vars
; j
++)
5199 pb
->geqs
[e
].coef
[j
] *= sign
;
5201 pb
->geqs
[e
].coef
[0]--;
5202 pb
->geqs
[e
].touched
= 1;
5203 pb
->geqs
[e
].color
= color
;
5208 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5209 omega_copy_eqn (&pb
->eqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5210 pb
->eqs
[e
].color
= color
;
5216 omega_init_eqn_zero (&pb
->geqs
[e
], pb
->num_vars
);
5217 pb
->geqs
[e
].coef
[k
] = sign
;
5218 pb
->geqs
[e
].coef
[0] = -1;
5219 pb
->geqs
[e
].touched
= 1;
5220 pb
->geqs
[e
].color
= color
;
5225 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5226 omega_init_eqn_zero (&pb
->eqs
[e
], pb
->num_vars
);
5227 pb
->eqs
[e
].coef
[k
] = 1;
5228 pb
->eqs
[e
].color
= color
;
5231 omega_unprotect_variable (pb
, var
);
5232 return omega_simplify_problem (pb
);
5235 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5238 omega_constrain_variable_value (omega_pb pb
, enum omega_eqn_color color
,
5242 int k
= pb
->forwarding_address
[var
];
5248 gcc_assert (pb
->num_eqs
<= OMEGA_MAX_EQS
);
5249 omega_copy_eqn (&pb
->eqs
[e
], &pb
->subs
[k
], pb
->num_vars
);
5250 pb
->eqs
[e
].coef
[0] -= value
;
5255 omega_init_eqn_zero (&pb
->eqs
[e
], pb
->num_vars
);
5256 pb
->eqs
[e
].coef
[k
] = 1;
5257 pb
->eqs
[e
].coef
[0] = -value
;
5260 pb
->eqs
[e
].color
= color
;
5263 /* Return false when the upper and lower bounds are not coupled.
5264 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5268 omega_query_variable (omega_pb pb
, int i
, int *lower_bound
, int *upper_bound
)
5270 int n_vars
= pb
->num_vars
;
5273 bool coupled
= false;
5275 *lower_bound
= neg_infinity
;
5276 *upper_bound
= pos_infinity
;
5277 i
= pb
->forwarding_address
[i
];
5283 for (j
= 1; j
<= n_vars
; j
++)
5284 if (pb
->subs
[i
].coef
[j
] != 0)
5287 *upper_bound
= *lower_bound
= pb
->subs
[i
].coef
[0];
5291 for (e
= pb
->num_subs
- 1; e
>= 0; e
--)
5292 if (pb
->subs
[e
].coef
[i
] != 0)
5295 for (e
= pb
->num_eqs
- 1; e
>= 0; e
--)
5296 if (pb
->eqs
[e
].coef
[i
] != 0)
5300 for (j
= 1; j
<= n_vars
; j
++)
5301 if (i
!= j
&& pb
->eqs
[e
].coef
[j
] != 0)
5312 *lower_bound
= *upper_bound
=
5313 -pb
->eqs
[e
].coef
[i
] * pb
->eqs
[e
].coef
[0];
5318 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5319 if (pb
->geqs
[e
].coef
[i
] != 0)
5321 if (pb
->geqs
[e
].key
== i
)
5322 *lower_bound
= MAX (*lower_bound
, -pb
->geqs
[e
].coef
[0]);
5324 else if (pb
->geqs
[e
].key
== -i
)
5325 *upper_bound
= MIN (*upper_bound
, pb
->geqs
[e
].coef
[0]);
5334 /* Sets the lower bound L and upper bound U for the values of variable
5335 I, and sets COULD_BE_ZERO to true if variable I might take value
5336 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5340 query_coupled_variable (omega_pb pb
, int i
, int *l
, int *u
,
5341 bool *could_be_zero
, int lower_bound
, int upper_bound
)
5348 /* Preconditions. */
5349 gcc_assert (abs (pb
->forwarding_address
[i
]) == 1
5350 && pb
->num_vars
+ pb
->num_subs
== 2
5351 && pb
->num_eqs
+ pb
->num_subs
== 1);
5353 /* Define variable I in terms of variable V. */
5354 if (pb
->forwarding_address
[i
] == -1)
5363 sign
= -eqn
->coef
[1];
5367 for (e
= pb
->num_geqs
- 1; e
>= 0; e
--)
5368 if (pb
->geqs
[e
].coef
[v
] != 0)
5370 if (pb
->geqs
[e
].coef
[v
] == 1)
5371 lower_bound
= MAX (lower_bound
, -pb
->geqs
[e
].coef
[0]);
5374 upper_bound
= MIN (upper_bound
, pb
->geqs
[e
].coef
[0]);
5377 if (lower_bound
> upper_bound
)
5385 if (lower_bound
== neg_infinity
)
5387 if (eqn
->coef
[v
] > 0)
5388 b1
= sign
* neg_infinity
;
5391 b1
= -sign
* neg_infinity
;
5394 b1
= sign
* (eqn
->coef
[0] + eqn
->coef
[v
] * lower_bound
);
5396 if (upper_bound
== pos_infinity
)
5398 if (eqn
->coef
[v
] > 0)
5399 b2
= sign
* pos_infinity
;
5402 b2
= -sign
* pos_infinity
;
5405 b2
= sign
* (eqn
->coef
[0] + eqn
->coef
[v
] * upper_bound
);
5407 *l
= MAX (*l
, b1
<= b2
? b1
: b2
);
5408 *u
= MIN (*u
, b1
<= b2
? b2
: b1
);
5410 *could_be_zero
= (*l
<= 0 && 0 <= *u
5411 && int_mod (eqn
->coef
[0], abs (eqn
->coef
[v
])) == 0);
5414 /* Return false when a lower bound L and an upper bound U for variable
5415 I in problem PB have been initialized. */
5418 omega_query_variable_bounds (omega_pb pb
, int i
, int *l
, int *u
)
5423 if (!omega_query_variable (pb
, i
, l
, u
)
5424 || (pb
->num_vars
== 1 && pb
->forwarding_address
[i
] == 1))
5427 if (abs (pb
->forwarding_address
[i
]) == 1
5428 && pb
->num_vars
+ pb
->num_subs
== 2
5429 && pb
->num_eqs
+ pb
->num_subs
== 1)
5432 query_coupled_variable (pb
, i
, l
, u
, &could_be_zero
, neg_infinity
,
5440 /* For problem PB, return an integer that represents the classic data
5441 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5442 masks that are added to the result. When DIST_KNOWN is true, DIST
5443 is set to the classic data dependence distance. LOWER_BOUND and
5444 UPPER_BOUND are bounds on the value of variable I, for example, it
5445 is possible to narrow the iteration domain with safe approximations
5446 of loop counts, and thus discard some data dependences that cannot
5450 omega_query_variable_signs (omega_pb pb
, int i
, int dd_lt
,
5451 int dd_eq
, int dd_gt
, int lower_bound
,
5452 int upper_bound
, bool *dist_known
, int *dist
)
5461 omega_query_variable (pb
, i
, &l
, &u
);
5462 query_coupled_variable (pb
, i
, &l
, &u
, &could_be_zero
, lower_bound
,
5481 *dist_known
= false;
5486 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5487 safe variables. Safe variables are not eliminated during the
5488 Fourier-Motzkin elimination. Safe variables are all those
5489 variables that are placed at the beginning of the array of
5490 variables: P->var[0, ..., NPROT - 1]. */
5493 omega_alloc_problem (int nvars
, int nprot
)
5497 gcc_assert (nvars
<= OMEGA_MAX_VARS
);
5498 omega_initialize ();
5500 /* Allocate and initialize PB. */
5501 pb
= XCNEW (struct omega_pb
);
5502 pb
->var
= XCNEWVEC (int, OMEGA_MAX_VARS
+ 2);
5503 pb
->forwarding_address
= XCNEWVEC (int, OMEGA_MAX_VARS
+ 2);
5504 pb
->geqs
= omega_alloc_eqns (0, OMEGA_MAX_GEQS
);
5505 pb
->eqs
= omega_alloc_eqns (0, OMEGA_MAX_EQS
);
5506 pb
->subs
= omega_alloc_eqns (0, OMEGA_MAX_VARS
+ 1);
5508 pb
->hash_version
= hash_version
;
5509 pb
->num_vars
= nvars
;
5510 pb
->safe_vars
= nprot
;
5511 pb
->variables_initialized
= false;
5512 pb
->variables_freed
= false;
5519 /* Keeps the state of the initialization. */
5520 static bool omega_initialized
= false;
5522 /* Initialization of the Omega solver. */
5525 omega_initialize (void)
5529 if (omega_initialized
)
5533 next_key
= OMEGA_MAX_VARS
+ 1;
5534 packing
= XCNEWVEC (int, OMEGA_MAX_VARS
);
5535 fast_lookup
= XCNEWVEC (int, MAX_KEYS
* 2);
5536 fast_lookup_red
= XCNEWVEC (int, MAX_KEYS
* 2);
5537 hash_master
= omega_alloc_eqns (0, HASH_TABLE_SIZE
);
5539 for (i
= 0; i
< HASH_TABLE_SIZE
; i
++)
5540 hash_master
[i
].touched
= -1;
5542 sprintf (wild_name
[0], "1");
5543 sprintf (wild_name
[1], "a");
5544 sprintf (wild_name
[2], "b");
5545 sprintf (wild_name
[3], "c");
5546 sprintf (wild_name
[4], "d");
5547 sprintf (wild_name
[5], "e");
5548 sprintf (wild_name
[6], "f");
5549 sprintf (wild_name
[7], "g");
5550 sprintf (wild_name
[8], "h");
5551 sprintf (wild_name
[9], "i");
5552 sprintf (wild_name
[10], "j");
5553 sprintf (wild_name
[11], "k");
5554 sprintf (wild_name
[12], "l");
5555 sprintf (wild_name
[13], "m");
5556 sprintf (wild_name
[14], "n");
5557 sprintf (wild_name
[15], "o");
5558 sprintf (wild_name
[16], "p");
5559 sprintf (wild_name
[17], "q");
5560 sprintf (wild_name
[18], "r");
5561 sprintf (wild_name
[19], "s");
5562 sprintf (wild_name
[20], "t");
5563 sprintf (wild_name
[40 - 1], "alpha");
5564 sprintf (wild_name
[40 - 2], "beta");
5565 sprintf (wild_name
[40 - 3], "gamma");
5566 sprintf (wild_name
[40 - 4], "delta");
5567 sprintf (wild_name
[40 - 5], "tau");
5568 sprintf (wild_name
[40 - 6], "sigma");
5569 sprintf (wild_name
[40 - 7], "chi");
5570 sprintf (wild_name
[40 - 8], "omega");
5571 sprintf (wild_name
[40 - 9], "pi");
5572 sprintf (wild_name
[40 - 10], "ni");
5573 sprintf (wild_name
[40 - 11], "Alpha");
5574 sprintf (wild_name
[40 - 12], "Beta");
5575 sprintf (wild_name
[40 - 13], "Gamma");
5576 sprintf (wild_name
[40 - 14], "Delta");
5577 sprintf (wild_name
[40 - 15], "Tau");
5578 sprintf (wild_name
[40 - 16], "Sigma");
5579 sprintf (wild_name
[40 - 17], "Chi");
5580 sprintf (wild_name
[40 - 18], "Omega");
5581 sprintf (wild_name
[40 - 19], "xxx");
5583 omega_initialized
= true;