blob: 24401df7a741466c7c04637793237fe2b37ad716 [file] [log] [blame]
/*
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;
}