| /* |
| sharp.c -- perform sharp, disjoint sharp, and intersection |
| */ |
| |
| #include "espresso.h" |
| |
| long start_time; |
| |
| |
| /* cv_sharp -- form the sharp product between two covers */ |
| pcover cv_sharp(A, B) |
| pcover A, B; |
| { |
| pcube last, p; |
| pcover T; |
| |
| T = new_cover(0); |
| foreach_set(A, last, p) |
| T = sf_union(T, cb_sharp(p, B)); |
| return T; |
| } |
| |
| |
| /* cb_sharp -- form the sharp product between a cube and a cover */ |
| pcover cb_sharp(c, T) |
| pcube c; |
| pcover T; |
| { |
| if (T->count == 0) { |
| T = sf_addset(new_cover(1), c); |
| } else { |
| start_time = ptime(); |
| T = cb_recur_sharp(c, T, 0, T->count-1, 0); |
| } |
| return T; |
| } |
| |
| |
| /* recursive formulation to provide balanced merging */ |
| pcover cb_recur_sharp(c, T, first, last, level) |
| pcube c; |
| pcover T; |
| int first, last, level; |
| { |
| pcover temp, left, right; |
| int middle; |
| |
| if (first == last) { |
| temp = sharp(c, GETSET(T, first)); |
| } else { |
| middle = (first + last) / 2; |
| left = cb_recur_sharp(c, T, first, middle, level+1); |
| right = cb_recur_sharp(c, T, middle+1, last, level+1); |
| temp = cv_intersect(left, right); |
| if ((debug & SHARP) && level < 4) { |
| printf("# SHARP[%d]: %4d = %4d x %4d, time = %s\n", |
| level, temp->count, left->count, right->count, |
| print_time(ptime() - start_time)); |
| (void) fflush(stdout); |
| } |
| free_cover(left); |
| free_cover(right); |
| } |
| return temp; |
| } |
| |
| |
| /* sharp -- form the sharp product between two cubes */ |
| pcover sharp(a, b) |
| pcube a, b; |
| { |
| register int var; |
| register pcube d=cube.temp[0], temp=cube.temp[1], temp1=cube.temp[2]; |
| pcover r = new_cover(cube.num_vars); |
| |
| if (cdist0(a, b)) { |
| set_diff(d, a, b); |
| for(var = 0; var < cube.num_vars; var++) { |
| if (! setp_empty(set_and(temp, d, cube.var_mask[var]))) { |
| set_diff(temp1, a, cube.var_mask[var]); |
| set_or(GETSET(r, r->count++), temp, temp1); |
| } |
| } |
| } else { |
| r = sf_addset(r, a); |
| } |
| return r; |
| } |
| |
| pcover make_disjoint(A) |
| pcover A; |
| { |
| pcover R, new; |
| register pset last, p; |
| |
| R = new_cover(0); |
| foreach_set(A, last, p) { |
| new = cb_dsharp(p, R); |
| R = sf_append(R, new); |
| } |
| return R; |
| } |
| |
| |
| /* cv_dsharp -- disjoint-sharp product between two covers */ |
| pcover cv_dsharp(A, B) |
| pcover A, B; |
| { |
| register pcube last, p; |
| pcover T; |
| |
| T = new_cover(0); |
| foreach_set(A, last, p) { |
| T = sf_union(T, cb_dsharp(p, B)); |
| } |
| return T; |
| } |
| |
| |
| /* cb1_dsharp -- disjoint-sharp product between a cover and a cube */ |
| pcover cb1_dsharp(T, c) |
| pcover T; |
| pcube c; |
| { |
| pcube last, p; |
| pcover R; |
| |
| R = new_cover(T->count); |
| foreach_set(T, last, p) { |
| R = sf_union(R, dsharp(p, c)); |
| } |
| return R; |
| } |
| |
| |
| /* cb_dsharp -- disjoint-sharp product between a cube and a cover */ |
| pcover cb_dsharp(c, T) |
| pcube c; |
| pcover T; |
| { |
| pcube last, p; |
| pcover Y, Y1; |
| |
| if (T->count == 0) { |
| Y = sf_addset(new_cover(1), c); |
| } else { |
| Y = new_cover(T->count); |
| set_copy(GETSET(Y,Y->count++), c); |
| foreach_set(T, last, p) { |
| Y1 = cb1_dsharp(Y, p); |
| free_cover(Y); |
| Y = Y1; |
| } |
| } |
| return Y; |
| } |
| |
| |
| /* dsharp -- form the disjoint-sharp product between two cubes */ |
| pcover dsharp(a, b) |
| pcube a, b; |
| { |
| register pcube mask, diff, and, temp, temp1 = cube.temp[0]; |
| int var; |
| pcover r; |
| |
| r = new_cover(cube.num_vars); |
| |
| if (cdist0(a, b)) { |
| diff = set_diff(new_cube(), a, b); |
| and = set_and(new_cube(), a, b); |
| mask = new_cube(); |
| for(var = 0; var < cube.num_vars; var++) { |
| /* check if position var of "a and not b" is not empty */ |
| if (! setp_disjoint(diff, cube.var_mask[var])) { |
| |
| /* coordinate var equals the difference between a and b */ |
| temp = GETSET(r, r->count++); |
| (void) set_and(temp, diff, cube.var_mask[var]); |
| |
| /* coordinates 0 ... var-1 equal the intersection */ |
| INLINEset_and(temp1, and, mask); |
| INLINEset_or(temp, temp, temp1); |
| |
| /* coordinates var+1 .. cube.num_vars equal a */ |
| set_or(mask, mask, cube.var_mask[var]); |
| INLINEset_diff(temp1, a, mask); |
| INLINEset_or(temp, temp, temp1); |
| } |
| } |
| free_cube(diff); |
| free_cube(and); |
| free_cube(mask); |
| } else { |
| r = sf_addset(r, a); |
| } |
| return r; |
| } |
| |
| /* cv_intersect -- form the intersection of two covers */ |
| |
| #define MAGIC 500 /* save 500 cubes before containment */ |
| |
| pcover cv_intersect(A, B) |
| pcover A, B; |
| { |
| register pcube pi, pj, lasti, lastj, pt; |
| pcover T, Tsave = NULL; |
| |
| /* How large should each temporary result cover be ? */ |
| T = new_cover(MAGIC); |
| pt = T->data; |
| |
| /* Form pairwise intersection of each cube of A with each cube of B */ |
| foreach_set(A, lasti, pi) { |
| foreach_set(B, lastj, pj) { |
| if (cdist0(pi, pj)) { |
| (void) set_and(pt, pi, pj); |
| if (++T->count >= T->capacity) { |
| if (Tsave == NULL) |
| Tsave = sf_contain(T); |
| else |
| Tsave = sf_union(Tsave, sf_contain(T)); |
| T = new_cover(MAGIC); |
| pt = T->data; |
| } else |
| pt += T->wsize; |
| } |
| } |
| } |
| |
| |
| if (Tsave == NULL) |
| Tsave = sf_contain(T); |
| else |
| Tsave = sf_union(Tsave, sf_contain(T)); |
| return Tsave; |
| } |