#include <iostream>
#include <stdio.h>
#include "include\cudd.h"
#include "include\cuddInt.h"
#include "include\util.h"
#include "LexAn.h"
//#include <time>
/////////////
#include <ctime>
//#include <conio.h> // jen na getch
//#include <map>
//#include <string>
////////////

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

  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;




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

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


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




void InitBDD(){
  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){
  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){
  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){
    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 **** ///////////////////////////////////////
///////////////////////////////////////////////////////////////////////////

//Function to determine the partitions
// partitions the array and returns the middle index (subscript)
int partition(int *count, int top, int bottom)
{
  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];    // switch elements at positions 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;           // returns middle index
}

//Quick Sort Functions for Descending Order
// (2 Functions)
void quicksort(int * count, int top, int bottom)
{
      // top = subscript of beginning of vector being considered
      // bottom = subscript of end of vector being considered
      // this process uses recursion - the process of calling itself
     int middle;
     if (top < bottom)
    {
          middle = partition(count,top, bottom);
          quicksort(count,top, middle);   // sort top partition
          quicksort(count,middle+1, bottom);    // sort bottom partition
     }

     ///////////////////////////////////////////////////
//     ULOZIT POLE VAH DO GLOBALU????????
     /////////////////////////////////////////////////////
     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=new int[1][1]; //pole termu - vsechny termy
  int **termy;
  termy=new int*[terms];
  for(int i=0;i<terms;i++)termy[i]=new int[prom];

//  int *termy=new int[prom+1][terms+1]; //pole termu - vsechny termy
  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
       //cout<<"vkladam : "<< E.Cislo<<"("<<countLit[abs(E.Cislo)-1]<<")  ,";
       termy[term][abs(E.Cislo)-1]=E.Cislo;
       vahyTermu[term]+=countLit[abs(E.Cislo)-1];
     }else{
       //cout<<endl;
       term=term+1;
       E.Element();
       //cout << "term :  " << term<< "("<<terms<<"+ "<<E.Cislo<<");  " ;
     }
  }

  poleTermu=termy;

  quicksort(vahyTermu,0,terms);
////////////////////////////////////////////////////////////
  /*  for(int i=0;i<terms;i++){
      for(int j=0;j<prom;j++){
         cout << " "<< poleTermu[i][j];
      }
      cout << "   -> " << vahyTermu[i]<< endl;
    }*/
////////////////////////////////////////////////////////////

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


///////////////////////////////////////////////////////////////////////////////////
///////////////// DUMP POLE TERMU DO SOUBORU TEMP - SESTUPNR -> max to min ////////
///////////////////////////////////////////////////////////////////////////////////
void dumpTermDesc(int prom,int term){
  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");
   }
}
///////////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////////
///////////////// DUMP POLE TERMU DO SOUBORU TEMP - VZESTUPNE -> min to max ///////
///////////////////////////////////////////////////////////////////////////////////
void dumpTermAsc(int prom,int term){
  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");
   }
}
///////////////////////////////////////////////////////////////////////////////////






DdNode *AddTerm(LexAn input){
  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){
        //cout<< "1. cisloF+ : " << input.Cislo << endl;
        var=Cudd_bddIthVar(manager,input.Cislo);
        tmp=Cudd_bddAnd(manager,var,fx);
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,fx);
        fx=tmp;
 //       printf( "+pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );
        input.Element();
      }else{
        //cout<< "dalsi cisloF+ : " << input.Cislo << endl;
        var=Cudd_bddIthVar(manager,input.Cislo);
        tmp=Cudd_bddOr(manager,var,fx);
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,fx);
        fx=tmp;
 //       printf( "+pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );
        input.Element();
      }
    }else{

       if(input.Cislo<0 && input.symb==NUMB){
          if(i==0){
            //cout<< " 1. cisloF- : " << input.Cislo << " abs hodnota : "<<abs(input.Cislo)<< endl;
            var=Cudd_bddIthVar(manager,abs(input.Cislo));
            tmp=Cudd_bddAnd(manager,Cudd_Not(var),fx);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(manager,fx);
            fx=tmp;
  //        printf( "-pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );
            input.Element();
          }else{
            //cout<< "dalsi cisloF- : " << input.Cislo << " abs hodnota : "<<abs(input.Cislo)<< endl;
            var=Cudd_bddIthVar(manager,abs(input.Cislo));
            tmp=Cudd_bddOr(manager,Cudd_Not(var),fx);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(manager,fx);
            fx=tmp;
  //        printf( "-pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );
           input.Element();
          }

       }else{
         //if(input.symb!=EOL ){
           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++;
   // input.vypis();
    if(i>inputN){
      input.Error("Chyba - term obsahuje vic promennzch nez je puvodne definovano");
    }

  }

 return fx;
}


void MakeBDD(LexAn input){
   int i=1;
   DdNode *tmp;
   vstup.Element();
   //int nodecount=0;

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

   while(i<=termN){
        cout<< "cislo termu : " << i <<endl;
        startTerm= clock();

           Cudd_RecursiveDeref(manager,f1);
           f1=AddTerm(vstup);
           // Cudd_Ref(f1);


           tmp=Cudd_bddAnd(manager,f,f1);
           Cudd_Ref(tmp);
           Cudd_RecursiveDeref(manager,f);
           f=tmp;
    ///////////////////////////////////////////////////////////////////
    //// **** REORDERING **** /////////////////////////////////////////
//           Cudd_AutodynEnable(manager,CUDD_REORDER_SIFT);
           //Cudd_ReduceHeap(manager, CUDD_REORDER_ANNEALING , 20 );
           //if( (i%10)==0 )Cudd_ReduceHeap(manager, CUDD_REORDER_SIFT , 5 );
          /*if(Cudd_ReadSize(manager)==inputN+1 ){
             if(Cudd_ShuffleHeap(manager,indexLit)==1){
               cout<<"shuftle succesed" << endl;
             }else{
               cout<<"shuftle didn't succed" << endl;
             }
            }
          */

          switch(Konfig){
             case 0:
                    cout << "reordering NONE" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_NONE);
                  /*  if((Cudd_ReadSize(manager)-nodecount)>100000){
                       Cudd_ReduceHeap(manager, CUDD_REORDER_NONE , 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 1:
                    cout << "reordering RANDOM" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM);
                    /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                       Cudd_ReduceHeap(manager,CUDD_REORDER_RANDOM , 20 );
                     }
                     nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 2:
                    cout << "reordering RANDOM_PIVOT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM_PIVOT);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_RANDOM_PIVOT , 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 3:
                    cout << "reordering SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_SIFT);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT , 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 4:
                    cout << "reordering SYMM_SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_SYMM_SIFT);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_SYMM_SIFT , 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 5:
                    cout << "reordering GROUP_SIFT" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_GROUP_SIFT);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_GROUP_SIFT, 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 6:
                    cout << "reordering WINDOW2" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_WINDOW2);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_WINDOW2, 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 7:
                    cout << "reordering ANNEALING" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_ANNEALING);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_ANNEALING, 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    break;
             case 8:
                    cout << "reordering GENETIC" << endl;
                    Cudd_AutodynEnable(manager,CUDD_REORDER_GENETIC);
                   /* if((Cudd_ReadSize(manager)-nodecount)>100000){
                      Cudd_ReduceHeap(manager,CUDD_REORDER_GENETIC, 20 );
                    }
                    nodecount=Cudd_ReadSize(manager);*/
                    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 ****//////////////////////////////////////
              // if(i%10==0){
              fprintf(graph,"%d , ",i);//cislo termu X
              fprintf(graph,"%d ,\n",Cudd_DagSize(f)); // pocet uzlu
              // }
         /////////////////////////////////////////////////////////////////

        if(vstup.Znak==EOF)vstup.Error("Chyba - pocet termu se neshoduje se yadanou hodnotou - chzbi");
        if(vstup.Cislo==0 && vstup.symb==NUMB)vstup.Element();
        if(vstup.symb==EOL)vstup.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) {
            for (i = 1; i < dd->size; i++) {
                v = list[i];
//                cout << "\nv :" << v << "  **  pro i :"<< i <<endl;
                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;
    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.";
//int konfig;

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

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

cout<< "jmeno vstup : "<< jmVstup<<endl;

////////////////////////////////////////////
////// **** 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();
/////////////////////////////////////////////
///// **** Vytvareni BDD **** ///////////////
  Start(vstup);
start_BDDTotal = clock();
  MakeBDD(vstup);
end_BDDTotal = clock();
////////////////////////////////////////////


/*for(int i=0;i<inputN+1;i++){

   cout << " " << Cudd_ReadInvPerm(manager,i) <<"("<< i <<") ";

}
cout<<endl;
*/


///////////////////////////////////////////////////
////// **** Nejkratsi term - cesta do 1 **** //////
/*int xx;
DdNode *xx1;
xx=Cudd_ShortestLength(manager,f,NULL);
cout<< "shortest path length : " << xx <<endl;
xx1=Cudd_ShortestPath(manager,f,NULL,NULL,Cudd_SupportIndex(manager,f));
Cudd_Ref(xx1);
Output_Minterm(manager,xx1,0,2);
Cudd_RecursiveDeref(manager,xx1);*/
///////////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////////////////////////////
/////////// **** 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)*inputN)<=25000000){ // priblizne 100MB - pokud bz bzl vypis vetsi, tak se nevypisuje
    cout <<"Probehl vypis mintermu v poradku (1-OK,0-CHYBA) : "<< Output_Minterm(manager,f,inputN,termN) <<endl;
  }else{
    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 <<"Vzpis graf       : " <<cuddP(manager,f)<<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;
}



