PIPS
|
#include <string.h>
#include <stdio.h>
#include <stdlib.h>
#include "linear_assert.h"
#include <limits.h>
#include "boolean.h"
#include "arithmetique.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
Go to the source code of this file.
Macros | |
#define | MAX_NUMBER_OF_CONSTRAINTS (x_max-x_min) |
#define | if_debug_sc_strong_normalize_2 if(false) |
#define | if_debug_sc_strong_normalize_and_check_feasibility2 if(false) |
Functions | |
static void | negate_value_interval (Value *pmin, Value *pmax) |
package sc More... | |
static void | swap_values (Value *p1, Value *p2) |
static void | swap_value_intervals (Value *px_min, Value *px_max, Value *py_min, Value *py_max) |
static void | update_lower_or_upper_bound (Pvecteur *bound_p, Pvecteur *bound_base_p, Variable var, Value nb, bool lower_p) |
Bounding box (not really a box most of the time) More... | |
static bool | update_lower_and_upper_bounds (Pvecteur *ubound_p, Pvecteur *ubound_base_p, Pvecteur *lbound_p, Pvecteur *lbound_base_p, Variable var, Value nb) |
Updates upper and lower bounds, (ubound_p, ubound_base_p) and (lbound_p, lbound_base_p), with equations var==nb. More... | |
static void | simplify_constraint_with_bounding_box (Pcontrainte eq, Pbase cb, Pvecteur l, bool is_inequality_p __attribute__((unused))) |
Use constants imposed by the bounding box to eliminate constant terms from constraint eq. More... | |
static Pvecteur | compute_x_and_y_bounds (Pvecteur v, Pvecteur l, Pvecteur lb, Pvecteur u, Pvecteur ub, Variable *px, Variable *py, Value *px_min, Value *px_max, int *pcb) |
v is supposed to be the equation of a line in a 2-D space. More... | |
static bool | eligible_for_coefficient_reduction_with_bounding_box_p (Pvecteur v, Pvecteur l, Pvecteur lb, Pvecteur u, Pvecteur ub) |
Is it possible to reduce the magnitude of at least one constraint coefficient because it is larger than the intervals defined by the bounding box for the other variable? More... | |
static bool | small_slope_and_first_quadrant_p (Pvecteur v) |
Check that the coefficients on the first and second variables, x and y, define a increasing line. More... | |
static Pvecteur | new_constraint_for_coefficient_reduction_with_bounding_box (Pvecteur v, int *pcb, Variable x, Variable y, Value *px_min, Value *px_max, Value *py_min, Value *py_max) |
Compute a normalized version of the constraint v and the corresponding change of basis. More... | |
static Pvecteur | vect_make_line (Variable x, Variable y, Value x0, Value y0, Value x1, Value y1) |
FI: Could be moved in vecteur library... More... | |
static bool | find_first_integer_point_in_between (Value x0, Value y0, Pvecteur up_c, Pvecteur low_c, Variable xv, Variable yv, Value dx, Value dy, Value xf, Value yf __attribute__((unused)), Value *pfx, Value *pfy) |
Find the first significant integer point (*pfx, *pfy) starting from (x0,y0) moving by (dx,dy) steps towards (xf,yf) that is between the constraint up_c and low_c such that *pfx!=xf and pfx!=x0. More... | |
static bool | find_integer_point_to_the_right (Value x0, Value y0, Pvecteur up, Pvecteur low, Variable x, Variable y, Value xf, Value yf, Value *pfx, Value *pfy) |
static bool | find_integer_point_to_the_left (Value x0, Value y0, Pvecteur up, Pvecteur low, Variable x, Variable y, Value xf, Value yf, Value *pfx, Value *pfy) |
static Value | eval_2D_vecteur (Pvecteur v, Variable x, Variable y, Value xv, Value yv) |
FI: a bit too specific for vecteur library? More... | |
static Pcontrainte | build_convex_constraints_from_vertices (Variable x, Variable y, int ni, int eni, Value ilmpx[ni+2], Value ilmpy[ni+2]) |
Use the first eni+2 points in ilmpx and ilmpy to build at most eni+1 convex constraints, all upper bounds for y. More... | |
Pcontrainte | find_intermediate_constraints_recursively (Pvecteur v, Variable x, Variable y, Value lmpx, Value lmpy, Value rmpx, Value rmpy) |
Find a set ineq of 2-D constraints equivalent to 2-D constraint v==ax+by+c over the interval [lmpx,rmpx]. More... | |
Pcontrainte | find_intermediate_constraints (Pvecteur v, Variable x, Variable y, Value lmpx, Value lmpy, Value rmpx, Value rmpy) |
Find a set ineq of 2-D constraints equivalent to 2-D constraint v==ax+by+c over the interval [lmpx,rmpx]. More... | |
static Pcontrainte | small_positive_slope_reduce_coefficients_with_bounding_box (Pvecteur v, Variable x, Value x_min, Value x_max, Variable y, Value y_min __attribute__((unused)), Value y_max __attribute__((unused))) |
Replace 2-D constraint v by a set of constraints when possible because variable x is bounded by [x_min,x_max]. More... | |
static void | update_coefficient_signs_in_vector (Pvecteur v, int cb, Variable x, Variable y) |
Perform a reverse change of base to go back into the source code frame. More... | |
static void | update_coefficient_signs_in_constraints (Pcontrainte eq, int cb, Variable x, Variable y, Value *x_min, Value *x_max, Value *y_min, Value *y_max) |
Perform the inverse change of basis and update the intervals for later checks. More... | |
static void | check_coefficient_reduction (Pvecteur v, Pcontrainte ineq, Variable x, Variable y, Value x_min, Value x_max) |
debug function: check that all 2-D constraints c in ineq are equivalent to contraint v on interval [x_min,x_max]. More... | |
static Pcontrainte | reduce_coefficients_with_bounding_box (Pvecteur v, Pvecteur l, Pvecteur lb, Pvecteur u, Pvecteur ub) |
If at least one of the coefficients of constraint v == ax+by<=c are greater that the intervals of the bounding box, reduce them to be at most the the size of the intervals. More... | |
static Psysteme | add_bounding_box_constraints (Psysteme ps, Pbase cb, Pbase lb, Pbase ub, Pvecteur l, Pvecteur u) |
Add the constraints defined by cb, lb and ub in Psysteme ps. More... | |
Psysteme | sc_bounded_normalization (Psysteme ps) |
Eliminate trivially redundant integer constraint using a O(n x d^2) algorithm, where n is the number of constraints and d the dimension. More... | |
Psysteme | sc_normalize (Psysteme ps) |
Psysteme sc_normalize(Psysteme ps): normalisation d'un systeme d'equation et d'inequations lineaires en nombres entiers ps, en place. More... | |
Psysteme | sc_normalize2 (volatile Psysteme ps) |
Psysteme sc_normalize2(Psysteme ps): normalisation d'un systeme d'equation et d'inequations lineaires en nombres entiers ps, en place. More... | |
Psysteme | sc_add_normalize_eq (Psysteme ps, Pcontrainte eq) |
Psysteme | sc_add_normalize_ineq (Psysteme ps, Pcontrainte ineq) |
Psysteme | sc_safe_normalize (Psysteme ps) |
Psysteme sc_safe_normalize(Psysteme ps) output : ps, normalized. More... | |
static Psysteme | sc_rational_feasibility (Psysteme sc) |
Psysteme | sc_strong_normalize (Psysteme ps) |
Psysteme sc_strong_normalize(Psysteme ps) More... | |
Psysteme | sc_strong_normalize3 (Psysteme ps) |
Psysteme | sc_strong_normalize_and_check_feasibility (volatile Psysteme ps, Psysteme(*check_feasibility)(Psysteme)) |
Psysteme | sc_strong_normalize2 (volatile Psysteme ps) |
Psysteme sc_strong_normalize2(Psysteme ps) More... | |
Psysteme | sc_strong_normalize4 (Psysteme ps, char *(*variable_name)(Variable)) |
Psysteme sc_strong_normalize4(Psysteme ps, char * (*variable_name)(Variable)) More... | |
Psysteme | sc_strong_normalize5 (Psysteme ps, char *(*variable_name)(Variable)) |
Psysteme | sc_strong_normalize_and_check_feasibility2 (volatile Psysteme ps, Psysteme(*check_feasibility)(Psysteme), char *(*variable_name)(Variable), int level) |
Psysteme sc_strong_normalize_and_check_feasibility2 (Psysteme ps, Psysteme (*check_feasibility)(Psysteme), char * (*variable_name)(Variable), int level) More... | |
void | sc_gcd_normalize (Psysteme ps) |
sc_gcd_normalize(ps) More... | |
#define MAX_NUMBER_OF_CONSTRAINTS (x_max-x_min) |
|
static |
Add the constraints defined by cb, lb and ub in Psysteme ps.
This is necessary when all constraints redundant wrt the bounding box are removed, for instance to detect simple equalities (x<=2 && x>=2) and to remove redundant constraints (x<=2 && x<=2).
add the equalities
Add the upper bounds
Add the lower bounds
Definition at line 1627 of file sc_normalize.c.
References assert, base_contains_variable_p(), contrainte_make_1D(), contrainte_succ, CONTRAINTE_UNDEFINED, eq, sc_add_egalites(), sc_add_inegalites(), sc_consistent_p(), VALUE_ONE, vect_coeff(), vecteur_succ, VECTEUR_UNDEFINED_P, vecteur_var, and x.
Referenced by sc_bounded_normalization().
|
static |
Use the first eni+2 points in ilmpx and ilmpy to build at most eni+1 convex constraints, all upper bounds for y.
As we build a partial convex hull, there should always be a solution.
The value in ilmpx are assumed to be striclty increasing. The value in ilmpy are increasing. To be convex, the slopes of the successive constraints must be decreasing.
build a constraint between left and right
Check that all points meet the constraint
We could skip the left and right points...
There is always at least one constraint.
All points have been used
The constraints are chained backwards with respect to the vectices
Definition at line 916 of file sc_normalize.c.
References assert, contrainte_make(), contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, count, eval_2D_vecteur(), fprintf(), inegalites_dump(), VALUE_MONE, value_pos_p, vect_make_line(), vect_multiply(), vect_rm(), and x.
Referenced by find_intermediate_constraints_recursively().
|
static |
debug function: check that all 2-D constraints c in ineq are equivalent to contraint v on interval [x_min,x_max].
It is assumed that ineq contains 1, 2 or three constraints.
FI: if the constraint list were properly built, there would be no NULL vector in the list...
FI: linked_regions02; I do not understand whu a NULL constraint is present in ineq...
Scan the x interval
compute bound for y according to v
Definition at line 1466 of file sc_normalize.c.
References abort, assert, CONTRAINTE_NULLE_P, contrainte_succ, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, fprintf(), inegalites_dump(), MAX_NUMBER_OF_CONSTRAINTS, TCST, value_ge, value_gt, value_le, VALUE_MAX, VALUE_MIN, value_negz_p, value_pdiv, value_pos_p, value_posz_p, vect_coeff(), vect_dump(), VECTEUR_NUL_P, and x.
Referenced by reduce_coefficients_with_bounding_box().
|
static |
v is supposed to be the equation of a line in a 2-D space.
l, lb, u and ub define a bounding box for variables in v. Retrieve, when possible, two variables x and y, such that the coefficients for y in v is greater than the interval for x in the bounding box.
Also, make sure that a, the coefficient for x is negative and that b, the coefficient for y is positive. If it is not true, change the frame accordingly and indicate it in *pcb for later conversions.
The bounds are assumed initialized to VALUE_MIN and VALUE_MAX.
If both v1 and v2 are eligible as x, chose arbitrarily v1. This is usually bad design because non determnistic, but I do not have a sorting function available here... A vect_sort() should be performed before calling this function. An intermediate option would be to chose the maximum of a_i/delta_i.
Is v1 eligible as x?
is v2 eligible as x?
We assume here that at least one of the two variables is eligible because it was tested earlier.
For debugging: init_variable_debug_name(entity_local_name)
Let's forget about the slope in ]0,1[, let's try positive slopes
For debugging: init_variable_debug_name(entity_local_name)
Definition at line 327 of file sc_normalize.c.
References assert, fprintf(), negate_value_interval(), TCST, value_abs, value_gt, VALUE_MAX, value_minus, VALUE_NAN, value_neg_p, value_notzero_p, value_pos_p, value_uminus, VALUE_ZERO, value_zero_p, variable_debug_name, vect_add_elem(), vect_coeff(), vect_dump(), vect_make(), vect_normalize(), VECTEUR_NUL, vecteur_succ, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by reduce_coefficients_with_bounding_box().
|
static |
Is it possible to reduce the magnitude of at least one constraint coefficient because it is larger than the intervals defined by the bounding box for the other variable?
Note: the modularity wastes computations. It would be nice to benefit from a, b, dx and dy.
v is a 2-D constraint
The two variables are bounded by a non-degenerated rectangle...
At least one variable is bounded by an interval: sufficient condition
The bounding box is not degenerated. If it is the case, the constraint should have been simplified in a much easier way.
make sure that at least one coefficient can be reduced
Definition at line 462 of file sc_normalize.c.
References TCST, value_abs, value_gt, VALUE_MAX, value_minus, value_notzero_p, value_pos_p, VALUE_ZERO, value_zero_p, VARIABLE_UNDEFINED, VARIABLE_UNDEFINED_P, vect_coeff(), vect_size(), vecteur_succ, VECTEUR_UNDEFINED_P, vecteur_var, and x.
Referenced by reduce_coefficients_with_bounding_box(), and sc_bounded_normalization().
FI: a bit too specific for vecteur library?
FI: overflow control should be added
Definition at line 894 of file sc_normalize.c.
References TCST, VALUE_ZERO, vect_coeff(), and x.
Referenced by build_convex_constraints_from_vertices().
|
static |
Find the first significant integer point (*pfx, *pfy) starting from (x0,y0) moving by (dx,dy) steps towards (xf,yf) that is between the constraint up_c and low_c such that *pfx!=xf and pfx!=x0.
Let x be *pfx and y be *pfy. Between the constraints means up_c(x,y)<=0 and low_c(x,y)>0.
The two constraints up_c and low_c have a positive slope with respect to variables xv and yv over interval [x0,xf] or [xf,x0].
Value yf is only useful for debugging.
It would be possible to find the intermediate points faster using intersections with the constraints instead of using an incremental step-by-step approach.
This is an auxiliary function for coefficient reduction.
Retrieve coefficients of the two constraints
FI: I am tired of using value macros
The two constraints have positive slopes, but not necessarily in the ]0,1[ interval
&& b_up>-a_up
&& b_low>-a_low
Constraint up is higher than constraint low on interval [x0,xf]
There are other points to explore
The intermediate point si strictly over the lower constraint and meet the upper constraint. It is not the initial nor the final point.
Are there more integer points along this direction? If yes, find the last one.
let ndx = x-x0, ndy = y - y0
let x = x0 + th ndx and y = y0 + th ndy (x and y are new variables)
what is the largest integer value for th such that up<=0?
a_up x0 + a_up th ndx + b_up y0 + b_up th ndy + c_up <= 0
th <= (-a_up x0 - b_up y0 - c_up)/(a_up ndx + b_up ndy)
if a_up dx + b_up dy >=0. Else
th >= (a_up x0 + b_up y0 + c_up)/(-a_up ndx - b_up ndy)
then you should find the last one in the [x0,xf] interval...
if ndx > 0, x0+k ndx<=xf else x0+ k ndx >= xf, x0-xf>=-k ndx
The constraint on th is d th + n <=0
lower bound for th: any th positive is good
d>0, upper bound for th
This should occur for slope07, 08 and 09
Make sure that (x,y) meets all the constraints
return the final resut
Definition at line 705 of file sc_normalize.c.
References assert, fprintf(), TCST, value_min, value_pdiv, value_uminus, vect_coeff(), vect_dump(), and x.
Referenced by find_integer_point_to_the_left(), and find_integer_point_to_the_right().
|
static |
Definition at line 879 of file sc_normalize.c.
References assert, find_first_integer_point_in_between(), value_le, VALUE_MONE, and x.
Referenced by find_intermediate_constraints().
|
static |
Definition at line 865 of file sc_normalize.c.
References assert, find_first_integer_point_in_between(), value_ge, VALUE_ONE, and x.
Referenced by find_intermediate_constraints(), and find_intermediate_constraints_recursively().
Pcontrainte find_intermediate_constraints | ( | Pvecteur | v, |
Variable | x, | ||
Variable | y, | ||
Value | lmpx, | ||
Value | lmpy, | ||
Value | rmpx, | ||
Value | rmpy | ||
) |
Find a set ineq of 2-D constraints equivalent to 2-D constraint v==ax+by+c over the interval [lmpx,rmpx].
The slope of the constraints is assumed positive. The values lmpy and rmpy could be computed from v and lmpx and rmpx but are passed down to simplify debugging. The coefficients of the new constraints are smaller than the coefficient of v, assuming that abs(b) is greater than rmpx-lmpx.
This function was based on the wrong assumption that at most three constraints were sufficient to replace exactly v. This is proved wrong by slope15.c.
This function is now obsolete: it was based on the wrong assumption that three constraints at most would be necessary to replace one rational constraint. We ended up with a case requiring four constraints in linked_regions02 and we have no proof that the number of integer vertices, and hence the number of constraints is bounded by a smaller bound than min(dx,dy+1).
Look for intermediate points
A lower upper bound
Start with the initial point in order to be able to compute the slope of the new constraint later
Two constraints
assert convexity
Three constraints at most: be careful about the convexity, the slopes must be decreasing...
We still might have some integer points between (ilmpx,ilmpy) and (rmlpx,rlmpy)...
The first intermediate point, (ilmpx,ilmpy), cannot be used
FI: I assume it never happens... by definition of an intermediate point
We must have slope2<slope3
FI: I assume it never happens... by definition of an intermediate point.
One constraint generated by (lmpx,lmpy) and (rmpx,rmpy)
Definition at line 1091 of file sc_normalize.c.
References abort, assert, contrainte_make(), contraintes_make(), find_integer_point_to_the_left(), find_integer_point_to_the_right(), fprintf(), VALUE_MONE, vect_make_line(), vect_multiply(), VECTEUR_NUL, and x.
Pcontrainte find_intermediate_constraints_recursively | ( | Pvecteur | v, |
Variable | x, | ||
Variable | y, | ||
Value | lmpx, | ||
Value | lmpy, | ||
Value | rmpx, | ||
Value | rmpy | ||
) |
Find a set ineq of 2-D constraints equivalent to 2-D constraint v==ax+by+c over the interval [lmpx,rmpx].
The slope of the constraint v is assumed positive. The values lmpy and rmpy could be computed from v and lmpx and rmpx but are passed down to simplify debugging. The coefficients of the new constraints are smaller than the coefficient of v, assuming that abs(b) is greater than rmpx-lmpx.
The function looks for intermediate points and build the constraints fromm this set of points, making sure to skip some intermediate points if the constraint they generate do not respect convexity.
No interesting intermediate point exists if lmpx and rmpx or lmpy and rmpy are too close. No values would be available for their coordinates.
maximal number of intermediate points
Look for at most for ni intermediate points, but reserve space to add the initial point and (perhaps) the final point.
The first element is the left most point
Effective number of intermediate points
The control structure of this piece of code could be improved by initializing ilmpx[0] and ilmpy[0] right away and by using a while(more_to_find_p) to avoid code replication.
A lower upper bound for v
add the final point to the arrays ilmpx and ilmpy
Process the intermediate points
One constraint generated by (lmpx,lmpy) and (rmpx,rmpy)
Definition at line 995 of file sc_normalize.c.
References assert, build_convex_constraints_from_vertices(), contrainte_make(), find_integer_point_to_the_right(), int, value_min, VALUE_MONE, vect_make_line(), vect_multiply(), and x.
Referenced by small_positive_slope_reduce_coefficients_with_bounding_box().
package sc
Normalization, which include some redundacy elimination include <values.h> Two candidates for arithmetique/value.c, which does not exist, or for value/value.c, which does not exist either.
Definition at line 50 of file sc_normalize.c.
References value_uminus.
Referenced by compute_x_and_y_bounds(), new_constraint_for_coefficient_reduction_with_bounding_box(), and update_coefficient_signs_in_constraints().
|
static |
Compute a normalized version of the constraint v and the corresponding change of basis.
The change of basis is encoded by an integer belonging to the interval [0,7]. Bit 2 is used to encode a change of sign for x, bit 1, a change of sign for y and bit 0 a permutation between x and y.
No new variable x' and y' are introduced. The new constraint is still expressed as a constraint on x and y.
The bounds on x and y must be adapted into bound on x' and y'.
substitute x by x'=-x
FI: could cause an overflow
FI: could cause an overflow
Build a_prime x + b_prime y <= -c
x and y must be exchanged: -b_prime x - a_prime y <= -c
Make sure that nv is properly built...
Definition at line 572 of file sc_normalize.c.
References assert, fprintf(), negate_value_interval(), small_slope_and_first_quadrant_p(), swap_value_intervals(), TCST, value_assign, value_gt, value_neg_p, value_pos_p, value_uminus, VALUE_ZERO, variable_debug_name, vect_add_elem(), vect_coeff(), vect_dump(), VECTEUR_NUL, vecteur_succ, VECTEUR_UNDEFINED_P, vecteur_var, and x.
Referenced by reduce_coefficients_with_bounding_box().
|
static |
If at least one of the coefficients of constraint v == ax+by<=c are greater that the intervals of the bounding box, reduce them to be at most the the size of the intervals.
This is similar to a Gomory cut, but we apply the procedure to 2-D constraints only.
Three steps:
0. Check eligibility: 2-D constraint and either |a|>y_max-y_min or |b|>x_max-x_min. Assume or ensure that gcd(a,b)=1. This step must be performed by the caller.
Beware of overflows if you compute the widths of these intervals...
Perform the reverse change of basis cb on constraints in constraint list ineq
Definition at line 1569 of file sc_normalize.c.
References assert, check_coefficient_reduction(), compute_x_and_y_bounds(), CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, eligible_for_coefficient_reduction_with_bounding_box_p(), fprintf(), new_constraint_for_coefficient_reduction_with_bounding_box(), small_positive_slope_reduce_coefficients_with_bounding_box(), update_coefficient_signs_in_constraints(), VALUE_MAX, VALUE_MIN, variable_debug_name, vect_fprint(), VECTEUR_NUL, and x.
Referenced by sc_bounded_normalization().
Psysteme sc_add_normalize_eq | ( | Psysteme | ps, |
Pcontrainte | eq | ||
) |
Definition at line 2407 of file sc_normalize.c.
References egalite_normalize(), eq, sc_elim_simple_redund_with_eq(), sc_rm(), sc_rm_empty_constraints(), Scontrainte::succ, vect_normalize(), and Scontrainte::vecteur.
Psysteme sc_add_normalize_ineq | ( | Psysteme | ps, |
Pcontrainte | ineq | ||
) |
Definition at line 2435 of file sc_normalize.c.
References inegalite_normalize(), sc_elim_simple_redund_with_ineq(), sc_rm(), sc_rm_empty_constraints(), Scontrainte::succ, vect_normalize(), and Scontrainte::vecteur.
Eliminate trivially redundant integer constraint using a O(n x d^2) algorithm, where n is the number of constraints and d the dimension.
And possibly detect an non feasible constraint system ps. Also, reduce the coefficients of 2-D constraints when possible.
This function must not be used to decide emptyness when checking redundancy with Fourier-Motzkin because this may increase the initial rational convex polyhedron. No integer point is added, but rational points may be added, which may lead to an accuracy loss when a convex hull is performed.
Principle: If two constant vectors, l et u, such that l<=x<=u, where x is the vector representing all variables, then the bound b of any constraint a.x<=b can be compared to a.k where k_i=u_i if a_i is positive, and k_i=l_i elsewhere. The constraint can be eliminated if a.k<=b.
It is not necessary to have upper and lower bounds for all components of x to compute the redundancy condition. It is sufficient to meet the condition:
\forall i s.t. a_i>0 \exists u_i and \forall i s.t. a_i<0 \exists b_i
The complexity is O(n x d) where n is the number of constraints and d the dimension, vs O(n^2 x d^2) for some other normalization functions.
With l and u available, we also use c, the vector containing constant variables. The variables are substituted by their constant values in equations and inequalities.
The normalization is not rational. It assumes that only integer points are relevant. For instance, 2x<=3 is reduced to x<=1. It would be possible to use the same function in rational, but the divisions should be removed, the bounding box would require six vectors, with two new vectors used to keep the variable coefficients, here 2, and the comparisons should be replaced by rational comparisons. Quite a lot of changes, although the general structure would stay the same.
This function was developped to cope successfully with Semantics/type03. The projection performed in transformer_intra_to_inter() explodes without this function.
Note that the upper and lower bounds, u and l, are stored in Pvecteur in an unusual way. The coefficients are used to store the constants.
Note also that constant terms are stored in the lhs in linear, but they are computed here as rhs. In other words, x - 2 <=0 is the internal storage, but the upper bound is 2 as in x<=2.
Note that the simple inequalities used to compute the bounding box cannot be eliminated. Hence, their exact copies are also preserved. Another redundancy test is necessary to get rid of them. They could be eliminated when computing the bounding box if the function updating the bounds returned the information. Note that non feasability cannot be checked because the opposite bound vectors are not passed. If they were, then no simple return code would do. THIS HAS BEEN CHANGED.
The same is true for equations. But the function updating the bounds cannot return directly two pieces of information: the constraint system is empty or the constraint is redundant.
It would be easier to simplify all constraints and then to add the bounding box constraints. Constraints must be normalized initially to avoid destroying useful constraints. For instance, 2i<=99 generates i<=49 whicg proves 21<=99 striclty redundant. THIS HAS BEEN PARTIALLY CHANGED.
Software engineering remarks
This function could be renamed sc_bounded_redundancy_elimination() and be placed into one of the two files, sc_elim_redund.c or sc_elim_simple_redund.c. It just happened that redundancy elimination uses normalization and gdb led me to sc_normalization() when I tried to debug Semantics/type03.c.
This function could be split into three functions, one to compute the bounding box, one to simplify a constraint system according to a bounding box and the third one calling those two, and the coefficient reduction function, which also uses the bounding box.
This split could be useful when projecting a system because the initial bounding box remains valid all along the projection, no matter that happens to the initial constraint. However, the bounding box might be improved with the projections... Since the bounding box computation is fast enough, the function was not split and the transformer (see Linear/C3 Library) projection uses it at each stage. Note that the bouding box may also disappear via overflows and redundancy detection. See for instance the disparition of declaration constraints in convex array regions when the corresponding option is set to true.
Compute the trivial upper and lower bounds for the systeme basis. Since we cannot distinguish between "exist" and "0", we need two extra basis to know if the bound exists or not
can be an equation or an inequality
First look for bounds in equalities, although they may have been exploited otherwise
FI: I do not trust the modulo operator
FI: value_div() instead of value_pdiv(); reason?
ps is empty with two contradictory equations supposedly trapped earlier
Secondly look for bounds in inequalities
This normalization is necessary in case a division is involved, or a useful constraint may be removed. For instance 2*i<=99 generates i<=49 which make 2*i<=99 strictly redundant.
The variable is bounded by zero
upper bound
lower bound
FI: I not too sure how div and pdiv operate nor on what I need here... This explains why the divisions are replicated after the test on the sign of the coefficient.
upper bound
lower bound
Check that the bounding box is not empty because a lower bound is strictly greater than the corresponding upper bound. This could be checked above each time a new bound is defined or redefined. Also, build the constant base, cb
The upper and lower bounds should be printed here for debug
Impression par intervalle, avec verification l<=u quand l et u sont tous les deux disponibles
lower>upper
Simplify equalities using cb and l
Check inequalities for redundancy with respect to ub and lb, if ub and lb contain a minum of information. Also simplify constraints using cb when possible.
new lower bound: useful to check feasiblity
new upper bound
old bound
a lower bound cannot be estimated
the bounding box does not contain enough information to check redundancy with the upper bound
Try to compute the bounds nub and nlb implied by the bounding box
I assume the constraint to be consistent with only one coefficient per dimension
move the bound to the right hand side of the inequality
an upper bound of var is needed
the value macro should be used
c<0 : a lower bound is needed for var
If the new bound nub is tighter, nub <= ob, ob-nub >= 0
Do not destroy the constraints defining the bounding box
The constraint eq is redundant
Preserve this constraint
The new estimated lower bound must be less than the upper bound of the constraint, or the system is empty.
the estimated lower bound, nlb, must be less or equal to the effective upper bound ob: nlb <= ob, 0<=ob-nlb
if ob==nlb, an equation has been detected but it is hard to exploit here
to have a nice breakpoint location
Try to reduce coefficients of 2-D constraints when one variable belongs to an interval.
Remove constraint v
Add the new constraints to the new constraint list, ncl
add the new constraint list to the system
Free all elements of the bounding box
Definition at line 1767 of file sc_normalize.c.
References abort, add_bounding_box_constraints(), assert, base_dimension, BASE_NULLE, contrainte_append(), contrainte_normalize(), contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, cyclic_constraint_list_p(), egalite_normalize(), eligible_for_coefficient_reduction_with_bounding_box_p(), eq, eq_set_vect_nul(), fprintf(), inegalite_normalize(), inegalites_dump(), modulo, reduce_coefficients_with_bounding_box(), sc_add_inegalites(), sc_consistent_p(), sc_elim_empty_constraints(), sc_empty(), sc_rm(), simplify_constraint_with_bounding_box(), TCST, update_lower_and_upper_bounds(), update_lower_or_upper_bound(), value_addto, value_assign, value_div, value_minus, value_mult, value_notzero_p, VALUE_ONE, value_pdiv, value_pos_p, value_posz_p, value_uminus, VALUE_ZERO, value_zero_p, variable_debug_name, vect_add_elem(), vect_coeff(), vect_dump(), vect_rm(), vect_size(), VECTEUR_NUL, VECTEUR_NUL_P, vecteur_succ, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by sc_normalize(), transformer_normalize(), and transformer_projection_with_redundancy_elimination_and_check().
void sc_gcd_normalize | ( | Psysteme | ps | ) |
sc_gcd_normalize(ps)
Normalization by gcd's of equalities and inequalities
Normalization by gcd's
Definition at line 3337 of file sc_normalize.c.
References contrainte_normalize(), Ssysteme::egalites, Ssysteme::inegalites, Scontrainte::succ, vect_normalize(), and Scontrainte::vecteur.
Referenced by internal_sc_feasibility(), and sc_fourier_motzkin_feasibility_ofl_ctrl().
Psysteme sc_normalize(Psysteme ps): normalisation d'un systeme d'equation et d'inequations lineaires en nombres entiers ps, en place.
Normalisation de chaque contrainte, i.e. division par le pgcd des coefficients (cf. ?!? )
Verification de la non redondance de chaque contrainte avec les autres:
Pour les egalites, on elimine une equation si on a un systeme d'egalites de la forme :
a1/ Ax - b == 0, ou b1/ Ax - b == 0, Ax - b == 0, b - Ax == 0,
ou c1/ 0 == 0
Pour les inegalites, on elimine une inequation si on a un systeme de contraintes de la forme :
a2/ Ax - b <= c, ou b2/ 0 <= const (avec const >=0) Ax - b <= c
ou c2/ Ax == b, Ax <= c avec b <= c,
ou d2/ Ax <= b, Ax <= c avec c >= b ou b >= c
Il manque une elimination de redondance particuliere pour traiter les booleens. Si on a deux vecteurs constants, l et u, tels que l<=x<=u, alors la borne b de n'importe quelle contrainte a.x<=b peut etre comparee a a.k ou k_i=u_i si a_i est positif et k_i=l_i sinon. La contrainte a peut etre eliminee si a.k <= b. Si des composantes de x n'aparaissent dans aucune contrainte, on ne dispose en consequence pas de bornes, mais ca n'a aucune importance. On veut donc avoir une condition pour chaque contrainte: forall i s.t. a.i!=0 \exists l_i and b_i s.t. l_i<=x_i<=b_i. Voir sc_bounded_normalization().
sc_normalize retourne NULL quand la normalisation a montre que le systeme etait non faisable
BC: now returns sc_empty when not feasible to avoid unecessary copy_base in caller.
FI: should check the input for sc_empty_p()
I do not want to disturb every pass of Linear/C3 Library that uses directly or indirectly sc_normalize. Since sc_bounded_normalization() has been developped specifically for transformer_projection(), it is called directly from the function implementing transformer_projection(). But it is not sufficient for type03.
FI: this takes (a lot of) time but I do not know why: O(n^2)?
normalisation de chaque equation
FI: piece of code that will appear in many places... How can we call it: empty_sc()? sc_make_empty()? sc_to_empty()?
Definition at line 2152 of file sc_normalize.c.
References BASE_UNDEFINED, egalite_normalize(), Ssysteme::egalites, eq, inegalite_normalize(), Ssysteme::inegalites, sc_bounded_normalization(), sc_elim_empty_constraints(), sc_elim_simple_redund_with_eq(), sc_elim_simple_redund_with_ineq(), sc_empty(), sc_empty_p(), sc_rm(), sc_rn_p(), sc_safe_kill_db_eg(), Scontrainte::succ, vect_normalize(), and Scontrainte::vecteur.
Referenced by broadcast_of_dataflow(), build_list_of_min(), build_sc_nredund_2pass_ofl_ctrl(), build_third_comb(), cutting_conditions(), dataflows_on_reference(), dependence_cone_positive(), find_implicit_equation(), include_trans_on_LC_in_ref(), main(), make_scanning_over_tiles(), movement_computation(), new_system_with_only_live_variable(), nullify_factors(), pa_intersect_system(), parallel_tiling(), plc_elim_var_with_eg(), plint(), prepare_reindexing(), sc_build_triang_elim_redund(), sc_faisabilite_optim(), sc_fm_project_variables(), sc_minmax_of_variable(), sc_minmax_of_variable2(), sc_minmax_of_variable_optim(), sc_of_constrs(), sc_projection_concat_proj_on_variables(), sc_projection_optim_along_vecteur_ofl(), sc_resol_smith(), sc_safe_normalize(), sc_strong_normalize2(), sc_strong_normalize4(), sc_strong_normalize_and_check_feasibility(), sc_strong_normalize_and_check_feasibility2(), sc_supress_parallel_redund_constraints(), sc_supress_same_constraints(), sc_triang_elim_redund(), separate_variables(), separate_variables_2(), set_dimensions_of_local_variable_family(), smith_int(), sys_int_redond(), syst_smith(), TestDependence(), tiling_transformation(), and valuer().
Psysteme sc_normalize2(Psysteme ps): normalisation d'un systeme d'equation et d'inequations lineaires en nombres entiers ps, en place.
Normalisation de chaque contrainte, i.e. division par le pgcd des coefficients (cf. ?!? )
Propagation des constantes definies par les equations dans les inequations. E.g. N==1.
Selection des variables de rang inferieur quand il y a ambiguite: N==M. M is used wherever possible.
Selection des variables eliminables exactement. E.g. N==4M. N is substituted by 4M wherever possible. Ceci permet de raffiner les constantes dans les inegalites.
Les equations de trois variables ou plus ne sont pas utilisees pour ne pas rendre les inegalites trop complexes.
Verification de la non redondance de chaque contrainte avec les autres.
Les contraintes sont normalisees par leurs PGCDs. Les constantes sont propagees dans les inegalites. Les paires de variables equivalentes sont propagees dans les inegalites en utilisant la variable de moindre rang dans la base.
Pour les egalites, on elimine une equation si on a un systeme d'egalites de la forme :
a1/ Ax - b == 0, ou b1/ Ax - b == 0,
Ax - b == 0, b - Ax == 0,
ou c1/ 0 == 0
Si on finit avec b==0, la non-faisabilite est detectee.
Pour les inegalites, on elimine une inequation si on a un systeme de contraintes de la forme :
a2/ Ax - b <= c, ou b2/ 0 <= const (avec const >=0) Ax - b <= c
ou c2/ Ax == b,
Ax <= c avec b <= c,
ou d2/ Ax <= b, Ax <= c avec c >= b ou b >= c
Les doubles inegalites syntaxiquement equivalentes a une egalite sont detectees: Ax <= b, Ax >= b
Si deux inegalites sont incompatibles, la non-faisabilite est detectee: b <= Ax <= c et c < b.
sc_normalize retourne NULL/SC_EMPTY quand la normalisation a montre que le systeme etait non faisable.
Une grande partie du travail est effectue dans sc_elim_db_constraints()
FI: a revoir de pres; devrait retourner SC_EMPTY en cas de non faisabilite
Eliminate variables linked by a two-term equation. Preserve integer information or choose variable with minimal rank in basis b if some ambiguity exists.
Then, after normalization, a1 and a2 must be one
An overflow is unlikely... but it should be handled here I guess rather than be subcontracted?
The substitution of the variable defined by "eq" by its value leads to an overflow in one some unknown constraint of "ps". It might be better to trap the overflow at a lower level, when you know which constraint fails because the constraint could be removed altogether.
Propagate constant definitions, only once although a triangular system might require n steps is the equations are in the worse order
An overflow is unlikely... but it should be handled here I guess rather than be subcontracted.
The substitution of the variable defined by "eq" by its value leads to an overflow in one some unknown constraint of "ps". It might be better to trap the overflow at a lower level, when you know which constraint fails because the constraint could be removed altogether.
Definition at line 2274 of file sc_normalize.c.
References CATCH, contrainte_vecteur, Ssysteme::egalites, eq, make_base_from_vect(), OFL_CTRL, overflow_error, rank_of_variable(), sc_copy(), sc_elim_double_constraints(), sc_elim_empty_constraints(), sc_rm(), Scontrainte::succ, TCST, term_cst, TRY, UNCATCH, value_abs, value_mod, value_mone_p, value_one_p, VALUE_ZERO, VARIABLE_DEFINED_P, VARIABLE_UNDEFINED, vect_coeff(), vect_size(), vecteur_succ, vecteur_val, and vecteur_var.
Referenced by effects_to_dma(), transformer_combine(), and transformer_normalize().
Definition at line 2476 of file sc_normalize.c.
References OFL_CTRL, sc_rational_feasibility_ofl_ctrl(), and sc_rm().
Referenced by sc_strong_normalize3(), and sc_strong_normalize5().
Psysteme sc_safe_normalize(Psysteme ps) output : ps, normalized.
modifies : ps. comment : when ps is not feasible, returns sc_empty.
Definition at line 2468 of file sc_normalize.c.
References sc_normalize().
Referenced by array_must_fully_written_by_regions_p(), precondition_intra_to_inter(), transformer_projection(), and transformer_temporary_value_projection().
Psysteme sc_strong_normalize(Psysteme ps)
Apply sc_normalize first. Then solve the equations in a copy of ps and propagate in equations and inequations.
Flag as redundant equations 0 == 0 and inequalities 0 <= k with k a positive integer constant when they appear.
Flag the system as non feasible if any equation 0 == k or any inequality 0 <= -k with k a strictly positive constant appears.
Then, we'll have to deal with remaining inequalities...
Argument ps is not modified by side-effect but it is freed for backward compatability. SC_EMPTY is returned for backward compatability.
The code is difficult to understand because a sparse representation is used. proj_ps is initially an exact copy of ps, with the same constraints in the same order. The one-to-one relationship between constraints must be maintained when proj_ps is modified. This makes it impossible to use most routines available in Linear.
Note: this is a redundancy elimination algorithm a bit too strong for sc_normalize.c...
Definition at line 2512 of file sc_normalize.c.
References sc_strong_normalize_and_check_feasibility().
Referenced by transformer_normalize().
Psysteme sc_strong_normalize2(Psysteme ps)
Apply sc_normalize first. Then solve the equations in ps and propagate substitutions in equations and inequations.
Flag as redundant equations 0 == 0 and inequalities 0 <= k with k a positive integer constant when they appear.
Flag the system as non feasible if any equation 0 == k or any inequality 0 <= -k with k a strictly positive constant appears.
Then, we'll have to deal with remaining inequalities...
Argument ps is modified by side-effect. SC_EMPTY is returned for backward compatability if ps is not feasible.
Note: this is a redundancy elimination algorithm a bit too strong for sc_normalize.c... but it's not strong enough to qualify as a normalization procedure.
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
CA
Solve the equalities
eq might suffer in the substitution...
eq is redundant
keep eq
use eq to eliminate a variable
Let's use a variable with coefficient 1 if possible
A softer substitution is used
eq itself is going to be modified in ps. use a copy!
The system is not feasible. Stop
Check the inequalities
copy projected inequalities left in ps
sc_base(ps) = BASE_UNDEFINED;
Definition at line 2825 of file sc_normalize.c.
References assert, base_copy(), base_rm, CATCH, contrainte_copy(), CONTRAINTE_NULLE_P, contrainte_rm, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, egalite_normalize(), eq, fprintf(), if_debug_sc_strong_normalize_2, new_eq(), NO_OFL_CTRL, overflow_error, sc_add_egalite(), sc_copy(), sc_default_dump(), sc_make(), sc_normalize(), sc_rm(), sc_safe_append(), sc_weak_consistent_p(), TCST, term_cst, TRY, UNCATCH, value_one_p, VECTEUR_NUL_P, vecteur_succ, vecteur_val, and vecteur_var.
Referenced by expression_less_than_in_context(), and transformer_normalize().
Definition at line 2521 of file sc_normalize.c.
References sc_rational_feasibility(), and sc_strong_normalize_and_check_feasibility().
Referenced by transformer_normalize().
Psysteme sc_strong_normalize4(Psysteme ps, char * (*variable_name)(Variable))
Definition at line 3013 of file sc_normalize.c.
References sc_normalize(), sc_strong_normalize_and_check_feasibility2(), and variable_name().
Referenced by transformer_empty_p(), and transformer_normalize().
Good, but pretty slow
Definition at line 3028 of file sc_normalize.c.
References sc_rational_feasibility(), sc_strong_normalize_and_check_feasibility2(), and variable_name().
Referenced by check_range_wrt_precondition(), transformer_normalize(), and transformer_strongly_empty_p().
Psysteme sc_strong_normalize_and_check_feasibility | ( | volatile Psysteme | ps, |
Psysteme(*)(Psysteme) | check_feasibility | ||
) |
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
CA
We need an exact copy of ps to have equalities and inequalities in the very same order
FI: may have is has been fixed with sc_dup() by now... see comments in sc_copy()
Solve the equalities
proj_eq might suffer in the substitution...
eq is redundant
keep eq
use proj_eq to eliminate a variable
Let's use a variable with coefficient 1 if possible
A softer substitution is needed in order to preserve the relationship between ps and proj_ps
proj_eq itself is going to be modified in proj_ps. use a copy!
The system is not feasible. Stop
Check the inequalities
ineq is redundant
keep ineq
ineq is redundant with another inequality: destroy ineq to avoid the mutual elimination of two identical constraints
The system is not feasible. Stop
Check redundancy between residual inequalities
sc_elim_simple_redund_with_ineq(ps,ineg)
Well, sc_normalize should not be able to do much here!
FI: test added for breakpoint placement
Definition at line 2535 of file sc_normalize.c.
References assert, BASE_NULLE, BASE_UNDEFINED, CATCH, contrainte_constante_p(), contrainte_copy(), CONTRAINTE_NULLE_P, contrainte_rm, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, contrainte_verifiee(), egalite_normalize(), eq, eq_set_vect_nul(), fprintf(), inegalite_normalize(), new_eq(), NO_OFL_CTRL, overflow_error, sc_add_egalite(), sc_add_inegalite(), sc_check_inequality_redundancy(), sc_copy(), sc_empty(), sc_make(), sc_normalize(), sc_rm(), sc_weak_consistent_p(), TCST, term_cst, TRY, UNCATCH, value_one_p, VECTEUR_NUL_P, vecteur_succ, vecteur_val, and vecteur_var.
Referenced by sc_strong_normalize(), and sc_strong_normalize3().
Psysteme sc_strong_normalize_and_check_feasibility2 | ( | volatile Psysteme | ps, |
Psysteme(*)(Psysteme) | check_feasibility, | ||
char *(*)(Variable) | variable_name, | ||
int | level | ||
) |
Psysteme sc_strong_normalize_and_check_feasibility2 (Psysteme ps, Psysteme (*check_feasibility)(Psysteme), char * (*variable_name)(Variable), int level)
Same as sc_strong_normalize2() but equations are used by increasing order of their numbers of variables, and, within one equation, the lexicographic minimal variables is chosen among equivalent variables.
Equations with more than "level" variables are not used for the substitution. Unless level==VALUE_MAX.
Finally, an additional normalization procedure is applied on the substituted system. Another stronger normalization can be chosen to benefit from the system size reduction (e.g. sc_elim_redund). Or a light one to benefit from the inequality simplifications due to equation solving (e.g. sc_normalize).
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
CA
Solve the equalities (if any)
Start with equalities with the smallest number of variables and stop when all equalities have been used and or when all equalities left have too many variables.
&& sc_nbre_egalites(ps) != 0
eq might suffer in the substitution...
eq is redundant
Equalities change because of substitutions. Their dimensions may go under the present required dimension, nvar. Hence the non-equality test.
keep eq
use eq to eliminate a variable
Let's use a variable with coefficient 1 if possible. Among such variables, choose the lexicographically minimal one.
v1 = TCST;
because of the !CONTRAINTE_NULLE_P() test
eq itself is going to be modified in ps. use a copy!
too early to use this equation eq
If there any hope to use it in the future? Yes, if its dimension is no more than nvar+1 because one of its variable might be substituted. If more variable are substituted, it's dimension is going to go down and it will be counted later... Well this is not true, it will be lost:-(
to be on the safe side till I find a better idea...
The system is not feasible. Stop
This reaaly generates a lot of about on real life system!
This is a much too much expensive transformation in an innermost loop!
It cannot be used as a convergence test.
feasible_p = (!SC_EMPTY_P(ps = sc_normalize(ps)));
Check the inequalities
copy projected inequalities left in ps
sc_base(ps) = BASE_UNDEFINED;
assert(sc_weak_consistent_p(new_ps));
Definition at line 3064 of file sc_normalize.c.
References assert, base_copy(), base_rm, CATCH, contrainte_copy(), CONTRAINTE_NULLE_P, contrainte_rm, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, egalite_normalize(), eq, fprintf(), if_debug_sc_strong_normalize_and_check_feasibility2, level, new_eq(), NO_OFL_CTRL, overflow_error, sc_add_egalite(), sc_copy(), sc_default_dump(), sc_elim_empty_constraints(), sc_make(), sc_normalize(), sc_rm(), sc_safe_append(), sc_weak_consistent_p(), TCST, term_cst, TRY, UNCATCH, value_one_p, variable_name(), vect_dimension(), VECTEUR_NUL_P, vecteur_succ, vecteur_val, and vecteur_var.
Referenced by sc_strong_normalize4(), and sc_strong_normalize5().
|
static |
Use constants imposed by the bounding box to eliminate constant terms from constraint eq.
Unless this is the constraint defining the bounding box? Destroy it any way to remove redundancy and expect the bounding box contraints to be added later.
Constant variables are defined by basis cb and their value are found in l (See description of bounding box above).
Substitute constant variables, computing a delta value to be added to the constant term and setting the variable coefficient to zero; we should have not only lb and ub but also cb, the base for the constant terms
We could check here if var has a constant value and eliminate it from the constraint v... if this did not break the surrounding loop on v... So the update is accumulated into a difference vector dv that is added to v at the end of the loop
We should update here the constant term with delta, the value accumulated with the constant terms
is_inequality_p &&
do not destroy this equation by simplification if it defines a constant...
For debugging: init_variable_debug_name(entity_local_name)
Definition at line 251 of file sc_normalize.c.
References contrainte_vecteur, eq, fprintf(), TCST, value_direct_multiply, value_notzero_p, value_uminus, value_zero_p, vect_add(), vect_add_elem(), vect_coeff(), vect_dump(), vect_rm(), vect_size(), VECTEUR_NUL, VECTEUR_NUL_P, vecteur_succ, vecteur_val, and vecteur_var.
Referenced by sc_bounded_normalization().
|
static |
Replace 2-D constraint v by a set of constraints when possible because variable x is bounded by [x_min,x_max].
The set of constraints contains one, two or three new constraints.
The slope of constraint v wrt variable x is in interval ]0,1[. On other words, if v is interpreted as a x + b y + c <=0, a is negative and b is greater than -a. Also b is greater than |low-up|. All these constraints have been checked earlier.
Retrieve coefficients and variables in v = ax+by+c
Compute two integer vertices for x_min and x_max using constraint ax+by+c=0, y = (- c - ax)/b
Reminder: the slope is positive, the function is increasing and y_x_min and y_x_max are upper bounds
x must be bounded, but y bounds are useless; they simply make the resolution more complex
In case, both x and y are bounded we think it useful to take advantage of the interval product
Compute two integer vertices for y_min and y_max using constraint ax+by+c=0, x = (- c - by)/a
The constraint ax+by+c=0 has at most two valid intersections with the bounding box. Because the slope is positive, 0<-a/b<1, the minimum point is obtained with x_min or y_min and the maximum point is obtained with x_max or y_max.
Constraint redundant with the bounding box should have been eliminated earlier with a simpler technique.
The constraint is a redundant tangent
The change of coordinates was meaningful when bounding both x and y
One new horizontal constraint defined by the two vertices lmp and rmp: y<=lmpy; test case slope01.c
Two constraints defined by (lmp,lrmp) and (lrmp, rmp). test case slope02.c
Only one constraint defined by : test case slope03.c
The slope is sufficiently large to find up to three constraints: look for the leftmost and rightmost integer points between (lmpx, lmpy) and (rmpx,rmpy) that meet v and are above nv, the line between (lmpx,lmpy) and (rmpx,rmpy). Let them be (ilmpx, ilmpy) and (irmpx, irmpy).
If ilmpx>irmpx, on constraint is enough, nv, because no intermediate points exist.
If ilmpx=irmpx, two constraints are necessary and they are defined by the two couples of points ((lmpx,lmpy),(ilmpx, ilmpy) and ((irmpx, irmpy), (rmpx, rmpy)).
Else ilmpx<irmpx, three constraints are necessary and they are defined by the segments delimited by the four points, (lmpx, lmpy), (ilmpx, ilmpy), (irmpx, irmpy) and (rmpx,rmpy). Only if no new intermediate point exists between the two intermediate points.
Test case: slope04.c
Default option
Definition at line 1205 of file sc_normalize.c.
References assert, contrainte_make(), contrainte_succ, CONTRAINTE_UNDEFINED, find_intermediate_constraints_recursively(), fprintf(), TCST, value_eq, value_ge, value_gt, value_le, value_lt, VALUE_MAX, VALUE_MIN, value_minus, VALUE_MONE, value_mult, value_ne, VALUE_ONE, value_pdiv, value_plus, value_uminus, VALUE_ZERO, variable_debug_name, vect_add_elem(), vect_coeff(), vect_copy(), vect_fprint(), vect_make(), vect_make_line(), vect_multiply(), VECTEUR_NUL, vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_var, and x.
Referenced by reduce_coefficients_with_bounding_box().
Check that the coefficients on the first and second variables, x and y, define a increasing line.
With a slope less than one? Used to be a condition, but was lifted.
Internal check used after a change of frame.
Note: dangerous use of term ordering inside a linear sparse vector.
Should work, although inefficiently for large slopes.
Definition at line 531 of file sc_normalize.c.
References TCST, value_gt, value_neg_p, value_notzero_p, value_pos_p, value_uminus, VALUE_ZERO, value_zero_p, vect_coeff(), vect_size(), vecteur_succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by new_constraint_for_coefficient_reduction_with_bounding_box().
|
static |
Definition at line 64 of file sc_normalize.c.
References swap_values().
Referenced by new_constraint_for_coefficient_reduction_with_bounding_box().
Definition at line 57 of file sc_normalize.c.
Referenced by swap_value_intervals().
|
static |
Perform the inverse change of basis and update the intervals for later checks.
Definition at line 1444 of file sc_normalize.c.
References contrainte_succ, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, eq, negate_value_interval(), update_coefficient_signs_in_vector(), and x.
Referenced by reduce_coefficients_with_bounding_box().
|
static |
Perform a reverse change of base to go back into the source code frame.
Definition at line 1429 of file sc_normalize.c.
References value_uminus, vect_chg_coeff(), vect_coeff(), and x.
Referenced by update_coefficient_signs_in_constraints().
|
static |
Updates upper and lower bounds, (ubound_p, ubound_base_p) and (lbound_p, lbound_base_p), with equations var==nb.
Do not test for nb==0. This would increase the code size a lot for a very limited benefit.
This function returns a boolean to signal an empy interval, i.e. a non-feasible system.
Auxiliary function of sc_bounded_normalization() new bound
Some constraint like 0==0, i.e. the NULL vector, or 0==3 an impossible constraint
Update the upper bound
A pre-existing upper bound exists
The new bound nb is stricter and consistent with the preexisting upper bound
ignore the non feasability
but maintain consistency to avoid a later abort
Update the lower bound, almost identical, but for the compatibility check
A lower bound has already been defined
The new bound nb is stricter and consistent with the preexisting lower bound
ps is empty with contradictory equations and inequalities supposedly trapped earlier
ignore the non feasability
but maintain consistency to avoid a later abort
Definition at line 169 of file sc_normalize.c.
References abort, base_add_dimension, TCST, value_eq, value_gt, value_lt, value_minus, value_zero_p, vect_add_elem(), and vect_coeff().
Referenced by sc_bounded_normalization().
|
static |
Bounding box (not really a box most of the time)
The bounding box is made of all 1-D constraints found in a constraint system and is represented by five vectors ub, lb, cb, u and l.
The function sc_bounded_normalization() and the function reduce_coefficients_with_bounding_box() both rely on numerical bounds l and b for vector x, such that l<=x<=b.
However, lower and upper bounds are not always available for all components x_i of x. And 0 is a perfectly valid bound, that is not represented with linear sparse vector representation. Hence, the bound information cannot be carried by only two vectors. Four vectors are used, two basis vectors, lb and ub, used to specifiy if a bound is available, and two vectors l and b to contain the bounds.
Note that l and u are not usual vectors. The constant bounds appear as variable coefficients. For instance, l=2u+3v, together with lb=u+v+w, means that the lower bounds for x_u, x_v and x_w are 2, 3 and 0.
When the lower and upper bounds are known and equal, another base vector, cb, is introduced to flag the constants.
FI: I do not want to introduce a new data structure to represent a bounding box, and I do not like the idea of keeping independently five vectors...
However, I could not think of a simple data structure to store the bounding box as a unique object. With more variables, it would be better to use hash tables to link variables to their lower and upper bound and to their value when they are constant. Hence the use of four sparse vectors as explained above. Auxiliary functions for sc_bounded_normalization(): build the bounding box
Update bound information for variable var. A lower or upper bound_p and bound_base_p must be passer regardless of lower_p. lower_p is only used to know how to tighten the bound if it is already defined. The information to use is:
lower_p? var <= nb : var>=nb
It is not possible to detect an empty system here because information on both bounds is not available simultaneously. lb, l, ub and u should all be passed for the check.
A bound is already known. It must be updated if the new one is better.
previous bound
bigger is better
update bound
The current constraint is redundant
smaller is better
update bound
The current constraint is redundant
No bound is known yet
lower_p | new bound |
Definition at line 122 of file sc_normalize.c.
References base_add_dimension, bound_p, value_minus, vect_add_elem(), and vect_coeff().
Referenced by sc_bounded_normalization().
|
static |
FI: Could be moved in vecteur library...
Compute the equation of the line joining (x0,y0) and (x1,y1)
(x1-x0) y = (y1 -y0) (x - x0) + y0 (x1-x0)
as ax+by+c=0, where a, b and c are prime together.
constant term: -x0 dy + y0 dx
Definition at line 671 of file sc_normalize.c.
References assert, TCST, value_minus, value_mult, vect_add_elem(), vect_new(), vect_normalize(), and x.
Referenced by build_convex_constraints_from_vertices(), find_intermediate_constraints(), find_intermediate_constraints_recursively(), and small_positive_slope_reduce_coefficients_with_bounding_box().