5 #include "ev_operations.h"
8 #define NALLOC(p,n) p = (typeof(p))malloc((n) * sizeof(*p))
10 void evalue_set_si(evalue
*ev
, int n
, int d
) {
11 value_set_si(ev
->d
, d
);
13 value_set_si(ev
->x
.n
, n
);
16 void evalue_set(evalue
*ev
, Value n
, Value d
) {
17 value_assign(ev
->d
, d
);
19 value_assign(ev
->x
.n
, n
);
22 void aep_evalue(evalue
*e
, int *ref
) {
27 if (value_notzero_p(e
->d
))
28 return; /* a rational number, its already reduced */
30 return; /* hum... an overflow probably occured */
32 /* First check the components of p */
33 for (i
=0;i
<p
->size
;i
++)
34 aep_evalue(&p
->arr
[i
],ref
);
41 p
->pos
= ref
[p
->pos
-1]+1;
47 void addeliminatedparams_evalue(evalue
*e
,Matrix
*CT
) {
53 if (value_notzero_p(e
->d
))
54 return; /* a rational number, its already reduced */
56 return; /* hum... an overflow probably occured */
59 ref
= (int *)malloc(sizeof(int)*(CT
->NbRows
-1));
60 for(i
=0;i
<CT
->NbRows
-1;i
++)
61 for(j
=0;j
<CT
->NbColumns
;j
++)
62 if(value_notzero_p(CT
->p
[i
][j
])) {
67 /* Transform the references in e, using ref */
71 } /* addeliminatedparams_evalue */
73 static int mod_rational_smaller(evalue
*e1
, evalue
*e2
)
79 assert(value_notzero_p(e1
->d
));
80 assert(value_notzero_p(e2
->d
));
81 value_multiply(m
, e1
->x
.n
, e2
->d
);
82 value_division(m
, m
, e1
->d
);
83 if (value_lt(m
, e2
->x
.n
))
85 else if (value_gt(m
, e2
->x
.n
))
94 static int mod_term_smaller_r(evalue
*e1
, evalue
*e2
)
96 if (value_notzero_p(e1
->d
)) {
97 if (value_zero_p(e2
->d
))
99 int r
= mod_rational_smaller(e1
, e2
);
100 return r
== -1 ? 0 : r
;
102 if (value_notzero_p(e2
->d
))
104 if (e1
->x
.p
->pos
< e2
->x
.p
->pos
)
106 else if (e1
->x
.p
->pos
> e2
->x
.p
->pos
)
109 int r
= mod_rational_smaller(&e1
->x
.p
->arr
[1], &e2
->x
.p
->arr
[1]);
111 ? mod_term_smaller_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0])
116 static int mod_term_smaller(evalue
*e1
, evalue
*e2
)
118 assert(value_zero_p(e1
->d
));
119 assert(value_zero_p(e2
->d
));
120 assert(e1
->x
.p
->type
== fractional
);
121 assert(e2
->x
.p
->type
== fractional
);
122 return mod_term_smaller_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]);
125 /* Negative pos means inequality */
126 /* s is negative of substitution if m is not zero */
135 struct fixed_param
*fixed
;
140 static int relations_depth(evalue
*e
)
145 value_zero_p(e
->d
) && e
->x
.p
->type
== relation
;
146 e
= &e
->x
.p
->arr
[1], ++d
);
150 static void Lcm3(Value i
, Value j
, Value
*res
)
156 value_multiply(*res
,i
,j
);
157 value_division(*res
, *res
, aux
);
161 static void poly_denom(evalue
*p
, Value
*d
)
165 while (value_zero_p(p
->d
)) {
166 assert(p
->x
.p
->type
== polynomial
);
167 assert(p
->x
.p
->size
== 2);
168 assert(value_notzero_p(p
->x
.p
->arr
[1].d
));
169 Lcm3(*d
, p
->x
.p
->arr
[1].d
, d
);
175 #define EVALUE_IS_ONE(ev) (value_pos_p((ev).d) && value_one_p((ev).x.n))
177 static void realloc_substitution(struct subst
*s
, int d
)
179 struct fixed_param
*n
;
182 for (i
= 0; i
< s
->n
; ++i
)
189 static int add_modulo_substitution(struct subst
*s
, evalue
*r
)
195 assert(value_zero_p(r
->d
) && r
->x
.p
->type
== relation
);
198 /* May have been reduced already */
199 if (value_notzero_p(m
->d
))
202 assert(value_zero_p(m
->d
) && m
->x
.p
->type
== fractional
);
203 assert(m
->x
.p
->size
== 3);
205 /* fractional was inverted during reduction
206 * invert it back and move constant in
208 if (!EVALUE_IS_ONE(m
->x
.p
->arr
[2])) {
209 assert(value_pos_p(m
->x
.p
->arr
[2].d
));
210 assert(value_mone_p(m
->x
.p
->arr
[2].x
.n
));
211 value_set_si(m
->x
.p
->arr
[2].x
.n
, 1);
212 value_increment(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].x
.n
);
213 assert(value_eq(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].d
));
214 value_set_si(m
->x
.p
->arr
[1].x
.n
, 1);
215 eadd(&m
->x
.p
->arr
[1], &m
->x
.p
->arr
[0]);
216 value_set_si(m
->x
.p
->arr
[1].x
.n
, 0);
217 value_set_si(m
->x
.p
->arr
[1].d
, 1);
220 /* Oops. Nested identical relations. */
221 if (!EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
224 if (s
->n
>= s
->max
) {
225 int d
= relations_depth(r
);
226 realloc_substitution(s
, d
);
230 assert(value_zero_p(p
->d
) && p
->x
.p
->type
== polynomial
);
231 assert(p
->x
.p
->size
== 2);
234 assert(value_pos_p(f
->x
.n
));
236 value_init(s
->fixed
[s
->n
].m
);
237 value_assign(s
->fixed
[s
->n
].m
, f
->d
);
238 s
->fixed
[s
->n
].pos
= p
->x
.p
->pos
;
239 value_init(s
->fixed
[s
->n
].d
);
240 value_assign(s
->fixed
[s
->n
].d
, f
->x
.n
);
241 value_init(s
->fixed
[s
->n
].s
.d
);
242 evalue_copy(&s
->fixed
[s
->n
].s
, &p
->x
.p
->arr
[0]);
248 static void reorder_terms(enode
*p
, evalue
*v
)
251 int offset
= p
->type
== fractional
;
253 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
255 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
256 free_evalue_refs(&(p
->arr
[i
]));
262 void _reduce_evalue (evalue
*e
, struct subst
*s
, int fract
) {
268 if (value_notzero_p(e
->d
)) {
270 mpz_fdiv_r(e
->x
.n
, e
->x
.n
, e
->d
);
271 return; /* a rational number, its already reduced */
275 return; /* hum... an overflow probably occured */
277 /* First reduce the components of p */
278 add
= p
->type
== relation
;
279 for (i
=0; i
<p
->size
; i
++) {
281 add
= add_modulo_substitution(s
, e
);
283 if (i
== 0 && p
->type
==fractional
)
284 _reduce_evalue(&p
->arr
[i
], s
, 1);
286 _reduce_evalue(&p
->arr
[i
], s
, fract
);
288 if (add
&& i
== p
->size
-1) {
290 value_clear(s
->fixed
[s
->n
].m
);
291 value_clear(s
->fixed
[s
->n
].d
);
292 free_evalue_refs(&s
->fixed
[s
->n
].s
);
293 } else if (add
&& i
== 1)
294 s
->fixed
[s
->n
-1].pos
*= -1;
297 if (p
->type
==periodic
) {
299 /* Try to reduce the period */
300 for (i
=1; i
<=(p
->size
)/2; i
++) {
301 if ((p
->size
% i
)==0) {
303 /* Can we reduce the size to i ? */
305 for (k
=j
+i
; k
<e
->x
.p
->size
; k
+=i
)
306 if (!eequal(&p
->arr
[j
], &p
->arr
[k
])) goto you_lose
;
309 for (j
=i
; j
<p
->size
; j
++) free_evalue_refs(&p
->arr
[j
]);
313 you_lose
: /* OK, lets not do it */
318 /* Try to reduce its strength */
321 memcpy(e
,&p
->arr
[0],sizeof(evalue
));
325 else if (p
->type
==polynomial
) {
326 for (k
= 0; s
&& k
< s
->n
; ++k
) {
327 if (s
->fixed
[k
].pos
== p
->pos
) {
328 int divide
= value_notone_p(s
->fixed
[k
].d
);
331 if (value_notzero_p(s
->fixed
[k
].m
)) {
334 assert(p
->size
== 2);
335 if (divide
&& value_ne(s
->fixed
[k
].d
, p
->arr
[1].x
.n
))
337 if (!mpz_divisible_p(s
->fixed
[k
].m
, p
->arr
[1].d
))
344 value_assign(d
.d
, s
->fixed
[k
].d
);
346 if (value_notzero_p(s
->fixed
[k
].m
))
347 value_oppose(d
.x
.n
, s
->fixed
[k
].m
);
349 value_set_si(d
.x
.n
, 1);
352 for (i
=p
->size
-1;i
>=1;i
--) {
353 emul(&s
->fixed
[k
].s
, &p
->arr
[i
]);
355 emul(&d
, &p
->arr
[i
]);
356 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
357 free_evalue_refs(&(p
->arr
[i
]));
360 _reduce_evalue(&p
->arr
[0], s
, fract
);
363 free_evalue_refs(&d
);
369 /* Try to reduce the degree */
370 for (i
=p
->size
-1;i
>=1;i
--) {
371 if (!(value_one_p(p
->arr
[i
].d
) && value_zero_p(p
->arr
[i
].x
.n
)))
373 /* Zero coefficient */
374 free_evalue_refs(&(p
->arr
[i
]));
379 /* Try to reduce its strength */
382 memcpy(e
,&p
->arr
[0],sizeof(evalue
));
386 else if (p
->type
==fractional
) {
390 if (value_notzero_p(p
->arr
[0].d
)) {
392 value_assign(v
.d
, p
->arr
[0].d
);
394 mpz_fdiv_r(v
.x
.n
, p
->arr
[0].x
.n
, p
->arr
[0].d
);
399 evalue
*pp
= &p
->arr
[0];
400 assert(value_zero_p(pp
->d
) && pp
->x
.p
->type
== polynomial
);
401 assert(pp
->x
.p
->size
== 2);
403 /* search for exact duplicate among the modulo inequalities */
405 f
= &pp
->x
.p
->arr
[1];
406 for (k
= 0; s
&& k
< s
->n
; ++k
) {
407 if (-s
->fixed
[k
].pos
== pp
->x
.p
->pos
&&
408 value_eq(s
->fixed
[k
].d
, f
->x
.n
) &&
409 value_eq(s
->fixed
[k
].m
, f
->d
) &&
410 eequal(&s
->fixed
[k
].s
, &pp
->x
.p
->arr
[0]))
417 /* replace { E/m } by { (E-1)/m } + 1/m */
422 evalue_set_si(&extra
, 1, 1);
423 value_assign(extra
.d
, g
);
424 eadd(&extra
, &v
.x
.p
->arr
[1]);
425 free_evalue_refs(&extra
);
427 /* We've been going in circles; stop now */
428 if (value_ge(v
.x
.p
->arr
[1].x
.n
, v
.x
.p
->arr
[1].d
)) {
429 free_evalue_refs(&v
);
431 evalue_set_si(&v
, 0, 1);
436 value_set_si(v
.d
, 0);
437 v
.x
.p
= new_enode(fractional
, 3, -1);
438 evalue_set_si(&v
.x
.p
->arr
[1], 1, 1);
439 value_assign(v
.x
.p
->arr
[1].d
, g
);
440 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
441 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
444 for (f
= &v
.x
.p
->arr
[0]; value_zero_p(f
->d
);
447 value_division(f
->d
, g
, f
->d
);
448 value_multiply(f
->x
.n
, f
->x
.n
, f
->d
);
449 value_assign(f
->d
, g
);
450 value_decrement(f
->x
.n
, f
->x
.n
);
451 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
453 Gcd(f
->d
, f
->x
.n
, &g
);
454 value_division(f
->d
, f
->d
, g
);
455 value_division(f
->x
.n
, f
->x
.n
, g
);
464 /* reduction may have made this fractional arg smaller */
465 i
= reorder
? p
->size
: 1;
466 for ( ; i
< p
->size
; ++i
)
467 if (value_zero_p(p
->arr
[i
].d
) &&
468 p
->arr
[i
].x
.p
->type
== fractional
&&
469 !mod_term_smaller(e
, &p
->arr
[i
]))
473 value_set_si(v
.d
, 0);
474 v
.x
.p
= new_enode(fractional
, 3, -1);
475 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
476 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
477 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
487 for (pp
= &p
->arr
[0]; value_zero_p(pp
->d
);
488 pp
= &pp
->x
.p
->arr
[0]) {
489 f
= &pp
->x
.p
->arr
[1];
490 assert(value_pos_p(f
->d
));
491 mpz_mul_ui(twice
, f
->x
.n
, 2);
492 if (value_lt(twice
, f
->d
))
494 if (value_eq(twice
, f
->d
))
502 value_set_si(v
.d
, 0);
503 v
.x
.p
= new_enode(fractional
, 3, -1);
504 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
505 poly_denom(&p
->arr
[0], &twice
);
506 value_assign(v
.x
.p
->arr
[1].d
, twice
);
507 value_decrement(v
.x
.p
->arr
[1].x
.n
, twice
);
508 evalue_set_si(&v
.x
.p
->arr
[2], -1, 1);
509 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
511 for (pp
= &v
.x
.p
->arr
[0]; value_zero_p(pp
->d
);
512 pp
= &pp
->x
.p
->arr
[0]) {
513 f
= &pp
->x
.p
->arr
[1];
514 value_oppose(f
->x
.n
, f
->x
.n
);
515 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
517 value_division(pp
->d
, twice
, pp
->d
);
518 value_multiply(pp
->x
.n
, pp
->x
.n
, pp
->d
);
519 value_assign(pp
->d
, twice
);
520 value_oppose(pp
->x
.n
, pp
->x
.n
);
521 value_decrement(pp
->x
.n
, pp
->x
.n
);
522 mpz_fdiv_r(pp
->x
.n
, pp
->x
.n
, pp
->d
);
532 reorder_terms(p
, &v
);
533 _reduce_evalue(&p
->arr
[1], s
, fract
);
536 /* Try to reduce the degree */
537 for (i
=p
->size
-1;i
>=2;i
--) {
538 if (!(value_one_p(p
->arr
[i
].d
) && value_zero_p(p
->arr
[i
].x
.n
)))
540 /* Zero coefficient */
541 free_evalue_refs(&(p
->arr
[i
]));
546 /* Try to reduce its strength */
549 memcpy(e
,&p
->arr
[1],sizeof(evalue
));
550 free_evalue_refs(&(p
->arr
[0]));
554 else if (p
->type
== relation
) {
555 if (p
->size
== 3 && eequal(&p
->arr
[1], &p
->arr
[2])) {
556 free_evalue_refs(&(p
->arr
[2]));
557 free_evalue_refs(&(p
->arr
[0]));
564 if (p
->size
== 3 && EVALUE_IS_ZERO(p
->arr
[2])) {
565 free_evalue_refs(&(p
->arr
[2]));
568 if (p
->size
== 2 && EVALUE_IS_ZERO(p
->arr
[1])) {
569 free_evalue_refs(&(p
->arr
[1]));
570 free_evalue_refs(&(p
->arr
[0]));
571 evalue_set_si(e
, 0, 1);
578 /* Relation was reduced by means of an identical
579 * inequality => remove
581 if (value_zero_p(m
->d
) && !EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
584 if (reduced
|| value_notzero_p(p
->arr
[0].d
)) {
585 if (!reduced
&& value_zero_p(p
->arr
[0].x
.n
)) {
587 memcpy(e
,&p
->arr
[1],sizeof(evalue
));
589 free_evalue_refs(&(p
->arr
[2]));
593 memcpy(e
,&p
->arr
[2],sizeof(evalue
));
595 evalue_set_si(e
, 0, 1);
596 free_evalue_refs(&(p
->arr
[1]));
598 free_evalue_refs(&(p
->arr
[0]));
604 } /* reduce_evalue */
606 static void add_substitution(struct subst
*s
, Value
*row
, unsigned dim
)
611 for (k
= 0; k
< dim
; ++k
)
612 if (value_notzero_p(row
[k
+1]))
615 Vector_Normalize_Positive(row
+1, dim
+1, k
);
616 assert(s
->n
< s
->max
);
617 value_init(s
->fixed
[s
->n
].d
);
618 value_init(s
->fixed
[s
->n
].m
);
619 value_assign(s
->fixed
[s
->n
].d
, row
[k
+1]);
620 s
->fixed
[s
->n
].pos
= k
+1;
621 value_set_si(s
->fixed
[s
->n
].m
, 0);
622 r
= &s
->fixed
[s
->n
].s
;
624 for (l
= k
+1; l
< dim
; ++l
)
625 if (value_notzero_p(row
[l
+1])) {
626 value_set_si(r
->d
, 0);
627 r
->x
.p
= new_enode(polynomial
, 2, l
+ 1);
628 value_init(r
->x
.p
->arr
[1].x
.n
);
629 value_oppose(r
->x
.p
->arr
[1].x
.n
, row
[l
+1]);
630 value_set_si(r
->x
.p
->arr
[1].d
, 1);
634 value_oppose(r
->x
.n
, row
[dim
+1]);
635 value_set_si(r
->d
, 1);
639 void reduce_evalue (evalue
*e
) {
640 struct subst s
= { NULL
, 0, 0 };
642 if (value_notzero_p(e
->d
))
643 return; /* a rational number, its already reduced */
645 if (e
->x
.p
->type
== partition
) {
648 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
650 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
651 /* This shouldn't really happen;
652 * Empty domains should not be added.
659 D
= DomainConvex(D
, 0);
660 if (!D
->next
&& D
->NbEq
) {
664 realloc_substitution(&s
, dim
);
666 int d
= relations_depth(&e
->x
.p
->arr
[2*i
+1]);
668 NALLOC(s
.fixed
, s
.max
);
671 for (j
= 0; j
< D
->NbEq
; ++j
)
672 add_substitution(&s
, D
->Constraint
[j
], dim
);
674 if (D
!= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]))
676 _reduce_evalue(&e
->x
.p
->arr
[2*i
+1], &s
, 0);
677 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
679 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
680 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
681 value_clear(e
->x
.p
->arr
[2*i
].d
);
683 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
684 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
689 for (j
= 0; j
< s
.n
; ++j
) {
690 value_clear(s
.fixed
[j
].d
);
691 value_clear(s
.fixed
[j
].m
);
692 free_evalue_refs(&s
.fixed
[j
].s
);
696 if (e
->x
.p
->size
== 0) {
698 evalue_set_si(e
, 0, 1);
701 _reduce_evalue(e
, &s
, 0);
706 void print_evalue(FILE *DST
,evalue
*e
,char **pname
) {
708 if(value_notzero_p(e
->d
)) {
709 if(value_notone_p(e
->d
)) {
710 value_print(DST
,VALUE_FMT
,e
->x
.n
);
712 value_print(DST
,VALUE_FMT
,e
->d
);
715 value_print(DST
,VALUE_FMT
,e
->x
.n
);
719 print_enode(DST
,e
->x
.p
,pname
);
723 void print_enode(FILE *DST
,enode
*p
,char **pname
) {
728 fprintf(DST
, "NULL");
734 for (i
=0; i
<p
->size
; i
++) {
735 print_evalue(DST
, &p
->arr
[i
], pname
);
739 fprintf(DST
, " }\n");
743 for (i
=p
->size
-1; i
>=0; i
--) {
744 print_evalue(DST
, &p
->arr
[i
], pname
);
745 if (i
==1) fprintf(DST
, " * %s + ", pname
[p
->pos
-1]);
747 fprintf(DST
, " * %s^%d + ", pname
[p
->pos
-1], i
);
749 fprintf(DST
, " )\n");
753 for (i
=0; i
<p
->size
; i
++) {
754 print_evalue(DST
, &p
->arr
[i
], pname
);
755 if (i
!=(p
->size
-1)) fprintf(DST
, ", ");
757 fprintf(DST
," ]_%s", pname
[p
->pos
-1]);
761 for (i
=p
->size
-1; i
>=1; i
--) {
762 print_evalue(DST
, &p
->arr
[i
], pname
);
766 print_evalue(DST
, &p
->arr
[0], pname
);
769 fprintf(DST
, "^%d + ", i
-1);
774 fprintf(DST
, " )\n");
778 print_evalue(DST
, &p
->arr
[0], pname
);
779 fprintf(DST
, "= 0 ] * \n");
780 print_evalue(DST
, &p
->arr
[1], pname
);
782 fprintf(DST
, " +\n [ ");
783 print_evalue(DST
, &p
->arr
[0], pname
);
784 fprintf(DST
, "!= 0 ] * \n");
785 print_evalue(DST
, &p
->arr
[2], pname
);
789 for (i
=0; i
<p
->size
/2; i
++) {
790 Print_Domain(DST
, EVALUE_DOMAIN(p
->arr
[2*i
]), pname
);
791 print_evalue(DST
, &p
->arr
[2*i
+1], pname
);
800 static void eadd_rev(evalue
*e1
, evalue
*res
)
804 evalue_copy(&ev
, e1
);
806 free_evalue_refs(res
);
810 static void eadd_rev_cst (evalue
*e1
, evalue
*res
)
814 evalue_copy(&ev
, e1
);
815 eadd(res
, &ev
.x
.p
->arr
[ev
.x
.p
->type
==fractional
]);
816 free_evalue_refs(res
);
820 struct section
{ Polyhedron
* D
; evalue E
; };
822 void eadd_partitions (evalue
*e1
,evalue
*res
)
827 s
= (struct section
*)
828 malloc((e1
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2+1) *
829 sizeof(struct section
));
833 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
834 assert(res
->x
.p
->size
>= 2);
835 fd
= DomainDifference(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
836 EVALUE_DOMAIN(res
->x
.p
->arr
[0]), 0);
838 for (i
= 1; i
< res
->x
.p
->size
/2; ++i
) {
840 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
849 value_init(s
[n
].E
.d
);
850 evalue_copy(&s
[n
].E
, &e1
->x
.p
->arr
[2*j
+1]);
854 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
855 fd
= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]);
856 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
858 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
859 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
865 fd
= DomainDifference(fd
, EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]), 0);
866 if (t
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
868 value_init(s
[n
].E
.d
);
869 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
870 eadd(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
875 s
[n
].E
= res
->x
.p
->arr
[2*i
+1];
879 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
882 if (fd
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
883 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
884 value_clear(res
->x
.p
->arr
[2*i
].d
);
888 res
->x
.p
= new_enode(partition
, 2*n
, -1);
889 for (j
= 0; j
< n
; ++j
) {
890 s
[j
].D
= DomainConstraintSimplify(s
[j
].D
, 0);
891 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
892 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
893 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
899 static void explicit_complement(evalue
*res
)
901 enode
*rel
= new_enode(relation
, 3, 0);
903 value_clear(rel
->arr
[0].d
);
904 rel
->arr
[0] = res
->x
.p
->arr
[0];
905 value_clear(rel
->arr
[1].d
);
906 rel
->arr
[1] = res
->x
.p
->arr
[1];
907 value_set_si(rel
->arr
[2].d
, 1);
908 value_init(rel
->arr
[2].x
.n
);
909 value_set_si(rel
->arr
[2].x
.n
, 0);
914 void eadd(evalue
*e1
,evalue
*res
) {
917 if (value_notzero_p(e1
->d
) && value_notzero_p(res
->d
)) {
918 /* Add two rational numbers */
924 value_multiply(m1
,e1
->x
.n
,res
->d
);
925 value_multiply(m2
,res
->x
.n
,e1
->d
);
926 value_addto(res
->x
.n
,m1
,m2
);
927 value_multiply(res
->d
,e1
->d
,res
->d
);
928 Gcd(res
->x
.n
,res
->d
,&g
);
929 if (value_notone_p(g
)) {
930 value_division(res
->d
,res
->d
,g
);
931 value_division(res
->x
.n
,res
->x
.n
,g
);
933 value_clear(g
); value_clear(m1
); value_clear(m2
);
936 else if (value_notzero_p(e1
->d
) && value_zero_p(res
->d
)) {
937 switch (res
->x
.p
->type
) {
939 /* Add the constant to the constant term of a polynomial*/
940 eadd(e1
, &res
->x
.p
->arr
[0]);
943 /* Add the constant to all elements of a periodic number */
944 for (i
=0; i
<res
->x
.p
->size
; i
++) {
945 eadd(e1
, &res
->x
.p
->arr
[i
]);
949 fprintf(stderr
, "eadd: cannot add const with vector\n");
952 eadd(e1
, &res
->x
.p
->arr
[1]);
955 assert(EVALUE_IS_ZERO(*e1
));
956 break; /* Do nothing */
958 /* Create (zero) complement if needed */
959 if (res
->x
.p
->size
< 3 && !EVALUE_IS_ZERO(*e1
))
960 explicit_complement(res
);
961 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
962 eadd(e1
, &res
->x
.p
->arr
[i
]);
968 /* add polynomial or periodic to constant
969 * you have to exchange e1 and res, before doing addition */
971 else if (value_zero_p(e1
->d
) && value_notzero_p(res
->d
)) {
975 else { // ((e1->d==0) && (res->d==0))
976 assert(!((e1
->x
.p
->type
== partition
) ^
977 (res
->x
.p
->type
== partition
)));
978 if (e1
->x
.p
->type
== partition
) {
979 eadd_partitions(e1
, res
);
982 if (e1
->x
.p
->type
== relation
&&
983 (res
->x
.p
->type
!= relation
||
984 mod_term_smaller(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]))) {
988 if (res
->x
.p
->type
== relation
) {
989 if (e1
->x
.p
->type
== relation
&&
990 eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0])) {
991 if (res
->x
.p
->size
< 3 && e1
->x
.p
->size
== 3)
992 explicit_complement(res
);
993 if (e1
->x
.p
->size
< 3 && res
->x
.p
->size
== 3)
994 explicit_complement(e1
);
995 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
996 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
999 if (res
->x
.p
->size
< 3)
1000 explicit_complement(res
);
1001 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1002 eadd(e1
, &res
->x
.p
->arr
[i
]);
1005 if ((e1
->x
.p
->type
!= res
->x
.p
->type
) ) {
1006 /* adding to evalues of different type. two cases are possible
1007 * res is periodic and e1 is polynomial, you have to exchange
1008 * e1 and res then to add e1 to the constant term of res */
1009 if (e1
->x
.p
->type
== polynomial
) {
1010 eadd_rev_cst(e1
, res
);
1012 else if (res
->x
.p
->type
== polynomial
) {
1013 /* res is polynomial and e1 is periodic,
1014 add e1 to the constant term of res */
1016 eadd(e1
,&res
->x
.p
->arr
[0]);
1022 else if (e1
->x
.p
->pos
!= res
->x
.p
->pos
||
1023 (res
->x
.p
->type
== fractional
&&
1024 !eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]))) {
1025 /* adding evalues of different position (i.e function of different unknowns
1026 * to case are possible */
1028 switch (res
->x
.p
->type
) {
1030 if(mod_term_smaller(res
, e1
))
1031 eadd(e1
,&res
->x
.p
->arr
[1]);
1033 eadd_rev_cst(e1
, res
);
1035 case polynomial
: // res and e1 are polynomials
1036 // add e1 to the constant term of res
1038 if(res
->x
.p
->pos
< e1
->x
.p
->pos
)
1039 eadd(e1
,&res
->x
.p
->arr
[0]);
1041 eadd_rev_cst(e1
, res
);
1042 // value_clear(g); value_clear(m1); value_clear(m2);
1044 case periodic
: // res and e1 are pointers to periodic numbers
1045 //add e1 to all elements of res
1047 if(res
->x
.p
->pos
< e1
->x
.p
->pos
)
1048 for (i
=0;i
<res
->x
.p
->size
;i
++) {
1049 eadd(e1
,&res
->x
.p
->arr
[i
]);
1058 //same type , same pos and same size
1059 if (e1
->x
.p
->size
== res
->x
.p
->size
) {
1060 // add any element in e1 to the corresponding element in res
1061 if (res
->x
.p
->type
== fractional
)
1062 assert(eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]));
1063 i
= res
->x
.p
->type
== fractional
? 1 : 0;
1064 for (; i
<res
->x
.p
->size
; i
++) {
1065 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1070 /* Sizes are different */
1071 switch(res
->x
.p
->type
) {
1074 /* VIN100: if e1-size > res-size you have to copy e1 in a */
1075 /* new enode and add res to that new node. If you do not do */
1076 /* that, you lose the the upper weight part of e1 ! */
1078 if(e1
->x
.p
->size
> res
->x
.p
->size
)
1082 if (res
->x
.p
->type
== fractional
)
1083 assert(eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]));
1084 i
= res
->x
.p
->type
== fractional
? 1 : 0;
1085 for (; i
<e1
->x
.p
->size
; i
++) {
1086 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1093 /* add two periodics of the same pos (unknown) but whith different sizes (periods) */
1096 /* you have to create a new evalue 'ne' in whitch size equals to the lcm
1097 of the sizes of e1 and res, then to copy res periodicaly in ne, after
1098 to add periodicaly elements of e1 to elements of ne, and finaly to
1103 value_init(ex
); value_init(ey
);value_init(ep
);
1106 value_set_si(ex
,e1
->x
.p
->size
);
1107 value_set_si(ey
,res
->x
.p
->size
);
1108 value_assign (ep
,*Lcm(ex
,ey
));
1109 p
=(int)mpz_get_si(ep
);
1110 ne
= (evalue
*) malloc (sizeof(evalue
));
1112 value_set_si( ne
->d
,0);
1114 ne
->x
.p
=new_enode(res
->x
.p
->type
,p
, res
->x
.p
->pos
);
1116 evalue_copy(&ne
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
%y
]);
1119 eadd(&e1
->x
.p
->arr
[i
%x
], &ne
->x
.p
->arr
[i
]);
1122 value_assign(res
->d
, ne
->d
);
1128 fprintf(stderr
, "eadd: ?cannot add vectors of different length\n");
1135 static void emul_rev (evalue
*e1
, evalue
*res
)
1139 evalue_copy(&ev
, e1
);
1141 free_evalue_refs(res
);
1145 static void emul_poly (evalue
*e1
, evalue
*res
)
1147 int i
, j
, o
= res
->x
.p
->type
== fractional
;
1149 int size
=(e1
->x
.p
->size
+ res
->x
.p
->size
- o
- 1);
1151 value_set_si(tmp
.d
,0);
1152 tmp
.x
.p
=new_enode(res
->x
.p
->type
, size
, res
->x
.p
->pos
);
1154 evalue_copy(&tmp
.x
.p
->arr
[0], &e1
->x
.p
->arr
[0]);
1155 for (i
=o
; i
< e1
->x
.p
->size
; i
++) {
1156 evalue_copy(&tmp
.x
.p
->arr
[i
], &e1
->x
.p
->arr
[i
]);
1157 emul(&res
->x
.p
->arr
[o
], &tmp
.x
.p
->arr
[i
]);
1160 evalue_set_si(&tmp
.x
.p
->arr
[i
], 0, 1);
1161 for (i
=o
+1; i
<res
->x
.p
->size
; i
++)
1162 for (j
=o
; j
<e1
->x
.p
->size
; j
++) {
1165 evalue_copy(&ev
, &e1
->x
.p
->arr
[j
]);
1166 emul(&res
->x
.p
->arr
[i
], &ev
);
1167 eadd(&ev
, &tmp
.x
.p
->arr
[i
+j
-o
]);
1168 free_evalue_refs(&ev
);
1170 free_evalue_refs(res
);
1174 void emul_partitions (evalue
*e1
,evalue
*res
)
1179 s
= (struct section
*)
1180 malloc((e1
->x
.p
->size
/2) * (res
->x
.p
->size
/2) *
1181 sizeof(struct section
));
1185 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
1186 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1187 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1188 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1194 /* This code is only needed because the partitions
1195 are not true partitions.
1197 for (k
= 0; k
< n
; ++k
) {
1198 if (DomainIncludes(s
[k
].D
, d
))
1200 if (DomainIncludes(d
, s
[k
].D
)) {
1201 Domain_Free(s
[k
].D
);
1202 free_evalue_refs(&s
[k
].E
);
1213 value_init(s
[n
].E
.d
);
1214 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
1215 emul(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
1219 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
1220 value_clear(res
->x
.p
->arr
[2*i
].d
);
1221 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
1225 res
->x
.p
= new_enode(partition
, 2*n
, -1);
1226 for (j
= 0; j
< n
; ++j
) {
1227 s
[j
].D
= DomainConstraintSimplify(s
[j
].D
, 0);
1228 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1229 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1230 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1236 #define value_two_p(val) (mpz_cmp_si(val,2) == 0)
1238 /* Computes the product of two evalues "e1" and "res" and puts the result in "res". you must
1239 * do a copy of "res" befor calling this function if you nead it after. The vector type of
1240 * evalues is not treated here */
1242 void emul (evalue
*e1
, evalue
*res
){
1245 if((value_zero_p(e1
->d
)&&e1
->x
.p
->type
==evector
)||(value_zero_p(res
->d
)&&(res
->x
.p
->type
==evector
))) {
1246 fprintf(stderr
, "emul: do not proced on evector type !\n");
1250 if (value_zero_p(e1
->d
) && e1
->x
.p
->type
== partition
) {
1251 if (value_zero_p(res
->d
) && res
->x
.p
->type
== partition
)
1252 emul_partitions(e1
, res
);
1255 } else if (value_zero_p(res
->d
) && res
->x
.p
->type
== partition
) {
1256 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
)
1257 emul(e1
, &res
->x
.p
->arr
[2*i
+1]);
1259 if (value_zero_p(res
->d
) && res
->x
.p
->type
== relation
) {
1260 if (value_zero_p(e1
->d
) && e1
->x
.p
->type
== relation
&&
1261 eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0])) {
1262 if (res
->x
.p
->size
< 3 && e1
->x
.p
->size
== 3)
1263 explicit_complement(res
);
1264 if (e1
->x
.p
->size
< 3 && res
->x
.p
->size
== 3)
1265 explicit_complement(e1
);
1266 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1267 emul(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1270 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1271 emul(e1
, &res
->x
.p
->arr
[i
]);
1273 if(value_zero_p(e1
->d
)&& value_zero_p(res
->d
)) {
1274 switch(e1
->x
.p
->type
) {
1276 switch(res
->x
.p
->type
) {
1278 if(e1
->x
.p
->pos
== res
->x
.p
->pos
) {
1279 /* Product of two polynomials of the same variable */
1284 /* Product of two polynomials of different variables */
1286 if(res
->x
.p
->pos
< e1
->x
.p
->pos
)
1287 for( i
=0; i
<res
->x
.p
->size
; i
++)
1288 emul(e1
, &res
->x
.p
->arr
[i
]);
1296 /* Product of a polynomial and a periodic or fractional */
1301 switch(res
->x
.p
->type
) {
1303 if(e1
->x
.p
->pos
==res
->x
.p
->pos
&& e1
->x
.p
->size
==res
->x
.p
->size
) {
1304 /* Product of two periodics of the same parameter and period */
1306 for(i
=0; i
<res
->x
.p
->size
;i
++)
1307 emul(&(e1
->x
.p
->arr
[i
]), &(res
->x
.p
->arr
[i
]));
1312 if(e1
->x
.p
->pos
==res
->x
.p
->pos
&& e1
->x
.p
->size
!=res
->x
.p
->size
) {
1313 /* Product of two periodics of the same parameter and different periods */
1317 value_init(x
); value_init(y
);value_init(z
);
1320 value_set_si(x
,e1
->x
.p
->size
);
1321 value_set_si(y
,res
->x
.p
->size
);
1322 value_assign (z
,*Lcm(x
,y
));
1323 lcm
=(int)mpz_get_si(z
);
1324 newp
= (evalue
*) malloc (sizeof(evalue
));
1325 value_init(newp
->d
);
1326 value_set_si( newp
->d
,0);
1327 newp
->x
.p
=new_enode(periodic
,lcm
, e1
->x
.p
->pos
);
1328 for(i
=0;i
<lcm
;i
++) {
1329 evalue_copy(&newp
->x
.p
->arr
[i
],
1330 &res
->x
.p
->arr
[i
%iy
]);
1333 emul(&e1
->x
.p
->arr
[i
%ix
], &newp
->x
.p
->arr
[i
]);
1335 value_assign(res
->d
,newp
->d
);
1338 value_clear(x
); value_clear(y
);value_clear(z
);
1342 /* Product of two periodics of different parameters */
1344 if(res
->x
.p
->pos
< e1
->x
.p
->pos
)
1345 for(i
=0; i
<res
->x
.p
->size
; i
++)
1346 emul(e1
, &(res
->x
.p
->arr
[i
]));
1354 /* Product of a periodic and a polynomial */
1356 for(i
=0; i
<res
->x
.p
->size
; i
++)
1357 emul(e1
, &(res
->x
.p
->arr
[i
]));
1363 switch(res
->x
.p
->type
) {
1365 for(i
=0; i
<res
->x
.p
->size
; i
++)
1366 emul(e1
, &(res
->x
.p
->arr
[i
]));
1371 if (e1
->x
.p
->pos
== res
->x
.p
->pos
&&
1372 eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0])) {
1375 poly_denom(&e1
->x
.p
->arr
[0], &d
.d
);
1376 if (!value_two_p(d
.d
))
1380 value_set_si(d
.x
.n
, 1);
1382 /* { x }^2 == { x }/2 */
1383 /* a0 b0 + (a0 b1 + a1 b0 + a1 b1/2) { x } */
1384 assert(e1
->x
.p
->size
== 3);
1385 assert(res
->x
.p
->size
== 3);
1387 evalue_copy(&tmp
, &res
->x
.p
->arr
[2]);
1389 eadd(&res
->x
.p
->arr
[1], &tmp
);
1390 emul(&e1
->x
.p
->arr
[2], &tmp
);
1391 emul(&e1
->x
.p
->arr
[1], res
);
1392 eadd(&tmp
, &res
->x
.p
->arr
[2]);
1393 free_evalue_refs(&tmp
);
1398 if(mod_term_smaller(res
, e1
))
1399 for(i
=1; i
<res
->x
.p
->size
; i
++)
1400 emul(e1
, &(res
->x
.p
->arr
[i
]));
1415 if (value_notzero_p(e1
->d
)&& value_notzero_p(res
->d
)) {
1416 /* Product of two rational numbers */
1420 value_multiply(res
->d
,e1
->d
,res
->d
);
1421 value_multiply(res
->x
.n
,e1
->x
.n
,res
->x
.n
);
1422 Gcd(res
->x
.n
, res
->d
,&g
);
1423 if (value_notone_p(g
)) {
1424 value_division(res
->d
,res
->d
,g
);
1425 value_division(res
->x
.n
,res
->x
.n
,g
);
1431 if(value_zero_p(e1
->d
)&& value_notzero_p(res
->d
)) {
1432 /* Product of an expression (polynomial or peririodic) and a rational number */
1438 /* Product of a rationel number and an expression (polynomial or peririodic) */
1440 i
= res
->x
.p
->type
== fractional
? 1 : 0;
1441 for (; i
<res
->x
.p
->size
; i
++)
1442 emul(e1
, &res
->x
.p
->arr
[i
]);
1452 /* Frees mask content ! */
1453 void emask(evalue
*mask
, evalue
*res
) {
1459 if (EVALUE_IS_ZERO(*res
)) {
1460 free_evalue_refs(mask
);
1464 assert(value_zero_p(mask
->d
));
1465 assert(mask
->x
.p
->type
== partition
);
1466 assert(value_zero_p(res
->d
));
1467 assert(res
->x
.p
->type
== partition
);
1469 s
= (struct section
*)
1470 malloc((mask
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2) *
1471 sizeof(struct section
));
1475 evalue_set_si(&mone
, -1, 1);
1478 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1479 assert(mask
->x
.p
->size
>= 2);
1480 fd
= DomainDifference(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1481 EVALUE_DOMAIN(mask
->x
.p
->arr
[0]), 0);
1483 for (i
= 1; i
< mask
->x
.p
->size
/2; ++i
) {
1485 fd
= DomainDifference(fd
, EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1494 value_init(s
[n
].E
.d
);
1495 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1499 for (i
= 0; i
< mask
->x
.p
->size
/2; ++i
) {
1500 if (EVALUE_IS_ONE(mask
->x
.p
->arr
[2*i
+1]))
1503 fd
= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]);
1504 eadd(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1505 emul(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1506 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1508 d
= DomainIntersection(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1509 EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1515 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]), 0);
1516 if (t
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1518 value_init(s
[n
].E
.d
);
1519 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1520 emul(&mask
->x
.p
->arr
[2*i
+1], &s
[n
].E
);
1526 /* Just ignore; this may have been previously masked off */
1528 if (fd
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1532 free_evalue_refs(&mone
);
1533 free_evalue_refs(mask
);
1534 free_evalue_refs(res
);
1537 evalue_set_si(res
, 0, 1);
1539 res
->x
.p
= new_enode(partition
, 2*n
, -1);
1540 for (j
= 0; j
< n
; ++j
) {
1541 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1542 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1543 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1550 void evalue_copy(evalue
*dst
, evalue
*src
)
1552 value_assign(dst
->d
, src
->d
);
1553 if(value_notzero_p(src
->d
)) {
1554 value_init(dst
->x
.n
);
1555 value_assign(dst
->x
.n
, src
->x
.n
);
1557 dst
->x
.p
= ecopy(src
->x
.p
);
1560 enode
*new_enode(enode_type type
,int size
,int pos
) {
1566 fprintf(stderr
, "Allocating enode of size 0 !\n" );
1569 res
= (enode
*) malloc(sizeof(enode
) + (size
-1)*sizeof(evalue
));
1573 for(i
=0; i
<size
; i
++) {
1574 value_init(res
->arr
[i
].d
);
1575 value_set_si(res
->arr
[i
].d
,0);
1576 res
->arr
[i
].x
.p
= 0;
1581 enode
*ecopy(enode
*e
) {
1586 res
= new_enode(e
->type
,e
->size
,e
->pos
);
1587 for(i
=0;i
<e
->size
;++i
) {
1588 value_assign(res
->arr
[i
].d
,e
->arr
[i
].d
);
1589 if(value_zero_p(res
->arr
[i
].d
))
1590 res
->arr
[i
].x
.p
= ecopy(e
->arr
[i
].x
.p
);
1591 else if (EVALUE_IS_DOMAIN(res
->arr
[i
]))
1592 EVALUE_SET_DOMAIN(res
->arr
[i
], Domain_Copy(EVALUE_DOMAIN(e
->arr
[i
])));
1594 value_init(res
->arr
[i
].x
.n
);
1595 value_assign(res
->arr
[i
].x
.n
,e
->arr
[i
].x
.n
);
1601 int ecmp(const evalue
*e1
, const evalue
*e2
)
1607 if (value_notzero_p(e1
->d
) && value_notzero_p(e2
->d
)) {
1611 value_multiply(m
, e1
->x
.n
, e2
->d
);
1612 value_multiply(m2
, e2
->x
.n
, e1
->d
);
1614 if (value_lt(m
, m2
))
1616 else if (value_gt(m
, m2
))
1626 if (value_notzero_p(e1
->d
))
1628 if (value_notzero_p(e2
->d
))
1634 if (p1
->type
!= p2
->type
)
1635 return p1
->type
- p2
->type
;
1636 if (p1
->pos
!= p2
->pos
)
1637 return p1
->pos
- p2
->pos
;
1638 if (p1
->size
!= p2
->size
)
1639 return p1
->size
- p2
->size
;
1641 for (i
= p1
->size
-1; i
>= 0; --i
)
1642 if ((r
= ecmp(&p1
->arr
[i
], &p2
->arr
[i
])) != 0)
1648 int eequal(evalue
*e1
,evalue
*e2
) {
1653 if (value_ne(e1
->d
,e2
->d
))
1656 /* e1->d == e2->d */
1657 if (value_notzero_p(e1
->d
)) {
1658 if (value_ne(e1
->x
.n
,e2
->x
.n
))
1661 /* e1->d == e2->d != 0 AND e1->n == e2->n */
1665 /* e1->d == e2->d == 0 */
1668 if (p1
->type
!= p2
->type
) return 0;
1669 if (p1
->size
!= p2
->size
) return 0;
1670 if (p1
->pos
!= p2
->pos
) return 0;
1671 for (i
=0; i
<p1
->size
; i
++)
1672 if (!eequal(&p1
->arr
[i
], &p2
->arr
[i
]) )
1677 void free_evalue_refs(evalue
*e
) {
1682 if (EVALUE_IS_DOMAIN(*e
)) {
1683 Domain_Free(EVALUE_DOMAIN(*e
));
1686 } else if (value_pos_p(e
->d
)) {
1688 /* 'e' stores a constant */
1690 value_clear(e
->x
.n
);
1693 assert(value_zero_p(e
->d
));
1696 if (!p
) return; /* null pointer */
1697 for (i
=0; i
<p
->size
; i
++) {
1698 free_evalue_refs(&(p
->arr
[i
]));
1702 } /* free_evalue_refs */
1704 static void mod2table_r(evalue
*e
, Vector
*periods
, Value m
, int p
,
1705 Vector
* val
, evalue
*res
)
1707 unsigned nparam
= periods
->Size
;
1710 double d
= compute_evalue(e
, val
->p
);
1711 d
*= VALUE_TO_DOUBLE(m
);
1716 value_assign(res
->d
, m
);
1717 value_init(res
->x
.n
);
1718 value_set_double(res
->x
.n
, d
);
1719 mpz_fdiv_r(res
->x
.n
, res
->x
.n
, m
);
1722 if (value_one_p(periods
->p
[p
]))
1723 mod2table_r(e
, periods
, m
, p
+1, val
, res
);
1728 value_assign(tmp
, periods
->p
[p
]);
1729 value_set_si(res
->d
, 0);
1730 res
->x
.p
= new_enode(periodic
, VALUE_TO_INT(tmp
), p
+1);
1732 value_decrement(tmp
, tmp
);
1733 value_assign(val
->p
[p
], tmp
);
1734 mod2table_r(e
, periods
, m
, p
+1, val
,
1735 &res
->x
.p
->arr
[VALUE_TO_INT(tmp
)]);
1736 } while (value_pos_p(tmp
));
1742 static void rel2table(evalue
*e
, int zero
)
1744 if (value_pos_p(e
->d
)) {
1745 if (value_zero_p(e
->x
.n
) == zero
)
1746 value_set_si(e
->x
.n
, 1);
1748 value_set_si(e
->x
.n
, 0);
1749 value_set_si(e
->d
, 1);
1752 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
1753 rel2table(&e
->x
.p
->arr
[i
], zero
);
1757 void evalue_mod2table(evalue
*e
, int nparam
)
1762 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
1765 for (i
=0; i
<p
->size
; i
++) {
1766 evalue_mod2table(&(p
->arr
[i
]), nparam
);
1768 if (p
->type
== relation
) {
1773 evalue_copy(©
, &p
->arr
[0]);
1775 rel2table(&p
->arr
[0], 1);
1776 emul(&p
->arr
[0], &p
->arr
[1]);
1778 rel2table(©
, 0);
1779 emul(©
, &p
->arr
[2]);
1780 eadd(&p
->arr
[2], &p
->arr
[1]);
1781 free_evalue_refs(&p
->arr
[2]);
1782 free_evalue_refs(©
);
1784 free_evalue_refs(&p
->arr
[0]);
1788 } else if (p
->type
== fractional
) {
1789 Vector
*periods
= Vector_Alloc(nparam
);
1790 Vector
*val
= Vector_Alloc(nparam
);
1796 value_set_si(tmp
, 1);
1797 Vector_Set(periods
->p
, 1, nparam
);
1798 Vector_Set(val
->p
, 0, nparam
);
1799 for (ev
= &p
->arr
[0]; value_zero_p(ev
->d
); ev
= &ev
->x
.p
->arr
[0]) {
1802 assert(p
->type
== polynomial
);
1803 assert(p
->size
== 2);
1804 value_assign(periods
->p
[p
->pos
-1], p
->arr
[1].d
);
1805 Lcm3(tmp
, p
->arr
[1].d
, &tmp
);
1808 mod2table_r(&p
->arr
[0], periods
, tmp
, 0, val
, &EP
);
1811 evalue_set_si(&res
, 0, 1);
1812 /* Compute the polynomial using Horner's rule */
1813 for (i
=p
->size
-1;i
>1;i
--) {
1814 eadd(&p
->arr
[i
], &res
);
1817 eadd(&p
->arr
[1], &res
);
1819 free_evalue_refs(e
);
1820 free_evalue_refs(&EP
);
1825 Vector_Free(periods
);
1827 } /* evalue_mod2table */
1829 /********************************************************/
1830 /* function in domain */
1831 /* check if the parameters in list_args */
1832 /* verifies the constraints of Domain P */
1833 /********************************************************/
1834 int in_domain(Polyhedron
*P
, Value
*list_args
) {
1837 Value v
; /* value of the constraint of a row when
1838 parameters are instanciated*/
1844 /*P->Constraint constraint matrice of polyhedron P*/
1845 for(row
=0;row
<P
->NbConstraints
;row
++) {
1846 value_assign(v
,P
->Constraint
[row
][P
->Dimension
+1]); /*constant part*/
1847 for(col
=1;col
<P
->Dimension
+1;col
++) {
1848 value_multiply(tmp
,P
->Constraint
[row
][col
],list_args
[col
-1]);
1849 value_addto(v
,v
,tmp
);
1851 if (value_notzero_p(P
->Constraint
[row
][0])) {
1853 /*if v is not >=0 then this constraint is not respected */
1854 if (value_neg_p(v
)) {
1858 return P
->next
? in_domain(P
->next
, list_args
) : 0;
1863 /*if v is not = 0 then this constraint is not respected */
1864 if (value_notzero_p(v
))
1869 /*if not return before this point => all
1870 the constraints are respected */
1876 /****************************************************/
1877 /* function compute enode */
1878 /* compute the value of enode p with parameters */
1879 /* list "list_args */
1880 /* compute the polynomial or the periodic */
1881 /****************************************************/
1883 static double compute_enode(enode
*p
, Value
*list_args
) {
1895 if (p
->type
== polynomial
) {
1897 value_assign(param
,list_args
[p
->pos
-1]);
1899 /* Compute the polynomial using Horner's rule */
1900 for (i
=p
->size
-1;i
>0;i
--) {
1901 res
+=compute_evalue(&p
->arr
[i
],list_args
);
1902 res
*=VALUE_TO_DOUBLE(param
);
1904 res
+=compute_evalue(&p
->arr
[0],list_args
);
1906 else if (p
->type
== fractional
) {
1907 double d
= compute_evalue(&p
->arr
[0], list_args
);
1908 d
-= floor(d
+1e-10);
1910 /* Compute the polynomial using Horner's rule */
1911 for (i
=p
->size
-1;i
>1;i
--) {
1912 res
+=compute_evalue(&p
->arr
[i
],list_args
);
1915 res
+=compute_evalue(&p
->arr
[1],list_args
);
1917 else if (p
->type
== periodic
) {
1918 value_assign(param
,list_args
[p
->pos
-1]);
1920 /* Choose the right element of the periodic */
1921 value_absolute(m
,param
);
1922 value_set_si(param
,p
->size
);
1923 value_modulus(m
,m
,param
);
1924 res
= compute_evalue(&p
->arr
[VALUE_TO_INT(m
)],list_args
);
1926 else if (p
->type
== relation
) {
1927 if (fabs(compute_evalue(&p
->arr
[0], list_args
)) < 1e-10)
1928 res
= compute_evalue(&p
->arr
[1], list_args
);
1929 else if (p
->size
> 2)
1930 res
= compute_evalue(&p
->arr
[2], list_args
);
1932 else if (p
->type
== partition
) {
1933 for (i
= 0; i
< p
->size
/2; ++i
)
1934 if (in_domain(EVALUE_DOMAIN(p
->arr
[2*i
]), list_args
)) {
1935 res
= compute_evalue(&p
->arr
[2*i
+1], list_args
);
1942 } /* compute_enode */
1944 /*************************************************/
1945 /* return the value of Ehrhart Polynomial */
1946 /* It returns a double, because since it is */
1947 /* a recursive function, some intermediate value */
1948 /* might not be integral */
1949 /*************************************************/
1951 double compute_evalue(evalue
*e
,Value
*list_args
) {
1955 if (value_notzero_p(e
->d
)) {
1956 if (value_notone_p(e
->d
))
1957 res
= VALUE_TO_DOUBLE(e
->x
.n
) / VALUE_TO_DOUBLE(e
->d
);
1959 res
= VALUE_TO_DOUBLE(e
->x
.n
);
1962 res
= compute_enode(e
->x
.p
,list_args
);
1964 } /* compute_evalue */
1967 /****************************************************/
1968 /* function compute_poly : */
1969 /* Check for the good validity domain */
1970 /* return the number of point in the Polyhedron */
1971 /* in allocated memory */
1972 /* Using the Ehrhart pseudo-polynomial */
1973 /****************************************************/
1974 Value
*compute_poly(Enumeration
*en
,Value
*list_args
) {
1977 /* double d; int i; */
1979 tmp
= (Value
*) malloc (sizeof(Value
));
1980 assert(tmp
!= NULL
);
1982 value_set_si(*tmp
,0);
1985 return(tmp
); /* no ehrhart polynomial */
1986 if(en
->ValidityDomain
) {
1987 if(!en
->ValidityDomain
->Dimension
) { /* no parameters */
1988 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
1993 return(tmp
); /* no Validity Domain */
1995 if(in_domain(en
->ValidityDomain
,list_args
)) {
1997 #ifdef EVAL_EHRHART_DEBUG
1998 Print_Domain(stdout
,en
->ValidityDomain
);
1999 print_evalue(stdout
,&en
->EP
);
2002 /* d = compute_evalue(&en->EP,list_args);
2004 printf("(double)%lf = %d\n", d, i ); */
2005 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
2011 value_set_si(*tmp
,0);
2012 return(tmp
); /* no compatible domain with the arguments */
2013 } /* compute_poly */
2015 size_t value_size(Value v
) {
2016 return (v
[0]._mp_size
> 0 ? v
[0]._mp_size
: -v
[0]._mp_size
)
2017 * sizeof(v
[0]._mp_d
[0]);
2020 size_t domain_size(Polyhedron
*D
)
2023 size_t s
= sizeof(*D
);
2025 for (i
= 0; i
< D
->NbConstraints
; ++i
)
2026 for (j
= 0; j
< D
->Dimension
+2; ++j
)
2027 s
+= value_size(D
->Constraint
[i
][j
]);
2030 for (i = 0; i < D->NbRays; ++i)
2031 for (j = 0; j < D->Dimension+2; ++j)
2032 s += value_size(D->Ray[i][j]);
2035 return D
->next
? s
+domain_size(D
->next
) : s
;
2038 size_t enode_size(enode
*p
) {
2039 size_t s
= sizeof(*p
) - sizeof(p
->arr
[0]);
2042 if (p
->type
== partition
)
2043 for (i
= 0; i
< p
->size
/2; ++i
) {
2044 s
+= domain_size(EVALUE_DOMAIN(p
->arr
[2*i
]));
2045 s
+= evalue_size(&p
->arr
[2*i
+1]);
2048 for (i
= 0; i
< p
->size
; ++i
) {
2049 s
+= evalue_size(&p
->arr
[i
]);
2054 size_t evalue_size(evalue
*e
)
2056 size_t s
= sizeof(*e
);
2057 s
+= value_size(e
->d
);
2058 if (value_notzero_p(e
->d
))
2059 s
+= value_size(e
->x
.n
);
2061 s
+= enode_size(e
->x
.p
);
2065 static evalue
*find_second(evalue
*base
, evalue
*cst
, evalue
*e
, Value m
)
2067 evalue
*found
= NULL
;
2072 if (value_pos_p(e
->d
) || e
->x
.p
->type
!= fractional
)
2075 value_init(offset
.d
);
2076 value_init(offset
.x
.n
);
2077 poly_denom(&e
->x
.p
->arr
[0], &offset
.d
);
2078 Lcm3(m
, offset
.d
, &offset
.d
);
2079 value_set_si(offset
.x
.n
, 1);
2082 evalue_copy(©
, cst
);
2085 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2087 if (eequal(base
, &e
->x
.p
->arr
[0]))
2088 found
= &e
->x
.p
->arr
[0];
2090 value_set_si(offset
.x
.n
, -2);
2093 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2095 if (eequal(base
, &e
->x
.p
->arr
[0]))
2098 free_evalue_refs(cst
);
2099 free_evalue_refs(&offset
);
2102 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2103 found
= find_second(base
, cst
, &e
->x
.p
->arr
[i
], m
);
2108 static evalue
*find_relation_pair(evalue
*e
)
2111 evalue
*found
= NULL
;
2113 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
2116 if (e
->x
.p
->type
== fractional
) {
2121 poly_denom(&e
->x
.p
->arr
[0], &m
);
2123 for (cst
= &e
->x
.p
->arr
[0]; value_zero_p(cst
->d
);
2124 cst
= &cst
->x
.p
->arr
[0])
2127 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2128 found
= find_second(&e
->x
.p
->arr
[0], cst
, &e
->x
.p
->arr
[i
], m
);
2133 i
= e
->x
.p
->type
== relation
;
2134 for (; !found
&& i
< e
->x
.p
->size
; ++i
)
2135 found
= find_relation_pair(&e
->x
.p
->arr
[i
]);
2140 void evalue_mod2relation(evalue
*e
) {
2143 if (value_zero_p(e
->d
) && e
->x
.p
->type
== partition
) {
2146 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2147 evalue_mod2relation(&e
->x
.p
->arr
[2*i
+1]);
2148 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
2149 value_clear(e
->x
.p
->arr
[2*i
].d
);
2150 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2152 if (2*i
< e
->x
.p
->size
) {
2153 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2154 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2159 if (e
->x
.p
->size
== 0) {
2161 evalue_set_si(e
, 0, 1);
2167 while ((d
= find_relation_pair(e
)) != NULL
) {
2171 value_init(split
.d
);
2172 value_set_si(split
.d
, 0);
2173 split
.x
.p
= new_enode(relation
, 3, 0);
2174 evalue_set_si(&split
.x
.p
->arr
[1], 1, 1);
2175 evalue_set_si(&split
.x
.p
->arr
[2], 1, 1);
2177 ev
= &split
.x
.p
->arr
[0];
2178 value_set_si(ev
->d
, 0);
2179 ev
->x
.p
= new_enode(fractional
, 3, -1);
2180 evalue_set_si(&ev
->x
.p
->arr
[1], 0, 1);
2181 evalue_set_si(&ev
->x
.p
->arr
[2], 1, 1);
2182 evalue_copy(&ev
->x
.p
->arr
[0], d
);
2188 free_evalue_refs(&split
);
2192 static int evalue_comp(const void * a
, const void * b
)
2194 const evalue
*e1
= *(const evalue
**)a
;
2195 const evalue
*e2
= *(const evalue
**)b
;
2196 return ecmp(e1
, e2
);
2199 void evalue_combine(evalue
*e
)
2206 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
2209 NALLOC(evs
, e
->x
.p
->size
/2);
2210 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2211 evs
[i
] = &e
->x
.p
->arr
[2*i
+1];
2212 qsort(evs
, e
->x
.p
->size
/2, sizeof(evs
[0]), evalue_comp
);
2213 p
= new_enode(partition
, e
->x
.p
->size
, -1);
2214 for (i
= 0, k
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2215 if (k
== 0 || ecmp(&p
->arr
[2*k
-1], evs
[i
]) != 0) {
2216 value_clear(p
->arr
[2*k
].d
);
2217 value_clear(p
->arr
[2*k
+1].d
);
2218 p
->arr
[2*k
] = *(evs
[i
]-1);
2219 p
->arr
[2*k
+1] = *(evs
[i
]);
2222 Polyhedron
*D
= EVALUE_DOMAIN(*(evs
[i
]-1));
2225 value_clear((evs
[i
]-1)->d
);
2229 L
->next
= EVALUE_DOMAIN(p
->arr
[2*k
-2]);
2230 EVALUE_SET_DOMAIN(p
->arr
[2*k
-2], D
);
2231 free_evalue_refs(evs
[i
]);
2235 for (i
= 2*k
; i
< p
->size
; ++i
)
2236 value_clear(p
->arr
[i
].d
);
2243 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2245 if (value_notzero_p(e
->x
.p
->arr
[2*i
+1].d
))
2247 H
= DomainConvex(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), 0);
2250 for (k
= 0; k
< e
->x
.p
->size
/2; ++k
) {
2251 Polyhedron
*D
, *N
, **P
;
2254 P
= &EVALUE_DOMAIN(e
->x
.p
->arr
[2*k
]);
2261 if (D
->NbEq
<= H
->NbEq
) {
2267 tmp
.x
.p
= new_enode(partition
, 2, -1);
2268 EVALUE_SET_DOMAIN(tmp
.x
.p
->arr
[0], Polyhedron_Copy(D
));
2269 evalue_copy(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*i
+1]);
2270 reduce_evalue(&tmp
);
2271 if (value_notzero_p(tmp
.d
) ||
2272 ecmp(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*k
+1]) != 0)
2275 D
->next
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2276 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]) = D
;
2279 free_evalue_refs(&tmp
);
2285 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2287 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2289 value_clear(e
->x
.p
->arr
[2*i
].d
);
2290 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2292 if (2*i
< e
->x
.p
->size
) {
2293 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2294 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2301 H
= DomainConvex(D
, 0);
2302 E
= DomainDifference(H
, D
, 0);
2304 D
= DomainDifference(H
, E
, 0);
2307 EVALUE_SET_DOMAIN(p
->arr
[2*i
], D
);
2311 /* May change coefficients to become non-standard
2312 * => reduce p afterwards to correct
2314 static Polyhedron
*polynomial_projection(enode
*p
, Polyhedron
*D
, Value
*d
,
2319 unsigned dim
= D
->Dimension
;
2320 Matrix
*T
= Matrix_Alloc(2, dim
+1);
2325 assert(p
->type
== fractional
);
2327 value_set_si(T
->p
[1][dim
], 1);
2329 while (value_zero_p(pp
->d
)) {
2330 assert(pp
->x
.p
->type
== polynomial
);
2331 assert(pp
->x
.p
->size
== 2);
2332 assert(value_notzero_p(pp
->x
.p
->arr
[1].d
));
2333 value_division(T
->p
[0][pp
->x
.p
->pos
-1], *d
, pp
->x
.p
->arr
[1].d
);
2334 mpz_mul_ui(twice
, pp
->x
.p
->arr
[1].x
.n
, 2);
2335 if (value_gt(twice
, pp
->x
.p
->arr
[1].d
))
2336 value_substract(pp
->x
.p
->arr
[1].x
.n
,
2337 pp
->x
.p
->arr
[1].x
.n
, pp
->x
.p
->arr
[1].d
);
2338 value_multiply(T
->p
[0][pp
->x
.p
->pos
-1],
2339 T
->p
[0][pp
->x
.p
->pos
-1], pp
->x
.p
->arr
[1].x
.n
);
2340 pp
= &pp
->x
.p
->arr
[0];
2342 value_division(T
->p
[0][dim
], *d
, pp
->d
);
2343 value_multiply(T
->p
[0][dim
], T
->p
[0][dim
], pp
->x
.n
);
2344 I
= DomainImage(D
, T
, 0);
2345 H
= DomainConvex(I
, 0);
2354 static int reduce_in_domain(evalue
*e
, Polyhedron
*D
)
2363 if (value_notzero_p(e
->d
))
2368 if (p
->type
== relation
) {
2374 I
= polynomial_projection(p
->arr
[0].x
.p
, D
, &d
, &T
);
2375 line_minmax(I
, &min
, &max
); /* frees I */
2376 equal
= value_eq(min
, max
);
2377 mpz_cdiv_q(min
, min
, d
);
2378 mpz_fdiv_q(max
, max
, d
);
2380 if (value_gt(min
, max
)) {
2386 evalue_set_si(e
, 0, 1);
2389 free_evalue_refs(&(p
->arr
[1]));
2390 free_evalue_refs(&(p
->arr
[0]));
2396 return r
? r
: reduce_in_domain(e
, D
);
2400 free_evalue_refs(&(p
->arr
[2]));
2403 free_evalue_refs(&(p
->arr
[0]));
2409 return reduce_in_domain(e
, D
);
2410 } else if (value_eq(min
, max
)) {
2411 /* zero for a single value */
2413 Matrix
*M
= Matrix_Alloc(1, D
->Dimension
+2);
2414 Vector_Copy(T
->p
[0], M
->p
[0]+1, D
->Dimension
+1);
2415 value_multiply(min
, min
, d
);
2416 value_substract(M
->p
[0][D
->Dimension
+1],
2417 M
->p
[0][D
->Dimension
+1], min
);
2418 E
= DomainAddConstraints(D
, M
, 0);
2424 r
= reduce_in_domain(&p
->arr
[1], E
);
2426 r
|= reduce_in_domain(&p
->arr
[2], D
);
2428 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2436 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2439 i
= p
->type
== relation
? 1 :
2440 p
->type
== fractional
? 1 : 0;
2441 for (; i
<p
->size
; i
++)
2442 r
|= reduce_in_domain(&p
->arr
[i
], D
);
2444 if (p
->type
!= fractional
) {
2445 if (r
&& p
->type
== polynomial
) {
2448 value_set_si(f
.d
, 0);
2449 f
.x
.p
= new_enode(polynomial
, 2, p
->pos
);
2450 evalue_set_si(&f
.x
.p
->arr
[0], 0, 1);
2451 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
2452 reorder_terms(p
, &f
);
2463 I
= polynomial_projection(p
, D
, &d
, &T
);
2465 line_minmax(I
, &min
, &max
); /* frees I */
2466 mpz_fdiv_q(min
, min
, d
);
2467 mpz_fdiv_q(max
, max
, d
);
2469 if (value_eq(min
, max
)) {
2472 value_init(inc
.x
.n
);
2473 value_set_si(inc
.d
, 1);
2474 value_oppose(inc
.x
.n
, min
);
2475 eadd(&inc
, &p
->arr
[0]);
2476 reorder_terms(p
, &p
->arr
[0]); /* frees arr[0] */
2480 free_evalue_refs(&inc
);
2483 _reduce_evalue(&p
->arr
[0], 0, 1);
2487 value_set_si(f
.d
, 0);
2488 f
.x
.p
= new_enode(fractional
, 3, -1);
2489 value_clear(f
.x
.p
->arr
[0].d
);
2490 f
.x
.p
->arr
[0] = p
->arr
[0];
2491 evalue_set_si(&f
.x
.p
->arr
[1], 0, 1);
2492 evalue_set_si(&f
.x
.p
->arr
[2], 1, 1);
2493 reorder_terms(p
, &f
);
2507 void evalue_range_reduction(evalue
*e
)
2510 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
2513 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2514 if (reduce_in_domain(&e
->x
.p
->arr
[2*i
+1],
2515 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]))) {
2516 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
2518 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
2519 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2520 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
2521 value_clear(e
->x
.p
->arr
[2*i
].d
);
2523 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2524 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];