From a49c6a32245acc6f42bc72064df81c552cae5464 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Thu, 11 Oct 2007 16:57:28 +0200 Subject: [PATCH] barvinok_enumerate: use verify infrastructure for verifying generating functions --- Makefile.am | 6 +- barvinok_enumerate.cc | 165 ++------------------------------------------------ skewed_genfun.cc | 67 ++++++++++++++++++++ skewed_genfun.h | 39 ++++++++++++ verify_series.cc | 54 +++++++++++++++++ verify_series.h | 7 +++ 6 files changed, 176 insertions(+), 162 deletions(-) create mode 100644 skewed_genfun.cc create mode 100644 skewed_genfun.h create mode 100644 verify_series.cc create mode 100644 verify_series.h diff --git a/Makefile.am b/Makefile.am index f1f2f4c..64a04dd 100644 --- a/Makefile.am +++ b/Makefile.am @@ -175,10 +175,14 @@ barvinok_enumerate_SOURCES = \ evalue_convert.cc \ evalue_convert.h \ $(FDSTREAM) \ + skewed_genfun.cc \ + skewed_genfun.h \ verify.h \ verify.c \ verif_ehrhart.h \ - verif_ehrhart.c + verif_ehrhart.c \ + verify_series.h \ + verify_series.cc EXTRA_barvinok_enumerate_SOURCES = fdstream.cc fdstream.h barvinok_enumerate_e_SOURCES = \ barvinok_enumerate_e.cc \ diff --git a/barvinok_enumerate.cc b/barvinok_enumerate.cc index f7627b7..4a1c992 100644 --- a/barvinok_enumerate.cc +++ b/barvinok_enumerate.cc @@ -8,9 +8,11 @@ #include "progname.h" #include "verify.h" #include "verif_ehrhart.h" +#include "verify_series.h" #include "remove_equalities.h" #include "evalue_convert.h" #include "conversion.h" +#include "skewed_genfun.h" #undef CS /* for Solaris 10 */ @@ -81,166 +83,6 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) return 0; } -struct skewed_gen_fun { - gen_fun *gf; - /* maps original space to space in which gf is defined */ - Matrix *T; - /* equalities in the original space that need to be satisfied for - * gf to be valid - */ - Matrix *eq; - /* divisibilities in the original space that need to be satisfied for - * gf to be valid - */ - Matrix *div; - - skewed_gen_fun(gen_fun *gf, Matrix *T, Matrix *eq, Matrix *div) : - gf(gf), T(T), eq(eq), div(div) {} - ~skewed_gen_fun() { - if (T) - Matrix_Free(T); - if (eq) - Matrix_Free(eq); - if (div) - Matrix_Free(div); - delete gf; - } - - void print(std::ostream& os, unsigned int nparam, char **param_name) const; - operator evalue *() const { - assert(T == NULL && eq == NULL); /* other cases not supported for now */ - return *gf; - } - void coefficient(Value* params, Value* c, barvinok_options *options) const; -}; - -void skewed_gen_fun::print(std::ostream& os, unsigned int nparam, - char **param_name) const -{ - mat_ZZ m; - if (T) { - os << "T:" << endl; - matrix2zz(T, m, T->NbRows, T->NbColumns); - os << m << endl; - } - if (eq) { - os << "eq:" << endl; - matrix2zz(eq, m, eq->NbRows, eq->NbColumns); - os << m << endl; - } - if (div) { - os << "div:" << endl; - matrix2zz(div, m, div->NbRows, div->NbColumns); - os << m << endl; - } - gf->print(os, nparam, param_name); -} - -void skewed_gen_fun::coefficient(Value* params, Value* c, - barvinok_options *options) const -{ - if (eq) { - for (int i = 0; i < eq->NbRows; ++i) { - Inner_Product(eq->p[i]+1, params, eq->NbColumns-2, eq->p[i]); - if (value_notzero_p(eq->p[i][0])) { - value_set_si(*c, 0); - return; - } - } - } - if (div) { - Value tmp; - value_init(tmp); - for (int i = 0; i < div->NbRows; ++i) { - Inner_Product(div->p[i], params, div->NbColumns-1, &tmp); - if (!mpz_divisible_p(tmp, div->p[i][div->NbColumns-1])) { - value_set_si(*c, 0); - return; - } - } - value_clear(tmp); - } - - ZZ coeff; - if (!T) - coeff = gf->coefficient(params, options); - else { - Vector *p2 = Vector_Alloc(T->NbRows); - Matrix_Vector_Product(T, params, p2->p); - if (value_notone_p(p2->p[T->NbRows-1])) - Vector_AntiScale(p2->p, p2->p, p2->p[T->NbRows-1], T->NbRows); - coeff = gf->coefficient(p2->p, options); - Vector_Free(p2); - } - - zz2value(coeff, *c); -} - -static int check_series(Polyhedron *S, Polyhedron *CS, skewed_gen_fun *gf, - int nparam, int pos, Value *z, verify_options *options) -{ - int k; - Value c, tmp, one; - Value LB, UB; - - value_init(c); - value_init(tmp); - value_init(LB); - value_init(UB); - value_init(one); - value_set_si(one, 1); - - if (pos == nparam) { - /* Computes the coefficient */ - gf->coefficient(&z[S->Dimension-nparam+1], &c, options->barvinok); - - /* if c=0 we may be out of context. */ - /* scanning is useless in this case*/ - - /* Manually count the number of points */ - count_points(1,S,z,&tmp); - - check_poly_print(value_eq(tmp, c), nparam, z+1+S->Dimension-nparam, - tmp, one, c, one, - "EP", "count", "EP eval", options); - - if (value_ne(tmp,c)) { - if (!options->continue_on_error) { - value_clear(c); value_clear(tmp); - return 0; - } - } - } 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 (!options->print_all) { - k = VALUE_TO_INT(tmp); - if(!pos && !(k % options->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, options)) { - 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(one); - value_clear(LB); - value_clear(UB); - return 1; -} - static int verify(Polyhedron *P, Polyhedron *C, evalue *EP, skewed_gen_fun *gf, arguments *options) { @@ -265,7 +107,8 @@ static int verify(Polyhedron *P, Polyhedron *C, evalue *EP, skewed_gen_fun *gf, &options->verify)) result = -1; } else { - if (!check_series(S, CS, gf, C->Dimension, 0, p->p, &options->verify)) + if (!check_poly_gf(S, CS, gf, 0, C->Dimension, 0, p->p, + &options->verify)) result = -1; } Domain_Free(S); diff --git a/skewed_genfun.cc b/skewed_genfun.cc new file mode 100644 index 0000000..6af5923 --- /dev/null +++ b/skewed_genfun.cc @@ -0,0 +1,67 @@ +#include +#include "conversion.h" +#include "skewed_genfun.h" + +using std::endl; + +void skewed_gen_fun::print(std::ostream& os, unsigned int nparam, + char **param_name) const +{ + mat_ZZ m; + if (T) { + os << "T:" << endl; + matrix2zz(T, m, T->NbRows, T->NbColumns); + os << m << endl; + } + if (eq) { + os << "eq:" << endl; + matrix2zz(eq, m, eq->NbRows, eq->NbColumns); + os << m << endl; + } + if (div) { + os << "div:" << endl; + matrix2zz(div, m, div->NbRows, div->NbColumns); + os << m << endl; + } + gf->print(os, nparam, param_name); +} + +void skewed_gen_fun::coefficient(Value* params, Value* c, + barvinok_options *options) const +{ + if (eq) { + for (int i = 0; i < eq->NbRows; ++i) { + Inner_Product(eq->p[i]+1, params, eq->NbColumns-2, eq->p[i]); + if (value_notzero_p(eq->p[i][0])) { + value_set_si(*c, 0); + return; + } + } + } + if (div) { + Value tmp; + value_init(tmp); + for (int i = 0; i < div->NbRows; ++i) { + Inner_Product(div->p[i], params, div->NbColumns-1, &tmp); + if (!mpz_divisible_p(tmp, div->p[i][div->NbColumns-1])) { + value_set_si(*c, 0); + return; + } + } + value_clear(tmp); + } + + ZZ coeff; + if (!T) + coeff = gf->coefficient(params, options); + else { + Vector *p2 = Vector_Alloc(T->NbRows); + Matrix_Vector_Product(T, params, p2->p); + if (value_notone_p(p2->p[T->NbRows-1])) + Vector_AntiScale(p2->p, p2->p, p2->p[T->NbRows-1], T->NbRows); + coeff = gf->coefficient(p2->p, options); + Vector_Free(p2); + } + + zz2value(coeff, *c); +} diff --git a/skewed_genfun.h b/skewed_genfun.h new file mode 100644 index 0000000..33de881 --- /dev/null +++ b/skewed_genfun.h @@ -0,0 +1,39 @@ +#ifndef SKEWED_GENFUN_H +#define SKEWED_GENFUN_H + +#include + +struct skewed_gen_fun { + gen_fun *gf; + /* maps original space to space in which gf is defined */ + Matrix *T; + /* equalities in the original space that need to be satisfied for + * gf to be valid + */ + Matrix *eq; + /* divisibilities in the original space that need to be satisfied for + * gf to be valid + */ + Matrix *div; + + skewed_gen_fun(gen_fun *gf, Matrix *T, Matrix *eq, Matrix *div) : + gf(gf), T(T), eq(eq), div(div) {} + ~skewed_gen_fun() { + if (T) + Matrix_Free(T); + if (eq) + Matrix_Free(eq); + if (div) + Matrix_Free(div); + delete gf; + } + + void print(std::ostream& os, unsigned int nparam, char **param_name) const; + operator evalue *() const { + assert(T == NULL && eq == NULL); /* other cases not supported for now */ + return *gf; + } + void coefficient(Value* params, Value* c, barvinok_options *options) const; +}; + +#endif diff --git a/verify_series.cc b/verify_series.cc new file mode 100644 index 0000000..8a0c067 --- /dev/null +++ b/verify_series.cc @@ -0,0 +1,54 @@ +#include +#include "skewed_genfun.h" +#include "verify_series.h" + +struct check_poly_gf_data { + struct check_poly_data cp; + Polyhedron *S; + const skewed_gen_fun *gf; + int exist; +}; + +static int cp_gf(const struct check_poly_data *data, int nparam, Value *z, + const struct verify_options *options) +{ + int k; + Value c, tmp, one; + struct check_poly_gf_data* gf_data = (struct check_poly_gf_data*) data; + const skewed_gen_fun *gf = gf_data->gf; + int exist = gf_data->exist; + Polyhedron *S = gf_data->S; + + value_init(c); + value_init(tmp); + value_init(one); + value_set_si(one, 1); + + /* Computes the coefficient */ + gf->coefficient(z, &c, options->barvinok); + + /* Manually count the number of points */ + count_points_e(1, S, exist, nparam, data->z, &tmp); + + check_poly_print(value_eq(tmp, c), nparam, z, tmp, one, c, one, + "EP", "count", "EP eval", options); + + value_clear(c); + value_clear(tmp); + value_clear(one); + return 1; +} + +int check_poly_gf(Polyhedron *S, Polyhedron *CS, skewed_gen_fun *gf, + int exist, int nparam, int pos, Value *z, + const struct verify_options *options) +{ + struct check_poly_gf_data data; + data.cp.z = z; + data.cp.check = cp_gf; + data.S = S; + data.gf = gf; + data.exist = exist; + return check_poly(CS, &data.cp, nparam, pos, z+S->Dimension-nparam+1, + options); +} diff --git a/verify_series.h b/verify_series.h new file mode 100644 index 0000000..78f6d5a --- /dev/null +++ b/verify_series.h @@ -0,0 +1,7 @@ +#include +#include "skewed_genfun.h" +#include "verify.h" + +int check_poly_gf(Polyhedron *S, Polyhedron *CS, skewed_gen_fun *gf, + int exist, int nparam, int pos, Value *z, + const struct verify_options *options); -- 2.11.4.GIT