binaires.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include "linear_assert.h"
#include "boolean.h"
#include "arithmetique.h"
#include "vecteur.h"
#include "contrainte.h"

Include dependency graph for binaires.c:

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...

Function Documentation

contrainte_append()

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.

Parameters

c1	1
c2	2

Definition at line 267 of file binaires.c.

{
    Pcontrainte c;
    
    if (c1==NULL) return(c2);
    if (c2==NULL) return(c1);
    for (c=c1; c->succ!=NULL; c=c->succ);
    c->succ=c2;
    return(c1);
}

References Scontrainte::succ.

Referenced by algorithm_row_echelon_generic(), and sc_bounded_normalization().

Here is the caller graph for this function:

contrainte_subst()

int contrainte_subst	(	Variable	v,
		Pcontrainte	def,
		Pcontrainte	c,
		bool	eq_p
	)

Parameters

def	ef
eq_p	q_p

Definition at line 48 of file binaires.c.

{
    return( contrainte_subst_ofl_ctrl(v,def,c,eq_p, NO_OFL_CTRL)); 
 
}

References contrainte_subst_ofl_ctrl(), and NO_OFL_CTRL.

Here is the call graph for this function:

contrainte_subst_ofl()

int contrainte_subst_ofl	(	Variable	v,
		Pcontrainte	def,
		Pcontrainte	c,
		bool	eq_p
	)

package contrainte - operations binaires

binaires.c

Parameters

def	ef
eq_p	q_p

Definition at line 40 of file binaires.c.

{
    return( contrainte_subst_ofl_ctrl(v,def,c,eq_p, FWD_OFL_CTRL)); 
}

References contrainte_subst_ofl_ctrl(), and FWD_OFL_CTRL.

Here is the call graph for this function:

contrainte_subst_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

Parameters

def	ef
eq_p	q_p
ofl_ctrl	fl_ctrl

Definition at line 107 of file binaires.c.

{
    Pvecteur save_c;
 
    /* cv_def = coeff de v dans def */
    Value cv_def = vect_coeff(v,def->vecteur);
    /* cv_c = coeff de v dans c */
    Value cv_c = vect_coeff(v,c->vecteur);
 
    /* il faut que cv_def soit non nul pour que la variable v puisse etre
       eliminee */
    assert(value_notzero_p(cv_def));
 
    /* il n'y a rien a faire si la variable v n'apparait pas dans la
       contrainte c */
    /* substitution inutile: variable v absente */
    if (value_zero_p(cv_c)) return 1;
 
    /* on garde trace de la valeur de c avant substitution pour pouvoir
       la desallouer apres le calcul de la nouvelle */
    save_c = c->vecteur;
    /* 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 */
    if (value_neg_p(cv_def)) {
        c->vecteur = vect_cl2_ofl_ctrl(value_uminus(cv_def),
                                       c->vecteur,cv_c,
                                       def->vecteur,
                                       ofl_ctrl);
    }
    else {
        c->vecteur = vect_cl2_ofl_ctrl(cv_def,c->vecteur,
                                       value_uminus(cv_c),
                                  def->vecteur, ofl_ctrl);
    }
    vect_rm(save_c);
 
    /* reste malikien: cette partie ne peut pas etre faite sans savoir
       si on est en train de traiter une egalite ou une inegalite */
    if(contrainte_constante_p(c)) {
        if(contrainte_verifiee(c,eq_p)) 
            /* => eliminer cette c inutile */
            return(-1); 
        else 
            /* => systeme non faisable      */
            return(false);
    }
    return(true);
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

contrainte_substitute_dimension()

Pcontrainte contrainte_substitute_dimension	(	Pcontrainte	e,
		Variable	i,
		Pvecteur	v
	)

Definition at line 57 of file binaires.c.

{
  Pvecteur nv = contrainte_vecteur(e);
  contrainte_vecteur(e) = vect_substitute_dimension(nv, i, v);
  return e;
}

References contrainte_vecteur, and vect_substitute_dimension().

Referenced by sc_substitute_dimension().

Here is the call graph for this function:

Here is the caller graph for this function:

eq_diff_const()

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:

• cette routine fait l'hypothese que CONTRAINTE_UNDEFINED=>CONTRAINTE_NULLE

Modifications:

• renvoie d'une valeur non nulle meme si une des contraintes est nulles

Parameters

c1	1
c2	2

Definition at line 218 of file binaires.c.

{
    if(c1!=NULL) 
        if(c2!=NULL) {
            Value b1 = vect_coeff(TCST,c1->vecteur),
                  b2 = vect_coeff(TCST,c2->vecteur);
            return value_minus(b1,b2);
        }
        else
            return vect_coeff(TCST,c1->vecteur);
    else
        if(c2!=NULL)
            return value_uminus(vect_coeff(TCST,c2->vecteur));
        else
            return VALUE_ZERO;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

eq_sum_const()

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:

• cette routine fait l'hypothese que CONTRAINTE_UNDEFINED=>CONTRAINTE_NULLE

Parameters

c1	1
c2	2

Definition at line 243 of file binaires.c.

{
    if(c1!=NULL) 
        if(c2!=NULL) {
            Value b1 = vect_coeff(TCST,c1->vecteur),
                  b2 = vect_coeff(TCST,c2->vecteur);
            return value_plus(b1, b2);
        }
        else
            return vect_coeff(TCST,c1->vecteur);
    else
        if(c2!=NULL)
            return vect_coeff(TCST,c2->vecteur);
        else
            return VALUE_ZERO;
}

References b1, b2, TCST, value_plus, VALUE_ZERO, and vect_coeff().

Referenced by sc_check_inequality_redundancy().

Here is the call graph for this function:

Here is the caller graph for this function:

extract_common_constraints()

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.

Parameters

pc1	c1
pc2	c2
eq	q

Definition at line 285 of file binaires.c.

{
  Pcontrainte c = CONTRAINTE_UNDEFINED, c1, c2, c1p, c2p, nc1, nc2;
  
  for (c1 = *pc1, 
         c1p = CONTRAINTE_UNDEFINED, 
         nc1 = c1? c1->succ: CONTRAINTE_UNDEFINED; 
       c1; 
       c1p = (c1==nc1)? c1p: c1, 
         c1 = nc1, 
         nc1 = c1? c1->succ: CONTRAINTE_UNDEFINED)
  {
    for (c2 = *pc2,
           c2p = CONTRAINTE_UNDEFINED,
           nc2 = c2? c2->succ: CONTRAINTE_UNDEFINED; 
         c2; 
         c2p = (c2==nc2)? c2p: c2,
           c2 = nc2,
           nc2 = c2? c2->succ: CONTRAINTE_UNDEFINED)
    {
      if ((eq && egalite_equal(c1, c2)) || (!eq && contrainte_equal(c1, c2)))
      {
        /* common! */
        Pcontrainte sc1 = c1->succ, sc2 = c2->succ;
 
        c1->succ = c, c = c1; /* link to result. */
        c2->succ = NULL, contrainte_free(c2);  /* clean */
 
        if (c1p) c1p->succ = sc1; else *pc1 = sc1;
        if (c2p) c2p->succ = sc2; else *pc2 = sc2;
        
        /* get to next. */
        c1 = nc1;
        c2 = nc2 = CONTRAINTE_UNDEFINED;
      }
    }
  }
 
  return c;
}

References contrainte_equal(), contrainte_free(), CONTRAINTE_UNDEFINED, egalite_equal(), eq, and Scontrainte::succ.

Referenced by extract_common_syst().

Here is the call graph for this function:

Here is the caller graph for this function:

inegalite_comb()

Pcontrainte inegalite_comb	(	Pcontrainte	posit,
		Pcontrainte	negat,
		Variable	v
	)

Parameters

posit	osit
negat	egat

Definition at line 65 of file binaires.c.

{
    return( inegalite_comb_ofl_ctrl(posit,negat,v, NO_OFL_CTRL));
}

References inegalite_comb_ofl_ctrl(), and NO_OFL_CTRL.

Here is the call graph for this function:

inegalite_comb_ofl()

Pcontrainte inegalite_comb_ofl	(	Pcontrainte	posit,
		Pcontrainte	negat,
		Variable	v
	)

Parameters

posit	osit
negat	egat

Definition at line 72 of file binaires.c.

{
    return( inegalite_comb_ofl_ctrl(posit,negat,v, FWD_OFL_CTRL));
 
}

References FWD_OFL_CTRL, and inegalite_comb_ofl_ctrl().

Here is the call graph for this function:

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:

• use gcd to reduce the combination coefficients in hope to reduce integer overflow risk (Francois Irigoin, 17 December 1991)

Le controle de l'overflow est effectue et traite par le retour du contexte correspondant au dernier CATCH(overflow_error) effectue.

pdiv ???

Parameters

posit	osit
negat	egat
ofl_ctrl	fl_ctrl

Definition at line 179 of file binaires.c.

{
    Value cv_p, cv_n, d;
    Pcontrainte ineg;
 
    cv_p = vect_coeff(v,posit->vecteur); 
    cv_n = vect_coeff(v,negat->vecteur);
 
    assert(value_pos_p(cv_p) && value_neg_p(cv_n));
 
    d = pgcd(cv_p, value_uminus(cv_n));
    if(value_notone_p(d)) {
        cv_p = value_div(cv_p,d); /* pdiv ??? */
        cv_n = value_div(cv_n,d);
    }
 
    ineg = contrainte_new();
 
    ineg->vecteur = vect_cl2_ofl_ctrl(cv_p,negat->vecteur,
                                      value_uminus(cv_n),
                                      posit->vecteur, ofl_ctrl);
    return(ineg);
}

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().

Here is the call graph for this function:

Here is the caller graph for this function: