From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/misc/espresso/sharp.c | 247 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 247 insertions(+) create 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 new file mode 100644 index 00000000..53435078 --- /dev/null +++ b/src/misc/espresso/sharp.c @@ -0,0 +1,247 @@ +/* + * 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