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


  DdManager * manager;
  DdNode *f, *f1, *one;
  int inputN=10,termN;

  DdNode *pom0,*pokus,*pom,*pom1;


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);
}


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();
              }
          //  if(input.symb==EOL)cout<<"** eol po ident";
            koment(input);
            break;
       case kwC:
                input.Element();
                koment(input);
                //cout<<"\n";
                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");
    }
}






DdNode *AddTerm(LexAn input){
  int i=0;
  DdNode *tmp, *var,*fx;
  fx=Cudd_ReadOne(manager); //vyvareni bdd x0'*x1'*x2'
  Cudd_Ref(fx);

  //Cudd_RecursiveDeref(manager,f1);
  input.Element();
  while(input.Cislo!=0 ){
  //  input.Element();
  // input.vypis();

    if(input.Cislo>0 && input.symb==NUMB){



      cout<< "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;
    //f1=tmp;
      printf( "+pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );


      input.Element();
    }else{
       if(input.Cislo<0 && input.symb==NUMB){


         cout<< "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;
       //   Cudd_RecursiveDeref(manager,tmp);
         printf( "-pocet uylu TMP : [%d] uzlu\n", Cudd_DagSize( fx) );

         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");
    }
  }

  printf( "***** vracim tmp -> pocet uylu f1 : [%d] uzlu\n", Cudd_DagSize( tmp) );

 return fx;
}


void MakeBDD(LexAn input){
   int i=1;
   DdNode *tmp;
   Cudd_RecursiveDeref(manager,f);
   cout << "termN : " <<termN <<endl;
   input.Element();
   while(i<=termN){ //i<termN){
      if(i<=termN){
        cout<< "cislo termu : " << i <<endl;

        f1=AddTerm(input);
printf("minterm : %d \n",Cudd_CountMinterm( manager, f1, 4));

         cout << "f0(0) -  je terminal? : [" << Cudd_IsConstant( f1 ) <<"] - index je : [" << Cudd_NodeReadIndex(  f1 ) <<"]"<< endl;

        pom0=Cudd_E(f1);
        cout << "f1(2) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_V(  pom0 ) <<"]"<< endl;
        if(pom0==one){
             printf("f1(2) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f1(2) - 0 - je terminal ** '0' **  \n");
           }

        pom1=Cudd_T(f1);
        cout << "f1(2) - 1 - je terminal? : [" << Cudd_IsConstant( pom1 ) <<"] - index je : [" << Cudd_NodeReadIndex(  pom1 ) <<"]"<< endl;
        cout<<endl;
        ////3
        pokus=Cudd_E(pom1);
        pom0=pokus;
        cout << "f1(3) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_V(  pom0 ) <<"]"<< endl;
        if(pom0==one){
            printf("f1(3) - 1 - je terminal ** '1' **  \n");
          }else{
            printf("f1(3) - 1 - je terminal ** '0' **  \n");
          }
        pokus=Cudd_T(pom1);
        pom1=pokus;
        cout << "f1(3) - 1 - je terminal? : [" << Cudd_IsConstant( pom1 ) <<"] - index je : [" << Cudd_NodeReadIndex(  pom1 ) <<"]"<< endl;


        cout<<endl;
        ///4
         cout<< "index : "<<Cudd_NodeReadIndex(  pom1) << endl;
        pokus=Cudd_E(pom1);
        cout << "f1(4) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
        if(pokus==one){
             printf("f1(4) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f1(4) - 0 - je terminal ** '0' **  \n");
           }


        pom1=Cudd_T(pom1);
        cout << "f1(4) - 1 - je terminal? : [" << Cudd_IsConstant( pom1 ) <<"] - index je : [" << Cudd_V( pom1 ) <<"]"<< endl;
        if(pom1==one){
             printf("f1(4) - 1 - je terminal ** '1' **  \n");
           }else{
             printf("f1(4) - 1 - je terminal ** '0' **  \n");
           }



        if(i==1){
          f=f1;
        }else{
           f=Cudd_bddOr(manager,f,f1); //vytvoreni celeho bdd
           Cudd_Ref(f);
        }
        printf( "************************* pocet uylu F : [%d] uzlu\n", Cudd_DagSize( f) );

        Cudd_RecursiveDeref(manager,f1);
        if(input.Znak==EOF)input.Error("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++;
   }

}



int main(){
  LexAn vstup;


  int vst;
  cout << "Zadejte 49slo vstupn9ho testovaneho souboru : ";
  cin >> vst;
  switch(vst){
        case  0:
                vstup.InitVstup("vstup.txt");
                break;
        case  1:
                vstup.InitVstup("vstup1.txt");
                break;
        case  2:
                vstup.InitVstup("vstup2.txt");
                break;
        case  3:
                vstup.InitVstup("vstup3.txt");
                break;
        case  4:
                vstup.InitVstup("vstup4.txt");
                break;

        default:
                vstup.InitVstup("vstup.txt");
                vst=0;
                break;
  }



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

  //vstup.InitVstup("vstup4.txt");
  InitBDD();
  Start(vstup);
  MakeBDD(vstup);
  ////////////////////////////////////////////
  cout << "*********** strom vytvoren ************" << endl;

vst=6;
 switch(vst){
      case 0:
           // *** vypis vstup.txt ***
           pokus = Cudd_E( f ); //uloyi potomka then
           pom0=pokus;
           cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
           pokus = Cudd_T( f ); //ulozi potomka then
           pom1=pokus;
           printf( "f(1) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),Cudd_NodeReadIndex( pokus));
           printf( "\n" );
           //pokus je v X3
           pom = pom1;
           pokus = Cudd_T( pom ); //ulozi potomka then
           printf( "f(3) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ), Cudd_V( pokus ) );
           if(pokus==one){
             printf("f(3) - 1 - je terminal ** '1' **  \n");
           }else{
             printf("f(3) - 1 - je terminal ** '0' **  \n");
           }
           pokus = Cudd_E( pom ); //ulozi potomka then
           printf( "f(3) - 0 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),  Cudd_V( pokus ) );
           if(pokus==one){
             printf("f(3) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f(3) - 0 - je terminal ** '0' **  \n");
           }
           printf( "\n" );
           //pokus je v x2
           pom = pom0;
           pokus = Cudd_E( pom ); //ulozi potomka then
           printf( "f(2) - 0 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ), Cudd_V( pokus ) );
           if(pokus==one){
             printf("f(2) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f(2) - 0 - je terminal ** '0' **  \n");
           }
           pokus = Cudd_T( pom ); //ulozi potomka then
           printf( "f(2) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ), Cudd_NodeReadIndex(  pokus ) );
           printf( "\n" );
           break;

   case 1:
          // *** vrchol vstup1.txt  - x1
          pokus = Cudd_E( f ); //uloyi potomka then
          pom0=pokus;
          cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus = Cudd_T( f ); //ulozi potomka then
          pom1=pokus;
          printf( "f(1) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),Cudd_NodeReadIndex( pokus));
          printf( "\n" );
          // *** pokracujem do x2
          pokus= Cudd_E(pom1);
          cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus=Cudd_T(pom1);
          cout << "f(2) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V( pokus ) <<"]"<< endl;
          if(pokus==one){
             printf("f(2) - 1 - je terminal ** '1' **  \n");
           }else{
             printf("f(2) - 1 - je terminal ** '0' **  \n");
           }
          printf( "\n" );
          // *** pokracujem do x3
          pokus=Cudd_E(pom0);
          cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V( pokus ) <<"]"<< endl;
          if(pokus==one){
             printf("f(3) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f(3) - 0 - je terminal ** '0' **  \n");
           }
          pokus=Cudd_T(pom0);
          cout << "f(3) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
           printf( "\n" );
          // *** pokracujeme do x4 ***
          pom0=Cudd_E(pokus);
          cout << "f(4) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_V( pom0 ) <<"]"<< endl;
          if(pom0==one){
             printf("f(4) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f(4) - 0 - je terminal ** '0' **  \n");
           }
           pom1=Cudd_T(pokus);
           cout << "f(4) - 1 - je terminal? : [" << Cudd_IsConstant( pom1 ) <<"] - index je : [" << Cudd_V(  pom1 ) <<"]"<< endl;
           if(pom1==one){
             printf("f(4) - 1 - je terminal ** '1' **  \n");
           }else{
             printf("f(4) - 1 - je terminal ** '0' **  \n");
           }
           break;
   case 2:
          // *** vrchol vstup2.txt  - x1
          pokus = Cudd_E( f ); //uloyi potomka then
          pom0=pokus;
          cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus = Cudd_T( f ); //ulozi potomka then
          pom1=pokus;
          printf( "f(1) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),Cudd_NodeReadIndex( pokus));
          printf( "\n" );
          // *** pokracujeme v x2
          pokus = Cudd_E( pom0 ); //uloyi potomka then
          pom0=pokus;
          cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus = Cudd_T( pom1 ); //ulozi potomka then
          pom1=pokus;
          printf( "f(2) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pom1 ),Cudd_NodeReadIndex( pom1));
          printf( "\n" );
          // *** pokracujeme v x3
          pokus = Cudd_E( pom0 ); //uloyi potomka then
          cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
             printf("f(3) - 0 - je terminal ** '1' **  \n");
           }else{
             printf("f(3) - 0 - je terminal ** '0' **  \n");
           }
          pokus = Cudd_T( pom1 ); //ulozi potomka then
          printf( "f(3) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),Cudd_V(  pokus ));
          if(pokus==one){
             printf("f(3) - 1 - je terminal ** '1' **  \n");
           }else{
             printf("f(3) - 1 - je terminal ** '0' **  \n");
           }

          printf( "\n" );
          break;
   case 3:
          // *** vrchol vstup3.txt  - x1
          pokus = Cudd_E( f ); //uloyi potomka then
          pom0=pokus;
          cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus = Cudd_T( f ); //ulozi potomka then
          pom1=pokus;
          printf( "f(1) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pokus ),Cudd_NodeReadIndex( pokus));
          printf( "\n" );
          // *** pokracujem x2
          pokus=Cudd_E(pom0);
          pom=pokus;
          cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(2) - 0 - je terminal ** '1' **  \n");
          }else{
            printf("f(2) - 0 - je terminal ** '0' **  \n");
          }
          pokus=Cudd_T(pom0);
          cout << "f(2) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          printf( "\n" );
          // *** pokracujem x3
          pokus = Cudd_E( pom1 );
          cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(3) - 0 - je terminal ** '1' **  \n");
          }else{
            printf("f(3) - 0 - je terminal ** '0' **  \n");
          }
          pokus = Cudd_T( pom1 );
          cout << "f(3) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(3) - 1 - je terminal ** '1' **  \n");
          }else{
            printf("f(3) - 1 - je terminal ** '0' **  \n");
          }
          break;
   case 4:
          // *** vrchol vstup4.txt  - x1
          cout << "f(0) je terminal? : [" << Cudd_IsConstant( f ) <<"] - index je : [" << Cudd_NodeReadIndex(  f ) <<"]"<< endl;
          printf( "\n" );

          pokus = Cudd_E( f ); //uloyi potomka then
          pom0=pokus;
          cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_NodeReadIndex(  pom0 ) <<"]"<< endl;
          pokus = Cudd_T( f ); //ulozi potomka then
          pom1=pokus;
          printf( "f(1) - 1 - je terminal? :[%d]  - index je : [%d] \n", Cudd_IsConstant( pom1 ),Cudd_NodeReadIndex( pom1));
          printf( "\n" );



          // *** pokracujem x2
          pokus=Cudd_E(pom0);
          pom0=pokus;
          cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_NodeReadIndex(  pokus ) <<"]"<< endl;
          pokus=Cudd_T(pom1);
          cout << "f(2) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(2) - 1 - je terminal ** '1' **  \n");
          }else{
            printf("f(2) - 1 - je terminal ** '0' **  \n");
          }
          printf( "\n" );
          // *** pokracujem x3
          pokus=Cudd_E(pom0);
          cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(3) - 0 - je terminal ** '1' **  \n");
          }else{
            printf("f(3) - 0 - je terminal ** '0' **  \n");
          }
          pokus=Cudd_T(pom0);
          cout << "f(3) - 1 - je terminal? : [" << Cudd_IsConstant( pokus ) <<"] - index je : [" << Cudd_V(  pokus ) <<"]"<< endl;
          if(pokus==one){
            printf("f(3) - 1 - je terminal ** '1' **  \n");
          }else{
            printf("f(3) - 1 - je terminal ** '0' **  \n");
          }
          printf( "pocet promennejch : [%d] \n", Cudd_ReadSize( manager ) );
          printf( "pocet uylu : [%d] uzlu\n", Cudd_DagSize( f) );
          break;



   default: break;


 }



//  printf( "pocet promennejch : [%d] \n", Cudd_ReadSize( manager ) );
//   printf( "pocet uylu : [%d] uzlu\n", Cudd_DagSize( f) );














































Cudd_RecursiveDeref(manager,f1);
Cudd_RecursiveDeref(manager,f);
Cudd_Quit(manager);
return 0;
}



/*


manager=Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
//inicializace manazeru
f1=Cudd_ReadOne(manager); //vytvareni bdd x0*x1*x2
Cudd_Ref(f1);


for(i=2;i>=0;i--){
var=Cudd_bddIthVar(manager,i);
tmp=Cudd_bddAnd(manager, var,f1);
Cudd_Ref(tmp);
Cudd_RecursiveDeref(manager,f1);
f1=tmp;
}
f2=Cudd_ReadOne(manager); //vyvareni bdd x0'*x1'*x2'
Cudd_Ref(f2);
for(i=2;i>=0;i--){
var=Cudd_bddIthVar(manager,i);
tmp=Cudd_bddAnd(manager, Cudd_Not(var),f2);
Cudd_Ref(tmp);
Cudd_RecursiveDeref(manager,f2);
f2=tmp;
}


f=Cudd_bddOr(manager,f1,f2); //vytvoreni celeho bdd
Cudd_Ref(f);
Cudd_RecursiveDeref(manager,f1);


return 0;
}

*/
