#include "EspressoLib.h"
#include "tables.h" /* obsahuje len debug_table[] */
#include "espresso.h"
#include <cstdio>
#include <map>

using namespace std;

const char *EspressoException::what() const throw(){
    return errorbuffer;
}

const char *UninitializedPLAException::what() const throw(){
    return "PLA has to be loaded after constructor has been called";
}

/* SABLONA METOD PRE ESPRESSO */
/* int PLA::espressoFunction(){
    if (loaded){
        int ret = 0; //inicializacia na dobre ukoncenie
        long start = ptime();
        // PROLOG
        intro(); //prvotne trace a summary a nastavenie ukazatelov
        
        // VLASTNA FUNKCIA
        {
            
        }
        // EPILOG = print total runtime
        if (summary || trace) {	print_trace(pla->F, "function", ptime()-start); }
        if (ret==-1){ invalidatePLA(); }
        outro(); //znevalidnenie ukazatelov
        return ret;
    } else return -1; 
}
*/
/* KOMPRIMOVANA SABLONA METOD PRE ESPRESSO */
/* int PLA::espressoFunction(){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        // VLASTNA FUNKCIA
       
        if (summary || trace) print_trace(pla->F, "espressoFunction", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        return ret;
    }
    return -1; 
}
*/
/*
int PLA::espressoFunction(){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
                    // VLASTNA FUNKCIA
        }
       
        if (summary || trace) print_trace(pla->F, "espressoFunction", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        return ret;
    }
    return -1; 
}
*/

int PLA::numInstances = 0;
bool PLA::optionsSet = false;
/*----------------------------------------------------------------------------*/
PLA::PLA(){ /* inicializuje ukazatele na globalne struktury */
    if (numInstances++ == 0) srand(314973); /* prva instancia zamiesa cisla */
    pla = NULL;
    loaded = paired = symboliced = symbolic_outputed = phased = false;
    
    output_type = F_type;
    memset(&mycube, 0, sizeof(cube_struct));
    memset(&mycdata, 0, sizeof(cdata_struct));
    mycube.num_vars = 0;
    mycube.temp = NULL;
    if (optionsSet==false) setOptions(EspressoOptions() ); /* na zasobniku docasne vytvori instanciu s NULL vystupmi */
}
/*----------------------------------------------------------------------------*/
PLA::~PLA(){ /* inicializuje ukazatele na globalne struktury */
	cube = &mycube; /* free_PLA aj setdown_cube potrebuju informacie z kocky */
    free_PLA(pla); /* free_PLA() kontroluje ukazatele */
    setdown_cube(&(this->mycube), &(this->mycdata)); /* kontroluje ukazatel */
    cube = NULL;
	sf_cleanup(); //nezabudnut uvolnit pokrytia pre F, D a R ;-)
	sm_cleanup();
    numInstances--;
}
/*----------------------------------------------------------------------------*/
/* output_type sa opat nastavuje do defautu */
void PLA::loadFromFile(const char* filename) throw (EspressoException){ /* inicializuje ukazatele na globalne struktury */
    if (loadForeword() != 0 || (filename==NULL) ) {
        outro();
        throw EspressoOperationException(); /* memory allocation error */
    }
    
    
    /* nacitanie samotnej logickej funkcie */
    FILE *fp = fopen(filename, "r"); /* otvorenie suboru */
    int ret = 0;
    if (fp!=NULL){
        pla->filename = util_strsav(filename);
        if (pla->filename != NULL){ /* ak chyba alokacie */
            ::filename = pla->filename;
            /** samotne nacitanie */
            ret = read_pla(fp, pla);
        }
        else ret = -1;        
        /* spolocna cast */
        fclose(fp); /* zatvorenie suboru */
    } else {
        if (erroroutput!=NULL) fprintf(erroroutput, "espresso: Unable to open %s\n", filename);
        snprintf(errorbuffer, sizeof(errorbuffer), "Unable to open %s\n", filename); /** MM: pridane kvoli hlaske pre vynimku */
        throw EspressoOperationException();
    }
    
    /* spolocna cast */
    if (ret == -1) invalidatePLA(); /* ak sa cokolvek nacitalo alebo ulozilo, treba to pri chybe odstranit */
    else loaded = true;
    outro();
    if (ret==-1) throw EspressoOperationException();
}
/*----------------------------------------------------------------------------*/
// obdoba loadFromFile(const char *filename)
// fp nezatvara
void PLA::loadFromFile(FILE* fp) throw (EspressoException){
    if (loadForeword() != 0 || (fp==NULL) ) {
        outro();
        throw EspressoOperationException(); /* memory allocation error */
    }
    
    int ret = 0;
    pla->filename = util_strsav("(stream)");
    if (pla->filename != NULL){ /* ak chyba alokacie */
        ::filename = pla->filename;
        /** samotne nacitanie */
        ret = read_pla(fp, pla);
    }
    else ret = -1;        
    /* spolocna cast */
    
    if (ret == -1) invalidatePLA(); /* ak sa cokolvek nacitalo alebo ulozilo, treba to pri chybe odstranit */
    else loaded = true;
    outro();
    if (ret==-1) throw EspressoOperationException();
}
/*----------------------------------------------------------------------------*/
void PLA::loadFromString(const char *function) throw (EspressoException){
    if (loadForeword() != 0 || (function == NULL) ) {
        outro();
        throw EspressoOperationException(); /* memory allocation error */
    }
    
    const char *ptr = function;
    int ret = 0;
    /* nacitanie samotnej logickej funkcie */
    pla->filename = util_strsav("(string)");
    if (pla->filename != NULL){ /* ak chyba alokacie */
        ::filename = pla->filename;
        /** samotne nacitanie */
        ret = read_pla_string(&ptr, pla);
    }
    else ret = -1;
    
    if (ret == -1) invalidatePLA(); /* ak sa cokolvek nacitalo alebo ulozilo, treba to pri chybe odstranit */
    else loaded = true;
    outro();
    if (ret==-1) throw EspressoOperationException();
}
/*----------------------------------------------------------------------------*/
bool PLA::isLoaded() const {
    return loaded;
}
/*----------------------------------------------------------------------------*/
bool PLA::hasPhase() const throw (UninitializedPLAException) {
    if (loaded){
        if (pla->phase!=NULL) return true;
        else return false;
    } else throw UninitializedPLAException();    
}
/*----------------------------------------------------------------------------*/
void PLA::setOptions(const EspressoOptions &opt){
    echo_comments = opt.echocomments;		 /* turned off by -eat option */
    echo_unknown_commands = opt.echounknowncommands;	 /* always true ?? */
    force_irredundant = opt.forceirredundant;          /* -nirr command line option */
    skip_make_sparse = opt.skipmakesparse;
    kiss = opt.kiss_;                       /* -kiss command line option */
    recompute_onset = opt.recomputeonset;            /* -onset command line option */
    remove_essential = opt.removeessential;           /* -ness command line option */
    single_expand = opt.singleexpand;              /* -fast command line option */
    debug = opt.debug_;
    verbose_debug = opt.verbose_;
    summary = opt.summary_;                    /* -s command line option */
    trace = opt.trace_;                      /* -t command line option */
    unwrap_onset = opt.unwraponset;               /* -nunwrap command line option */
    use_random_order = opt.userandomorder;		 /* -random command line option */
    use_super_gasp = opt.usesupergasp;		 /* -strong command line option */
    /* outputs */
    tracesumoutput = opt.tracesumout;
    debugoutput = opt.debugout;
    erroroutput = opt.errorout;
    eatoutput = opt.eatout;
    eatdotsoutput = opt.eatdotsout;
    standardoutput = opt.standardout;
    
    optionsSet = true;
}
/*----------------------------------------------------------------------------*/
void PLA::setDefaultOptions(){
    debug = 0;			/* default -d: no debugging info */
    verbose_debug = FALSE3;	/* default -v: not verbose */
    summary = FALSE3;		/* default -s: no summary */
    trace = FALSE3;		/* default -t: no trace information */
    remove_essential = TRUE3;	/* default -e: */
    force_irredundant = TRUE3;
    skip_make_sparse = FALSE3;
    unwrap_onset = TRUE3;
    single_expand = FALSE3;
    recompute_onset = FALSE3;
    use_super_gasp = FALSE3;
    use_random_order = FALSE3;
    kiss = FALSE3;
    
    echo_comments = TRUE3;
    eatoutput = stdout;
    
    echo_unknown_commands = TRUE3;
    eatdotsoutput = stdout;
    
    standardoutput = stdout;
    erroroutput = stderr;
    tracesumoutput = stdout; //ak si program nezapne trace/summary sam, tak sa nebude nic vypisovat; okrem opoall()
    debugoutput = NULL;
    
    optionsSet = true;
}
/*----------------------------------------------------------------------------*/
/* OCCTOOLS copyright */
const char* PLA::copyright(){
    return octtools_copyright;
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"ESPRESSO", KEY_ESPRESSO, 1, TRUE3, TRUE3} */
void PLA::espresso() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            int tmp_unwrap = unwrap_onset;
            pcover Fold = sf_save(pla->F);
            if (Fold!=NULL) { /** MM: ak chyba alokacie zalohy */
                pla->F = ::espresso(pla->F, pla->D, pla->R); /** MM: hlavna funkcia minimalizatora */
                if (pla->F!=NULL){ /** MM: ak chyba v espresso(); povodne F je vzdy zmenene */
                    cost_t cost; int error;
                	EXECUTE(error=::verify(pla->F,Fold,pla->D), VERIFY_TIME, pla->F, cost);
                    if (error) {
                        ret = -1;
                	    pla->F = Fold;
                        check_consistency(pla, standardoutput); /* chyba v check_consistency ma nezaujima, lebo k chybe uz doslo */
                        snprintf(errorbuffer, sizeof(errorbuffer), "espresso(): cover verification failed");
                    } else {
                        free_cover(Fold);
                    }
                }
                else {
                    pla->F = Fold; /* pri chybe Fold nemusim zmazat; zmaze ho invalidatePLA() */
                    ret = -1;
                }
                unwrap_onset = tmp_unwrap; /* spolocne pre if aj else */
            }
            else ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, "espresso", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"exact", KEY_exact, 1, TRUE3, TRUE3} */
void PLA::exact() throw (EspressoException){
    minimizeExact(TRUE3, "exact");
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"qm", KEY_qm, 1, TRUE3, TRUE3} */
void PLA::qm() throw (EspressoException){
    minimizeExact(FALSE3, "qm");
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* je to PRIVATNA METODA!!! */
/* {"qm", KEY_qm, 1, TRUE3, TRUE3} aj {"exact", KEY_exact, 1, TRUE3, TRUE3} */
void PLA::minimizeExact(int exact_cover, const char* function) throw (EspressoException){
    if ( loaded && (function!=NULL) ){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            pcover Fold = sf_save(pla->F);
        	if (Fold!=NULL) { /** MM: ak chyba alokacie zalohy */
            	pla->F = minimize_exact(pla->F, pla->D, pla->R, exact_cover);
            	if (pla->F!=NULL){ /** ak chyba v minimize_exact, tak F je uz dealokovane */
                	cost_t cost; int error;
                	EXECUTE(error=::verify(pla->F,Fold,pla->D), VERIFY_TIME, pla->F, cost);
                	if (error) {
                        sf_free(pla->F);
                	    pla->F = Fold;
                	    check_consistency(pla, standardoutput); /* chyba v check_consistency ma nezaujima, lebo k chybe uz doslo */
                        ret = -1;
                        snprintf(errorbuffer, sizeof(errorbuffer), "minimizeExact(): cover verification failed");
                    }
                    else sf_free(Fold);
            	}
            	else {
                    pla->F = Fold; /* Fold bude zmazane cez invalidatePLA() */
                    ret = -1;
                }
            }
            else ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, function, ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"so", KEY_so, 1, TRUE3, TRUE3} */
/* strategy: 0=minimize, 1=exact */
void PLA::so(int strategy) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            if (strategy < 0 || strategy > 1) {
        	    strategy = 0;
        	}
        	ret = so_espresso(pla, strategy);
        }
       
        if (summary || trace) print_trace(pla->F, "single_output", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"so_both", KEY_so_both, 1, TRUE3, TRUE3} */
/* strategy: 0=minimize, 1=exact */
void PLA::so_both(int strategy) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            if (strategy < 0 || strategy > 1) {
        	    strategy = 0;
        	}
        	ret = so_both_espresso(pla, strategy);
        }
       
        if (summary || trace) print_trace(pla->F, "so_both", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets */
/* {"simplify", KEY_simplify, 1, FALSE3, FALSE3} */
void PLA::simplify() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            pcover Ftmp;
            EXEC(Ftmp = ::simplify(cube1list(pla->F)), "SIMPLIFY  ", pla->F);
        	if (Ftmp == NULL) ret = -1;
            else{
                sf_free(pla->F); 
                pla->F = Ftmp;
            }
        }
        else invalidatePLA();
       
        if (summary || trace) print_trace(pla->F, "simplify", ptime()-start);
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"signature", KEY_signature, 1, TRUE3, TRUE3} */
void PLA::signature() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            pcover Fold = sf_save(pla->F); /** MM: Fold kvoli verify() */
        	if (Fold!=NULL) { /** MM: ak chyba alokacie zalohy */
            	pcover Ftmp = ::signature(pla->F, pla->D, pla->R); /** MM: pridane kvoli memory leaku */
            	/** MM: parametre navonok nemeni */
    			if (Ftmp != NULL) {
                    cost_t cost; int error;
    				sf_free(pla->F); 
    				pla->F = Ftmp;
                	EXECUTE(error=::verify(pla->F,Fold,pla->D), VERIFY_TIME, pla->F, cost);
                	if (error) {
                	    ret = -1;
                	    sf_free(pla->F); 
        				pla->F = Fold;
                	    check_consistency(pla, standardoutput); /* chyba v check_consistency ma nezaujima, lebo k chybe uz doslo */
                	    snprintf(errorbuffer, sizeof(errorbuffer), "signature(): cover verification failed");
                	} else {
                	    free_cover(Fold);
                	}
                }
            	else {
    				ret = -1;
    				sf_free(Fold);
    			} 
            }
            else ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, "signature", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"opo", KEY_opo, 1, TRUE3, TRUE3} */
void PLA::opo(bool exact_minimize, bool repeated, bool skip_sparse) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            /* konverzia boolov na int */
            int strategy = 0;
            if (exact_minimize) strategy += 4; /* opo_exact = (opo_strategy / 4) % 2; */
            if (repeated) strategy += 2; /* opo_repeated = (opo_strategy / 2) % 2; */
            if (skip_sparse) strategy += 1; /* skip sparse = opo_no_make_sparse = opo_strategy % 2; */
            /* samotne opo */
            int tmp_skip = skip_make_sparse;
        	ret = phase_assignment(pla, strategy);
        	skip_make_sparse = tmp_skip;
        }
       
        if (summary || trace) print_trace(pla->F, "opo", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"opoall", KEY_opoall, 1, TRUE3, TRUE3} */
/* strategy: 0=espresso minimalizacia; 1=exaktna minimalizacia; defaultna je espresso */
void PLA::opoall(int first, int last, int strategy) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            if (first < 0 || first >= cube->part_size[cube->output]) {
        	    first = 0;
        	}
        	if (last < 0 || last >= cube->part_size[cube->output]) {
        	    last = cube->part_size[cube->output] - 1;
        	}
        	if (strategy < 0 || strategy > 1) strategy = 0;
        	
        	int tmp_unwrap = unwrap_onset;
        	ret = ::opoall(pla, first, last, strategy);
        	unwrap_onset = tmp_unwrap;
        }
       
        if (summary || trace) print_trace(pla->F, "opoall", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"pair", KEY_pair, 1, TRUE3, TRUE3} */
/* strategy: 0=algebraic, 1=strong, 2=espresso, 3=exact */
void PLA::pair(int strategy) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            if (strategy < 0 || strategy > 3) strategy = 0;
            int tmp_unwrap = unwrap_onset;
        	ret = find_optimal_pairing(pla, strategy);
        	unwrap_onset = tmp_unwrap;
        }
       
        if (summary || trace) print_trace(pla->F, "pair", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"pairall", KEY_pairall, 1, TRUE3, TRUE3} */
/* strategy: 0=minimize, 1=exact, 2=opo */
void PLA::pairall(int strategy) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            if (strategy < 0 || strategy > 2) strategy = 0;
            int tmp_skip = skip_make_sparse;
            int tmp_unwrap = unwrap_onset;
        	ret = pair_all(pla, strategy);
        	skip_make_sparse = tmp_skip;
        	unwrap_onset = tmp_unwrap;
        }
       
        if (summary || trace) print_trace(pla->F, "pairall", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
/* {"union", KEY_union, 2, FALSE3, FALSE3} */
PLA* PLA::_union_(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        PLA *ret = NULL;
        
        if (computeSets(FALSE3, FALSE3, second) == 0) {
            /* moze sa pristupit k priprave noveho PLA */
            try{
                ret = new PLA();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            long start = ptime();
            pPLA PLAstr = new_PLA();
            if (ret!=NULL && PLAstr!=NULL){ /* ak sa vytvorilo nove PLA */
                ret->pla = PLAstr;
                pcover newF;
                
                // samotna operacia, ktora vytvori nove pokrytie F 
                newF = sf_union_no_dispose(pla->F, second->pla->F);
                
                if (newF!=NULL){
                    ret->pla->F = newF;
                    //skopirovanie kocky a ostatnych struktur PLA
                    ret = fillUpPLA(ret); /* tu moze byt ret vymazane a vratene NULL */
                }
                else { /* ak doslo k chybe pri novom pokryti */
                    delete(ret); ret = NULL;
                }
            }
            else { /* ak doslo k chybe pri alokacii PLA alebo PLAt */
                if (ret!=NULL) {delete(ret); ret = NULL;} //volanie destruktoru by nemalo vadit
                if (PLAstr!=NULL) free(PLAstr);
            }
            if (summary || trace) print_trace(pla->F, "_union_", ptime()-start);
        }
        
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* {"xor", KEY_xor, 2, TRUE3, TRUE3} */
PLA* PLA::_xor_(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        PLA *ret = NULL;
        
        if (computeSets(TRUE3, TRUE3, second) == 0) {
            /* moze sa pristupit k priprave noveho PLA */
            try{
                ret = new PLA();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            long start = ptime();
            pPLA PLAstr = new_PLA();
            if (ret!=NULL && PLAstr!=NULL){ /* ak sa vytvorilo nove PLA */
                ret->pla = PLAstr;
                pcover newF;
                
                // samotna operacia, ktora vytvori nove pokrytie F 
                pcover T1 = cv_intersect(pla->F, second->pla->R);
            	pcover T2 = cv_intersect(second->pla->F, pla->R);
            	newF = sf_contain(sf_join(T1, T2)); /* sf_join aj sf_contain vedia pracovat s NULL */
            	free_cover(T1); /* free_cover aka sf_free vie pracovat s NULL */
            	free_cover(T2);

                if (newF!=NULL){ /* chybu staci idchytit az na konci */
                    ret->pla->F = newF;
                    //skopirovanie kocky a ostatnych struktur PLA
                    ret = fillUpPLA(ret); /* tu moze byt ret vymazane a vratene NULL */
                }
                else { /* ak doslo k chybe pri novom pokryti */
                    delete(ret); ret = NULL;
                }
            }
            else { /* ak doslo k chybe pri alokacii PLA alebo PLAt */
                if (ret!=NULL) {delete(ret); ret = NULL;} //volanie destruktoru by nemalo vadit
                if (PLAstr!=NULL) free(PLAstr);
            }
            if (summary || trace) print_trace(pla->F, "_xor_", ptime()-start);
        }
        
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* {"sharp", KEY_sharp, 2, FALSE3, FALSE3} */
PLA* PLA::sharp(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        PLA *ret = NULL;
        
        if (computeSets(FALSE3, FALSE3, second) == 0) {
            /* moze sa pristupit k priprave noveho PLA */
            try{
                ret = new PLA();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            long start = ptime();
            pPLA PLAstr = new_PLA();
            if (ret!=NULL && PLAstr!=NULL){ /* ak sa vytvorilo nove PLA */
                ret->pla = PLAstr;
                pcover newF;
                
                // samotna operacia, ktora vytvori nove pokrytie F 
                newF = cv_sharp(pla->F, second->pla->F);
                
                if (newF!=NULL){
                    ret->pla->F = newF;
                    //skopirovanie kocky a ostatnych struktur PLA
                    ret = fillUpPLA(ret); /* tu moze byt ret vymazane a vratene NULL */
                }
                else { /* ak doslo k chybe pri novom pokryti */
                    delete(ret); ret = NULL;
                }
            }
            else { /* ak doslo k chybe pri alokacii PLA alebo PLAt */
                if (ret!=NULL) {delete(ret); ret = NULL;} //volanie destruktoru by nemalo vadit
                if (PLAstr!=NULL) free(PLAstr);
            }
            if (summary || trace) print_trace(pla->F, "sharp", ptime()-start);
        }
        
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* {"dsharp", KEY_dsharp, 2, FALSE3, FALSE3} */
PLA* PLA::dsharp(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        PLA *ret = NULL;
        
        if (computeSets(FALSE3, FALSE3, second) == 0) {
            /* moze sa pristupit k priprave noveho PLA */
            try{
                ret = new PLA();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            long start = ptime();
            pPLA PLAstr = new_PLA();
            if (ret!=NULL && PLAstr!=NULL){ /* ak sa vytvorilo nove PLA */
                ret->pla = PLAstr;
                pcover newF;
                
                // samotna operacia, ktora vytvori nove pokrytie F 
                newF = cv_dsharp(pla->F, second->pla->F);
            
                if (newF!=NULL){
                    ret->pla->F = newF;
                    //skopirovanie kocky a ostatnych struktur PLA
                    ret = fillUpPLA(ret); /* tu moze byt ret vymazane a vratene NULL */
                }
                else { /* ak doslo k chybe pri novom pokryti */
                    delete(ret); ret = NULL;
                }
            }
            else { /* ak doslo k chybe pri alokacii PLA alebo PLAt */
                if (ret!=NULL) {delete(ret); ret = NULL;} //volanie destruktoru by nemalo vadit
                if (PLAstr!=NULL) free(PLAstr);
            }
            if (summary || trace) print_trace(pla->F, "dsharp", ptime()-start);
        }
        
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* {"intersect", KEY_intersect, 2, FALSE3, FALSE3} */
PLA* PLA::intersect(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        PLA *ret = NULL;
        
        if (computeSets(FALSE3, FALSE3, second) == 0) {
            /* moze sa pristupit k priprave noveho PLA */
            try{
                ret = new PLA();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            long start = ptime();
            pPLA PLAstr = new_PLA();
            if (ret!=NULL && PLAstr!=NULL){ /* ak sa vytvorilo nove PLA */
                ret->pla = PLAstr;
                pcover newF;
                
                // samotna operacia, ktora vytvori nove pokrytie F 
                newF = cv_intersect(pla->F, second->pla->F);

                if (newF!=NULL){
                    ret->pla->F = newF;
                    //skopirovanie kocky a ostatnych struktur PLA
                    ret = fillUpPLA(ret); /* tu moze byt ret vymazane a vratene NULL */
                }
                else { /* ak doslo k chybe pri novom pokryti */
                    delete(ret); ret = NULL;
                }
            }
            else { /* ak doslo k chybe pri alokacii PLA alebo PLAt */
                if (ret!=NULL) {delete(ret); ret = NULL;} //volanie destruktoru by nemalo vadit
                if (PLAstr!=NULL) free(PLAstr);
            }
            if (summary || trace) print_trace(pla->F, "intersect", ptime()-start);
        }
        
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* 1 = PLA su rovnake, 0 = PLA nie su rovnake, -1 = ina chyba */
/* pri chybe nemeni PLA */
/* {"verify", KEY_verify, 2, FALSE3, TRUE3} */
bool PLA::verify(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        int ret = -1; int error; cost_t cost;
        long start = ptime();
        
        if (computeSets(FALSE3, TRUE3, second) == 0) {    
            // samotna operacia
        	EXECUTE(error=::verify(second->pla->F, pla->F, pla->D), VERIFY_TIME, pla->F, cost);
        	if (error == -1){ 
        	   ret = -1; /** ak chyba vo verify, v errorbuffer uz je memory alloction error */
            } else if (error) { //ak error == TRUE3, ret == FALSE3
                ret = FALSE3;
        	    if (standardoutput!=NULL) fprintf(standardoutput, "PLA comparison failed; the PLA's are not equivalent\n");
        	} else {
                ret = TRUE3;
        	    if (standardoutput!=NULL) fprintf(standardoutput, "PLA's compared equal\n");
        	}
        	if (summary || trace) print_trace(pla->F, "verify", ptime()-start);
        }
    	
    	outro();
    	if (ret==-1) throw EspressoOperationException();
		return (ret==TRUE3)?true:false;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* 1 = PLA su rovnake, 0 = PLA nie su rovnake, -1 = ina chyba */
/* {"PLAverify", KEY_PLA_verify, 2, FALSE3, TRUE3} */
bool PLA::PLAverify(PLA* second) throw (EspressoException){
    if (twoPLAsForeword(second) == 0){ /* overi sa nacitanie oboch PLA */
        intro();
        int ret = -1; int error; cost_t cost;
        long start = ptime();
        
        if (computeSets(FALSE3, TRUE3, second) == 0) {
            // samotna operacia
            EXECUTE(error = PLA_verify(pla, second->pla), VERIFY_TIME, pla->F, cost);
        	if (error == -1){ 
        	   ret = -1; /** chyba alokacie pamati v PLA_verify alebo verify */
            } else if (error==TRUE3) {
                ret = FALSE3;
        	    if (standardoutput!=NULL) fprintf(standardoutput, "PLA comparison failed; the PLA's are not equivalent\n");
        	} else {
                ret = TRUE3;
        	    if (standardoutput!=NULL) fprintf(standardoutput, "PLA's compared equal\n");
        	}
        	if (summary || trace) print_trace(pla->F, "PLAverify", ptime()-start);
        }
        
        outro();
        if (ret==-1) throw EspressoOperationException();
		return (ret==TRUE3)?true:false;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets */
/* {"essen", KEY_essen, 1, FALSE3, TRUE3} */
void PLA::essen() throw (EspressoException){
    if (loaded){
        intro(); 
        int ret = 0; long start = ptime();
        
        if ( (ret=computeSets(FALSE3, TRUE3)) == 0 ){
            pset last1, p;
            foreach_set(pla->F, last1, p) {
        	    SET(p, RELESSEN);
        	    RESET(p, NONESSEN);
        	}
        	pcover F;
        	cost_t cost;
        	EXECUTE(F = essential(&(pla->F), &(pla->D)), ESSEN_TIME, pla->F, cost);
        	if (F == NULL){ /** MM: ak chyba */
                ret = -1; /** MM: parametre F a D ostali nezmenene */
            } else {
            	free_cover(F);
            }
        }
        else invalidatePLA();
       
        if (summary || trace) print_trace(pla->F, "essen", ptime()-start);
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"expand", KEY_expand, 1, TRUE3, FALSE3} */
void PLA::expand() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, FALSE3)) == 0 ){
            cost_t cost;
            EXECUTE(pla->F=::expand(pla->F,pla->R,FALSE3),EXPAND_TIME, pla->F, cost);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba v expand; F je dealokovane */
        }
       
        if (summary || trace) print_trace(pla->F, "expand", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"gasp", KEY_gasp, 1, TRUE3, TRUE3} */
void PLA::gasp() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            cost_t cost;
            pla->F = last_gasp(pla->F, pla->D, pla->R, &cost);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba */
        }
       
        if (summary || trace) print_trace(pla->F, "gasp", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"super_gasp", KEY_super_gasp, 1, TRUE3, TRUE3} */
void PLA::super_gasp() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            cost_t cost;
            pla->F = ::super_gasp(pla->F, pla->D, pla->R, &cost);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba */
        }
       
        if (summary || trace) print_trace(pla->F, "super_gasp", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"irred", KEY_irred, 1, FALSE3, TRUE3} */
void PLA::irred() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, TRUE3)) == 0 ){
            cost_t cost;
            EXECUTE(pla->F = irredundant(pla->F, pla->D), IRRED_TIME, pla->F, cost);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba v irredundant */
        }
       
        if (summary || trace) print_trace(pla->F, "irred", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"make_sparse", KEY_make_sparse, 1, TRUE3, TRUE3} */
void PLA::make_sparse() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            pla->F = ::make_sparse(pla->F, pla->D, pla->R);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba make_sparse, tak PLA->F je uz dealokovane */
        }
       
        if (summary || trace) print_trace(pla->F, "make_sparse", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"reduce", KEY_reduce, 1, FALSE3, TRUE3} */
void PLA::reduce() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, TRUE3)) == 0 ){
            cost_t cost;
            EXECUTE(pla->F = ::reduce(pla->F, pla->D), REDUCE_TIME, pla->F, cost);
        	if (pla->F==NULL) ret = -1; /** MM: ak chyba reduce */
        }
       
        if (summary || trace) print_trace(pla->F, "reduce", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"test", KEY_test, 1, TRUE3, TRUE3} */
void PLA::test() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            pcover T, E;
        	T = sf_join(pla->D, pla->R);
        	if (T!=NULL) { /** MM: ak chyba sf_join */
            	cost_t cost;
            	E = new_cover(10); /** MM: irredundant vie pracovat s NULL */
            	sf_free(pla->F); /** MM: povodny ON-set zmaze a dopocita si novy */
            	EXECUTE(pla->F = complement(cube1list(T)), COMPL_TIME, pla->F, cost); /** MM: funckie vedia pracovat s NULL */
            	EXECUTE(pla->F = ::expand(pla->F, T, FALSE3), EXPAND_TIME, pla->F, cost); /** MM: funckie vedia pracovat s NULL */
            	EXECUTE(pla->F = irredundant(pla->F, E), IRRED_TIME, pla->F, cost); /** MM: funckie vedia pracovat s NULL */
            	sf_free(T); /** MM: zmazanie spolocneho pokrytia OFF a DC setu */
            	if (pla->F!=NULL) { /** MM: ak chyba pocas funkcii */
                	T = sf_join(pla->F, pla->R);
                	EXECUTE(pla->D = ::expand(pla->D, T, FALSE3), EXPAND_TIME, pla->D, cost); /** MM: funckie vedia pracovat s NULL */
                	EXECUTE(pla->D = irredundant(pla->D, E), IRRED_TIME, pla->D, cost); /** MM: funckie vedia pracovat s NULL */
                	sf_free(T);
                	sf_free(E);
                	if (pla->D==NULL) ret = -1; /** MM: ak chyba pocas funkcii */
                }
                else {
                    sf_free(E);
                    ret = -1;
                }
            }
            else ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, "test", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
PLA* PLA::copy() throw (EspressoException) {
    if (loaded){
        int tmp = 0;
        PLA *ret;
        try{
            ret = new PLA();
        } catch (exception &e){
            ret = NULL;
            snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            throw EspressoOperationException();
        }
        if ( (ret->pla=new_PLA()) == NULL ) {
            delete(ret); throw EspressoOperationException();
        }
        /* tu zacina solidne kopirovanie a aj inicializacia */
        intro();
        
        /* najskor sa musi vykonat copyCube, lebo keby zlyhalo copyPLA, kocka podla ktorej by sa to nasledne dealokovalo by obsahovala zle hodnoty a doslo by k padu */
        if ( (copyCube(&(ret->mycube), &(ret->mycdata) )!=0) || (copyPLA(ret->pla)!=0) ) tmp = -1;
        else { ret->loaded = true; ret->output_type = output_type; }
        
        outro(); /* najskor outro a az potom delete, lebo delete meni globalne ukazatele!!! */
		if (tmp==-1) { delete ret; throw EspressoOperationException(); }// ak nejaka chyba, tak delete 
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* ked je nespravny poziadavok, tak output_type sa nezmeni */
/* da sa menit aj ked PLA nie je nacitane */
int PLA::seto(const char *type) { /* ukazatele na globalne struktury nastavi na NULL */
    if (type){
        int j;
        for(j = 0; pla_types[j].key != 0; j++) {
            if (strcmp(type, pla_types[j].key+1) == 0) {
                break;
            }    
        }        
        if (pla_types[j].key == 0) {
            if (erroroutput) fprintf(erroroutput, "espresso: bad output type \"%s\"\n", type );
            return -1;
        }        
        output_type = pla_types[j].value;
        return 0;
    }
    return -1;
}
/*----------------------------------------------------------------------------*/
void PLA::print(FILE* target) throw (EspressoException){
    if (loaded == true && target!=NULL){
        int ret = 0; long start = ptime();
        intro(); 
        
        int needs_offset = ( (output_type & R_type) != 0 );
        int needs_dcset = ( (output_type & D_type) != 0 );
        if ((ret=computeSets(needs_offset, needs_dcset)) == 0){
            ret = fprint_pla(target, pla, output_type); /* pri neuspechu sa zmaze PLA, lebo moze dojst k uprave vnutornych dat */
        }
        
        if (summary || trace) print_trace(pla->F, "print", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
void PLA::print(const char *filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using print(const char*)");
        throw EspressoOperationException();
    }
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            print(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename);
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
/* pri kazdej chybe maze PLA */
/* needs_offset = TRUE3; */
void PLA::pos() throw (EspressoException){
    if (loaded == true){
        int ret = 0; long start = ptime();
        intro();
        
		phased = true; /* by sa nedopocitala faza pomocou computeSets */
        if ( (ret = computeSets(TRUE3, FALSE3)) == 0 ){
            pcover onset = pla->F;
            pla->F = pla->R;
            pla->R = onset;
            FREE(pla->phase); /** MM: dealokacia starej phase */
            pla->phase = new_cube();
            if (pla->phase != NULL) { 
                set_diff(pla->phase, cube->fullset, cube->var_mask[cube->num_vars-1]);
            } else ret = -1; /** MM: ak chyba alokacie */
        }       

        if (summary || trace) {	print_trace(pla->F, "pos", ptime()-start); }
        if (ret == -1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
    
}
/*----------------------------------------------------------------------------*/
/* pri kazdej chybe maze PLA */
/* {"lexsort", KEY_lexsort, 1, FALSE3, FALSE3} */
void PLA::lexsort() throw (EspressoException){
    if (loaded == true){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            pla->F = lex_sort(pla->F); /** MM: disposes F */
            if (pla->F==NULL) ret = -1; /** MM: ak chyba v lex_sort */
        }
       
        if (summary || trace) print_trace(pla->F, "lexsort", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
/* pri chybe nemusi znicit PLA */
/* akceptuje aj NULL ukazatel na fp */
/* maze PLA, len pri chybe v computeSets */
/* ak vsetko OK, vrati 1 */
/* {"check", KEY_check, 1, TRUE3, TRUE3} */
bool PLA::check(FILE* target) throw (EspressoException){
    if (target==NULL){
        snprintf(errorbuffer, sizeof(errorbuffer), "must insert valid fd when using check(FILE*)"); /** MM: pridane kvoli hlaske pre vynimku */
        throw EspressoOperationException();
    }
    if (loaded){
        int ret = 0; long start = ptime(); 
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0){
            int error = check_consistency(pla, target); /* ak chyba v check_consistency, PLA netreba zmazat */
            /* check_consistency vracia bool3, ci doslo k chybe, ale check vracia 1, ak je vsetko OK => konverzia navratovej hodnoty */
            if (error==TRUE3) ret = FALSE3;
            else if (error==FALSE3) ret = TRUE3;
            else ret = -1;
        }
        else invalidate = true; /* ak chyba vypoctov pokryti, treba zmazat PLA */
       
        if (summary || trace) print_trace(pla->F, "check_consistency", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* otvori subor a vola check(FILE*) */
bool PLA::check(const char *filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using check(const char*)");
        throw EspressoOperationException();
    }
    bool ret;
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            ret = check(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
        return ret;
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename);
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
/* ON-SET and DC-SET are disjoint? */
/* zmaze PLA len pri chybe v computeSets */
bool PLA::ONDCdisjoint() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(FALSE3, TRUE3)) == 0){
            pcover T = cv_intersect(pla->F, pla->D);
            if (T!=NULL) {
                if (T->count == 0) ret = TRUE3;
                else ret = FALSE3;
                free_cover(T);
            }
            else ret = -1;
        }
        else invalidate = true; /* ak chyba dopoctu pokryti */
       
        if (summary || trace) print_trace(pla->F, "ONDCdisjoint", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets */
/* ON-SET and OFF-SET are disjoint? */
/* needs OFFset */
bool PLA::ONOFFdisjoint() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, FALSE3)) == 0){
            pcover T = cv_intersect(pla->F, pla->R);
            if (T!=NULL) {
                if (T->count == 0) ret = TRUE3;
                else ret = FALSE3;
                free_cover(T);
            }
            else ret = -1;
        }
        else invalidate = true; /* ak chyba dopoctu pokryti */
       
        if (summary || trace) print_trace(pla->F, "ONOFFdisjoint", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets */
/* needs OFF set aj DC set */
/* DC-SET and OFF-SET are disjoint? */
bool PLA::DCOFFdisjoint() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0){
            pcover T = cv_intersect(pla->D, pla->R);
            if (T!=NULL) {
                if (T->count == 0) ret = TRUE3;
                else ret = FALSE3;
                free_cover(T);
            }
            else ret = -1;
        }
        else invalidate = true; /* ak chyba dopoctu pokryti */
       
        if (summary || trace) print_trace(pla->F, "DCOFFdisjoint", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets */
/* needs OFF set aj DC set */
/* je zjednotenie F, D a R vesmir? */
bool PLA::universe() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0){
            ret = tautology(cube3list(pla->F, pla->D, pla->R)); 
            /* ret je -1 pri chybe, 0 pre false a 1 pre true => netreba s tym nic robit */
        }
        else invalidate = true; /* ak chyba dopoctu pokryti */
       
        if (summary || trace) print_trace(pla->F, "universe", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* nemusia sa dopocitavat SETy */        
/* vypisuju sa debug informacie; PLA sa pri chybe nezmaze */
/* {"stats", KEY_stats, 1, FALSE3, FALSE3} */
void PLA::printStats(FILE* target) throw (EspressoException){
    if (loaded && (target!=NULL) ){
        /* intro - kvoli print cost a pc1*/
        cube = &(this->mycube);
        cdata = &(this->mycdata);
        filename = this->pla->filename;
        int ret = 0;
        
        if (computeSets(FALSE3, FALSE3) == 0){
            
            /*--------------------------------------*/
            int var, i;
            symbolic_list_t *p2;
            symbolic_t *p1;
            if (pla->filename)
                fprintf(target, "# PLA is %s", pla->filename);
            if (mycube.num_binary_vars == mycube.num_vars - 1)
        	   fprintf(target, " with %d inputs and %d outputs\n",
        	    mycube.num_binary_vars, mycube.part_size[mycube.num_vars - 1]);
            else {
            	fprintf(target, " with %d variables (%d binary, mv sizes",
            	    mycube.num_vars, mycube.num_binary_vars);
            	for(var = mycube.num_binary_vars; var < mycube.num_vars; var++)
            	    fprintf(target, " %d", mycube.part_size[var]);
            	fprintf(target, ")\n");
            }
            fprintf(target, "# ON-set cost is  %s\n", print_cost(pla->F));
            fprintf(target, "# OFF-set cost is %s\n", print_cost(pla->R));
            fprintf(target, "# DC-set cost is  %s\n", print_cost(pla->D));
            if (pla->phase != NULL)
        	   fprintf(target, "# phase is %s\n", pc1(pla->phase));
            if (pla->pair != NULL) {
            	fprintf(target, "# two-bit decoders:");
            	for(i = 0; i < pla->pair->cnt; i++)
            	    fprintf(target, " (%d %d)", pla->pair->var1[i], pla->pair->var2[i]);
            	fprintf(target, "\n");
            }
            if (pla->symbolic != NIL(symbolic_t)) {
            	for(p1 = pla->symbolic; p1 != NIL(symbolic_t); p1 = p1->next) {
            	    fprintf(target, "# symbolic: ");
            	    for(p2=p1->symbolic_list; p2!=NIL(symbolic_list_t); p2=p2->next) {
                		fprintf(target, " %d", p2->variable);
            	    }
            	    fprintf(target, "\n");
            	}
            }
            if (pla->symbolic_output != NIL(symbolic_t)) {
            	for(p1 = pla->symbolic_output; p1 != NIL(symbolic_t); p1 = p1->next) {
            	    fprintf(target, "# output symbolic: ");
            	    for(p2=p1->symbolic_list; p2!=NIL(symbolic_list_t); p2=p2->next) {
                		fprintf(target, " %d", p2->pos);
            	    }
            	    fprintf(target, "\n");
            	}
            }
            /*--------------------------------------*/
        }
        else ret = -1;
    
        /* outro */
        cube = NULL;
        cdata = NULL;
        filename = NULL;
        if (ret==-1) throw EspressoOperationException();
    } else {
        if (!loaded)
            throw UninitializedPLAException();
        else {
            snprintf(errorbuffer, sizeof(errorbuffer), "must insert valid fd when using printStats(FILE*)"); /** MM: pridane kvoli hlaske pre vynimku */
            throw EspressoOperationException();
        }
    }
}
/*----------------------------------------------------------------------------*/
void PLA::printStats(const char *filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using printStats(const char*)");
        throw EspressoOperationException();
    }
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            printStats(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename); /** MM: pridane kvoli hlaske pre vynimku */
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
#define costToCost(cost1, cost2) cost2.cubes = cost1.cubes;\
    cost2.primes = cost1.primes;\
    cost2.in = cost1.in;\
    cost2.out = cost1.out;\
    cost2.mv = cost1.mv;\
    cost2.total = cost1.total;
/* ak chyba vo vnutri alebo PLA nie je nacitane, vrati NULL */
PLAStats* PLA::getStats() throw (EspressoException){
    if (loaded){
        PLAStats *ret = NULL;
        /* intro - kvoli cover_cost a pc1*/
        cube = &(this->mycube);
        cdata = &(this->mycdata);
        filename = this->pla->filename;
        
        if (computeSets(FALSE3, FALSE3) == 0){

            try {
                ret = new PLAStats();
            } catch (exception &e){
                ret = NULL;
                snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
            }
            if (ret != NULL){
                int var, i;
                symbolic_list_t *p2;
                symbolic_t *p1;
                
                ret->variables = ret->binary_variables = ret->multiplevalued_variables = ret->outputs = 0;
            
                if (pla->filename)
                    ret->source = pla->filename;
                if (mycube.num_binary_vars == mycube.num_vars - 1){
                    ret->variables = mycube.num_vars;
                    ret->binary_variables = mycube.num_binary_vars;
                    ret->outputs = mycube.part_size[mycube.num_vars - 1];
                }
                else {
                    ret->variables = mycube.num_vars;
                    ret->binary_variables = mycube.num_binary_vars;
                    try{
                        ret->mv_sizes.reserve(mycube.num_vars-mycube.num_binary_vars); /* ak zlyha realokacia */
                    } catch (exception &e){
                        snprintf(errorbuffer, sizeof(errorbuffer), e.what());
                        delete(ret);
                        ret = NULL;
                        goto outro;
                    }
                    catch (...){
                        snprintf(errorbuffer, sizeof(errorbuffer), "unknown exception in PLAStats->mv_sizes->reserve");
                        delete(ret);
                        ret = NULL;
                        goto outro;
                    }
                	for(var = mycube.num_binary_vars; var < mycube.num_vars; var++)
                    	ret->mv_sizes.push_back(mycube.part_size[var]);
                }
                cost_t cost;
                cover_cost(pla->F, &cost);
                costToCost(cost, ret->ON_set)
                cover_cost(pla->D, &cost);
                costToCost(cost, ret->DC_set)
                cover_cost(pla->R, &cost);
                costToCost(cost, ret->OFF_set)
    
                if (pla->phase != NULL)
            	   ret->phase = pc1(pla->phase);
                if (pla->pair != NULL) {
                	try{
                    	ret->two_bit_decoders.reserve(pla->pair->cnt);
                    } catch (exception &e){
                        snprintf(errorbuffer, sizeof(errorbuffer), e.what());
                        delete(ret); ret = NULL; goto outro;
                    } catch (...) {
                        snprintf(errorbuffer, sizeof(errorbuffer), "unknown exception in PLAStats->two_bit_decoders->reserve" );
                        delete(ret); ret = NULL; goto outro;
                    }
                	for(i = 0; i < pla->pair->cnt; i++)
                        ret->two_bit_decoders.push_back(std::pair<int, int>(pla->pair->var1[i], pla->pair->var2[i]));
                }
                if (pla->symbolic != NIL(symbolic_t)) {
                    vector<int> tmpvect;
                    try { // kvoli dvom push_backom
                    	for(p1 = pla->symbolic; p1 != NIL(symbolic_t); p1 = p1->next) {
                    	    for(p2=p1->symbolic_list; p2!=NIL(symbolic_list_t); p2=p2->next)
                                tmpvect.push_back(p2->variable);
                            ret->symbolic.push_back(tmpvect);
    						tmpvect.clear();
                    	}
                    } catch (exception &e) {
                        snprintf(errorbuffer, sizeof(errorbuffer), e.what());
                        delete(ret); ret = NULL; goto outro;
                    } catch(...){
                        snprintf(errorbuffer, sizeof(errorbuffer), "unknown exception in vector->push_back()" );
                        delete(ret); ret = NULL; goto outro;
                    }
                }
                if (pla->symbolic_output != NIL(symbolic_t)) {
                    vector<int> tmpvect;
                    try { // kvoli dvom push_backom
                    	for(p1 = pla->symbolic_output; p1 != NIL(symbolic_t); p1 = p1->next) {
                    	    for(p2=p1->symbolic_list; p2!=NIL(symbolic_list_t); p2=p2->next)
                        		tmpvect.push_back(p2->pos);
                    	    ret->symbolic_output.push_back(tmpvect);
    						tmpvect.clear();
                    	}
                    } catch (exception &e){
                        snprintf(errorbuffer, sizeof(errorbuffer), e.what());
                        delete(ret); ret = NULL; goto outro;
                    } catch (...){
                        snprintf(errorbuffer, sizeof(errorbuffer), "unknown exception in vector->push_back()");
                        delete(ret); ret = NULL; goto outro;
                    }
                }
            }
        }
        else ret = NULL;
        
outro: /* spolocna vetva pre dobry aj zly koniec */
        /* outro */
        cube = NULL;
        cdata = NULL;
        filename = NULL;
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* {"taut", KEY_taut, 1, FALSE3, FALSE3} */
/* pri chybe sa PLA neznici */
/* 0 = false, 1 = true, -1 = chyba */
bool PLA::taut() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        ret = tautology(cube1list(pla->F));
       
        if (summary || trace) print_trace(pla->F, "tautology", ptime()-start);
        outro();
        if (ret==-1) throw EspressoOperationException();
        else return (ret==FALSE3)?false:true;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* len otvara a zatvara subor; ostatok obstara printTaut(FILE*) */
bool PLA::printTaut(const char* filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using printTaut(const char*)");
        throw EspressoOperationException();
    }
    bool ret;
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            ret = printTaut(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
        return ret;
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename); /** MM: pridane kvoli hlaske pre vynimku */
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
/* ak target, tak vypise hodnotu v zavislosti na taut() */
bool PLA::printTaut(FILE *target) throw (EspressoException){
    if (target==NULL){
        snprintf(errorbuffer, sizeof(errorbuffer), "must insert valid fd when using printTaut(FILE*)"); /** MM: pridane kvoli hlaske pre vynimku */
        throw EspressoOperationException();
    }
    bool ret = taut(); /* nemusi tu byt try{} catch(){}, lebo netreba nic "zmazat" ani zmenit ukazatele */
    fprintf(target, "ON-set is%sa tautology\n", ret ? " " : " not ");
    return ret;
}
/*----------------------------------------------------------------------------*/
int PLA::inputs() throw (UninitializedPLAException) {
    if (loaded){
        return mycube.num_vars;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
int PLA::outputs() throw (UninitializedPLAException){
    if (loaded){
        return mycube.part_size[mycube.output];
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
/* maze PLA len pri chybe v computeSets */
/* {"equiv", KEY_equiv, 1, TRUE3, TRUE3} */
void PLA::printEquiv(FILE* target) throw (EspressoException){
    if (loaded && (target!=NULL) ){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            ret=find_equiv_outputs(pla, target); 
        }
        else invalidate = true;
       
        if (summary || trace) print_trace(pla->F, "printEquiv", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else {
        if (!loaded)
            throw UninitializedPLAException();
        else {
            snprintf(errorbuffer, sizeof(errorbuffer), "must insert valid fd when using printEquiv(FILE*)"); /** MM: pridane kvoli hlaske pre vynimku */
            throw EspressoOperationException();
        }
    }
}
/*----------------------------------------------------------------------------*/
void PLA::printEquiv(const char *filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using print(const char*)");
        throw EspressoOperationException();
    }
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            printEquiv(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename);
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
/* maze PLA len pri chybe v computeSets */
/* {"equiv", KEY_equiv, 1, TRUE3, TRUE3} */
vector< std::pair<int, int> >* PLA::equiv() throw (EspressoException){
    if (loaded){
        int tmp = 0; long start = ptime();
        vector< std::pair<int, int> > *ret = NULL;
        intro(); 
        try {
            ret = new vector< std::pair<int, int> >();
        } catch (exception &e){
            ret = NULL;
            snprintf(errorbuffer, sizeof(errorbuffer), "%s", e.what() );
        }
        if (ret !=NULL){        
            if ( (tmp=computeSets(TRUE3, TRUE3)) == 0 ){
            /*---------------------------------------*/     
                int i, j, ipart, jpart;
                pcover *R, *F;
            
                makeup_labels(pla);
            
                F = ALLOC(pcover, cube->part_size[cube->output]);
                R = ALLOC(pcover, cube->part_size[cube->output]);
                if ( (F==NULL) || (R==NULL) ) { /** MM: ak chyba alokacie */
                    delete ret; ret = NULL;
                    goto end;
                }
                /** MM: pridane NULLovanie poloziek -> vyuzite pri dealokacii pri chybe */
                for (int i = 0; i < cube->part_size[cube->output]; i++){
                    F[i] = R[i] = NULL;
                }
            
                for(i = 0; i < cube->part_size[cube->output]; i++) {
                	ipart = cube->first_part[cube->output] + i;
                	R[i] = cof_output(pla->R, ipart);
                	F[i] = complement(cube1list(R[i]));
                	if ( (R[i]==NULL) || (F[i]==NULL) ) { /** MM: ak chyba alokacie */
                    	delete ret; ret = NULL;
                        goto cleanup; 
                    }
                }
            	
            	/** MM: samotne plnenie vektora */
                for(i = 0; i < cube->part_size[cube->output]-1; i++) {
                	for(j = i+1; j < cube->part_size[cube->output]; j++) {
                	    ipart = cube->first_part[cube->output] + i;
                	    jpart = cube->first_part[cube->output] + j;

                        try { //kvoli allocator exception
                    	    if (check_equiv(F[i], F[j])) {
                                ret->push_back(std::pair<int, int>(i, j) );
                    	    } else if (check_equiv(F[i], R[j])) {
                                ret->push_back(std::pair<int, int>(i, -j) );
                    	    } else if (check_equiv(R[i], F[j])) {
                                ret->push_back(std::pair<int, int>(-i, j) );
                    	    } else if (check_equiv(R[i], R[j])) {
                                ret->push_back(std::pair<int, int>(-i, -j) );
                    	    }
                        } catch (exception &e) {
                            snprintf(errorbuffer, sizeof(errorbuffer), e.what());
                            delete ret; ret = NULL;
                            goto cleanup;
                        } catch (...) {
                            snprintf(errorbuffer, sizeof(errorbuffer), "unknown exception in vector->push_back()" );
                            delete ret; ret = NULL;
                            goto cleanup;
                        }
                	}
                }
                    
            /** MM: novo pridane navestie, ktore spaja epilog funkcie pre dobry aj zly pripad */
            cleanup:
                for(i = 0; i < cube->part_size[cube->output]; i++) {
                	free_cover(F[i]);
                	free_cover(R[i]);
                }
            end:
                FREE(F);
                FREE(R);
            /*---------------------------------------*/
            }
        }
       
        if (summary || trace) print_trace(pla->F, "equiv", ptime()-start);
        if (tmp==-1) invalidatePLA();
        outro();
        if (ret==NULL) throw EspressoOperationException();
        return ret;
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* PLA maze len pri zlyhani computeSets */
/* {"map", KEY_map, 1, FALSE3, FALSE3} */
void PLA::map(FILE* target) throw (EspressoException){
    if (loaded && (target!=NULL) ){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            ret = ::map(pla->F, target);
        }
        else invalidate = true;
       
        if (summary || trace) print_trace(pla->F, "map", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else {
        if (!loaded)
            throw UninitializedPLAException();
        else {
            snprintf(errorbuffer, sizeof(errorbuffer), "must insert valid fd when using map(FILE*)"); /** MM: pridane kvoli hlaske pre vynimku */
            throw EspressoOperationException();
        }
    }
}
/*----------------------------------------------------------------------------*/
void PLA::map(const char *filename) throw (EspressoException){
    if (filename==NULL) {
        snprintf(errorbuffer, sizeof(errorbuffer), "must input filename when using print(const char*)");
        throw EspressoOperationException();
    }
    FILE *fp = fopen(filename, "w");
    if (fp!=NULL) {
        try {
            map(fp);
        } catch (...){
            fclose(fp);
            throw;
        }
        fclose(fp);
    } else {
        snprintf(errorbuffer, sizeof(errorbuffer), "unable to open file %s", filename);
        throw EspressoOperationException();
    }
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* zmeni vystup PLA na FD_type */
/* {"mapdc", KEY_mapdc, 1, FALSE3, FALSE3} */
void PLA::map_dcset() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            ret = ::map_dcset(pla);
            output_type = FD_type;
        }
       
        if (summary || trace) print_trace(pla->F, "map_dcset", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri chybe zmaze PLA */
/* {"contain", KEY_contain, 1, FALSE3, FALSE3} */
void PLA::contain() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            pla->F = sf_contain(pla->F);
            if (pla->F==NULL) ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, "contain", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri chybe zmaze PLA */
/* {"d1merge", KEY_d1merge, 1, FALSE3, FALSE3} */
void PLA::d1merge(int first, int last) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            if (first < 0 || first >= cube->num_vars) first = 0;
        	if (last < 0 || last >= cube->num_vars) last = cube->num_vars - 1;
        	for(int i = first; i <= last; i++) {
        	    pla->F = ::d1merge(pla->F, i);
        	    if (pla->F==NULL){ /** MM: ak chyba v d1merge */
                    ret = -1;
                    break;
                }
        	}
        }
       
        if (summary || trace) print_trace(pla->F, "d1merge", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri chybe zmaze PLA */
/* {"d1merge_in", KEY_d1merge_in, 1, FALSE3, FALSE3} */
void PLA::d1merge_in() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            for(int i = 0; i < cube->num_binary_vars; i++) {
        	    pla->F = ::d1merge(pla->F, i);
        	    if (pla->F==NULL){ /** MM: ak chyba v d1merge */
                    ret = -1;
                    break;
                }
        	}
        }
       
        if (summary || trace) print_trace(pla->F, "d1merge_in", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* zmaze PLA len pri chybe v computeSets*/
/* {"disjoint", KEY_disjoint, 1, TRUE3, FALSE3} */
void PLA::disjoint() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, FALSE3)) == 0 ){
            pcover Ftmp = make_disjoint(pla->F); /** MM: make_disjoint disposes nic */
        	if (Ftmp==NULL){
                ret = -1;
            } else {
                sf_free(pla->F);
                pla->F=Ftmp;
            }
        }
        else invalidate = true;
       
        if (summary || trace) print_trace(pla->F, "disjoint", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* pri hocijakej chybe zmaze PLA */
/* {"minterms", KEY_minterms, 1, FALSE3, FALSE3} */
void PLA::minterms(int first, int last) throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        intro(); 
        
        if ( (ret=computeSets(FALSE3, FALSE3)) == 0 ){
            if (first < 0 || first >= cube->num_vars) {
        	    first = 0;
        	}
        	if (last < 0 || last >= cube->num_vars) {
        	    last = cube->num_vars - 1;
        	}
        	pla->F = sf_dupl(unravel_range(pla->F, first, last));
        	if (pla->F == NULL) ret = -1;
        }
       
        if (summary || trace) print_trace(pla->F, "minterms", ptime()-start);
        if (ret==-1) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* maze PLA len pri chybe computeSets */
/* {"primes", KEY_primes, 1, FALSE3, TRUE3} */
void PLA::primes() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(FALSE3, TRUE3)) == 0 ){
            pcover Ftmp;
            EXEC(Ftmp = primes_consensus(cube2list(pla->F, pla->D)), "PRIMES     ", pla->F);
        	if (Ftmp == NULL){ /** MM: ak chyba */
        		ret = -1;
        	}else { /** MM: pridane kvoli memory leakom */
        		sf_free(pla->F);
        		pla->F = Ftmp;
        	}
        }
        else invalidate = true;;
       
        if (summary || trace) print_trace(pla->F, "primes", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}
/*----------------------------------------------------------------------------*/
/* maze PLA len pri chybe v computeSets */
/* {"separate", KEY_separate, 1, TRUE3, TRUE3} */
void PLA::separate() throw (EspressoException){
    if (loaded){
        int ret = 0; long start = ptime();
        bool invalidate = false;
        intro(); 
        
        if ( (ret=computeSets(TRUE3, TRUE3)) == 0 ){
            pcover Ftmp = complement(cube2list(pla->D, pla->R));
			if (Ftmp == NULL){
				ret = -1;
			}else {
				sf_free(pla->F);
				pla->F = Ftmp;
			}
        }
        else invalidate = true;
       
        if (summary || trace) print_trace(pla->F, "separate", ptime()-start);
        if (invalidate) invalidatePLA();
        outro();
        if (ret==-1) throw EspressoOperationException();
    } else throw UninitializedPLAException();
}

/*--------------------------- PRIVATNE METODY --------------------------------*/
/*----------------------------------------------------------------------------*/
/* pocita s tym, ze vsetky struktury su inicializovane a naplnene */
int PLA::computeSets(bool3 needs_offset, bool3 needs_dcset){ 
    cost_t cost;
    long time;
    int ret = 0;
    
    needs_offset |= (output_type & R_type) != 0;
    needs_dcset |= (output_type & D_type) != 0;
    
    /* Decide how to break PLA into ON-set, OFF-set and DC-set */
    time = ptime();
	if (!phased){ /* vykona sa to len pri prvom raze */
		if ( pla->phase != NULL || pla->symbolic_output != NULL) {
			needs_offset = TRUE3;
		}
	}
    /** MM: je treba dopocitat OFF-set? */
    if (needs_offset && (pla->pla_type==F_type || pla->pla_type==FD_type)) {
        free_cover(pla->R);
        pla->R = complement(cube2list(pla->F, pla->D));
        if (pla->R == NULL){ /** MM: ak chyba alokacie */
            ret = -1;
            goto cleanup;
        }
        /* MM: treba upravit typ, aby sa to vypocitavalo len raz */
        pla->pla_type |= R_type;
    } 
    /** MM: je treba dopocitat DC-set? */
    else if (needs_dcset && pla->pla_type == FR_type) {
        pcover X, Dtmp; /** MM: Dtmp kvoli kontrole a zalohe pri chybe */
        
        /* hack, why not? */
        X = ::d1merge(sf_join(pla->F, pla->R), cube->num_vars - 1);
        if (X == NULL){ /** MM: ak chyba alokacie */
            ret = -1;
            goto cleanup;
        }
        Dtmp = complement(cube1list(X));
        free_cover(X); /** MM: X je docasne pokrytie pre zjednotenie F a R */
        if (Dtmp == NULL){
			ret = -1;
            goto cleanup;
        } else {
            free_cover(pla->D);
            pla->D = Dtmp;
        }
        /* MM: treba upravit typ, aby sa to vypocitavalo len raz */
        pla->pla_type |= D_type;
    } 
    /** MM: je potreba dopocitat ON-set? */
    else if (pla->pla_type == R_type || pla->pla_type == DR_type) {
        free_cover(pla->F);
        pla->F = complement(cube2list(pla->D, pla->R));
        if (pla->F == NULL){ /** MM: ak chyba alokacie complementu */
            ret = -1;
            goto cleanup;
        }
        /* MM: treba upravit typ, aby sa to vypocitavalo len raz */
        pla->pla_type |= F_type;
    }
    
    /** povodne tomu predchadzala vetva s "pos"; pos() zabrani spusteniu tejto vetvy prostrednictvom toho, ze zmaze pla->phase este pred zavolanim computeSets */
	/* Check for phase rearrangement of the functions */
	if (!phased){ /* vykona sa to len pri prvom raze */
		phased = true;
		if (pla->phase != NULL) { 
			/** MM: set_phase modifikuje ON a OFF set; treba dopocitat OFF-set!!! */
			if (pla->pla_type==F_type || pla->pla_type==FD_type) {
				free_cover(pla->R);
				pla->R = complement(cube2list(pla->F, pla->D));
				if (pla->R == NULL){ /** MM: ak chyba alokacie */
					ret = -1; goto cleanup; /** MM: ak chyba alokacie v complement */
				}
				/* treba upravit typ, aby sa to vypocitavalo len raz */
				pla->pla_type |= R_type;
			} 
			pPLA tmpPLA = set_phase(pla);
			if (tmpPLA==NULL) { ret = -1; goto cleanup; }/** MM: ak chyba alokacie v set_phase */
		}
	}
    
    /* Setup minimization for two-bit decoders */
    if (!paired){ /* vykona sa to len pri prvom raze */
		paired = true;
        if (pla->pair != (ppair) NULL) {
            ret = set_pair(pla);
            if (ret == -1) goto cleanup; /** MM: ak chyba v set_pair */
        }
    }

    if (!symboliced){ /* vykona sa to len pri prvom raze */
		symboliced = true;
        if (pla->symbolic != NIL(symbolic_t)) {
            EXEC(ret = map_symbolic(pla), "MAP-INPUT  ", pla->F);
            if (ret != 0) goto cleanup; /** MM: ak chyba v map_symbolic*/ 
        }
    }

    if (!symbolic_outputed){ /* vykona sa to len pri prvom raze */
		symbolic_outputed = true;
        if (pla->symbolic_output != NIL(symbolic_t)) {
            EXEC(ret = map_output_symbolic(pla), "MAP-OUTPUT ", pla->F);
            if (ret != 0) goto cleanup; /** MM: ak chyba v map_output_symbolic */
            /** MM: prepocitanie noveho off-setu? */
            if (needs_offset) { /* ak treba OFF-set pri tomto spusteni */
                free_cover(pla->R);
                EXECUTE(pla->R=complement(cube2list(pla->F,pla->D)), COMPL_TIME, pla->R, cost);
                if (pla->R==NULL) { ret = -1; goto cleanup; } /* skok je tu momontalne zbytocny, ale ak by sa nieco doplnilo, mohlo by sa stat, ze to zabudnem zmenit */
            }
			else pla->pla_type &= ~R_type; /* aby sa OFF-set prepocital vtedy, ked ho bude treba */
        }
    }

/* navestie pre zjednodusenie */
cleanup:
    if (trace) {
        totals(time, COMPL_TIME, pla->R, &cost);
    }
    return ret;
}
/*-----------------------------------------------------------------------------*/
/* dopocita pokrytia obom PLA a v pripade chyby znevalidni PLA, v ktorom doslo k chybe */
/* ak dojde k chybe, nesmie sa uz volat print_trace a ani ziadna ina funkcia, ktora pracuje s pla->F, lebo pla bude uz dealokovane */
/* -1 pre chybu, 0 = OK */
int PLA::computeSets(bool3 needs_offset, bool3 needs_dcset, PLA* second){
    if (this->computeSets(needs_offset, needs_dcset) != 0){
        invalidatePLA(); return -1;
    }
    else {
        if (second->computeSets(needs_offset, needs_dcset) != 0){
            invalidatePLA(second); return -1;
        }
    }
    return 0;
}
/*-----------------------------------------------------------------------------*/
void PLA::intro(){ /* inicializuje ukazatele na globalne struktury a nastavi total_call[] a total_time[] na nuly*/
    cube = &(this->mycube);
    cdata = &(this->mycdata);
    filename = this->pla->filename;
    /* vynulovanie pocitadiel */
    for (int i = 0; i < TIME_COUNT; i++){
        total_time[i] = total_calls[i] = 0;
    }
    /* Poskytne informacie o verzii a spracovavanom PLA */
    if (summary || trace) {
        if (tracesumoutput!=NULL){
            fprintf(tracesumoutput, "# %s\n", VERSION);
            if (loaded && pla!=NULL) PLA_summary(pla, tracesumoutput); /* lebo intro() je volane aj predtym, nez je funkcia nacitana */
        }
    }
    toggle = TRUE3; /* pridane kvoli tomu, ze povodne bola inicializovana na zaciatku modulu [len raz za spustenie], co teraz prekaza */
    /** MM: az teraz sa moze pristupit k vykonavaniu Espresso funkcii */
}
/*----------------------------------------------------------------------------*/
void PLA::outro(){ /* ukazatele na globalne struktury nastavi na NULL */
    /* Print a runtime summary if trace mode enabled */
    if (trace) {
    	runtime();
    }
    /* samotna dealokacia premennych */
    cube = NULL;
    cdata = NULL;
    filename = NULL;
    /* garbage collection */
    sf_cleanup();
    sm_cleanup();
}
/*----------------------------------------------------------------------------*/
int PLA::loadForeword(){
    /* uvolnenie existuucich struktur */
	cube = &mycube; /* ak existuje pla, tak sa potrebuje dealokovat podla dat obsiahnutych v kocke */
    free_PLA(pla);
    setdown_cube(&(this->mycube), &(this->mycdata));
    mycube.num_binary_vars = -1; mycube.num_vars = -2; /* uprava, aby cube_setup skoncilo neuspechom pri predcasnom volani */
    loaded = paired = symboliced = symbolic_outputed = phased = false;
    
    pla = new_PLA();
    if (pla==NULL) return -1; /* chyba alokacie */
	intro();
    pla->pla_type = FD_type; /* defaultny typ */
    output_type = F_type; /* defaultny typ */
    return 0;
}
/*----------------------------------------------------------------------------*/
/* tvori uvod ku praci s dvomi PLA */
/* overi validnost a nacitanie oboch PLA... */
/* ... a overi pocet a velkosti premennych ulozenych v kocke */
int PLA::twoPLAsForeword(PLA* secondPLA){
    if (loaded){/* musi byt nacitane prve PLA */
        if (secondPLA!=NULL){ /* musi byt validny ukazatel na druhe PLA */
            if (secondPLA->loaded){ /* musi byt nacitane aj druhe PLA */
                /* porovnacie kociek oboch PLA */
                cube_struct *first = &this->mycube;
                cube_struct *second = &secondPLA->mycube;
                if (first->size == second->size){ /* aka sf_size musi byt rovnaka, lebo vacsinou sa pouziva funkcia new_cover, ktora pracuje s implicitnym parametrom cube->size */
                    if ( (first->num_binary_vars == second->num_binary_vars) && (first->num_vars == second->num_vars) ){ /* ak maju rovnaky pocet premennych */
                        /* ak su velkosti mv premennych rovnake v oboch PLA, moze sa pristupit k praci s dvomi PLA */
                        if ( memcmp(&first->part_size[first->num_binary_vars], &second->part_size[first->num_binary_vars], (first->num_vars-first->num_binary_vars-1)*sizeof(int)) == 0 ){
                            return 0;
                        }
                    }
                }
            }
        }
    }
    return -1; /* pri hocijakej chybe sa dostane sem */
}
/*----------------------------------------------------------------------------*/
/* ak nastala chyba v Espresso funkciach a PLA s kockou je poskodene, tak sa zmazu */
void PLA::invalidatePLA(){
    free_PLA(pla); /* potrebuje mat nastavene ukazatele na cube a cdata */
    pla = NULL;
    setdown_cube(&mycube, &mycdata); /* odstrani aj part_size[] a premenne nastavi na "nezmyselne" hodnoty */
    loaded = paired = symboliced = symbolic_outputed = phased = false;
}
/*----------------------------------------------------------------------------*/
/* ak nastala chyba pri vypocte pokryti pri druhom PLA */
void PLA::invalidatePLA(PLA *second){
    cube_struct *oldcube = cube;
    cdata_struct *oldcdata = cdata;
    cube = &second->mycube;
    cdata = &second->mycdata;
    second->invalidatePLA();
    cube = oldcube;
    cdata = oldcdata;
}
/*----------------------------------------------------------------------------*/
/* kontroluje parameter; -1 pri chybe */
/* pocita s tym, ze intro uz bolo zavolane */
int PLA::copyPLA(pPLA destPLA, bool copySets){
    if (destPLA==NULL) return -1;
    int ret = 0; // indikator chyby
    
    /* kopirovanie setov */
    if (copySets){
        if ( (destPLA->F = sf_save(pla->F)) == NULL) ret = -1;
        if (ret==0)
            if ( (destPLA->D = sf_save(pla->D)) == NULL) ret = -1;
        if (ret==0)
            if ( (destPLA->R = sf_save(pla->R)) == NULL) ret = -1;
    }
        
    if (ret==0){
        if (pla->filename!=NULL)
            if ( (destPLA->filename = util_strsav(pla->filename)) == NULL) ret = -1;
    }
    
    destPLA->pla_type = pla->pla_type;
    
    /* kopirovanie phase */
    if (ret==0){
        if (pla->phase!=NULL)
            if ( (destPLA->phase = set_save(pla->phase)) == NULL) ret = -1;
    }
    
    /* kopirovanie pair */
    if (ret==0){
        if (pla->pair!=NULL)
            if ( (destPLA->pair = pair_save(pla->pair, pla->pair->cnt)) == NULL) ret = -1;
    }
    symbolic_list_t *p2, *new_list;
    symbolic_label_t *p3, *new_label; /** MM: kvoli memory leaku na symbolic_label_t */
    symbolic_t *p1, *new_t;
    std::map<char*, char*> labelmap; /* mapa oldlabels na newlabels */
    
    /* kopirovanie symbolic */
    if (ret==0){
        if (pla->symbolic!=NULL){
            new_t = destPLA->symbolic = ALLOC( symbolic_t, 1 );
            if (new_t!=NULL){
                /* hlavny cyklus prechadzania zoznamom symbolic_t */
                for(p1 = pla->symbolic; p1 != NIL(symbolic_t); p1 = p1->next) {
                    new_t->symbolic_list_length = p1->symbolic_list_length;
                    new_t->symbolic_label_length = p1->symbolic_label_length;
                    new_t->symbolic_list = NULL; /* nastavenie na NULL kvoli breaku a predcasnemu ukonceniu cyklu */
                    new_t->symbolic_label = NULL;
                    new_t->next = NULL; 
                    
                    if (p1->symbolic_list!=NULL){
                        new_list = new_t->symbolic_list = ALLOC( symbolic_list_t, 1 );
                        if (new_list==NULL) {ret = -1; break; } /* ak chyba, ukoncenie hlavneho cyklu */
                        /* cyklus kopirovania symbolic_list_t */
                        for(p2 = p1->symbolic_list; p2 != NIL(symbolic_list_t); p2 = p2->next) {
                            new_list->variable = p2->variable;
                            new_list->pos = p2->pos;
                            /* sme uz na konci zoznamu? */
                            if (p2->next!=NULL){ /* ak nie, alokovanie new_listu do dalsieho kola */
                                new_list->next = ALLOC( symbolic_list_t, 1 );
                                new_list = new_list->next;
                                if (new_list==NULL) {
                                    ret = -1; break; /* ak chyba, ukoncenie kopirovania symbolic_list_t */
                                }
                            } 
                            else new_list->next = NULL;
                        }
                    } 
                    
            		if (p1->symbolic_label!=NULL){
                        new_label = new_t->symbolic_label = ALLOC( symbolic_label_t, 1 );
                        if (new_label==NULL) {ret = -1; break; } /* ak chyba, ukoncenie hlavneho cyklu */
                        /* cyklus kopirovania symbolic_label_t */
                        for(p3 = p1->symbolic_label; p3 != NIL(symbolic_label_t); p3 = p3->next) {
                			new_label->label = util_strsav(p3->label);
                            new_label->next = NULL; /* inicializa na NULL, ak by kopirovanie labelu skoncilo zle */
                            /* ulozenie ukazatelov do mapy */
                            labelmap.insert(std::pair<char*, char*>(p3->label, new_label->label));
                            /* sme uz na konci zoznamu? */
                            if (p3->next!=NULL){ /* ak nie, alokovanie new_listu do dalsieho kola */
                                new_label->next = ALLOC( symbolic_label_t, 1 );
                                new_label = new_label->next;
                                if (new_label==NULL) {
                                    ret = -1; break; /* ak chyba, ukoncenie kopirovania symbolic_list_t */
                                }
                            } 
                        }
                    } 
                    
                    if (p1->next!=NULL){ /* ak ma povodny zoznam dalsi prvok, vytvori a posunie sa dalsi prvok aj v novom zozname */
                        new_t->next = ALLOC( symbolic_t, 1 );
                        new_t = new_t->next;
                        if (new_t==NULL){ /* ak chyba alokacie */
                            ret = -1; break;
                        }
                    }
                }
            }
            else ret = -1;
        }
    }
    /* kopirovanie symbolic output */
    if (ret==0){
        if (pla->symbolic_output!=NULL){
            new_t = destPLA->symbolic_output = ALLOC( symbolic_t, 1 );
            if (new_t!=NULL){
                /* hlavny cyklus prechadzania zoznamom symbolic_t */
                for(p1 = pla->symbolic_output; p1 != NIL(symbolic_t); p1 = p1->next) {
                    new_t->symbolic_list_length = p1->symbolic_list_length;
                    new_t->symbolic_label_length = p1->symbolic_label_length;
                    new_t->symbolic_list = NULL; /* nastavenie na NULL kvoli breaku a predcasnemu ukonceniu cyklu */
                    new_t->symbolic_label = NULL;
                    new_t->next = NULL; 
                    
                    if (p1->symbolic_list!=NULL){
                        new_list = new_t->symbolic_list = ALLOC( symbolic_list_t, 1 );
                        if (new_list==NULL) {ret = -1; break; } /* ak chyba, ukoncenie hlavneho cyklu */
                        /* cyklus kopirovania symbolic_list_t */
                        for(p2 = p1->symbolic_list; p2 != NIL(symbolic_list_t); p2 = p2->next) {
                            new_list->variable = p2->variable;
                            new_list->pos = p2->pos;
                            /* sme uz na konci zoznamu? */
                            if (p2->next!=NULL){ /* ak nie, alokovanie new_listu do dalsieho kola */
                                new_list->next = ALLOC( symbolic_list_t, 1 );
                                new_list = new_list->next;
                                if (new_list==NULL) {
                                    ret = -1; break; /* ak chyba, ukoncenie kopirovania symbolic_list_t */
                                }
                            } 
                            else new_list->next = NULL;
                        }
                    } 
                    
            		if (p1->symbolic_label!=NULL){
                        new_label = new_t->symbolic_label = ALLOC( symbolic_label_t, 1 );
                        if (new_label==NULL) {ret = -1; break; } /* ak chyba, ukoncenie hlavneho cyklu */
                        /* cyklus kopirovania symbolic_label_t */
                        for(p3 = p1->symbolic_label; p3 != NIL(symbolic_label_t); p3 = p3->next) {
                			new_label->label = util_strsav(p3->label);
                            new_label->next = NULL; /* inicializa na NULL, ak by kopirovanie labelu skoncilo zle */
                            /* ulozenie ukazatelov do mapy */
                            labelmap.insert(std::pair<char*, char*>(p3->label, new_label->label));
                            /* sme uz na konci zoznamu? */
                            if (p3->next!=NULL){ /* ak nie, alokovanie new_listu do dalsieho kola */
                                new_label->next = ALLOC( symbolic_label_t, 1 );
                                new_label = new_label->next;
                                if (new_label==NULL) {
                                    ret = -1; break; /* ak chyba, ukoncenie kopirovania symbolic_list_t */
                                }
                            } 
                        }
                    } 
                    
                    if (p1->next!=NULL){ /* ak ma povodny zoznam dalsi prvok, vytvori a posunie sa dalsi prvok aj v novom zozname */
                        new_t->next = ALLOC( symbolic_t, 1 );
                        new_t = new_t->next;
                        if (new_t==NULL){ /* ak chyba alokacie */
                            ret = -1; break;
                        }
                    }
                }
            }
            else ret = -1;
        }
    }
    
    /* kopirovanie labelov az na zaver, lebo labelmap obsahuje vsetky ukazatele z zo symbolic a aj nejake nove navyse*/
    /* ak bude ukazatel na povodny label v mape, do pola sa zapise ukazatel na novo alokovany label v symbolic*/
    /* ak sa ukazatel nenajde, alokuje sa novy retazec */
    if (ret==0){
        if (pla->label!=NULL){
            destPLA->label = ALLOC( char*, cube->size);
            if (destPLA->label!=NULL){
                for (int i = 0; i < cube->size; i++) destPLA->label[i] = NULL; /* pociatocne NULLovanie kvoli chybe */
                /* samotne kopirovanie labelov */
                char *tmplabel;
                for (int i = 0; i < cube->size; i++){
                    /* kopirovanie labelu, len ak existuje */
                    if (pla->label[i] != NULL){
                        std::map<char*, char*>::iterator it;
                        it = labelmap.find(pla->label[i]);
                        /* ak label nebol najdeny => strsav */
                        if (it == labelmap.end()){
                            tmplabel = destPLA->label[i] = util_strsav(pla->label[i]);
                            if (tmplabel==NULL){ /* ak chyba alokacie */
                                ret = -1; break;
                            }
                        }
                        /* ak bol label najdeny => dohladanie novej referencie*/
                        else {
                            destPLA->label[i] = it->second;
                        }
                    }
                }                
            }
            /* ak sa nepodarilo alokovat pole label */
            else ret = -1;
        }
    }
    return ret;
}

/*----------------------------------------------------------------------------*/
/* kontroluje parameter; -1 pri chybe */
/* pocita s tym, ze intro uz bolo zavolane */
int PLA::copyCube(cube_struct *destcube, cdata_struct *destcdata) {
    if (destcube==NULL || destcdata==NULL) return -1;
    int ret = 0; /* navratova hodnota a indikator chyby */
    int tmp; /* na ukladanie pomocnych cisel */
    
    /* kopirovanie integralnych typov */
    destcube->size = cube->size;
    destcube->num_vars = cube->num_vars;
    destcube->num_binary_vars = cube->num_binary_vars;
    destcube->num_mv_vars = cube->num_mv_vars;
    destcube->output = cube->output;
    destcube->inmask = cube->inmask;
    destcube->inword = cube->inword;
    destcdata->vars_active = cdata->vars_active;
    destcdata->vars_unate = cdata->vars_unate;
    destcdata->best = cdata->best;

    /* kopirovanie struktur, poli,... pre cube_struct */
    tmp = cube->num_vars;
    destcube->first_part = ALLOC(int, tmp); /* najskor alokacia */
    destcube->last_part = ALLOC(int, tmp);
    destcube->part_size = ALLOC(int, tmp);
    destcube->first_word = ALLOC(int, tmp);
    destcube->last_word = ALLOC(int, tmp);
    if ( (destcube->first_part==NULL) || (destcube->last_part==NULL) || (destcube->first_word==NULL) || (destcube->last_word==NULL) || (destcube->part_size==NULL) ) ret = -1; /** MM: ak chyba alokacie */
        
    if (ret==0){ /* dalsia etapa = kopirovanie */
        memcpy(destcube->first_part, cube->first_part, sizeof(int)*tmp);
        memcpy(destcube->last_part, cube->last_part, sizeof(int)*tmp);
        memcpy(destcube->part_size, cube->part_size, sizeof(int)*tmp);
        memcpy(destcube->first_word, cube->first_word, sizeof(int)*tmp);
        memcpy(destcube->last_word, cube->last_word, sizeof(int)*tmp);
    }
    
    if (ret==0){ /* dalsia alokacia & kopirovanie */
        destcube->sparse = ALLOC(int, tmp);
        destcube->binary_mask = set_save(cube->binary_mask);
        destcube->mv_mask = set_save(cube->mv_mask);
        destcube->fullset = set_save(cube->fullset);
        destcube->emptyset = set_save(cube->emptyset);
        if ( (destcube->binary_mask==NULL) || (destcube->mv_mask==NULL) || (destcube->fullset==NULL) || (destcube->emptyset==NULL) || (destcube->sparse==NULL) ) ret = -1; /** MM: ak chyba alokacie */
        /* namiesto set_save by sa dalo pouzit aj ALLOC( unsigned int, SET_SIZE(NELEM(set)))? */
    }
    
    if (ret==0){ /* kopirovanie */
        memcpy(destcube->sparse, cube->sparse, sizeof(int)*tmp); /* najskor kopirovanie sparse, lebo to ma velkost cube->num_vars */
    }
    
    if (ret==0){ /* alokacia tempu */
        destcube->temp = ALLOC(pset, CUBE_TEMP);
        if (destcube->temp == NULL) ret = -1; /** MM: ak chyba alokacie */
        if (ret==0){
            for(int i = 0; i < CUBE_TEMP; i++) destcube->temp[i] = NULL; /* NULLovanie kvoli dealokacii pri chybe */
            for(int i = 0; i < CUBE_TEMP; i++){
            	destcube->temp[i] = new_cube();
            	if (destcube->temp[i] == NULL) { ret = -1; break; } /** MM: ak chyba alokacie */
            }
        }
    }
    
    if (ret==0){ /* alokacia var_mask */
        destcube->var_mask = ALLOC(pset, tmp);
        if (destcube->var_mask==NULL) ret = -1; /** MM: ak chyba alokacie */
        if (ret==0){
            for(int var = 0; var < tmp; var++) destcube->var_mask[var] = NULL; /* NULLovanie kvoli dealokacii pri chybe */
            for(int var = 0; var < tmp; var++){
                if (cube->var_mask[var]!=NULL){ /* pre istotu, ak by bolo nejake pole prazdne? */
                    destcube->var_mask[var] = set_save(cube->var_mask[var]);
                    if (destcube->var_mask[var]==NULL) { ret = -1; break; } /* ak chyba alokacie */
                }
            }
        }
    }
    
    /* kopirovanie struktur, poli,... pre cdata_struct */
    if (ret==0){
        /* POZN. tmp = cube->num_vars; */
        destcdata->part_zeros = ALLOC(int, cube->size);
        destcdata->var_zeros = ALLOC(int, tmp);
        destcdata->parts_active = ALLOC(int, tmp);
        destcdata->is_unate = ALLOC(int, tmp);
        if ( (destcdata->part_zeros == NULL) || (destcdata->var_zeros == NULL) || (destcdata->parts_active == NULL) || (destcdata->is_unate == NULL) ) ret = -1; /** MM: ak chyba alokacie */    
    }
    if (ret==0){ /* posledne kopirovanie */
        memcpy( destcdata->part_zeros, cdata->part_zeros, sizeof(int)*cube->size);
        memcpy( destcdata->var_zeros, cdata->var_zeros, sizeof(int)*tmp);
        memcpy( destcdata->parts_active, cdata->parts_active, sizeof(int)*tmp);
        memcpy( destcdata->is_unate, cdata->is_unate, sizeof(int)*tmp);
    }

    return ret;
}
/*----------------------------------------------------------------------------*/
/* skopiruje kocku, PLA (okrem OFFsetu) a nastavi globalne premenne */
/* metoda sa pouziva pri vytvoreni produktu operacie nad dvomi PLA */
/* typ bude F alebo FD */
/* output_type zdedi po predkovi */
PLA* PLA::fillUpPLA(PLA* toFill){
    // skopirovanie kocky
    if (copyCube(&toFill->mycube, &toFill->mycdata) != 0) {
        delete(toFill); return NULL;
    }
    else {
        // skopirovanie vnutornosti PLAt
        if (copyPLA(toFill->pla, false) != 0){
            delete(toFill); return NULL;
        }
        else {
            //kopirovanie globalnych premennych a DCsetu
            toFill->loaded = true;
            toFill->paired = paired;
            toFill->symboliced = symboliced;
            toFill->symbolic_outputed = symbolic_outputed;
			toFill->phased = phased;
            toFill->output_type = output_type;
            toFill->pla->R = new_cover(0); // OFFset bude prazdny
            if ( (pla->pla_type & D_type) != 0){ // ak mam DC-set, tak ho skopirujem
                toFill->pla->D = sf_save(pla->D);
                toFill->pla->pla_type = FD_type;            
            }
            else {
                toFill->pla->D = new_cover(0);
                toFill->pla->pla_type = F_type;
            }
            if ( (toFill->pla->D==NULL) || (toFill->pla->R==NULL) ){ // chyba alokacie
                delete(toFill); return NULL;
            }
        }
    }
    return toFill;
}


/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
/*                              ESPRESSOOPTIONS                               */
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
EspressoOptions::EspressoOptions(){
    reset();
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::reset(){
    echocomments = echounknowncommands = forceirredundant = FALSE3;
    skipmakesparse = kiss_ = recomputeonset = FALSE3;
    removeessential = singleexpand = summary_ = FALSE3;
    trace_ = unwraponset = userandomorder = usesupergasp = FALSE3;
    
    debug_ = 0; /* priznak obycajneho debugingu */
    verbose_ = trace_ = summary_ = FALSE3;
    
    tracesumout = debugout = errorout = eatout = eatdotsout =  standardout = NULL;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setEspressoDefaults(){
    debug_ = 0;			/* default -d: no debugging info */
    verbose_ = FALSE3;	/* default -v: not verbose */
    summary_ = FALSE3;		/* default -s: no summary */
    trace_ = FALSE3;		/* default -t: no trace information */
    removeessential = TRUE3;	/* default -e: */
    forceirredundant = TRUE3;
    unwraponset = TRUE3;
    singleexpand = FALSE3;
    recomputeonset = FALSE3;
    usesupergasp = FALSE3;
    userandomorder = FALSE3;
    kiss_ = FALSE3;
    
    echocomments = TRUE3;
    eatout = stdout;
    
    echounknowncommands = TRUE3;
    eatdotsout = stdout;
    
    standardout = stdout;
    errorout = stderr;
    tracesumout = stdout;
    debugout = NULL;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::trace() const{
    return (trace_==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setTrace(bool value){
    trace_ = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::summary() const{
    return (summary_==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setSummary(bool value){
    summary_ = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::debug() const{
    return (debug_==TRUE3)?true:false; /* ak je nenula, tak true */
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setDebug(bool value){
    if (value)
        debug_ = EXPAND + ESSEN + IRRED + REDUCE + SPARSE + GASP + SHARP + MINCOV;
    else {
        debug_ = false;
        setVerboseDebug(false);
    }
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::verboseDebug() const{
    return (verbose_==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setVerboseDebug(bool value){
    verbose_ = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
int EspressoOptions::setVerboseDebug(const char* type){
    verbose_ = TRUE3;
    int j;
	for(j = 0; debug_table[j].name != 0; j++) {
	    if (strcmp(type, debug_table[j].name) == 0) {
			debug_ |= debug_table[j].value;
			break;
	    }
	}
	if (debug_table[j].name == 0) {
	    if (erroroutput) fprintf(erroroutput, "espresso: bad debug type \"%s\"\n", type);
	    return -1;
	}

	return 0;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setTraceSummaryOutput(FILE* fdescr){
    tracesumout = fdescr; /* vystup sa priradi vzdy */
    if (!fdescr){ /* bool3 sa urcia na zaklade hodnoty */
        trace_ = summary_ = FALSE3;
    }
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setDebugOutput(FILE* fdescr){
    debugout = fdescr; /* vystup sa priradi vzdy */
    if (!fdescr){ /* bool3 sa urcia na zaklade hodnoty */
        debug_ = 0;
        verbose_ = FALSE3;
    }
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setErrorOutput(FILE* fdescr){
    errorout = fdescr; /* vystup sa priradi vzdy */
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setEatOutput(FILE* fdescr){
    eatout = fdescr; /* vystup sa priradi vzdy */
    echocomments = (fdescr==NULL)?FALSE3:TRUE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setEatdotsOutput(FILE* fdescr){
    eatdotsout = fdescr; /* vystup sa priradi vzdy */
    echounknowncommands = (fdescr==NULL)?FALSE3:TRUE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setStandardOutput(FILE* fdescr){
    standardout = fdescr; /* funkcie, ktore som nevedel zaradit musia kontrolovat tento deskriptor */
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
void EspressoOptions::setEat(bool value){
    if (value == true && eatout!=NULL) echocomments = TRUE3;
    else echocomments = FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setEatdots(bool value){
    if (value == true && eatdotsout!=NULL) echounknowncommands = TRUE3;
    else echounknowncommands = FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setFast(bool value){
    singleexpand = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setKiss(bool value){
    kiss_ = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setNess(bool value){
    removeessential = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setNirr(bool value){
    forceirredundant = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setNunwrap(bool value){
    unwraponset = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setOnset(bool value){
    recomputeonset = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setRandom(bool value){
    userandomorder = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
void EspressoOptions::setStrong(bool value){
    usesupergasp = value?TRUE3:FALSE3;
}
/*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*/
bool EspressoOptions::eat() const{
    return (echocomments==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::eatdots() const{
    return (echounknowncommands==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::fast() const{
    return (singleexpand==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::kiss() const{
    return (kiss_==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::ness() const{
    return (removeessential==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::nirr() const{
    return (forceirredundant==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::nunwrap() const{
    return (unwraponset==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::onset() const{
    return (recomputeonset==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::random() const{
    return (userandomorder==TRUE3)?true:false;
}
/*----------------------------------------------------------------------------*/
bool EspressoOptions::strong() const{
    return (usesupergasp==TRUE3)?true:false;
}
