src/misc/espresso/primes.c File Reference

#include "espresso.h"

Include dependency graph for primes.c:

Go to the source code of this file.

Functions
static bool	primes_consensus_special_cases ()
static pcover	primes_consensus_merge ()
static pcover	and_with_cofactor ()
pcover	primes_consensus (pcube *T)
static bool	primes_consensus_special_cases (pcube *T, pcover *Tnew)
static pcover	primes_consensus_merge (pcover Tl, pcover Tr, pcube cl, pcube cr)
static pcover	and_with_cofactor (pset_family A, pset cof)

---

Function Documentation

static pcover and_with_cofactor	(	pset_family	A,
		pset	cof
	)			[static]

Definition at line 155 of file primes.c.

{
    register pset last, p;

    foreach_set(A, last, p) {
        INLINEset_and(p, p, cof);
        if (cdist(p, cube.fullset) > 0) {
            RESET(p, ACTIVE);
        } else {
            SET(p, ACTIVE);
        }
    }
    return sf_inactive(A);
}

static pcover and_with_cofactor

(

)

[static]

pcover primes_consensus

(

pcube *

T

)

Definition at line 18 of file primes.c.

{
    register pcube cl, cr;
    register int best;
    pcover Tnew, Tl, Tr;

    if (primes_consensus_special_cases(T, &Tnew) == MAYBE) {
        cl = new_cube();
        cr = new_cube();
        best = binate_split_select(T, cl, cr, COMPL);

        Tl = primes_consensus(scofactor(T, cl, best));
        Tr = primes_consensus(scofactor(T, cr, best));
        Tnew = primes_consensus_merge(Tl, Tr, cl, cr);

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

    return Tnew;
}

static pcover primes_consensus_merge	(	pcover	Tl,
		pcover	Tr,
		pcube	cl,
		pcube	cr
	)			[static]

Definition at line 118 of file primes.c.

{
    register pcube pl, pr, lastl, lastr, pt;
    pcover T, Tsave;

    Tl = and_with_cofactor(Tl, cl);
    Tr = and_with_cofactor(Tr, cr);

    T = sf_new(500, Tl->sf_size);
    pt = T->data;
    Tsave = sf_contain(sf_join(Tl, Tr));

    foreach_set(Tl, lastl, pl) {
        foreach_set(Tr, lastr, pr) {
            if (cdist01(pl, pr) == 1) {
                consensus(pt, pl, pr);
                if (++T->count >= T->capacity) {
                    Tsave = sf_union(Tsave, sf_contain(T));
                    T = sf_new(500, Tl->sf_size);
                    pt = T->data;
                } else {
                    pt += T->wsize;
                }
            }
        }
    }
    free_cover(Tl);
    free_cover(Tr);

    Tsave = sf_union(Tsave, sf_contain(T));
    return Tsave;
}

static pcover primes_consensus_merge

(

)

[static]

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

Definition at line 43 of file primes.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 = primes_consensus(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 primes_consensus_special_cases

(

)

[static]