#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, *zero;
  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 );
  one = Cudd_ReadOne(manager);
  Cudd_Ref(one);
  zero = Cudd_ReadZero(manager);
  cout << " jlkhjlgj: "<<Cudd_V(one) << endl;
  cout << " jlkhjlgj1111: "<<Cudd_Not(cuddV(one)) << endl;
}


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 ){


    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.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( fx) );

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


        if(i==1){
          f=f1;
        }else{
           f=Cudd_bddAnd(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("vstup.txt");
  InitBDD();
  Start(vstup);
  MakeBDD(vstup);
  ////////////////////////////////////////////
  cout << "*********** strom vytvoren ************" << endl;

printf("one uzel : %g\n", Cudd_V(one) );
printf("zero uzel : %g\n", Cudd_V(zero) );
cout << "cout one uzel  : " << Cudd_V(one) << endl;
cout << "cout zero uzel : " << Cudd_V(zero)<< endl;

cout << "index one  : " << Cudd_NodeReadIndex(Cudd_Regular(one)) << endl;
cout << "index zero : " << Cudd_NodeReadIndex(Cudd_Regular(zero)) << endl;



switch(vst){
    case 0:
        cout << "vzpsano do souboru out.o ? : " << cuddP(manager,f) << endl;

        cout << "Index prvniho uzlu : " << Cudd_NodeReadIndex(f) << endl;
        pom0 = Cudd_E( f ); //uloyi potomka then
        cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_NodeReadIndex(  pom0 ) <<"]"<< endl;
        pom1 = Cudd_T( f ); //ulozi potomka then
        cout << "f(1) - 1 - je terminal? :[" << Cudd_IsConstant( pom1 ) << "]  - index je : [" <<  Cudd_V(pom1 )<< "]" << endl;
        cout << endl;

        pom1=Cudd_T(pom0);
        pom0=Cudd_E(pom0);
        cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_NodeReadIndex(  pom0 ) <<"]"<< endl;
        pokus = Cudd_T( f ); //ulozi potomka then
        cout << "f(2) - 1 - je terminal? :[" << Cudd_IsConstant( pom1 ) <<"]  - index je : [" << Cudd_NodeReadIndex( pom1) << "]" << endl;
        cout << endl;

        cout << "f(4) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom0) ) <<"] - index je : [" <<  Cudd_V(  Cudd_E(pom0)  ) <<"]"<< endl;
        cout << "f(4) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom0) ) << "]  - index je : [" << Cudd_V( Cudd_T(pom0)  ) << "]" << endl;
        cout << endl;

        cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom1) ) <<"] - index je : [" << Cudd_V(  Cudd_E(pom1) ) <<"]"<< endl;
        if(Cudd_IsComplement(Cudd_E(pom1))){
          cout << "f(3) - 0 - je to terminal 0 : "<< Cudd_V(Cudd_E(pom1)) << endl;
        }else{
          cout << "f(3) - 0 - je to terminal 1 :"<<  Cudd_V(Cudd_E(pom1)) << endl;
        }

        cout << "f(3) - 1 - je terminal? : [" << Cudd_IsConstant( Cudd_T(pom1) ) <<"] - index je : [" << Cudd_V(  Cudd_T(pom1) ) <<"]"<< endl;
        if(Cudd_IsComplement(Cudd_T(pom1))){
          cout << "f(3) - 1 - je to terminal 0 : " << Cudd_V(Cudd_T(pom1)) << endl;
        }else{
          cout << "f(3) - 1 - je to terminal 1 : " << Cudd_V(Cudd_T(pom1)) << endl;
        }


        cout << endl;

        cout <<"pocet cest : " <<Cudd_CountPathsToNonZero(f)<<endl;
        cout <<"pocet cest do terminalu : " << Cudd_CountPath(f);

        break;

    case 1:
        cout << "vzpsano do souboru out.o ? : " << cuddP(manager,f) << endl;

        cout << "Index prvniho uzlu : " << Cudd_NodeReadIndex(f) << endl;
        pom0 = Cudd_E( f ); //uloyi potomka then
        cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_NodeReadIndex( pom0 ) <<"]"<< endl;
        pom1 = Cudd_T( f ); //ulozi potomka then
        cout << "f(1) - 1 - je terminal? :[" << Cudd_IsConstant( pom1 ) << "]  - index je : [" << Cudd_NodeReadIndex( pom1 ) << "]" << endl;
        cout << endl;

        cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom0) ) <<"] - index je : [" << Cudd_NodeReadIndex(Cudd_E(pom0)) <<"]"<< endl;
        cout << "f(3) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom0) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom0)) << "]" << endl;
        pom=Cudd_E(pom0);
        cout << endl;

        cout << "f(4) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom) ) <<"] - index je : [" << Cudd_V(Cudd_E(pom)) <<"]"<< endl;
        cout << "f(4) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom)) << "]" << endl;
        cout << endl;

        cout << "f(2) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom1) ) <<"] - index je : [" << Cudd_V(Cudd_E(pom1)) <<"]"<< endl;
        cout << "f(2) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom1) ) <<"]  - index je : [" << Cudd_NodeReadIndex(Cudd_T(pom1)) << "]" << endl;

        cout <<"pocet cest : " <<Cudd_CountPathsToNonZero(f)<<endl;
        cout <<"pocet cest do terminalu : " << Cudd_CountPath(f);

        break;

    case 2:
        cout << "vzpsano do souboru out.o ? : " << cuddP(manager,f) << endl;

        cout << "Index prvniho uzlu : " << Cudd_NodeReadIndex(f) << endl;
        pom0 = Cudd_E( f ); //uloyi potomka then
        cout << "f(1) - 0 - je terminal? : [" << Cudd_IsConstant( pom0 ) <<"] - index je : [" << Cudd_NodeReadIndex( pom0 ) <<"]"<< endl;
        pom1 = Cudd_T( f ); //ulozi potomka then
        cout << "f(1) - 1 - je terminal? :[" << Cudd_IsConstant( pom1 ) << "]  - index je : [" << Cudd_NodeReadIndex( pom1 ) << "]" << endl;
        cout << endl;

        cout << "f(2.0) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom0) ) <<"] - index je : [" << Cudd_NodeReadIndex(Cudd_E(pom0)) <<"]"<< endl;
        cout << "f(2.0) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom0) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom0)) << "]" << endl;
        pom=Cudd_E(pom0);
        cout << endl;

        cout << "f(3) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom) ) <<"] - index je : [" << Cudd_V(Cudd_E(pom)) <<"]"<< endl;
        cout << "f(3) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom)) << "]" << endl;
        cout << endl;

        cout << "f(2.1) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom1) ) <<"] - index je : [" << Cudd_NodeReadIndex(Cudd_E(pom1)) <<"]"<< endl;
        cout << "f(2.1) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom1) ) <<"]  - index je : [" << Cudd_NodeReadIndex(Cudd_T(pom1)) << "]" << endl;
        pom=Cudd_E(pom1);
        cout << endl;

        cout << "f(3.1) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom) ) <<"] - index je : [" << Cudd_V(Cudd_E(pom)) <<"]"<< endl;
        cout << "f(3.1) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom)) << "]" << endl;
        pom=Cudd_T(pom1);
        cout << endl;

        cout << "f(4) - 0 - je terminal? : [" << Cudd_IsConstant( Cudd_E(pom) ) <<"] - index je : [" << Cudd_V(Cudd_E(pom)) <<"]"<< endl;
        cout << "f(4) - 1 - je terminal? :[" << Cudd_IsConstant( Cudd_T(pom) ) <<"]  - index je : [" << Cudd_V(Cudd_T(pom)) << "]" << endl;
        //pom=Cudd_E(pom1);
        cout << endl;

        cout <<"pocet cest : " <<Cudd_CountPathsToNonZero(f)<<endl;
        cout <<"pocet cest do terminalu : " << Cudd_CountPath(f);
        break;
    case 3:
        cout << "vzpsano do souboru out.o ? : " << cuddP(manager,f) << endl;
        cout <<"pocet cest : " <<Cudd_CountPathsToNonZero(f)<<endl;
        cout <<"pocet cest do terminalu : " << Cudd_CountPath(f);

    case 4:
        cout << "vzpsano do souboru out.o ? : " << cuddP(manager,f) << endl;
        cout <<"pocet cest : " <<Cudd_CountPathsToNonZero(f)<<endl;
        cout <<"pocet cest do terminalu : " << Cudd_CountPath(f);





        break;
    default: break;
}



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

*/
