/*
 */

#include "espresso.h"

/*
 *  verify -- check that all minterms of F are contained in (Fold u Dold)
 *  and that all minterms of Fold are contained in (F u Dold).
 */
/** MM: pridana kontrola parametrov */
/** MM: vracia -1 pri alokacnej chybe; inak vracia "verify_error" */
/** MM: vystupy posiela na standardoutput a debugoutput */
bool3 verify(pset_family F, pset_family Fold, pset_family Dold)
{
    pcube p, last, *FD;
    bool3 verify_error = FALSE3;
    
    if ( (F==NULL) || (Fold==NULL) || (Dold==NULL) ) return -1; /** MM: ak chyba parametrov */

    /* Make sure the function didn't grow too large */
    FD = cube2list(Fold, Dold);
    if (FD==NULL) return -1; /** MM: ak chyba alokacie */
    foreach_set(F, last, p)
    	if (! cube_is_covered(FD, p)) {
    	    if (standardoutput!=NULL) fprintf(standardoutput, "some minterm in F is not covered by Fold u Dold\n");
    	    verify_error = TRUE3;
    	    if (verbose_debug) {
                if (debugoutput!=NULL) fprintf(debugoutput, "%s\n", pc1(p)); 
            }
            else break;
    	}
    free_cubelist(FD);

    /* Make sure minimized function covers the original function */
    FD = cube2list(F, Dold);
    if (FD==NULL) return -1; /** MM: ak chyba alokacie */
    foreach_set(Fold, last, p)
    	if (! cube_is_covered(FD, p)) {
    	    if (standardoutput!=NULL) fprintf(standardoutput, "some minterm in Fold is not covered by F u Dold\n");
    	    verify_error = TRUE3;
    	    if (verbose_debug) { 
                if (debugoutput!=NULL) fprintf(debugoutput, "%s\n", pc1(p));
            }
            else break;
    	}
    free_cubelist(FD);

    return verify_error;
}



/*
 *  PLA_verify -- verify that two PLA's are identical
 *
 *  If names are given, row and column permutations are done to make
 *  the comparison meaningful.
 *
 */
/** MM: navratova hodnota zmamena, ci doslo k chybe */
/** MM: TRUE3 = PLA nie su rovnake, FALSE3 = PLA su rovnake, -1 = chyba alokacie */
bool3 PLA_verify(pPLA PLA1, pPLA PLA2)
{
    /* Check if both have names given; if so, attempt to permute to
     * match the names
     */
    if (PLA1->label != NULL && PLA1->label[0] != NULL &&
	   PLA2->label != NULL && PLA2->label[0] != NULL) {
    	if (PLA_permute(PLA1, PLA2) != 0) return -1; /** MM: ak chyba alokacie v PLA_permute */
    } else {
    	if (erroroutput!=NULL) fprintf(erroroutput, "PLA_verify: cannot permute columns without names\n");
        snprintf(errorbuffer, sizeof(errorbuffer), "PLA_verify: cannot permute columns without names"); /** MM: pridane kvoli hlaske pre vynimku */
    	return -1; /* zmenene z TRUE3 na -1 */
    }

    if (PLA1->F->sf_size != PLA2->F->sf_size) {
    	if (erroroutput!=NULL) fprintf(erroroutput, "PLA_verify: PLA's are not the same size\n");
    	snprintf(errorbuffer, sizeof(errorbuffer), "PLA_verify: PLA's are not the same size"); /** MM: pridane kvoli hlaske pre vynimku */
    	return -1; /* zmenene z TRUE3 na -1 */
    }

    return verify(PLA2->F, PLA1->F, PLA1->D);
}



/*
 *  Permute the columns of PLA1 so that they match the order of PLA2
 *  Discard any columns of PLA1 which are not in PLA2
 *  Association is strictly by the names of the columns of the cover.
 */
/** MM: pridana kontrola parametrov */
/** MM: pridany int; alokacna chyba cez -1, inak 0 */
/** MM: pri alokacnej chybe nic nemeni [sf_permute neosetrene] */
int PLA_permute(pPLA PLA1, pPLA PLA2)
{
    register int i, j, *permute, npermute;
    register char *labi;
    char **label;
/*    int strcmp(const char *, const char *); */ /** MM: included via port.h */

    /* determine which columns of PLA1 to save, and place these in the list
     * "permute"; the order in this list is the final output order
     */
    
    if ( (PLA1==NULL) || (PLA2==NULL) ) return -1; 
    
    npermute = 0;
    permute = ALLOC(int, PLA2->F->sf_size);
    if (permute==NULL) return -1; /** MM: ak chyba alokacie */
    /* forward alokacia noveho labelu */
    label = ALLOC(char *, cube->size);
    if (label==NULL){ /** MM: ak chyba alokacie */
        FREE(permute); return -1;
    }
    for(i = 0; i < PLA2->F->sf_size; i++) {
    	labi = PLA2->label[i];
    	for(j = 0; j < PLA1->F->sf_size; j++) {
    	    if (strcmp(labi, PLA1->label[j]) == 0) {
        		permute[npermute++] = j;
        		break;
    	    }
    	}
    }

    /* permute columns */
    if (PLA1->F != NULL) {
    	PLA1->F = sf_permute(PLA1->F, permute, npermute);
    }
    if (PLA1->R != NULL) {
    	PLA1->R = sf_permute(PLA1->R, permute, npermute);
    }
    if (PLA1->D != NULL) {
    	PLA1->D = sf_permute(PLA1->D, permute, npermute);
    }

    /* permute the labels */
    /** MM: kopirovanie existujucich labelov */
    for(i = 0; i < npermute; i++) {
    	label[i] = PLA1->label[permute[i]];
    }
    /** MM: NULLovanie zvysnych labelov */
    for(i = npermute; i < cube->size; i++) {
    	label[i] = NULL;
    }
    FREE(PLA1->label);
    PLA1->label = label;

    FREE(permute);
    return 0;
}



/*
 *  check_consistency -- test that the ON-set, OFF-set and DC-set form
 *  a partition of the boolean space.
 */
/** MM: povodne vracia TRUE3/FALSE3 podla toho, ci doslo k chybe */
/** MM: po novom vracia aj -1 pri alokacnej chybe */
/** MM: akceptupe fp=NULL */
bool3 check_consistency(pPLA PLA, FILE* fp)
{
    bool3 verify_error = FALSE3;
    int tmp;
    pcover T;
    
    if (PLA==NULL) return -1; /** MM: ak chyba parametra */

    T = cv_intersect(PLA->F, PLA->D);
    if (T==NULL) return -1; /** MM: ak chyba alokacie */
    if (T->count == 0){
    	if (fp) fprintf(fp, "ON-SET and DC-SET are disjoint\n");
    }
    else {
    	if (fp) {fprintf(fp, "Some minterm(s) belong to both the ON-SET and DC-SET !\n");}
    	if (verbose_debug)
    	    cprint(T);
    	verify_error = TRUE3;
    }
    if (fp) fflush(fp);
    free_cover(T);

    T = cv_intersect(PLA->F, PLA->R);
    if (T==NULL) return -1; /** MM: ak chyba alokacie */
    if (T->count == 0){
    	if (fp) fprintf(fp, "ON-SET and OFF-SET are disjoint\n");
    }
    else {
    	if (fp) {fprintf(fp, "Some minterm(s) belong to both the ON-SET and OFF-SET !\n");}
    	if (verbose_debug)
    	    cprint(T);
    	verify_error = TRUE3;
    }
    if (fp) fflush(fp);
    free_cover(T);

    T = cv_intersect(PLA->D, PLA->R);
    if (T==NULL) return -1; /** MM: ak chyba alokacie */
    if (T->count == 0){
    	if (fp) fprintf(fp, "DC-SET and OFF-SET are disjoint\n");
    }
    else {
    	if (fp) {fprintf(fp, "Some minterm(s) belong to both the OFF-SET and DC-SET !\n");}
    	if (verbose_debug)
    	    cprint(T);
    	verify_error = TRUE3;
    }
    if (fp) fflush(fp);
    free_cover(T);

    tmp = tautology(cube3list(PLA->F, PLA->D, PLA->R));
    if (tmp == -1) return -1; /** MM: ak chyba v tautology */
    /** MM: pokracuje povodna vetva funkcie */
    if (tmp){
    	if (fp) fprintf(fp, "Union of ON-SET, OFF-SET and DC-SET is the universe\n");
    }
    else {
    	T = complement(cube3list(PLA->F, PLA->D, PLA->R));
    	if (T==NULL) return -1; /** MM: ak chyba alokacie; mohla byt zavolana neskor, ale aspon sa bude vediet, kde to zlyhalo */
    	if (fp) {fprintf(fp, "There are minterms left unspecified !\n");}
    	if (verbose_debug)
    	    cprint(T);
    	verify_error = TRUE3;
    	free_cover(T);
    }
    if (fp) fflush(fp);
    return verify_error;
}
