From 9afd93e083fae0fa29c996c4bd3fb4b937f33b9e Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 14 Mar 2008 11:31:26 +0100 Subject: [PATCH] verify.c: extract common code for verifying operation on evalue --- maximize.cc | 92 +++++------------------------------------- summate.cc | 111 ++++++--------------------------------------------- verify.c | 130 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ verify.h | 11 +++++ 4 files changed, 164 insertions(+), 180 deletions(-) diff --git a/maximize.cc b/maximize.cc index 2ff58b7..0c7c6ac 100644 --- a/maximize.cc +++ b/maximize.cc @@ -88,16 +88,12 @@ static int check_poly_max(const struct check_poly_data *data, int nparam, Value *z, const struct verify_options *options); -struct check_poly_max_data : public check_poly_data { - int n_S; - Polyhedron **S; - evalue *EP; +struct check_poly_max_data : public check_EP_data { piecewise_lst *pl; - check_poly_max_data(Value *z, evalue *EP, piecewise_lst *pl) : - EP(EP), pl(pl) { - this->z = z; - this->check = check_poly_max; + check_poly_max_data(evalue *EP, piecewise_lst *pl) : pl(pl) { + this->EP = EP; + this->cp.check = check_poly_max; } }; @@ -108,7 +104,7 @@ static void optimum(Polyhedron *S, int pos, const check_poly_max_data *data, if (!S) { Value c; value_init(c); - value_set_double(c, compute_evalue(data->EP, data->z+1)+.25); + value_set_double(c, compute_evalue(data->EP, data->cp.z+1)+.25); if (!found) { value_assign(*opt, c); found = true; @@ -127,13 +123,13 @@ static void optimum(Polyhedron *S, int pos, const check_poly_max_data *data, int ok; value_init(LB); value_init(UB); - ok = !(lower_upper_bounds(1+pos, S, data->z, &LB, &UB)); + ok = !(lower_upper_bounds(1+pos, S, data->cp.z, &LB, &UB)); assert(ok); for (; value_le(LB, UB); value_increment(LB, LB)) { - value_assign(data->z[1+pos], LB); + value_assign(data->cp.z[1+pos], LB); optimum(S->next, pos+1, data, opt, found, options); } - value_set_si(data->z[1+pos], 0); + value_set_si(data->cp.z[1+pos], 0); value_clear(LB); value_clear(UB); } @@ -156,7 +152,7 @@ static int check_poly_max(const struct check_poly_data *data, int k; int ok; const check_poly_max_data *max_data; - max_data = static_cast(data); + max_data = (const check_poly_max_data *)data; const char *minmax; Value m, n, d; value_init(m); @@ -236,77 +232,11 @@ static int check_poly_max(const struct check_poly_data *data, return ok; } -static int verify(Polyhedron *D, piecewise_lst *pl, evalue *EP, - unsigned nvar, unsigned nparam, Vector *p, - struct verify_options *options) -{ - Polyhedron *CS, *S; - unsigned MaxRays = options->barvinok->MaxRays; - assert(value_zero_p(EP->d)); - assert(EP->x.p->type == partition); - int ok = 1; - - CS = check_poly_context_scan(NULL, &D, D->Dimension, options); - - check_poly_init(D, options); - - if (!(CS && emptyQ2(CS))) { - int n_S = 0; - - for (int i = 0; i < EP->x.p->size/2; ++i) { - Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]); - for (; A; A = A->next) - ++n_S; - } - - check_poly_max_data data(p->p, EP, pl); - data.n_S = n_S; - data.S = ALLOCN(Polyhedron *, n_S); - n_S = 0; - for (int i = 0; i < EP->x.p->size/2; ++i) { - Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]); - for (; A; A = A->next) { - Polyhedron *next = A->next; - A->next = NULL; - data.S[n_S++] = Polyhedron_Scan(A, D, - MaxRays & POL_NO_DUAL ? 0 : MaxRays); - A->next = next; - } - } - ok = check_poly(CS, &data, nparam, 0, p->p+1+nvar, options); - for (int i = 0; i < data.n_S; ++i) - Domain_Free(data.S[i]); - free(data.S); - } - - if (!options->print_all) - printf("\n"); - - if (CS) { - Domain_Free(CS); - Domain_Free(D); - } - - return ok; -} - static int verify(piecewise_lst *pl, evalue *EP, unsigned nvar, unsigned nparam, struct verify_options *options) { - Vector *p; - - p = Vector_Alloc(nvar+nparam+2); - value_set_si(p->p[nvar+nparam+1], 1); - - for (int i = 0; i < pl->list.size(); ++i) { - int ok = verify(pl->list[i].first, pl, EP, nvar, nparam, p, options); - if (!ok && !options->continue_on_error) - break; - } - - Vector_Free(p); - - return 0; + check_poly_max_data data(EP, pl); + return !check_EP(&data, nvar, nparam, options); } static int optimize(evalue *EP, char **all_vars, unsigned nvar, unsigned nparam, diff --git a/summate.cc b/summate.cc index 1a5b276..fc802cb 100644 --- a/summate.cc +++ b/summate.cc @@ -53,15 +53,12 @@ static int check_poly_sum(const struct check_poly_data *data, int nparam, Value *z, const struct verify_options *options); -struct check_poly_sum_data : public check_poly_data { - Polyhedron **S; - evalue *EP; +struct check_poly_sum_data : public check_EP_data { evalue *sum; - check_poly_sum_data(Value *z, evalue *EP, evalue *sum) : - EP(EP), sum(sum) { - this->z = z; - this->check = check_poly_sum; + check_poly_sum_data(const evalue *EP, evalue *sum) : sum(sum) { + this->EP = EP; + this->cp.check = check_poly_sum; } }; @@ -69,7 +66,7 @@ static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data, evalue *s, const struct verify_options *options) { if (!S) { - evalue *e = evalue_eval(data->EP, data->z+1); + evalue *e = evalue_eval(data->EP, data->cp.z+1); eadd(e, s); evalue_free(e); } else { @@ -77,13 +74,13 @@ static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data, int ok; value_init(LB); value_init(UB); - ok = !(lower_upper_bounds(1+pos, S, data->z, &LB, &UB)); + ok = !(lower_upper_bounds(1+pos, S, data->cp.z, &LB, &UB)); assert(ok); for (; value_le(LB, UB); value_increment(LB, LB)) { - value_assign(data->z[1+pos], LB); + value_assign(data->cp.z[1+pos], LB); sum(S->next, pos+1, data, s, options); } - value_set_si(data->z[1+pos], 0); + value_set_si(data->cp.z[1+pos], 0); value_clear(LB); value_clear(UB); } @@ -93,7 +90,7 @@ static evalue *sum(const check_poly_sum_data *data, const struct verify_options *options) { evalue *s = evalue_zero(); - for (int i = 0; i < data->EP->x.p->size/2; ++i) + for (int i = 0; i < data->n_S; ++i) if (!emptyQ2(data->S[i])) sum(data->S[i], 0, data, s, options); return s; @@ -104,7 +101,7 @@ static int check_poly_sum(const struct check_poly_data *data, const struct verify_options *options) { const check_poly_sum_data *sum_data; - sum_data = static_cast(data); + sum_data = (const check_poly_sum_data *)data; evalue *e, *s; int k; int ok; @@ -123,95 +120,11 @@ static int check_poly_sum(const struct check_poly_data *data, return ok; } -static int verify(Polyhedron *P, evalue *sum, evalue *EP, - unsigned nvar, unsigned nparam, Vector *p, - struct verify_options *options) -{ - Polyhedron *CS; - unsigned MaxRays = options->barvinok->MaxRays; - int error = 0; - - CS = check_poly_context_scan(NULL, &P, P->Dimension, options); - - check_poly_init(P, options); - - if (!(CS && emptyQ2(CS))) { - check_poly_sum_data data(p->p, EP, sum); - data.S = ALLOCN(Polyhedron *, EP->x.p->size/2); - for (int i = 0; i < EP->x.p->size/2; ++i) { - Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]); - data.S[i] = Polyhedron_Scan(A, P, MaxRays & POL_NO_DUAL ? 0 : MaxRays); - } - error = !check_poly(CS, &data, nparam, 0, p->p+1+nvar, options); - for (int i = 0; i < EP->x.p->size/2; ++i) - Domain_Free(data.S[i]); - free(data.S); - } - - if (!options->print_all) - printf("\n"); - - if (CS) { - Domain_Free(CS); - Domain_Free(P); - } - - return error; -} - -/* - * Project on final dim dimensions - */ -Polyhedron *DomainProject(Polyhedron *D, unsigned dim, unsigned MaxRays) -{ - Polyhedron *P; - Polyhedron *R; - - R = Polyhedron_Project(D, dim); - for (P = D->next; P; P = P->next) { - Polyhedron *R2 = Polyhedron_Project(P, dim); - Polyhedron *R3 = DomainUnion(R, R2, MaxRays); - Polyhedron_Free(R2); - Domain_Free(R); - R = R3; - } - return R; -} - static int verify(evalue *EP, evalue *sum, unsigned nvar, unsigned nparam, struct verify_options *options) { - Vector *p; - - p = Vector_Alloc(nvar+nparam+2); - value_set_si(p->p[nvar+nparam+1], 1); - - assert(value_zero_p(EP->d)); - assert(EP->x.p->type == partition); - - Polyhedron *EP_D = EVALUE_DOMAIN(EP->x.p->arr[0]); - Polyhedron *D = Polyhedron_Project(EP_D, nparam); - - for (int i = 1; i < EP->x.p->size/2; ++i) { - Polyhedron *D2 = D; - EP_D = DomainProject(EVALUE_DOMAIN(EP->x.p->arr[2*i]), nparam, - options->barvinok->MaxRays); - D = DomainUnion(EP_D, D, options->barvinok->MaxRays); - Domain_Free(D2); - } - - int error = 0; - - for (Polyhedron *P = D; P; P = P->next) { - error = verify(P, sum, EP, nvar, nparam, p, options); - if (error && !options->continue_on_error) - break; - } - - Domain_Free(D); - Vector_Free(p); - - return error; + check_poly_sum_data data(EP, sum); + return !check_EP(&data, nvar, nparam, options); } int main(int argc, char **argv) diff --git a/verify.c b/verify.c index 336ba88..b1ed8b8 100644 --- a/verify.c +++ b/verify.c @@ -4,6 +4,8 @@ #include #include "verify.h" +#define ALLOCN(type,n) (type*)malloc((n) * sizeof(type)) + /* RANGE : normal range for evalutations (-RANGE -> RANGE) */ #define RANGE 50 @@ -314,3 +316,131 @@ int check_poly(Polyhedron *CS, const struct check_poly_data *data, } return 1; } /* check_poly */ + +static int check_EP_on_poly(Polyhedron *P, + struct check_EP_data *data, + unsigned nvar, unsigned nparam, + struct verify_options *options) +{ + Polyhedron *CS; + unsigned MaxRays = options->barvinok->MaxRays; + int ok = 1; + const evalue *EP = data->EP; + + CS = check_poly_context_scan(NULL, &P, P->Dimension, options); + + check_poly_init(P, options); + + if (!(CS && emptyQ2(CS))) { + int i; + int n_S = 0; + + for (i = 0; i < EP->x.p->size/2; ++i) { + Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]); + for (; A; A = A->next) + ++n_S; + } + + data->n_S = n_S; + data->S = ALLOCN(Polyhedron *, n_S); + n_S = 0; + for (i = 0; i < EP->x.p->size/2; ++i) { + Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]); + for (; A; A = A->next) { + Polyhedron *next = A->next; + A->next = NULL; + data->S[n_S++] = Polyhedron_Scan(A, P, + MaxRays & POL_NO_DUAL ? 0 : MaxRays); + A->next = next; + } + } + ok = check_poly(CS, &data->cp, nparam, 0, data->cp.z+1+nvar, options); + for (i = 0; i < data->n_S; ++i) + Domain_Free(data->S[i]); + free(data->S); + } + + if (!options->print_all) + printf("\n"); + + if (CS) { + Domain_Free(CS); + Domain_Free(P); + } + + return ok; +} + +/* + * Project on final dim dimensions + */ +Polyhedron *DomainProject(Polyhedron *D, unsigned dim, unsigned MaxRays) +{ + Polyhedron *P; + Polyhedron *R; + + R = Polyhedron_Project(D, dim); + for (P = D->next; P; P = P->next) { + Polyhedron *R2 = Polyhedron_Project(P, dim); + Polyhedron *R3 = DomainUnion(R, R2, MaxRays); + Polyhedron_Free(R2); + Domain_Free(R); + R = R3; + } + return R; +} + +static Polyhedron *evalue_parameter_domain(const evalue *e, unsigned nparam, + unsigned MaxRays) +{ + int i; + Polyhedron *U = NULL; + + if (EVALUE_IS_ZERO(*e)) + return Universe_Polyhedron(0); + + assert(value_zero_p(e->d)); + assert(e->x.p->type == partition); + assert(e->x.p->size >= 2); + + for (i = 0; i < e->x.p->size/2; ++i) { + Polyhedron *D = EVALUE_DOMAIN(e->x.p->arr[2*i]); + Polyhedron *P = DomainProject(D, nparam, MaxRays); + if (!U) { + U = P; + } else { + Polyhedron *T = U; + U = DomainUnion(U, P, MaxRays); + Domain_Free(P); + Domain_Free(T); + } + } + return U; +} + +int check_EP(struct check_EP_data *data, unsigned nvar, unsigned nparam, + struct verify_options *options) +{ + Vector *p; + int i; + int ok = 1; + Polyhedron *D, *P; + + p = Vector_Alloc(nvar+nparam+2); + value_set_si(p->p[nvar+nparam+1], 1); + + data->cp.z = p->p; + + D = evalue_parameter_domain(data->EP, nparam, options->barvinok->MaxRays); + + for (P = D; P; P = P->next) { + ok = check_EP_on_poly(P, data, nvar, nparam, options); + if (!ok && !options->continue_on_error) + break; + } + + Domain_Free(D); + Vector_Free(p); + + return ok; +} diff --git a/verify.h b/verify.h index 390b8b8..2e24dcc 100644 --- a/verify.h +++ b/verify.h @@ -50,6 +50,17 @@ int check_poly(Polyhedron *CS, const struct check_poly_data *data, int nparam, int pos, Value *z, const struct verify_options *options); +struct check_EP_data { + struct check_poly_data cp; + int n_S; + Polyhedron **S; + + const evalue *EP; +}; + +int check_EP(struct check_EP_data *data, unsigned nvar, unsigned nparam, + struct verify_options *options); + #if defined(__cplusplus) } #endif -- 2.11.4.GIT