#include <iostream>
#include <stdio.h>
#include "include\cudd.h"
#include "include\cuddInt.h"
#include "include\util.h"
#include "LexAn.h"
#include <ctime>

/////////////////

  DdManager * manager;
  DdNode *f, *f1, *one, *zero;
  int inputN=0,termN=0;
  bool SAT=true;
  clock_t start_BDDTotal,end_BDDTotal,startTerm,endTerm;
////////////////////////////////////
  LexAn vstup;
  char* jmVstup;
  char* jmVystup;
  int Konfig=20;
/////////////////////////
  DdNode * background ;
  FILE * vystup;
  FILE * debug;
  FILE * graph;
  int * countLit;
  int * indexLit;
  int pole[4]={3,1,2,0};
  int **poleTermu;
  int vypsano=0;
  long vypsat;

void InitVystup(char * jmVystup){ //INICIALIZUJE VYSTUPNI SOUBOR .pla
   vystup=fopen(jmVystup,"w");
   if(!vystup){
     cout << "\n Chyba - vstupni soubor -> "<< jmVystup <<" nelze vytvorit/nenalezen" << endl;
     exit(1);
   }
}

void InitDebug(char * jmDebug){ //INICIALIZUJE VYSTUPNI SOUBOR DEBUG
   debug=fopen(jmDebug,"w");
   if(!debug){
     cout << "\n Chyba - debug soubor -> "<< jmVystup <<" nelze vytvorit/nenalezen" << endl;
     exit(1);
   }
}

void InitGraph(char * jmVystup){ //INICIALIZUJE VYSTUPNI SOUBOR GRAPH
   graph=fopen(jmVystup,"w");
   if(!graph){
     cout << "\n Chyba - debug soubor -> "<< jmVystup <<" nelze vytvorit/nenalezen" << endl;
     exit(1);
   }
}


void InitBDD(){ // inicializace manageru a nastavení "ukazatelů" nutných pro sestavení BDD
  manager = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
 //inicializace manazeru
  f=Cudd_ReadOne(manager);
  Cudd_Ref(f);
  f1=Cudd_ReadOne(manager);
  Cudd_Ref(f1);
  one = Cudd_ReadOne(manager);
  Cudd_Ref(one);
  zero = Cudd_Not(manager->one);
}


void koment(LexAn input){ //první část syntaktického elementu zpracovávající komentáře
  switch(input.symb){
       case IDENT: case NUMB:
                while((input.symb==NUMB || input.symb==IDENT) && input.symb!=EOL){
                  if(input.symb==NUMB)cout<<input.Cislo << " ";
                  if(input.symb==IDENT)cout<<input.id << " ";
                    input.Element();
                }
                koment(input);
                break;
       case kwC:
                input.Element();
                koment(input);
                break;
       case EOL:
                cout<<"\n";
                input.Element();
                if(input.symb==kwC )koment(input);
                break;
       default: break;
  }
}


void declCNF(LexAn input){ // druhá část syntaktického analyzátoru zpracovávající deklaraci CNF - hlavičku p cnf X X
  if(input.symb==kwCNF){
    input.Element();
    if(input.symb==NUMB){
      cout << "\nPocet vstupu je : " << input.Cislo<<endl;
      inputN=input.Cislo;
      input.Element();
      if(input.symb==NUMB){
        cout << "Pocet radku je : " << input.Cislo<<endl;
        termN=input.Cislo;
      }else{
        input.Error("Chyba - nespravna syntaxe vstupniho souboru - po yadani poctu promennych se ocekava pocet termu");
      }
    }else{
       input.Error("Chyba - nespravna syntaxe vstupniho souboru - po klicovem slove 'cnf' se ocekava Cislo - pocet promennych");
    }
  }else{
    input.Error("Chyba - nespravna syntaxe vstupniho souboru - po klicovem slove 'p' se ocekava 'cnf'");
  }
}


void Start(LexAn input){ // třetí část syntaktického analyzátoru
    input.Element();
    switch(input.symb){
          case kwC:
                   koment(input);
                   input.Element();
                   declCNF(input);
                   break;
          case kwP:
                   input.Element();
                   declCNF(input);
                   break;
          default:
                  input.Error("Chyba - nespravna syntaxe vstupniho souboru");
    }
}

///////////////////////////////////////////////////////////////////////////
////// **** RAZENI - QuickSort **** ///////////////////////////////////////
//////////////////////////////////////////////////////////////////////////

int partition(int *count, int top, int bottom) //funkce rozděluje pole na části a vrací index středu pole
{
  int x = count[top];
  int i = top - 1;
  int j = bottom;
  int temp;

  if(bottom==termN){j=termN;
  }else{ j=bottom+1;}

   do{
     do{
       j --;
     }while (x >count[j]);
     do{
       i++;
     }while (x <count[i]);

     if(i < j){
       temp = count[i];    // prohodí elementy na pozici i and j
       count[i] = count[j];
       count[j] = temp;

       for(int x=0;x<inputN;x++){
         temp = poleTermu[i][x];
         poleTermu[i][x] = poleTermu[j][x];
         poleTermu[j][x] = temp;
       }
     }
   }while (i < j);
return j;           // vrací střední index pole
}

//Quick Sort - pro sestupné pořadí
void quicksort(int * count, int top, int bottom)
{
      // top = udává začátek vektoru který se řadí
      // bottom = udává konec vektoru který se řadí
      // využívá rekurzivní volání sebe sama k nalezení výsledku
     int middle;
     if (top < bottom)
    {
          middle = partition(count,top, bottom);
          quicksort(count,top, middle);   // rovnání horní části pole(top)
          quicksort(count,middle+1, bottom); // rovnání dolní části pole(bottom)
     }
 return;
}

////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////
///////////// ZJISTI VELIKOST ZASTOUPENI PROMENNYCH VE FUNKCI /////////////
///////////////////////////////////////////////////////////////////////////

void varCount(int pocet){ // zjisti kolikrat se promenna vyskytuje ve funkci ...
  FILE * vst;
  LexAn E;
  int term=0;
  int *count=new int[pocet];

  for(int i=0;i<pocet;i++){
    count[i]=0;
  }

  E.InitVstup(jmVstup);
  Start(E);
  vst=fopen(jmVstup,"r");
  if(!vst){
    cout << "\n Chyba - vstupni soubor " <<jmVstup << " nenalezen(pravdepodobne neexistuje)" << endl;
    exit(1);
  }

  E.Element();
  while(E.Znak!=EOF || termN-1>term){
     E.Element();
     if(E.Cislo!=0){
        count[abs(E.Cislo)-1]++;
     }else{
       term++;
     }
  }

////////////////////////////////////////////////////////////
    for(int i=0;i<inputN;i++){
      cout << " " << i <<"("<< count[i] <<")";
     }
////////////////////////////////////////////////////////////
countLit=count;
fclose(vst);
}

///////////////////////////////////////////////////////////////////////////////////

///////////////////////////////////////////////////////////////////////////////////
///////////////// SERADI POLE TERMU PODLE VAH /////////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////

void termOrder(int terms,int prom){ // zjisti kolikrat se promenna vyskytuje ve funkci ...
  FILE * vst;
  LexAn E;
  int term=0;
  int **termy;
  termy=new int*[terms];
  for(int i=0;i<terms;i++)termy[i]=new int[prom];

  int *vahyTermu=new int[terms]; // ke kazdemu termu jeho soucet vah...

    for(int i=0;i<terms;i++){ // inicialiyuju pole termu na same 0
      for(int j=0;j<prom;j++){
        termy[i][j]=0;
      }
      vahyTermu[i]=0;
    }

  E.InitVstup(jmVstup);
  Start(E);
  vst=fopen(jmVstup,"r");
  if(!vst){
    cout << "\n Chyba - vstupni soubor " <<jmVstup << " nenalezen(pravdepodobne neexistuje)" << endl;
    exit(1);
  }


  E.Element();//vezmu prvni element
  while(E.Znak!=EOF || terms-1>term){//){
     E.Element();
     if(E.Cislo!=0){ //odradkovani termu
       termy[term][abs(E.Cislo)-1]=E.Cislo;
       vahyTermu[term]+=countLit[abs(E.Cislo)-1];
     }else{
       term=term+1;
       E.Element();
     }
  }
  poleTermu=termy;

  quicksort(vahyTermu,0,terms);

fclose(vst);
}
///////////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////////
///////////////// DUMP POLE TERMU DO SOUBORU TEMP - SESTUPNR -> max to min ////////
///////////////////////////////////////////////////////////////////////////////////
void dumpTermDesc(int prom,int term){ //provede výpis termů do souboru temp sestupně
  FILE * vystupTemp;
   vystupTemp=fopen("temp.txt","w");
   if(!vystupTemp){
     cout << "\n Chyba - vystupni soubor -> temp.txt nelze vytvorit" << endl;
     exit(1);
   }

   for(int i=0;i<term;i++){
     for(int j=0;j<prom;j++){
       if(poleTermu[i][j]!=0){
         fprintf(vystupTemp,"%d ",poleTermu[i][j]);//cislo termu X
       }
     }
     fprintf(vystupTemp," 0 \n");
   }
 fclose(vystupTemp);
}
///////////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////////
///////////////// DUMP POLE TERMU DO SOUBORU TEMP - VZESTUPNE -> min to max ///////
///////////////////////////////////////////////////////////////////////////////////
void dumpTermAsc(int prom,int term){ //provede výpis termů do souboru temp vzestupně
  FILE * vystupTemp;
  LexAn vstup;
   vystupTemp=fopen("temp.txt","w");
   if(!vystupTemp){
     cout << "\n Chyba - vystupni soubor -> temp.txt nelze vytvorit" << endl;
     exit(1);
   }

   for(int i=term-1;i>=0;i--){
     for(int j=0;j<prom;j++){
       if(poleTermu[i][j]!=0){
         fprintf(vystupTemp,"%d ",poleTermu[i][j]);//cislo termu X
       }
     }
     fprintf(vystupTemp," 0 \n");
   }
   fclose(vystupTemp);
}
///////////////////////////////////////////////////////////////////////////////////



DdNode *AddTerm(LexAn input){ //vytváří ze vstupních termů dílčí podstromy a vrací ukazatel na ně
  int i=0;
  DdNode *tmp, *var,*fx;
  fx=Cudd_ReadOne(manager);
  Cudd_Ref(fx);
  input.Element();

  while(input.Cislo!=0 ){
    if(input.Cislo>0 && input.symb==NUMB){
      if(i==0){
        var=Cudd_bddIthVar(manager,input.Cislo);
        tmp=Cudd_bddAnd(manager,var,fx);
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,fx);
        fx=tmp;
        input.Element();
      }else{
        var=Cudd_bddIthVar(manager,input.Cislo);
        tmp=Cudd_bddOr(manager,var,fx);
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,fx);
        fx=tmp;
        input.Element();
      }
    }else{

       if(input.Cislo<0 && input.symb==NUMB){
          if(i==0){
            var=Cudd_bddIthVar(manager,abs(input.Cislo));
            tmp=Cudd_bddAnd(manager,Cudd_Not(var),fx);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(manager,fx);
            fx=tmp;
            input.Element();
          }else{
            var=Cudd_bddIthVar(manager,abs(input.Cislo));
            tmp=Cudd_bddOr(manager,Cudd_Not(var),fx);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(manager,fx);
            fx=tmp;
            input.Element();
          }

       }else{
           if(input.Znak==EOF)input.Error("Chyba - predcasnz konec souboru");
           input.Error("Chyba - spatna syntaxe vstupu v oblasti deklarace termu je jiny znak nez cislo");
       }
    }
    i++;
    if(i>inputN){
      input.Error("Chyba - term obsahuje vic promennzch nez je puvodne definovano");
    }

  }
 return fx;
}


void MakeBDD(LexAn input){ // funkce spojuje pomocí operace apply dílčí BDD do celkového ROBDD a kontroluje splnitelnost
   int i=1;
   DdNode *tmp;

   input.Element();
   if(Konfig>=10){//kdyz je konfigurace vetsi nez 10 -> pravdepodobnost unsat -> temp + reorder term
     varCount(inputN);
     termOrder(termN,inputN);
     if(Konfig>=20){
       dumpTermAsc(inputN,termN);//vyestupne
       Konfig=Konfig-20; //srovnani konfigu na standartni uroven ... po vytvoreni tempu
     }else{
       if(Konfig>=10 && Konfig<20){
         dumpTermDesc(inputN,termN);//sestupne
         Konfig=Konfig-10; //srovnani konfigu na standartni uroven ... po vytvoreni tempu
       }
     }
     input.InitVstup("temp.txt");
   }

   while(i<=termN){
        cout<< "cislo termu : " << i <<endl;
        startTerm= clock(); // začátek měření doby vytvoření ROBDD
        Cudd_RecursiveDeref(manager,f1);
        f1=AddTerm(input);
        tmp=Cudd_bddAnd(manager,f,f1);
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,f);
        f=tmp;
    ///////////////////////////////////////////////////////////////////
    //// **** REORDERING **** /////////////////////////////////////////
          switch(Konfig){
             case 0:
                    cout << "reordering NONE" << endl;
                    break;
             case 1:
                    cout << "reordering RANDOM" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM);
                    break;
             case 2:
                    cout << "reordering RANDOM_PIVOT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM_PIVOT);
                    break;
             case 3:
                    cout << "reordering SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_SIFT);
                    break;
             case 4:
                    cout << "reordering SYMM_SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_SYMM_SIFT);
                    break;
             case 5:
                    cout << "reordering GROUP_SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_GROUP_SIFT);
                    break;
             case 6:
                    cout << "reordering WINDOW2" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_WINDOW2);
                    break;
             case 7:
                    cout << "reordering ANNEALING" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_ANNEALING);
                    break;
             case 8:
                    cout << "reordering GENETIC" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_GENETIC);
                    break;
           default:
                   cout << "Spatne zadany parametr - konfigurace" << endl;
                   exit(0);
          }

           ////////////////////////////////////////////////////////////
           //// **** Kontrola splnitelnosti **** //////////////////////
           if(Cudd_IsConstant(f)){
             SAT=false;
             break;
           }
           ////////////////////////////////////////////////////////////

           ////////////////////////////////////////////////////////////
           //// **** Garbage collection **** //////////////////////////
           if(Cudd_ReadDead(manager)>30){ // pokud je "dead" uzlu vic nez 30 provede GC.
              cuddGarbageCollect(manager,5);
           }
           ////////////////////////////////////////////////////////////
        endTerm=clock();

        ////////////////////////////////////////////////////////////////////////////
        /////// **** VYSTUPY - STD. + DEBUG + GRAPH **** ///////////////////////////

        //// **** STD. OUTPUT **** ///////////////////////////////////////
           cout << " pocet dead nodes : " << Cudd_ReadDead(manager) << endl;
           cout << " pocet vsech uylu : " << Cudd_DagSize(f) << endl;
           cout << "number of BDD variables in existance : " << Cudd_ReadSize(manager) <<endl;
           cout << " zabrana pamet (manager) - [kB] : " << Cudd_ReadMemoryInUse(manager)/1000<<endl;
           cout << " number of reordering : " << Cudd_ReadReorderings(manager)<<endl;
           cout << "Pridani termu trvalo : " << (endTerm-startTerm)/CLOCKS_PER_SEC << " sekund" <<endl;

        //// **** DEBUG OUTPUT **** //////////////////////////////////////
           fprintf(debug,"\n");
           fprintf(debug,"****  term cislo %d  ****\n",i);
           fprintf(debug,"Pridani termu %d trvalo : %g sekund \n",i,(endTerm-startTerm)/CLOCKS_PER_SEC);
           fprintf(debug,"Pocet dead nodes : %d\n",Cudd_ReadDead(manager));
           fprintf(debug,"Pocet vsech uzlu : %d\n",Cudd_DagSize(f));
           fprintf(debug,"Pamet zabrana managerem [kB] : %d\n",Cudd_ReadMemoryInUse(manager)/1000);
           fprintf(debug,"Number of reorderings : %d\n",Cudd_ReadReorderings(manager));
           fprintf(debug,"Celkova doba tvorby bdd : %g\n",(endTerm-start_BDDTotal)/CLOCKS_PER_SEC);

         //// **** GRAPH OUTPUT ****//////////////////////////////////////
              fprintf(graph,"%d , ",i);//cislo termu X
              fprintf(graph,"%d ,",Cudd_DagSize(f)); // pocet uzlu
              fprintf(graph,"%g ,\n",(endTerm-startTerm)/CLOCKS_PER_SEC);//doba pridani termu
         /////////////////////////////////////////////////////////////////

        if(input.Znak==EOF)input.Error("xx Chyba - pocet termu se neshoduje se yadanou hodnotou - chzbi");
        if(input.Cislo==0 && input.symb==NUMB)input.Element();
        if(input.symb==EOL)input.Element();

      i++;
   }
}
//////////////////////////////////////////////////////////////////////////////





///////////////////////////////////////////////////////////////////////////////////
//////// ****  VYSTUP - tisteni mintermu **** /////////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////
static void PrintMinterm( DdManager * dd, DdNode * node , int * list, int in, int termN ){
    DdNode *N,*Nv,*Nnv;
    int	   i,v,index;
    N = Cudd_Regular(node);

    if (cuddIsConstant(N)) {
        if (node != background && node != zero) {
          if(vypsano< vypsat){
            vypsano++;
            for (i = 1; i < dd->size; i++) {
                v = list[i];

                if (v == 0) (void) fprintf(vystup,"0");
                else if (v == 1) (void) fprintf(vystup,"1");
                else (void) fprintf(vystup,"-");

            }

            (void) fprintf(vystup," % g\n", cuddV(node));
        }
        }
    } else {
        Nv  = cuddT(N);
        Nnv = cuddE(N);
        if (Cudd_IsComplement(node)) {
            Nv  = Cudd_Not(Nv);
            Nnv = Cudd_Not(Nnv);
        }
        index = N->index;
        list[index] = 0;
        PrintMinterm(dd,Nnv,list,in,termN);
        list[index] = 1;
        PrintMinterm(dd,Nv,list,in,termN);
        list[index] = 2;
    }

    return;

}


int Output_Minterm( DdManager *dd, DdNode * node, int in , int termN)
{
    int	i, *list;
    vypsano=0;
    fprintf(vystup,".i %i\n",in);
    fprintf(vystup,".o 1\n");

    background = dd->background;
    zero = Cudd_Not(dd->one);
    list = ALLOC(int,dd->size);
    if (list == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) list[i] = 2;
    PrintMinterm(dd,node,list,in,termN);
    fprintf(vystup,".e\n");
    FREE(list);
    return(1);

}
///////////////////////////////////////////////////////////////////////////////////////////////////



int main(int argc, char *argv[]){

char * jmGraph="Graph.";
char* debugF="Debug.";
long pomX;

  if (argc<5){
     cout << " Musi byt zadany minimalne dva parametry <vstupni soubor> <vystupni soubor> <cislo konfigurace> <pocet vystupnich vektoru>"<<endl;
     exit(0);
  }

  jmVstup=argv[1];
  jmVystup=argv[2];
  Konfig = atoi(argv[3]);
  char * K=argv[3];
  pomX = atoi(argv[4]);

////////////////////////////////////////////
////// **** Inicializace **** //////////////
  strcat(debugF,jmVystup);
  strcat(debugF,"-");
  strcat(debugF,K);
  strcat(debugF,".txt");
  InitDebug(debugF);

  strcat(jmGraph,jmVystup);
  strcat(jmGraph,"-");
  strcat(jmGraph,K);
  strcat(jmGraph,".csv");
  InitGraph(jmGraph);
  vstup.InitVstup(jmVstup);
  InitVystup(jmVystup);
  InitBDD();

///////////////////////////////////////////

if(pomX!=-1){
 vypsat=abs(pomX);
}else{
 vypsat=LONG_MAX;
}



/////////////////////////////////////////////
///// **** Vytvareni BDD **** ///////////////
  Start(vstup);
start_BDDTotal = clock();
  MakeBDD(vstup);
end_BDDTotal = clock();
////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////////////////////////////
/////////// **** Vypis debug **** //////////////////////////////////////////////////////////////
fprintf(debug,"\n");
fprintf(debug,"**************************************************************************\n");
fprintf(debug,"\n");
fprintf(debug,"Vytvoreni BDD trvalo celkem : %g sekund \n",(end_BDDTotal-start_BDDTotal)/CLOCKS_PER_SEC);
fprintf(debug,"Cas straveny reorderingem : %d \n",Cudd_ReadReorderingTime(manager));
fprintf(debug,"Pocet cest do terminalu '1' : %g\n",Cudd_CountPathsToNonZero(f));
////////////////////////////////////////////////////////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////////////////////////////
///////////// **** Vypis vysledku na standartni vystup **** ////////////////////////////////////
  cout << "  *********** Strom vytvoren ************" << endl;
  cout <<"Pocet cest do terminalu '1'       : " <<Cudd_CountPathsToNonZero(f)<<endl;
  cout << endl;
  cout << " **** Parametry BDD **** " << endl;
///////////////////////////////////////////////////////////////////////////////////////
if(Cudd_CountPathsToNonZero(f)>vypsat){
  if((vypsat*inputN)>=25000000){ // priblizne 100MB - pokud bz bzl vypis vetsi, tak se nevypisuje
    fprintf(vystup,"Reseni nebylo vypsano -> vysledek prekrocil max povolenou velikost(100MB)\n");
    fprintf(vystup,"Velikost souboru by byla [MB] : %d \n",((Cudd_CountPathsToNonZero(f)*inputN)*4)/1000000 );
    cout <<"Probehl vypis mintermu neprobehl protoze vystupni soubor by prekrocil max. povolenou velikost"<<endl;
  }
}else{
  if((Cudd_CountPathsToNonZero(f)*inputN)>=25000000){ // priblizne 100MB - pokud bz bzl vypis vetsi, tak se nevypisuje
    fprintf(vystup,"Reseni nebylo vypsano -> vysledek prekrocil max povolenou velikost(100MB)\n");
    fprintf(vystup,"Velikost souboru by byla [MB] : %d \n",((Cudd_CountPathsToNonZero(f)*inputN)*4)/1000000 );
    cout <<"Probehl vypis mintermu neprobehl protoze vystupni soubor by prekrocil max. povolenou velikost"<<endl;
  }
}

cout <<"Probehl vypis mintermu v poradku (1-OK,0-CHYBA) : "<< Output_Minterm(manager,f,inputN,termN) <<endl;

////////////////////////////////////////////////////////////////////////////////////////
  cout <<"Pocet cest do terminalu '1'       : " <<Cudd_CountPathsToNonZero(f)<<endl;
  cout <<"Pocet vsech cest do terminalu     : " << Cudd_CountPath(f) << endl;
  cout <<"Number of reordering              : " << Cudd_ReadReorderings(manager)<<endl;
  cout <<"Zabrana pamet (manager) - [kB] : " << Cudd_ReadMemoryInUse(manager)/1000<<endl;
  cout <<"Pocet \"dead\" uzlů    : " << Cudd_ReadDead(manager) << endl;
  cout <<"Pocet vsech uzlu     : " << Cudd_DagSize(f) << endl;
  cout << "number of BDD variables in existance : " << Cudd_ReadSize(manager) <<endl;
  cout << "Vytvoreni BDD trvalo celkem : " << (end_BDDTotal-start_BDDTotal)/CLOCKS_PER_SEC << " sekund" << endl;
//////////////////////////////////////////////////////////////////////////////////////////////


if(SAT==true){
  cout <<"Funkce JE SPLNITELNA !!!!!"<< endl;
  fprintf(debug,"\n********************************************\nFunkce JE SPLNITELNA !!!!\n");
}else{
  cout <<"Funkce NENI SPLNITELNA !!!!!"<< endl;
  fprintf(debug,"\n********************************************\nFunkce NENI SPLNITELNA !!!!\n");
}

Cudd_RecursiveDeref(manager,f1);
Cudd_RecursiveDeref(manager,f);
Cudd_RecursiveDeref(manager,one);
cout <<"Existuji pred ukoncenim nejake reference ??? : " <<Cudd_CheckZeroRef(manager)<<endl;
Cudd_Quit(manager);
return 0;
}



