/*
 *  module: compl.c
 *  purpose: compute the complement of a multiple-valued function
 *
 *  The "unate recursive paradigm" is used.  After a set of special
 *  cases are examined, the function is split on the "most active
 *  variable".  These two halves are complemented recursively, and then
 *  the results are merged.
 *
 *  Changes (from Version 2.1 to Version 2.2)
 *      1. Minor bug in compl_lifting -- cubes in the left half were
 *      not marked as active, so that when merging a leaf from the left
 *      hand side, the active flags were essentially random.  This led
 *      to minor impredictability problem, but never affected the
 *      accuracy of the results.
 */

#include "espresso.h"

#define USE_COMPL_LIFT			0
#define USE_COMPL_LIFT_ONSET		1
#define USE_COMPL_LIFT_ONSET_COMPLEX	2
#define NO_LIFTING			3

static bool3 compl_special_cases(pset *T, pset_family *Tbar);
static pcover compl_merge(pset *T1, pset_family L, pset_family R, register pset cl, register pset cr, int var, int lifting);
static void compl_d1merge(register pset *L1, register pset *R1);
static pcover compl_cube(register pset p);
static void compl_lift(pset *A1, pset *B1, pset bcube, int var);
static void compl_lift_onset(pset *A1, pset_family T, pset bcube, int var);
static int compl_lift_onset_complex(pset *A1, pset_family T, int var);
static bool3 simp_comp_special_cases(pset *T, pset_family *Tnew, pset_family *Tbar);
static bool3 simplify_special_cases(pset *T, pset_family *Tnew);


/* complement -- compute the complement of T */
/** MM: ak chyba, tak NULL, inak nova struktura a disposes T */
/** MM: parameter uz kontroluje a dealokuje */
pcover complement(pset *T)
         			/* T will be disposed of */
{
    register pcube cl, cr;
    register int best;
    pcover Tbar, Tl, Tr;
    int lifting;
    static int compl_level = 0;
    bool3 tmpbool;
    
    /** MM: ak je parameter NULL, treba sa ukoncit */
    if (T == NULL) return NULL;
    
    compl_level++;
    if (debug & COMPL)
	debug_print(T, "COMPLEMENT", compl_level);
    
    tmpbool = compl_special_cases(T, &Tbar); /* &Tbar je ukazatel na ukazatela */
    if ( tmpbool == MAYBE3) {

    	/* Allocate space for the partition cubes */
    	cl = new_cube();
    	cr = new_cube();
    	/** MM: nenastala chyba? NULL je chyba, ak cube->size != 0 */
    	if (( (cl == NULL) || (cr==NULL)) && (cube->size != 0)){
            free_cube(cl); /** MM: kontroluje validnost ukazatela, je to makro */
            free_cube(cr);
            --compl_level;
            return NULL;
        }
    	best = binate_split_select(T, cl, cr, COMPL); /** MM: nic nealokuje */
    
    	/* Complement the left and right halves */
    	Tl = complement(scofactor(T, cl, best));
    	Tr = complement(scofactor(T, cr, best));
    	if ( (Tl==NULL) || (Tr==NULL) ){
            free_cover(Tl); 
            free_cover(Tr);
            free_cubelist(T); /** MM: uvolni pole a kontroluje ukazatel -> je to len makro */
            free_cube(cl);
        	free_cube(cr);
        	--compl_level;
            return NULL;
        }
    
    	if (Tr->count*Tl->count > (Tr->count+Tl->count)*CUBELISTSIZE(T)) {
    	    lifting = USE_COMPL_LIFT_ONSET;
    	} else {
    	    lifting = USE_COMPL_LIFT;
    	}
    	/** MM: chybu staci indikovat az pri exite */
    	Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting); /** MM: maze Tr a Tl, ostatok musi volajuci */
    
    	free_cube(cl);
    	free_cube(cr);
    	free_cubelist(T);
    	/** MM: chybu staci indikovat az tu */
    	if (Tbar==NULL) {
            --compl_level;
            return NULL;
        }
    }
    /** MM: kontrola, ci compl_special_cases() neskoncilo chybou */
    else if ( tmpbool == FALSE3 ){
        /** MM: T je disposed of a v Tbar sa nic nevratilo */
        --compl_level;
        return NULL;
    }
    /** MM: chyba nenastala -> normalny zaver funkcie */

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

/** MM: povodne vratila len "TRUE3" alebo "MAYBE3", teraz indikuje chybu pomocou "FALSE3" */
static bool3 compl_special_cases(pset *T, pset_family *Tbar)
         			/* T will be disposed if answer is determined and FALSE3*/
             		/* Tbar returned only if answer is determined */
{
    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);
    	if (*Tbar==NULL) return FALSE3; /** MM: ak chyba */
    	return TRUE3;
    }

    /* 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);
    	if (*Tbar==NULL) return FALSE3; /** MM: ak chyba */
    	return TRUE3;
    }

    /* 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);
    	    if (*Tbar == NULL) return FALSE3; /** MM: ak chyba alokacie */
    	    return TRUE3;
    	}
    }

    /* Check for a column of all 0's which can be factored out */
    ceil = set_save(cof);
    if (ceil == NULL){ /** MM: ak chyba, zmazat data a FALSE3 */
        free_cubelist(T);
        return FALSE3;
    }
    /** MM: pri chybe treba uvolnit ceil a T */
    for(T1 = T+2; (p = *T1++) != NULL; ) {
    	INLINEset_or(ceil, ceil, p);
    }
    if (! setp_equal(ceil, cube->fullset)) {
    	ceil_compl = compl_cube(ceil);
        if (ceil_compl == NULL){ /** MM: ak chyba */
            free_cubelist(T);
        	set_free(ceil);
            return FALSE3;
        }
    	(void) set_or(cof, cof, set_diff(ceil, cube->fullset, ceil));
    	set_free(ceil);
    	*Tbar = sf_append(complement(T), ceil_compl); 
    	if (*Tbar == NULL){ /** MM: ak chyba, T a ceil_compl je uz zmazane... */
            set_free(ceil);
            return FALSE3;
        }
    	return TRUE3;
    }
    set_free(ceil);
    /** MM: treba upratat len T */

    /* Collect column counts, determine unate variables, etc. */
    massive_count(T); /** MM: nic sa nealokuje */

    /* If single active variable not factored out above, then tautology ! */
    if (cdata->vars_active == 1) {
    	*Tbar = new_cover(0);
    	free_cubelist(T);
    	if (*Tbar == NULL ) return FALSE3; /** MM: ak chyba */
    	return TRUE3;

    /* Check for unate cover */
    } else if (cdata->vars_unate == cdata->vars_active) {
    	A = map_cover_to_unate(T);
    	free_cubelist(T);
    	if (A == NULL) { /** MM: ak chyba */
    	   return FALSE3;
        }
    	A = unate_compl(A);
    	if (A == NULL) return FALSE3; /** MM: ak chyba, netreba uz nic upratovat; T uz je a povodne A je uz neplatne... */
    	*Tbar = map_unate_to_cover(A);
    	sf_free(A);
    	if (*Tbar == NULL ) return FALSE3; /** MM: ak chyba */
    	return TRUE3;

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

/*
 *  compl_merge -- merge the two cofactors around the splitting
 *  variable
 *
 *  The merge operation involves intersecting each cube of the left
 *  cofactor with cl, and intersecting each cube of the right cofactor
 *  with cr.  The union of these two covers is the merged result.
 *
 *  In order to reduce the number of cubes, a distance-1 merge is
 *  performed (note that two cubes can only combine distance-1 in the
 *  splitting variable).  Also, a simple expand is performed in the
 *  splitting variable (simple implies the covering check for the
 *  expansion is not full containment, but single-cube containment).
 */

/** MM: L a R are disposed of */
static pcover compl_merge(pset *T1, pset_family L, pset_family R, register pset cl, register pset cr, int var, int lifting)
/* T1 = Original ON-set */
/* L, R = Complement from each recursion branch */
/* cl, cr = cubes used for cofactoring */
/* var = splitting variable */
/* lifting = whether to perform lifting or not */
{
    register pcube p, last, pt;
    pcover T, Tbar;
    pcube *L1, *R1;
    int tmp; /** MM: pridane pre navratovu hodnotu compl_lift_onset_complex */

    if (debug & COMPL) {
    	fprintf(debugoutput, "compl_merge: left %d, right %d\n", L->count, R->count);
    	fprintf(debugoutput, "%s (cl)\n%s (cr)\nLeft is\n", pc1(cl), pc2(cr));
    	cprint(L);
    	fprintf(debugoutput, "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 */
    /** MM: nic sa tu nealokuje */
    (void) set_copy(cube->temp[0], cube->var_mask[var]);
    
    /** MM: naraz vytvorenie oboch zoznamov */
    L1 = sf_list(L);
    R1 = sf_list(R);
    /** MM: pri kazdej chybe treba uvolnit L1, R1, L, R! */
    if ( (L1==NULL) || (R1==NULL) ) {
        FREE(L1);
        FREE(R1);
        free_cover(L);
        free_cover(R);
        return NULL;
    }
    /** MM: ak vsetko prebehlo v poriadku, moze sa pristupit k radeniu */
    qsort((void *) (L1), L->count, sizeof(pset), d1_order);
    qsort((void *) (R1), R->count, sizeof(pset), d1_order);

    /* Perform distance-1 merge */
    compl_d1merge(L1, R1); /** MM: nic nealokuje */

    /* Perform lifting */
    switch(lifting) {
    	case USE_COMPL_LIFT_ONSET:
    	    T = cubeunlist(T1);
    	    /** MM: ak nastala chyba... */
    	    if (T==NULL){
                FREE(L1);
                FREE(R1);
                free_cover(L);
                free_cover(R);
                return NULL;
            }
    	    compl_lift_onset(L1, T, cr, var); /** MM: nic nealokuje */
    	    compl_lift_onset(R1, T, cl, var); /** MM: nic nealokuje */
    	    free_cover(T);     	    
    	    break;
    	case USE_COMPL_LIFT_ONSET_COMPLEX:
    	    T = cubeunlist(T1);
    	    /** MM: ak nastala chyba... */
    	    if (T==NULL){
                FREE(L1);
                FREE(R1);
                free_cover(L);
                free_cover(R);
                return NULL;
            }
    	    tmp = compl_lift_onset_complex(L1, T, var); /** MM: alokuje!!! */
    	    if (tmp == 0) /** MM: vykona sa, len ak k chybe nedoslo */
        	    tmp = compl_lift_onset_complex(R1, T, var); /** MM: alokuje!!! */
    	    free_cover(T); /** MM: musi sa uvolnit vzdy */
    	    if (tmp != 0){ /** MM: ak chyba (v prvom, alebo neskor v druhom) */
                FREE(L1);
                FREE(R1);
                free_cover(L);
                free_cover(R);
                return NULL;
            }
    	    break;
    	case USE_COMPL_LIFT:
    	    compl_lift(L1, R1, cr, var); /** MM: nic nealokuje */
    	    compl_lift(R1, L1, cl, var); /** MM: nic nealokuje */
    	    break;
    	case NO_LIFTING:
    	    break;
    }
    FREE(L1);
    FREE(R1);

    /* Re-create the merged cover */
    Tbar = new_cover(L->count + R->count); /** MM: vytvori dostatocne velke pole */
    /** MM: ak nastala chyba... */
    if (Tbar==NULL){
        FREE(L1);
        FREE(R1);
        free_cover(L);
        free_cover(R);
        return NULL;
    }
    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) {
    	fprintf(debugoutput, "Result %d\n", Tbar->count);
    	if (verbose_debug)
    	    cprint(Tbar);
    }

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

/*
 *  compl_lift_simple -- expand in the splitting variable using single
 *  cube containment against the other recursion branch to check
 *  validity of the expansion, and expanding all (or none) of the
 *  splitting variable.
 */
/** MM: nic nealokuje, len upravuje vstupy */
static void compl_lift(pset *A1, pset *B1, pset bcube, int var)
{
    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;
    	    }
    	}
    }
}



/*
 *  compl_lift_onset -- expand in the splitting variable using a
 *  distance-1 check against the original on-set; expand all (or
 *  none) of the splitting variable.  Each cube of A1 is expanded
 *  against the original on-set T.
 */
/** MM: nic nealokuje */
static void compl_lift_onset(pset *A1, pset_family T, pset bcube, int var)
{
    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 : ;
    	}
    }
}

/*
 *  compl_lift_complex -- expand in the splitting variable, but expand all
 *  parts which can possibly expand.
 *  T is the original ON-set
 *  A1 is either the left or right cofactor
 */
/** MM: alokuje jednu cube */
/** MM: fatal zmeneny na fatal2. Chyba=-1, inak 0*/
static int compl_lift_onset_complex(pset *A1, pset_family T, int var)
          			/* A1 array of pointers to new result */
         			/* T original ON-set */
        			/* var which variable we split on */
{
    register int dist;
    register pcube last, p, a, xlower;

    /* for each cube in the complement */
    xlower = new_cube();
    /** MM: prebehla alokacia uspesne? */
    if (!xlower) {
        return -1;
    }
    /** MM: vsetko OK, moze sa prejst k cyklu */
    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) {
            			fatal2("compl: ON-set and OFF-set are not orthogonal");
            			free_cube(xlower); /** MM: nezabudut uvolnit alokovane data */
            			return -1;
        		    } 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);
    	}
    }
    return 0;
}



/*
 *  compl_d1merge -- distance-1 merge in the splitting variable
 */
/** MM: nic nealokuje, len upravuje L1 */
static void compl_d1merge(register pset *L1, register pset *R1)
{
    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);
	}
}



/* compl_cube -- return the complement of a single cube (De Morgan's law) */
/** MM: vrati NULL pri neuspechu; kontroluje aj parameter */
static pcover compl_cube(register pset p)
{
    register pcube diff=cube->temp[7], pdest, mask, full=cube->fullset;
    int var;
    pcover R;
    
    if (p == NULL) return NULL; /** MM: ak neplatny parameter */

    /* Allocate worst-case size cover (to avoid checking overflow) */
    R = new_cover(cube->num_vars);
    if (R == NULL) return NULL; /** MM: ak neuspesna alokacia */

    /* 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;
}

/* simp_comp -- quick simplification of T */
/** MM: uz kontroluje parametre; T vzdy disposes */
/** int pre kontrolu chyby; -1 pre chybu */
/** MM: Tnew a Tbar maju byt neinicializovane ukazatele */
int simp_comp(pset *T, pset_family *Tnew, pset_family *Tbar)
         			/* T will be disposed of */
{
    register pcube cl, cr;
    register int best;
    pcover Tl=NULL, Tr=NULL, Tlbar=NULL, Trbar=NULL; /** MM: inicializacia kvoli dealokacii pri chybe */
    int lifting;
    static int simplify_level = 0;
    int tmp; /** MM: pre navratove hodnoty */
    
    if ( (T==NULL) || (Tnew==NULL) || (Tbar==NULL) ) {
        if (T!=NULL) free_cubelist(T);
        return -1;
    }

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

    tmp = simp_comp_special_cases(T, Tnew, Tbar);
    if (tmp==-1){ /** MM: pridane pre kontrolu chyby */
        free_cubelist(T);
        return -1; /** MM: T uz je disposed */
    } else if (tmp == MAYBE3) { /** MM: pokracuje povodna vetva */
    
    	/* Allocate space for the partition cubes */
    	cl = new_cube();
    	cr = new_cube();
    	if ( (cl==NULL) || (cr==NULL) ) { /** MM: ak chyba alokacie */
            FREE(cl); FREE(cr); return -1;
        }
    	best = binate_split_select(T, cl, cr, COMPL);
    
    	/* Complement the left and right halves */
    	tmp = simp_comp(scofactor(T, cl, best), &Tl, &Tlbar);
    	if (tmp==-1){ /** MM: ak chyba v simp_comp */
            free_cube(cl); free_cube(cr); free_cubelist(T);
            sf_free(Tl); sf_free(Tlbar);
            return -1;
        }
    	tmp = simp_comp(scofactor(T, cr, best), &Tr, &Trbar);
    	if (tmp==-1){ /** MM: ak chyba v simp_comp */
            free_cube(cl); free_cube(cr); free_cubelist(T);
            sf_free(Tl); sf_free(Tlbar);
            sf_free(Tl); sf_free(Tlbar);
            return -1;
        }
    
    	lifting = USE_COMPL_LIFT;
    	*Tnew = compl_merge(T, Tl, Tr, cl, cr, best, lifting); /** Tl a Tr su disposed of */
        if (*Tnew==NULL){ /** MM: ak chyba compl_merge */
            free_cube(cl); free_cube(cr); free_cubelist(T);
            sf_free(Tlbar); sf_free(Trbar);
            return -1;
        }
    	lifting = USE_COMPL_LIFT;
    	*Tbar = compl_merge(T, Tlbar, Trbar, cl, cr, best, lifting); /** Tlbar a Trbar su disposed of */
    	if (*Tbar==NULL){ /** MM: ak chyba compl_merge */
            free_cube(cl); free_cube(cr); free_cubelist(T);
            return -1;
        }
    
    	/* All of this work for nothing ? Let's hope not ... */
    	if ((*Tnew)->count > CUBELISTSIZE(T)) {
    	    sf_free(*Tnew);
    	    *Tnew = cubeunlist(T); /** MM: kontrola posunuta na neskor */
    	}
    
    	free_cube(cl);
    	free_cube(cr);
    	free_cubelist(T);
    	if (*Tnew==NULL){ /** MM: ak chyba vo vetve if (...) cubeunlist(T) */
            return -1;    
        }

    }

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

/** MM: T je disposed, ak je odpoved TRUE3 a aj pri chybe -1 */
/** MM: Tnew a Tbar maju byt neinicializovane ukazatele */
static bool3 simp_comp_special_cases(pset *T, pset_family *Tnew, pset_family *Tbar)
         			/* will be disposed if answer is determined */
             			/* returned only if answer 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 (function is empty) */
    if (T[2] == NULL) {
    	*Tnew = new_cover(1);
    	*Tbar = sf_addset(new_cover(1), cube->fullset);
    	free_cubelist(T);
    	return TRUE3;
    }

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

    /* 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 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);
    	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 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);
	*Tbar = new_cover(1);
	free_cubelist(T);
	return TRUE3;

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

    /* Not much we can do about it */
    } else {
	return MAYBE3;
    }
}

/* simplify -- quick simplification of T */
pcover simplify(pset *T)
         			/* T will be disposed of */
{
    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) == MAYBE3) {

	/* 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 bool3 simplify_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 = simplify(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;
    }
}
