PIPS
pip_interface.c
Go to the documentation of this file.
1 /*
2 
3  $Id: pip_interface.c 23065 2016-03-02 09:05:50Z coelho $
4 
5  Copyright 1989-2016 MINES ParisTech
6 
7  This file is part of PIPS.
8 
9  PIPS is free software: you can redistribute it and/or modify it
10  under the terms of the GNU General Public License as published by
11  the Free Software Foundation, either version 3 of the License, or
12  any later version.
13 
14  PIPS is distributed in the hope that it will be useful, but WITHOUT ANY
15  WARRANTY; without even the implied warranty of MERCHANTABILITY or
16  FITNESS FOR A PARTICULAR PURPOSE.
17 
18  See the GNU General Public License for more details.
19 
20  You should have received a copy of the GNU General Public License
21  along with PIPS. If not, see <http://www.gnu.org/licenses/>.
22 
23 */
24 #ifdef HAVE_CONFIG_H
25  #include "pips_config.h"
26 #endif
27 /* Name : pip_interface.c
28  * Package : paf-util
29  * Author : A. Leservot
30  * Date : 01 12 1993
31  * Historic :
32  * Documents:
33  * Comments : Functions to call directly PIP from C3 and get results back in
34  * a newgen data (quast).
35  */
36 
37 /* Ansi includes */
38 #include <setjmp.h>
39 #include <stdio.h>
40 #include <string.h>
41 #include <errno.h>
42 
43 /* Newgen includes */
44 #include "genC.h"
45 
46 /* C3 includes */
47 #include "boolean.h"
48 #include "arithmetique.h"
49 #include "vecteur.h"
50 #include "contrainte.h"
51 #include "ray_dte.h"
52 #include "sommet.h"
53 #include "sg.h"
54 #include "sc.h"
55 #include "polyedre.h"
56 #include "matrix.h"
57 
58 /* Pips includes */
59 #include "ri.h"
60 #include "constants.h"
61 #include "ri-util.h"
62 #include "misc.h"
63 #include "bootstrap.h"
64 #include "complexity_ri.h"
65 #include "database.h"
66 #include "graph.h"
67 #include "dg.h"
68 #include "paf_ri.h"
69 #include "parser_private.h"
70 #include "property.h"
71 #include "reduction.h"
72 #include "text.h"
73 #include "paf-util.h"
74 #include "static_controlize.h"
75 #include "pip.h"
76 
77 
78 /* Global variables */
81 extern quast quast_act;
83 extern int ind_min_max; /* Tag for MIN or MAX resolution */
84 extern Pbase base_var_ref, /* Base of the unknowns */
85  old_base_var, /* Base of the unknowns */
86  base_ref, /* Base of the parameters */
87  old_base; /* Base of the parameters */
88 
89 struct S {
90  int flags;
92 };
93 extern struct S sol_space[];
94 
95 
96 /* Internal variables */
97 #define Nil 1
98 #define If 2
99 #define List 3
100 #define Form 4
101 #define New 5
102 #define Div 6
103 #define Val 7
104 Pvecteur vect_for_sort; /* Useful for the sorting of the variables in the
105  * system's Pvecteur.
106  */
107 
108 
109 
110 /*===========================================================================*/
111 /* int integer_sol_edit((int) i) AL 28/03/94
112  * We will simulate a patern matching when the solution is produced.
113  * Warning : we use here the Feautrier version of the pgcd (accept negative nb).
114  */
116 int i;
117 {
118  int j, n, first_entier, second_entier = 0, longueur_liste;
119  struct S *p;
120  Entier N, D, d;
121  p = sol_space + i;
122 
123  switch(p->flags) {
124  /* We have a newparm */
125  case New : n = p->param1;
126  first_entier = n;
127  i++; p++; /* call to Div case */
128  /* Let's take the first vector : vecteur2 (case Form) */
129  i++; p++; /* Call to Form */
130  n = p->param1;
131  /* Take all the coefficient2 */
132  init_vecteur();
133  for(j = 0; j<n; j++) {
134  i++; p++;
135  N = p->param1; D = p->param2;
136  d = sol_pgcd(N, D);
137 
138  if(d == D){
139  if(N/d < 0) ecrit_coeff_neg2( -N/d );
140  else ecrit_coeff2( N/d );
141  }
142  /* Should not be called here */
143  else{ pips_internal_error("Division 1 in newparm");
144  }
145  }
146  i++; p++;
147 
148  /* Take the corresponding new parameter */
149  N = p->param1; D = p->param2;
150  d = sol_pgcd(N, D);
151  if(d == D){
152  second_entier = N/d;
153  }
154  /* Should not happen here */
155  else{
156  pips_internal_error("Division 2 in newparm");
157  }
158  i++; p++;
159 
160  ajoute_new_var( second_entier, first_entier );
161 
162  i = integer_sol_edit( i ); /* Look at the superquast */
163 
165  break;
166 
167  /* Our quast is a conditional */
168  case If : init_quast();
169  /* Take vecteur1 part of the if */
170  i++; p++; /* Call to case Form */
171 
172  creer_Psysteme();
173 
174  n = p->param1;
175  for(j = 0; j<n; j++) {
176  i++; p++;
177  N = p->param1; D = p->param2;
178  d = sol_pgcd(N, D);
179  if(d == D){
180  ecrit_coeff1( N/d );
181  }
182  /* Should not be called here */
183  else{ pips_internal_error("Division 3 in newparm");
184  }
185  }
186 
187  creer_predicat();
188  i++; p++;
189 
190  /* Take true super quast */
191  i = integer_sol_edit(i);
192 
194 
195  /* Take false super quast */
196  i = integer_sol_edit(i);
197 
199 
200  fait_quast();
201  break;
202 
203  /* Quast is a list of solutions */
204  case List: init_quast();
205  longueur_liste = p->param1;
206  if (longueur_liste > 0) init_liste_vecteur();
207 
208  i++; p++; /* call to the liste_vecteur */
209  /* Take each vecteur (call to Form case) */
210  while(longueur_liste--) {
211  init_vecteur();
212  n = p->param1;
213  for(j = 0; j<n; j++) {
214  i++; p++;
215  N = p->param1; D = p->param2;
216  d = sol_pgcd(N, D);
217  if(d == D){
218  if (N/d < 0) ecrit_une_var_neg(-N/d);
219  else ecrit_une_var( N/d );
220  }
221  /* Should not happen here */
222  else{
223  pips_internal_error("Division 4 in newparm");
224  }
225  }
227  i++; p++;
228  }
229 
231  fait_quast();
232  break;
233 
234  /* We have an undefined quast */
235  case Nil : init_quast();
237  fait_quast();
238  i++; break;
239 
240  /* This should not happen any more */
241  case Form: pips_internal_error("Form case call");
242  break;
243 
244  /* This case should not happen any more */
245  case Div: pips_internal_error("Div case call");
246  break;
247 
248  /* This case should not happen any more */
249  case Val: pips_internal_error("Val case call");
250  break;
251 
252  default : pips_internal_error("Undefined kind of quast ");
253  }
254 
255  return(i);
256 }
257 
258 /*===========================================================================*/
259 /* int rational_sol_edit((int) i) AL 28/03/94
260  * We will simulate a patern matching when the solution is produced.
261  * Warning : we use here the Feautrier version of the pgcd (accept negative nb).
262  */
264 int i;
265 {int j, n, longueur_liste;
266  struct S *p,*p_init;
267  Entier N, D, d;
268  int lcm, i_init;
269 
270 
271  p = sol_space + i;
272 
273  switch(p->flags) {
274 
275 
276 
277 
278  /* We have a newparm */
279  case New:
280  pips_internal_error("There is a new parameter for a rational compute !");
281  break;
282 
283 
284  /* Our quast is a conditional */
285  case If : init_quast();
286 
287  /* Take vecteur1 part of the if */
288  i++; p++; /* Call to case Form */
289 
290  creer_Psysteme();
291 
292  n = p->param1;
293 
294  /* First scan to get the lcm (ppcm) of the denominator */
295  i_init = i;
296  p_init = p;
297  lcm = 1;
298  for(j = 0; j<n; j++) {
299  i++; p++;
300  N = p->param1; D = p->param2;
301  d = sol_pgcd( N, D );
302  lcm = sol_ppcm( lcm, D/d );
303  }
304 
305  /* Then write the new predicate */
306  i = i_init;
307  p = p_init;
308  for(j = 0; j<n; j++) {
309  i++; p++;
310  N = p->param1; D = p->param2;
311  ecrit_coeff1( (lcm*N)/D );
312  }
313 
314  creer_predicat();
315  i++; p++;
316 
317 
318  /* Take true super quast */
319  i = rational_sol_edit(i);
320 
321 
323 
324 
325  /* Take false super quast */
326  i = rational_sol_edit(i);
327 
328 
330 
331  fait_quast();
332  break;
333 
334 
335 
336 
337 
338  /* Quast is a list of solutions */
339  case List: init_quast();
340  longueur_liste = p->param1;
341  if (longueur_liste > 0) init_liste_vecteur();
342 
343 
344  i++; p++; /* call to the liste_vecteur */
345  /* Take each vecteur (call to Form case) */
346  while(longueur_liste--) {
347  init_vecteur();
348  n = p->param1;
349 
350  /* First scan to get the lcm (ppcm) of the denominator */
351  i_init = i;
352  p_init = p;
353  lcm = 1;
354  for(j = 0; j<n; j++) {
355  i++; p++;
356  N = p->param1; D = p->param2;
357  d = sol_pgcd( N, D );
358  lcm = sol_ppcm( lcm, D/d );
359  }
360 
361  /* Then write the expression */
362  i = i_init;
363  p = p_init;
364  for(j = 0; j<n; j++) {
365  i++; p++;
366  N = p->param1; D = p->param2;
367  d = (lcm*N)/D;
368  if (d < 0) ecrit_une_var_neg( -d );
369  else ecrit_une_var( d );
370  }
371 
372 
375  int_to_expression(lcm));
377  i++; p++;
378  }
379 
381  fait_quast();
382  break;
383 
384 
385 
386 
387  /* We have an undefined quast */
388  case Nil : init_quast();
390  fait_quast();
391  i++; break;
392 
393 
394 
395 
396  /* This should not happen any more */
397  case Form: pips_internal_error("Form case call");
398  break;
399 
400  /* This case should not happen any more */
401  case Div: pips_internal_error("Div case call");
402  break;
403 
404  /* This case should not happen any more */
405  case Val: pips_internal_error("Val case call");
406  break;
407 
408 
409  default: pips_internal_error("Undefined kind of quast ");
410 
411  }
412 
413  return(i);
414 }
415 
416 /*===========================================================================*/
417 /* int new_sol_edit((int) i) AL 8/12/93
418  * We will simulate a patern matching when the solution is produced.
419  * Warning : we use here the Feautrier version of the pgcd (accept negative nb).
420  *
421  * Just keep for compatibility. Should be thrown away AL 28 03 94.
422  */
424 int i;
425 {
426  int j, n, first_entier, second_entier = 0, longueur_liste;
427  struct S *p;
428  Entier N, D, d;
429  p = sol_space + i;
430 
431  switch(p->flags) {
432 
433 
434 
435 
436  /* We have a newparm */
437  case New : n = p->param1;
438  first_entier = n;
439 
440  i++; p++; /* call to Div case */
441  /* Let's take the first vector : vecteur2 (case Form) */
442  i++; p++; /* Call to Form */
443  n = p->param1;
444  /* Take all the coefficient2 */
445  init_vecteur();
446  for(j = 0; j<n; j++) {
447  i++; p++;
448  N = p->param1; D = p->param2;
449  d = sol_pgcd(N, D);
450 
451  if(d == D){
452  if(N/d < 0) ecrit_coeff_neg2( -N/d );
453  else ecrit_coeff2( N/d );
454  }
455  /* Should not be called here */
456  else{ pips_internal_error("Division 1 in newparm");
457  }
458  }
459  i++; p++;
460 
461 
462  /* Take the corresponding new parameter */
463  N = p->param1; D = p->param2;
464  d = sol_pgcd(N, D);
465  if(d == D){ second_entier = N/d;
466  }
467  /* Should not happen here */
468  else{ pips_internal_error("Division 2 in newparm");
469  }
470  i++; p++;
471 
472  ajoute_new_var( second_entier, first_entier );
473 
474 
475  i = new_sol_edit( i ); /* Look at the superquast */
476 
478  break;
479 
480 
481 
482  /* Our quast is a conditional */
483  case If : init_quast();
484 
485  /* Take vecteur1 part of the if */
486  i++; p++; /* Call to case Form */
487 
488  creer_Psysteme();
489 
490  n = p->param1;
491  for(j = 0; j<n; j++) {
492  i++; p++;
493  N = p->param1; D = p->param2;
494  d = sol_pgcd(N, D);
495  if(d == D){
496  ecrit_coeff1( N/d );
497  }
498  /* Should not be called here */
499  else{ pips_internal_error("Division 3 in newparm");
500  }
501  }
502 
503  creer_predicat();
504  i++; p++;
505 
506 
507  /* Take true super quast */
508  i = new_sol_edit(i);
509 
510 
512 
513 
514  /* Take false super quast */
515  i = new_sol_edit(i);
516 
517 
519 
520  fait_quast();
521  break;
522 
523 
524 
525 
526 
527  /* Quast is a list of solutions */
528  case List: init_quast();
529  longueur_liste = p->param1;
530  if (longueur_liste > 0) init_liste_vecteur();
531 
532 
533  i++; p++; /* call to the liste_vecteur */
534  /* Take each vecteur (call to Form case) */
535  while(longueur_liste--) {
536  init_vecteur();
537  n = p->param1;
538  for(j = 0; j<n; j++) {
539  i++; p++;
540  N = p->param1; D = p->param2;
541  d = sol_pgcd(N, D);
542  if(d == D){
543  if (N/d < 0) ecrit_une_var_neg(-N/d);
544  else ecrit_une_var( N/d );
545  }
546  /* Should not happen here */
547  else{ pips_internal_error("Division 4 in newparm");
548  }
549  }
551  i++; p++;
552  }
553 
555  fait_quast();
556  break;
557 
558 
559 
560 
561  /* We have an undefined quast */
562  case Nil : init_quast();
564  fait_quast();
565  i++; break;
566 
567 
568 
569 
570  /* This should not happen any more */
571  case Form: pips_internal_error("Form case call");
572  break;
573 
574  /* This case should not happen any more */
575  case Div: pips_internal_error("Div case call");
576  break;
577 
578  /* This case should not happen any more */
579  case Val: pips_internal_error("Val case call");
580  break;
581 
582 
583  default : pips_internal_error("Undefined kind of quast ");
584  }
585 
586 
587  return(i);
588 }
589 
590 
591 
592 /*===========================================================================*/
593 /* void new_ecrit_ligne(p_vect, p_sys_base, nb_var, in_val) AL 6/12/93
594  */
595 void new_ecrit_ligne(p_vect, p_sys_base, nb_var, in_val)
596 Entier *in_val;
597 Pvecteur p_vect;
598 Pbase p_sys_base;
599 int nb_var;
600 {
601  Pvecteur base = (Pvecteur) p_sys_base;
602  int aux = 0; /* Compteur de variables deja vues */
603 
604 
605  /* We run over the base and fill in in_val */
606  /* First, we put variables, then constant terms and then parameters */
607  for(; (base != NULL) || (aux <= nb_var); aux++) {
608  int val;
609 
610  if(aux == nb_var) val = (int) vect_coeff(TCST, p_vect);
611  else {
612  val = (int) vect_coeff(base->var, p_vect);
613  base = base->succ;
614  }
615 
616  *(in_val+aux) = -val;
617  }
618 }
619 
620 /*===========================================================================*/
621 /* Tableau* sc_to_tableau( (Psysteme) in_ps, (int) nb_var ) AL 6/12/93
622  * Allocates a new Tableau and fill it with in_ps.
623  * nb_var represents the number of variables in the systeme in_ps.
624  * The input systeme base should be ordered:
625  * nb_var first, constant term, then the parameters.
626  * If nb_var = 0, there is no variables : the order is then
627  * parameters first, then constant.
628  */
629 Tableau * sc_to_tableau( in_ps, nb_var )
630 Psysteme in_ps;
631 int nb_var;
632 {
633  Tableau *p;
634  int h, w, n;
635  int i;
636  Pcontrainte cont;
637 
638  debug(7, "sc_to_tableau", "Input Psysteme :\n");
639  if (get_debug_level()>7) fprint_psysteme(stderr, in_ps);
640 
641  /* Let's define h, w, and n according to tab_get in Pip/tab.c*/
642  h = 2*in_ps->nb_eq + in_ps->nb_ineq;
643  w = in_ps->dimension + 1;
644  n = nb_var;
645 
646 
647  p = tab_alloc(h, w, n);
648  if (in_ps == NULL) return NULL;
649 
650  /* If nb_var = 0, put parameter before constant */
651  if (nb_var == 0) nb_var = vect_size(in_ps->base);
652 
653  i = n;
654  for( cont = in_ps->egalites; cont != NULL; cont = cont->succ) {
655  p->row[i].flags = Unknown;
656  new_ecrit_ligne(cont->vecteur, in_ps->base, nb_var,
657  p->row[i].objet.val);
658  i++;
659 
660 
661  p->row[i].flags = Unknown;
663  VALUE_MONE),
664  in_ps->base, nb_var, p->row[i].objet.val);
665  i++;
666  }
667  for( cont = in_ps->inegalites; cont != NULL; cont = cont->succ) {
668  p->row[i].flags = Unknown;
669  new_ecrit_ligne(cont->vecteur, in_ps->base, nb_var,
670  p->row[i].objet.val);
671  i++;
672  }
673 
674  debug(7, "sc_to_tableau", "Output Tableau :\n");
675  if (get_debug_level()>6) tab_display(p, stderr);
676  return((Tableau *) p);
677 }
678 
void const char const char const int
#define VALUE_MONE
bdt base
Current expression.
Definition: bdt_read_paf.c:100
#define D(A)
Definition: iabrev.h:56
int vect_size(Pvecteur v)
package vecteur - reductions
Definition: reductions.c:47
#define pips_internal_error
Definition: misc-local.h:149
int get_debug_level(void)
GET_DEBUG_LEVEL returns the current debugging level.
Definition: debug.c:67
void debug(const int the_expected_debug_level, const char *calling_function_name, const char *a_message_format,...)
ARARGS0.
Definition: debug.c:189
void fprint_psysteme(FILE *, Psysteme)
===========================================================================
Definition: print.c:302
int sol_pgcd()
int sol_ppcm()
Tableau * tab_alloc()
#define Unknown
Definition: pip__tab.h:41
void tab_display()
#define Entier
Definition: pip__type.h:24
#define If
Definition: pip_interface.c:98
Pbase old_base
Base of the parameters.
Definition: pip_interface.c:79
int integer_sol_edit(int i)
Useful for the sorting of the variables in the system's Pvecteur.
Pbase base_ref
Base of the unknowns.
Definition: pip_interface.c:79
int ind_min_max
Definition: pip_interface.c:80
Pvecteur vect_for_sort
Pbase old_base_var
Base of the unknowns.
Definition: pip_interface.c:79
#define Form
void new_ecrit_ligne(Pvecteur p_vect, Pbase p_sys_base, int nb_var, Entier *in_val)
==========================================================================
#define Div
struct S sol_space[]
Definition: sol.c:48
int rational_sol_edit(int i)
==========================================================================
quast quast_act
Global variables
Definition: pip.c:101
expression expression_act
Definition: solpip.c:94
Tableau * sc_to_tableau(Psysteme in_ps, int nb_var)
==========================================================================
Pbase base_var_ref
Name : pip_interface.c Package : paf-util Author : A.
Definition: pip_interface.c:79
#define New
int new_sol_edit(int i)
==========================================================================
#define Nil
Internal variables
Definition: pip_interface.c:97
#define Val
#define List
Definition: pip_interface.c:99
#define DIVIDE_OPERATOR_NAME
expression int_to_expression(_int i)
transform an int into an expression and generate the corresponding entity if necessary; it is not cle...
Definition: expression.c:1188
expression make_op_exp(char *op_name, expression exp1, expression exp2)
================================================================
Definition: expression.c:2012
Pvecteur vect_multiply(Pvecteur v, Value x)
Pvecteur vect_multiply(Pvecteur v, Value x): multiplication du vecteur v par le scalaire x,...
Definition: scalaires.c:123
int aux
Definition: solpip.c:104
void fait_quast()
Name: fait_quast.
Definition: solpip.c:331
void ecrit_coeff_neg2(int ent)
Name: ecrit_coeff_neg2.
Definition: solpip.c:1028
void ajoute_new_var(int ent, int rang)
Name: ajoute_new_var.
Definition: solpip.c:715
void creer_Psysteme()
Name: creer_Psysteme.
Definition: solpip.c:558
void ecrit_une_var(int ent)
Name: ecrire_une_var.
Definition: solpip.c:823
void ecrit_liste_vecteur()
Name: ecrit_liste_vecteur.
Definition: solpip.c:783
void ecrit_coeff2(int ent)
Name: ecrire_coeff2 .
Definition: solpip.c:1070
void retire_par_de_pile()
Name: retire_par_de_pile.
Definition: solpip.c:168
void creer_true_quast()
Name: creer_true_quast.
Definition: solpip.c:264
void init_liste_vecteur()
Name: init_liste_vecteur.
Definition: solpip.c:405
void fait_quast_value()
Name: fait_quast_value.
Definition: solpip.c:365
void init_vecteur()
Name: init_vecteur.
Definition: solpip.c:438
void ecrit_une_var_neg(int ent)
Name: ecrit_une_var_neg.
Definition: solpip.c:935
void creer_predicat()
Name: creer_predicat.
Definition: solpip.c:296
void creer_quast_value()
Name: creer_quast_value
Definition: solpip.c:232
void ecrit_coeff1(int ent)
Name: ecrit_coeff1.
Definition: solpip.c:474
void init_quast()
Name: init_quast.
Definition: solpip.c:205
int flags
Definition: pip__tab.h:30
Entier * val
Definition: pip__tab.h:32
union L::@15 objet
Base of the parameters.
Definition: pip_interface.c:89
Entier param1
Definition: pip_interface.c:91
int flags
Definition: pip_interface.c:90
Entier param2
Definition: pip_interface.c:91
Pvecteur vecteur
struct Scontrainte * succ
le type des coefficients dans les vecteurs: Value est defini dans le package arithmetique
Definition: vecteur-local.h:89
Definition: pip__tab.h:48
struct L row[1]
Definition: pip__tab.h:49
#define TCST
VARIABLE REPRESENTANT LE TERME CONSTANT.
struct Svecteur * Pvecteur
Pvecteur vect_dup(Pvecteur v_in)
Pvecteur vect_dup(Pvecteur v_in): duplication du vecteur v_in; allocation de et copie dans v_out;.
Definition: alloc.c:51
Value vect_coeff(Variable var, Pvecteur vect)
Variable vect_coeff(Variable var, Pvecteur vect): coefficient de coordonnee var du vecteur vect —> So...
Definition: unaires.c:228