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 /***********************************************************************/
15 #include <barvinok/evalue.h>
16 #include <barvinok/barvinok.h>
17 #include <barvinok/util.h>
20 #ifndef value_pmodulus
21 #define value_pmodulus(ref,val1,val2) (mpz_fdiv_r((ref),(val1),(val2)))
24 #define ALLOC(type) (type*)malloc(sizeof(type))
25 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
28 #define NALLOC(p,n) p = (typeof(p))malloc((n) * sizeof(*p))
30 #define NALLOC(p,n) p = (void *)malloc((n) * sizeof(*p))
33 void evalue_set_si(evalue
*ev
, int n
, int d
) {
34 value_set_si(ev
->d
, d
);
36 value_set_si(ev
->x
.n
, n
);
39 void evalue_set(evalue
*ev
, Value n
, Value d
) {
40 value_assign(ev
->d
, d
);
42 value_assign(ev
->x
.n
, n
);
45 void evalue_set_reduce(evalue
*ev
, Value n
, Value d
) {
47 value_gcd(ev
->x
.n
, n
, d
);
48 value_divexact(ev
->d
, d
, ev
->x
.n
);
49 value_divexact(ev
->x
.n
, n
, ev
->x
.n
);
54 evalue
*EP
= ALLOC(evalue
);
56 evalue_set_si(EP
, 0, 1);
62 evalue
*EP
= ALLOC(evalue
);
64 value_set_si(EP
->d
, -2);
69 /* returns an evalue that corresponds to
73 evalue
*evalue_var(int var
)
75 evalue
*EP
= ALLOC(evalue
);
77 value_set_si(EP
->d
,0);
78 EP
->x
.p
= new_enode(polynomial
, 2, var
+ 1);
79 evalue_set_si(&EP
->x
.p
->arr
[0], 0, 1);
80 evalue_set_si(&EP
->x
.p
->arr
[1], 1, 1);
84 void aep_evalue(evalue
*e
, int *ref
) {
89 if (value_notzero_p(e
->d
))
90 return; /* a rational number, its already reduced */
92 return; /* hum... an overflow probably occured */
94 /* First check the components of p */
95 for (i
=0;i
<p
->size
;i
++)
96 aep_evalue(&p
->arr
[i
],ref
);
103 p
->pos
= ref
[p
->pos
-1]+1;
109 void addeliminatedparams_evalue(evalue
*e
,Matrix
*CT
) {
115 if (value_notzero_p(e
->d
))
116 return; /* a rational number, its already reduced */
118 return; /* hum... an overflow probably occured */
121 ref
= (int *)malloc(sizeof(int)*(CT
->NbRows
-1));
122 for(i
=0;i
<CT
->NbRows
-1;i
++)
123 for(j
=0;j
<CT
->NbColumns
;j
++)
124 if(value_notzero_p(CT
->p
[i
][j
])) {
129 /* Transform the references in e, using ref */
133 } /* addeliminatedparams_evalue */
135 static void addeliminatedparams_partition(enode
*p
, Matrix
*CT
, Polyhedron
*CEq
,
136 unsigned nparam
, unsigned MaxRays
)
139 assert(p
->type
== partition
);
142 for (i
= 0; i
< p
->size
/2; i
++) {
143 Polyhedron
*D
= EVALUE_DOMAIN(p
->arr
[2*i
]);
144 Polyhedron
*T
= DomainPreimage(D
, CT
, MaxRays
);
148 T
= DomainIntersection(D
, CEq
, MaxRays
);
151 EVALUE_SET_DOMAIN(p
->arr
[2*i
], T
);
155 void addeliminatedparams_enum(evalue
*e
, Matrix
*CT
, Polyhedron
*CEq
,
156 unsigned MaxRays
, unsigned nparam
)
161 if (CT
->NbRows
== CT
->NbColumns
)
164 if (EVALUE_IS_ZERO(*e
))
167 if (value_notzero_p(e
->d
)) {
170 value_set_si(res
.d
, 0);
171 res
.x
.p
= new_enode(partition
, 2, nparam
);
172 EVALUE_SET_DOMAIN(res
.x
.p
->arr
[0],
173 DomainConstraintSimplify(Polyhedron_Copy(CEq
), MaxRays
));
174 value_clear(res
.x
.p
->arr
[1].d
);
175 res
.x
.p
->arr
[1] = *e
;
183 addeliminatedparams_partition(p
, CT
, CEq
, nparam
, MaxRays
);
184 for (i
= 0; i
< p
->size
/2; i
++)
185 addeliminatedparams_evalue(&p
->arr
[2*i
+1], CT
);
188 static int mod_rational_cmp(evalue
*e1
, evalue
*e2
)
196 assert(value_notzero_p(e1
->d
));
197 assert(value_notzero_p(e2
->d
));
198 value_multiply(m
, e1
->x
.n
, e2
->d
);
199 value_multiply(m2
, e2
->x
.n
, e1
->d
);
202 else if (value_gt(m
, m2
))
212 static int mod_term_cmp_r(evalue
*e1
, evalue
*e2
)
214 if (value_notzero_p(e1
->d
)) {
216 if (value_zero_p(e2
->d
))
218 return mod_rational_cmp(e1
, e2
);
220 if (value_notzero_p(e2
->d
))
222 if (e1
->x
.p
->pos
< e2
->x
.p
->pos
)
224 else if (e1
->x
.p
->pos
> e2
->x
.p
->pos
)
227 int r
= mod_rational_cmp(&e1
->x
.p
->arr
[1], &e2
->x
.p
->arr
[1]);
229 ? mod_term_cmp_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0])
234 static int mod_term_cmp(const evalue
*e1
, const evalue
*e2
)
236 assert(value_zero_p(e1
->d
));
237 assert(value_zero_p(e2
->d
));
238 assert(e1
->x
.p
->type
== fractional
|| e1
->x
.p
->type
== flooring
);
239 assert(e2
->x
.p
->type
== fractional
|| e2
->x
.p
->type
== flooring
);
240 return mod_term_cmp_r(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]);
243 static void check_order(const evalue
*e
)
248 if (value_notzero_p(e
->d
))
251 switch (e
->x
.p
->type
) {
253 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
254 check_order(&e
->x
.p
->arr
[2*i
+1]);
257 for (i
= 1; i
< e
->x
.p
->size
; ++i
) {
259 if (value_notzero_p(a
->d
))
261 switch (a
->x
.p
->type
) {
263 assert(mod_term_cmp(&e
->x
.p
->arr
[0], &a
->x
.p
->arr
[0]) < 0);
272 for (i
= 0; i
< e
->x
.p
->size
; ++i
) {
274 if (value_notzero_p(a
->d
))
276 switch (a
->x
.p
->type
) {
278 assert(e
->x
.p
->pos
< a
->x
.p
->pos
);
289 for (i
= 1; i
< e
->x
.p
->size
; ++i
) {
291 if (value_notzero_p(a
->d
))
293 switch (a
->x
.p
->type
) {
304 /* Negative pos means inequality */
305 /* s is negative of substitution if m is not zero */
314 struct fixed_param
*fixed
;
319 static int relations_depth(evalue
*e
)
324 value_zero_p(e
->d
) && e
->x
.p
->type
== relation
;
325 e
= &e
->x
.p
->arr
[1], ++d
);
329 static void poly_denom_not_constant(evalue
**pp
, Value
*d
)
334 while (value_zero_p(p
->d
)) {
335 assert(p
->x
.p
->type
== polynomial
);
336 assert(p
->x
.p
->size
== 2);
337 assert(value_notzero_p(p
->x
.p
->arr
[1].d
));
338 value_lcm(*d
, *d
, p
->x
.p
->arr
[1].d
);
344 static void poly_denom(evalue
*p
, Value
*d
)
346 poly_denom_not_constant(&p
, d
);
347 value_lcm(*d
, *d
, p
->d
);
350 static void realloc_substitution(struct subst
*s
, int d
)
352 struct fixed_param
*n
;
355 for (i
= 0; i
< s
->n
; ++i
)
362 static int add_modulo_substitution(struct subst
*s
, evalue
*r
)
368 assert(value_zero_p(r
->d
) && r
->x
.p
->type
== relation
);
371 /* May have been reduced already */
372 if (value_notzero_p(m
->d
))
375 assert(value_zero_p(m
->d
) && m
->x
.p
->type
== fractional
);
376 assert(m
->x
.p
->size
== 3);
378 /* fractional was inverted during reduction
379 * invert it back and move constant in
381 if (!EVALUE_IS_ONE(m
->x
.p
->arr
[2])) {
382 assert(value_pos_p(m
->x
.p
->arr
[2].d
));
383 assert(value_mone_p(m
->x
.p
->arr
[2].x
.n
));
384 value_set_si(m
->x
.p
->arr
[2].x
.n
, 1);
385 value_increment(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].x
.n
);
386 assert(value_eq(m
->x
.p
->arr
[1].x
.n
, m
->x
.p
->arr
[1].d
));
387 value_set_si(m
->x
.p
->arr
[1].x
.n
, 1);
388 eadd(&m
->x
.p
->arr
[1], &m
->x
.p
->arr
[0]);
389 value_set_si(m
->x
.p
->arr
[1].x
.n
, 0);
390 value_set_si(m
->x
.p
->arr
[1].d
, 1);
393 /* Oops. Nested identical relations. */
394 if (!EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
397 if (s
->n
>= s
->max
) {
398 int d
= relations_depth(r
);
399 realloc_substitution(s
, d
);
403 assert(value_zero_p(p
->d
) && p
->x
.p
->type
== polynomial
);
404 assert(p
->x
.p
->size
== 2);
407 assert(value_pos_p(f
->x
.n
));
409 value_init(s
->fixed
[s
->n
].m
);
410 value_assign(s
->fixed
[s
->n
].m
, f
->d
);
411 s
->fixed
[s
->n
].pos
= p
->x
.p
->pos
;
412 value_init(s
->fixed
[s
->n
].d
);
413 value_assign(s
->fixed
[s
->n
].d
, f
->x
.n
);
414 value_init(s
->fixed
[s
->n
].s
.d
);
415 evalue_copy(&s
->fixed
[s
->n
].s
, &p
->x
.p
->arr
[0]);
421 static int type_offset(enode
*p
)
423 return p
->type
== fractional
? 1 :
424 p
->type
== flooring
? 1 :
425 p
->type
== relation
? 1 : 0;
428 static void reorder_terms_about(enode
*p
, evalue
*v
)
431 int offset
= type_offset(p
);
433 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
435 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
436 free_evalue_refs(&(p
->arr
[i
]));
442 void evalue_reorder_terms(evalue
*e
)
448 assert(value_zero_p(e
->d
));
450 assert(p
->type
== fractional
||
451 p
->type
== flooring
||
452 p
->type
== polynomial
); /* for now */
454 offset
= type_offset(p
);
456 value_set_si(f
.d
, 0);
457 f
.x
.p
= new_enode(p
->type
, offset
+2, p
->pos
);
459 value_clear(f
.x
.p
->arr
[0].d
);
460 f
.x
.p
->arr
[0] = p
->arr
[0];
462 evalue_set_si(&f
.x
.p
->arr
[offset
], 0, 1);
463 evalue_set_si(&f
.x
.p
->arr
[offset
+1], 1, 1);
464 reorder_terms_about(p
, &f
);
470 static void evalue_reduce_size(evalue
*e
)
474 assert(value_zero_p(e
->d
));
477 offset
= type_offset(p
);
479 /* Try to reduce the degree */
480 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
481 if (!EVALUE_IS_ZERO(p
->arr
[i
]))
483 free_evalue_refs(&p
->arr
[i
]);
488 /* Try to reduce its strength */
489 if (p
->type
== relation
) {
491 free_evalue_refs(&p
->arr
[0]);
492 evalue_set_si(e
, 0, 1);
495 } else if (p
->size
== offset
+1) {
497 memcpy(e
, &p
->arr
[offset
], sizeof(evalue
));
499 free_evalue_refs(&p
->arr
[0]);
504 void _reduce_evalue (evalue
*e
, struct subst
*s
, int fract
) {
510 if (value_notzero_p(e
->d
)) {
512 mpz_fdiv_r(e
->x
.n
, e
->x
.n
, e
->d
);
513 return; /* a rational number, its already reduced */
517 return; /* hum... an overflow probably occured */
519 /* First reduce the components of p */
520 add
= p
->type
== relation
;
521 for (i
=0; i
<p
->size
; i
++) {
523 add
= add_modulo_substitution(s
, e
);
525 if (i
== 0 && p
->type
==fractional
)
526 _reduce_evalue(&p
->arr
[i
], s
, 1);
528 _reduce_evalue(&p
->arr
[i
], s
, fract
);
530 if (add
&& i
== p
->size
-1) {
532 value_clear(s
->fixed
[s
->n
].m
);
533 value_clear(s
->fixed
[s
->n
].d
);
534 free_evalue_refs(&s
->fixed
[s
->n
].s
);
535 } else if (add
&& i
== 1)
536 s
->fixed
[s
->n
-1].pos
*= -1;
539 if (p
->type
==periodic
) {
541 /* Try to reduce the period */
542 for (i
=1; i
<=(p
->size
)/2; i
++) {
543 if ((p
->size
% i
)==0) {
545 /* Can we reduce the size to i ? */
547 for (k
=j
+i
; k
<e
->x
.p
->size
; k
+=i
)
548 if (!eequal(&p
->arr
[j
], &p
->arr
[k
])) goto you_lose
;
551 for (j
=i
; j
<p
->size
; j
++) free_evalue_refs(&p
->arr
[j
]);
555 you_lose
: /* OK, lets not do it */
560 /* Try to reduce its strength */
563 memcpy(e
,&p
->arr
[0],sizeof(evalue
));
567 else if (p
->type
==polynomial
) {
568 for (k
= 0; s
&& k
< s
->n
; ++k
) {
569 if (s
->fixed
[k
].pos
== p
->pos
) {
570 int divide
= value_notone_p(s
->fixed
[k
].d
);
573 if (value_notzero_p(s
->fixed
[k
].m
)) {
576 assert(p
->size
== 2);
577 if (divide
&& value_ne(s
->fixed
[k
].d
, p
->arr
[1].x
.n
))
579 if (!mpz_divisible_p(s
->fixed
[k
].m
, p
->arr
[1].d
))
586 value_assign(d
.d
, s
->fixed
[k
].d
);
588 if (value_notzero_p(s
->fixed
[k
].m
))
589 value_oppose(d
.x
.n
, s
->fixed
[k
].m
);
591 value_set_si(d
.x
.n
, 1);
594 for (i
=p
->size
-1;i
>=1;i
--) {
595 emul(&s
->fixed
[k
].s
, &p
->arr
[i
]);
597 emul(&d
, &p
->arr
[i
]);
598 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
599 free_evalue_refs(&(p
->arr
[i
]));
602 _reduce_evalue(&p
->arr
[0], s
, fract
);
605 free_evalue_refs(&d
);
611 evalue_reduce_size(e
);
613 else if (p
->type
==fractional
) {
617 if (value_notzero_p(p
->arr
[0].d
)) {
619 value_assign(v
.d
, p
->arr
[0].d
);
621 mpz_fdiv_r(v
.x
.n
, p
->arr
[0].x
.n
, p
->arr
[0].d
);
626 evalue
*pp
= &p
->arr
[0];
627 assert(value_zero_p(pp
->d
) && pp
->x
.p
->type
== polynomial
);
628 assert(pp
->x
.p
->size
== 2);
630 /* search for exact duplicate among the modulo inequalities */
632 f
= &pp
->x
.p
->arr
[1];
633 for (k
= 0; s
&& k
< s
->n
; ++k
) {
634 if (-s
->fixed
[k
].pos
== pp
->x
.p
->pos
&&
635 value_eq(s
->fixed
[k
].d
, f
->x
.n
) &&
636 value_eq(s
->fixed
[k
].m
, f
->d
) &&
637 eequal(&s
->fixed
[k
].s
, &pp
->x
.p
->arr
[0]))
644 /* replace { E/m } by { (E-1)/m } + 1/m */
649 evalue_set_si(&extra
, 1, 1);
650 value_assign(extra
.d
, g
);
651 eadd(&extra
, &v
.x
.p
->arr
[1]);
652 free_evalue_refs(&extra
);
654 /* We've been going in circles; stop now */
655 if (value_ge(v
.x
.p
->arr
[1].x
.n
, v
.x
.p
->arr
[1].d
)) {
656 free_evalue_refs(&v
);
658 evalue_set_si(&v
, 0, 1);
663 value_set_si(v
.d
, 0);
664 v
.x
.p
= new_enode(fractional
, 3, -1);
665 evalue_set_si(&v
.x
.p
->arr
[1], 1, 1);
666 value_assign(v
.x
.p
->arr
[1].d
, g
);
667 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
668 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
671 for (f
= &v
.x
.p
->arr
[0]; value_zero_p(f
->d
);
674 value_division(f
->d
, g
, f
->d
);
675 value_multiply(f
->x
.n
, f
->x
.n
, f
->d
);
676 value_assign(f
->d
, g
);
677 value_decrement(f
->x
.n
, f
->x
.n
);
678 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
680 value_gcd(g
, f
->d
, f
->x
.n
);
681 value_division(f
->d
, f
->d
, g
);
682 value_division(f
->x
.n
, f
->x
.n
, g
);
691 /* reduction may have made this fractional arg smaller */
692 i
= reorder
? p
->size
: 1;
693 for ( ; i
< p
->size
; ++i
)
694 if (value_zero_p(p
->arr
[i
].d
) &&
695 p
->arr
[i
].x
.p
->type
== fractional
&&
696 mod_term_cmp(e
, &p
->arr
[i
]) >= 0)
700 value_set_si(v
.d
, 0);
701 v
.x
.p
= new_enode(fractional
, 3, -1);
702 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
703 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
704 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
712 evalue
*pp
= &p
->arr
[0];
715 poly_denom_not_constant(&pp
, &m
);
716 mpz_fdiv_r(r
, m
, pp
->d
);
717 if (value_notzero_p(r
)) {
719 value_set_si(v
.d
, 0);
720 v
.x
.p
= new_enode(fractional
, 3, -1);
722 value_multiply(r
, m
, pp
->x
.n
);
723 value_multiply(v
.x
.p
->arr
[1].d
, m
, pp
->d
);
724 value_init(v
.x
.p
->arr
[1].x
.n
);
725 mpz_fdiv_r(v
.x
.p
->arr
[1].x
.n
, r
, pp
->d
);
726 mpz_fdiv_q(r
, r
, pp
->d
);
728 evalue_set_si(&v
.x
.p
->arr
[2], 1, 1);
729 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
731 while (value_zero_p(pp
->d
))
732 pp
= &pp
->x
.p
->arr
[0];
734 value_assign(pp
->d
, m
);
735 value_assign(pp
->x
.n
, r
);
737 value_gcd(r
, pp
->d
, pp
->x
.n
);
738 value_division(pp
->d
, pp
->d
, r
);
739 value_division(pp
->x
.n
, pp
->x
.n
, r
);
752 for (pp
= &p
->arr
[0]; value_zero_p(pp
->d
);
753 pp
= &pp
->x
.p
->arr
[0]) {
754 f
= &pp
->x
.p
->arr
[1];
755 assert(value_pos_p(f
->d
));
756 mpz_mul_ui(twice
, f
->x
.n
, 2);
757 if (value_lt(twice
, f
->d
))
759 if (value_eq(twice
, f
->d
))
767 value_set_si(v
.d
, 0);
768 v
.x
.p
= new_enode(fractional
, 3, -1);
769 evalue_set_si(&v
.x
.p
->arr
[1], 0, 1);
770 poly_denom(&p
->arr
[0], &twice
);
771 value_assign(v
.x
.p
->arr
[1].d
, twice
);
772 value_decrement(v
.x
.p
->arr
[1].x
.n
, twice
);
773 evalue_set_si(&v
.x
.p
->arr
[2], -1, 1);
774 evalue_copy(&v
.x
.p
->arr
[0], &p
->arr
[0]);
776 for (pp
= &v
.x
.p
->arr
[0]; value_zero_p(pp
->d
);
777 pp
= &pp
->x
.p
->arr
[0]) {
778 f
= &pp
->x
.p
->arr
[1];
779 value_oppose(f
->x
.n
, f
->x
.n
);
780 mpz_fdiv_r(f
->x
.n
, f
->x
.n
, f
->d
);
782 value_division(pp
->d
, twice
, pp
->d
);
783 value_multiply(pp
->x
.n
, pp
->x
.n
, pp
->d
);
784 value_assign(pp
->d
, twice
);
785 value_oppose(pp
->x
.n
, pp
->x
.n
);
786 value_decrement(pp
->x
.n
, pp
->x
.n
);
787 mpz_fdiv_r(pp
->x
.n
, pp
->x
.n
, pp
->d
);
789 /* Maybe we should do this during reduction of
792 value_gcd(twice
, pp
->d
, pp
->x
.n
);
793 value_division(pp
->d
, pp
->d
, twice
);
794 value_division(pp
->x
.n
, pp
->x
.n
, twice
);
804 reorder_terms_about(p
, &v
);
805 _reduce_evalue(&p
->arr
[1], s
, fract
);
808 evalue_reduce_size(e
);
810 else if (p
->type
== flooring
) {
811 /* Replace floor(constant) by its value */
812 if (value_notzero_p(p
->arr
[0].d
)) {
815 value_set_si(v
.d
, 1);
817 mpz_fdiv_q(v
.x
.n
, p
->arr
[0].x
.n
, p
->arr
[0].d
);
818 reorder_terms_about(p
, &v
);
819 _reduce_evalue(&p
->arr
[1], s
, fract
);
821 evalue_reduce_size(e
);
823 else if (p
->type
== relation
) {
824 if (p
->size
== 3 && eequal(&p
->arr
[1], &p
->arr
[2])) {
825 free_evalue_refs(&(p
->arr
[2]));
826 free_evalue_refs(&(p
->arr
[0]));
833 evalue_reduce_size(e
);
834 if (value_notzero_p(e
->d
) || p
!= e
->x
.p
)
841 /* Relation was reduced by means of an identical
842 * inequality => remove
844 if (value_zero_p(m
->d
) && !EVALUE_IS_ZERO(m
->x
.p
->arr
[1]))
847 if (reduced
|| value_notzero_p(p
->arr
[0].d
)) {
848 if (!reduced
&& value_zero_p(p
->arr
[0].x
.n
)) {
850 memcpy(e
,&p
->arr
[1],sizeof(evalue
));
852 free_evalue_refs(&(p
->arr
[2]));
856 memcpy(e
,&p
->arr
[2],sizeof(evalue
));
858 evalue_set_si(e
, 0, 1);
859 free_evalue_refs(&(p
->arr
[1]));
861 free_evalue_refs(&(p
->arr
[0]));
867 } /* reduce_evalue */
869 static void add_substitution(struct subst
*s
, Value
*row
, unsigned dim
)
874 for (k
= 0; k
< dim
; ++k
)
875 if (value_notzero_p(row
[k
+1]))
878 Vector_Normalize_Positive(row
+1, dim
+1, k
);
879 assert(s
->n
< s
->max
);
880 value_init(s
->fixed
[s
->n
].d
);
881 value_init(s
->fixed
[s
->n
].m
);
882 value_assign(s
->fixed
[s
->n
].d
, row
[k
+1]);
883 s
->fixed
[s
->n
].pos
= k
+1;
884 value_set_si(s
->fixed
[s
->n
].m
, 0);
885 r
= &s
->fixed
[s
->n
].s
;
887 for (l
= k
+1; l
< dim
; ++l
)
888 if (value_notzero_p(row
[l
+1])) {
889 value_set_si(r
->d
, 0);
890 r
->x
.p
= new_enode(polynomial
, 2, l
+ 1);
891 value_init(r
->x
.p
->arr
[1].x
.n
);
892 value_oppose(r
->x
.p
->arr
[1].x
.n
, row
[l
+1]);
893 value_set_si(r
->x
.p
->arr
[1].d
, 1);
897 value_oppose(r
->x
.n
, row
[dim
+1]);
898 value_set_si(r
->d
, 1);
902 static void _reduce_evalue_in_domain(evalue
*e
, Polyhedron
*D
, struct subst
*s
)
905 Polyhedron
*orig
= D
;
910 D
= DomainConvex(D
, 0);
911 /* We don't perform any substitutions if the domain is a union.
912 * We may therefore miss out on some possible simplifications,
913 * e.g., if a variable is always even in the whole union,
914 * while there is a relation in the evalue that evaluates
915 * to zero for even values of the variable.
917 if (!D
->next
&& D
->NbEq
) {
921 realloc_substitution(s
, dim
);
923 int d
= relations_depth(e
);
925 NALLOC(s
->fixed
, s
->max
);
928 for (j
= 0; j
< D
->NbEq
; ++j
)
929 add_substitution(s
, D
->Constraint
[j
], dim
);
933 _reduce_evalue(e
, s
, 0);
936 for (j
= 0; j
< s
->n
; ++j
) {
937 value_clear(s
->fixed
[j
].d
);
938 value_clear(s
->fixed
[j
].m
);
939 free_evalue_refs(&s
->fixed
[j
].s
);
944 void reduce_evalue_in_domain(evalue
*e
, Polyhedron
*D
)
946 struct subst s
= { NULL
, 0, 0 };
947 POL_ENSURE_VERTICES(D
);
949 if (EVALUE_IS_ZERO(*e
))
953 evalue_set_si(e
, 0, 1);
956 _reduce_evalue_in_domain(e
, D
, &s
);
961 void reduce_evalue (evalue
*e
) {
962 struct subst s
= { NULL
, 0, 0 };
964 if (value_notzero_p(e
->d
))
965 return; /* a rational number, its already reduced */
967 if (e
->x
.p
->type
== partition
) {
969 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
970 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
972 /* This shouldn't really happen;
973 * Empty domains should not be added.
975 POL_ENSURE_VERTICES(D
);
977 _reduce_evalue_in_domain(&e
->x
.p
->arr
[2*i
+1], D
, &s
);
979 if (emptyQ(D
) || EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
980 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
981 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
982 value_clear(e
->x
.p
->arr
[2*i
].d
);
984 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
985 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
989 if (e
->x
.p
->size
== 0) {
991 evalue_set_si(e
, 0, 1);
994 _reduce_evalue(e
, &s
, 0);
999 static void print_evalue_r(FILE *DST
, const evalue
*e
, const char **pname
)
1001 if (EVALUE_IS_NAN(*e
)) {
1002 fprintf(DST
, "NaN");
1006 if(value_notzero_p(e
->d
)) {
1007 if(value_notone_p(e
->d
)) {
1008 value_print(DST
,VALUE_FMT
,e
->x
.n
);
1010 value_print(DST
,VALUE_FMT
,e
->d
);
1013 value_print(DST
,VALUE_FMT
,e
->x
.n
);
1017 print_enode(DST
,e
->x
.p
,pname
);
1019 } /* print_evalue */
1021 void print_evalue(FILE *DST
, const evalue
*e
, const char **pname
)
1023 print_evalue_r(DST
, e
, pname
);
1024 if (value_notzero_p(e
->d
))
1028 void print_enode(FILE *DST
, enode
*p
, const char **pname
)
1033 fprintf(DST
, "NULL");
1039 for (i
=0; i
<p
->size
; i
++) {
1040 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1044 fprintf(DST
, " }\n");
1048 for (i
=p
->size
-1; i
>=0; i
--) {
1049 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1050 if (i
==1) fprintf(DST
, " * %s + ", pname
[p
->pos
-1]);
1052 fprintf(DST
, " * %s^%d + ", pname
[p
->pos
-1], i
);
1054 fprintf(DST
, " )\n");
1058 for (i
=0; i
<p
->size
; i
++) {
1059 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1060 if (i
!=(p
->size
-1)) fprintf(DST
, ", ");
1062 fprintf(DST
," ]_%s", pname
[p
->pos
-1]);
1067 for (i
=p
->size
-1; i
>=1; i
--) {
1068 print_evalue_r(DST
, &p
->arr
[i
], pname
);
1070 fprintf(DST
, " * ");
1071 fprintf(DST
, p
->type
== flooring
? "[" : "{");
1072 print_evalue_r(DST
, &p
->arr
[0], pname
);
1073 fprintf(DST
, p
->type
== flooring
? "]" : "}");
1075 fprintf(DST
, "^%d + ", i
-1);
1077 fprintf(DST
, " + ");
1080 fprintf(DST
, " )\n");
1084 print_evalue_r(DST
, &p
->arr
[0], pname
);
1085 fprintf(DST
, "= 0 ] * \n");
1086 print_evalue_r(DST
, &p
->arr
[1], pname
);
1088 fprintf(DST
, " +\n [ ");
1089 print_evalue_r(DST
, &p
->arr
[0], pname
);
1090 fprintf(DST
, "!= 0 ] * \n");
1091 print_evalue_r(DST
, &p
->arr
[2], pname
);
1095 char **new_names
= NULL
;
1096 const char **names
= pname
;
1097 int maxdim
= EVALUE_DOMAIN(p
->arr
[0])->Dimension
;
1098 if (!pname
|| p
->pos
< maxdim
) {
1099 new_names
= ALLOCN(char *, maxdim
);
1100 for (i
= 0; i
< p
->pos
; ++i
) {
1102 new_names
[i
] = (char *)pname
[i
];
1104 new_names
[i
] = ALLOCN(char, 10);
1105 snprintf(new_names
[i
], 10, "%c", 'P'+i
);
1108 for ( ; i
< maxdim
; ++i
) {
1109 new_names
[i
] = ALLOCN(char, 10);
1110 snprintf(new_names
[i
], 10, "_p%d", i
);
1112 names
= (const char**)new_names
;
1115 for (i
=0; i
<p
->size
/2; i
++) {
1116 Print_Domain(DST
, EVALUE_DOMAIN(p
->arr
[2*i
]), names
);
1117 print_evalue_r(DST
, &p
->arr
[2*i
+1], names
);
1118 if (value_notzero_p(p
->arr
[2*i
+1].d
))
1122 if (!pname
|| p
->pos
< maxdim
) {
1123 for (i
= pname
? p
->pos
: 0; i
< maxdim
; ++i
)
1137 * 0 if toplevels of e1 and e2 are at the same level
1138 * <0 if toplevel of e1 should be outside of toplevel of e2
1139 * >0 if toplevel of e2 should be outside of toplevel of e1
1141 static int evalue_level_cmp(const evalue
*e1
, const evalue
*e2
)
1143 if (value_notzero_p(e1
->d
) && value_notzero_p(e2
->d
))
1145 if (value_notzero_p(e1
->d
))
1147 if (value_notzero_p(e2
->d
))
1149 if (e1
->x
.p
->type
== partition
&& e2
->x
.p
->type
== partition
)
1151 if (e1
->x
.p
->type
== partition
)
1153 if (e2
->x
.p
->type
== partition
)
1155 if (e1
->x
.p
->type
== relation
&& e2
->x
.p
->type
== relation
) {
1156 if (eequal(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]))
1158 return mod_term_cmp(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]);
1160 if (e1
->x
.p
->type
== relation
)
1162 if (e2
->x
.p
->type
== relation
)
1164 if (e1
->x
.p
->type
== polynomial
&& e2
->x
.p
->type
== polynomial
)
1165 return e1
->x
.p
->pos
- e2
->x
.p
->pos
;
1166 if (e1
->x
.p
->type
== polynomial
)
1168 if (e2
->x
.p
->type
== polynomial
)
1170 if (e1
->x
.p
->type
== periodic
&& e2
->x
.p
->type
== periodic
)
1171 return e1
->x
.p
->pos
- e2
->x
.p
->pos
;
1172 assert(e1
->x
.p
->type
!= periodic
);
1173 assert(e2
->x
.p
->type
!= periodic
);
1174 assert(e1
->x
.p
->type
== e2
->x
.p
->type
);
1175 if (eequal(&e1
->x
.p
->arr
[0], &e2
->x
.p
->arr
[0]))
1177 return mod_term_cmp(e1
, e2
);
1180 static void eadd_rev(const evalue
*e1
, evalue
*res
)
1184 evalue_copy(&ev
, e1
);
1186 free_evalue_refs(res
);
1190 static void eadd_rev_cst(const evalue
*e1
, evalue
*res
)
1194 evalue_copy(&ev
, e1
);
1195 eadd(res
, &ev
.x
.p
->arr
[type_offset(ev
.x
.p
)]);
1196 free_evalue_refs(res
);
1200 struct section
{ Polyhedron
* D
; evalue E
; };
1202 void eadd_partitions(const evalue
*e1
, evalue
*res
)
1207 s
= (struct section
*)
1208 malloc((e1
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2+1) *
1209 sizeof(struct section
));
1211 assert(e1
->x
.p
->pos
== res
->x
.p
->pos
);
1212 assert(e1
->x
.p
->pos
== EVALUE_DOMAIN(e1
->x
.p
->arr
[0])->Dimension
);
1213 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1216 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1217 assert(res
->x
.p
->size
>= 2);
1218 fd
= DomainDifference(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1219 EVALUE_DOMAIN(res
->x
.p
->arr
[0]), 0);
1221 for (i
= 1; i
< res
->x
.p
->size
/2; ++i
) {
1223 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1228 fd
= DomainConstraintSimplify(fd
, 0);
1233 value_init(s
[n
].E
.d
);
1234 evalue_copy(&s
[n
].E
, &e1
->x
.p
->arr
[2*j
+1]);
1238 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
1239 fd
= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]);
1240 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1242 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1243 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1244 d
= DomainConstraintSimplify(d
, 0);
1250 fd
= DomainDifference(fd
, EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]), 0);
1251 if (t
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
1253 value_init(s
[n
].E
.d
);
1254 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
1255 eadd(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
1260 s
[n
].E
= res
->x
.p
->arr
[2*i
+1];
1264 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
1267 if (fd
!= EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]))
1268 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
1269 value_clear(res
->x
.p
->arr
[2*i
].d
);
1274 res
->x
.p
= new_enode(partition
, 2*n
, e1
->x
.p
->pos
);
1275 for (j
= 0; j
< n
; ++j
) {
1276 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1277 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1278 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1284 static void explicit_complement(evalue
*res
)
1286 enode
*rel
= new_enode(relation
, 3, 0);
1288 value_clear(rel
->arr
[0].d
);
1289 rel
->arr
[0] = res
->x
.p
->arr
[0];
1290 value_clear(rel
->arr
[1].d
);
1291 rel
->arr
[1] = res
->x
.p
->arr
[1];
1292 value_set_si(rel
->arr
[2].d
, 1);
1293 value_init(rel
->arr
[2].x
.n
);
1294 value_set_si(rel
->arr
[2].x
.n
, 0);
1299 static void reduce_constant(evalue
*e
)
1304 value_gcd(g
, e
->x
.n
, e
->d
);
1305 if (value_notone_p(g
)) {
1306 value_division(e
->d
, e
->d
,g
);
1307 value_division(e
->x
.n
, e
->x
.n
,g
);
1312 /* Add two rational numbers */
1313 static void eadd_rationals(const evalue
*e1
, evalue
*res
)
1315 if (value_eq(e1
->d
, res
->d
))
1316 value_addto(res
->x
.n
, res
->x
.n
, e1
->x
.n
);
1318 value_multiply(res
->x
.n
, res
->x
.n
, e1
->d
);
1319 value_addmul(res
->x
.n
, e1
->x
.n
, res
->d
);
1320 value_multiply(res
->d
,e1
->d
,res
->d
);
1322 reduce_constant(res
);
1325 static void eadd_relations(const evalue
*e1
, evalue
*res
)
1329 if (res
->x
.p
->size
< 3 && e1
->x
.p
->size
== 3)
1330 explicit_complement(res
);
1331 for (i
= 1; i
< e1
->x
.p
->size
; ++i
)
1332 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1335 static void eadd_arrays(const evalue
*e1
, evalue
*res
, int n
)
1339 // add any element in e1 to the corresponding element in res
1340 i
= type_offset(res
->x
.p
);
1342 assert(eequal(&e1
->x
.p
->arr
[0], &res
->x
.p
->arr
[0]));
1344 eadd(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1347 static void eadd_poly(const evalue
*e1
, evalue
*res
)
1349 if (e1
->x
.p
->size
> res
->x
.p
->size
)
1352 eadd_arrays(e1
, res
, e1
->x
.p
->size
);
1356 * Product or sum of two periodics of the same parameter
1357 * and different periods
1359 static void combine_periodics(const evalue
*e1
, evalue
*res
,
1360 void (*op
)(const evalue
*, evalue
*))
1368 value_set_si(es
, e1
->x
.p
->size
);
1369 value_set_si(rs
, res
->x
.p
->size
);
1370 value_lcm(rs
, es
, rs
);
1371 size
= (int)mpz_get_si(rs
);
1374 p
= new_enode(periodic
, size
, e1
->x
.p
->pos
);
1375 for (i
= 0; i
< res
->x
.p
->size
; i
++) {
1376 value_clear(p
->arr
[i
].d
);
1377 p
->arr
[i
] = res
->x
.p
->arr
[i
];
1379 for (i
= res
->x
.p
->size
; i
< size
; i
++)
1380 evalue_copy(&p
->arr
[i
], &res
->x
.p
->arr
[i
% res
->x
.p
->size
]);
1381 for (i
= 0; i
< size
; i
++)
1382 op(&e1
->x
.p
->arr
[i
% e1
->x
.p
->size
], &p
->arr
[i
]);
1387 static void eadd_periodics(const evalue
*e1
, evalue
*res
)
1393 if (e1
->x
.p
->size
== res
->x
.p
->size
) {
1394 eadd_arrays(e1
, res
, e1
->x
.p
->size
);
1398 combine_periodics(e1
, res
, eadd
);
1401 void evalue_assign(evalue
*dst
, const evalue
*src
)
1403 if (value_pos_p(dst
->d
) && value_pos_p(src
->d
)) {
1404 value_assign(dst
->d
, src
->d
);
1405 value_assign(dst
->x
.n
, src
->x
.n
);
1408 free_evalue_refs(dst
);
1410 evalue_copy(dst
, src
);
1413 void eadd(const evalue
*e1
, evalue
*res
)
1417 if (EVALUE_IS_ZERO(*e1
))
1420 if (EVALUE_IS_NAN(*res
))
1423 if (EVALUE_IS_NAN(*e1
)) {
1424 evalue_assign(res
, e1
);
1428 if (EVALUE_IS_ZERO(*res
)) {
1429 evalue_assign(res
, e1
);
1433 cmp
= evalue_level_cmp(res
, e1
);
1435 switch (e1
->x
.p
->type
) {
1439 eadd_rev_cst(e1
, res
);
1444 } else if (cmp
== 0) {
1445 if (value_notzero_p(e1
->d
)) {
1446 eadd_rationals(e1
, res
);
1448 switch (e1
->x
.p
->type
) {
1450 eadd_partitions(e1
, res
);
1453 eadd_relations(e1
, res
);
1456 assert(e1
->x
.p
->size
== res
->x
.p
->size
);
1463 eadd_periodics(e1
, res
);
1471 switch (res
->x
.p
->type
) {
1475 /* Add to the constant term of a polynomial */
1476 eadd(e1
, &res
->x
.p
->arr
[type_offset(res
->x
.p
)]);
1479 /* Add to all elements of a periodic number */
1480 for (i
= 0; i
< res
->x
.p
->size
; i
++)
1481 eadd(e1
, &res
->x
.p
->arr
[i
]);
1484 fprintf(stderr
, "eadd: cannot add const with vector\n");
1489 /* Create (zero) complement if needed */
1490 if (res
->x
.p
->size
< 3)
1491 explicit_complement(res
);
1492 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1493 eadd(e1
, &res
->x
.p
->arr
[i
]);
1501 static void emul_rev(const evalue
*e1
, evalue
*res
)
1505 evalue_copy(&ev
, e1
);
1507 free_evalue_refs(res
);
1511 static void emul_poly(const evalue
*e1
, evalue
*res
)
1513 int i
, j
, offset
= type_offset(res
->x
.p
);
1516 int size
= (e1
->x
.p
->size
+ res
->x
.p
->size
- offset
- 1);
1518 p
= new_enode(res
->x
.p
->type
, size
, res
->x
.p
->pos
);
1520 for (i
= offset
; i
< e1
->x
.p
->size
-1; ++i
)
1521 if (!EVALUE_IS_ZERO(e1
->x
.p
->arr
[i
]))
1524 /* special case pure power */
1525 if (i
== e1
->x
.p
->size
-1) {
1527 value_clear(p
->arr
[0].d
);
1528 p
->arr
[0] = res
->x
.p
->arr
[0];
1530 for (i
= offset
; i
< e1
->x
.p
->size
-1; ++i
)
1531 evalue_set_si(&p
->arr
[i
], 0, 1);
1532 for (i
= offset
; i
< res
->x
.p
->size
; ++i
) {
1533 value_clear(p
->arr
[i
+e1
->x
.p
->size
-offset
-1].d
);
1534 p
->arr
[i
+e1
->x
.p
->size
-offset
-1] = res
->x
.p
->arr
[i
];
1535 emul(&e1
->x
.p
->arr
[e1
->x
.p
->size
-1],
1536 &p
->arr
[i
+e1
->x
.p
->size
-offset
-1]);
1544 value_set_si(tmp
.d
,0);
1547 evalue_copy(&p
->arr
[0], &e1
->x
.p
->arr
[0]);
1548 for (i
= offset
; i
< e1
->x
.p
->size
; i
++) {
1549 evalue_copy(&tmp
.x
.p
->arr
[i
], &e1
->x
.p
->arr
[i
]);
1550 emul(&res
->x
.p
->arr
[offset
], &tmp
.x
.p
->arr
[i
]);
1553 evalue_set_si(&tmp
.x
.p
->arr
[i
], 0, 1);
1554 for (i
= offset
+1; i
<res
->x
.p
->size
; i
++)
1555 for (j
= offset
; j
<e1
->x
.p
->size
; j
++) {
1558 evalue_copy(&ev
, &e1
->x
.p
->arr
[j
]);
1559 emul(&res
->x
.p
->arr
[i
], &ev
);
1560 eadd(&ev
, &tmp
.x
.p
->arr
[i
+j
-offset
]);
1561 free_evalue_refs(&ev
);
1563 free_evalue_refs(res
);
1567 void emul_partitions(const evalue
*e1
, evalue
*res
)
1572 s
= (struct section
*)
1573 malloc((e1
->x
.p
->size
/2) * (res
->x
.p
->size
/2) *
1574 sizeof(struct section
));
1576 assert(e1
->x
.p
->pos
== res
->x
.p
->pos
);
1577 assert(e1
->x
.p
->pos
== EVALUE_DOMAIN(e1
->x
.p
->arr
[0])->Dimension
);
1578 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1581 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
) {
1582 for (j
= 0; j
< e1
->x
.p
->size
/2; ++j
) {
1583 d
= DomainIntersection(EVALUE_DOMAIN(e1
->x
.p
->arr
[2*j
]),
1584 EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]), 0);
1585 d
= DomainConstraintSimplify(d
, 0);
1591 /* This code is only needed because the partitions
1592 are not true partitions.
1594 for (k
= 0; k
< n
; ++k
) {
1595 if (DomainIncludes(s
[k
].D
, d
))
1597 if (DomainIncludes(d
, s
[k
].D
)) {
1598 Domain_Free(s
[k
].D
);
1599 free_evalue_refs(&s
[k
].E
);
1610 value_init(s
[n
].E
.d
);
1611 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*i
+1]);
1612 emul(&e1
->x
.p
->arr
[2*j
+1], &s
[n
].E
);
1616 Domain_Free(EVALUE_DOMAIN(res
->x
.p
->arr
[2*i
]));
1617 value_clear(res
->x
.p
->arr
[2*i
].d
);
1618 free_evalue_refs(&res
->x
.p
->arr
[2*i
+1]);
1623 evalue_set_si(res
, 0, 1);
1625 res
->x
.p
= new_enode(partition
, 2*n
, e1
->x
.p
->pos
);
1626 for (j
= 0; j
< n
; ++j
) {
1627 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1628 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1629 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1636 /* Product of two rational numbers */
1637 static void emul_rationals(const evalue
*e1
, evalue
*res
)
1639 value_multiply(res
->d
, e1
->d
, res
->d
);
1640 value_multiply(res
->x
.n
, e1
->x
.n
, res
->x
.n
);
1641 reduce_constant(res
);
1644 static void emul_relations(const evalue
*e1
, evalue
*res
)
1648 if (e1
->x
.p
->size
< 3 && res
->x
.p
->size
== 3) {
1649 free_evalue_refs(&res
->x
.p
->arr
[2]);
1652 for (i
= 1; i
< res
->x
.p
->size
; ++i
)
1653 emul(&e1
->x
.p
->arr
[i
], &res
->x
.p
->arr
[i
]);
1656 static void emul_periodics(const evalue
*e1
, evalue
*res
)
1663 if (e1
->x
.p
->size
== res
->x
.p
->size
) {
1664 /* Product of two periodics of the same parameter and period */
1665 for (i
= 0; i
< res
->x
.p
->size
; i
++)
1666 emul(&(e1
->x
.p
->arr
[i
]), &(res
->x
.p
->arr
[i
]));
1670 combine_periodics(e1
, res
, emul
);
1673 #define value_two_p(val) (mpz_cmp_si(val,2) == 0)
1675 static void emul_fractionals(const evalue
*e1
, evalue
*res
)
1679 poly_denom(&e1
->x
.p
->arr
[0], &d
.d
);
1680 if (!value_two_p(d
.d
))
1685 value_set_si(d
.x
.n
, 1);
1686 /* { x }^2 == { x }/2 */
1687 /* a0 b0 + (a0 b1 + a1 b0 + a1 b1/2) { x } */
1688 assert(e1
->x
.p
->size
== 3);
1689 assert(res
->x
.p
->size
== 3);
1691 evalue_copy(&tmp
, &res
->x
.p
->arr
[2]);
1693 eadd(&res
->x
.p
->arr
[1], &tmp
);
1694 emul(&e1
->x
.p
->arr
[2], &tmp
);
1695 emul(&e1
->x
.p
->arr
[1], &res
->x
.p
->arr
[1]);
1696 emul(&e1
->x
.p
->arr
[1], &res
->x
.p
->arr
[2]);
1697 eadd(&tmp
, &res
->x
.p
->arr
[2]);
1698 free_evalue_refs(&tmp
);
1704 /* Computes the product of two evalues "e1" and "res" and puts
1705 * the result in "res". You need to make a copy of "res"
1706 * before calling this function if you still need it afterward.
1707 * The vector type of evalues is not treated here
1709 void emul(const evalue
*e1
, evalue
*res
)
1713 assert(!(value_zero_p(e1
->d
) && e1
->x
.p
->type
== evector
));
1714 assert(!(value_zero_p(res
->d
) && res
->x
.p
->type
== evector
));
1716 if (EVALUE_IS_ZERO(*res
))
1719 if (EVALUE_IS_ONE(*e1
))
1722 if (EVALUE_IS_ZERO(*e1
)) {
1723 evalue_assign(res
, e1
);
1727 if (EVALUE_IS_NAN(*res
))
1730 if (EVALUE_IS_NAN(*e1
)) {
1731 evalue_assign(res
, e1
);
1735 cmp
= evalue_level_cmp(res
, e1
);
1738 } else if (cmp
== 0) {
1739 if (value_notzero_p(e1
->d
)) {
1740 emul_rationals(e1
, res
);
1742 switch (e1
->x
.p
->type
) {
1744 emul_partitions(e1
, res
);
1747 emul_relations(e1
, res
);
1754 emul_periodics(e1
, res
);
1757 emul_fractionals(e1
, res
);
1763 switch (res
->x
.p
->type
) {
1765 for (i
= 0; i
< res
->x
.p
->size
/2; ++i
)
1766 emul(e1
, &res
->x
.p
->arr
[2*i
+1]);
1773 for (i
= type_offset(res
->x
.p
); i
< res
->x
.p
->size
; ++i
)
1774 emul(e1
, &res
->x
.p
->arr
[i
]);
1780 /* Frees mask content ! */
1781 void emask(evalue
*mask
, evalue
*res
) {
1788 if (EVALUE_IS_ZERO(*res
)) {
1789 free_evalue_refs(mask
);
1793 assert(value_zero_p(mask
->d
));
1794 assert(mask
->x
.p
->type
== partition
);
1795 assert(value_zero_p(res
->d
));
1796 assert(res
->x
.p
->type
== partition
);
1797 assert(mask
->x
.p
->pos
== res
->x
.p
->pos
);
1798 assert(res
->x
.p
->pos
== EVALUE_DOMAIN(res
->x
.p
->arr
[0])->Dimension
);
1799 assert(mask
->x
.p
->pos
== EVALUE_DOMAIN(mask
->x
.p
->arr
[0])->Dimension
);
1800 pos
= res
->x
.p
->pos
;
1802 s
= (struct section
*)
1803 malloc((mask
->x
.p
->size
/2+1) * (res
->x
.p
->size
/2) *
1804 sizeof(struct section
));
1808 evalue_set_si(&mone
, -1, 1);
1811 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1812 assert(mask
->x
.p
->size
>= 2);
1813 fd
= DomainDifference(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1814 EVALUE_DOMAIN(mask
->x
.p
->arr
[0]), 0);
1816 for (i
= 1; i
< mask
->x
.p
->size
/2; ++i
) {
1818 fd
= DomainDifference(fd
, EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1827 value_init(s
[n
].E
.d
);
1828 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1832 for (i
= 0; i
< mask
->x
.p
->size
/2; ++i
) {
1833 if (EVALUE_IS_ONE(mask
->x
.p
->arr
[2*i
+1]))
1836 fd
= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]);
1837 eadd(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1838 emul(&mone
, &mask
->x
.p
->arr
[2*i
+1]);
1839 for (j
= 0; j
< res
->x
.p
->size
/2; ++j
) {
1841 d
= DomainIntersection(EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]),
1842 EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]), 0);
1848 fd
= DomainDifference(fd
, EVALUE_DOMAIN(res
->x
.p
->arr
[2*j
]), 0);
1849 if (t
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1851 value_init(s
[n
].E
.d
);
1852 evalue_copy(&s
[n
].E
, &res
->x
.p
->arr
[2*j
+1]);
1853 emul(&mask
->x
.p
->arr
[2*i
+1], &s
[n
].E
);
1859 /* Just ignore; this may have been previously masked off */
1861 if (fd
!= EVALUE_DOMAIN(mask
->x
.p
->arr
[2*i
]))
1865 free_evalue_refs(&mone
);
1866 free_evalue_refs(mask
);
1867 free_evalue_refs(res
);
1870 evalue_set_si(res
, 0, 1);
1872 res
->x
.p
= new_enode(partition
, 2*n
, pos
);
1873 for (j
= 0; j
< n
; ++j
) {
1874 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*j
], s
[j
].D
);
1875 value_clear(res
->x
.p
->arr
[2*j
+1].d
);
1876 res
->x
.p
->arr
[2*j
+1] = s
[j
].E
;
1883 void evalue_copy(evalue
*dst
, const evalue
*src
)
1885 value_assign(dst
->d
, src
->d
);
1886 if (EVALUE_IS_NAN(*dst
)) {
1890 if (value_pos_p(src
->d
)) {
1891 value_init(dst
->x
.n
);
1892 value_assign(dst
->x
.n
, src
->x
.n
);
1894 dst
->x
.p
= ecopy(src
->x
.p
);
1897 evalue
*evalue_dup(const evalue
*e
)
1899 evalue
*res
= ALLOC(evalue
);
1901 evalue_copy(res
, e
);
1905 enode
*new_enode(enode_type type
,int size
,int pos
) {
1911 fprintf(stderr
, "Allocating enode of size 0 !\n" );
1914 res
= (enode
*) malloc(sizeof(enode
) + (size
-1)*sizeof(evalue
));
1918 for(i
=0; i
<size
; i
++) {
1919 value_init(res
->arr
[i
].d
);
1920 value_set_si(res
->arr
[i
].d
,0);
1921 res
->arr
[i
].x
.p
= 0;
1926 enode
*ecopy(enode
*e
) {
1931 res
= new_enode(e
->type
,e
->size
,e
->pos
);
1932 for(i
=0;i
<e
->size
;++i
) {
1933 value_assign(res
->arr
[i
].d
,e
->arr
[i
].d
);
1934 if(value_zero_p(res
->arr
[i
].d
))
1935 res
->arr
[i
].x
.p
= ecopy(e
->arr
[i
].x
.p
);
1936 else if (EVALUE_IS_DOMAIN(res
->arr
[i
]))
1937 EVALUE_SET_DOMAIN(res
->arr
[i
], Domain_Copy(EVALUE_DOMAIN(e
->arr
[i
])));
1939 value_init(res
->arr
[i
].x
.n
);
1940 value_assign(res
->arr
[i
].x
.n
,e
->arr
[i
].x
.n
);
1946 int ecmp(const evalue
*e1
, const evalue
*e2
)
1952 if (value_notzero_p(e1
->d
) && value_notzero_p(e2
->d
)) {
1956 value_multiply(m
, e1
->x
.n
, e2
->d
);
1957 value_multiply(m2
, e2
->x
.n
, e1
->d
);
1959 if (value_lt(m
, m2
))
1961 else if (value_gt(m
, m2
))
1971 if (value_notzero_p(e1
->d
))
1973 if (value_notzero_p(e2
->d
))
1979 if (p1
->type
!= p2
->type
)
1980 return p1
->type
- p2
->type
;
1981 if (p1
->pos
!= p2
->pos
)
1982 return p1
->pos
- p2
->pos
;
1983 if (p1
->size
!= p2
->size
)
1984 return p1
->size
- p2
->size
;
1986 for (i
= p1
->size
-1; i
>= 0; --i
)
1987 if ((r
= ecmp(&p1
->arr
[i
], &p2
->arr
[i
])) != 0)
1993 int eequal(const evalue
*e1
, const evalue
*e2
)
1998 if (value_ne(e1
->d
,e2
->d
))
2001 if (EVALUE_IS_DOMAIN(*e1
))
2002 return PolyhedronIncludes(EVALUE_DOMAIN(*e2
), EVALUE_DOMAIN(*e1
)) &&
2003 PolyhedronIncludes(EVALUE_DOMAIN(*e1
), EVALUE_DOMAIN(*e2
));
2005 if (EVALUE_IS_NAN(*e1
))
2008 assert(value_posz_p(e1
->d
));
2010 /* e1->d == e2->d */
2011 if (value_notzero_p(e1
->d
)) {
2012 if (value_ne(e1
->x
.n
,e2
->x
.n
))
2015 /* e1->d == e2->d != 0 AND e1->n == e2->n */
2019 /* e1->d == e2->d == 0 */
2022 if (p1
->type
!= p2
->type
) return 0;
2023 if (p1
->size
!= p2
->size
) return 0;
2024 if (p1
->pos
!= p2
->pos
) return 0;
2025 for (i
=0; i
<p1
->size
; i
++)
2026 if (!eequal(&p1
->arr
[i
], &p2
->arr
[i
]) )
2031 void free_evalue_refs(evalue
*e
) {
2036 if (EVALUE_IS_NAN(*e
)) {
2041 if (EVALUE_IS_DOMAIN(*e
)) {
2042 Domain_Free(EVALUE_DOMAIN(*e
));
2045 } else if (value_pos_p(e
->d
)) {
2047 /* 'e' stores a constant */
2049 value_clear(e
->x
.n
);
2052 assert(value_zero_p(e
->d
));
2055 if (!p
) return; /* null pointer */
2056 for (i
=0; i
<p
->size
; i
++) {
2057 free_evalue_refs(&(p
->arr
[i
]));
2061 } /* free_evalue_refs */
2063 void evalue_free(evalue
*e
)
2065 free_evalue_refs(e
);
2069 static void mod2table_r(evalue
*e
, Vector
*periods
, Value m
, int p
,
2070 Vector
* val
, evalue
*res
)
2072 unsigned nparam
= periods
->Size
;
2075 double d
= compute_evalue(e
, val
->p
);
2076 d
*= VALUE_TO_DOUBLE(m
);
2081 value_assign(res
->d
, m
);
2082 value_init(res
->x
.n
);
2083 value_set_double(res
->x
.n
, d
);
2084 mpz_fdiv_r(res
->x
.n
, res
->x
.n
, m
);
2087 if (value_one_p(periods
->p
[p
]))
2088 mod2table_r(e
, periods
, m
, p
+1, val
, res
);
2093 value_assign(tmp
, periods
->p
[p
]);
2094 value_set_si(res
->d
, 0);
2095 res
->x
.p
= new_enode(periodic
, VALUE_TO_INT(tmp
), p
+1);
2097 value_decrement(tmp
, tmp
);
2098 value_assign(val
->p
[p
], tmp
);
2099 mod2table_r(e
, periods
, m
, p
+1, val
,
2100 &res
->x
.p
->arr
[VALUE_TO_INT(tmp
)]);
2101 } while (value_pos_p(tmp
));
2107 static void rel2table(evalue
*e
, int zero
)
2109 if (value_pos_p(e
->d
)) {
2110 if (value_zero_p(e
->x
.n
) == zero
)
2111 value_set_si(e
->x
.n
, 1);
2113 value_set_si(e
->x
.n
, 0);
2114 value_set_si(e
->d
, 1);
2117 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
2118 rel2table(&e
->x
.p
->arr
[i
], zero
);
2122 void evalue_mod2table(evalue
*e
, int nparam
)
2127 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
2130 for (i
=0; i
<p
->size
; i
++) {
2131 evalue_mod2table(&(p
->arr
[i
]), nparam
);
2133 if (p
->type
== relation
) {
2138 evalue_copy(©
, &p
->arr
[0]);
2140 rel2table(&p
->arr
[0], 1);
2141 emul(&p
->arr
[0], &p
->arr
[1]);
2143 rel2table(©
, 0);
2144 emul(©
, &p
->arr
[2]);
2145 eadd(&p
->arr
[2], &p
->arr
[1]);
2146 free_evalue_refs(&p
->arr
[2]);
2147 free_evalue_refs(©
);
2149 free_evalue_refs(&p
->arr
[0]);
2153 } else if (p
->type
== fractional
) {
2154 Vector
*periods
= Vector_Alloc(nparam
);
2155 Vector
*val
= Vector_Alloc(nparam
);
2161 value_set_si(tmp
, 1);
2162 Vector_Set(periods
->p
, 1, nparam
);
2163 Vector_Set(val
->p
, 0, nparam
);
2164 for (ev
= &p
->arr
[0]; value_zero_p(ev
->d
); ev
= &ev
->x
.p
->arr
[0]) {
2167 assert(p
->type
== polynomial
);
2168 assert(p
->size
== 2);
2169 value_assign(periods
->p
[p
->pos
-1], p
->arr
[1].d
);
2170 value_lcm(tmp
, tmp
, p
->arr
[1].d
);
2172 value_lcm(tmp
, tmp
, ev
->d
);
2174 mod2table_r(&p
->arr
[0], periods
, tmp
, 0, val
, &EP
);
2177 evalue_set_si(&res
, 0, 1);
2178 /* Compute the polynomial using Horner's rule */
2179 for (i
=p
->size
-1;i
>1;i
--) {
2180 eadd(&p
->arr
[i
], &res
);
2183 eadd(&p
->arr
[1], &res
);
2185 free_evalue_refs(e
);
2186 free_evalue_refs(&EP
);
2191 Vector_Free(periods
);
2193 } /* evalue_mod2table */
2195 /********************************************************/
2196 /* function in domain */
2197 /* check if the parameters in list_args */
2198 /* verifies the constraints of Domain P */
2199 /********************************************************/
2200 int in_domain(Polyhedron
*P
, Value
*list_args
)
2203 Value v
; /* value of the constraint of a row when
2204 parameters are instantiated*/
2206 if (P
->Dimension
== 0)
2211 for (row
= 0; row
< P
->NbConstraints
; row
++) {
2212 Inner_Product(P
->Constraint
[row
]+1, list_args
, P
->Dimension
, &v
);
2213 value_addto(v
, v
, P
->Constraint
[row
][P
->Dimension
+1]); /*constant part*/
2214 if (value_neg_p(v
) ||
2215 value_zero_p(P
->Constraint
[row
][0]) && value_notzero_p(v
)) {
2222 return in
|| (P
->next
&& in_domain(P
->next
, list_args
));
2225 /****************************************************/
2226 /* function compute enode */
2227 /* compute the value of enode p with parameters */
2228 /* list "list_args */
2229 /* compute the polynomial or the periodic */
2230 /****************************************************/
2232 static double compute_enode(enode
*p
, Value
*list_args
) {
2244 if (p
->type
== polynomial
) {
2246 value_assign(param
,list_args
[p
->pos
-1]);
2248 /* Compute the polynomial using Horner's rule */
2249 for (i
=p
->size
-1;i
>0;i
--) {
2250 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2251 res
*=VALUE_TO_DOUBLE(param
);
2253 res
+=compute_evalue(&p
->arr
[0],list_args
);
2255 else if (p
->type
== fractional
) {
2256 double d
= compute_evalue(&p
->arr
[0], list_args
);
2257 d
-= floor(d
+1e-10);
2259 /* Compute the polynomial using Horner's rule */
2260 for (i
=p
->size
-1;i
>1;i
--) {
2261 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2264 res
+=compute_evalue(&p
->arr
[1],list_args
);
2266 else if (p
->type
== flooring
) {
2267 double d
= compute_evalue(&p
->arr
[0], list_args
);
2270 /* Compute the polynomial using Horner's rule */
2271 for (i
=p
->size
-1;i
>1;i
--) {
2272 res
+=compute_evalue(&p
->arr
[i
],list_args
);
2275 res
+=compute_evalue(&p
->arr
[1],list_args
);
2277 else if (p
->type
== periodic
) {
2278 value_assign(m
,list_args
[p
->pos
-1]);
2280 /* Choose the right element of the periodic */
2281 value_set_si(param
,p
->size
);
2282 value_pmodulus(m
,m
,param
);
2283 res
= compute_evalue(&p
->arr
[VALUE_TO_INT(m
)],list_args
);
2285 else if (p
->type
== relation
) {
2286 if (fabs(compute_evalue(&p
->arr
[0], list_args
)) < 1e-10)
2287 res
= compute_evalue(&p
->arr
[1], list_args
);
2288 else if (p
->size
> 2)
2289 res
= compute_evalue(&p
->arr
[2], list_args
);
2291 else if (p
->type
== partition
) {
2292 int dim
= EVALUE_DOMAIN(p
->arr
[0])->Dimension
;
2293 Value
*vals
= list_args
;
2296 for (i
= 0; i
< dim
; ++i
) {
2297 value_init(vals
[i
]);
2299 value_assign(vals
[i
], list_args
[i
]);
2302 for (i
= 0; i
< p
->size
/2; ++i
)
2303 if (DomainContains(EVALUE_DOMAIN(p
->arr
[2*i
]), vals
, p
->pos
, 0, 1)) {
2304 res
= compute_evalue(&p
->arr
[2*i
+1], vals
);
2308 for (i
= 0; i
< dim
; ++i
)
2309 value_clear(vals
[i
]);
2318 } /* compute_enode */
2320 /*************************************************/
2321 /* return the value of Ehrhart Polynomial */
2322 /* It returns a double, because since it is */
2323 /* a recursive function, some intermediate value */
2324 /* might not be integral */
2325 /*************************************************/
2327 double compute_evalue(const evalue
*e
, Value
*list_args
)
2331 if (value_notzero_p(e
->d
)) {
2332 if (value_notone_p(e
->d
))
2333 res
= VALUE_TO_DOUBLE(e
->x
.n
) / VALUE_TO_DOUBLE(e
->d
);
2335 res
= VALUE_TO_DOUBLE(e
->x
.n
);
2338 res
= compute_enode(e
->x
.p
,list_args
);
2340 } /* compute_evalue */
2343 /****************************************************/
2344 /* function compute_poly : */
2345 /* Check for the good validity domain */
2346 /* return the number of point in the Polyhedron */
2347 /* in allocated memory */
2348 /* Using the Ehrhart pseudo-polynomial */
2349 /****************************************************/
2350 Value
*compute_poly(Enumeration
*en
,Value
*list_args
) {
2353 /* double d; int i; */
2355 tmp
= (Value
*) malloc (sizeof(Value
));
2356 assert(tmp
!= NULL
);
2358 value_set_si(*tmp
,0);
2361 return(tmp
); /* no ehrhart polynomial */
2362 if(en
->ValidityDomain
) {
2363 if(!en
->ValidityDomain
->Dimension
) { /* no parameters */
2364 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
2369 return(tmp
); /* no Validity Domain */
2371 if(in_domain(en
->ValidityDomain
,list_args
)) {
2373 #ifdef EVAL_EHRHART_DEBUG
2374 Print_Domain(stdout
,en
->ValidityDomain
);
2375 print_evalue(stdout
,&en
->EP
);
2378 /* d = compute_evalue(&en->EP,list_args);
2380 printf("(double)%lf = %d\n", d, i ); */
2381 value_set_double(*tmp
,compute_evalue(&en
->EP
,list_args
)+.25);
2387 value_set_si(*tmp
,0);
2388 return(tmp
); /* no compatible domain with the arguments */
2389 } /* compute_poly */
2391 static evalue
*eval_polynomial(const enode
*p
, int offset
,
2392 evalue
*base
, Value
*values
)
2397 res
= evalue_zero();
2398 for (i
= p
->size
-1; i
> offset
; --i
) {
2399 c
= evalue_eval(&p
->arr
[i
], values
);
2404 c
= evalue_eval(&p
->arr
[offset
], values
);
2411 evalue
*evalue_eval(const evalue
*e
, Value
*values
)
2418 if (value_notzero_p(e
->d
)) {
2419 res
= ALLOC(evalue
);
2421 evalue_copy(res
, e
);
2424 switch (e
->x
.p
->type
) {
2426 value_init(param
.x
.n
);
2427 value_assign(param
.x
.n
, values
[e
->x
.p
->pos
-1]);
2428 value_init(param
.d
);
2429 value_set_si(param
.d
, 1);
2431 res
= eval_polynomial(e
->x
.p
, 0, ¶m
, values
);
2432 free_evalue_refs(¶m
);
2435 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2436 mpz_fdiv_r(param2
->x
.n
, param2
->x
.n
, param2
->d
);
2438 res
= eval_polynomial(e
->x
.p
, 1, param2
, values
);
2439 evalue_free(param2
);
2442 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2443 mpz_fdiv_q(param2
->x
.n
, param2
->x
.n
, param2
->d
);
2444 value_set_si(param2
->d
, 1);
2446 res
= eval_polynomial(e
->x
.p
, 1, param2
, values
);
2447 evalue_free(param2
);
2450 param2
= evalue_eval(&e
->x
.p
->arr
[0], values
);
2451 if (value_zero_p(param2
->x
.n
))
2452 res
= evalue_eval(&e
->x
.p
->arr
[1], values
);
2453 else if (e
->x
.p
->size
> 2)
2454 res
= evalue_eval(&e
->x
.p
->arr
[2], values
);
2456 res
= evalue_zero();
2457 evalue_free(param2
);
2460 assert(e
->x
.p
->pos
== EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
);
2461 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2462 if (in_domain(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), values
)) {
2463 res
= evalue_eval(&e
->x
.p
->arr
[2*i
+1], values
);
2467 res
= evalue_zero();
2475 size_t value_size(Value v
) {
2476 return (v
[0]._mp_size
> 0 ? v
[0]._mp_size
: -v
[0]._mp_size
)
2477 * sizeof(v
[0]._mp_d
[0]);
2480 size_t domain_size(Polyhedron
*D
)
2483 size_t s
= sizeof(*D
);
2485 for (i
= 0; i
< D
->NbConstraints
; ++i
)
2486 for (j
= 0; j
< D
->Dimension
+2; ++j
)
2487 s
+= value_size(D
->Constraint
[i
][j
]);
2490 for (i = 0; i < D->NbRays; ++i)
2491 for (j = 0; j < D->Dimension+2; ++j)
2492 s += value_size(D->Ray[i][j]);
2495 return D
->next
? s
+domain_size(D
->next
) : s
;
2498 size_t enode_size(enode
*p
) {
2499 size_t s
= sizeof(*p
) - sizeof(p
->arr
[0]);
2502 if (p
->type
== partition
)
2503 for (i
= 0; i
< p
->size
/2; ++i
) {
2504 s
+= domain_size(EVALUE_DOMAIN(p
->arr
[2*i
]));
2505 s
+= evalue_size(&p
->arr
[2*i
+1]);
2508 for (i
= 0; i
< p
->size
; ++i
) {
2509 s
+= evalue_size(&p
->arr
[i
]);
2514 size_t evalue_size(evalue
*e
)
2516 size_t s
= sizeof(*e
);
2517 s
+= value_size(e
->d
);
2518 if (value_notzero_p(e
->d
))
2519 s
+= value_size(e
->x
.n
);
2521 s
+= enode_size(e
->x
.p
);
2525 static evalue
*find_second(evalue
*base
, evalue
*cst
, evalue
*e
, Value m
)
2527 evalue
*found
= NULL
;
2532 if (value_pos_p(e
->d
) || e
->x
.p
->type
!= fractional
)
2535 value_init(offset
.d
);
2536 value_init(offset
.x
.n
);
2537 poly_denom(&e
->x
.p
->arr
[0], &offset
.d
);
2538 value_lcm(offset
.d
, m
, offset
.d
);
2539 value_set_si(offset
.x
.n
, 1);
2542 evalue_copy(©
, cst
);
2545 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2547 if (eequal(base
, &e
->x
.p
->arr
[0]))
2548 found
= &e
->x
.p
->arr
[0];
2550 value_set_si(offset
.x
.n
, -2);
2553 mpz_fdiv_r(cst
->x
.n
, cst
->x
.n
, cst
->d
);
2555 if (eequal(base
, &e
->x
.p
->arr
[0]))
2558 free_evalue_refs(cst
);
2559 free_evalue_refs(&offset
);
2562 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2563 found
= find_second(base
, cst
, &e
->x
.p
->arr
[i
], m
);
2568 static evalue
*find_relation_pair(evalue
*e
)
2571 evalue
*found
= NULL
;
2573 if (EVALUE_IS_DOMAIN(*e
) || value_pos_p(e
->d
))
2576 if (e
->x
.p
->type
== fractional
) {
2581 poly_denom(&e
->x
.p
->arr
[0], &m
);
2583 for (cst
= &e
->x
.p
->arr
[0]; value_zero_p(cst
->d
);
2584 cst
= &cst
->x
.p
->arr
[0])
2587 for (i
= 1; !found
&& i
< e
->x
.p
->size
; ++i
)
2588 found
= find_second(&e
->x
.p
->arr
[0], cst
, &e
->x
.p
->arr
[i
], m
);
2593 i
= e
->x
.p
->type
== relation
;
2594 for (; !found
&& i
< e
->x
.p
->size
; ++i
)
2595 found
= find_relation_pair(&e
->x
.p
->arr
[i
]);
2600 void evalue_mod2relation(evalue
*e
) {
2603 if (value_zero_p(e
->d
) && e
->x
.p
->type
== partition
) {
2606 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2607 evalue_mod2relation(&e
->x
.p
->arr
[2*i
+1]);
2608 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
2609 value_clear(e
->x
.p
->arr
[2*i
].d
);
2610 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2612 if (2*i
< e
->x
.p
->size
) {
2613 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2614 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2619 if (e
->x
.p
->size
== 0) {
2621 evalue_set_si(e
, 0, 1);
2627 while ((d
= find_relation_pair(e
)) != NULL
) {
2631 value_init(split
.d
);
2632 value_set_si(split
.d
, 0);
2633 split
.x
.p
= new_enode(relation
, 3, 0);
2634 evalue_set_si(&split
.x
.p
->arr
[1], 1, 1);
2635 evalue_set_si(&split
.x
.p
->arr
[2], 1, 1);
2637 ev
= &split
.x
.p
->arr
[0];
2638 value_set_si(ev
->d
, 0);
2639 ev
->x
.p
= new_enode(fractional
, 3, -1);
2640 evalue_set_si(&ev
->x
.p
->arr
[1], 0, 1);
2641 evalue_set_si(&ev
->x
.p
->arr
[2], 1, 1);
2642 evalue_copy(&ev
->x
.p
->arr
[0], d
);
2648 free_evalue_refs(&split
);
2652 static int evalue_comp(const void * a
, const void * b
)
2654 const evalue
*e1
= *(const evalue
**)a
;
2655 const evalue
*e2
= *(const evalue
**)b
;
2656 return ecmp(e1
, e2
);
2659 void evalue_combine(evalue
*e
)
2666 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
2669 NALLOC(evs
, e
->x
.p
->size
/2);
2670 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
2671 evs
[i
] = &e
->x
.p
->arr
[2*i
+1];
2672 qsort(evs
, e
->x
.p
->size
/2, sizeof(evs
[0]), evalue_comp
);
2673 p
= new_enode(partition
, e
->x
.p
->size
, e
->x
.p
->pos
);
2674 for (i
= 0, k
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2675 if (k
== 0 || ecmp(&p
->arr
[2*k
-1], evs
[i
]) != 0) {
2676 value_clear(p
->arr
[2*k
].d
);
2677 value_clear(p
->arr
[2*k
+1].d
);
2678 p
->arr
[2*k
] = *(evs
[i
]-1);
2679 p
->arr
[2*k
+1] = *(evs
[i
]);
2682 Polyhedron
*D
= EVALUE_DOMAIN(*(evs
[i
]-1));
2685 value_clear((evs
[i
]-1)->d
);
2689 L
->next
= EVALUE_DOMAIN(p
->arr
[2*k
-2]);
2690 EVALUE_SET_DOMAIN(p
->arr
[2*k
-2], D
);
2691 free_evalue_refs(evs
[i
]);
2695 for (i
= 2*k
; i
< p
->size
; ++i
)
2696 value_clear(p
->arr
[i
].d
);
2703 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2705 if (value_notzero_p(e
->x
.p
->arr
[2*i
+1].d
))
2707 H
= DomainConvex(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), 0);
2710 for (k
= 0; k
< e
->x
.p
->size
/2; ++k
) {
2711 Polyhedron
*D
, *N
, **P
;
2714 P
= &EVALUE_DOMAIN(e
->x
.p
->arr
[2*k
]);
2721 if (D
->NbEq
<= H
->NbEq
) {
2727 tmp
.x
.p
= new_enode(partition
, 2, e
->x
.p
->pos
);
2728 EVALUE_SET_DOMAIN(tmp
.x
.p
->arr
[0], Polyhedron_Copy(D
));
2729 evalue_copy(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*i
+1]);
2730 reduce_evalue(&tmp
);
2731 if (value_notzero_p(tmp
.d
) ||
2732 ecmp(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*k
+1]) != 0)
2735 D
->next
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2736 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]) = D
;
2739 free_evalue_refs(&tmp
);
2745 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
2747 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
2749 value_clear(e
->x
.p
->arr
[2*i
].d
);
2750 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
2752 if (2*i
< e
->x
.p
->size
) {
2753 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
2754 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
2761 H
= DomainConvex(D
, 0);
2762 E
= DomainDifference(H
, D
, 0);
2764 D
= DomainDifference(H
, E
, 0);
2767 EVALUE_SET_DOMAIN(p
->arr
[2*i
], D
);
2771 /* Use smallest representative for coefficients in affine form in
2772 * argument of fractional.
2773 * Since any change will make the argument non-standard,
2774 * the containing evalue will have to be reduced again afterward.
2776 static void fractional_minimal_coefficients(enode
*p
)
2782 assert(p
->type
== fractional
);
2784 while (value_zero_p(pp
->d
)) {
2785 assert(pp
->x
.p
->type
== polynomial
);
2786 assert(pp
->x
.p
->size
== 2);
2787 assert(value_notzero_p(pp
->x
.p
->arr
[1].d
));
2788 mpz_mul_ui(twice
, pp
->x
.p
->arr
[1].x
.n
, 2);
2789 if (value_gt(twice
, pp
->x
.p
->arr
[1].d
))
2790 value_subtract(pp
->x
.p
->arr
[1].x
.n
,
2791 pp
->x
.p
->arr
[1].x
.n
, pp
->x
.p
->arr
[1].d
);
2792 pp
= &pp
->x
.p
->arr
[0];
2798 static Polyhedron
*polynomial_projection(enode
*p
, Polyhedron
*D
, Value
*d
,
2803 unsigned dim
= D
->Dimension
;
2804 Matrix
*T
= Matrix_Alloc(2, dim
+1);
2807 assert(p
->type
== fractional
|| p
->type
== flooring
);
2808 value_set_si(T
->p
[1][dim
], 1);
2809 evalue_extract_affine(&p
->arr
[0], T
->p
[0], &T
->p
[0][dim
], d
);
2810 I
= DomainImage(D
, T
, 0);
2811 H
= DomainConvex(I
, 0);
2821 static void replace_by_affine(evalue
*e
, Value offset
)
2828 value_init(inc
.x
.n
);
2829 value_set_si(inc
.d
, 1);
2830 value_oppose(inc
.x
.n
, offset
);
2831 eadd(&inc
, &p
->arr
[0]);
2832 reorder_terms_about(p
, &p
->arr
[0]); /* frees arr[0] */
2836 free_evalue_refs(&inc
);
2839 int evalue_range_reduction_in_domain(evalue
*e
, Polyhedron
*D
)
2848 if (value_notzero_p(e
->d
))
2853 if (p
->type
== relation
) {
2860 fractional_minimal_coefficients(p
->arr
[0].x
.p
);
2861 I
= polynomial_projection(p
->arr
[0].x
.p
, D
, &d
, &T
);
2862 bounded
= line_minmax(I
, &min
, &max
); /* frees I */
2863 equal
= value_eq(min
, max
);
2864 mpz_cdiv_q(min
, min
, d
);
2865 mpz_fdiv_q(max
, max
, d
);
2867 if (bounded
&& value_gt(min
, max
)) {
2873 evalue_set_si(e
, 0, 1);
2876 free_evalue_refs(&(p
->arr
[1]));
2877 free_evalue_refs(&(p
->arr
[0]));
2883 return r
? r
: evalue_range_reduction_in_domain(e
, D
);
2884 } else if (bounded
&& equal
) {
2887 free_evalue_refs(&(p
->arr
[2]));
2890 free_evalue_refs(&(p
->arr
[0]));
2896 return evalue_range_reduction_in_domain(e
, D
);
2897 } else if (bounded
&& value_eq(min
, max
)) {
2898 /* zero for a single value */
2900 Matrix
*M
= Matrix_Alloc(1, D
->Dimension
+2);
2901 Vector_Copy(T
->p
[0], M
->p
[0]+1, D
->Dimension
+1);
2902 value_multiply(min
, min
, d
);
2903 value_subtract(M
->p
[0][D
->Dimension
+1],
2904 M
->p
[0][D
->Dimension
+1], min
);
2905 E
= DomainAddConstraints(D
, M
, 0);
2911 r
= evalue_range_reduction_in_domain(&p
->arr
[1], E
);
2913 r
|= evalue_range_reduction_in_domain(&p
->arr
[2], D
);
2915 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2923 _reduce_evalue(&p
->arr
[0].x
.p
->arr
[0], 0, 1);
2926 i
= p
->type
== relation
? 1 :
2927 p
->type
== fractional
? 1 : 0;
2928 for (; i
<p
->size
; i
++)
2929 r
|= evalue_range_reduction_in_domain(&p
->arr
[i
], D
);
2931 if (p
->type
!= fractional
) {
2932 if (r
&& p
->type
== polynomial
) {
2935 value_set_si(f
.d
, 0);
2936 f
.x
.p
= new_enode(polynomial
, 2, p
->pos
);
2937 evalue_set_si(&f
.x
.p
->arr
[0], 0, 1);
2938 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
2939 reorder_terms_about(p
, &f
);
2950 fractional_minimal_coefficients(p
);
2951 I
= polynomial_projection(p
, D
, &d
, NULL
);
2952 bounded
= line_minmax(I
, &min
, &max
); /* frees I */
2953 mpz_fdiv_q(min
, min
, d
);
2954 mpz_fdiv_q(max
, max
, d
);
2955 value_subtract(d
, max
, min
);
2957 if (bounded
&& value_eq(min
, max
)) {
2958 replace_by_affine(e
, min
);
2960 } else if (bounded
&& value_one_p(d
) && p
->size
> 3) {
2961 /* replace {g}^2 by -(g-min)^2 + (2{g}+1)*(g-min) - {g}
2962 * See pages 199-200 of PhD thesis.
2970 value_set_si(rem
.d
, 0);
2971 rem
.x
.p
= new_enode(fractional
, 3, -1);
2972 evalue_copy(&rem
.x
.p
->arr
[0], &p
->arr
[0]);
2973 value_clear(rem
.x
.p
->arr
[1].d
);
2974 value_clear(rem
.x
.p
->arr
[2].d
);
2975 rem
.x
.p
->arr
[1] = p
->arr
[1];
2976 rem
.x
.p
->arr
[2] = p
->arr
[2];
2977 for (i
= 3; i
< p
->size
; ++i
)
2978 p
->arr
[i
-2] = p
->arr
[i
];
2982 value_init(inc
.x
.n
);
2983 value_set_si(inc
.d
, 1);
2984 value_oppose(inc
.x
.n
, min
);
2987 evalue_copy(&t
, &p
->arr
[0]);
2991 value_set_si(f
.d
, 0);
2992 f
.x
.p
= new_enode(fractional
, 3, -1);
2993 evalue_copy(&f
.x
.p
->arr
[0], &p
->arr
[0]);
2994 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
2995 evalue_set_si(&f
.x
.p
->arr
[2], 2, 1);
2997 value_init(factor
.d
);
2998 evalue_set_si(&factor
, -1, 1);
3004 value_clear(f
.x
.p
->arr
[1].x
.n
);
3005 value_clear(f
.x
.p
->arr
[2].x
.n
);
3006 evalue_set_si(&f
.x
.p
->arr
[1], 0, 1);
3007 evalue_set_si(&f
.x
.p
->arr
[2], -1, 1);
3011 evalue_reorder_terms(&rem
);
3012 evalue_reorder_terms(e
);
3018 free_evalue_refs(&inc
);
3019 free_evalue_refs(&t
);
3020 free_evalue_refs(&f
);
3021 free_evalue_refs(&factor
);
3022 free_evalue_refs(&rem
);
3024 evalue_range_reduction_in_domain(e
, D
);
3028 _reduce_evalue(&p
->arr
[0], 0, 1);
3030 evalue_reorder_terms(e
);
3040 void evalue_range_reduction(evalue
*e
)
3043 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
)
3046 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3047 if (evalue_range_reduction_in_domain(&e
->x
.p
->arr
[2*i
+1],
3048 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]))) {
3049 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3051 if (EVALUE_IS_ZERO(e
->x
.p
->arr
[2*i
+1])) {
3052 free_evalue_refs(&e
->x
.p
->arr
[2*i
+1]);
3053 Domain_Free(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]));
3054 value_clear(e
->x
.p
->arr
[2*i
].d
);
3056 e
->x
.p
->arr
[2*i
] = e
->x
.p
->arr
[e
->x
.p
->size
];
3057 e
->x
.p
->arr
[2*i
+1] = e
->x
.p
->arr
[e
->x
.p
->size
+1];
3065 Enumeration
* partition2enumeration(evalue
*EP
)
3068 Enumeration
*en
, *res
= NULL
;
3070 if (EVALUE_IS_ZERO(*EP
)) {
3075 assert(value_zero_p(EP
->d
));
3076 assert(EP
->x
.p
->type
== partition
);
3077 assert(EP
->x
.p
->size
>= 2);
3079 for (i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
3080 assert(EP
->x
.p
->pos
== EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
])->Dimension
);
3081 en
= (Enumeration
*)malloc(sizeof(Enumeration
));
3084 res
->ValidityDomain
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
3085 value_clear(EP
->x
.p
->arr
[2*i
].d
);
3086 res
->EP
= EP
->x
.p
->arr
[2*i
+1];
3094 int evalue_frac2floor_in_domain3(evalue
*e
, Polyhedron
*D
, int shift
)
3103 if (value_notzero_p(e
->d
))
3108 i
= p
->type
== relation
? 1 :
3109 p
->type
== fractional
? 1 : 0;
3110 for (; i
<p
->size
; i
++)
3111 r
|= evalue_frac2floor_in_domain3(&p
->arr
[i
], D
, shift
);
3113 if (p
->type
!= fractional
) {
3114 if (r
&& p
->type
== polynomial
) {
3117 value_set_si(f
.d
, 0);
3118 f
.x
.p
= new_enode(polynomial
, 2, p
->pos
);
3119 evalue_set_si(&f
.x
.p
->arr
[0], 0, 1);
3120 evalue_set_si(&f
.x
.p
->arr
[1], 1, 1);
3121 reorder_terms_about(p
, &f
);
3131 I
= polynomial_projection(p
, D
, &d
, NULL
);
3134 Polyhedron_Print(stderr, P_VALUE_FMT, I);
3137 assert(I
->NbEq
== 0); /* Should have been reduced */
3140 for (i
= 0; i
< I
->NbConstraints
; ++i
)
3141 if (value_pos_p(I
->Constraint
[i
][1]))
3144 if (i
< I
->NbConstraints
) {
3146 value_oppose(I
->Constraint
[i
][2], I
->Constraint
[i
][2]);
3147 mpz_cdiv_q(min
, I
->Constraint
[i
][2], I
->Constraint
[i
][1]);
3148 if (value_neg_p(min
)) {
3150 mpz_fdiv_q(min
, min
, d
);
3151 value_init(offset
.d
);
3152 value_set_si(offset
.d
, 1);
3153 value_init(offset
.x
.n
);
3154 value_oppose(offset
.x
.n
, min
);
3155 eadd(&offset
, &p
->arr
[0]);
3156 free_evalue_refs(&offset
);
3166 value_set_si(fl
.d
, 0);
3167 fl
.x
.p
= new_enode(flooring
, 3, -1);
3168 evalue_set_si(&fl
.x
.p
->arr
[1], 0, 1);
3169 evalue_set_si(&fl
.x
.p
->arr
[2], -1, 1);
3170 evalue_copy(&fl
.x
.p
->arr
[0], &p
->arr
[0]);
3172 eadd(&fl
, &p
->arr
[0]);
3173 reorder_terms_about(p
, &p
->arr
[0]);
3177 free_evalue_refs(&fl
);
3182 int evalue_frac2floor_in_domain(evalue
*e
, Polyhedron
*D
)
3184 return evalue_frac2floor_in_domain3(e
, D
, 1);
3187 void evalue_frac2floor2(evalue
*e
, int shift
)
3190 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
) {
3192 if (evalue_frac2floor_in_domain3(e
, NULL
, 0))
3198 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3199 if (evalue_frac2floor_in_domain3(&e
->x
.p
->arr
[2*i
+1],
3200 EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), shift
))
3201 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3204 void evalue_frac2floor(evalue
*e
)
3206 evalue_frac2floor2(e
, 1);
3209 /* Add a new variable with lower bound 1 and upper bound specified
3210 * by row. If negative is true, then the new variable has upper
3211 * bound -1 and lower bound specified by row.
3213 static Matrix
*esum_add_constraint(int nvar
, Polyhedron
*D
, Matrix
*C
,
3214 Vector
*row
, int negative
)
3218 int nparam
= D
->Dimension
- nvar
;
3221 nr
= D
->NbConstraints
+ 2;
3222 nc
= D
->Dimension
+ 2 + 1;
3223 C
= Matrix_Alloc(nr
, nc
);
3224 for (i
= 0; i
< D
->NbConstraints
; ++i
) {
3225 Vector_Copy(D
->Constraint
[i
], C
->p
[i
], 1 + nvar
);
3226 Vector_Copy(D
->Constraint
[i
] + 1 + nvar
, C
->p
[i
] + 1 + nvar
+ 1,
3227 D
->Dimension
+ 1 - nvar
);
3232 nc
= C
->NbColumns
+ 1;
3233 C
= Matrix_Alloc(nr
, nc
);
3234 for (i
= 0; i
< oldC
->NbRows
; ++i
) {
3235 Vector_Copy(oldC
->p
[i
], C
->p
[i
], 1 + nvar
);
3236 Vector_Copy(oldC
->p
[i
] + 1 + nvar
, C
->p
[i
] + 1 + nvar
+ 1,
3237 oldC
->NbColumns
- 1 - nvar
);
3240 value_set_si(C
->p
[nr
-2][0], 1);
3242 value_set_si(C
->p
[nr
-2][1 + nvar
], -1);
3244 value_set_si(C
->p
[nr
-2][1 + nvar
], 1);
3245 value_set_si(C
->p
[nr
-2][nc
- 1], -1);
3247 Vector_Copy(row
->p
, C
->p
[nr
-1], 1 + nvar
+ 1);
3248 Vector_Copy(row
->p
+ 1 + nvar
+ 1, C
->p
[nr
-1] + C
->NbColumns
- 1 - nparam
,
3254 static void floor2frac_r(evalue
*e
, int nvar
)
3261 if (value_notzero_p(e
->d
))
3266 assert(p
->type
== flooring
);
3267 for (i
= 1; i
< p
->size
; i
++)
3268 floor2frac_r(&p
->arr
[i
], nvar
);
3270 for (pp
= &p
->arr
[0]; value_zero_p(pp
->d
); pp
= &pp
->x
.p
->arr
[0]) {
3271 assert(pp
->x
.p
->type
== polynomial
);
3272 pp
->x
.p
->pos
-= nvar
;
3276 value_set_si(f
.d
, 0);
3277 f
.x
.p
= new_enode(fractional
, 3, -1);
3278 evalue_set_si(&f
.x
.p
->arr
[1], 0, 1);
3279 evalue_set_si(&f
.x
.p
->arr
[2], -1, 1);
3280 evalue_copy(&f
.x
.p
->arr
[0], &p
->arr
[0]);
3282 eadd(&f
, &p
->arr
[0]);
3283 reorder_terms_about(p
, &p
->arr
[0]);
3287 free_evalue_refs(&f
);
3290 /* Convert flooring back to fractional and shift position
3291 * of the parameters by nvar
3293 static void floor2frac(evalue
*e
, int nvar
)
3295 floor2frac_r(e
, nvar
);
3299 int evalue_floor2frac(evalue
*e
)
3304 if (value_notzero_p(e
->d
))
3307 if (e
->x
.p
->type
== partition
) {
3308 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3309 if (evalue_floor2frac(&e
->x
.p
->arr
[2*i
+1]))
3310 reduce_evalue(&e
->x
.p
->arr
[2*i
+1]);
3314 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
3315 r
|= evalue_floor2frac(&e
->x
.p
->arr
[i
]);
3317 if (e
->x
.p
->type
== flooring
) {
3323 evalue_reorder_terms(e
);
3328 evalue
*esum_over_domain_cst(int nvar
, Polyhedron
*D
, Matrix
*C
)
3331 int nparam
= D
->Dimension
- nvar
;
3335 D
= Constraints2Polyhedron(C
, 0);
3339 t
= barvinok_enumerate_e(D
, 0, nparam
, 0);
3341 /* Double check that D was not unbounded. */
3342 assert(!(value_pos_p(t
->d
) && value_neg_p(t
->x
.n
)));
3350 static void domain_signs(Polyhedron
*D
, int *signs
)
3354 POL_ENSURE_VERTICES(D
);
3355 for (j
= 0; j
< D
->Dimension
; ++j
) {
3357 for (k
= 0; k
< D
->NbRays
; ++k
) {
3358 signs
[j
] = value_sign(D
->Ray
[k
][1+j
]);
3365 static evalue
*esum_over_domain(evalue
*e
, int nvar
, Polyhedron
*D
,
3366 int *signs
, Matrix
*C
, unsigned MaxRays
)
3372 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
))
3423 signs
= ALLOCN(int, D
->Dimension
);
3424 domain_signs(D
, signs
);
3427 switch (e
->x
.p
->type
) {
3429 evalue
*pp
= &e
->x
.p
->arr
[0];
3431 if (pp
->x
.p
->pos
> nvar
) {
3432 /* remainder is independent of the summated vars */
3438 floor2frac(&f
, nvar
);
3440 t
= esum_over_domain_cst(nvar
, D
, C
);
3444 free_evalue_refs(&f
);
3452 row
= Vector_Alloc(1 + D
->Dimension
+ 1 + 1);
3453 poly_denom(pp
, &row
->p
[1 + nvar
]);
3454 value_set_si(row
->p
[0], 1);
3455 for (pp
= &e
->x
.p
->arr
[0]; value_zero_p(pp
->d
);
3456 pp
= &pp
->x
.p
->arr
[0]) {
3458 assert(pp
->x
.p
->type
== polynomial
);
3460 if (pos
>= 1 + nvar
)
3462 value_assign(row
->p
[pos
], row
->p
[1+nvar
]);
3463 value_division(row
->p
[pos
], row
->p
[pos
], pp
->x
.p
->arr
[1].d
);
3464 value_multiply(row
->p
[pos
], row
->p
[pos
], pp
->x
.p
->arr
[1].x
.n
);
3466 value_assign(row
->p
[1 + D
->Dimension
+ 1], row
->p
[1+nvar
]);
3467 value_division(row
->p
[1 + D
->Dimension
+ 1],
3468 row
->p
[1 + D
->Dimension
+ 1],
3470 value_multiply(row
->p
[1 + D
->Dimension
+ 1],
3471 row
->p
[1 + D
->Dimension
+ 1],
3473 value_oppose(row
->p
[1 + nvar
], row
->p
[1 + nvar
]);
3477 int pos
= e
->x
.p
->pos
;
3480 factor
= ALLOC(evalue
);
3481 value_init(factor
->d
);
3482 value_set_si(factor
->d
, 0);
3483 factor
->x
.p
= new_enode(polynomial
, 2, pos
- nvar
);
3484 evalue_set_si(&factor
->x
.p
->arr
[0], 0, 1);
3485 evalue_set_si(&factor
->x
.p
->arr
[1], 1, 1);
3489 row
= Vector_Alloc(1 + D
->Dimension
+ 1 + 1);
3490 negative
= signs
[pos
-1] < 0;
3491 value_set_si(row
->p
[0], 1);
3493 value_set_si(row
->p
[pos
], -1);
3494 value_set_si(row
->p
[1 + nvar
], 1);
3496 value_set_si(row
->p
[pos
], 1);
3497 value_set_si(row
->p
[1 + nvar
], -1);
3505 offset
= type_offset(e
->x
.p
);
3507 res
= esum_over_domain(&e
->x
.p
->arr
[offset
], nvar
, D
, signs
, C
, MaxRays
);
3511 evalue_copy(&cum
, factor
);
3515 for (i
= 1; offset
+i
< e
->x
.p
->size
; ++i
) {
3519 C
= esum_add_constraint(nvar
, D
, C
, row
, negative
);
3525 Vector_Print(stderr, P_VALUE_FMT, row);
3527 Matrix_Print(stderr, P_VALUE_FMT, C);
3529 t
= esum_over_domain(&e
->x
.p
->arr
[offset
+i
], nvar
, D
, signs
, C
, MaxRays
);
3534 if (negative
&& (i
% 2))
3544 if (factor
&& offset
+i
+1 < e
->x
.p
->size
)
3551 free_evalue_refs(&cum
);
3552 evalue_free(factor
);
3566 static void Polyhedron_Insert(Polyhedron
***next
, Polyhedron
*Q
)
3576 static Polyhedron
*Polyhedron_Split_Into_Orthants(Polyhedron
*P
,
3581 Vector
*c
= Vector_Alloc(1 + P
->Dimension
+ 1);
3582 value_set_si(c
->p
[0], 1);
3584 if (P
->Dimension
== 0)
3585 return Polyhedron_Copy(P
);
3587 for (i
= 0; i
< P
->Dimension
; ++i
) {
3588 Polyhedron
*L
= NULL
;
3589 Polyhedron
**next
= &L
;
3592 for (I
= D
; I
; I
= I
->next
) {
3594 value_set_si(c
->p
[1+i
], 1);
3595 value_set_si(c
->p
[1+P
->Dimension
], 0);
3596 Q
= AddConstraints(c
->p
, 1, I
, MaxRays
);
3597 Polyhedron_Insert(&next
, Q
);
3598 value_set_si(c
->p
[1+i
], -1);
3599 value_set_si(c
->p
[1+P
->Dimension
], -1);
3600 Q
= AddConstraints(c
->p
, 1, I
, MaxRays
);
3601 Polyhedron_Insert(&next
, Q
);
3602 value_set_si(c
->p
[1+i
], 0);
3612 /* Make arguments of all floors non-negative */
3613 static void shift_floor_in_domain(evalue
*e
, Polyhedron
*D
)
3620 if (value_notzero_p(e
->d
))
3625 for (i
= type_offset(p
); i
< p
->size
; ++i
)
3626 shift_floor_in_domain(&p
->arr
[i
], D
);
3628 if (p
->type
!= flooring
)
3634 I
= polynomial_projection(p
, D
, &d
, NULL
);
3635 assert(I
->NbEq
== 0); /* Should have been reduced */
3637 for (i
= 0; i
< I
->NbConstraints
; ++i
)
3638 if (value_pos_p(I
->Constraint
[i
][1]))
3640 assert(i
< I
->NbConstraints
);
3641 if (i
< I
->NbConstraints
) {
3642 value_oppose(I
->Constraint
[i
][2], I
->Constraint
[i
][2]);
3643 mpz_fdiv_q(m
, I
->Constraint
[i
][2], I
->Constraint
[i
][1]);
3644 if (value_neg_p(m
)) {
3645 /* replace [e] by [e-m]+m such that e-m >= 0 */
3650 value_set_si(f
.d
, 1);
3651 value_oppose(f
.x
.n
, m
);
3652 eadd(&f
, &p
->arr
[0]);
3655 value_set_si(f
.d
, 0);
3656 f
.x
.p
= new_enode(flooring
, 3, -1);
3657 value_clear(f
.x
.p
->arr
[0].d
);
3658 f
.x
.p
->arr
[0] = p
->arr
[0];
3659 evalue_set_si(&f
.x
.p
->arr
[2], 1, 1);
3660 value_set_si(f
.x
.p
->arr
[1].d
, 1);
3661 value_init(f
.x
.p
->arr
[1].x
.n
);
3662 value_assign(f
.x
.p
->arr
[1].x
.n
, m
);
3663 reorder_terms_about(p
, &f
);
3674 evalue
*box_summate(Polyhedron
*P
, evalue
*E
, unsigned nvar
, unsigned MaxRays
)
3676 evalue
*sum
= evalue_zero();
3677 Polyhedron
*D
= Polyhedron_Split_Into_Orthants(P
, MaxRays
);
3678 for (P
= D
; P
; P
= P
->next
) {
3680 evalue
*fe
= evalue_dup(E
);
3681 Polyhedron
*next
= P
->next
;
3683 reduce_evalue_in_domain(fe
, P
);
3684 evalue_frac2floor2(fe
, 0);
3685 shift_floor_in_domain(fe
, P
);
3686 t
= esum_over_domain(fe
, nvar
, P
, NULL
, NULL
, MaxRays
);
3698 /* Initial silly implementation */
3699 void eor(evalue
*e1
, evalue
*res
)
3705 evalue_set_si(&mone
, -1, 1);
3707 evalue_copy(&E
, res
);
3713 free_evalue_refs(&E
);
3714 free_evalue_refs(&mone
);
3717 /* computes denominator of polynomial evalue
3718 * d should point to a value initialized to 1
3720 void evalue_denom(const evalue
*e
, Value
*d
)
3724 if (value_notzero_p(e
->d
)) {
3725 value_lcm(*d
, *d
, e
->d
);
3728 assert(e
->x
.p
->type
== polynomial
||
3729 e
->x
.p
->type
== fractional
||
3730 e
->x
.p
->type
== flooring
);
3731 offset
= type_offset(e
->x
.p
);
3732 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3733 evalue_denom(&e
->x
.p
->arr
[i
], d
);
3736 /* Divides the evalue e by the integer n */
3737 void evalue_div(evalue
*e
, Value n
)
3741 if (value_one_p(n
) || EVALUE_IS_ZERO(*e
))
3744 if (value_notzero_p(e
->d
)) {
3747 value_multiply(e
->d
, e
->d
, n
);
3748 value_gcd(gc
, e
->x
.n
, e
->d
);
3749 if (value_notone_p(gc
)) {
3750 value_division(e
->d
, e
->d
, gc
);
3751 value_division(e
->x
.n
, e
->x
.n
, gc
);
3756 if (e
->x
.p
->type
== partition
) {
3757 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3758 evalue_div(&e
->x
.p
->arr
[2*i
+1], n
);
3761 offset
= type_offset(e
->x
.p
);
3762 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3763 evalue_div(&e
->x
.p
->arr
[i
], n
);
3766 /* Multiplies the evalue e by the integer n */
3767 void evalue_mul(evalue
*e
, Value n
)
3771 if (value_one_p(n
) || EVALUE_IS_ZERO(*e
))
3774 if (value_notzero_p(e
->d
)) {
3777 value_multiply(e
->x
.n
, e
->x
.n
, n
);
3778 value_gcd(gc
, e
->x
.n
, e
->d
);
3779 if (value_notone_p(gc
)) {
3780 value_division(e
->d
, e
->d
, gc
);
3781 value_division(e
->x
.n
, e
->x
.n
, gc
);
3786 if (e
->x
.p
->type
== partition
) {
3787 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3788 evalue_mul(&e
->x
.p
->arr
[2*i
+1], n
);
3791 offset
= type_offset(e
->x
.p
);
3792 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3793 evalue_mul(&e
->x
.p
->arr
[i
], n
);
3796 /* Multiplies the evalue e by the n/d */
3797 void evalue_mul_div(evalue
*e
, Value n
, Value d
)
3801 if ((value_one_p(n
) && value_one_p(d
)) || EVALUE_IS_ZERO(*e
))
3804 if (value_notzero_p(e
->d
)) {
3807 value_multiply(e
->x
.n
, e
->x
.n
, n
);
3808 value_multiply(e
->d
, e
->d
, d
);
3809 value_gcd(gc
, e
->x
.n
, e
->d
);
3810 if (value_notone_p(gc
)) {
3811 value_division(e
->d
, e
->d
, gc
);
3812 value_division(e
->x
.n
, e
->x
.n
, gc
);
3817 if (e
->x
.p
->type
== partition
) {
3818 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3819 evalue_mul_div(&e
->x
.p
->arr
[2*i
+1], n
, d
);
3822 offset
= type_offset(e
->x
.p
);
3823 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3824 evalue_mul_div(&e
->x
.p
->arr
[i
], n
, d
);
3827 void evalue_negate(evalue
*e
)
3831 if (value_notzero_p(e
->d
)) {
3832 value_oppose(e
->x
.n
, e
->x
.n
);
3835 if (e
->x
.p
->type
== partition
) {
3836 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3837 evalue_negate(&e
->x
.p
->arr
[2*i
+1]);
3840 offset
= type_offset(e
->x
.p
);
3841 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
3842 evalue_negate(&e
->x
.p
->arr
[i
]);
3845 void evalue_add_constant(evalue
*e
, const Value cst
)
3849 if (value_zero_p(e
->d
)) {
3850 if (e
->x
.p
->type
== partition
) {
3851 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
3852 evalue_add_constant(&e
->x
.p
->arr
[2*i
+1], cst
);
3855 if (e
->x
.p
->type
== relation
) {
3856 for (i
= 1; i
< e
->x
.p
->size
; ++i
)
3857 evalue_add_constant(&e
->x
.p
->arr
[i
], cst
);
3861 e
= &e
->x
.p
->arr
[type_offset(e
->x
.p
)];
3862 } while (value_zero_p(e
->d
));
3864 value_addmul(e
->x
.n
, cst
, e
->d
);
3867 static void evalue_frac2polynomial_r(evalue
*e
, int *signs
, int sign
, int in_frac
)
3872 int sign_odd
= sign
;
3874 if (value_notzero_p(e
->d
)) {
3875 if (in_frac
&& sign
* value_sign(e
->x
.n
) < 0) {
3876 value_set_si(e
->x
.n
, 0);
3877 value_set_si(e
->d
, 1);
3882 if (e
->x
.p
->type
== relation
) {
3883 for (i
= e
->x
.p
->size
-1; i
>= 1; --i
)
3884 evalue_frac2polynomial_r(&e
->x
.p
->arr
[i
], signs
, sign
, in_frac
);
3888 if (e
->x
.p
->type
== polynomial
)
3889 sign_odd
*= signs
[e
->x
.p
->pos
-1];
3890 offset
= type_offset(e
->x
.p
);
3891 evalue_frac2polynomial_r(&e
->x
.p
->arr
[offset
], signs
, sign
, in_frac
);
3892 in_frac
|= e
->x
.p
->type
== fractional
;
3893 for (i
= e
->x
.p
->size
-1; i
> offset
; --i
)
3894 evalue_frac2polynomial_r(&e
->x
.p
->arr
[i
], signs
,
3895 (i
- offset
) % 2 ? sign_odd
: sign
, in_frac
);
3897 if (e
->x
.p
->type
!= fractional
)
3900 /* replace { a/m } by (m-1)/m if sign != 0
3901 * and by (m-1)/(2m) if sign == 0
3905 evalue_denom(&e
->x
.p
->arr
[0], &d
);
3906 free_evalue_refs(&e
->x
.p
->arr
[0]);
3907 value_init(e
->x
.p
->arr
[0].d
);
3908 value_init(e
->x
.p
->arr
[0].x
.n
);
3910 value_addto(e
->x
.p
->arr
[0].d
, d
, d
);
3912 value_assign(e
->x
.p
->arr
[0].d
, d
);
3913 value_decrement(e
->x
.p
->arr
[0].x
.n
, d
);
3917 reorder_terms_about(p
, &p
->arr
[0]);
3923 /* Approximate the evalue in fractional representation by a polynomial.
3924 * If sign > 0, the result is an upper bound;
3925 * if sign < 0, the result is a lower bound;
3926 * if sign = 0, the result is an intermediate approximation.
3928 void evalue_frac2polynomial(evalue
*e
, int sign
, unsigned MaxRays
)
3933 if (value_notzero_p(e
->d
))
3935 assert(e
->x
.p
->type
== partition
);
3936 /* make sure all variables in the domains have a fixed sign */
3938 evalue_split_domains_into_orthants(e
, MaxRays
);
3939 if (EVALUE_IS_ZERO(*e
))
3943 assert(e
->x
.p
->size
>= 2);
3944 dim
= EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
;
3946 signs
= ALLOCN(int, dim
);
3949 for (i
= 0; i
< dim
; ++i
)
3951 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
3953 domain_signs(EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]), signs
);
3954 evalue_frac2polynomial_r(&e
->x
.p
->arr
[2*i
+1], signs
, sign
, 0);
3960 /* Split the domains of e (which is assumed to be a partition)
3961 * such that each resulting domain lies entirely in one orthant.
3963 void evalue_split_domains_into_orthants(evalue
*e
, unsigned MaxRays
)
3966 assert(value_zero_p(e
->d
));
3967 assert(e
->x
.p
->type
== partition
);
3968 assert(e
->x
.p
->size
>= 2);
3969 dim
= EVALUE_DOMAIN(e
->x
.p
->arr
[0])->Dimension
;
3971 for (i
= 0; i
< dim
; ++i
) {
3974 C
= Matrix_Alloc(1, 1 + dim
+ 1);
3975 value_set_si(C
->p
[0][0], 1);
3976 value_init(split
.d
);
3977 value_set_si(split
.d
, 0);
3978 split
.x
.p
= new_enode(partition
, 4, dim
);
3979 value_set_si(C
->p
[0][1+i
], 1);
3980 C2
= Matrix_Copy(C
);
3981 EVALUE_SET_DOMAIN(split
.x
.p
->arr
[0], Constraints2Polyhedron(C2
, MaxRays
));
3983 evalue_set_si(&split
.x
.p
->arr
[1], 1, 1);
3984 value_set_si(C
->p
[0][1+i
], -1);
3985 value_set_si(C
->p
[0][1+dim
], -1);
3986 EVALUE_SET_DOMAIN(split
.x
.p
->arr
[2], Constraints2Polyhedron(C
, MaxRays
));
3987 evalue_set_si(&split
.x
.p
->arr
[3], 1, 1);
3989 free_evalue_refs(&split
);
3994 static evalue
*find_fractional_with_max_periods(evalue
*e
, Polyhedron
*D
,
3997 Value
*min
, Value
*max
)
4004 if (value_notzero_p(e
->d
))
4007 if (e
->x
.p
->type
== fractional
) {
4012 I
= polynomial_projection(e
->x
.p
, D
, &d
, &T
);
4013 bounded
= line_minmax(I
, min
, max
); /* frees I */
4017 value_set_si(mp
, max_periods
);
4018 mpz_fdiv_q(*min
, *min
, d
);
4019 mpz_fdiv_q(*max
, *max
, d
);
4020 value_assign(T
->p
[1][D
->Dimension
], d
);
4021 value_subtract(d
, *max
, *min
);
4022 if (value_ge(d
, mp
))
4025 f
= evalue_dup(&e
->x
.p
->arr
[0]);
4036 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4037 if ((f
= find_fractional_with_max_periods(&e
->x
.p
->arr
[i
], D
, max_periods
,
4044 static void replace_fract_by_affine(evalue
*e
, evalue
*f
, Value val
)
4048 if (value_notzero_p(e
->d
))
4051 offset
= type_offset(e
->x
.p
);
4052 for (i
= e
->x
.p
->size
-1; i
>= offset
; --i
)
4053 replace_fract_by_affine(&e
->x
.p
->arr
[i
], f
, val
);
4055 if (e
->x
.p
->type
!= fractional
)
4058 if (!eequal(&e
->x
.p
->arr
[0], f
))
4061 replace_by_affine(e
, val
);
4064 /* Look for fractional parts that can be removed by splitting the corresponding
4065 * domain into at most max_periods parts.
4066 * We use a very simply strategy that looks for the first fractional part
4067 * that satisfies the condition, performs the split and then continues
4068 * looking for other fractional parts in the split domains until no
4069 * such fractional part can be found anymore.
4071 void evalue_split_periods(evalue
*e
, int max_periods
, unsigned int MaxRays
)
4078 if (EVALUE_IS_ZERO(*e
))
4080 if (value_notzero_p(e
->d
) || e
->x
.p
->type
!= partition
) {
4082 "WARNING: evalue_split_periods called on incorrect evalue type\n");
4090 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
4095 Polyhedron
*D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]);
4097 f
= find_fractional_with_max_periods(&e
->x
.p
->arr
[2*i
+1], D
, max_periods
,
4102 M
= Matrix_Alloc(2, 2+D
->Dimension
);
4104 value_subtract(d
, max
, min
);
4105 n
= VALUE_TO_INT(d
)+1;
4107 value_set_si(M
->p
[0][0], 1);
4108 Vector_Copy(T
->p
[0], M
->p
[0]+1, D
->Dimension
+1);
4109 value_multiply(d
, max
, T
->p
[1][D
->Dimension
]);
4110 value_subtract(M
->p
[0][1+D
->Dimension
], M
->p
[0][1+D
->Dimension
], d
);
4111 value_set_si(d
, -1);
4112 value_set_si(M
->p
[1][0], 1);
4113 Vector_Scale(T
->p
[0], M
->p
[1]+1, d
, D
->Dimension
+1);
4114 value_addmul(M
->p
[1][1+D
->Dimension
], max
, T
->p
[1][D
->Dimension
]);
4115 value_addto(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
],
4116 T
->p
[1][D
->Dimension
]);
4117 value_decrement(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
]);
4119 p
= new_enode(partition
, e
->x
.p
->size
+ (n
-1)*2, e
->x
.p
->pos
);
4120 for (j
= 0; j
< 2*i
; ++j
) {
4121 value_clear(p
->arr
[j
].d
);
4122 p
->arr
[j
] = e
->x
.p
->arr
[j
];
4124 for (j
= 2*i
+2; j
< e
->x
.p
->size
; ++j
) {
4125 value_clear(p
->arr
[j
+2*(n
-1)].d
);
4126 p
->arr
[j
+2*(n
-1)] = e
->x
.p
->arr
[j
];
4128 for (j
= n
-1; j
>= 0; --j
) {
4130 value_clear(p
->arr
[2*i
+1].d
);
4131 p
->arr
[2*i
+1] = e
->x
.p
->arr
[2*i
+1];
4133 evalue_copy(&p
->arr
[2*(i
+j
)+1], &e
->x
.p
->arr
[2*i
+1]);
4135 value_subtract(M
->p
[1][1+D
->Dimension
], M
->p
[1][1+D
->Dimension
],
4136 T
->p
[1][D
->Dimension
]);
4137 value_addto(M
->p
[0][1+D
->Dimension
], M
->p
[0][1+D
->Dimension
],
4138 T
->p
[1][D
->Dimension
]);
4140 replace_fract_by_affine(&p
->arr
[2*(i
+j
)+1], f
, max
);
4141 E
= DomainAddConstraints(D
, M
, MaxRays
);
4142 EVALUE_SET_DOMAIN(p
->arr
[2*(i
+j
)], E
);
4143 if (evalue_range_reduction_in_domain(&p
->arr
[2*(i
+j
)+1], E
))
4144 reduce_evalue(&p
->arr
[2*(i
+j
)+1]);
4145 value_decrement(max
, max
);
4147 value_clear(e
->x
.p
->arr
[2*i
].d
);
4162 void evalue_extract_affine(const evalue
*e
, Value
*coeff
, Value
*cst
, Value
*d
)
4164 value_set_si(*d
, 1);
4166 for ( ; value_zero_p(e
->d
); e
= &e
->x
.p
->arr
[0]) {
4168 assert(e
->x
.p
->type
== polynomial
);
4169 assert(e
->x
.p
->size
== 2);
4170 c
= &e
->x
.p
->arr
[1];
4171 value_multiply(coeff
[e
->x
.p
->pos
-1], *d
, c
->x
.n
);
4172 value_division(coeff
[e
->x
.p
->pos
-1], coeff
[e
->x
.p
->pos
-1], c
->d
);
4174 value_multiply(*cst
, *d
, e
->x
.n
);
4175 value_division(*cst
, *cst
, e
->d
);
4178 /* returns an evalue that corresponds to
4182 static evalue
*term(int param
, Value c
, Value den
)
4184 evalue
*EP
= ALLOC(evalue
);
4186 value_set_si(EP
->d
,0);
4187 EP
->x
.p
= new_enode(polynomial
, 2, param
+ 1);
4188 evalue_set_si(&EP
->x
.p
->arr
[0], 0, 1);
4189 evalue_set_reduce(&EP
->x
.p
->arr
[1], c
, den
);
4193 evalue
*affine2evalue(Value
*coeff
, Value denom
, int nvar
)
4196 evalue
*E
= ALLOC(evalue
);
4198 evalue_set_reduce(E
, coeff
[nvar
], denom
);
4199 for (i
= 0; i
< nvar
; ++i
) {
4201 if (value_zero_p(coeff
[i
]))
4203 t
= term(i
, coeff
[i
], denom
);
4210 void evalue_substitute(evalue
*e
, evalue
**subs
)
4216 if (value_notzero_p(e
->d
))
4220 assert(p
->type
!= partition
);
4222 for (i
= 0; i
< p
->size
; ++i
)
4223 evalue_substitute(&p
->arr
[i
], subs
);
4225 if (p
->type
== relation
) {
4226 /* For relation a ? b : c, compute (a' ? 1) * b' + (a' ? 0 : 1) * c' */
4230 value_set_si(v
->d
, 0);
4231 v
->x
.p
= new_enode(relation
, 3, 0);
4232 evalue_copy(&v
->x
.p
->arr
[0], &p
->arr
[0]);
4233 evalue_set_si(&v
->x
.p
->arr
[1], 0, 1);
4234 evalue_set_si(&v
->x
.p
->arr
[2], 1, 1);
4235 emul(v
, &p
->arr
[2]);
4240 value_set_si(v
->d
, 0);
4241 v
->x
.p
= new_enode(relation
, 2, 0);
4242 value_clear(v
->x
.p
->arr
[0].d
);
4243 v
->x
.p
->arr
[0] = p
->arr
[0];
4244 evalue_set_si(&v
->x
.p
->arr
[1], 1, 1);
4245 emul(v
, &p
->arr
[1]);
4248 eadd(&p
->arr
[2], &p
->arr
[1]);
4249 free_evalue_refs(&p
->arr
[2]);
4257 if (p
->type
== polynomial
)
4262 value_set_si(v
->d
, 0);
4263 v
->x
.p
= new_enode(p
->type
, 3, -1);
4264 value_clear(v
->x
.p
->arr
[0].d
);
4265 v
->x
.p
->arr
[0] = p
->arr
[0];
4266 evalue_set_si(&v
->x
.p
->arr
[1], 0, 1);
4267 evalue_set_si(&v
->x
.p
->arr
[2], 1, 1);
4270 offset
= type_offset(p
);
4272 for (i
= p
->size
-1; i
>= offset
+1; i
--) {
4273 emul(v
, &p
->arr
[i
]);
4274 eadd(&p
->arr
[i
], &p
->arr
[i
-1]);
4275 free_evalue_refs(&(p
->arr
[i
]));
4278 if (p
->type
!= polynomial
)
4282 *e
= p
->arr
[offset
];
4286 /* evalue e is given in terms of "new" parameter; CP maps the new
4287 * parameters back to the old parameters.
4288 * Transforms e such that it refers back to the old parameters and
4289 * adds appropriate constraints to the domain.
4290 * In particular, if CP maps the new parameters onto an affine
4291 * subspace of the old parameters, then the corresponding equalities
4292 * are added to the domain.
4293 * Also, if any of the new parameters was a rational combination
4294 * of the old parameters $p' = (<a, p> + c)/m$, then modulo
4295 * constraints ${<a, p> + c)/m} = 0$ are added to ensure
4296 * the new evalue remains non-zero only for integer parameters
4297 * of the new parameters (which have been removed by the substitution).
4299 void evalue_backsubstitute(evalue
*e
, Matrix
*CP
, unsigned MaxRays
)
4306 unsigned nparam
= CP
->NbColumns
-1;
4310 if (EVALUE_IS_ZERO(*e
))
4313 assert(value_zero_p(e
->d
));
4315 assert(p
->type
== partition
);
4317 inv
= left_inverse(CP
, &eq
);
4318 subs
= ALLOCN(evalue
*, nparam
);
4319 for (i
= 0; i
< nparam
; ++i
)
4320 subs
[i
] = affine2evalue(inv
->p
[i
], inv
->p
[nparam
][inv
->NbColumns
-1],
4323 CEq
= Constraints2Polyhedron(eq
, MaxRays
);
4324 addeliminatedparams_partition(p
, inv
, CEq
, inv
->NbColumns
-1, MaxRays
);
4325 Polyhedron_Free(CEq
);
4327 for (i
= 0; i
< p
->size
/2; ++i
)
4328 evalue_substitute(&p
->arr
[2*i
+1], subs
);
4330 for (i
= 0; i
< nparam
; ++i
)
4331 evalue_free(subs
[i
]);
4335 for (i
= 0; i
< inv
->NbRows
-1; ++i
) {
4336 Vector_Gcd(inv
->p
[i
], inv
->NbColumns
, &gcd
);
4337 value_gcd(gcd
, gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]);
4338 if (value_eq(gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]))
4340 Vector_AntiScale(inv
->p
[i
], inv
->p
[i
], gcd
, inv
->NbColumns
);
4341 value_divexact(gcd
, inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1], gcd
);
4343 for (j
= 0; j
< p
->size
/2; ++j
) {
4344 evalue
*arg
= affine2evalue(inv
->p
[i
], gcd
, inv
->NbColumns
-1);
4349 value_set_si(rel
.d
, 0);
4350 rel
.x
.p
= new_enode(relation
, 2, 0);
4351 value_clear(rel
.x
.p
->arr
[1].d
);
4352 rel
.x
.p
->arr
[1] = p
->arr
[2*j
+1];
4353 ev
= &rel
.x
.p
->arr
[0];
4354 value_set_si(ev
->d
, 0);
4355 ev
->x
.p
= new_enode(fractional
, 3, -1);
4356 evalue_set_si(&ev
->x
.p
->arr
[1], 0, 1);
4357 evalue_set_si(&ev
->x
.p
->arr
[2], 1, 1);
4358 value_clear(ev
->x
.p
->arr
[0].d
);
4359 ev
->x
.p
->arr
[0] = *arg
;
4362 p
->arr
[2*j
+1] = rel
;
4373 * \sum_{i=0}^n c_i/d X^i
4375 * where d is the last element in the vector c.
4377 evalue
*evalue_polynomial(Vector
*c
, const evalue
* X
)
4379 unsigned dim
= c
->Size
-2;
4381 evalue
*EP
= ALLOC(evalue
);
4386 if (EVALUE_IS_ZERO(*X
) || dim
== 0) {
4387 evalue_set(EP
, c
->p
[0], c
->p
[dim
+1]);
4388 reduce_constant(EP
);
4392 evalue_set(EP
, c
->p
[dim
], c
->p
[dim
+1]);
4395 evalue_set(&EC
, c
->p
[dim
], c
->p
[dim
+1]);
4397 for (i
= dim
-1; i
>= 0; --i
) {
4399 value_assign(EC
.x
.n
, c
->p
[i
]);
4402 free_evalue_refs(&EC
);
4406 /* Create an evalue from an array of pairs of domains and evalues. */
4407 evalue
*evalue_from_section_array(struct evalue_section
*s
, int n
)
4412 res
= ALLOC(evalue
);
4416 evalue_set_si(res
, 0, 1);
4418 value_set_si(res
->d
, 0);
4419 res
->x
.p
= new_enode(partition
, 2*n
, s
[0].D
->Dimension
);
4420 for (i
= 0; i
< n
; ++i
) {
4421 EVALUE_SET_DOMAIN(res
->x
.p
->arr
[2*i
], s
[i
].D
);
4422 value_clear(res
->x
.p
->arr
[2*i
+1].d
);
4423 res
->x
.p
->arr
[2*i
+1] = *s
[i
].E
;
4430 /* shift variables (>= first, 0-based) in polynomial n up (may be negative) */
4431 void evalue_shift_variables(evalue
*e
, int first
, int n
)
4434 if (value_notzero_p(e
->d
))
4436 assert(e
->x
.p
->type
== polynomial
||
4437 e
->x
.p
->type
== flooring
||
4438 e
->x
.p
->type
== fractional
);
4439 if (e
->x
.p
->type
== polynomial
&& e
->x
.p
->pos
>= first
+1) {
4440 assert(e
->x
.p
->pos
+ n
>= 1);
4443 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
4444 evalue_shift_variables(&e
->x
.p
->arr
[i
], first
, n
);
4447 static const evalue
*outer_floor(evalue
*e
, const evalue
*outer
)
4451 if (value_notzero_p(e
->d
))
4453 switch (e
->x
.p
->type
) {
4455 if (!outer
|| evalue_level_cmp(outer
, &e
->x
.p
->arr
[0]) > 0)
4456 return &e
->x
.p
->arr
[0];
4462 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4463 outer
= outer_floor(&e
->x
.p
->arr
[i
], outer
);
4466 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
)
4467 outer
= outer_floor(&e
->x
.p
->arr
[2*i
+1], outer
);
4474 /* Find and return outermost floor argument or NULL if e has no floors */
4475 evalue
*evalue_outer_floor(evalue
*e
)
4477 const evalue
*floor
= outer_floor(e
, NULL
);
4478 return floor
? evalue_dup(floor
): NULL
;
4481 static void evalue_set_to_zero(evalue
*e
)
4483 if (EVALUE_IS_ZERO(*e
))
4485 if (value_zero_p(e
->d
)) {
4486 free_evalue_refs(e
);
4490 value_set_si(e
->d
, 1);
4491 value_set_si(e
->x
.n
, 0);
4494 /* Replace (outer) floor with argument "floor" by variable "var" (0-based)
4495 * and drop terms not containing the floor.
4496 * Returns true if e contains the floor.
4498 int evalue_replace_floor(evalue
*e
, const evalue
*floor
, int var
)
4504 if (value_notzero_p(e
->d
))
4506 switch (e
->x
.p
->type
) {
4508 if (!eequal(floor
, &e
->x
.p
->arr
[0]))
4510 e
->x
.p
->type
= polynomial
;
4511 e
->x
.p
->pos
= 1 + var
;
4513 free_evalue_refs(&e
->x
.p
->arr
[0]);
4514 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
4515 e
->x
.p
->arr
[i
] = e
->x
.p
->arr
[i
+1];
4516 evalue_set_to_zero(&e
->x
.p
->arr
[0]);
4521 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
) {
4522 int c
= evalue_replace_floor(&e
->x
.p
->arr
[i
], floor
, var
);
4525 evalue_set_to_zero(&e
->x
.p
->arr
[i
]);
4526 if (c
&& !reorder
&& evalue_level_cmp(&e
->x
.p
->arr
[i
], e
) < 0)
4529 evalue_reduce_size(e
);
4531 evalue_reorder_terms(e
);
4539 /* Replace (outer) floor with argument "floor" by variable zero */
4540 void evalue_drop_floor(evalue
*e
, const evalue
*floor
)
4545 if (value_notzero_p(e
->d
))
4547 switch (e
->x
.p
->type
) {
4549 if (!eequal(floor
, &e
->x
.p
->arr
[0]))
4552 free_evalue_refs(&p
->arr
[0]);
4553 for (i
= 2; i
< p
->size
; ++i
)
4554 free_evalue_refs(&p
->arr
[i
]);
4562 for (i
= type_offset(e
->x
.p
); i
< e
->x
.p
->size
; ++i
)
4563 evalue_drop_floor(&e
->x
.p
->arr
[i
], floor
);
4564 evalue_reduce_size(e
);