1#include <assert.h> 2#include <isl/stream.h> 3#include <isl_polynomial_private.h> 4#include <isl_scan.h> 5#include <isl/options.h> 6 7struct bound_options { 8 struct isl_options *isl; 9 unsigned verify; 10 int print_all; 11 int continue_on_error; 12}; 13 14ISL_ARGS_START(struct bound_options, bound_options_args) 15ISL_ARG_CHILD(struct bound_options, isl, "isl", &isl_options_args, 16 "isl options") 17ISL_ARG_BOOL(struct bound_options, verify, 'T', "verify", 0, NULL) 18ISL_ARG_BOOL(struct bound_options, print_all, 'A', "print-all", 0, NULL) 19ISL_ARG_BOOL(struct bound_options, continue_on_error, '\0', "continue-on-error", 0, NULL) 20ISL_ARGS_END 21 22ISL_ARG_DEF(bound_options, struct bound_options, bound_options_args) 23 24static __isl_give isl_set *set_bounds(__isl_take isl_set *set) 25{ 26 unsigned nparam; 27 int i, r; 28 isl_point *pt, *pt2; 29 isl_set *box; 30 31 nparam = isl_set_dim(set, isl_dim_param); 32 r = nparam >= 8 ? 5 : nparam >= 5 ? 15 : 50; 33 34 pt = isl_set_sample_point(isl_set_copy(set)); 35 pt2 = isl_point_copy(pt); 36 37 for (i = 0; i < nparam; ++i) { 38 pt = isl_point_add_ui(pt, isl_dim_param, i, r); 39 pt2 = isl_point_sub_ui(pt2, isl_dim_param, i, r); 40 } 41 42 box = isl_set_box_from_points(pt, pt2); 43 44 return isl_set_intersect(set, box); 45} 46 47struct verify_point_bound { 48 struct bound_options *options; 49 int stride; 50 int n; 51 int exact; 52 int error; 53 54 isl_pw_qpolynomial_fold *pwf; 55 isl_pw_qpolynomial_fold *bound; 56}; 57 58static int verify_point(__isl_take isl_point *pnt, void *user) 59{ 60 int i; 61 unsigned nvar; 62 unsigned nparam; 63 struct verify_point_bound *vpb = (struct verify_point_bound *) user; 64 isl_int t; 65 isl_ctx *ctx; 66 isl_pw_qpolynomial_fold *pwf; 67 isl_qpolynomial *bound = NULL; 68 isl_qpolynomial *opt = NULL; 69 isl_set *dom = NULL; 70 isl_printer *p; 71 const char *minmax; 72 int bounded; 73 int sign; 74 int ok; 75 FILE *out = vpb->options->print_all ? stdout : stderr; 76 77 vpb->n--; 78 79 if (1) { 80 minmax = "ub"; 81 sign = 1; 82 } else { 83 minmax = "lb"; 84 sign = -1; 85 } 86 87 ctx = isl_point_get_ctx(pnt); 88 p = isl_printer_to_file(ctx, out); 89 90 isl_int_init(t); 91 92 pwf = isl_pw_qpolynomial_fold_copy(vpb->pwf); 93 94 nparam = isl_pw_qpolynomial_fold_dim(pwf, isl_dim_param); 95 for (i = 0; i < nparam; ++i) { 96 isl_point_get_coordinate(pnt, isl_dim_param, i, &t); 97 pwf = isl_pw_qpolynomial_fold_fix_dim(pwf, isl_dim_param, i, t); 98 } 99 100 bound = isl_pw_qpolynomial_fold_eval( 101 isl_pw_qpolynomial_fold_copy(vpb->bound), 102 isl_point_copy(pnt)); 103 104 dom = isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf)); 105 bounded = isl_set_is_bounded(dom); 106 107 if (bounded < 0) 108 goto error; 109 110 if (!bounded) 111 opt = isl_pw_qpolynomial_fold_eval( 112 isl_pw_qpolynomial_fold_copy(pwf), 113 isl_set_sample_point(isl_set_copy(dom))); 114 else if (sign > 0) 115 opt = isl_pw_qpolynomial_fold_max(isl_pw_qpolynomial_fold_copy(pwf)); 116 else 117 opt = isl_pw_qpolynomial_fold_min(isl_pw_qpolynomial_fold_copy(pwf)); 118 119 nvar = isl_set_dim(dom, isl_dim_set); 120 opt = isl_qpolynomial_project_domain_on_params(opt); 121 if (vpb->exact && bounded) 122 ok = isl_qpolynomial_plain_is_equal(opt, bound); 123 else if (sign > 0) 124 ok = isl_qpolynomial_le_cst(opt, bound); 125 else 126 ok = isl_qpolynomial_le_cst(bound, opt); 127 if (ok < 0) 128 goto error; 129 130 if (vpb->options->print_all || !ok) { 131 p = isl_printer_print_str(p, minmax); 132 p = isl_printer_print_str(p, "("); 133 for (i = 0; i < nparam; ++i) { 134 if (i) 135 p = isl_printer_print_str(p, ", "); 136 isl_point_get_coordinate(pnt, isl_dim_param, i, &t); 137 p = isl_printer_print_isl_int(p, t); 138 } 139 p = isl_printer_print_str(p, ") = "); 140 p = isl_printer_print_qpolynomial(p, bound); 141 p = isl_printer_print_str(p, ", "); 142 p = isl_printer_print_str(p, bounded ? "opt" : "sample"); 143 p = isl_printer_print_str(p, " = "); 144 p = isl_printer_print_qpolynomial(p, opt); 145 if (ok) 146 p = isl_printer_print_str(p, ". OK"); 147 else 148 p = isl_printer_print_str(p, ". NOT OK"); 149 p = isl_printer_end_line(p); 150 } else if ((vpb->n % vpb->stride) == 0) { 151 p = isl_printer_print_str(p, "o"); 152 p = isl_printer_flush(p); 153 } 154 155 if (0) { 156error: 157 ok = 0; 158 } 159 160 isl_pw_qpolynomial_fold_free(pwf); 161 isl_qpolynomial_free(bound); 162 isl_qpolynomial_free(opt); 163 isl_point_free(pnt); 164 isl_set_free(dom); 165 166 isl_int_clear(t); 167 168 isl_printer_free(p); 169 170 if (!ok) 171 vpb->error = 1; 172 173 if (vpb->options->continue_on_error) 174 ok = 1; 175 176 return (vpb->n >= 1 && ok) ? 0 : -1; 177} 178 179static int check_solution(__isl_take isl_pw_qpolynomial_fold *pwf, 180 __isl_take isl_pw_qpolynomial_fold *bound, int exact, 181 struct bound_options *options) 182{ 183 struct verify_point_bound vpb; 184 isl_int count, max; 185 isl_set *dom; 186 isl_set *context; 187 int i, r, n; 188 189 dom = isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf)); 190 context = isl_set_params(isl_set_copy(dom)); 191 context = isl_set_remove_divs(context); 192 context = set_bounds(context); 193 194 isl_int_init(count); 195 isl_int_init(max); 196 197 isl_int_set_si(max, 200); 198 r = isl_set_count_upto(context, max, &count); 199 assert(r >= 0); 200 n = isl_int_get_si(count); 201 202 isl_int_clear(max); 203 isl_int_clear(count); 204 205 vpb.options = options; 206 vpb.pwf = pwf; 207 vpb.bound = bound; 208 vpb.n = n; 209 vpb.stride = n > 70 ? 1 + (n + 1)/70 : 1; 210 vpb.error = 0; 211 vpb.exact = exact; 212 213 if (!options->print_all) { 214 for (i = 0; i < vpb.n; i += vpb.stride) 215 printf("."); 216 printf("\r"); 217 fflush(stdout); 218 } 219 220 isl_set_foreach_point(context, verify_point, &vpb); 221 222 isl_set_free(context); 223 isl_set_free(dom); 224 isl_pw_qpolynomial_fold_free(pwf); 225 isl_pw_qpolynomial_fold_free(bound); 226 227 if (!options->print_all) 228 printf("\n"); 229 230 if (vpb.error) { 231 fprintf(stderr, "Check failed !\n"); 232 return -1; 233 } 234 235 return 0; 236} 237 238int main(int argc, char **argv) 239{ 240 isl_ctx *ctx; 241 isl_pw_qpolynomial_fold *copy; 242 isl_pw_qpolynomial_fold *pwf; 243 struct isl_stream *s; 244 struct isl_obj obj; 245 struct bound_options *options; 246 int exact; 247 int r = 0; 248 249 options = bound_options_new_with_defaults(); 250 assert(options); 251 argc = bound_options_parse(options, argc, argv, ISL_ARG_ALL); 252 253 ctx = isl_ctx_alloc_with_options(&bound_options_args, options); 254 255 s = isl_stream_new_file(ctx, stdin); 256 obj = isl_stream_read_obj(s); 257 if (obj.type == isl_obj_pw_qpolynomial) 258 pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(isl_fold_max, 259 obj.v); 260 else if (obj.type == isl_obj_pw_qpolynomial_fold) 261 pwf = obj.v; 262 else { 263 obj.type->free(obj.v); 264 isl_die(ctx, isl_error_invalid, "invalid input", goto error); 265 } 266 267 if (options->verify) 268 copy = isl_pw_qpolynomial_fold_copy(pwf); 269 270 pwf = isl_pw_qpolynomial_fold_bound(pwf, &exact); 271 pwf = isl_pw_qpolynomial_fold_coalesce(pwf); 272 273 if (options->verify) { 274 r = check_solution(copy, pwf, exact, options); 275 } else { 276 if (!exact) 277 printf("# NOT exact\n"); 278 isl_pw_qpolynomial_fold_print(pwf, stdout, 0); 279 fprintf(stdout, "\n"); 280 isl_pw_qpolynomial_fold_free(pwf); 281 } 282 283error: 284 isl_stream_free(s); 285 286 isl_ctx_free(ctx); 287 288 return r; 289} 290