📄 sharp.c
字号:
/* * Revision Control Information * * $Source: /projects/mvsis/Repository/mvsis-1.3/src/sis/espresso/sharp.c,v $ * $Author: wjiang $ * $Revision: 1.1.1.1 $ * $Date: 2003/02/24 22:24:08 $ * *//* 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) { (void) 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)) { (void) set_diff(d, a, b); for(var = 0; var < cube.num_vars; var++) { if (! setp_empty(set_and(temp, d, cube.var_mask[var]))) { (void) set_diff(temp1, a, cube.var_mask[var]); (void) 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); (void) 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 */ (void) 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;}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -