1 /***********************************************************************/
2 /* copyright 1997, Doran Wilde */
3 /* copyright 1997-2000, Vincent Loechner */
4 /* copyright 2003-2006, Sven Verdoolaege */
5 /* Permission is granted to copy, use, and distribute */
6 /* for any commercial or noncommercial purpose under the terms */
7 /* of the GNU General Public license, version 2, June 1991 */
8 /* (see file : LICENSE). */
9 /***********************************************************************/
16 #include <barvinok/evalue.h>
17 #include <barvinok/barvinok.h>
18 #include <barvinok/util.h>
21 #ifndef value_pmodulus
22 #define value_pmodulus(ref,val1,val2) (mpz_fdiv_r((ref),(val1),(val2)))
25 #define ALLOC(type) (type*)malloc(sizeof(type))
26 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
29 #define NALLOC(p,n) p = (typeof(p))malloc((n) * sizeof(*p))
31 #define NALLOC(p,n) p = (void *)malloc((n) * sizeof(*p))
34 void evalue_set_si(evalue
*ev
, int n
, int d
) {
35 value_set_si(ev
->d
, d
);
37 value_set_si(ev
->x
.n
, n
);
40 void evalue_set(evalue
*ev
, Value n
, Value d
) {
41 value_assign(ev
->d
, d
);
43 value_assign(ev
->x
.n
, n
);
46 void evalue_set_reduce(evalue
*ev
, Value n
, Value d
) {
48 value_gcd(ev
->x
.n
, n
, d
);
49 value_divexact(ev
->d
, d
, ev
->x
.n
);
50 value_divexact(ev
->x
.n
, n
, ev
->x
.n
);
55 evalue
*EP
= ALLOC(evalue
);
57 evalue_set_si(EP
, 0, 1);
63 evalue
*EP
= ALLOC(evalue
);
65 value_set_si(EP
->d
, -2);
70 /* returns an evalue that corresponds to
74 evalue
*evalue_var(int var
)
76 evalue
*EP
= ALLOC(evalue
);
78 value_set_si(EP
->d
,0);
79 EP
->x
.p
= new_enode(polynomial
, 2, var
+ 1);
80 evalue_set_si(&EP
->x
.p
->arr
[0], 0, 1);
81 evalue_set_si(&EP
->x
.p
->arr
[1], 1, 1);
85 void aep_evalue(evalue
*e
, int *ref
) {
90 if (value_notzero_p(e
->d
))
91 return; /* a rational number, its already reduced */
93 return; /* hum... an overflow probably occured */
95 /* First check the components of p */
96 for (i
=0;i
<p
->size
;i
++)
97 aep_evalue(&p
->arr
[i
],ref
);
104 p
->pos
= ref
[p
->pos
-1]+1;
110 void addeliminatedparams_evalue(evalue
*e
,Matrix
*CT
) {
116 if (value_notzero_p(e
->d
))
117 return; /* a rational number, its already reduced */
119 return; /* hum... an overflow probably occured */
122 ref
= (int *)malloc(sizeof(int)*(CT
->NbRows
-1));
123 for(i
=0;i
<CT
->NbRows
-1;i
++)
124 for(j
=0;j
<CT
->NbColumns
;j
++)
125 if(value_notzero_p(CT
->p
[i
][j
])) {
130 /* Transform the references in e, using ref */
134 } /* addeliminatedparams_evalue */
136 static void addeliminatedparams_partition(enode
*p
, Matrix
*CT
, Polyhedron
*CEq
,
137 unsigned nparam
, unsigned MaxRays
)
140 assert(p
->type
== partition
);
143 for (i
= 0; i
< p
->size
/2; i
++) {
144 Polyhedron
*D
= EVALUE_DOMAIN(p
->arr
[2*i
]);
145 Polyhedron
*T
= DomainPreimage(D
, CT
, MaxRays
);
149 T
= DomainIntersection(D
, CEq
, MaxRays
);
152 EVALUE_SET_DOMAIN(p
->arr
[2*i
], T
);
156 void addeliminatedparams_enum(evalue
*e
, Matrix
*CT
, Polyhedron
*CEq
,
157 unsigned MaxRays
, unsigned nparam
)
162 if (CT
->NbRows
== CT
->NbColumns
)
165 if (EVALUE_IS_ZERO(*e
))
168 if (value_notzero_p(e
->d
)) {
171 value_set_si(res
.d
, 0);
172 res
.x
.p
= new_enode(partition
, 2, nparam
);
173 EVALUE_SET_DOMAIN(res
.x
.p
->arr
[0],
174 DomainConstraintSimplify(Polyhedron_Copy(CEq
), MaxRays
));
175 value_clear(res
.x
.p
->arr
[1].d
);
176 res
.x
.p
->arr
[1] = *e
;
184 addeliminatedparams_partition(p
, CT
, CEq
, nparam
, MaxRays
);
185 for (i
= 0; i
< p
->size
/2; i
++)
186 addeliminatedparams_evalue(&p
->arr
[2*i
+1], CT
);
189 static int mod_rational_cmp(evalue
*e1
, evalue
*e2
)
197 assert(value_notzero_p(e1
->d
));
198 assert(value_notzero_p(e2
->d
));
199 value_multiply(m
, e1
->x
.n
, e2
->d
);
200 value_multiply(m2
, e2
->x
.n
, e1
->d
);
203 else if (value_gt(m
, m2
))
213 static int mod_term_cmp_r(evalue
*e1
, evalue
*e2
)
215 if (value_notzero_p(e1
->d
)) {
217 if (value_zero_p(e2
->d
))
219 return mod_rational_cmp(e1
, e2
);
221 if (value_notzero_p(e2
->d
))
223 if (e1
->x
.p
->pos
< e2
->x
.p
->pos
)
225 else if (e1
->x
.p
->pos
> e2
->x
.p
->pos
)
228 int r
= mod_rational_cmp(&e1
->x
.p
->arr
[1], &e2
->x
.p
->arr
[1]);
230 ? mod_term_cmp_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0])
235 static int mod_term_cmp(const evalue
*e1
, const evalue
*e2
)
237 assert(value_zero_p(e1
->d
));
238 assert(value_zero_p(e2
->d
));
239 assert(e1
->x
.p
->type
== fractional
|| e1
->x
.p
->type
== flooring
);
240 assert(e2
->x
.p
->type
== fractional
|| e2
->x
.p
->type
== flooring
);
241 return mod_term_cmp_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]);
244 static void check_order(const evalue
*e
)
249 if (value_notzero_p(e
->d
))
252 switch (e
->x
.p
->type
) {
254 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
255 check_order(&e
->x
.p
->arr
[2*i
+1]);
258 for (i
= 1; i
< e
->x
.p
->size
; ++i
) {
260 if (value_notzero_p(a
->d
))
262 switch (a
->x
.p
->type
) {
264 assert(mod_term_cmp(&e
->x
.p
->arr
[0], &a
->x
.p
->arr
[0]) < 0);
273 for (i
= 0; i
< e
->x
.p
->size
; ++i
) {
275 if (value_notzero_p(a
->d
))
277 switch (a
->x
.p
->type
) {
279 assert(e
->x
.p
->pos
< a
->x
.p
->pos
);
290 for (i
= 1; i
< e
->x
.p
->size
; ++i
) {
292 if (value_notzero_p(a
->d
))
294 switch (a
->x
.p
->type
) {
305 /* Negative pos means inequality */
306 /* s is negative of substitution if m is not zero */
315 struct fixed_param
*fixed
;
320 static int relations_depth(evalue
*e
)
325 value_zero_p(e
->d
) && e
->x
.p
->type
== relation
;
326 e
= &e
->x
.p
->arr
[1], ++d
);
330 static void poly_denom_not_constant(evalue
**pp
, Value
*d
)
335 while (value_zero_p(p
->d
)) {
336 assert(p
->x
.p
->type
== polynomial
);
337 assert(p
->x
.p
->size
== 2);
338 assert(value_notzero_p(p
->x
.p
->arr
[1].d
));
339 value_lcm(*d
, *d
, p
->x
.p
->arr
[1].d
);
345 static void poly_denom(evalue
*p
, Value
*d
)
347 poly_denom_not_constant(&p
, d
);
348 value_lcm(*d
, *d
, p
->d
);
351 static void realloc_substitution(struct subst
*s
, int d
)
353 struct fixed_param
*n
;
356 for (i
= 0; i
< s
->n
; ++i
)
363 static int add_modulo_substitution(struct subst
*s
, evalue
*r
)
369 assert(value_zero_p(r
->d
) && r
->x
.p
->type
== relation
);
372 /* May have been reduced already */
373 if (value_notzero_p(m
->d
))
376 assert(value_zero_p(m
->d
) && m
->x
.p
->type
== fractional
);
377 assert(m
->x
.p
->size
== 3);
379 /* fractional was inverted during reduction
380 * invert it back and move constant in
382 if (!EVALUE_IS_ONE(m
->x
.p
->arr
[2])) {
383 assert(value_pos_p(m
->x
.p
->arr
[2].d
));
384 assert(value_mone_p(m
->x
.p
->arr
[2].x
.n
));
385 value_set_si(m
->x
.p
->arr
[2].x
.n
, 1);
386 value_increment(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].x
.n
);
387 assert(value_eq(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].d
));
388 value_set_si(m
->x
.p
->arr
[1].x
.n
, 1);
389 eadd(&m
->x
.p
->arr
[1], &m
->x
.p
->arr
[0]);
390 value_set_si(m
->x
.p
->arr
[1].x
.n
, 0);
391 value_set_si(m
->x
.p
->arr
[1].d
, 1);
394 /* Oops. Nested identical relations. */
395 if (!EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
398 if (s
->n
>= s
->max
) {
399 int d
= relations_depth(r
);
400 realloc_substitution(s
, d
);
404 assert(value_zero_p(p
->d
) && p
->x
.p
->type
== polynomial
);
405 assert(p
->x
.p
->size
== 2);
408 assert(value_pos_p(f
->x
.n
));
410 value_init(s
->fixed
[s
->n
].m
);
411 value_assign(s
->fixed
[s
->n
].m
, f
->d
);
412 s
->fixed
[s
->n
].pos
= p
->x
.p
->pos
;
413 value_init(s
->fixed
[s
->n
].d
);
414 value_assign(s
->fixed
[s
->n
].d
, f
->x
.n
);
415 value_init(s
->fixed
[s
->n
].s
.d
);
416 evalue_copy(&s
->fixed
[s
->n
].s
, &p
->x
.p
->arr
[0]);
422 static int type_offset(enode
*p
)
424 return p
->type
== fractional
? 1 :
425 p
->type
== flooring
? 1 :
426 p
->type
== relation
? 1 : 0;
429 static void reorder_terms_about(enode
*p
, evalue
*v
)
432 int offset
= type_offset(p
);
434 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
436 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
437 free_evalue_refs(&(p
->arr
[i
]));
443 void evalue_reorder_terms(evalue
*e
)
449 assert(value_zero_p(e
->d
));
451 assert(p
->type
== fractional
||
452 p
->type
== flooring
||
453 p
->type
== polynomial
); /* for now */
455 offset
= type_offset(p
);
457 value_set_si(f
.d
, 0);
458 f
.x
.p
= new_enode(p
->type
, offset
+2, p
->pos
);
460 value_clear(f
.x
.p
->arr
[0].d
);
461 f
.x
.p
->arr
[0] = p
->arr
[0];
463 evalue_set_si(&f
.x
.p
->arr
[offset
], 0, 1);
464 evalue_set_si(&f
.x
.p
->arr
[offset
+1], 1, 1);
465 reorder_terms_about(p
, &f
);
471 static void evalue_reduce_size(evalue
*e
)
475 assert(value_zero_p(e
->d
));
478 offset
= type_offset(p
);
480 /* Try to reduce the degree */
481 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
482 if (!EVALUE_IS_ZERO(p
->arr
[i
]))
484 free_evalue_refs(&p
->arr
[i
]);
489 /* Try to reduce its strength */
490 if (p
->type
== relation
) {
492 free_evalue_refs(&p
->arr
[0]);
493 evalue_set_si(e
, 0, 1);
496 } else if (p
->size
== offset
+1) {
498 memcpy(e
, &p
->arr
[offset
], sizeof(evalue
));
500 free_evalue_refs(&p
->arr
[0]);
505 void _reduce_evalue (evalue
*e
, struct subst
*s
, int fract
) {
511 if (value_notzero_p(e
->d
)) {
513 mpz_fdiv_r(e
->x
.n
, e
->x
.n
, e
->d
);
514 return; /* a rational number, its already reduced */
518 return; /* hum... an overflow probably occured */
520 /* First reduce the components of p */
521 add
= p
->type
== relation
;
522 for (i
=0; i
<p
->size
; i
++) {
524 add
= add_modulo_substitution(s
, e
);
526 if (i
== 0 && p
->type
==fractional
)
527 _reduce_evalue(&p
->arr
[i
], s
, 1);
529 _reduce_evalue(&p
->arr
[i
], s
, fract
);
531 if (add
&& i
== p
->size
-1) {
533 value_clear(s
->fixed
[s
->n
].m
);
534 value_clear(s
->fixed
[s
->n
].d
);
535 free_evalue_refs(&s
->fixed
[s
->n
].s
);
536 } else if (add
&& i
== 1)
537 s
->fixed
[s
->n
-1].pos
*= -1;
540 if (p
->type
==periodic
) {
542 /* Try to reduce the period */
543 for (i
=1; i
<=(p
->size
)/2; i
++) {
544 if ((p
->size
% i
)==0) {
546 /* Can we reduce the size to i ? */
548 for (k
=j
+i
; k
<e
->x
.p
->size
; k
+=i
)
549 if (!eequal(&p
->arr
[j
], &p
->arr
[k
])) goto you_lose
;
552 for (j
=i
; j
<p
->size
; j
++) free_evalue_refs(&p
->arr
[j
]);
556 you_lose
: /* OK, lets not do it */
561 /* Try to reduce its strength */
564 memcpy(e
,&p
->arr
[0],sizeof(evalue
));
568 else if (p
->type
==polynomial
) {
569 for (k
= 0; s
&& k
< s
->n
; ++k
) {
570 if (s
->fixed
[k
].pos
== p
->pos
) {
571 int divide
= value_notone_p(s
->fixed
[k
].d
);
574 if (value_notzero_p(s
->fixed
[k
].m
)) {
577 assert(p
->size
== 2);
578 if (divide
&& value_ne(s
->fixed
[k
].d
, p
->arr
[1].x
.n
))
580 if (!mpz_divisible_p(s
->fixed
[k
].m
, p
->arr
[1].d
))
587 value_assign(d
.d
, s
->fixed
[k
].d
);
589 if (value_notzero_p(s
->fixed
[k
].m
))
590 value_oppose(d
.x
.n
, s
->fixed
[k
].m
);
592 value_set_si(d
.x
.n
, 1);
595 for (i
=p
->size
-1;i
>=1;i
--) {
596 emul(&s
->fixed
[k
].s
, &p
->arr
[i
]);
598 emul(&d
, &p
->arr
[i
]);
599 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
600 free_evalue_refs(&(p
->arr
[i
]));
603 _reduce_evalue(&p
->arr
[0], s
, fract
);
606 free_evalue_refs(&d
);
612 evalue_reduce_size(e
);
614 else if (p
->type
==fractional
) {
618 if (value_notzero_p(p
->arr
[0].d
)) {
620 value_assign(v
.d
, p
->arr
[0].d
);
622 mpz_fdiv_r(v
.x
.n
, p
->arr
[0].x
.n
, p
->arr
[0].d
);
627 evalue
*pp
= &p
->arr
[0];
628 assert(value_zero_p(pp
->d
) && pp
->x
.p
->type
== polynomial
);
629 assert(pp
->x
.p
->size
== 2);
631 /* search for exact duplicate among the modulo inequalities */
633 f
= &pp
->x
.p
->arr
[1];
634 for (k
= 0; s
&& k
< s
->n
; ++k
) {
635 if (-s
->fixed
[k
].pos
== pp
->x
.p
->pos
&&
636 value_eq(s
->fixed
[k
].d
, f
->x
.n
) &&
637 value_eq(s
->fixed
[k
].m
, f
->d
) &&
638 eequal(&s
->fixed
[k
].s
, &pp
->x
.p
->arr
[0]))
645 /* replace { E/m } by { (E-1)/m } + 1/m */
650 evalue_set_si(&extra
, 1, 1);
651 value_assign(extra
.d
, g
);
652 eadd(&extra
, &v
.x
.p
->arr
[1]);
653 free_evalue_refs(&extra
);
655 /* We've been going in circles; stop now */
656 if (value_ge(v
.x
.p
->arr
[1].x
.n
, v
.x
.p
->arr
[1].d
)) {
657 free_evalue_refs(&v
);
659 evalue_set_si(&v
, 0, 1);
664 value_set_si(v
.d
, 0);
665 v
.x
.p
= new_enode(fractional
, 3, -1);
666 evalue_set_si(&v
.x
.p
->arr
[1], 1, 1);
667 value_assign(v
.x
.p
->arr
[1].d
, g
);
668 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
669 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
672 for (f
= &v
.x
.p
->arr
[0]; value_zero_p(f
->d
);
675 value_division(f
->d
, g
, f
->d
);
676 value_multiply(f
->x
.n
, f
->x
.n
, f
->d
);
677 value_assign(f
->d
, g
);
678 value_decrement(f
->x
.n
, f
->x
.n
);
679 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
681 value_gcd(g
, f
->d
, f
->x
.n
);
682 value_division(f
->d
, f
->d
, g
);
683 value_division(f
->x
.n
, f
->x
.n
, g
);
692 /* reduction may have made this fractional arg smaller */
693 i
= reorder
? p
->size
: 1;
694 for ( ; i
< p
->size
; ++i
)
695 if (value_zero_p(p
->arr
[i
].d
) &&
696 p
->arr
[i
].x
.p
->type
== fractional
&&
697 mod_term_cmp(e
, &p
->arr
[i
]) >= 0)
701 value_set_si(v
.d
, 0);
702 v
.x
.p
= new_enode(fractional
, 3, -1);
703 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
704 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
705 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
713 evalue
*pp
= &p
->arr
[0];
716 poly_denom_not_constant(&pp
, &m
);
717 mpz_fdiv_r(r
, m
, pp
->d
);
718 if (value_notzero_p(r
)) {
720 value_set_si(v
.d
, 0);
721 v
.x
.p
= new_enode(fractional
, 3, -1);
723 value_multiply(r
, m
, pp
->x
.n
);
724 value_multiply(v
.x
.p
->arr
[1].d
, m
, pp
->d
);
725 value_init(v
.x
.p
->arr
[1].x
.n
);
726 mpz_fdiv_r(v
.x
.p
->arr
[1].x
.n
, r
, pp
->d
);
727 mpz_fdiv_q(r
, r
, pp
->d
);
729 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
730 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
732 while (value_zero_p(pp
->d
))
733 pp
= &pp
->x
.p
->arr
[0];
735 value_assign(pp
->d
, m
);
736 value_assign(pp
->x
.n
, r
);
738 value_gcd(r
, pp
->d
, pp
->x
.n
);
739 value_division(pp
->d
, pp
->d
, r
);
740 value_division(pp
->x
.n
, pp
->x
.n
, r
);
753 for (pp
= &p
->arr
[0]; value_zero_p(pp
->d
);
754 pp
= &pp
->x
.p
->arr
[0]) {
755 f
= &pp
->x
.p
->arr
[1];
756 assert(value_pos_p(f
->d
));
757 mpz_mul_ui(twice
, f
->x
.n
, 2);
758 if (value_lt(twice
, f
->d
))
760 if (value_eq(twice
, f
->d
))
768 value_set_si(v
.d
, 0);
769 v
.x
.p
= new_enode(fractional
, 3, -1);
770 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
771 poly_denom(&p
->arr
[0], &twice
);
772 value_assign(v
.x
.p
->arr
[1].d
, twice
);
773 value_decrement(v
.x
.p
->arr
[1].x
.n
, twice
);
774 evalue_set_si(&v
.x
.p
->arr
[2], -1, 1);
775 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
777 for (pp
= &v
.x
.p
->arr
[0]; value_zero_p(pp
->d
);
778 pp
= &pp
->x
.p
->arr
[0]) {
779 f
= &pp
->x
.p
->arr
[1];
780 value_oppose(f
->x
.n
, f
->x
.n
);
781 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
783 value_division(pp
->d
, twice
, pp
->d
);
784 value_multiply(pp
->x
.n
, pp
->x
.n
, pp
->d
);
785 value_assign(pp
->d
, twice
);
786 value_oppose(pp
->x
.n
, pp
->x
.n
);
787 value_decrement(pp
->x
.n
, pp
->x
.n
);
788 mpz_fdiv_r(pp
->x
.n
, pp
->x
.n
, pp
->d
);
790 /* Maybe we should do this during reduction of
793 value_gcd(twice
, pp
->d
, pp
->x
.n
);
794 value_division(pp
->d
, pp
->d
, twice
);
795 value_division(pp
->x
.n
, pp
->x
.n
, twice
);
805 reorder_terms_about(p
, &v
);
806 _reduce_evalue(&p
->arr
[1], s
, fract
);
809 evalue_reduce_size(e
);
811 else if (p
->type
== flooring
) {
812 /* Replace floor(constant) by its value */
813 if (value_notzero_p(p
->arr
[0].d
)) {
816 value_set_si(v
.d
, 1);
818 mpz_fdiv_q(v
.x
.n
, p
->arr
[0].x
.n
, p
->arr
[0].d
);
819 reorder_terms_about(p
, &v
);
820 _reduce_evalue(&p
->arr
[1], s
, fract
);
822 evalue_reduce_size(e
);
824 else if (p
->type
== relation
) {
825 if (p
->size
== 3 && eequal(&p
->arr
[1], &p
->arr
[2])) {
826 free_evalue_refs(&(p
->arr
[2]));
827 free_evalue_refs(&(p
->arr
[0]));
834 evalue_reduce_size(e
);
835 if (value_notzero_p(e
->d
) || p
!= e
->x
.p
)
842 /* Relation was reduced by means of an identical
843 * inequality => remove
845 if (value_zero_p(m
->d
) && !EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
848 if (reduced
|| value_notzero_p(p
->arr
[0].d
)) {
849 if (!reduced
&& value_zero_p(p
->arr
[0].x
.n
)) {
851 memcpy(e
,&p
->arr
[1],sizeof(evalue
));
853 free_evalue_refs(&(p
->arr
[2]));
857 memcpy(e
,&p
->arr
[2],sizeof(evalue
));
859 evalue_set_si(e
, 0, 1);
860 free_evalue_refs(&(p
->arr
[1]));
862 free_evalue_refs(&(p
->arr
[0]));
868 } /* reduce_evalue */
870 static void add_substitution(struct subst
*s
, Value
*row
, unsigned dim
)
875 for (k
= 0; k
< dim
; ++k
)
876 if (value_notzero_p(row
[k
+1]))
879 Vector_Normalize_Positive(row
+1, dim
+1, k
);
880 assert(s
->n
< s
->max
);
881 value_init(s
->fixed
[s
->n
].d
);
882 value_init(s
->fixed
[s
->n
].m
);
883 value_assign(s
->fixed
[s
->n
].d
, row
[k
+1]);
884 s
->fixed
[s
->n
].pos
= k
+1;
885 value_set_si(s
->fixed
[s
->n
].m
, 0);
886 r
= &s
->fixed
[s
->n
].s
;
888 for (l
= k
+1; l
< dim
; ++l
)
889 if (value_notzero_p(row
[l
+1])) {
890 value_set_si(r
->d
, 0);
891 r
->x
.p
= new_enode(polynomial
, 2, l
+ 1);
892 value_init(r
->x
.p
->arr
[1].x
.n
);
893 value_oppose(r
->x
.p
->arr
[1].x
.n
, row
[l
+1]);
894 value_set_si(r
->x
.p
->arr
[1].d
, 1);
898 value_oppose(r
->x
.n
, row
[dim
+1]);
899 value_set_si(r
->d
, 1);
903 static void _reduce_evalue_in_domain(evalue
*e
, Polyhedron
*D
, struct subst
*s
)
906 Polyhedron
*orig
= D
;
911 D
= DomainConvex(D
, 0);
912 /* We don't perform any substitutions if the domain is a union.
913 * We may therefore miss out on some possible simplifications,
914 * e.g., if a variable is always even in the whole union,
915 * while there is a relation in the evalue that evaluates
916 * to zero for even values of the variable.
918 if (!D
->next
&& D
->NbEq
) {
922 realloc_substitution(s
, dim
);
924 int d
= relations_depth(e
);
926 NALLOC(s
->fixed
, s
->max
);
929 for (j
= 0; j
< D
->NbEq
; ++j
)
930 add_substitution(s
, D
->Constraint
[j
], dim
);
934 _reduce_evalue(e
, s
, 0);
937 for (j
= 0; j
< s
->n
; ++j
) {
938 value_clear(s
->fixed
[j
].d
);
939 value_clear(s
->fixed
[j
].m
);
940 free_evalue_refs(&s
->fixed
[j
].s
);
945 void reduce_evalue_in_domain(evalue
*e
, Polyhedron
*D
)
947 struct subst s
= { NULL
, 0, 0 };
948 POL_ENSURE_VERTICES(D
);
950 if (EVALUE_IS_ZERO(*e
))
954 evalue_set_si(e
, 0, 1);
957 _reduce_evalue_in_domain(e
, D
, &s
);
962 void reduce_evalue (evalue
*e
) {
963 struct subst s
= { NULL
, 0, 0 };
965 if (value_notzero_p(e
->d
))
966 return; /* a rational number, its already reduced */
968 if (e
->x
.p
->type
== partition
) {
970 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
971 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
973 /* This shouldn't really happen;
974 * Empty domains should not be added.
976 POL_ENSURE_VERTICES(D
);
978 _reduce_evalue_in_domain(&e
->x
.p
->arr
[2*i
+1], D
, &s
);
980 if (emptyQ(D
) || EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
981 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
982 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
983 value_clear(e
->x
.p
->arr
[2*i
].d
);
985 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
986 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
990 if (e
->x
.p
->size
== 0) {
992 evalue_set_si(e
, 0, 1);
995 _reduce_evalue(e
, &s
, 0);
1000 static void print_evalue_r(FILE *DST
, const evalue
*e
, const char **pname
)
1002 if (EVALUE_IS_NAN(*e
)) {
1003 fprintf(DST
, "NaN");
1007 if(value_notzero_p(e
->d
)) {
1008 if(value_notone_p(e
->d
)) {
1009 value_print(DST
,VALUE_FMT
,e
->x
.n
);
1011 value_print(DST
,VALUE_FMT
,e
->d
);
1014 value_print(DST
,VALUE_FMT
,e
->x
.n
);
1018 print_enode(DST
,e
->x
.p
,pname
);
1020 } /* print_evalue */
1022 void print_evalue(FILE *DST
, const evalue
*e
, const char **pname
)
1024 print_evalue_r(DST
, e
, pname
);
1025 if (value_notzero_p(e
->d
))
1029 void print_enode(FILE *DST
, enode
*p
, const char **pname
)
1034 fprintf(DST
, "NULL");
1040 for (i
=0; i
<p
->size
; i
++) {
1041 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1045 fprintf(DST
, " }\n");
1049 for (i
=p
->size
-1; i
>=0; i
--) {
1050 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1051 if (i
==1) fprintf(DST
, " * %s + ", pname
[p
->pos
-1]);
1053 fprintf(DST
, " * %s^%d + ", pname
[p
->pos
-1], i
);
1055 fprintf(DST
, " )\n");
1059 for (i
=0; i
<p
->size
; i
++) {
1060 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1061 if (i
!=(p
->size
-1)) fprintf(DST
, ", ");
1063 fprintf(DST
," ]_%s", pname
[p
->pos
-1]);
1068 for (i
=p
->size
-1; i
>=1; i
--) {
1069 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1071 fprintf(DST
, " * ");
1072 fprintf(DST
, p
->type
== flooring
? "[" : "{");
1073 print_evalue_r(DST
, &p
->arr
[0], pname
);
1074 fprintf(DST
, p
->type
== flooring
? "]" : "}");
1076 fprintf(DST
, "^%d + ", i
-1);
1078 fprintf(DST
, " + ");
1081 fprintf(DST
, " )\n");
1085 print_evalue_r(DST
, &p
->arr
[0], pname
);
1086 fprintf(DST
, "= 0 ] * \n");
1087 print_evalue_r(DST
, &p
->arr
[1], pname
);
1089 fprintf(DST
, " +\n [ ");
1090 print_evalue_r(DST
, &p
->arr
[0], pname
);
1091 fprintf(DST
, "!= 0 ] * \n");
1092 print_evalue_r(DST
, &p
->arr
[2], pname
);
1096 char **new_names
= NULL
;
1097 const char **names
= pname
;
1098 int maxdim
= EVALUE_DOMAIN(p
->arr
[0])->Dimension
;
1099 if (!pname
|| p
->pos
< maxdim
) {
1100 new_names
= ALLOCN(char *, maxdim
);
1101 for (i
= 0; i
< p
->pos
; ++i
) {
1103 new_names
[i
] = (char *)pname
[i
];
1105 new_names
[i
] = ALLOCN(char, 10);
1106 snprintf(new_names
[i
], 10, "%c", 'P'+i
);
1109 for ( ; i
< maxdim
; ++i
) {
1110 new_names
[i
] = ALLOCN(char, 10);
1111 snprintf(new_names
[i
], 10, "_p%d", i
);
1113 names
= (const char**)new_names
;
1116 for (i
=0; i
<p
->size
/2; i
++) {
1117 Print_Domain(DST
, EVALUE_DOMAIN(p
->arr
[2*i
]), names
);
1118 print_evalue_r(DST
, &p
->arr
[2*i
+1], names
);
1119 if (value_notzero_p(p
->arr
[2*i
+1].d
))
1123 if (!pname
|| p
->pos
< maxdim
) {
1124 for (i
= pname
? p
->pos
: 0; i
< maxdim
; ++i
)
1138 * 0 if toplevels of e1 and e2 are at the same level
1139 * <0 if toplevel of e1 should be outside of toplevel of e2
1140 * >0 if toplevel of e2 should be outside of toplevel of e1
1142 static int evalue_level_cmp(const evalue
*e1
, const evalue
*e2
)
1144 if (value_notzero_p(e1
->d
) && value_notzero_p(e2
->d
))
1146 if (value_notzero_p(e1
->d
))
1148 if (value_notzero_p(e2
->d
))
1150 if (e1
->x
.p
->type
== partition
&& e2
->x
.p
->type
== partition
)
1152 if (e1
->x
.p
->type
== partition
)
1154 if (e2
->x
.p
->type
== partition
)
1156 if (e1
->x
.p
->type
== relation
&& e2
->x
.p
->type
== relation
) {
1157 if (eequal(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]))
1159 return mod_term_cmp(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]);
1161 if (e1
->x
.p
->type
== relation
)
1163 if (e2
->x
.p
->type
== relation
)
1165 if (e1
->x
.p
->type
== polynomial
&& e2
->x
.p
->type
== polynomial
)
1166 return e1
->x
.p
->pos
- e2
->x
.p
->pos
;
1167 if (e1
->x
.p
->type
== polynomial
)
1169 if (e2
->x
.p
->type
== polynomial
)
1171 if (e1
->x
.p
->type
== periodic
&& e2
->x
.p
->type
== periodic
)
1172 return e1
->x
.p
->pos
- e2
->x
.p
->pos
;
1173 assert(e1
->x
.p
->type
!= periodic
);
1174 assert(e2
->x
.p
->type
!= periodic
);
1175 assert(e1
->x
.p
->type
== e2
->x
.p
->type
);
1176 if (eequal(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]))
1178 return mod_term_cmp(e1
, e2
);
1181 static void eadd_rev(const evalue
*e1
, evalue
*res
)
1185 evalue_copy(&ev
, e1
);
1187 free_evalue_refs(res
);
1191 static void eadd_rev_cst(const evalue
*e1
, evalue
*res
)
1195 evalue_copy(&ev
, e1
);
1196 eadd(res
, &ev
.x
.p
->arr
[type_offset(ev
.x
.p
)]);
1197 free_evalue_refs(res
);
1201 struct section
{ Polyhedron
* D
; evalue E
; };
1203 void eadd_partitions(const evalue
*e1
, evalue
*res
)
1208 s
= (struct section
*)
1209 malloc((e1
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2+1) *
1210 sizeof(struct section
));
1212 assert(e1
->x
.p
->pos
== res
->x
.p
->pos
);
1213 assert(e1
->x
.p
->pos
== EVALUE_DOMAIN(e1
->x
.p
->arr
[0])->Dimension
);
1214 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1217 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1218 assert(res
->x
.p
->size
>= 2);
1219 fd
= DomainDifference(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1220 EVALUE_DOMAIN(res
->x
.p
->arr
[0]), 0);
1222 for (i
= 1; i
< res
->x
.p
->size
/2; ++i
) {
1224 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1229 fd
= DomainConstraintSimplify(fd
, 0);
1234 value_init(s
[n
].E
.d
);
1235 evalue_copy(&s
[n
].E
, &e1
->x
.p
->arr
[2*j
+1]);
1239 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
1240 fd
= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]);
1241 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1243 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1244 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1245 d
= DomainConstraintSimplify(d
, 0);
1251 fd
= DomainDifference(fd
, EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]), 0);
1252 if (t
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
1254 value_init(s
[n
].E
.d
);
1255 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
1256 eadd(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
1261 s
[n
].E
= res
->x
.p
->arr
[2*i
+1];
1265 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
1268 if (fd
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
1269 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
1270 value_clear(res
->x
.p
->arr
[2*i
].d
);
1275 res
->x
.p
= new_enode(partition
, 2*n
, e1
->x
.p
->pos
);
1276 for (j
= 0; j
< n
; ++j
) {
1277 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1278 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1279 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1285 static void explicit_complement(evalue
*res
)
1287 enode
*rel
= new_enode(relation
, 3, 0);
1289 value_clear(rel
->arr
[0].d
);
1290 rel
->arr
[0] = res
->x
.p
->arr
[0];
1291 value_clear(rel
->arr
[1].d
);
1292 rel
->arr
[1] = res
->x
.p
->arr
[1];
1293 value_set_si(rel
->arr
[2].d
, 1);
1294 value_init(rel
->arr
[2].x
.n
);
1295 value_set_si(rel
->arr
[2].x
.n
, 0);
1300 static void reduce_constant(evalue
*e
)
1305 value_gcd(g
, e
->x
.n
, e
->d
);
1306 if (value_notone_p(g
)) {
1307 value_division(e
->d
, e
->d
,g
);
1308 value_division(e
->x
.n
, e
->x
.n
,g
);
1313 /* Add two rational numbers */
1314 static void eadd_rationals(const evalue
*e1
, evalue
*res
)
1316 if (value_eq(e1
->d
, res
->d
))
1317 value_addto(res
->x
.n
, res
->x
.n
, e1
->x
.n
);
1319 value_multiply(res
->x
.n
, res
->x
.n
, e1
->d
);
1320 value_addmul(res
->x
.n
, e1
->x
.n
, res
->d
);
1321 value_multiply(res
->d
,e1
->d
,res
->d
);
1323 reduce_constant(res
);
1326 static void eadd_relations(const evalue
*e1
, evalue
*res
)
1330 if (res
->x
.p
->size
< 3 && e1
->x
.p
->size
== 3)
1331 explicit_complement(res
);
1332 for (i
= 1; i
< e1
->x
.p
->size
; ++i
)
1333 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1336 static void eadd_arrays(const evalue
*e1
, evalue
*res
, int n
)
1340 // add any element in e1 to the corresponding element in res
1341 i
= type_offset(res
->x
.p
);
1343 assert(eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]));
1345 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1348 static void eadd_poly(const evalue
*e1
, evalue
*res
)
1350 if (e1
->x
.p
->size
> res
->x
.p
->size
)
1353 eadd_arrays(e1
, res
, e1
->x
.p
->size
);
1357 * Product or sum of two periodics of the same parameter
1358 * and different periods
1360 static void combine_periodics(const evalue
*e1
, evalue
*res
,
1361 void (*op
)(const evalue
*, evalue
*))
1369 value_set_si(es
, e1
->x
.p
->size
);
1370 value_set_si(rs
, res
->x
.p
->size
);
1371 value_lcm(rs
, es
, rs
);
1372 size
= (int)mpz_get_si(rs
);
1375 p
= new_enode(periodic
, size
, e1
->x
.p
->pos
);
1376 for (i
= 0; i
< res
->x
.p
->size
; i
++) {
1377 value_clear(p
->arr
[i
].d
);
1378 p
->arr
[i
] = res
->x
.p
->arr
[i
];
1380 for (i
= res
->x
.p
->size
; i
< size
; i
++)
1381 evalue_copy(&p
->arr
[i
], &res
->x
.p
->arr
[i
% res
->x
.p
->size
]);
1382 for (i
= 0; i
< size
; i
++)
1383 op(&e1
->x
.p
->arr
[i
% e1
->x
.p
->size
], &p
->arr
[i
]);
1388 static void eadd_periodics(const evalue
*e1
, evalue
*res
)
1394 if (e1
->x
.p
->size
== res
->x
.p
->size
) {
1395 eadd_arrays(e1
, res
, e1
->x
.p
->size
);
1399 combine_periodics(e1
, res
, eadd
);
1402 void evalue_assign(evalue
*dst
, const evalue
*src
)
1404 if (value_pos_p(dst
->d
) && value_pos_p(src
->d
)) {
1405 value_assign(dst
->d
, src
->d
);
1406 value_assign(dst
->x
.n
, src
->x
.n
);
1409 free_evalue_refs(dst
);
1411 evalue_copy(dst
, src
);
1414 void eadd(const evalue
*e1
, evalue
*res
)
1418 if (EVALUE_IS_ZERO(*e1
))
1421 if (EVALUE_IS_NAN(*res
))
1424 if (EVALUE_IS_NAN(*e1
)) {
1425 evalue_assign(res
, e1
);
1429 if (EVALUE_IS_ZERO(*res
)) {
1430 evalue_assign(res
, e1
);
1434 cmp
= evalue_level_cmp(res
, e1
);
1436 switch (e1
->x
.p
->type
) {
1440 eadd_rev_cst(e1
, res
);
1445 } else if (cmp
== 0) {
1446 if (value_notzero_p(e1
->d
)) {
1447 eadd_rationals(e1
, res
);
1449 switch (e1
->x
.p
->type
) {
1451 eadd_partitions(e1
, res
);
1454 eadd_relations(e1
, res
);
1457 assert(e1
->x
.p
->size
== res
->x
.p
->size
);
1464 eadd_periodics(e1
, res
);
1472 switch (res
->x
.p
->type
) {
1476 /* Add to the constant term of a polynomial */
1477 eadd(e1
, &res
->x
.p
->arr
[type_offset(res
->x
.p
)]);
1480 /* Add to all elements of a periodic number */
1481 for (i
= 0; i
< res
->x
.p
->size
; i
++)
1482 eadd(e1
, &res
->x
.p
->arr
[i
]);
1485 fprintf(stderr
, "eadd: cannot add const with vector\n");
1490 /* Create (zero) complement if needed */
1491 if (res
->x
.p
->size
< 3)
1492 explicit_complement(res
);
1493 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1494 eadd(e1
, &res
->x
.p
->arr
[i
]);
1502 static void emul_rev(const evalue
*e1
, evalue
*res
)
1506 evalue_copy(&ev
, e1
);
1508 free_evalue_refs(res
);
1512 static void emul_poly(const evalue
*e1
, evalue
*res
)
1514 int i
, j
, offset
= type_offset(res
->x
.p
);
1517 int size
= (e1
->x
.p
->size
+ res
->x
.p
->size
- offset
- 1);
1519 p
= new_enode(res
->x
.p
->type
, size
, res
->x
.p
->pos
);
1521 for (i
= offset
; i
< e1
->x
.p
->size
-1; ++i
)
1522 if (!EVALUE_IS_ZERO(e1
->x
.p
->arr
[i
]))
1525 /* special case pure power */
1526 if (i
== e1
->x
.p
->size
-1) {
1528 value_clear(p
->arr
[0].d
);
1529 p
->arr
[0] = res
->x
.p
->arr
[0];
1531 for (i
= offset
; i
< e1
->x
.p
->size
-1; ++i
)
1532 evalue_set_si(&p
->arr
[i
], 0, 1);
1533 for (i
= offset
; i
< res
->x
.p
->size
; ++i
) {
1534 value_clear(p
->arr
[i
+e1
->x
.p
->size
-offset
-1].d
);
1535 p
->arr
[i
+e1
->x
.p
->size
-offset
-1] = res
->x
.p
->arr
[i
];
1536 emul(&e1
->x
.p
->arr
[e1
->x
.p
->size
-1],
1537 &p
->arr
[i
+e1
->x
.p
->size
-offset
-1]);
1545 value_set_si(tmp
.d
,0);
1548 evalue_copy(&p
->arr
[0], &e1
->x
.p
->arr
[0]);
1549 for (i
= offset
; i
< e1
->x
.p
->size
; i
++) {
1550 evalue_copy(&tmp
.x
.p
->arr
[i
], &e1
->x
.p
->arr
[i
]);
1551 emul(&res
->x
.p
->arr
[offset
], &tmp
.x
.p
->arr
[i
]);
1554 evalue_set_si(&tmp
.x
.p
->arr
[i
], 0, 1);
1555 for (i
= offset
+1; i
<res
->x
.p
->size
; i
++)
1556 for (j
= offset
; j
<e1
->x
.p
->size
; j
++) {
1559 evalue_copy(&ev
, &e1
->x
.p
->arr
[j
]);
1560 emul(&res
->x
.p
->arr
[i
], &ev
);
1561 eadd(&ev
, &tmp
.x
.p
->arr
[i
+j
-offset
]);
1562 free_evalue_refs(&ev
);
1564 free_evalue_refs(res
);
1568 void emul_partitions(const evalue
*e1
, evalue
*res
)
1573 s
= (struct section
*)
1574 malloc((e1
->x
.p
->size
/2) * (res
->x
.p
->size
/2) *
1575 sizeof(struct section
));
1577 assert(e1
->x
.p
->pos
== res
->x
.p
->pos
);
1578 assert(e1
->x
.p
->pos
== EVALUE_DOMAIN(e1
->x
.p
->arr
[0])->Dimension
);
1579 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1582 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
1583 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1584 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1585 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1586 d
= DomainConstraintSimplify(d
, 0);
1592 /* This code is only needed because the partitions
1593 are not true partitions.
1595 for (k
= 0; k
< n
; ++k
) {
1596 if (DomainIncludes(s
[k
].D
, d
))
1598 if (DomainIncludes(d
, s
[k
].D
)) {
1599 Domain_Free(s
[k
].D
);
1600 free_evalue_refs(&s
[k
].E
);
1611 value_init(s
[n
].E
.d
);
1612 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
1613 emul(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
1617 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
1618 value_clear(res
->x
.p
->arr
[2*i
].d
);
1619 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
1624 evalue_set_si(res
, 0, 1);
1626 res
->x
.p
= new_enode(partition
, 2*n
, e1
->x
.p
->pos
);
1627 for (j
= 0; j
< n
; ++j
) {
1628 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1629 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1630 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1637 /* Product of two rational numbers */
1638 static void emul_rationals(const evalue
*e1
, evalue
*res
)
1640 value_multiply(res
->d
, e1
->d
, res
->d
);
1641 value_multiply(res
->x
.n
, e1
->x
.n
, res
->x
.n
);
1642 reduce_constant(res
);
1645 static void emul_relations(const evalue
*e1
, evalue
*res
)
1649 if (e1
->x
.p
->size
< 3 && res
->x
.p
->size
== 3) {
1650 free_evalue_refs(&res
->x
.p
->arr
[2]);
1653 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1654 emul(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1657 static void emul_periodics(const evalue
*e1
, evalue
*res
)
1664 if (e1
->x
.p
->size
== res
->x
.p
->size
) {
1665 /* Product of two periodics of the same parameter and period */
1666 for (i
= 0; i
< res
->x
.p
->size
; i
++)
1667 emul(&(e1
->x
.p
->arr
[i
]), &(res
->x
.p
->arr
[i
]));
1671 combine_periodics(e1
, res
, emul
);
1674 #define value_two_p(val) (mpz_cmp_si(val,2) == 0)
1676 static void emul_fractionals(const evalue
*e1
, evalue
*res
)
1680 poly_denom(&e1
->x
.p
->arr
[0], &d
.d
);
1681 if (!value_two_p(d
.d
))
1686 value_set_si(d
.x
.n
, 1);
1687 /* { x }^2 == { x }/2 */
1688 /* a0 b0 + (a0 b1 + a1 b0 + a1 b1/2) { x } */
1689 assert(e1
->x
.p
->size
== 3);
1690 assert(res
->x
.p
->size
== 3);
1692 evalue_copy(&tmp
, &res
->x
.p
->arr
[2]);
1694 eadd(&res
->x
.p
->arr
[1], &tmp
);
1695 emul(&e1
->x
.p
->arr
[2], &tmp
);
1696 emul(&e1
->x
.p
->arr
[1], &res
->x
.p
->arr
[1]);
1697 emul(&e1
->x
.p
->arr
[1], &res
->x
.p
->arr
[2]);
1698 eadd(&tmp
, &res
->x
.p
->arr
[2]);
1699 free_evalue_refs(&tmp
);
1705 /* Computes the product of two evalues "e1" and "res" and puts
1706 * the result in "res". You need to make a copy of "res"
1707 * before calling this function if you still need it afterward.
1708 * The vector type of evalues is not treated here
1710 void emul(const evalue
*e1
, evalue
*res
)
1714 assert(!(value_zero_p(e1
->d
) && e1
->x
.p
->type
== evector
));
1715 assert(!(value_zero_p(res
->d
) && res
->x
.p
->type
== evector
));
1717 if (EVALUE_IS_ZERO(*res
))
1720 if (EVALUE_IS_ONE(*e1
))
1723 if (EVALUE_IS_ZERO(*e1
)) {
1724 evalue_assign(res
, e1
);
1728 if (EVALUE_IS_NAN(*res
))
1731 if (EVALUE_IS_NAN(*e1
)) {
1732 evalue_assign(res
, e1
);
1736 cmp
= evalue_level_cmp(res
, e1
);
1739 } else if (cmp
== 0) {
1740 if (value_notzero_p(e1
->d
)) {
1741 emul_rationals(e1
, res
);
1743 switch (e1
->x
.p
->type
) {
1745 emul_partitions(e1
, res
);
1748 emul_relations(e1
, res
);
1755 emul_periodics(e1
, res
);
1758 emul_fractionals(e1
, res
);
1764 switch (res
->x
.p
->type
) {
1766 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
)
1767 emul(e1
, &res
->x
.p
->arr
[2*i
+1]);
1774 for (i
= type_offset(res
->x
.p
); i
< res
->x
.p
->size
; ++i
)
1775 emul(e1
, &res
->x
.p
->arr
[i
]);
1781 /* Frees mask content ! */
1782 void emask(evalue
*mask
, evalue
*res
) {
1789 if (EVALUE_IS_ZERO(*res
)) {
1790 free_evalue_refs(mask
);
1794 assert(value_zero_p(mask
->d
));
1795 assert(mask
->x
.p
->type
== partition
);
1796 assert(value_zero_p(res
->d
));
1797 assert(res
->x
.p
->type
== partition
);
1798 assert(mask
->x
.p
->pos
== res
->x
.p
->pos
);
1799 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1800 assert(mask
->x
.p
->pos
== EVALUE_DOMAIN(mask
->x
.p
->arr
[0])->Dimension
);
1801 pos
= res
->x
.p
->pos
;
1803 s
= (struct section
*)
1804 malloc((mask
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2) *
1805 sizeof(struct section
));
1809 evalue_set_si(&mone
, -1, 1);
1812 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1813 assert(mask
->x
.p
->size
>= 2);
1814 fd
= DomainDifference(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1815 EVALUE_DOMAIN(mask
->x
.p
->arr
[0]), 0);
1817 for (i
= 1; i
< mask
->x
.p
->size
/2; ++i
) {
1819 fd
= DomainDifference(fd
, EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1828 value_init(s
[n
].E
.d
);
1829 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1833 for (i
= 0; i
< mask
->x
.p
->size
/2; ++i
) {
1834 if (EVALUE_IS_ONE(mask
->x
.p
->arr
[2*i
+1]))
1837 fd
= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]);
1838 eadd(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1839 emul(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1840 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1842 d
= DomainIntersection(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1843 EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1849 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]), 0);
1850 if (t
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1852 value_init(s
[n
].E
.d
);
1853 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1854 emul(&mask
->x
.p
->arr
[2*i
+1], &s
[n
].E
);
1860 /* Just ignore; this may have been previously masked off */
1862 if (fd
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1866 free_evalue_refs(&mone
);
1867 free_evalue_refs(mask
);
1868 free_evalue_refs(res
);
1871 evalue_set_si(res
, 0, 1);
1873 res
->x
.p
= new_enode(partition
, 2*n
, pos
);
1874 for (j
= 0; j
< n
; ++j
) {
1875 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1876 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1877 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1884 void evalue_copy(evalue
*dst
, const evalue
*src
)
1886 value_assign(dst
->d
, src
->d
);
1887 if (EVALUE_IS_NAN(*dst
)) {
1891 if (value_pos_p(src
->d
)) {
1892 value_init(dst
->x
.n
);
1893 value_assign(dst
->x
.n
, src
->x
.n
);
1895 dst
->x
.p
= ecopy(src
->x
.p
);
1898 evalue
*evalue_dup(const evalue
*e
)
1900 evalue
*res
= ALLOC(evalue
);
1902 evalue_copy(res
, e
);
1906 enode
*new_enode(enode_type type
,int size
,int pos
) {
1912 fprintf(stderr
, "Allocating enode of size 0 !\n" );
1915 res
= (enode
*) malloc(sizeof(enode
) + (size
-1)*sizeof(evalue
));
1919 for(i
=0; i
<size
; i
++) {
1920 value_init(res
->arr
[i
].d
);
1921 value_set_si(res
->arr
[i
].d
,0);
1922 res
->arr
[i
].x
.p
= 0;
1927 enode
*ecopy(enode
*e
) {
1932 res
= new_enode(e
->type
,e
->size
,e
->pos
);
1933 for(i
=0;i
<e
->size
;++i
) {
1934 value_assign(res
->arr
[i
].d
,e
->arr
[i
].d
);
1935 if(value_zero_p(res
->arr
[i
].d
))
1936 res
->arr
[i
].x
.p
= ecopy(e
->arr
[i
].x
.p
);
1937 else if (EVALUE_IS_DOMAIN(res
->arr
[i
]))
1938 EVALUE_SET_DOMAIN(res
->arr
[i
], Domain_Copy(EVALUE_DOMAIN(e
->arr
[i
])));
1940 value_init(res
->arr
[i
].x
.n
);
1941 value_assign(res
->arr
[i
].x
.n
,e
->arr
[i
].x
.n
);
1947 int ecmp(const evalue
*e1
, const evalue
*e2
)
1953 if (value_notzero_p(e1
->d
) && value_notzero_p(e2
->d
)) {
1957 value_multiply(m
, e1
->x
.n
, e2
->d
);
1958 value_multiply(m2
, e2
->x
.n
, e1
->d
);
1960 if (value_lt(m
, m2
))
1962 else if (value_gt(m
, m2
))
1972 if (value_notzero_p(e1
->d
))
1974 if (value_notzero_p(e2
->d
))
1980 if (p1
->type
!= p2
->type
)
1981 return p1
->type
- p2
->type
;
1982 if (p1
->pos
!= p2
->pos
)
1983 return p1
->pos
- p2
->pos
;
1984 if (p1
->size
!= p2
->size
)
1985 return p1
->size
- p2
->size
;
1987 for (i
= p1
->size
-1; i
>= 0; --i
)
1988 if ((r
= ecmp(&p1
->arr
[i
], &p2
->arr
[i
])) != 0)
1994 int eequal(const evalue
*e1
, const evalue
*e2
)
1999 if (value_ne(e1
->d
,e2
->d
))
2002 if (EVALUE_IS_DOMAIN(*e1
))
2003 return PolyhedronIncludes(EVALUE_DOMAIN(*e2
), EVALUE_DOMAIN(*e1
)) &&
2004 PolyhedronIncludes(EVALUE_DOMAIN(*e1
), EVALUE_DOMAIN(*e2
));
2006 if (EVALUE_IS_NAN(*e1
))
2009 assert(value_posz_p(e1
->d
));
2011 /* e1->d == e2->d */
2012 if (value_notzero_p(e1
->d
)) {
2013 if (value_ne(e1
->x
.n
,e2
->x
.n
))
2016 /* e1->d == e2->d != 0 AND e1->n == e2->n */
2020 /* e1->d == e2->d == 0 */
2023 if (p1
->type
!= p2
->type
) return 0;
2024 if (p1
->size
!= p2
->size
) return 0;
2025 if (p1
->pos
!= p2
->pos
) return 0;
2026 for (i
=0; i
<p1
->size
; i
++)
2027 if (!eequal(&p1
->arr
[i
], &p2
->arr
[i
]) )
2032 void free_evalue_refs(evalue
*e
) {
2037 if (EVALUE_IS_NAN(*e
)) {
2042 if (EVALUE_IS_DOMAIN(*e
)) {
2043 Domain_Free(EVALUE_DOMAIN(*e
));
2046 } else if (value_pos_p(e
->d
)) {
2048 /* 'e' stores a constant */
2050 value_clear(e
->x
.n
);
2053 assert(value_zero_p(e
->d
));
2056 if (!p
) return; /* null pointer */
2057 for (i
=0; i
<p
->size
; i
++) {
2058 free_evalue_refs(&(p
->arr
[i
]));
2062 } /* free_evalue_refs */
2064 void evalue_free(evalue
*e
)
2066 free_evalue_refs(e
);
2070 static void mod2table_r(evalue
*e
, Vector
*periods
, Value m
, int p
,
2071 Vector
* val
, evalue
*res
)
2073 unsigned nparam
= periods
->Size
;
2076 double d
= compute_evalue(e
, val
->p
);
2077 d
*= VALUE_TO_DOUBLE(m
);
2082 value_assign(res
->d
, m
);
2083 value_init(res
->x
.n
);
2084 value_set_double(res
->x
.n
, d
);
2085 mpz_fdiv_r(res
->x
.n
, res
->x
.n
, m
);
2088 if (value_one_p(periods
->p
[p
]))
2089 mod2table_r(e
, periods
, m
, p
+1, val
, res
);
2094 value_assign(tmp
, periods
->p
[p
]);
2095 value_set_si(res
->d
, 0);
2096 res
->x
.p
= new_enode(periodic
, VALUE_TO_INT(tmp
), p
+1);
2098 value_decrement(tmp
, tmp
);
2099 value_assign(val
->p
[p
], tmp
);
2100 mod2table_r(e
, periods
, m
, p
+1, val
,
2101 &res
->x
.p
->arr
[VALUE_TO_INT(tmp
)]);
2102 } while (value_pos_p(tmp
));
2108 static void rel2table(evalue
*e
, int zero
)
2110 if (value_pos_p(e
->d
)) {
2111 if (value_zero_p(e
->x
.n
) == zero
)
2112 value_set_si(e
->x
.n
, 1);
2114 value_set_si(e
->x
.n
, 0);
2115 value_set_si(e
->d
, 1);
2118 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
2119 rel2table(&e
->x
.p
->arr
[i
], zero
);
2123 void evalue_mod2table(evalue
*e
, int nparam
)
2128 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
2131 for (i
=0; i
<p
->size
; i
++) {
2132 evalue_mod2table(&(p
->arr
[i
]), nparam
);
2134 if (p
->type
== relation
) {
2139 evalue_copy(©
, &p
->arr
[0]);
2141 rel2table(&p
->arr
[0], 1);
2142 emul(&p
->arr
[0], &p
->arr
[1]);
2144 rel2table(©
, 0);
2145 emul(©
, &p
->arr
[2]);
2146 eadd(&p
->arr
[2], &p
->arr
[1]);
2147 free_evalue_refs(&p
->arr
[2]);
2148 free_evalue_refs(©
);
2150 free_evalue_refs(&p
->arr
[0]);
2154 } else if (p
->type
== fractional
) {
2155 Vector
*periods
= Vector_Alloc(nparam
);
2156 Vector
*val
= Vector_Alloc(nparam
);
2162 value_set_si(tmp
, 1);
2163 Vector_Set(periods
->p
, 1, nparam
);
2164 Vector_Set(val
->p
, 0, nparam
);
2165 for (ev
= &p
->arr
[0]; value_zero_p(ev
->d
); ev
= &ev
->x
.p
->arr
[0]) {
2168 assert(p
->type
== polynomial
);
2169 assert(p
->size
== 2);
2170 value_assign(periods
->p
[p
->pos
-1], p
->arr
[1].d
);
2171 value_lcm(tmp
, tmp
, p
->arr
[1].d
);
2173 value_lcm(tmp
, tmp
, ev
->d
);
2175 mod2table_r(&p
->arr
[0], periods
, tmp
, 0, val
, &EP
);
2178 evalue_set_si(&res
, 0, 1);
2179 /* Compute the polynomial using Horner's rule */
2180 for (i
=p
->size
-1;i
>1;i
--) {
2181 eadd(&p
->arr
[i
], &res
);
2184 eadd(&p
->arr
[1], &res
);
2186 free_evalue_refs(e
);
2187 free_evalue_refs(&EP
);
2192 Vector_Free(periods
);
2194 } /* evalue_mod2table */
2196 /********************************************************/
2197 /* function in domain */
2198 /* check if the parameters in list_args */
2199 /* verifies the constraints of Domain P */
2200 /********************************************************/
2201 int in_domain(Polyhedron
*P
, Value
*list_args
)
2204 Value v
; /* value of the constraint of a row when
2205 parameters are instantiated*/
2207 if (P
->Dimension
== 0)
2212 for (row
= 0; row
< P
->NbConstraints
; row
++) {
2213 Inner_Product(P
->Constraint
[row
]+1, list_args
, P
->Dimension
, &v
);
2214 value_addto(v
, v
, P
->Constraint
[row
][P
->Dimension
+1]); /*constant part*/
2215 if (value_neg_p(v
) ||
2216 value_zero_p(P
->Constraint
[row
][0]) && value_notzero_p(v
)) {
2223 return in
|| (P
->next
&& in_domain(P
->next
, list_args
));
2226 /****************************************************/
2227 /* function compute enode */
2228 /* compute the value of enode p with parameters */
2229 /* list "list_args */
2230 /* compute the polynomial or the periodic */
2231 /****************************************************/
2233 static double compute_enode(enode
*p
, Value
*list_args
) {
2245 if (p
->type
== polynomial
) {
2247 value_assign(param
,list_args
[p
->pos
-1]);
2249 /* Compute the polynomial using Horner's rule */
2250 for (i
=p
->size
-1;i
>0;i
--) {
2251 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2252 res
*=VALUE_TO_DOUBLE(param
);
2254 res
+=compute_evalue(&p
->arr
[0],list_args
);
2256 else if (p
->type
== fractional
) {
2257 double d
= compute_evalue(&p
->arr
[0], list_args
);
2258 d
-= floor(d
+1e-10);
2260 /* Compute the polynomial using Horner's rule */
2261 for (i
=p
->size
-1;i
>1;i
--) {
2262 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2265 res
+=compute_evalue(&p
->arr
[1],list_args
);
2267 else if (p
->type
== flooring
) {
2268 double d
= compute_evalue(&p
->arr
[0], list_args
);
2271 /* Compute the polynomial using Horner's rule */
2272 for (i
=p
->size
-1;i
>1;i
--) {
2273 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2276 res
+=compute_evalue(&p
->arr
[1],list_args
);
2278 else if (p
->type
== periodic
) {
2279 value_assign(m
,list_args
[p
->pos
-1]);
2281 /* Choose the right element of the periodic */
2282 value_set_si(param
,p
->size
);
2283 value_pmodulus(m
,m
,param
);
2284 res
= compute_evalue(&p
->arr
[VALUE_TO_INT(m
)],list_args
);
2286 else if (p
->type
== relation
) {
2287 if (fabs(compute_evalue(&p
->arr
[0], list_args
)) < 1e-10)
2288 res
= compute_evalue(&p
->arr
[1], list_args
);
2289 else if (p
->size
> 2)
2290 res
= compute_evalue(&p
->arr
[2], list_args
);
2292 else if (p
->type
== partition
) {
2293 int dim
= EVALUE_DOMAIN(p
->arr
[0])->Dimension
;
2294 Value
*vals
= list_args
;
2297 for (i
= 0; i
< dim
; ++i
) {
2298 value_init(vals
[i
]);
2300 value_assign(vals
[i
], list_args
[i
]);
2303 for (i
= 0; i
< p
->size
/2; ++i
)
2304 if (DomainContains(EVALUE_DOMAIN(p
->arr
[2*i
]), vals
, p
->pos
, 0, 1)) {
2305 res
= compute_evalue(&p
->arr
[2*i
+1], vals
);
2309 for (i
= 0; i
< dim
; ++i
)
2310 value_clear(vals
[i
]);
2319 } /* compute_enode */
2321 /*************************************************/
2322 /* return the value of Ehrhart Polynomial */
2323 /* It returns a double, because since it is */
2324 /* a recursive function, some intermediate value */
2325 /* might not be integral */
2326 /*************************************************/
2328 double compute_evalue(const evalue
*e
, Value
*list_args
)
2332 if (value_notzero_p(e
->d
)) {
2333 if (value_notone_p(e
->d
))
2334 res
= VALUE_TO_DOUBLE(e
->x
.n
) / VALUE_TO_DOUBLE(e
->d
);
2336 res
= VALUE_TO_DOUBLE(e
->x
.n
);
2339 res
= compute_enode(e
->x
.p
,list_args
);
2341 } /* compute_evalue */
2344 /****************************************************/
2345 /* function compute_poly : */
2346 /* Check for the good validity domain */
2347 /* return the number of point in the Polyhedron */
2348 /* in allocated memory */
2349 /* Using the Ehrhart pseudo-polynomial */
2350 /****************************************************/
2351 Value
*compute_poly(Enumeration
*en
,Value
*list_args
) {
2354 /* double d; int i; */
2356 tmp
= (Value
*) malloc (sizeof(Value
));
2357 assert(tmp
!= NULL
);
2359 value_set_si(*tmp
,0);
2362 return(tmp
); /* no ehrhart polynomial */
2363 if(en
->ValidityDomain
) {
2364 if(!en
->ValidityDomain
->Dimension
) { /* no parameters */
2365 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
2370 return(tmp
); /* no Validity Domain */
2372 if(in_domain(en
->ValidityDomain
,list_args
)) {
2374 #ifdef EVAL_EHRHART_DEBUG
2375 Print_Domain(stdout
,en
->ValidityDomain
);
2376 print_evalue(stdout
,&en
->EP
);
2379 /* d = compute_evalue(&en->EP,list_args);
2381 printf("(double)%lf = %d\n", d, i ); */
2382 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
2388 value_set_si(*tmp
,0);
2389 return(tmp
); /* no compatible domain with the arguments */
2390 } /* compute_poly */
2392 static evalue
*eval_polynomial(const enode
*p
, int offset
,
2393 evalue
*base
, Value
*values
)
2398 res
= evalue_zero();
2399 for (i
= p
->size
-1; i
> offset
; --i
) {
2400 c
= evalue_eval(&p
->arr
[i
], values
);
2405 c
= evalue_eval(&p
->arr
[offset
], values
);
2412 evalue
*evalue_eval(const evalue
*e
, Value
*values
)
2419 if (value_notzero_p(e
->d
)) {
2420 res
= ALLOC(evalue
);
2422 evalue_copy(res
, e
);
2425 switch (e
->x
.p
->type
) {
2427 value_init(param
.x
.n
);
2428 value_assign(param
.x
.n
, values
[e
->x
.p
->pos
-1]);
2429 value_init(param
.d
);
2430 value_set_si(param
.d
, 1);
2432 res
= eval_polynomial(e
->x
.p
, 0, ¶m
, values
);
2433 free_evalue_refs(¶m
);
2436 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2437 mpz_fdiv_r(param2
->x
.n
, param2
->x
.n
, param2
->d
);
2439 res
= eval_polynomial(e
->x
.p
, 1, param2
, values
);
2440 evalue_free(param2
);
2443 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2444 mpz_fdiv_q(param2
->x
.n
, param2
->x
.n
, param2
->d
);
2445 value_set_si(param2
->d
, 1);
2447 res
= eval_polynomial(e
->x
.p
, 1, param2
, values
);
2448 evalue_free(param2
);
2451 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2452 if (value_zero_p(param2
->x
.n
))
2453 res
= evalue_eval(&e
->x
.p
->arr
[1], values
);
2454 else if (e
->x
.p
->size
> 2)
2455 res
= evalue_eval(&e
->x
.p
->arr
[2], values
);
2457 res
= evalue_zero();
2458 evalue_free(param2
);
2461 assert(e
->x
.p
->pos
== EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
);
2462 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2463 if (in_domain(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), values
)) {
2464 res
= evalue_eval(&e
->x
.p
->arr
[2*i
+1], values
);
2468 res
= evalue_zero();
2476 size_t value_size(Value v
) {
2477 return (v
[0]._mp_size
> 0 ? v
[0]._mp_size
: -v
[0]._mp_size
)
2478 * sizeof(v
[0]._mp_d
[0]);
2481 size_t domain_size(Polyhedron
*D
)
2484 size_t s
= sizeof(*D
);
2486 for (i
= 0; i
< D
->NbConstraints
; ++i
)
2487 for (j
= 0; j
< D
->Dimension
+2; ++j
)
2488 s
+= value_size(D
->Constraint
[i
][j
]);
2491 for (i = 0; i < D->NbRays; ++i)
2492 for (j = 0; j < D->Dimension+2; ++j)
2493 s += value_size(D->Ray[i][j]);
2496 return D
->next
? s
+domain_size(D
->next
) : s
;
2499 size_t enode_size(enode
*p
) {
2500 size_t s
= sizeof(*p
) - sizeof(p
->arr
[0]);
2503 if (p
->type
== partition
)
2504 for (i
= 0; i
< p
->size
/2; ++i
) {
2505 s
+= domain_size(EVALUE_DOMAIN(p
->arr
[2*i
]));
2506 s
+= evalue_size(&p
->arr
[2*i
+1]);
2509 for (i
= 0; i
< p
->size
; ++i
) {
2510 s
+= evalue_size(&p
->arr
[i
]);
2515 size_t evalue_size(evalue
*e
)
2517 size_t s
= sizeof(*e
);
2518 s
+= value_size(e
->d
);
2519 if (value_notzero_p(e
->d
))
2520 s
+= value_size(e
->x
.n
);
2522 s
+= enode_size(e
->x
.p
);
2526 static evalue
*find_second(evalue
*base
, evalue
*cst
, evalue
*e
, Value m
)
2528 evalue
*found
= NULL
;
2533 if (value_pos_p(e
->d
) || e
->x
.p
->type
!= fractional
)
2536 value_init(offset
.d
);
2537 value_init(offset
.x
.n
);
2538 poly_denom(&e
->x
.p
->arr
[0], &offset
.d
);
2539 value_lcm(offset
.d
, m
, offset
.d
);
2540 value_set_si(offset
.x
.n
, 1);
2543 evalue_copy(©
, cst
);
2546 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2548 if (eequal(base
, &e
->x
.p
->arr
[0]))
2549 found
= &e
->x
.p
->arr
[0];
2551 value_set_si(offset
.x
.n
, -2);
2554 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2556 if (eequal(base
, &e
->x
.p
->arr
[0]))
2559 free_evalue_refs(cst
);
2560 free_evalue_refs(&offset
);
2563 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2564 found
= find_second(base
, cst
, &e
->x
.p
->arr
[i
], m
);
2569 static evalue
*find_relation_pair(evalue
*e
)
2572 evalue
*found
= NULL
;
2574 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
2577 if (e
->x
.p
->type
== fractional
) {
2582 poly_denom(&e
->x
.p
->arr
[0], &m
);
2584 for (cst
= &e
->x
.p
->arr
[0]; value_zero_p(cst
->d
);
2585 cst
= &cst
->x
.p
->arr
[0])
2588 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2589 found
= find_second(&e
->x
.p
->arr
[0], cst
, &e
->x
.p
->arr
[i
], m
);
2594 i
= e
->x
.p
->type
== relation
;
2595 for (; !found
&& i
< e
->x
.p
->size
; ++i
)
2596 found
= find_relation_pair(&e
->x
.p
->arr
[i
]);
2601 void evalue_mod2relation(evalue
*e
) {
2604 if (value_zero_p(e
->d
) && e
->x
.p
->type
== partition
) {
2607 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2608 evalue_mod2relation(&e
->x
.p
->arr
[2*i
+1]);
2609 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
2610 value_clear(e
->x
.p
->arr
[2*i
].d
);
2611 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2613 if (2*i
< e
->x
.p
->size
) {
2614 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2615 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2620 if (e
->x
.p
->size
== 0) {
2622 evalue_set_si(e
, 0, 1);
2628 while ((d
= find_relation_pair(e
)) != NULL
) {
2632 value_init(split
.d
);
2633 value_set_si(split
.d
, 0);
2634 split
.x
.p
= new_enode(relation
, 3, 0);
2635 evalue_set_si(&split
.x
.p
->arr
[1], 1, 1);
2636 evalue_set_si(&split
.x
.p
->arr
[2], 1, 1);
2638 ev
= &split
.x
.p
->arr
[0];
2639 value_set_si(ev
->d
, 0);
2640 ev
->x
.p
= new_enode(fractional
, 3, -1);
2641 evalue_set_si(&ev
->x
.p
->arr
[1], 0, 1);
2642 evalue_set_si(&ev
->x
.p
->arr
[2], 1, 1);
2643 evalue_copy(&ev
->x
.p
->arr
[0], d
);
2649 free_evalue_refs(&split
);
2653 static int evalue_comp(const void * a
, const void * b
)
2655 const evalue
*e1
= *(const evalue
**)a
;
2656 const evalue
*e2
= *(const evalue
**)b
;
2657 return ecmp(e1
, e2
);
2660 void evalue_combine(evalue
*e
)
2667 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
2670 NALLOC(evs
, e
->x
.p
->size
/2);
2671 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2672 evs
[i
] = &e
->x
.p
->arr
[2*i
+1];
2673 qsort(evs
, e
->x
.p
->size
/2, sizeof(evs
[0]), evalue_comp
);
2674 p
= new_enode(partition
, e
->x
.p
->size
, e
->x
.p
->pos
);
2675 for (i
= 0, k
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2676 if (k
== 0 || ecmp(&p
->arr
[2*k
-1], evs
[i
]) != 0) {
2677 value_clear(p
->arr
[2*k
].d
);
2678 value_clear(p
->arr
[2*k
+1].d
);
2679 p
->arr
[2*k
] = *(evs
[i
]-1);
2680 p
->arr
[2*k
+1] = *(evs
[i
]);
2683 Polyhedron
*D
= EVALUE_DOMAIN(*(evs
[i
]-1));
2686 value_clear((evs
[i
]-1)->d
);
2690 L
->next
= EVALUE_DOMAIN(p
->arr
[2*k
-2]);
2691 EVALUE_SET_DOMAIN(p
->arr
[2*k
-2], D
);
2692 free_evalue_refs(evs
[i
]);
2696 for (i
= 2*k
; i
< p
->size
; ++i
)
2697 value_clear(p
->arr
[i
].d
);
2704 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2706 if (value_notzero_p(e
->x
.p
->arr
[2*i
+1].d
))
2708 H
= DomainConvex(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), 0);
2711 for (k
= 0; k
< e
->x
.p
->size
/2; ++k
) {
2712 Polyhedron
*D
, *N
, **P
;
2715 P
= &EVALUE_DOMAIN(e
->x
.p
->arr
[2*k
]);
2722 if (D
->NbEq
<= H
->NbEq
) {
2728 tmp
.x
.p
= new_enode(partition
, 2, e
->x
.p
->pos
);
2729 EVALUE_SET_DOMAIN(tmp
.x
.p
->arr
[0], Polyhedron_Copy(D
));
2730 evalue_copy(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*i
+1]);
2731 reduce_evalue(&tmp
);
2732 if (value_notzero_p(tmp
.d
) ||
2733 ecmp(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*k
+1]) != 0)
2736 D
->next
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2737 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]) = D
;
2740 free_evalue_refs(&tmp
);
2746 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2748 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2750 value_clear(e
->x
.p
->arr
[2*i
].d
);
2751 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2753 if (2*i
< e
->x
.p
->size
) {
2754 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2755 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2762 H
= DomainConvex(D
, 0);
2763 E
= DomainDifference(H
, D
, 0);
2765 D
= DomainDifference(H
, E
, 0);
2768 EVALUE_SET_DOMAIN(p
->arr
[2*i
], D
);
2772 /* Use smallest representative for coefficients in affine form in
2773 * argument of fractional.
2774 * Since any change will make the argument non-standard,
2775 * the containing evalue will have to be reduced again afterward.
2777 static void fractional_minimal_coefficients(enode
*p
)
2783 assert(p
->type
== fractional
);
2785 while (value_zero_p(pp
->d
)) {
2786 assert(pp
->x
.p
->type
== polynomial
);
2787 assert(pp
->x
.p
->size
== 2);
2788 assert(value_notzero_p(pp
->x
.p
->arr
[1].d
));
2789 mpz_mul_ui(twice
, pp
->x
.p
->arr
[1].x
.n
, 2);
2790 if (value_gt(twice
, pp
->x
.p
->arr
[1].d
))
2791 value_subtract(pp
->x
.p
->arr
[1].x
.n
,
2792 pp
->x
.p
->arr
[1].x
.n
, pp
->x
.p
->arr
[1].d
);
2793 pp
= &pp
->x
.p
->arr
[0];
2799 static Polyhedron
*polynomial_projection(enode
*p
, Polyhedron
*D
, Value
*d
,
2804 unsigned dim
= D
->Dimension
;
2805 Matrix
*T
= Matrix_Alloc(2, dim
+1);
2808 assert(p
->type
== fractional
|| p
->type
== flooring
);
2809 value_set_si(T
->p
[1][dim
], 1);
2810 evalue_extract_affine(&p
->arr
[0], T
->p
[0], &T
->p
[0][dim
], d
);
2811 I
= DomainImage(D
, T
, 0);
2812 H
= DomainConvex(I
, 0);
2822 static void replace_by_affine(evalue
*e
, Value offset
)
2829 value_init(inc
.x
.n
);
2830 value_set_si(inc
.d
, 1);
2831 value_oppose(inc
.x
.n
, offset
);
2832 eadd(&inc
, &p
->arr
[0]);
2833 reorder_terms_about(p
, &p
->arr
[0]); /* frees arr[0] */
2837 free_evalue_refs(&inc
);
2840 int evalue_range_reduction_in_domain(evalue
*e
, Polyhedron
*D
)
2849 if (value_notzero_p(e
->d
))
2854 if (p
->type
== relation
) {
2861 fractional_minimal_coefficients(p
->arr
[0].x
.p
);
2862 I
= polynomial_projection(p
->arr
[0].x
.p
, D
, &d
, &T
);
2863 bounded
= line_minmax(I
, &min
, &max
); /* frees I */
2864 equal
= value_eq(min
, max
);
2865 mpz_cdiv_q(min
, min
, d
);
2866 mpz_fdiv_q(max
, max
, d
);
2868 if (bounded
&& value_gt(min
, max
)) {
2874 evalue_set_si(e
, 0, 1);
2877 free_evalue_refs(&(p
->arr
[1]));
2878 free_evalue_refs(&(p
->arr
[0]));
2884 return r
? r
: evalue_range_reduction_in_domain(e
, D
);
2885 } else if (bounded
&& equal
) {
2888 free_evalue_refs(&(p
->arr
[2]));
2891 free_evalue_refs(&(p
->arr
[0]));
2897 return evalue_range_reduction_in_domain(e
, D
);
2898 } else if (bounded
&& value_eq(min
, max
)) {
2899 /* zero for a single value */
2901 Matrix
*M
= Matrix_Alloc(1, D
->Dimension
+2);
2902 Vector_Copy(T
->p
[0], M
->p
[0]+1, D
->Dimension
+1);
2903 value_multiply(min
, min
, d
);
2904 value_subtract(M
->p
[0][D
->Dimension
+1],
2905 M
->p
[0][D
->Dimension
+1], min
);
2906 E
= DomainAddConstraints(D
, M
, 0);
2912 r
= evalue_range_reduction_in_domain(&p
->arr
[1], E
);
2914 r
|= evalue_range_reduction_in_domain(&p
->arr
[2], D
);
2916 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2924 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2927 i
= p
->type
== relation
? 1 :
2928 p
->type
== fractional
? 1 : 0;
2929 for (; i
<p
->size
; i
++)
2930 r
|= evalue_range_reduction_in_domain(&p
->arr
[i
], D
);
2932 if (p
->type
!= fractional
) {
2933 if (r
&& p
->type
== polynomial
) {
2936 value_set_si(f
.d
, 0);
2937 f
.x
.p
= new_enode(polynomial
, 2, p
->pos
);
2938 evalue_set_si(&f
.x
.p
->arr
[0], 0, 1);
2939 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
2940 reorder_terms_about(p
, &f
);
2951 fractional_minimal_coefficients(p
);
2952 I
= polynomial_projection(p
, D
, &d
, NULL
);
2953 bounded
= line_minmax(I
, &min
, &max
); /* frees I */
2954 mpz_fdiv_q(min
, min
, d
);
2955 mpz_fdiv_q(max
, max
, d
);
2956 value_subtract(d
, max
, min
);
2958 if (bounded
&& value_eq(min
, max
)) {
2959 replace_by_affine(e
, min
);
2961 } else if (bounded
&& value_one_p(d
) && p
->size
> 3) {
2962 /* replace {g}^2 by -(g-min)^2 + (2{g}+1)*(g-min) - {g}
2963 * See pages 199-200 of PhD thesis.
2971 value_set_si(rem
.d
, 0);
2972 rem
.x
.p
= new_enode(fractional
, 3, -1);
2973 evalue_copy(&rem
.x
.p
->arr
[0], &p
->arr
[0]);
2974 value_clear(rem
.x
.p
->arr
[1].d
);
2975 value_clear(rem
.x
.p
->arr
[2].d
);
2976 rem
.x
.p
->arr
[1] = p
->arr
[1];
2977 rem
.x
.p
->arr
[2] = p
->arr
[2];
2978 for (i
= 3; i
< p
->size
; ++i
)
2979 p
->arr
[i
-2] = p
->arr
[i
];
2983 value_init(inc
.x
.n
);
2984 value_set_si(inc
.d
, 1);
2985 value_oppose(inc
.x
.n
, min
);
2988 evalue_copy(&t
, &p
->arr
[0]);
2992 value_set_si(f
.d
, 0);
2993 f
.x
.p
= new_enode(fractional
, 3, -1);
2994 evalue_copy(&f
.x
.p
->arr
[0], &p
->arr
[0]);
2995 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
2996 evalue_set_si(&f
.x
.p
->arr
[2], 2, 1);
2998 value_init(factor
.d
);
2999 evalue_set_si(&factor
, -1, 1);
3005 value_clear(f
.x
.p
->arr
[1].x
.n
);
3006 value_clear(f
.x
.p
->arr
[2].x
.n
);
3007 evalue_set_si(&f
.x
.p
->arr
[1], 0, 1);
3008 evalue_set_si(&f
.x
.p
->arr
[2], -1, 1);
3012 evalue_reorder_terms(&rem
);
3013 evalue_reorder_terms(e
);
3019 free_evalue_refs(&inc
);
3020 free_evalue_refs(&t
);
3021 free_evalue_refs(&f
);
3022 free_evalue_refs(&factor
);
3023 free_evalue_refs(&rem
);
3025 evalue_range_reduction_in_domain(e
, D
);
3029 _reduce_evalue(&p
->arr
[0], 0, 1);
3031 evalue_reorder_terms(e
);
3041 void evalue_range_reduction(evalue
*e
)
3044 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
3047 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3048 if (evalue_range_reduction_in_domain(&e
->x
.p
->arr
[2*i
+1],
3049 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]))) {
3050 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3052 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
3053 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
3054 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
3055 value_clear(e
->x
.p
->arr
[2*i
].d
);
3057 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
3058 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
3066 Enumeration
* partition2enumeration(evalue
*EP
)
3069 Enumeration
*en
, *res
= NULL
;
3071 if (EVALUE_IS_ZERO(*EP
)) {
3076 assert(value_zero_p(EP
->d
));
3077 assert(EP
->x
.p
->type
== partition
);
3078 assert(EP
->x
.p
->size
>= 2);
3080 for (i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
3081 assert(EP
->x
.p
->pos
== EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
])->Dimension
);
3082 en
= (Enumeration
*)malloc(sizeof(Enumeration
));
3085 res
->ValidityDomain
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
3086 value_clear(EP
->x
.p
->arr
[2*i
].d
);
3087 res
->EP
= EP
->x
.p
->arr
[2*i
+1];
3095 int evalue_frac2floor_in_domain3(evalue
*e
, Polyhedron
*D
, int shift
)
3104 if (value_notzero_p(e
->d
))
3109 i
= p
->type
== relation
? 1 :
3110 p
->type
== fractional
? 1 : 0;
3111 for (; i
<p
->size
; i
++)
3112 r
|= evalue_frac2floor_in_domain3(&p
->arr
[i
], D
, shift
);
3114 if (p
->type
!= fractional
) {
3115 if (r
&& p
->type
== polynomial
) {
3118 value_set_si(f
.d
, 0);
3119 f
.x
.p
= new_enode(polynomial
, 2, p
->pos
);
3120 evalue_set_si(&f
.x
.p
->arr
[0], 0, 1);
3121 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
3122 reorder_terms_about(p
, &f
);
3132 I
= polynomial_projection(p
, D
, &d
, NULL
);
3135 Polyhedron_Print(stderr, P_VALUE_FMT, I);
3138 assert(I
->NbEq
== 0); /* Should have been reduced */
3141 for (i
= 0; i
< I
->NbConstraints
; ++i
)
3142 if (value_pos_p(I
->Constraint
[i
][1]))
3145 if (i
< I
->NbConstraints
) {
3147 value_oppose(I
->Constraint
[i
][2], I
->Constraint
[i
][2]);
3148 mpz_cdiv_q(min
, I
->Constraint
[i
][2], I
->Constraint
[i
][1]);
3149 if (value_neg_p(min
)) {
3151 mpz_fdiv_q(min
, min
, d
);
3152 value_init(offset
.d
);
3153 value_set_si(offset
.d
, 1);
3154 value_init(offset
.x
.n
);
3155 value_oppose(offset
.x
.n
, min
);
3156 eadd(&offset
, &p
->arr
[0]);
3157 free_evalue_refs(&offset
);
3167 value_set_si(fl
.d
, 0);
3168 fl
.x
.p
= new_enode(flooring
, 3, -1);
3169 evalue_set_si(&fl
.x
.p
->arr
[1], 0, 1);
3170 evalue_set_si(&fl
.x
.p
->arr
[2], -1, 1);
3171 evalue_copy(&fl
.x
.p
->arr
[0], &p
->arr
[0]);
3173 eadd(&fl
, &p
->arr
[0]);
3174 reorder_terms_about(p
, &p
->arr
[0]);
3178 free_evalue_refs(&fl
);
3183 int evalue_frac2floor_in_domain(evalue
*e
, Polyhedron
*D
)
3185 return evalue_frac2floor_in_domain3(e
, D
, 1);
3188 void evalue_frac2floor2(evalue
*e
, int shift
)
3191 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
) {
3193 if (evalue_frac2floor_in_domain3(e
, NULL
, 0))
3199 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3200 if (evalue_frac2floor_in_domain3(&e
->x
.p
->arr
[2*i
+1],
3201 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), shift
))
3202 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3205 void evalue_frac2floor(evalue
*e
)
3207 evalue_frac2floor2(e
, 1);
3210 /* Add a new variable with lower bound 1 and upper bound specified
3211 * by row. If negative is true, then the new variable has upper
3212 * bound -1 and lower bound specified by row.
3214 static Matrix
*esum_add_constraint(int nvar
, Polyhedron
*D
, Matrix
*C
,
3215 Vector
*row
, int negative
)
3219 int nparam
= D
->Dimension
- nvar
;
3222 nr
= D
->NbConstraints
+ 2;
3223 nc
= D
->Dimension
+ 2 + 1;
3224 C
= Matrix_Alloc(nr
, nc
);
3225 for (i
= 0; i
< D
->NbConstraints
; ++i
) {
3226 Vector_Copy(D
->Constraint
[i
], C
->p
[i
], 1 + nvar
);
3227 Vector_Copy(D
->Constraint
[i
] + 1 + nvar
, C
->p
[i
] + 1 + nvar
+ 1,
3228 D
->Dimension
+ 1 - nvar
);
3233 nc
= C
->NbColumns
+ 1;
3234 C
= Matrix_Alloc(nr
, nc
);
3235 for (i
= 0; i
< oldC
->NbRows
; ++i
) {
3236 Vector_Copy(oldC
->p
[i
], C
->p
[i
], 1 + nvar
);
3237 Vector_Copy(oldC
->p
[i
] + 1 + nvar
, C
->p
[i
] + 1 + nvar
+ 1,
3238 oldC
->NbColumns
- 1 - nvar
);
3241 value_set_si(C
->p
[nr
-2][0], 1);
3243 value_set_si(C
->p
[nr
-2][1 + nvar
], -1);
3245 value_set_si(C
->p
[nr
-2][1 + nvar
], 1);
3246 value_set_si(C
->p
[nr
-2][nc
- 1], -1);
3248 Vector_Copy(row
->p
, C
->p
[nr
-1], 1 + nvar
+ 1);
3249 Vector_Copy(row
->p
+ 1 + nvar
+ 1, C
->p
[nr
-1] + C
->NbColumns
- 1 - nparam
,
3255 static void floor2frac_r(evalue
*e
, int nvar
)
3262 if (value_notzero_p(e
->d
))
3267 assert(p
->type
== flooring
);
3268 for (i
= 1; i
< p
->size
; i
++)
3269 floor2frac_r(&p
->arr
[i
], nvar
);
3271 for (pp
= &p
->arr
[0]; value_zero_p(pp
->d
); pp
= &pp
->x
.p
->arr
[0]) {
3272 assert(pp
->x
.p
->type
== polynomial
);
3273 pp
->x
.p
->pos
-= nvar
;
3277 value_set_si(f
.d
, 0);
3278 f
.x
.p
= new_enode(fractional
, 3, -1);
3279 evalue_set_si(&f
.x
.p
->arr
[1], 0, 1);
3280 evalue_set_si(&f
.x
.p
->arr
[2], -1, 1);
3281 evalue_copy(&f
.x
.p
->arr
[0], &p
->arr
[0]);
3283 eadd(&f
, &p
->arr
[0]);
3284 reorder_terms_about(p
, &p
->arr
[0]);
3288 free_evalue_refs(&f
);
3291 /* Convert flooring back to fractional and shift position
3292 * of the parameters by nvar
3294 static void floor2frac(evalue
*e
, int nvar
)
3296 floor2frac_r(e
, nvar
);
3300 int evalue_floor2frac(evalue
*e
)
3305 if (value_notzero_p(e
->d
))
3308 if (e
->x
.p
->type
== partition
) {
3309 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3310 if (evalue_floor2frac(&e
->x
.p
->arr
[2*i
+1]))
3311 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3315 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
3316 r
|= evalue_floor2frac(&e
->x
.p
->arr
[i
]);
3318 if (e
->x
.p
->type
== flooring
) {
3324 evalue_reorder_terms(e
);
3329 evalue
*esum_over_domain_cst(int nvar
, Polyhedron
*D
, Matrix
*C
)
3332 int nparam
= D
->Dimension
- nvar
;
3336 D
= Constraints2Polyhedron(C
, 0);
3340 t
= barvinok_enumerate_e(D
, 0, nparam
, 0);
3342 /* Double check that D was not unbounded. */
3343 assert(!(value_pos_p(t
->d
) && value_neg_p(t
->x
.n
)));
3351 static void domain_signs(Polyhedron
*D
, int *signs
)
3355 POL_ENSURE_VERTICES(D
);
3356 for (j
= 0; j
< D
->Dimension
; ++j
) {
3358 for (k
= 0; k
< D
->NbRays
; ++k
) {
3359 signs
[j
] = value_sign(D
->Ray
[k
][1+j
]);
3366 static evalue
*esum_over_domain(evalue
*e
, int nvar
, Polyhedron
*D
,
3367 int *signs
, Matrix
*C
, unsigned MaxRays
)
3373 evalue
*factor
= NULL
;
3377 if (EVALUE_IS_ZERO(*e
))
3381 Polyhedron
*DD
= Disjoint_Domain(D
, 0, MaxRays
);
3388 res
= esum_over_domain(e
, nvar
, Q
, signs
, C
, MaxRays
);
3391 for (Q
= DD
; Q
; Q
= DD
) {
3397 t
= esum_over_domain(e
, nvar
, Q
, signs
, C
, MaxRays
);
3410 if (value_notzero_p(e
->d
)) {
3413 t
= esum_over_domain_cst(nvar
, D
, C
);
3415 if (!EVALUE_IS_ONE(*e
))
3422 signs
= alloca(sizeof(int) * D
->Dimension
);
3423 domain_signs(D
, signs
);
3426 switch (e
->x
.p
->type
) {
3428 evalue
*pp
= &e
->x
.p
->arr
[0];
3430 if (pp
->x
.p
->pos
> nvar
) {
3431 /* remainder is independent of the summated vars */
3437 floor2frac(&f
, nvar
);
3439 t
= esum_over_domain_cst(nvar
, D
, C
);
3443 free_evalue_refs(&f
);
3448 row
= Vector_Alloc(1 + D
->Dimension
+ 1 + 1);
3449 poly_denom(pp
, &row
->p
[1 + nvar
]);
3450 value_set_si(row
->p
[0], 1);
3451 for (pp
= &e
->x
.p
->arr
[0]; value_zero_p(pp
->d
);
3452 pp
= &pp
->x
.p
->arr
[0]) {
3454 assert(pp
->x
.p
->type
== polynomial
);
3456 if (pos
>= 1 + nvar
)
3458 value_assign(row
->p
[pos
], row
->p
[1+nvar
]);
3459 value_division(row
->p
[pos
], row
->p
[pos
], pp
->x
.p
->arr
[1].d
);
3460 value_multiply(row
->p
[pos
], row
->p
[pos
], pp
->x
.p
->arr
[1].x
.n
);
3462 value_assign(row
->p
[1 + D
->Dimension
+ 1], row
->p
[1+nvar
]);
3463 value_division(row
->p
[1 + D
->Dimension
+ 1],
3464 row
->p
[1 + D
->Dimension
+ 1],
3466 value_multiply(row
->p
[1 + D
->Dimension
+ 1],
3467 row
->p
[1 + D
->Dimension
+ 1],
3469 value_oppose(row
->p
[1 + nvar
], row
->p
[1 + nvar
]);
3473 int pos
= e
->x
.p
->pos
;
3476 factor
= ALLOC(evalue
);
3477 value_init(factor
->d
);
3478 value_set_si(factor
->d
, 0);
3479 factor
->x
.p
= new_enode(polynomial
, 2, pos
- nvar
);
3480 evalue_set_si(&factor
->x
.p
->arr
[0], 0, 1);
3481 evalue_set_si(&factor
->x
.p
->arr
[1], 1, 1);
3485 row
= Vector_Alloc(1 + D
->Dimension
+ 1 + 1);
3486 negative
= signs
[pos
-1] < 0;
3487 value_set_si(row
->p
[0], 1);
3489 value_set_si(row
->p
[pos
], -1);
3490 value_set_si(row
->p
[1 + nvar
], 1);
3492 value_set_si(row
->p
[pos
], 1);
3493 value_set_si(row
->p
[1 + nvar
], -1);
3501 offset
= type_offset(e
->x
.p
);
3503 res
= esum_over_domain(&e
->x
.p
->arr
[offset
], nvar
, D
, signs
, C
, MaxRays
);
3507 evalue_copy(&cum
, factor
);
3511 for (i
= 1; offset
+i
< e
->x
.p
->size
; ++i
) {
3515 C
= esum_add_constraint(nvar
, D
, C
, row
, negative
);
3521 Vector_Print(stderr, P_VALUE_FMT, row);
3523 Matrix_Print(stderr, P_VALUE_FMT, C);
3525 t
= esum_over_domain(&e
->x
.p
->arr
[offset
+i
], nvar
, D
, signs
, C
, MaxRays
);
3530 if (negative
&& (i
% 2))
3540 if (factor
&& offset
+i
+1 < e
->x
.p
->size
)
3547 free_evalue_refs(&cum
);
3548 evalue_free(factor
);
3559 static void Polyhedron_Insert(Polyhedron
***next
, Polyhedron
*Q
)
3569 static Polyhedron
*Polyhedron_Split_Into_Orthants(Polyhedron
*P
,
3574 Vector
*c
= Vector_Alloc(1 + P
->Dimension
+ 1);
3575 value_set_si(c
->p
[0], 1);
3577 if (P
->Dimension
== 0)
3578 return Polyhedron_Copy(P
);
3580 for (i
= 0; i
< P
->Dimension
; ++i
) {
3581 Polyhedron
*L
= NULL
;
3582 Polyhedron
**next
= &L
;
3585 for (I
= D
; I
; I
= I
->next
) {
3587 value_set_si(c
->p
[1+i
], 1);
3588 value_set_si(c
->p
[1+P
->Dimension
], 0);
3589 Q
= AddConstraints(c
->p
, 1, I
, MaxRays
);
3590 Polyhedron_Insert(&next
, Q
);
3591 value_set_si(c
->p
[1+i
], -1);
3592 value_set_si(c
->p
[1+P
->Dimension
], -1);
3593 Q
= AddConstraints(c
->p
, 1, I
, MaxRays
);
3594 Polyhedron_Insert(&next
, Q
);
3595 value_set_si(c
->p
[1+i
], 0);
3605 /* Make arguments of all floors non-negative */
3606 static void shift_floor_in_domain(evalue
*e
, Polyhedron
*D
)
3613 if (value_notzero_p(e
->d
))
3618 for (i
= type_offset(p
); i
< p
->size
; ++i
)
3619 shift_floor_in_domain(&p
->arr
[i
], D
);
3621 if (p
->type
!= flooring
)
3627 I
= polynomial_projection(p
, D
, &d
, NULL
);
3628 assert(I
->NbEq
== 0); /* Should have been reduced */
3630 for (i
= 0; i
< I
->NbConstraints
; ++i
)
3631 if (value_pos_p(I
->Constraint
[i
][1]))
3633 assert(i
< I
->NbConstraints
);
3634 if (i
< I
->NbConstraints
) {
3635 value_oppose(I
->Constraint
[i
][2], I
->Constraint
[i
][2]);
3636 mpz_fdiv_q(m
, I
->Constraint
[i
][2], I
->Constraint
[i
][1]);
3637 if (value_neg_p(m
)) {
3638 /* replace [e] by [e-m]+m such that e-m >= 0 */
3643 value_set_si(f
.d
, 1);
3644 value_oppose(f
.x
.n
, m
);
3645 eadd(&f
, &p
->arr
[0]);
3648 value_set_si(f
.d
, 0);
3649 f
.x
.p
= new_enode(flooring
, 3, -1);
3650 value_clear(f
.x
.p
->arr
[0].d
);
3651 f
.x
.p
->arr
[0] = p
->arr
[0];
3652 evalue_set_si(&f
.x
.p
->arr
[2], 1, 1);
3653 value_set_si(f
.x
.p
->arr
[1].d
, 1);
3654 value_init(f
.x
.p
->arr
[1].x
.n
);
3655 value_assign(f
.x
.p
->arr
[1].x
.n
, m
);
3656 reorder_terms_about(p
, &f
);
3667 evalue
*box_summate(Polyhedron
*P
, evalue
*E
, unsigned nvar
, unsigned MaxRays
)
3669 evalue
*sum
= evalue_zero();
3670 Polyhedron
*D
= Polyhedron_Split_Into_Orthants(P
, MaxRays
);
3671 for (P
= D
; P
; P
= P
->next
) {
3673 evalue
*fe
= evalue_dup(E
);
3674 Polyhedron
*next
= P
->next
;
3676 reduce_evalue_in_domain(fe
, P
);
3677 evalue_frac2floor2(fe
, 0);
3678 shift_floor_in_domain(fe
, P
);
3679 t
= esum_over_domain(fe
, nvar
, P
, NULL
, NULL
, MaxRays
);
3691 /* Initial silly implementation */
3692 void eor(evalue
*e1
, evalue
*res
)
3698 evalue_set_si(&mone
, -1, 1);
3700 evalue_copy(&E
, res
);
3706 free_evalue_refs(&E
);
3707 free_evalue_refs(&mone
);
3710 /* computes denominator of polynomial evalue
3711 * d should point to a value initialized to 1
3713 void evalue_denom(const evalue
*e
, Value
*d
)
3717 if (value_notzero_p(e
->d
)) {
3718 value_lcm(*d
, *d
, e
->d
);
3721 assert(e
->x
.p
->type
== polynomial
||
3722 e
->x
.p
->type
== fractional
||
3723 e
->x
.p
->type
== flooring
);
3724 offset
= type_offset(e
->x
.p
);
3725 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3726 evalue_denom(&e
->x
.p
->arr
[i
], d
);
3729 /* Divides the evalue e by the integer n */
3730 void evalue_div(evalue
*e
, Value n
)
3734 if (value_one_p(n
) || EVALUE_IS_ZERO(*e
))
3737 if (value_notzero_p(e
->d
)) {
3740 value_multiply(e
->d
, e
->d
, n
);
3741 value_gcd(gc
, e
->x
.n
, e
->d
);
3742 if (value_notone_p(gc
)) {
3743 value_division(e
->d
, e
->d
, gc
);
3744 value_division(e
->x
.n
, e
->x
.n
, gc
);
3749 if (e
->x
.p
->type
== partition
) {
3750 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3751 evalue_div(&e
->x
.p
->arr
[2*i
+1], n
);
3754 offset
= type_offset(e
->x
.p
);
3755 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3756 evalue_div(&e
->x
.p
->arr
[i
], n
);
3759 /* Multiplies the evalue e by the integer n */
3760 void evalue_mul(evalue
*e
, Value n
)
3764 if (value_one_p(n
) || EVALUE_IS_ZERO(*e
))
3767 if (value_notzero_p(e
->d
)) {
3770 value_multiply(e
->x
.n
, e
->x
.n
, n
);
3771 value_gcd(gc
, e
->x
.n
, e
->d
);
3772 if (value_notone_p(gc
)) {
3773 value_division(e
->d
, e
->d
, gc
);
3774 value_division(e
->x
.n
, e
->x
.n
, gc
);
3779 if (e
->x
.p
->type
== partition
) {
3780 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3781 evalue_mul(&e
->x
.p
->arr
[2*i
+1], n
);
3784 offset
= type_offset(e
->x
.p
);
3785 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3786 evalue_mul(&e
->x
.p
->arr
[i
], n
);
3789 /* Multiplies the evalue e by the n/d */
3790 void evalue_mul_div(evalue
*e
, Value n
, Value d
)
3794 if ((value_one_p(n
) && value_one_p(d
)) || EVALUE_IS_ZERO(*e
))
3797 if (value_notzero_p(e
->d
)) {
3800 value_multiply(e
->x
.n
, e
->x
.n
, n
);
3801 value_multiply(e
->d
, e
->d
, d
);
3802 value_gcd(gc
, e
->x
.n
, e
->d
);
3803 if (value_notone_p(gc
)) {
3804 value_division(e
->d
, e
->d
, gc
);
3805 value_division(e
->x
.n
, e
->x
.n
, gc
);
3810 if (e
->x
.p
->type
== partition
) {
3811 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3812 evalue_mul_div(&e
->x
.p
->arr
[2*i
+1], n
, d
);
3815 offset
= type_offset(e
->x
.p
);
3816 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3817 evalue_mul_div(&e
->x
.p
->arr
[i
], n
, d
);
3820 void evalue_negate(evalue
*e
)
3824 if (value_notzero_p(e
->d
)) {
3825 value_oppose(e
->x
.n
, e
->x
.n
);
3828 if (e
->x
.p
->type
== partition
) {
3829 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3830 evalue_negate(&e
->x
.p
->arr
[2*i
+1]);
3833 offset
= type_offset(e
->x
.p
);
3834 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3835 evalue_negate(&e
->x
.p
->arr
[i
]);
3838 void evalue_add_constant(evalue
*e
, const Value cst
)
3842 if (value_zero_p(e
->d
)) {
3843 if (e
->x
.p
->type
== partition
) {
3844 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3845 evalue_add_constant(&e
->x
.p
->arr
[2*i
+1], cst
);
3848 if (e
->x
.p
->type
== relation
) {
3849 for (i
= 1; i
< e
->x
.p
->size
; ++i
)
3850 evalue_add_constant(&e
->x
.p
->arr
[i
], cst
);
3854 e
= &e
->x
.p
->arr
[type_offset(e
->x
.p
)];
3855 } while (value_zero_p(e
->d
));
3857 value_addmul(e
->x
.n
, cst
, e
->d
);
3860 static void evalue_frac2polynomial_r(evalue
*e
, int *signs
, int sign
, int in_frac
)
3865 int sign_odd
= sign
;
3867 if (value_notzero_p(e
->d
)) {
3868 if (in_frac
&& sign
* value_sign(e
->x
.n
) < 0) {
3869 value_set_si(e
->x
.n
, 0);
3870 value_set_si(e
->d
, 1);
3875 if (e
->x
.p
->type
== relation
) {
3876 for (i
= e
->x
.p
->size
-1; i
>= 1; --i
)
3877 evalue_frac2polynomial_r(&e
->x
.p
->arr
[i
], signs
, sign
, in_frac
);
3881 if (e
->x
.p
->type
== polynomial
)
3882 sign_odd
*= signs
[e
->x
.p
->pos
-1];
3883 offset
= type_offset(e
->x
.p
);
3884 evalue_frac2polynomial_r(&e
->x
.p
->arr
[offset
], signs
, sign
, in_frac
);
3885 in_frac
|= e
->x
.p
->type
== fractional
;
3886 for (i
= e
->x
.p
->size
-1; i
> offset
; --i
)
3887 evalue_frac2polynomial_r(&e
->x
.p
->arr
[i
], signs
,
3888 (i
- offset
) % 2 ? sign_odd
: sign
, in_frac
);
3890 if (e
->x
.p
->type
!= fractional
)
3893 /* replace { a/m } by (m-1)/m if sign != 0
3894 * and by (m-1)/(2m) if sign == 0
3898 evalue_denom(&e
->x
.p
->arr
[0], &d
);
3899 free_evalue_refs(&e
->x
.p
->arr
[0]);
3900 value_init(e
->x
.p
->arr
[0].d
);
3901 value_init(e
->x
.p
->arr
[0].x
.n
);
3903 value_addto(e
->x
.p
->arr
[0].d
, d
, d
);
3905 value_assign(e
->x
.p
->arr
[0].d
, d
);
3906 value_decrement(e
->x
.p
->arr
[0].x
.n
, d
);
3910 reorder_terms_about(p
, &p
->arr
[0]);
3916 /* Approximate the evalue in fractional representation by a polynomial.
3917 * If sign > 0, the result is an upper bound;
3918 * if sign < 0, the result is a lower bound;
3919 * if sign = 0, the result is an intermediate approximation.
3921 void evalue_frac2polynomial(evalue
*e
, int sign
, unsigned MaxRays
)
3926 if (value_notzero_p(e
->d
))
3928 assert(e
->x
.p
->type
== partition
);
3929 /* make sure all variables in the domains have a fixed sign */
3931 evalue_split_domains_into_orthants(e
, MaxRays
);
3932 if (EVALUE_IS_ZERO(*e
))
3936 assert(e
->x
.p
->size
>= 2);
3937 dim
= EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
;
3939 signs
= alloca(sizeof(int) * dim
);
3942 for (i
= 0; i
< dim
; ++i
)
3944 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
3946 domain_signs(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), signs
);
3947 evalue_frac2polynomial_r(&e
->x
.p
->arr
[2*i
+1], signs
, sign
, 0);
3951 /* Split the domains of e (which is assumed to be a partition)
3952 * such that each resulting domain lies entirely in one orthant.
3954 void evalue_split_domains_into_orthants(evalue
*e
, unsigned MaxRays
)
3957 assert(value_zero_p(e
->d
));
3958 assert(e
->x
.p
->type
== partition
);
3959 assert(e
->x
.p
->size
>= 2);
3960 dim
= EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
;
3962 for (i
= 0; i
< dim
; ++i
) {
3965 C
= Matrix_Alloc(1, 1 + dim
+ 1);
3966 value_set_si(C
->p
[0][0], 1);
3967 value_init(split
.d
);
3968 value_set_si(split
.d
, 0);
3969 split
.x
.p
= new_enode(partition
, 4, dim
);
3970 value_set_si(C
->p
[0][1+i
], 1);
3971 C2
= Matrix_Copy(C
);
3972 EVALUE_SET_DOMAIN(split
.x
.p
->arr
[0], Constraints2Polyhedron(C2
, MaxRays
));
3974 evalue_set_si(&split
.x
.p
->arr
[1], 1, 1);
3975 value_set_si(C
->p
[0][1+i
], -1);
3976 value_set_si(C
->p
[0][1+dim
], -1);
3977 EVALUE_SET_DOMAIN(split
.x
.p
->arr
[2], Constraints2Polyhedron(C
, MaxRays
));
3978 evalue_set_si(&split
.x
.p
->arr
[3], 1, 1);
3980 free_evalue_refs(&split
);
3985 static evalue
*find_fractional_with_max_periods(evalue
*e
, Polyhedron
*D
,
3988 Value
*min
, Value
*max
)
3995 if (value_notzero_p(e
->d
))
3998 if (e
->x
.p
->type
== fractional
) {
4003 I
= polynomial_projection(e
->x
.p
, D
, &d
, &T
);
4004 bounded
= line_minmax(I
, min
, max
); /* frees I */
4008 value_set_si(mp
, max_periods
);
4009 mpz_fdiv_q(*min
, *min
, d
);
4010 mpz_fdiv_q(*max
, *max
, d
);
4011 value_assign(T
->p
[1][D
->Dimension
], d
);
4012 value_subtract(d
, *max
, *min
);
4013 if (value_ge(d
, mp
))
4016 f
= evalue_dup(&e
->x
.p
->arr
[0]);
4027 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4028 if ((f
= find_fractional_with_max_periods(&e
->x
.p
->arr
[i
], D
, max_periods
,
4035 static void replace_fract_by_affine(evalue
*e
, evalue
*f
, Value val
)
4039 if (value_notzero_p(e
->d
))
4042 offset
= type_offset(e
->x
.p
);
4043 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
4044 replace_fract_by_affine(&e
->x
.p
->arr
[i
], f
, val
);
4046 if (e
->x
.p
->type
!= fractional
)
4049 if (!eequal(&e
->x
.p
->arr
[0], f
))
4052 replace_by_affine(e
, val
);
4055 /* Look for fractional parts that can be removed by splitting the corresponding
4056 * domain into at most max_periods parts.
4057 * We use a very simply strategy that looks for the first fractional part
4058 * that satisfies the condition, performs the split and then continues
4059 * looking for other fractional parts in the split domains until no
4060 * such fractional part can be found anymore.
4062 void evalue_split_periods(evalue
*e
, int max_periods
, unsigned int MaxRays
)
4069 if (EVALUE_IS_ZERO(*e
))
4071 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
) {
4073 "WARNING: evalue_split_periods called on incorrect evalue type\n");
4081 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
4086 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
4088 f
= find_fractional_with_max_periods(&e
->x
.p
->arr
[2*i
+1], D
, max_periods
,
4093 M
= Matrix_Alloc(2, 2+D
->Dimension
);
4095 value_subtract(d
, max
, min
);
4096 n
= VALUE_TO_INT(d
)+1;
4098 value_set_si(M
->p
[0][0], 1);
4099 Vector_Copy(T
->p
[0], M
->p
[0]+1, D
->Dimension
+1);
4100 value_multiply(d
, max
, T
->p
[1][D
->Dimension
]);
4101 value_subtract(M
->p
[0][1+D
->Dimension
], M
->p
[0][1+D
->Dimension
], d
);
4102 value_set_si(d
, -1);
4103 value_set_si(M
->p
[1][0], 1);
4104 Vector_Scale(T
->p
[0], M
->p
[1]+1, d
, D
->Dimension
+1);
4105 value_addmul(M
->p
[1][1+D
->Dimension
], max
, T
->p
[1][D
->Dimension
]);
4106 value_addto(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
],
4107 T
->p
[1][D
->Dimension
]);
4108 value_decrement(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
]);
4110 p
= new_enode(partition
, e
->x
.p
->size
+ (n
-1)*2, e
->x
.p
->pos
);
4111 for (j
= 0; j
< 2*i
; ++j
) {
4112 value_clear(p
->arr
[j
].d
);
4113 p
->arr
[j
] = e
->x
.p
->arr
[j
];
4115 for (j
= 2*i
+2; j
< e
->x
.p
->size
; ++j
) {
4116 value_clear(p
->arr
[j
+2*(n
-1)].d
);
4117 p
->arr
[j
+2*(n
-1)] = e
->x
.p
->arr
[j
];
4119 for (j
= n
-1; j
>= 0; --j
) {
4121 value_clear(p
->arr
[2*i
+1].d
);
4122 p
->arr
[2*i
+1] = e
->x
.p
->arr
[2*i
+1];
4124 evalue_copy(&p
->arr
[2*(i
+j
)+1], &e
->x
.p
->arr
[2*i
+1]);
4126 value_subtract(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
],
4127 T
->p
[1][D
->Dimension
]);
4128 value_addto(M
->p
[0][1+D
->Dimension
], M
->p
[0][1+D
->Dimension
],
4129 T
->p
[1][D
->Dimension
]);
4131 replace_fract_by_affine(&p
->arr
[2*(i
+j
)+1], f
, max
);
4132 E
= DomainAddConstraints(D
, M
, MaxRays
);
4133 EVALUE_SET_DOMAIN(p
->arr
[2*(i
+j
)], E
);
4134 if (evalue_range_reduction_in_domain(&p
->arr
[2*(i
+j
)+1], E
))
4135 reduce_evalue(&p
->arr
[2*(i
+j
)+1]);
4136 value_decrement(max
, max
);
4138 value_clear(e
->x
.p
->arr
[2*i
].d
);
4153 void evalue_extract_affine(const evalue
*e
, Value
*coeff
, Value
*cst
, Value
*d
)
4155 value_set_si(*d
, 1);
4157 for ( ; value_zero_p(e
->d
); e
= &e
->x
.p
->arr
[0]) {
4159 assert(e
->x
.p
->type
== polynomial
);
4160 assert(e
->x
.p
->size
== 2);
4161 c
= &e
->x
.p
->arr
[1];
4162 value_multiply(coeff
[e
->x
.p
->pos
-1], *d
, c
->x
.n
);
4163 value_division(coeff
[e
->x
.p
->pos
-1], coeff
[e
->x
.p
->pos
-1], c
->d
);
4165 value_multiply(*cst
, *d
, e
->x
.n
);
4166 value_division(*cst
, *cst
, e
->d
);
4169 /* returns an evalue that corresponds to
4173 static evalue
*term(int param
, Value c
, Value den
)
4175 evalue
*EP
= ALLOC(evalue
);
4177 value_set_si(EP
->d
,0);
4178 EP
->x
.p
= new_enode(polynomial
, 2, param
+ 1);
4179 evalue_set_si(&EP
->x
.p
->arr
[0], 0, 1);
4180 evalue_set_reduce(&EP
->x
.p
->arr
[1], c
, den
);
4184 evalue
*affine2evalue(Value
*coeff
, Value denom
, int nvar
)
4187 evalue
*E
= ALLOC(evalue
);
4189 evalue_set_reduce(E
, coeff
[nvar
], denom
);
4190 for (i
= 0; i
< nvar
; ++i
) {
4192 if (value_zero_p(coeff
[i
]))
4194 t
= term(i
, coeff
[i
], denom
);
4201 void evalue_substitute(evalue
*e
, evalue
**subs
)
4207 if (value_notzero_p(e
->d
))
4211 assert(p
->type
!= partition
);
4213 for (i
= 0; i
< p
->size
; ++i
)
4214 evalue_substitute(&p
->arr
[i
], subs
);
4216 if (p
->type
== relation
) {
4217 /* For relation a ? b : c, compute (a' ? 1) * b' + (a' ? 0 : 1) * c' */
4221 value_set_si(v
->d
, 0);
4222 v
->x
.p
= new_enode(relation
, 3, 0);
4223 evalue_copy(&v
->x
.p
->arr
[0], &p
->arr
[0]);
4224 evalue_set_si(&v
->x
.p
->arr
[1], 0, 1);
4225 evalue_set_si(&v
->x
.p
->arr
[2], 1, 1);
4226 emul(v
, &p
->arr
[2]);
4231 value_set_si(v
->d
, 0);
4232 v
->x
.p
= new_enode(relation
, 2, 0);
4233 value_clear(v
->x
.p
->arr
[0].d
);
4234 v
->x
.p
->arr
[0] = p
->arr
[0];
4235 evalue_set_si(&v
->x
.p
->arr
[1], 1, 1);
4236 emul(v
, &p
->arr
[1]);
4239 eadd(&p
->arr
[2], &p
->arr
[1]);
4240 free_evalue_refs(&p
->arr
[2]);
4248 if (p
->type
== polynomial
)
4253 value_set_si(v
->d
, 0);
4254 v
->x
.p
= new_enode(p
->type
, 3, -1);
4255 value_clear(v
->x
.p
->arr
[0].d
);
4256 v
->x
.p
->arr
[0] = p
->arr
[0];
4257 evalue_set_si(&v
->x
.p
->arr
[1], 0, 1);
4258 evalue_set_si(&v
->x
.p
->arr
[2], 1, 1);
4261 offset
= type_offset(p
);
4263 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
4264 emul(v
, &p
->arr
[i
]);
4265 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
4266 free_evalue_refs(&(p
->arr
[i
]));
4269 if (p
->type
!= polynomial
)
4273 *e
= p
->arr
[offset
];
4277 /* evalue e is given in terms of "new" parameter; CP maps the new
4278 * parameters back to the old parameters.
4279 * Transforms e such that it refers back to the old parameters and
4280 * adds appropriate constraints to the domain.
4281 * In particular, if CP maps the new parameters onto an affine
4282 * subspace of the old parameters, then the corresponding equalities
4283 * are added to the domain.
4284 * Also, if any of the new parameters was a rational combination
4285 * of the old parameters $p' = (<a, p> + c)/m$, then modulo
4286 * constraints ${<a, p> + c)/m} = 0$ are added to ensure
4287 * the new evalue remains non-zero only for integer parameters
4288 * of the new parameters (which have been removed by the substitution).
4290 void evalue_backsubstitute(evalue
*e
, Matrix
*CP
, unsigned MaxRays
)
4297 unsigned nparam
= CP
->NbColumns
-1;
4301 if (EVALUE_IS_ZERO(*e
))
4304 assert(value_zero_p(e
->d
));
4306 assert(p
->type
== partition
);
4308 inv
= left_inverse(CP
, &eq
);
4309 subs
= ALLOCN(evalue
*, nparam
);
4310 for (i
= 0; i
< nparam
; ++i
)
4311 subs
[i
] = affine2evalue(inv
->p
[i
], inv
->p
[nparam
][inv
->NbColumns
-1],
4314 CEq
= Constraints2Polyhedron(eq
, MaxRays
);
4315 addeliminatedparams_partition(p
, inv
, CEq
, inv
->NbColumns
-1, MaxRays
);
4316 Polyhedron_Free(CEq
);
4318 for (i
= 0; i
< p
->size
/2; ++i
)
4319 evalue_substitute(&p
->arr
[2*i
+1], subs
);
4321 for (i
= 0; i
< nparam
; ++i
)
4322 evalue_free(subs
[i
]);
4326 for (i
= 0; i
< inv
->NbRows
-1; ++i
) {
4327 Vector_Gcd(inv
->p
[i
], inv
->NbColumns
, &gcd
);
4328 value_gcd(gcd
, gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]);
4329 if (value_eq(gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]))
4331 Vector_AntiScale(inv
->p
[i
], inv
->p
[i
], gcd
, inv
->NbColumns
);
4332 value_divexact(gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1], gcd
);
4334 for (j
= 0; j
< p
->size
/2; ++j
) {
4335 evalue
*arg
= affine2evalue(inv
->p
[i
], gcd
, inv
->NbColumns
-1);
4340 value_set_si(rel
.d
, 0);
4341 rel
.x
.p
= new_enode(relation
, 2, 0);
4342 value_clear(rel
.x
.p
->arr
[1].d
);
4343 rel
.x
.p
->arr
[1] = p
->arr
[2*j
+1];
4344 ev
= &rel
.x
.p
->arr
[0];
4345 value_set_si(ev
->d
, 0);
4346 ev
->x
.p
= new_enode(fractional
, 3, -1);
4347 evalue_set_si(&ev
->x
.p
->arr
[1], 0, 1);
4348 evalue_set_si(&ev
->x
.p
->arr
[2], 1, 1);
4349 value_clear(ev
->x
.p
->arr
[0].d
);
4350 ev
->x
.p
->arr
[0] = *arg
;
4353 p
->arr
[2*j
+1] = rel
;
4364 * \sum_{i=0}^n c_i/d X^i
4366 * where d is the last element in the vector c.
4368 evalue
*evalue_polynomial(Vector
*c
, const evalue
* X
)
4370 unsigned dim
= c
->Size
-2;
4372 evalue
*EP
= ALLOC(evalue
);
4377 if (EVALUE_IS_ZERO(*X
) || dim
== 0) {
4378 evalue_set(EP
, c
->p
[0], c
->p
[dim
+1]);
4379 reduce_constant(EP
);
4383 evalue_set(EP
, c
->p
[dim
], c
->p
[dim
+1]);
4386 evalue_set(&EC
, c
->p
[dim
], c
->p
[dim
+1]);
4388 for (i
= dim
-1; i
>= 0; --i
) {
4390 value_assign(EC
.x
.n
, c
->p
[i
]);
4393 free_evalue_refs(&EC
);
4397 /* Create an evalue from an array of pairs of domains and evalues. */
4398 evalue
*evalue_from_section_array(struct evalue_section
*s
, int n
)
4403 res
= ALLOC(evalue
);
4407 evalue_set_si(res
, 0, 1);
4409 value_set_si(res
->d
, 0);
4410 res
->x
.p
= new_enode(partition
, 2*n
, s
[0].D
->Dimension
);
4411 for (i
= 0; i
< n
; ++i
) {
4412 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*i
], s
[i
].D
);
4413 value_clear(res
->x
.p
->arr
[2*i
+1].d
);
4414 res
->x
.p
->arr
[2*i
+1] = *s
[i
].E
;
4421 /* shift variables (>= first, 0-based) in polynomial n up (may be negative) */
4422 void evalue_shift_variables(evalue
*e
, int first
, int n
)
4425 if (value_notzero_p(e
->d
))
4427 assert(e
->x
.p
->type
== polynomial
||
4428 e
->x
.p
->type
== flooring
||
4429 e
->x
.p
->type
== fractional
);
4430 if (e
->x
.p
->type
== polynomial
&& e
->x
.p
->pos
>= first
+1) {
4431 assert(e
->x
.p
->pos
+ n
>= 1);
4434 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
4435 evalue_shift_variables(&e
->x
.p
->arr
[i
], first
, n
);
4438 static const evalue
*outer_floor(evalue
*e
, const evalue
*outer
)
4442 if (value_notzero_p(e
->d
))
4444 switch (e
->x
.p
->type
) {
4446 if (!outer
|| evalue_level_cmp(outer
, &e
->x
.p
->arr
[0]) > 0)
4447 return &e
->x
.p
->arr
[0];
4453 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4454 outer
= outer_floor(&e
->x
.p
->arr
[i
], outer
);
4457 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
4458 outer
= outer_floor(&e
->x
.p
->arr
[2*i
+1], outer
);
4465 /* Find and return outermost floor argument or NULL if e has no floors */
4466 evalue
*evalue_outer_floor(evalue
*e
)
4468 const evalue
*floor
= outer_floor(e
, NULL
);
4469 return floor
? evalue_dup(floor
): NULL
;
4472 static void evalue_set_to_zero(evalue
*e
)
4474 if (EVALUE_IS_ZERO(*e
))
4476 if (value_zero_p(e
->d
)) {
4477 free_evalue_refs(e
);
4481 value_set_si(e
->d
, 1);
4482 value_set_si(e
->x
.n
, 0);
4485 /* Replace (outer) floor with argument "floor" by variable "var" (0-based)
4486 * and drop terms not containing the floor.
4487 * Returns true if e contains the floor.
4489 int evalue_replace_floor(evalue
*e
, const evalue
*floor
, int var
)
4495 if (value_notzero_p(e
->d
))
4497 switch (e
->x
.p
->type
) {
4499 if (!eequal(floor
, &e
->x
.p
->arr
[0]))
4501 e
->x
.p
->type
= polynomial
;
4502 e
->x
.p
->pos
= 1 + var
;
4504 free_evalue_refs(&e
->x
.p
->arr
[0]);
4505 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
4506 e
->x
.p
->arr
[i
] = e
->x
.p
->arr
[i
+1];
4507 evalue_set_to_zero(&e
->x
.p
->arr
[0]);
4512 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
) {
4513 int c
= evalue_replace_floor(&e
->x
.p
->arr
[i
], floor
, var
);
4516 evalue_set_to_zero(&e
->x
.p
->arr
[i
]);
4517 if (c
&& !reorder
&& evalue_level_cmp(&e
->x
.p
->arr
[i
], e
) < 0)
4520 evalue_reduce_size(e
);
4522 evalue_reorder_terms(e
);
4530 /* Replace (outer) floor with argument "floor" by variable zero */
4531 void evalue_drop_floor(evalue
*e
, const evalue
*floor
)
4536 if (value_notzero_p(e
->d
))
4538 switch (e
->x
.p
->type
) {
4540 if (!eequal(floor
, &e
->x
.p
->arr
[0]))
4543 free_evalue_refs(&p
->arr
[0]);
4544 for (i
= 2; i
< p
->size
; ++i
)
4545 free_evalue_refs(&p
->arr
[i
]);
4553 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4554 evalue_drop_floor(&e
->x
.p
->arr
[i
], floor
);
4555 evalue_reduce_size(e
);