PIPS
|
#include <stdio.h>
#include <stdlib.h>
#include "linear_assert.h"
#include "boolean.h"
#include "arithmetique.h"
#include "vecteur.h"
#include "contrainte.h"
Go to the source code of this file.
Functions | |
int | contrainte_subst_ofl (Variable v, Pcontrainte def, Pcontrainte c, bool eq_p) |
package contrainte - operations binaires More... | |
int | contrainte_subst (Variable v, Pcontrainte def, Pcontrainte c, bool eq_p) |
Pcontrainte | contrainte_substitute_dimension (Pcontrainte e, Variable i, Pvecteur v) |
Pcontrainte | inegalite_comb (Pcontrainte posit, Pcontrainte negat, Variable v) |
Pcontrainte | inegalite_comb_ofl (Pcontrainte posit, Pcontrainte negat, Variable v) |
int | contrainte_subst_ofl_ctrl (Variable v, Pcontrainte def, Pcontrainte c, bool eq_p, int ofl_ctrl) |
int contrainte_subst_ofl_ctrl(Variable v, Pcontrainte def, Pcontrainte c Boolean eq_p, int ofl_ctrl): elimination d'une variable v entre une equation def et une contrainte, egalite ou inegalite, c. More... | |
Pcontrainte | inegalite_comb_ofl_ctrl (Pcontrainte posit, Pcontrainte negat, Variable v, int ofl_ctrl) |
Pcontrainte inegalite_comb_ofl_ctrl(Pcontrainte posit, Pcontrainte negat, Variable v, int ofl_ctrl): combinaison lineaire positive des deux inegalites posit et negat eliminant la variable v. More... | |
Value | eq_diff_const (Pcontrainte c1, Pcontrainte c2) |
Value eq_diff_const(Pcontrainte c1, Pcontrainte c2): calcul de la difference des deux termes constants des deux equations c1 et c2. More... | |
Value | eq_sum_const (Pcontrainte c1, Pcontrainte c2) |
Value eq_sum_const(Pcontrainte c1, Pcontrainte c2): calcul de la somme des deux termes constants des deux contraintes c1 et c2. More... | |
Pcontrainte | contrainte_append (Pcontrainte c1, Pcontrainte c2) |
Pcontrainte contrainte_append(c1, c2) Pcontrainte c1, c2;. More... | |
Pcontrainte | extract_common_constraints (Pcontrainte *pc1, Pcontrainte *pc2, bool eq) |
common (simply equal) contraints are extracted, whether equalities or inequalities. More... | |
Pcontrainte contrainte_append | ( | Pcontrainte | c1, |
Pcontrainte | c2 | ||
) |
Pcontrainte contrainte_append(c1, c2) Pcontrainte c1, c2;.
append directly c2 to c1. Neither c1 nor c2 are relevant when the result is returned.
c1 | 1 |
c2 | 2 |
Definition at line 267 of file binaires.c.
References Scontrainte::succ.
Referenced by algorithm_row_echelon_generic(), and sc_bounded_normalization().
int contrainte_subst | ( | Variable | v, |
Pcontrainte | def, | ||
Pcontrainte | c, | ||
bool | eq_p | ||
) |
def | ef |
eq_p | q_p |
Definition at line 48 of file binaires.c.
References contrainte_subst_ofl_ctrl(), and NO_OFL_CTRL.
int contrainte_subst_ofl | ( | Variable | v, |
Pcontrainte | def, | ||
Pcontrainte | c, | ||
bool | eq_p | ||
) |
package contrainte - operations binaires
binaires.c
def | ef |
eq_p | q_p |
Definition at line 40 of file binaires.c.
References contrainte_subst_ofl_ctrl(), and FWD_OFL_CTRL.
int contrainte_subst_ofl_ctrl | ( | Variable | v, |
Pcontrainte | def, | ||
Pcontrainte | c, | ||
bool | eq_p, | ||
int | ofl_ctrl | ||
) |
int contrainte_subst_ofl_ctrl(Variable v, Pcontrainte def, Pcontrainte c
Boolean eq_p, int ofl_ctrl): elimination d'une variable v entre une equation def et une contrainte, egalite ou inegalite, c.
La contrainte c est modifiee en substituant v par sa valeur impliquee par def.
La contrainte c est interpretee comme une inegalite et la valeur retournee vaut: -1 si la contrainte c est trivialement verifiee et peut etre eliminee 0 si la contrainte c est trivialement impossible 1 sinon (tout va bien) Si la contrainte c passee en argument etait trivialement impossible ou trivialement verifiee, aucune subsitution n'a lieu et la valeur 1 est retournee.
La substitution d'une variable dans une inegalite peut aussi introduire une non-faisabilite testable par calcul de PGCD, mais cela n'est pas fait puisqu'on ne sait pas si c est une egalite ou une inegalite. Le traitement du terme constant n'est pas decidable.
Note: il faudrait separer le probleme de la combinaison lineaire a coefficients positifs de celui de la faisabilite et de la trivialite
Le controle de l'overflow est effectue et traite par le retour du contexte correspondant au dernier CATCH(overflow_error) effectue.
cv_def = coeff de v dans def
cv_c = coeff de v dans c
il faut que cv_def soit non nul pour que la variable v puisse etre eliminee
il n'y a rien a faire si la variable v n'apparait pas dans la contrainte c
substitution inutile: variable v absente
on garde trace de la valeur de c avant substitution pour pouvoir la desallouer apres le calcul de la nouvelle
on ne fait pas de distinction entre egalites et inegalites, mais on prend soin de toujours multiplier la contrainte, inegalite potentielle, par un coefficient positif
reste malikien: cette partie ne peut pas etre faite sans savoir si on est en train de traiter une egalite ou une inegalite
=> eliminer cette c inutile
=> systeme non faisable
def | ef |
eq_p | q_p |
ofl_ctrl | fl_ctrl |
Definition at line 107 of file binaires.c.
References assert, contrainte_constante_p(), contrainte_verifiee(), value_neg_p, value_notzero_p, value_uminus, value_zero_p, vect_cl2_ofl_ctrl(), vect_coeff(), vect_rm(), and Scontrainte::vecteur.
Referenced by better_elim_var_with_eg(), contrainte_subst(), contrainte_subst_ofl(), and new_elim_var_with_eg().
Pcontrainte contrainte_substitute_dimension | ( | Pcontrainte | e, |
Variable | i, | ||
Pvecteur | v | ||
) |
Definition at line 57 of file binaires.c.
References contrainte_vecteur, and vect_substitute_dimension().
Referenced by sc_substitute_dimension().
Value eq_diff_const | ( | Pcontrainte | c1, |
Pcontrainte | c2 | ||
) |
Value eq_diff_const(Pcontrainte c1, Pcontrainte c2): calcul de la difference des deux termes constants des deux equations c1 et c2.
Notes:
Modifications:
c1 | 1 |
c2 | 2 |
Definition at line 218 of file binaires.c.
References b1, b2, TCST, value_minus, value_uminus, VALUE_ZERO, and vect_coeff().
Referenced by sc_check_inequality_redundancy(), sc_elim_simple_redund_with_eq(), and sc_elim_simple_redund_with_ineq().
Value eq_sum_const | ( | Pcontrainte | c1, |
Pcontrainte | c2 | ||
) |
Value eq_sum_const(Pcontrainte c1, Pcontrainte c2): calcul de la somme des deux termes constants des deux contraintes c1 et c2.
Notes:
c1 | 1 |
c2 | 2 |
Definition at line 243 of file binaires.c.
References b1, b2, TCST, value_plus, VALUE_ZERO, and vect_coeff().
Referenced by sc_check_inequality_redundancy().
Pcontrainte extract_common_constraints | ( | Pcontrainte * | pc1, |
Pcontrainte * | pc2, | ||
bool | eq | ||
) |
common (simply equal) contraints are extracted, whether equalities or inequalities.
returns the common extracted constaints. WARNING: *pc1 and *pc2 are modified.
common!
link to result.
clean
get to next.
pc1 | c1 |
pc2 | c2 |
eq | q |
Definition at line 285 of file binaires.c.
References contrainte_equal(), contrainte_free(), CONTRAINTE_UNDEFINED, egalite_equal(), eq, and Scontrainte::succ.
Referenced by extract_common_syst().
Pcontrainte inegalite_comb | ( | Pcontrainte | posit, |
Pcontrainte | negat, | ||
Variable | v | ||
) |
posit | osit |
negat | egat |
Definition at line 65 of file binaires.c.
References inegalite_comb_ofl_ctrl(), and NO_OFL_CTRL.
Pcontrainte inegalite_comb_ofl | ( | Pcontrainte | posit, |
Pcontrainte | negat, | ||
Variable | v | ||
) |
posit | osit |
negat | egat |
Definition at line 72 of file binaires.c.
References FWD_OFL_CTRL, and inegalite_comb_ofl_ctrl().
Pcontrainte inegalite_comb_ofl_ctrl | ( | Pcontrainte | posit, |
Pcontrainte | negat, | ||
Variable | v, | ||
int | ofl_ctrl | ||
) |
Pcontrainte inegalite_comb_ofl_ctrl(Pcontrainte posit, Pcontrainte negat, Variable v, int ofl_ctrl): combinaison lineaire positive des deux inegalites posit et negat eliminant la variable v.
Une nouvelle contrainte est allouee et renvoyee.
Si le coefficient de v dans negat egale -1 ou si le coefficient de v dans posit egale 1, la nouvelle contrainte est equivalente en nombres entiers avec posit et negat.
Modifications:
Le controle de l'overflow est effectue et traite par le retour du contexte correspondant au dernier CATCH(overflow_error) effectue.
pdiv ???
posit | osit |
negat | egat |
ofl_ctrl | fl_ctrl |
Definition at line 179 of file binaires.c.
References assert, contrainte_new(), pgcd, value_div, value_neg_p, value_notone_p, value_pos_p, value_uminus, vect_cl2_ofl_ctrl(), vect_coeff(), and Scontrainte::vecteur.
Referenced by inegalite_comb(), and inegalite_comb_ofl().