From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/misc/espresso/sharp.c | 247 ---------------------------------------------- 1 file changed, 247 deletions(-) delete mode 100644 src/misc/espresso/sharp.c (limited to 'src/misc/espresso/sharp.c') diff --git a/src/misc/espresso/sharp.c b/src/misc/espresso/sharp.c deleted file mode 100644 index 53435078..00000000 --- a/src/misc/espresso/sharp.c +++ /dev/null @@ -1,247 +0,0 @@ -/* - * Revision Control Information - * - * $Source$ - * $Author$ - * $Revision$ - * $Date$ - * - */ -/* - 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; -} -- cgit v1.2.3