src/misc/espresso/sharp.c File Reference

#include "espresso.h"

Include dependency graph for sharp.c:

Go to the source code of this file.

Defines
#define	MAGIC   500
Functions
pcover	cv_sharp (pcover A, pcover B)
pcover	cb_sharp (pcube c, pcover T)
pcover	cb_recur_sharp (pcube c, pcover T, int first, int last, int level)
pcover	sharp (pcube a, pcube b)
pcover	make_disjoint (pcover A)
pcover	cv_dsharp (pcover A, pcover B)
pcover	cb1_dsharp (pcover T, pcube c)
pcover	cb_dsharp (pcube c, pcover T)
pcover	dsharp (pcube a, pcube b)
pcover	cv_intersect (pcover A, pcover B)
Variables
long	start_time

---

Define Documentation

#define MAGIC   500

Definition at line 211 of file sharp.c.

---

Function Documentation

pcover cb1_dsharp	(	pcover	T,
		pcube	c
	)

Definition at line 130 of file sharp.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;
}

pcover cb_dsharp	(	pcube	c,
		pcover	T
	)

Definition at line 146 of file sharp.c.

{
    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;
}

pcover cb_recur_sharp	(	pcube	c,
		pcover	T,
		int	first,
		int	last,
		int	level
	)

Definition at line 49 of file sharp.c.

{
    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;
}

pcover cb_sharp	(	pcube	c,
		pcover	T
	)

Definition at line 34 of file sharp.c.

{
    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;
}

pcover cv_dsharp	(	pcover	A,
		pcover	B
	)

Definition at line 115 of file sharp.c.

{
    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;
}

pcover cv_intersect	(	pcover	A,
		pcover	B
	)

Definition at line 213 of file sharp.c.

{
    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;
}

pcover cv_sharp	(	pcover	A,
		pcover	B
	)

Definition at line 20 of file sharp.c.

{
    pcube last, p;
    pcover T;

    T = new_cover(0);
    foreach_set(A, last, p)
        T = sf_union(T, cb_sharp(p, B));
    return T;
}

pcover dsharp	(	pcube	a,
		pcube	b
	)

Definition at line 169 of file sharp.c.

{
    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;
}

pcover make_disjoint

(

pcover

A

)

Definition at line 99 of file sharp.c.

{
    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;
}

pcover sharp	(	pcube	a,
		pcube	b
	)

Definition at line 78 of file sharp.c.

{
    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;
}

---

Variable Documentation

long start_time

Definition at line 16 of file sharp.c.