#include "stdafx.h"
#include "include/util.h"
#include "include/cudd.h"
#include <stdio.h>
#include <time.h>

#define MAX_NAME_LENGTH 10

struct BddArray* cudd_PlaLoad(DdManager *ddMgr, FILE* fp);	//funkce na nahrani pole BDD
struct Data* fileLoad(FILE *fp);	//pomocna funkce pro nahrani PLA souboru do pomocne struktury
void freeMem(struct Data *data, int type);	//pomocna funkce na uvolneni nepotrebne pameti

struct Data{                         //pomocna struktura - je v ni ulozeny nacitany soubor ve vnitrni forme
	struct PlaArray	*iplaArray;
	struct PlaArray	*oplaArray;
	char  					**inames;
	char  					**onames;
	int   					terms;
	int   					inputs;
  int   					outputs;
  };

struct BddArray{       					//struktura s načtenými BDD a pomocnými informacemi
  int     outputs;
  int     inputs;
  char    **inames;
  char    **onames;
  DdNode  **roots;
	};

struct PlaArray{                   //pomocna struktura pro ulozeni matice hodnot vstupu a vystupu
	int 						*line;
	struct PlaArray	*next;
	};

int main()
{
  clock_t         start, konec;
  struct BddArray *array;
  DdManager       *manager;
  FILE            *fp;
  int             i;
  double          k;

  start=clock();
  manager=Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
  fp=fopen("c:\\testy\\vystupy\\i50o100t1000dc0.pla","r");
  array=cudd_PlaLoad(manager,fp);
  fclose(fp);
  konec=clock();
  if(array){
 	for(i=0;i<array->outputs;i++){
		if(array->roots[i]){
			k=Cudd_DagSize(array->roots[i]);
      printf("%2d   %f\n",i,k);
      }
    }
    }
  printf("\n\n%f\n",(double)(konec-start)/(double)CLOCKS_PER_SEC);
  FILE *f;
  f = fopen("c:\\cuddtest.txt", "w");
  Cudd_PrintInfo(manager, f);
  printf("%d", Cudd_ReadNodeCount(manager));
  system("PAUSE");
  return 0;
}



struct BddArray* cudd_PlaLoad(DdManager *ddMgr, FILE* fp){        //nacteni pole BDD
  struct Data     *data;
  struct BddArray *array;
  struct PlaArray	*temp;
  DdNode          **terms;
  DdNode          *f,*var,*tmp;
  int             i,j;

  if(!fp){
  	fprintf(stderr,"No file to load.");
    return NULL;
    }

  data=fileLoad(fp);          //pomocna funkce, ktera vrati naacteny soubor ve vnitrnim tvaru
  if(!data){
    fprintf(stderr,"Error in fileload.");
    return NULL;
    }

  terms=(DdNode**)malloc(sizeof(DdNode*)*data->terms);          //alokovani potrebne pameti
  array = (BddArray *)malloc(sizeof(struct BddArray));
  array->roots=(DdNode**)malloc(sizeof(DdNode*)*data->outputs);
  if(!terms||!array||!array->roots){
  	fprintf(stderr,"Can't allocate memory.");
    freeMem(data,0);
    if(!terms){
    	free(terms);
      }
    if(!array->roots){
    	free(array->roots);
      }
    if(!array){
    	free(array);
      }
    return NULL;
    }

  array->inames=data->inames;
  array->onames=data->onames;
  array->outputs=data->outputs;
  array->inputs=data->inputs;

  for(i=0,temp=data->iplaArray;temp;temp=temp->next,i++){   //vytvoreni docasnych bdd z termu
    f=Cudd_ReadOne(ddMgr);
    Cudd_Ref(f);
    for(j=data->inputs-1;j>=0;j--){
			if(temp->line[j]==-1){
        continue;
        }
      var=Cudd_bddIthVar(ddMgr,j);
      if(temp->line[j]==1){
        tmp=Cudd_bddAnd(ddMgr, var,f);
        }
      else{
        tmp=Cudd_bddAnd(ddMgr,Cudd_Not(var),f);
        }
      Cudd_Ref(tmp);
      Cudd_RecursiveDeref(ddMgr, f);
      f=tmp;
      }
    terms[i]=f;
    }

  for(i=0;i<data->outputs;i++){     //vytvoreni konecnych bdd z docasnych bdd
    tmp=NULL;
	  f=NULL;
    for(j=0,temp=data->oplaArray;temp;temp=temp->next,j++){
      if(temp->line[i]==-1||temp->line[i]==0){
       continue;
       }
      if(!f){
        f=terms[j];
        Cudd_Ref(f);
        continue;
        }
      tmp=Cudd_bddOr(ddMgr,f,terms[j]);
      Cudd_Ref(tmp);
	    Cudd_RecursiveDeref(ddMgr,f);
			f=tmp;
      }

		if(!f){               //pokud je funkce nulova (kontradikce)
    	f=Cudd_Not(Cudd_ReadOne(ddMgr));
      Cudd_Ref(f);
			}
		array->roots[i]=f;
		}

	for(i=0;i<data->terms;i++){                //dereference docasnych bdd
  	Cudd_RecursiveDeref(ddMgr,terms[i]);
    }

  freeMem(data,1);
	return array;
}

struct Data* fileLoad(FILE* fp){        //pomocna funkce na nahrani souboru do vnitrniho tvaru
	char        		buf;
	char        		namebuf[MAX_NAME_LENGTH];
	int         		i,term;
	struct Data 		*data;
	struct PlaArray *itemp,*otemp;

  data=(Data*)malloc(sizeof(struct Data));
	if(!data){
  	fprintf(stderr,"Can't allocate memory.");
    return NULL;
    }
  data->iplaArray=NULL;
	data->oplaArray=NULL;
	data->inputs=0;
	data->outputs=0;
	data->terms=0;
	term=0;
	itemp=NULL;
  otemp=NULL;

	while(!feof(fp)){     //nacitani souboru
		buf=fgetc(fp);
		while(buf==' '||buf=='\n'||buf=='.'||buf=='\t')      //bile znaky
			buf=fgetc(fp);
		switch(buf){
			case 'i': buf=fgetc(fp);            //rozpoznavani klicovych slov
				switch(buf){
					case 'l': buf=fgetc(fp);
						if(buf=='b'){
							if(data->inputs==0){
								fprintf(stderr,"Number of inputs missing.\n");
								freeMem(data,0);
								return NULL;
								}
							else{
								data->inames=(char **)malloc(sizeof(char*)*data->inputs);
                if(!data->inames){
 									fprintf(stderr,"Can't allocate memory.");
                  freeMem(data,0);
							    return NULL;
							    }
								for(i=0;i<data->inputs;i++){
									fscanf(fp,"%s",&namebuf);
									data->inames[i]=(char*)malloc(sizeof(char)*strlen(namebuf));
                  if(!data->inames[i]){
 										fprintf(stderr,"Can't allocate memory.");
										freeMem(data,0);
							    	return NULL;
							    }
									strcpy(data->inames[i],namebuf);
									}
								}
							}
						else{
							fprintf(stderr,"Unknown identifier.\n");
							freeMem(data,0);
							return NULL;
							}
						break;
					case ' ': fscanf(fp,"%d",&data->inputs);
 						break;
					default: fprintf(stderr,"Unknown identifier.\n");
						freeMem(data,0);
						return NULL;
						}
				break;
			case 'o': buf=fgetc(fp);
				switch(buf){
					case 'b': if(data->outputs==0){
							fprintf(stderr,"Number of inputs missing.\n");
							freeMem(data,0);
							return NULL;
							}
						else{
							data->onames=(char**)malloc(sizeof(char*)*data->outputs);
              if(!data->onames){
            		fprintf(stderr,"Can't allocate memory.");
                freeMem(data,0);
							  return NULL;
                }
							for(i=0;i<data->outputs;i++){
								fscanf(fp,"%s",&namebuf);
								data->onames[i]=(char*)malloc(sizeof(char)*strlen(namebuf));
                if(!data->onames[i]){
 								 	fprintf(stderr,"Can't allocate memory.");
                  freeMem(data,0);
							   	return NULL;
							    }
								strcpy(data->inames[i],namebuf);
								}
							}
						break;
					case ' ': fscanf(fp,"%d",&data->outputs);
						break;
					default: fprintf(stderr,"Unknown identifier.\n");
						freeMem(data,0);
						return NULL;
						}
				break;
			case 'p':fscanf(fp,"%d",&data->terms);
				break;
			case '-':          //nahravani matice hodnot vstupu a vystupu
			case '0':
			case '1': if(data->inputs==0||data->outputs==0){
					fprintf(stderr,"Numer of inputs or outputs missing.\n");
					freeMem(data,0);
					return NULL;
					}                        
        if(!data->iplaArray){
					data->iplaArray=(PlaArray*)malloc(sizeof(struct PlaArray));
          if(!data->iplaArray){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }
					itemp=data->iplaArray;
          itemp->next=NULL;
					}
			 	else{                      
					itemp->next=(PlaArray*)malloc(sizeof(struct PlaArray));
          if(!itemp->next){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }
					itemp=itemp->next;
          itemp->next=NULL;
          }
					itemp->line=(int *)malloc(sizeof(int)*data->inputs);
          if(!itemp->line){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }

				for(i=0;i<data->inputs;i++){
					while(buf==' '||buf=='\n'||buf=='\t'){
						buf=fgetc(fp);
						}
					if(buf!='0'&&buf!='1'&&buf!='-'){
						fprintf(stderr,"Expected '1', '0' or '-' in term %d\n",term+1);
						freeMem(data,0);
						return NULL;
						}
					if(buf=='-'){
						itemp->line[i]=-1;
						}
					else{
						itemp->line[i]=buf-'0';
						}
					buf=fgetc(fp);
					}

        if(buf!=' '&&buf!='\n'&&buf!='\t'){
		 			fprintf(stderr, "Error in term %d.\n", term);
					freeMem(data,0);
          return NULL;
					}

        if(!data->oplaArray){
				 	data->oplaArray=(PlaArray*)malloc(sizeof(struct PlaArray));
          if(!data->oplaArray){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }
					otemp=data->oplaArray;
          otemp->next=NULL;
					}
				else{
				 	otemp->next=(PlaArray*)malloc(sizeof(struct PlaArray));
          if(!otemp->next){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }
					otemp=otemp->next;
          otemp->next=NULL;
          }
					otemp->line=(int *)malloc(sizeof(int)*data->outputs);
          if(!otemp->line){
 						fprintf(stderr,"Can't allocate memory.");
            freeMem(data,0);
					 	return NULL;
					  }

        for(i=0;i<data->outputs;i++){
        	buf=fgetc(fp);
          while(buf==' '||buf=='\n'||buf=='\t'){
						buf=fgetc(fp);
						}
          if(buf!='0'&&buf!='1'&&buf!='-'){
						fprintf(stderr,"Expected '1', '0' or '-' in term %d\n",term);
						freeMem(data,0);
						return NULL;
						}
          if(buf=='-'){
           	otemp->line[i]=-1;
            }
          else{
           	otemp->line[i]=buf-'0';
            }
          }
        term++;
        break;
      case 'e': break;
      case EOF: break;
      default: fprintf(stderr,"Unexpected symbol at start of a line.\n");
      	freeMem(NULL,0);
        return NULL;
      }
		}
	if(data->iplaArray&&data->oplaArray){ //kontrola, jestli bylo neco nahrano
    if(data->terms&&data->terms!=term){
    	fprintf(stderr,"Warning found %d terms instead %d.\n",term,data->terms);
      }
		data->terms=term;
    return data;
    }
	else{
  	fprintf(stderr,"Unknown error in reading file\n");
  	freeMem(data,0);
    return NULL;
    }
	}

void freeMem(struct Data *data, int type){    //uvolneni pameti
	int 						i;
  struct PlaArray	*temp,*temp2;
  if(data->iplaArray&&data->inputs>0){
    for(temp=data->iplaArray;temp;){
    	free(temp->line);
      temp2=temp->next;
    	free(temp);
    	temp=temp2;
      }
    }
  else{
  	fprintf(stderr,"Warning:not freeing iplaArray memory.\n");
    }
  if(data->oplaArray&&data->outputs>0){
    for(temp=data->oplaArray;temp;){
    	free(temp->line);
      temp2=temp->next;
    	free(temp);
    	temp=temp2;
      }
    }
  else{
  	fprintf(stderr,"Warning:not freeing oplaArray memory.\n");
    }
  if(data->inames&&!type){
  	for(i=0;i<data->inputs;i++){
    	free(data->inames[i]);
      }
    }
  if(data->onames&&!type){
  	for(i=0;i<data->outputs;i++){
    	free(data->onames[i]);
      }
    }
  free(data);
  }



