src/misc/espresso/compl.c File Reference

#include "espresso.h"

Include dependency graph for compl.c:

Go to the source code of this file.

Defines
#define	USE_COMPL_LIFT   0
#define	USE_COMPL_LIFT_ONSET   1
#define	USE_COMPL_LIFT_ONSET_COMPLEX   2
#define	NO_LIFTING   3
Functions
static bool	compl_special_cases ()
static pcover	compl_merge ()
static void	compl_d1merge ()
static pcover	compl_cube ()
static void	compl_lift ()
static void	compl_lift_onset ()
static void	compl_lift_onset_complex ()
static bool	simp_comp_special_cases ()
static bool	simplify_special_cases ()
pcover	complement (pcube *T)
static bool	compl_special_cases (pcube *T, pcover *Tbar)
static pcover	compl_merge (pcube *T1, pcover L, pcover R, pcube cl, pcube cr, int var, int lifting)
static void	compl_lift (pcube *A1, pcube *B1, pcube bcube, int var)
static void	compl_lift_onset (pcube *A1, pcover T, pcube bcube, int var)
static void	compl_lift_onset_complex (pcube *A1, pcover T, int var)
static void	compl_d1merge (pcube *L1, pcube *R1)
static pcover	compl_cube (pcube p)
void	simp_comp (pcube *T, pcover *Tnew, pcover *Tbar)
static bool	simp_comp_special_cases (pcube *T, pcover *Tnew, pcover *Tbar)
pcover	simplify (pcube *T)
static bool	simplify_special_cases (pcube *T, pcover *Tnew)

---

Define Documentation

#define NO_LIFTING   3

Definition at line 32 of file compl.c.

#define USE_COMPL_LIFT   0

Definition at line 29 of file compl.c.

#define USE_COMPL_LIFT_ONSET   1

Definition at line 30 of file compl.c.

#define USE_COMPL_LIFT_ONSET_COMPLEX   2

Definition at line 31 of file compl.c.

---

Function Documentation

static pcover compl_cube

(

pcube

p

)

[static]

Definition at line 397 of file compl.c.

{
    register pcube diff=cube.temp[7], pdest, mask, full=cube.fullset;
    int var;
    pcover R;

    /* Allocate worst-case size cover (to avoid checking overflow) */
    R = new_cover(cube.num_vars);

    /* Compute bit-wise complement of the cube */
    INLINEset_diff(diff, full, p);

    for(var = 0; var < cube.num_vars; var++) {
        mask = cube.var_mask[var];
        /* If the bit-wise complement is not empty in var ... */
        if (! setp_disjoint(diff, mask)) {
            pdest = GETSET(R, R->count++);
            INLINEset_merge(pdest, diff, full, mask);
        }
    }
    return R;
}

static pcover compl_cube

(

)

[static]

static void compl_d1merge	(	pcube *	L1,
		pcube *	R1
	)			[static]

Definition at line 373 of file compl.c.

{
    register pcube pl, pr;

    /* Find equal cubes between the two cofactors */
    for(pl = *L1, pr = *R1; (pl != NULL) && (pr != NULL); )
        switch (d1_order(L1, R1)) {
            case 1:
                pr = *(++R1); break;            /* advance right pointer */
            case -1:
                pl = *(++L1); break;            /* advance left pointer */
            case 0:
                RESET(pr, ACTIVE);
                INLINEset_or(pl, pl, pr);
                pr = *(++R1);
            default:
                ;
        }
}

static void compl_d1merge

(

)

[static]

static void compl_lift	(	pcube *	A1,
		pcube *	B1,
		pcube	bcube,
		int	var
	)			[static]

Definition at line 263 of file compl.c.

{
    register pcube a, b, *B2, lift=cube.temp[4], liftor=cube.temp[5];
    pcube mask = cube.var_mask[var];

    (void) set_and(liftor, bcube, mask);

    /* for each cube in the first array ... */
    for(; (a = *A1++) != NULL; ) {
        if (TESTP(a, ACTIVE)) {

            /* create a lift of this cube in the merging coord */
            (void) set_merge(lift, bcube, a, mask);

            /* for each cube in the second array */
            for(B2 = B1; (b = *B2++) != NULL; ) {
                INLINEsetp_implies(lift, b, /* when_false => */ continue);
                /* when_true => fall through to next statement */

                /* cube of A1 was contained by some cube of B1, so raise */
                INLINEset_or(a, a, liftor);
                break;
            }
        }
    }
}

static void compl_lift

(

)

[static]

static void compl_lift_onset	(	pcube *	A1,
		pcover	T,
		pcube	bcube,
		int	var
	)			[static]

Definition at line 300 of file compl.c.

{
    register pcube a, last, p, lift=cube.temp[4], mask=cube.var_mask[var];

    /* for each active cube from one branch of the complement */
    for(; (a = *A1++) != NULL; ) {
        if (TESTP(a, ACTIVE)) {

            /* create a lift of this cube in the merging coord */
            INLINEset_and(lift, bcube, mask);   /* isolate parts to raise */
            INLINEset_or(lift, a, lift);        /* raise these parts in a */

            /* for each cube in the ON-set, check for intersection */
            foreach_set(T, last, p) {
                if (cdist0(p, lift)) {
                    goto nolift;
                }
            }
            INLINEset_copy(a, lift);            /* save the raising */
            SET(a, ACTIVE);
nolift : ;
        }
    }
}

static void compl_lift_onset

(

)

[static]

static void compl_lift_onset_complex	(	pcube *	A1,
		pcover	T,
		int	var
	)			[static]

Definition at line 335 of file compl.c.

{
    register int dist;
    register pcube last, p, a, xlower;

    /* for each cube in the complement */
    xlower = new_cube();
    for(; (a = *A1++) != NULL; ) {

        if (TESTP(a, ACTIVE)) {

            /* Find which parts of the splitting variable are forced low */
            INLINEset_clear(xlower, cube.size);
            foreach_set(T, last, p) {
                if ((dist = cdist01(p, a)) < 2) {
                    if (dist == 0) {
                        fatal("compl: ON-set and OFF-set are not orthogonal");
                    } else {
                        (void) force_lower(xlower, p, a);
                    }
                }
            }

            (void) set_diff(xlower, cube.var_mask[var], xlower);
            (void) set_or(a, a, xlower);
            free_cube(xlower);
        }
    }
}

static void compl_lift_onset_complex

(

)

[static]

static pcover compl_merge	(	pcube *	T1,
		pcover	L,
		pcover	R,
		pcube	cl,
		pcube	cr,
		int	var,
		int	lifting
	)			[static]

Definition at line 169 of file compl.c.

{
    register pcube p, last, pt;
    pcover T, Tbar;
    pcube *L1, *R1;

    if (debug & COMPL) {
        (void) printf("compl_merge: left %d, right %d\n", L->count, R->count);
        (void) printf("%s (cl)\n%s (cr)\nLeft is\n", pc1(cl), pc2(cr));
        cprint(L);
        (void) printf("Right is\n");
        cprint(R);
    }

    /* Intersect each cube with the cofactored cube */
    foreach_set(L, last, p) {
        INLINEset_and(p, p, cl);
        SET(p, ACTIVE);
    }
    foreach_set(R, last, p) {
        INLINEset_and(p, p, cr);
        SET(p, ACTIVE);
    }

    /* Sort the arrays for a distance-1 merge */
    (void) set_copy(cube.temp[0], cube.var_mask[var]);
    qsort((char *) (L1 = sf_list(L)), L->count, sizeof(pset), (int (*)()) d1_order);
    qsort((char *) (R1 = sf_list(R)), R->count, sizeof(pset), (int (*)()) d1_order);

    /* Perform distance-1 merge */
    compl_d1merge(L1, R1);

    /* Perform lifting */
    switch(lifting) {
        case USE_COMPL_LIFT_ONSET:
            T = cubeunlist(T1);
            compl_lift_onset(L1, T, cr, var);
            compl_lift_onset(R1, T, cl, var);
            free_cover(T);
            break;
        case USE_COMPL_LIFT_ONSET_COMPLEX:
            T = cubeunlist(T1);
            compl_lift_onset_complex(L1, T, var);
            compl_lift_onset_complex(R1, T, var);
            free_cover(T);
            break;
        case USE_COMPL_LIFT:
            compl_lift(L1, R1, cr, var);
            compl_lift(R1, L1, cl, var);
            break;
        case NO_LIFTING:
            break;
        default:
            ;
    }
    FREE(L1);
    FREE(R1);

    /* Re-create the merged cover */
    Tbar = new_cover(L->count + R->count);
    pt = Tbar->data;
    foreach_set(L, last, p) {
        INLINEset_copy(pt, p);
        Tbar->count++;
        pt += Tbar->wsize;
    }
    foreach_active_set(R, last, p) {
        INLINEset_copy(pt, p);
        Tbar->count++;
        pt += Tbar->wsize;
    }

    if (debug & COMPL) {
        (void) printf("Result %d\n", Tbar->count);
        if (verbose_debug)
            cprint(Tbar);
    }

    free_cover(L);
    free_cover(R);
    return Tbar;
}

static pcover compl_merge

(

)

[static]

static bool compl_special_cases	(	pcube *	T,
		pcover *	Tbar
	)			[static]

Definition at line 86 of file compl.c.

{
    register pcube *T1, p, ceil, cof=T[0];
    pcover A, ceil_compl;

    /* Check for no cubes in the cover */
    if (T[2] == NULL) {
        *Tbar = sf_addset(new_cover(1), cube.fullset);
        free_cubelist(T);
        return TRUE;
    }

    /* Check for only a single cube in the cover */
    if (T[3] == NULL) {
        *Tbar = compl_cube(set_or(cof, cof, T[2]));
        free_cubelist(T);
        return TRUE;
    }

    /* Check for a row of all 1's (implies complement is null) */
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        if (full_row(p, cof)) {
            *Tbar = new_cover(0);
            free_cubelist(T);
            return TRUE;
        }
    }

    /* Check for a column of all 0's which can be factored out */
    ceil = set_save(cof);
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        INLINEset_or(ceil, ceil, p);
    }
    if (! setp_equal(ceil, cube.fullset)) {
        ceil_compl = compl_cube(ceil);
        (void) set_or(cof, cof, set_diff(ceil, cube.fullset, ceil));
        set_free(ceil);
        *Tbar = sf_append(complement(T), ceil_compl);
        return TRUE;
    }
    set_free(ceil);

    /* Collect column counts, determine unate variables, etc. */
    massive_count(T);

    /* If single active variable not factored out above, then tautology ! */
    if (cdata.vars_active == 1) {
        *Tbar = new_cover(0);
        free_cubelist(T);
        return TRUE;

    /* Check for unate cover */
    } else if (cdata.vars_unate == cdata.vars_active) {
        A = map_cover_to_unate(T);
        free_cubelist(T);
        A = unate_compl(A);
        *Tbar = map_unate_to_cover(A);
        sf_free(A);
        return TRUE;

    /* Not much we can do about it */
    } else {
        return MAYBE;
    }
}

static bool compl_special_cases

(

)

[static]

pcover complement

(

pcube *

T

)

Definition at line 46 of file compl.c.

{
    register pcube cl, cr;
    register int best;
    pcover Tbar, Tl, Tr;
    int lifting;
    static int compl_level = 0;

    if (debug & COMPL)
        debug_print(T, "COMPLEMENT", compl_level++);

    if (compl_special_cases(T, &Tbar) == MAYBE) {

        /* Allocate space for the partition cubes */
        cl = new_cube();
        cr = new_cube();
        best = binate_split_select(T, cl, cr, COMPL);

        /* Complement the left and right halves */
        Tl = complement(scofactor(T, cl, best));
        Tr = complement(scofactor(T, cr, best));

        if (Tr->count*Tl->count > (Tr->count+Tl->count)*CUBELISTSIZE(T)) {
            lifting = USE_COMPL_LIFT_ONSET;
        } else {
            lifting = USE_COMPL_LIFT;
        }
        Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);

        free_cube(cl);
        free_cube(cr);
        free_cubelist(T);
    }

    if (debug & COMPL)
        debug1_print(Tbar, "exit COMPLEMENT", --compl_level);
    return Tbar;
}

void simp_comp	(	pcube *	T,
		pcover *	Tnew,
		pcover *	Tbar
	)

Definition at line 422 of file compl.c.

{
    register pcube cl, cr;
    register int best;
    pcover Tl, Tr, Tlbar, Trbar;
    int lifting;
    static int simplify_level = 0;

    if (debug & COMPL)
        debug_print(T, "SIMPCOMP", simplify_level++);

    if (simp_comp_special_cases(T, Tnew, Tbar) == MAYBE) {

        /* Allocate space for the partition cubes */
        cl = new_cube();
        cr = new_cube();
        best = binate_split_select(T, cl, cr, COMPL);

        /* Complement the left and right halves */
        simp_comp(scofactor(T, cl, best), &Tl, &Tlbar);
        simp_comp(scofactor(T, cr, best), &Tr, &Trbar);

        lifting = USE_COMPL_LIFT;
        *Tnew = compl_merge(T, Tl, Tr, cl, cr, best, lifting);

        lifting = USE_COMPL_LIFT;
        *Tbar = compl_merge(T, Tlbar, Trbar, cl, cr, best, lifting);

        /* All of this work for nothing ? Let's hope not ... */
        if ((*Tnew)->count > CUBELISTSIZE(T)) {
            sf_free(*Tnew);
            *Tnew = cubeunlist(T);
        }

        free_cube(cl);
        free_cube(cr);
        free_cubelist(T);
    }

    if (debug & COMPL) {
        debug1_print(*Tnew, "exit SIMPCOMP (new)", simplify_level);
        debug1_print(*Tbar, "exit SIMPCOMP (compl)", simplify_level);
        simplify_level--;
    }
}

static bool simp_comp_special_cases	(	pcube *	T,
		pcover *	Tnew,
		pcover *	Tbar
	)			[static]

Definition at line 471 of file compl.c.

{
    register pcube *T1, p, ceil, cof=T[0];
    pcube last;
    pcover A;

    /* Check for no cubes in the cover (function is empty) */
    if (T[2] == NULL) {
        *Tnew = new_cover(1);
        *Tbar = sf_addset(new_cover(1), cube.fullset);
        free_cubelist(T);
        return TRUE;
    }

    /* Check for only a single cube in the cover */
    if (T[3] == NULL) {
        (void) set_or(cof, cof, T[2]);
        *Tnew = sf_addset(new_cover(1), cof);
        *Tbar = compl_cube(cof);
        free_cubelist(T);
        return TRUE;
    }

    /* Check for a row of all 1's (function is a tautology) */
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        if (full_row(p, cof)) {
            *Tnew = sf_addset(new_cover(1), cube.fullset);
            *Tbar = new_cover(1);
            free_cubelist(T);
            return TRUE;
        }
    }

    /* Check for a column of all 0's which can be factored out */
    ceil = set_save(cof);
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        INLINEset_or(ceil, ceil, p);
    }
    if (! setp_equal(ceil, cube.fullset)) {
        p = new_cube();
        (void) set_diff(p, cube.fullset, ceil);
        (void) set_or(cof, cof, p);
        set_free(p);
        simp_comp(T, Tnew, Tbar);

        /* Adjust the ON-set */
        A = *Tnew;
        foreach_set(A, last, p) {
            INLINEset_and(p, p, ceil);
        }

        /* Compute the new complement */
        *Tbar = sf_append(*Tbar, compl_cube(ceil));
        set_free(ceil);
        return TRUE;
    }
    set_free(ceil);

    /* Collect column counts, determine unate variables, etc. */
    massive_count(T);

    /* If single active variable not factored out above, then tautology ! */
    if (cdata.vars_active == 1) {
        *Tnew = sf_addset(new_cover(1), cube.fullset);
        *Tbar = new_cover(1);
        free_cubelist(T);
        return TRUE;

    /* Check for unate cover */
    } else if (cdata.vars_unate == cdata.vars_active) {
        /* Make the cover minimum by single-cube containment */
        A = cubeunlist(T);
        *Tnew = sf_contain(A);

        /* Now form a minimum representation of the complement */
        A = map_cover_to_unate(T);
        A = unate_compl(A);
        *Tbar = map_unate_to_cover(A);
        sf_free(A);
        free_cubelist(T);
        return TRUE;

    /* Not much we can do about it */
    } else {
        return MAYBE;
    }
}

static bool simp_comp_special_cases

(

)

[static]

pcover simplify

(

pcube *

T

)

Definition at line 563 of file compl.c.

{
    register pcube cl, cr;
    register int best;
    pcover Tbar, Tl, Tr;
    int lifting;
    static int simplify_level = 0;

    if (debug & COMPL) {
        debug_print(T, "SIMPLIFY", simplify_level++);
    }

    if (simplify_special_cases(T, &Tbar) == MAYBE) {

        /* Allocate space for the partition cubes */
        cl = new_cube();
        cr = new_cube();

        best = binate_split_select(T, cl, cr, COMPL);

        /* Complement the left and right halves */
        Tl = simplify(scofactor(T, cl, best));
        Tr = simplify(scofactor(T, cr, best));

        lifting = USE_COMPL_LIFT;
        Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);

        /* All of this work for nothing ? Let's hope not ... */
        if (Tbar->count > CUBELISTSIZE(T)) {
            sf_free(Tbar);
            Tbar = cubeunlist(T);
        }

        free_cube(cl);
        free_cube(cr);
        free_cubelist(T);
    }

    if (debug & COMPL) {
        debug1_print(Tbar, "exit SIMPLIFY", --simplify_level);
    }
    return Tbar;
}

static bool simplify_special_cases	(	pcube *	T,
		pcover *	Tnew
	)			[static]

Definition at line 608 of file compl.c.

{
    register pcube *T1, p, ceil, cof=T[0];
    pcube last;
    pcover A;

    /* Check for no cubes in the cover */
    if (T[2] == NULL) {
        *Tnew = new_cover(0);
        free_cubelist(T);
        return TRUE;
    }

    /* Check for only a single cube in the cover */
    if (T[3] == NULL) {
        *Tnew = sf_addset(new_cover(1), set_or(cof, cof, T[2]));
        free_cubelist(T);
        return TRUE;
    }

    /* Check for a row of all 1's (implies function is a tautology) */
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        if (full_row(p, cof)) {
            *Tnew = sf_addset(new_cover(1), cube.fullset);
            free_cubelist(T);
            return TRUE;
        }
    }

    /* Check for a column of all 0's which can be factored out */
    ceil = set_save(cof);
    for(T1 = T+2; (p = *T1++) != NULL; ) {
        INLINEset_or(ceil, ceil, p);
    }
    if (! setp_equal(ceil, cube.fullset)) {
        p = new_cube();
        (void) set_diff(p, cube.fullset, ceil);
        (void) set_or(cof, cof, p);
        free_cube(p);

        A = simplify(T);
        foreach_set(A, last, p) {
            INLINEset_and(p, p, ceil);
        }
        *Tnew = A;
        set_free(ceil);
        return TRUE;
    }
    set_free(ceil);

    /* Collect column counts, determine unate variables, etc. */
    massive_count(T);

    /* If single active variable not factored out above, then tautology ! */
    if (cdata.vars_active == 1) {
        *Tnew = sf_addset(new_cover(1), cube.fullset);
        free_cubelist(T);
        return TRUE;

    /* Check for unate cover */
    } else if (cdata.vars_unate == cdata.vars_active) {
        A = cubeunlist(T);
        *Tnew = sf_contain(A);
        free_cubelist(T);
        return TRUE;

    /* Not much we can do about it */
    } else {
        return MAYBE;
    }
}

static bool simplify_special_cases

(

)

[static]