From 76e9ef18112fc4cdc37e432dd7bf6e723ebe7bd4 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 5 Jan 2007 16:31:42 +0100 Subject: [PATCH] barvinok_enumerate: integrate verif_ehrhart --- Makefile.am | 14 +- barvinok_enumerate.cc | 250 ++++++++++++++++++++++++++++++++++-- verify_main.cc | 344 -------------------------------------------------- 3 files changed, 245 insertions(+), 363 deletions(-) delete mode 100644 verify_main.cc diff --git a/Makefile.am b/Makefile.am index 004812b..20b91d3 100644 --- a/Makefile.am +++ b/Makefile.am @@ -9,7 +9,7 @@ AM_LDFLAGS = -Llib lib_LTLIBRARIES = libbarvinok.la noinst_PROGRAMS = test barvinok_count randomtest barvinok_enumerate \ barvinok_ehrhart \ - verif_ehrhart barvinok_enumerate_e \ + barvinok_enumerate_e \ remove_redundant_equalities \ barvinok_union \ @bv_extra_programs@ @@ -94,7 +94,12 @@ BEEO_SOURCES = omega/Exit.cc omega/convert.cc else BEEO_SOURCES = endif -barvinok_enumerate_SOURCES = barvinok_enumerate.cc +barvinok_enumerate_SOURCES = \ + barvinok_enumerate.cc \ + verify.h \ + verify.c \ + verif_ehrhart.h \ + verif_ehrhart.c barvinok_enumerate_e_SOURCES = \ verify.h \ verify.c \ @@ -103,7 +108,6 @@ barvinok_enumerate_e_SOURCES = \ barvinok_enumerate_e_CPPFLAGS = @OMEGA_CPPFLAGS@ $(AM_CPPFLAGS) barvinok_enumerate_e_LDFLAGS = @OMEGA_LDFLAGS@ @LDFLAGS@ barvinok_enumerate_e_LDADD = @OMEGA_LIBS@ libbarvinok.la -verif_ehrhart_SOURCES = verif_ehrhart.c verify_main.cc verif_ehrhart.h 4coins_SOURCES = 4coins.cc if HAVE_CDDLIB POLYSIGN = polysign_cddf.cc polysign_cdd.cc @@ -181,14 +185,14 @@ check-series: @for i in $(top_srcdir)/tests/ehrhart/*; do \ if test -f $$i; then \ echo $$i; \ - ./verif_ehrhart --series < $$i; \ + ./barvinok_enumerate --verify --series < $$i; \ fi \ done check: @for i in $(top_srcdir)/tests/ehrhart/*; do \ if test -f $$i; then \ echo $$i; \ - ./verif_ehrhart < $$i; \ + ./barvinok_enumerate --verify < $$i; \ fi \ done @for dir in $(BEE_TESTDIRS); do \ diff --git a/barvinok_enumerate.cc b/barvinok_enumerate.cc index d8c8c25..ea795f7 100644 --- a/barvinok_enumerate.cc +++ b/barvinok_enumerate.cc @@ -4,6 +4,8 @@ #include #include #include "argp.h" +#include "verify.h" +#include "verif_ehrhart.h" /* The input of this example program is the same as that of testehrhart * in the PolyLib distribution, i.e., a polytope in combined @@ -18,6 +20,7 @@ struct argp_option argp_options[] = { { "size", 'S' }, { "series", 's', 0, 0, "compute rational generating function" }, { "explicit", 'e', 0, 0, "convert rgf to psp" }, + { "verbose", 'v' }, { 0 } }; @@ -28,20 +31,24 @@ struct arguments { int size; int series; int function; + int verbose; + struct verify_options verify; }; -error_t parse_opt(int key, char *arg, struct argp_state *state) +static error_t parse_opt(int key, char *arg, struct argp_state *state) { struct arguments *options = (struct arguments*) state->input; switch (key) { case ARGP_KEY_INIT: state->child_inputs[0] = options->barvinok; + state->child_inputs[1] = &options->verify; options->convert = 0; options->floor = 0; options->size = 0; options->series = 0; options->function = 0; + options->verbose = 0; break; case 'c': options->convert = 1; @@ -58,21 +65,212 @@ error_t parse_opt(int key, char *arg, struct argp_state *state) case 's': options->series = 1; break; + case 'v': + options->verbose = 1; + break; default: return ARGP_ERR_UNKNOWN; } return 0; } +static int check_series(Polyhedron *S, Polyhedron *CS, gen_fun *gf, + int nparam, int pos, Value *z, int print_all) +{ + int k; + Value c, tmp; + Value LB, UB; + + value_init(c); + value_init(tmp); + value_init(LB); + value_init(UB); + + if (pos == nparam) { + /* Computes the coefficient */ + gf->coefficient(&z[S->Dimension-nparam+1], &c); + + /* if c=0 we may be out of context. */ + /* scanning is useless in this case*/ + + if (print_all) { + printf("EP( "); + value_print(stdout,VALUE_FMT,z[S->Dimension-nparam+1]); + for(k=S->Dimension-nparam+2;k<=S->Dimension;++k) { + printf(", "); + value_print(stdout,VALUE_FMT,z[k]); + } + printf(" ) = "); + value_print(stdout,VALUE_FMT,c); + printf(" "); + } + + /* Manually count the number of points */ + count_points(1,S,z,&tmp); + if (print_all) { + printf(", count = "); + value_print(stdout, P_VALUE_FMT, tmp); + printf(". "); + } + + if (value_ne(tmp,c)) { + printf("\n"); + fflush(stdout); + fprintf(stderr,"Error !\n"); + fprintf(stderr,"EP( "); + value_print(stderr,VALUE_FMT,z[S->Dimension-nparam+1]); + for (k=S->Dimension-nparam+2;k<=S->Dimension;++k) { + fprintf(stderr,", "); + value_print(stderr,VALUE_FMT,z[k]); + } + fprintf(stderr," ) should be "); + value_print(stderr,VALUE_FMT,tmp); + fprintf(stderr,", while EP eval gives "); + value_print(stderr,VALUE_FMT,c); + fprintf(stderr,".\n"); +#ifndef DONT_BREAK_ON_ERROR + value_clear(c); value_clear(tmp); + return 0; +#endif + } else if (print_all) + printf("OK.\n"); + } else { + int ok = + !(lower_upper_bounds(1+pos, CS, &z[S->Dimension-nparam], &LB, &UB)); + assert(ok); + for (value_assign(tmp,LB); value_le(tmp,UB); value_increment(tmp,tmp)) { + if (!print_all) { + k = VALUE_TO_INT(tmp); + if(!pos && !(k%st)) { + printf("o"); + fflush(stdout); + } + } + value_assign(z[pos+S->Dimension-nparam+1],tmp); + if (!check_series(S, CS->next, gf, nparam, pos+1, z, print_all)) { + value_clear(c); value_clear(tmp); + value_clear(LB); + value_clear(UB); + return(0); + } + } + value_set_si(z[pos+S->Dimension-nparam+1],0); + } + + value_clear(c); + value_clear(tmp); + value_clear(LB); + value_clear(UB); + return 1; +} + +static int verify(Polyhedron *P, Polyhedron **C, Enumeration *en, gen_fun *gf, + arguments *options) +{ + Polyhedron *CC, *PP, *CS, *S, *U; + Matrix *C1, *MM; + Vector *p; + int result = 0; + + /******* Compute true context *******/ + CC = align_context(*C, P->Dimension, options->barvinok->MaxRays); + PP = DomainIntersection(P, CC, options->barvinok->MaxRays); + Domain_Free(CC); + C1 = Matrix_Alloc((*C)->Dimension+1, P->Dimension+1); + + for (int i = 0; i < C1->NbRows; i++) + for (int j = 0; j < C1->NbColumns; j++) + if (i == j-P->Dimension+(*C)->Dimension) + value_set_si(C1->p[i][j], 1); + else + value_set_si(C1->p[i][j], 0); + CC = Polyhedron_Image(PP, C1, options->barvinok->MaxRays); + Matrix_Free(C1); + Domain_Free(PP); + Domain_Free(*C); + *C = CC; + + /* Intersect context with range */ + if ((*C)->Dimension > 0) { + MM = Matrix_Alloc(2*(*C)->Dimension, (*C)->Dimension+2); + for (int i = 0; i < (*C)->Dimension; ++i) { + value_set_si(MM->p[2*i][0], 1); + value_set_si(MM->p[2*i][1+i], 1); + value_set_si(MM->p[2*i][1+(*C)->Dimension], -options->verify.m); + value_set_si(MM->p[2*i+1][0], 1); + value_set_si(MM->p[2*i+1][1+i], -1); + value_set_si(MM->p[2*i+1][1+(*C)->Dimension], options->verify.M); + } + CC = AddConstraints(MM->p[0], 2*(*C)->Dimension, *C, + options->barvinok->MaxRays); + U = Universe_Polyhedron(0); + CS = Polyhedron_Scan(CC, U, options->barvinok->MaxRays); + Polyhedron_Free(U); + Polyhedron_Free(CC); + Matrix_Free(MM); + } else + CS = NULL; + + p = Vector_Alloc(P->Dimension+2); + value_set_si(p->p[P->Dimension+1], 1); + + /* S = scanning list of polyhedra */ + S = Polyhedron_Scan(P, *C, options->barvinok->MaxRays); + + if (!options->verify.print_all) + if ((*C)->Dimension > 0) { + int d = options->verify.M - options->verify.m; + if (d > 80) + st = 1+d/80; + else + st=1; + for (int i = options->verify.m; i <= options->verify.M; i += st) + printf("."); + printf( "\r" ); + fflush(stdout); + } + + /******* CHECK NOW *********/ + if (S) { + if (!options->series || options->function) { + if (!check_poly(S, CS, en, (*C)->Dimension, 0, p->p, + options->verify.print_all)) + result = -1; + } else { + if (!check_series(S, CS, gf, (*C)->Dimension, 0, p->p, + options->verify.print_all)) + result = -1; + } + Domain_Free(S); + } + + if (result == -1) + fprintf(stderr,"Check failed !\n"); + + if (!options->verify.print_all) + printf( "\n" ); + + Vector_Free(p); + if (CS) + Domain_Free(CS); + + return result; +} + int main(int argc, char **argv) { Polyhedron *A, *C; Matrix *M; - evalue *EP; + evalue *EP = NULL; + Enumeration *en = NULL; + gen_fun *gf = NULL; char **param_name; + int print_solution = 1; + int result = 0; struct arguments options; static struct argp_child argp_children[] = { - { &barvinok_argp, 0, 0, 0 }, + { &barvinok_argp, 0, 0, 0 }, + { &verify_argp, 0, "verification", 1 }, { 0 } }; static struct argp argp = { argp_options, parse_opt, 0, 0, argp_children }; @@ -87,25 +285,34 @@ int main(int argc, char **argv) M = Matrix_Read(); C = Constraints2Polyhedron(M, bv_options->MaxRays); Matrix_Free(M); - Polyhedron_Print(stdout, P_VALUE_FMT, A); - Polyhedron_Print(stdout, P_VALUE_FMT, C); param_name = Read_ParamNames(stdin, C->Dimension); + if (options.verify.verify) { + verify_options_set_range(&options.verify, A); + if (!options.verbose) + print_solution = 0; + } + + if (print_solution) { + Polyhedron_Print(stdout, P_VALUE_FMT, A); + Polyhedron_Print(stdout, P_VALUE_FMT, C); + } + if (options.series) { - gen_fun *gf; gf = barvinok_series_with_options(A, C, bv_options); - gf->print(std::cout, C->Dimension, param_name); - puts(""); + if (print_solution) { + gf->print(std::cout, C->Dimension, param_name); + puts(""); + } if (options.function) { EP = *gf; - print_evalue(stdout, EP, param_name); - free_evalue_refs(EP); - free(EP); + if (print_solution) + print_evalue(stdout, EP, param_name); } - delete gf; } else { EP = barvinok_enumerate_with_options(A, C, bv_options); - print_evalue(stdout, EP, param_name); + if (print_solution) + print_evalue(stdout, EP, param_name); if (options.size) printf("\nSize: %d\n", evalue_size(EP)); if (options.floor) { @@ -118,6 +325,21 @@ int main(int argc, char **argv) if (options.size) printf("\nSize: %d\n", evalue_size(EP)); } + } + + if (options.verify.verify) { + if (EP) { + en = partition2enumeration(EP); + EP = NULL; + } + result = verify(A, &C, en, gf, &options); + } + + if (en) + Enumeration_Free(en); + if (gf) + delete gf; + if (EP) { free_evalue_refs(EP); free(EP); } @@ -126,5 +348,5 @@ int main(int argc, char **argv) Polyhedron_Free(A); Polyhedron_Free(C); free(bv_options); - return 0; + return result; } diff --git a/verify_main.cc b/verify_main.cc deleted file mode 100644 index a3e8164..0000000 --- a/verify_main.cc +++ /dev/null @@ -1,344 +0,0 @@ -#include -#include -#include -#include -#include - -#include "verif_ehrhart.h" - -#ifdef HAVE_GROWING_CHERNIKOVA -#define MAXRAYS 0 -#else -#define MAXRAYS 600 -#endif - -#include "config.h" -#ifndef HAVE_GETOPT_H -#define getopt_long(a,b,c,d,e) getopt(a,b,c) -#else -#include -struct option options[] = { - { "explicit", no_argument, 0, 'e' }, - { "series", no_argument, 0, 's' }, - { "print-all", no_argument, 0, 'A' }, - { "verbose", no_argument, 0, 'v' }, - { "version", no_argument, 0, 'V' }, - { 0, 0, 0, 0 } -}; -#endif - -/* RANGE : normal range for evalutations (-RANGE -> RANGE) */ -#define RANGE 50 - -/* SRANGE : small range for evalutations */ -#define SRANGE 15 - -/* if dimension >= BIDDIM, use SRANGE */ -#define BIGDIM 5 - -/* VSRANGE : very small range for evalutations */ -#define VSRANGE 5 - -/* if dimension >= VBIDDIM, use VSRANGE */ -#define VBIGDIM 8 - -int check_series(Polyhedron *S, Polyhedron *CS, gen_fun *gf, - int nparam, int pos, Value *z, int print_all) -{ - int k; - Value c, tmp; - Value LB, UB; - - value_init(c); - value_init(tmp); - value_init(LB); - value_init(UB); - - if(pos == nparam) { - /* Computes the coefficient */ - gf->coefficient(&z[S->Dimension-nparam+1], &c); - - /* if c=0 we may be out of context. */ - /* scanning is useless in this case*/ - - if (print_all) { - printf("EP( "); - value_print(stdout,VALUE_FMT,z[S->Dimension-nparam+1]); - for(k=S->Dimension-nparam+2;k<=S->Dimension;++k) { - printf(", "); - value_print(stdout,VALUE_FMT,z[k]); - } - printf(" ) = "); - value_print(stdout,VALUE_FMT,c); - printf(" "); - } - /* Manually count the number of points */ - count_points(1,S,z,&tmp); - if (print_all) { - printf(", count = "); - value_print(stdout, P_VALUE_FMT, tmp); - printf(". "); - } - - if(value_ne(tmp,c)) { - printf("\n"); - fflush(stdout); - fprintf(stderr,"Error !\n"); - fprintf(stderr,"EP( "); - value_print(stderr,VALUE_FMT,z[S->Dimension-nparam+1]); - for(k=S->Dimension-nparam+2;k<=S->Dimension;++k) { - fprintf(stderr,", "); - value_print(stderr,VALUE_FMT,z[k]); - } - fprintf(stderr," ) should be "); - value_print(stderr,VALUE_FMT,tmp); - fprintf(stderr,", while EP eval gives "); - value_print(stderr,VALUE_FMT,c); - fprintf(stderr,".\n"); -#ifndef DONT_BREAK_ON_ERROR - value_clear(c); value_clear(tmp); - return 0; -#endif - } else if (print_all) - printf("OK.\n"); - } else { - int ok = - !(lower_upper_bounds(1+pos, CS, &z[S->Dimension-nparam], &LB, &UB)); - assert(ok); - for(value_assign(tmp,LB); value_le(tmp,UB); value_increment(tmp,tmp)) { - if (!print_all) { - k = VALUE_TO_INT(tmp); - if(!pos && !(k%st)) { - printf("o"); - fflush(stdout); - } - } - value_assign(z[pos+S->Dimension-nparam+1],tmp); - if (!check_series(S, CS->next, gf, nparam, pos+1, z, print_all)) { - value_clear(c); value_clear(tmp); - value_clear(LB); - value_clear(UB); - return(0); - } - } - value_set_si(z[pos+S->Dimension-nparam+1],0); - } - - value_clear(c); - value_clear(tmp); - value_clear(LB); - value_clear(UB); - return 1; -} - -int main(int argc,char *argv[]) { - - Matrix *C1, *P1, *MM; - Polyhedron *C, *P, *S, *CS, *U; - Polyhedron *CC, *PP; - Enumeration *en = NULL; - Value *p, tmp; - Value Min, Max; - int i,j; - int m = INT_MAX, M = INT_MIN, r; - int c, ind = 0; - int series = 0; - int verbose = 0; - int function = 0; - int result = 0; - int print_all = 0; - - while ((c = getopt_long(argc, argv, "m:M:r:sveVA", options, &ind)) != -1) { - switch (c) { - case 'A': - print_all = 1; - break; - case 'e': - function = 1; - break; - case 's': - series = 1; - break; - case 'v': - verbose = 1; - break; - case 'm': - m = atoi(optarg); - break; - case 'M': - M = atoi(optarg); - break; - case 'r': - M = atoi(optarg); - m = -M; - break; - case 'V': - printf(barvinok_version()); - exit(0); - break; - } - } - -/******* Read the input *********/ - P1 = Matrix_Read(); - C1 = Matrix_Read(); - - if(C1->NbColumns < 2) { - fprintf(stderr,"Not enough parameters !\n"); - exit(0); - } - - P = Constraints2Polyhedron(P1,MAXRAYS); - C = Constraints2Polyhedron(C1,MAXRAYS); - params = Read_ParamNames(stdin, C->Dimension); - Matrix_Free(C1); - Matrix_Free(P1); - - /******* Read the options: initialize Min and Max ********/ - if(P->Dimension >= VBIGDIM) - r = VSRANGE; - else if(P->Dimension >= BIGDIM) - r = SRANGE; - else - r = RANGE; - if (M == INT_MIN) - M = r; - if (m == INT_MAX) - m = -r; - - - if(m > M) { - fprintf(stderr,"Nothing to do: Min > Max !\n"); - return(0); - } - value_init(Min); - value_init(Max); - value_set_si(Min,m); - value_set_si(Max,M); - value_init(tmp); - - /******* Compute true context *******/ - CC = align_context(C,P->Dimension,MAXRAYS); - PP = DomainIntersection(P,CC,MAXRAYS); - Domain_Free(CC); - C1 = Matrix_Alloc(C->Dimension+1,P->Dimension+1); - - for(i=0;iNbRows;i++) - for(j=0;jNbColumns;j++) - if(i==j-P->Dimension+C->Dimension) - value_set_si(C1->p[i][j],1); - else - value_set_si(C1->p[i][j],0); - CC = Polyhedron_Image(PP,C1,MAXRAYS); - Matrix_Free(C1); - Domain_Free(PP); - Domain_Free(C); - C = CC; - - /* Intersect context with range */ - if(C->Dimension > 0) { - MM = Matrix_Alloc(2*C->Dimension, C->Dimension+2); - for (i = 0; i < C->Dimension; ++i) { - value_set_si(MM->p[2*i][0], 1); - value_set_si(MM->p[2*i][1+i], 1); - value_set_si(MM->p[2*i][1+C->Dimension], -m); - value_set_si(MM->p[2*i+1][0], 1); - value_set_si(MM->p[2*i+1][1+i], -1); - value_set_si(MM->p[2*i+1][1+C->Dimension], M); - } - CC = AddConstraints(MM->p[0], 2*C->Dimension, C, MAXRAYS); - U = Universe_Polyhedron(0); - CS = Polyhedron_Scan(CC, U, MAXRAYS); - Polyhedron_Free(U); - Polyhedron_Free(CC); - Matrix_Free(MM); - } else - CS = NULL; - - gen_fun *gf = 0; - - /******* Compute EP *********/ - if (!series) { - en = barvinok_enumerate(P,C,MAXRAYS); - if (verbose) - Enumeration_Print(stdout, en, params); - } else { - evalue *EP; - gf = barvinok_series(P, C, MAXRAYS); - if (verbose) { - gf->print(std::cout, C->Dimension, params); - puts(""); - } - if (function) { - EP = *gf; - en = partition2enumeration(EP); - if (verbose) - Enumeration_Print(stdout, en, params); - } - } - - /******* Initializations for check *********/ - p = (Value *)malloc(sizeof(Value) * (P->Dimension+2)); - for(i=0;i<=P->Dimension;i++) { - value_init(p[i]); - value_set_si(p[i],0); - } - value_init(p[i]); - value_set_si(p[i],1); - - /* S = scanning list of polyhedra */ - S = Polyhedron_Scan(P,C,MAXRAYS); - - if (!print_all) - if (C->Dimension > 0) { - value_subtract(tmp,Max,Min); - if (VALUE_TO_INT(tmp) > 80) - st = 1+(VALUE_TO_INT(tmp))/80; - else - st=1; - for(i=VALUE_TO_INT(Min);i<=VALUE_TO_INT(Max);i+=st) - printf("."); - printf( "\r" ); - fflush(stdout); - } - - /******* CHECK NOW *********/ - if(S) { - if (!series || function) { - if (!check_poly(S, CS,en,C->Dimension,0,p, print_all)) - result = -1; - } else { - if (!check_series(S, CS,gf,C->Dimension,0,p, print_all)) - result = -1; - } - Domain_Free(S); - } - - if (result == -1) - fprintf(stderr,"Check failed !\n"); - - if (!print_all) - printf( "\n" ); - - if (en) - Enumeration_Free(en); - if (gf) - delete gf; - - for(i=0;i<=(P->Dimension+1);i++) - value_clear(p[i]); - free(p); - value_clear(Min); - value_clear(Max); - value_clear(tmp); - Free_ParamNames(params, C->Dimension); - Domain_Free(P); - Domain_Free(C); - if (CS) - Domain_Free(CS); - return result; -} /* main */ - - - - -- 2.11.4.GIT