#include "espresso.h"

static bool3 primes_consensus_special_cases(pset *T, pset_family *Tnew);
static pcover primes_consensus_merge(pset_family Tl, pset_family Tr, pset cl, pset cr);
static pcover and_with_cofactor(pset_family A, register pset cof); 


/* primes_consensus -- generate primes using consensus */
/** MM: kontroluje parameter, ktory dealokuje */
/** MM: pri chybe NULL */
pcover primes_consensus(pset *T)
         			/* T will be disposed of */
{
    register pcube cl, cr;
    register int best;
    pcover Tnew, Tl, Tr;
    
    if (T==NULL) return NULL;

    if (primes_consensus_special_cases(T, &Tnew) == MAYBE3) { /** MM: ak TRUE3, T will be disposed of */
    	cl = new_cube();
    	cr = new_cube();
    	if ( (cl==NULL) || (cr==NULL) ) { free_cube(cl); free_cube(cr); free_cubelist(T); return NULL;} /** MM: ak chyba alokacie */
    	best = binate_split_select(T, cl, cr, COMPL);
    
    	Tl = primes_consensus(scofactor(T, cl, best));
    	Tr = primes_consensus(scofactor(T, cr, best));
    	if ( (Tl==NULL) || (Tr==NULL) ) { /** MM: ak chyba alokacie */
            free_cube(cl); free_cube(cr); free_cubelist(T); 
            sf_free(Tl); sf_free(Tr); return NULL;
        }
    	Tnew = primes_consensus_merge(Tl, Tr, cl, cr);
    
    	free_cube(cl);
    	free_cube(cr);
    	free_cubelist(T);
    }

    return Tnew;
}

/** MM: vnutorne neosetrena */
static bool3 
primes_consensus_special_cases(pset *T, pset_family *Tnew)
         			/* will be disposed if answer is determined */
             			/* returned only if answer determined */
{
    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 TRUE3;
    }

    /* 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 TRUE3;
    }

    /* 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 TRUE3;
    	}
    }

    /* 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 TRUE3;
    }
    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 TRUE3;

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

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

/** MM: disposes of Tl a Tr */
/** MM: kontroluje parametre, ktore dealokuje */
/** MM: pri chybe NULL */
static pcover 
primes_consensus_merge(pset_family Tl, pset_family Tr, pset cl, pset cr)
{
    register pcube pl, pr, lastl, lastr, pt;
    pcover T, Tsave;
    
    if ( (Tl==NULL) || (Tr==NULL) ) { /** MM: ak chyba parametrov */
        sf_free(Tl); sf_free(Tr);
        return NULL;
    }

    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));
    if ( (T==NULL) || (Tsave==NULL) ) { /** MM: ak chyba alokacie */
        sf_free(Tl); sf_free(Tr);
        sf_free(T); sf_free(Tsave);
        return NULL;
    }

    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);
        		    if ( (T==NULL) || (Tsave==NULL) ) { /** MM: ak chyba alokacie */
                        sf_free(Tl); sf_free(Tr);
                        sf_free(T); sf_free(Tsave);
                        return NULL;
                    }
        		    pt = T->data;
        		} else {
        		    pt += T->wsize;
        		}
    	    }
    	}
    }
    free_cover(Tl);
    free_cover(Tr);

    Tsave = sf_union(Tsave, sf_contain(T)); /** MM: tuto chybu si musi osefovat volajuci */
    return Tsave;
}

/** MM: len upravuje set_family, nic nealokuje */
static pcover
and_with_cofactor(pset_family A, register pset cof)
{
    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); /** MM: sf_inactive tiez len upravuje A */
}
