1 #include <assert.h> 2 #include <isl/stream.h> 3 #include <isl_map_private.h> 4 #include <isl/polynomial.h> 5 #include <isl_scan.h> 6 #include <isl/val.h> 7 #include <isl/options.h> 8 9 struct bound_options { 10 struct isl_options *isl; 11 unsigned verify; 12 int print_all; 13 int continue_on_error; 14 }; 15 16 ISL_ARGS_START(struct bound_options, bound_options_args) 17 ISL_ARG_CHILD(struct bound_options, isl, "isl", &isl_options_args, 18 "isl options") 19 ISL_ARG_BOOL(struct bound_options, verify, 'T', "verify", 0, NULL) 20 ISL_ARG_BOOL(struct bound_options, print_all, 'A', "print-all", 0, NULL) 21 ISL_ARG_BOOL(struct bound_options, continue_on_error, '\0', "continue-on-error", 0, NULL) 22 ISL_ARGS_END 23 24 ISL_ARG_DEF(bound_options, struct bound_options, bound_options_args) 25 26 static __isl_give isl_set *set_bounds(__isl_take isl_set *set) 27 { 28 isl_size nparam; 29 int i, r; 30 isl_point *pt, *pt2; 31 isl_set *box; 32 33 nparam = isl_set_dim(set, isl_dim_param); 34 if (nparam < 0) 35 return isl_set_free(set); 36 r = nparam >= 8 ? 5 : nparam >= 5 ? 15 : 50; 37 38 pt = isl_set_sample_point(isl_set_copy(set)); 39 pt2 = isl_point_copy(pt); 40 41 for (i = 0; i < nparam; ++i) { 42 pt = isl_point_add_ui(pt, isl_dim_param, i, r); 43 pt2 = isl_point_sub_ui(pt2, isl_dim_param, i, r); 44 } 45 46 box = isl_set_box_from_points(pt, pt2); 47 48 return isl_set_intersect(set, box); 49 } 50 51 struct verify_point_bound { 52 struct bound_options *options; 53 int stride; 54 int n; 55 int exact; 56 int error; 57 58 isl_pw_qpolynomial_fold *pwf; 59 isl_pw_qpolynomial_fold *bound; 60 }; 61 62 static isl_stat verify_point(__isl_take isl_point *pnt, void *user) 63 { 64 int i; 65 isl_size nparam; 66 struct verify_point_bound *vpb = (struct verify_point_bound *) user; 67 isl_val *v; 68 isl_ctx *ctx; 69 isl_pw_qpolynomial_fold *pwf; 70 isl_val *bound = NULL; 71 isl_val *opt = NULL; 72 isl_set *dom = NULL; 73 isl_printer *p; 74 const char *minmax; 75 isl_bool bounded; 76 int sign; 77 int ok; 78 FILE *out = vpb->options->print_all ? stdout : stderr; 79 80 vpb->n--; 81 82 if (1) { 83 minmax = "ub"; 84 sign = 1; 85 } else { 86 minmax = "lb"; 87 sign = -1; 88 } 89 90 ctx = isl_point_get_ctx(pnt); 91 p = isl_printer_to_file(ctx, out); 92 93 pwf = isl_pw_qpolynomial_fold_copy(vpb->pwf); 94 95 nparam = isl_pw_qpolynomial_fold_dim(pwf, isl_dim_param); 96 if (nparam < 0) 97 pwf = isl_pw_qpolynomial_fold_free(pwf); 98 for (i = 0; i < nparam; ++i) { 99 v = isl_point_get_coordinate_val(pnt, isl_dim_param, i); 100 pwf = isl_pw_qpolynomial_fold_fix_val(pwf, isl_dim_param, i, v); 101 } 102 103 bound = isl_pw_qpolynomial_fold_eval( 104 isl_pw_qpolynomial_fold_copy(vpb->bound), 105 isl_point_copy(pnt)); 106 107 dom = isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf)); 108 bounded = isl_set_is_bounded(dom); 109 110 if (bounded < 0) 111 goto error; 112 113 if (!bounded) 114 opt = isl_pw_qpolynomial_fold_eval( 115 isl_pw_qpolynomial_fold_copy(pwf), 116 isl_set_sample_point(isl_set_copy(dom))); 117 else if (sign > 0) 118 opt = isl_pw_qpolynomial_fold_max(isl_pw_qpolynomial_fold_copy(pwf)); 119 else 120 opt = isl_pw_qpolynomial_fold_min(isl_pw_qpolynomial_fold_copy(pwf)); 121 122 if (vpb->exact && bounded) 123 ok = isl_val_eq(opt, bound); 124 else if (sign > 0) 125 ok = isl_val_le(opt, bound); 126 else 127 ok = isl_val_le(bound, opt); 128 if (ok < 0) 129 goto error; 130 131 if (vpb->options->print_all || !ok) { 132 p = isl_printer_print_str(p, minmax); 133 p = isl_printer_print_str(p, "("); 134 for (i = 0; i < nparam; ++i) { 135 if (i) 136 p = isl_printer_print_str(p, ", "); 137 v = isl_point_get_coordinate_val(pnt, isl_dim_param, i); 138 p = isl_printer_print_val(p, v); 139 isl_val_free(v); 140 } 141 p = isl_printer_print_str(p, ") = "); 142 p = isl_printer_print_val(p, bound); 143 p = isl_printer_print_str(p, ", "); 144 p = isl_printer_print_str(p, bounded ? "opt" : "sample"); 145 p = isl_printer_print_str(p, " = "); 146 p = isl_printer_print_val(p, opt); 147 if (ok) 148 p = isl_printer_print_str(p, ". OK"); 149 else 150 p = isl_printer_print_str(p, ". NOT OK"); 151 p = isl_printer_end_line(p); 152 } else if ((vpb->n % vpb->stride) == 0) { 153 p = isl_printer_print_str(p, "o"); 154 p = isl_printer_flush(p); 155 } 156 157 if (0) { 158 error: 159 ok = 0; 160 } 161 162 isl_pw_qpolynomial_fold_free(pwf); 163 isl_val_free(bound); 164 isl_val_free(opt); 165 isl_point_free(pnt); 166 isl_set_free(dom); 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) ? isl_stat_ok : isl_stat_error; 177 } 178 179 static 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 238 int main(int argc, char **argv) 239 { 240 isl_ctx *ctx; 241 isl_pw_qpolynomial_fold *copy; 242 isl_pw_qpolynomial_fold *pwf; 243 isl_stream *s; 244 struct isl_obj obj; 245 struct bound_options *options; 246 isl_bool 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 283 error: 284 isl_stream_free(s); 285 286 isl_ctx_free(ctx); 287 288 return r; 289 } 290
Indexes created Fri Aug 28 00:25:22 UTC 2026