/**CFile*******************************************************************
  PackageName [bdd]
  Synopsis    [Package 'bdd' enable symbolic computations by representing
               Boolean functions with ROBDDs.]

  FileName    [bddOutput.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [The file bddOutput.c contains functions for writing and
               drawing logical functions and BDDs.]
  SeeAlso     [bdd.h, bddInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "bddInt.h"

#ifdef ESTWIN32
#else
#  include <sys/types.h>
#  include <sys/wait.h>
#endif

/*-----------------------------------------------------------------------*/
/* Structure declarations                                                */
/*-----------------------------------------------------------------------*/

typedef struct SezBesed {
  struct SezBesed *p;
  Est_String ime;
  Est_Boolean mark;
} SezBesed;

typedef struct {
  int n;
  void *p;
  int t;
} tNode;

typedef struct {
  int id;
  Est_String label;
  int x;
  int y;
} tableXY;

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

static void WriteList(FILE *s, SezBesed *b);

static void WriteFunction_R(FILE *s, Bdd_Edge f, Est_Boolean pik,
                            SezBesed *ze, int *large);

static void WriteBDD_R(FILE *s, Bdd_Edge f, int *large);

static void EnumerateNodes(Bdd_Edge f, tNode **tnode, int *t, int *n);

static void WriteDot_Nodes(FILE *dotfile, tNode *tnode, int n, int id);

static void WriteDot_Edges(FILE *dotfile, Bdd_Edge f, tNode *tnode,
                           int *t, int n);

static void WriteDot_Connections(FILE *funfile, Bdd_Edge f, tNode *tnode,
                                 int *t, int n);

static int ParseDot(FILE *dotfile, tableXY *table, int *xsize,
                    int *ysize);

static Est_String getvariablename(void *p);

static Est_String getname(void *p);

static Est_String getshortname(void *p, int n);

static void addNode(tNode **tnode, int n, void *p, int t);

static int findNode(tNode *tnode, int n, void *p, int t);

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function Bdd_WriteFunction.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Bdd_WriteFunction(FILE *s, Est_String name)
{
  Bdd_Edge f;
  int large = 100;

  if (!Bdd_FindFormula(name,&f)) {
    printf("Function %s does not exists!\n",name);
    return;
  } else {

    if (Bdd_isNull(f)) {
      if (s == stdout) {
        printf("NULL\n");
      } else {
        fprintf(s,"NULL\n");
      }
    } else {
      WriteFunction_R(s, f, f.mark, NULL, &large);
      if (s == stdout) {
        printf("\n");
      } else {
        fprintf(s,"\n");
      }
    }
  }
}

/**Function****************************************************************
  Synopsis    [Function Bdd_WriteBDD.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Bdd_WriteBDD(FILE *s, Est_String name)
{
  Bdd_Edge f;
  int large = 2000;

  if (!Bdd_FindFormula(name,&f)) {
    printf("Function %s does not exists!\n",name);
    return;
  } else {

    if (Bdd_isNull(f)) {
      if (s == stdout) {
        printf("NULL\n");
      } else {
        fprintf(s,"NULL\n");
      }
    } else {
      WriteBDD_R(s, f, &large);
      if (s == stdout) {
        printf("\n");
      } else {
        fprintf(s,"\n");
      }
    }
  }
}

/**Function****************************************************************
  Synopsis    [Function Bdd_WriteDot.]
  Description []
  SideEffects [if (id != -1) use it instead of <...>]
  SeeAlso     []
  ************************************************************************/

int
Bdd_WriteDot(FILE *s, Est_String name, int id)
{
  Bdd_Edge f;
  int t,n;
  tNode *tn;
  Est_String hash;

  n = 0;
  if (!Bdd_FindFormula(name,&f)) {
    printf("Function %s does not exists!\n",name);
    return(0);
  } else {

    while ((hash=strchr(name,'#'))) hash[0]='_';

    fprintf(s,"digraph BDD {\n");
    fprintf(s,"  ordering = out;\n");
    fprintf(s,"  splines = true;\n");
    fprintf(s,"  node [shape = none, label = %s] 0;\n",name);

    t = 0;
    n = 0;
    tn = NULL;
    EnumerateNodes(f,&tn,&t,&n);
    BddNodeRepair(f);
    WriteDot_Nodes(s,tn,n,id);
    fprintf(s,"  0 -> 1;\n");
    t = 1;
    WriteDot_Edges(s,f,tn,&t,n);
    BddNodeRepair(f);
    fprintf(s,"}\n");

    free(tn);
  }

  return n;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_WriteBDDView.]
  Description []
  SideEffects [Uses Bdd_WriteDot and graphviz package]
  SeeAlso     []
  ************************************************************************/

int
Bdd_WriteBDDView(FILE *s, Est_String name, int id)
{
  Est_String dotname,xdotname;
  FILE *dotfile;
  FILE *xdotfile;
  int i,t,n;
  tNode *tn;
  tableXY *table;
  int xsize,ysize;
  Bdd_Edge f;
#ifndef ESTWIN32
  pid_t childpid;
  int status;
#endif

  if (!Bdd_FindFormula(name,&f)) {
    printf("Function %s does not exists!\n",name);
    return -1;
  } else {


#ifdef ESTWIN32
    dotname = strdup("bdd.dot");
    xdotname = strdup("bdd.xdot");
#else
    dotname = strdup(tmpnam(NULL));
    xdotname = strdup(tmpnam(NULL));
#endif

    dotfile = fopen(dotname,"w");
    if (!dotfile) {
      printf("File error (%s)\n",dotname);
      return -1;
    }

    n = Bdd_WriteDot(dotfile,name,id); /* n = number of nodes */
    fclose(dotfile);

#ifdef ESTWIN32
    _spawnlp(P_WAIT,"dot.exe","dot.exe","-y","-o",xdotname,dotname,NULL);
#else
    childpid = fork();
    if (childpid == 0) {
      execlp("dot","dot","-y","-o",xdotname,dotname,NULL);
    } else if (childpid > 0) {
      waitpid(childpid,&status,0);
    }
#endif

    xdotfile = fopen(xdotname,"r");
    if (!xdotfile) {
      printf("File error (%s)\n",xdotname);
      return -1;
    }

    table = (tableXY *) malloc((n+1) * sizeof(tableXY)); /* n = nodes + label */
    ParseDot(xdotfile,table,&xsize,&ysize);
    fclose(xdotfile);

    free(dotname);
    free(xdotname);

    t = 0;
    n = 0;
    tn = NULL;
    EnumerateNodes(f,&tn,&t,&n);
    BddNodeRepair(f);

    fprintf(s,"label %d %s %d %d\n",table[0].id,table[0].label,table[0].x,table[0].y);
    for (i=1;i<(n+1);i++) {
      if (tn[i-1].t == 0) {
        fprintf(s,"node %d %s %d %d\n",table[i].id,table[i].label,table[i].x,table[i].y);
      } else {
        fprintf(s,"terminal %d %s %d %d\n",table[i].id,table[i].label,table[i].x,table[i].y);
      }
      free(table[i].label);
    }
    free(table);

    fprintf(s,"connect 0 1 ");
    if (f.mark) {
      fprintf(s,"si\n");
    } else {
      fprintf(s,"s\n");
    }

    t = 1;
    WriteDot_Connections(s,f,tn,&t,n);
    BddNodeRepair(f);

    free(tn);

  }

  return 0;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_WriteGraphML.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Bdd_WriteGraphML(FILE *s, Est_String name)
{
  Bdd_Edge f;

  if (!Bdd_FindFormula(name,&f)) {
    printf("Function %s does not exists!\n",name);
    return -1;
  } else {

  fprintf(s,"<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n");
  fprintf(s,"<!DOCTYPE graphml SYSTEM \"http://graphml.graphdrawing.org/dtds/graphml.dtd\">\n");
  fprintf(s,"<graphml>\n");
  fprintf(s,"  <key id=\"i\" for=\"graph\"></key>\n");
  fprintf(s,"  <key id=\"t\" for=\"node\"></key>\n");
  fprintf(s,"  <key id=\"d\" for=\"edge\"></key>\n");
  fprintf(s,"  <key id=\"c\" for=\"edge\"></key>\n");
  fprintf(s,"  <graph id=\"%s\" edgedefault=\"directed\">\n",name);
  fprintf(s,"    <data key=\"i\">false</data>\n");
  fprintf(s,"    <node id=\"terminal\"><data key=\"t\">true</data></node>\n");
  fprintf(s,"    <node id=\"a\"/>\n");
  fprintf(s,"    <node id=\"b\"/>\n");
  fprintf(s,"    <edge source=\"a\" target=\"terminal\"><data key=\"d\">else</data></edge>\n");
  fprintf(s,"    <edge source=\"a\" target=\"b\"><data key=\"d\">then</data></edge>\n");
  fprintf(s,"    <edge source=\"b\" target=\"terminal\"><data key=\"d\">else</data><data key=\"c\">true</data></edge>\n");
  fprintf(s,"    <edge source=\"b\" target=\"terminal\"><data key=\"d\">then</data></edge>\n");
  fprintf(s,"  </graph>\n");
  fprintf(s,"</graphml>\n");

  }

  return 0;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_ReadGraphML.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Bdd_ReadGraphML(FILE *s)
{
  return 0;

}

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function WriteList.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteList(FILE *s, SezBesed *b)
{
  if (b) {
    WriteList(s,b->p);
    if (s == stdout) {
      printf(" ");
    } else {
      fprintf(s," ");
    }
    if (b->mark) {
      if (s == stdout) {
        printf("*");
      } else {
        fprintf(s,"*");
      }
    }
    if (s == stdout) {
      printf("%s",b->ime);
    } else {
      fprintf(s,"%s",b->ime);
    }
  }
}

/**Function****************************************************************
  Synopsis    [Function WriteFunction_R.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteFunction_R(FILE *s, Bdd_Edge f, Est_Boolean pik, SezBesed *ze, int *large)
{
  SezBesed spr;

  if (*large == 0) return;

  if (Bdd_isTerminal(f)) {

    if (!pik) {
      if (s == stdout) {
        printf("  + ");
      } else {
        fprintf(s,"  + ");
      }

      if (ze) {
        WriteList(s,ze);
        if (s == stdout) {
          printf("\n");
        } else {
          fprintf(s,"\n");
        }
        if (--(*large) == 0) {
          if (s == stdout) {
            printf("Function to large.");
          } else {
            fprintf(s,"Function to large.");
          }
          return;
        }
      } else {
        if (s == stdout) {
          printf(" 1");
        } else {
          fprintf(s," 1");
        }
      }

    } else {

      if (!ze) {
        if (s == stdout) {
          printf("  +  0");
        } else {
          fprintf(s,"  +  0");
        }
      }

    }

  } else {
    spr.p = ze;
    spr.ime = Bdd_GetVariableName(f);
    spr.mark = TRUE;
    WriteFunction_R(s,Bdd_GetElse(f), pik ^ (Bdd_GetElse(f)).mark, &spr, large);
    spr.mark = FALSE;
    WriteFunction_R(s,Bdd_GetThen(f), pik ^ (Bdd_GetThen(f)).mark, &spr, large);
  }
}

/**Function****************************************************************
  Synopsis    [Function WriteBDD_R.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteBDD_R(FILE *s, Bdd_Edge f, int *large)
{

  if (*large == 0) return;
  if (--(*large) == 0) {
    if (s == stdout) {
      printf("\nBDD to large.");
    } else {
      fprintf(s,"\nBDD to large.");
    }
    return;
  }

  if (f.mark) {
    if (s == stdout) {
      printf("* ");
    } else {
      fprintf(s,"* ");
    }
  }

  if (s == stdout) {
    printf("%s",Bdd_GetVariableName(f));
  } else {
    fprintf(s,"%s",Bdd_GetVariableName(f));
  }

  if (!Bdd_isTerminal(f)) {

    if (s == stdout) {
      printf(" (");
    } else {
      fprintf(s," (");
    }

    WriteBDD_R(s,Bdd_GetElse(f),large);

    if (*large) {
      if (s == stdout) {
        printf(") (");
      } else {
        fprintf(s,") (");
      }
    }

    WriteBDD_R(s,Bdd_GetThen(f),large);

    if (*large) {
      if (s == stdout) {
        printf(")");
      } else {
        fprintf(s,")");
      }
    }

  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
EnumerateNodes(Bdd_Edge f, tNode **tnode, int *t, int *n)
{
  if (!BddisSelected(f)) {
    BddSelectNode(f);
    if (Bdd_isTerminal(f)) {
      (*n)++;
      (*t)++;
      addNode(tnode,(*n),f.p,(*t));
    } else {
      (*n)++;
      addNode(tnode,(*n),f.p,0);
      if (Bdd_isTerminal(Bdd_GetElse(f)) || Bdd_isTerminal(Bdd_GetThen(f))) {
        (*n)++;
        (*t)++;
        addNode(tnode,(*n),f.p,(*t));
      }
      if (!Bdd_isTerminal(Bdd_GetElse(f))) {
        EnumerateNodes(Bdd_GetElse(f),tnode,t,n);
      }
      if (!Bdd_isTerminal(Bdd_GetThen(f))) {
        EnumerateNodes(Bdd_GetThen(f),tnode,t,n);
      }
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteDot_Nodes(FILE *dotfile, tNode *tnode, int n, int id)
{
  int i;
  void *p;
  Est_String name,hash;

  for (i=0; i<n; i++) {
    if (tnode[i].t == 0) {
      p = tnode[i].p;
      if (id == -1) {
        name = getname(p);
      } else {
        name = getshortname(p,id);
      }
      while ((hash=strchr(name,'#'))) hash[0]='_';

      fprintf(dotfile,"  node [shape = circle, label = %s] %d;\n",name,tnode[i].n);
      free(name);
    } else {
      fprintf(dotfile,"  node [shape = none, label = 1] %d;\n",tnode[i].n);
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteDot_Edges(FILE *dotfile, Bdd_Edge f, tNode *tnode, int *t, int n)
{
  int n1,n2;

  if (!Bdd_isTerminal(f) && !BddisSelected(f)) {
    BddSelectNode(f);
    n1 = findNode(tnode,n,f.p,0);

    if (Bdd_isTerminal(Bdd_GetElse(f))) {
      n2 = findNode(tnode,n,f.p,(*t));
    } else {
      n2 = findNode(tnode,n,(Bdd_GetElse(f)).p,0);
    }
    fprintf(dotfile,"  %d -> %d;\n",n1,n2);

    if (Bdd_isTerminal(Bdd_GetThen(f))) {
      n2 = findNode(tnode,n,f.p,(*t));
    } else {
      n2 = findNode(tnode,n,(Bdd_GetThen(f)).p,0);
    }
    fprintf(dotfile,"  %d -> %d;\n",n1,n2);

    if (Bdd_isTerminal(Bdd_GetElse(f)) || Bdd_isTerminal(Bdd_GetThen(f))) (*t)++;
    WriteDot_Edges(dotfile,Bdd_GetElse(f),tnode,t,n);
    WriteDot_Edges(dotfile,Bdd_GetThen(f),tnode,t,n);
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
WriteDot_Connections(FILE *funfile, Bdd_Edge f, tNode *tnode, int *t, int n)
{
  int n1,n2;

  if (!Bdd_isTerminal(f) && !BddisSelected(f)) {
    BddSelectNode(f);
    n1 = findNode(tnode,n,f.p,0);

    if ((Bdd_GetThen(f)).p == (Bdd_GetElse(f)).p) {

      if (Bdd_isTerminal(Bdd_GetThen(f))) {
        n2 = findNode(tnode,n,f.p,(*t));
      } else {
        n2 = findNode(tnode,n,(Bdd_GetThen(f)).p,0);
      }
      fprintf(funfile,"connect %d %d d\n",n1,n2);

    } else {

      if (Bdd_isTerminal(Bdd_GetElse(f))) {
        n2 = findNode(tnode,n,f.p,(*t));
      } else {
        n2 = findNode(tnode,n,(Bdd_GetElse(f)).p,0);
      }
      fprintf(funfile,"connect %d %d ",n1,n2);
      if ((Bdd_GetElse(f)).mark) {
        fprintf(funfile,"li\n");
      } else {
        fprintf(funfile,"l\n");
      }

      if (Bdd_isTerminal(Bdd_GetThen(f))) {
        n2 = findNode(tnode,n,f.p,(*t));
      } else {
        n2 = findNode(tnode,n,(Bdd_GetThen(f)).p,0);
      }
      fprintf(funfile,"connect %d %d r\n",n1,n2);

    }

    if (Bdd_isTerminal(Bdd_GetElse(f)) || Bdd_isTerminal(Bdd_GetThen(f))) (*t)++;
    WriteDot_Connections(funfile,Bdd_GetElse(f),tnode,t,n);
    WriteDot_Connections(funfile,Bdd_GetThen(f),tnode,t,n);
  }
}

/**Function****************************************************************
  Synopsis    [Function Bdd_Dot]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
ParseDot(FILE *dotfile, tableXY *table, int *xsize, int *ysize)
{
  char line[128];
  Est_String r,label,pos;
  int n,id,x,y;

  n = 0;

  r = fgets(line,128,dotfile);
  while (r) {
    if (strstr(line,"bb=")) {
      pos = (Est_String) malloc(strlen(line));
      sscanf(&(strstr(line,"bb=")[4]),"%s",pos);
      sscanf(pos,"%d,%d,%d,%d",&x,&y,xsize,ysize);
      free(pos);
    }
    if ((strstr(line,"label=")) && (strstr(line,"pos="))) {

      /*
      fprintf(stderr,line);
      */

      label = (Est_String) malloc(strlen(line));
      pos = (Est_String) malloc(strlen(line));

      sscanf(line,"%d",&id);
      sscanf(&(strstr(line,"label=")[6]),"%s",label);
      label[strlen(label)-1] = 0;
      sscanf(&(strstr(line,"pos=")[5]),"%s",pos);
      sscanf(pos,"%d,%d",&x,&y);

      /*
      fprintf(stderr,"id = %d, label = %s, x = %d, y = %d\n",id,label,x,y);
      */

      table[n].id = id;
      table[n].label = strdup(label);
      table[n].x = x;
      table[n].y = y;

      n++;
      free(label);
      free(pos);
    }

    while (r &&
           !(strchr(line,';')) &&
           !(strchr(line,'{')) &&
           !(strchr(line,'}'))) r= fgets(line,128,dotfile);

    if (r) r = fgets(line,128,dotfile);
  }

  return (n-1);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_String
getvariablename(void *p) {
  Bdd_Edge tmp;

  tmp = bdd_termNull;
  tmp.p = p;
  return (Bdd_GetVariableName(tmp));
}

/**Function****************************************************************
  Synopsis    [Function getname]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_String
getname(void *p) {
  int i;
  Est_String newname;

  newname = strdup(getvariablename(p));
  for (i=0; i<strlen(newname);i++) {
    if (newname[i] == '<') newname[i] = '_';
    if (newname[i] == '>') newname[i] = 0;
  }

  return (newname);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_String
getshortname(void *p, int n) {
  int i;
  Est_String name;
  Est_String shortname;

  name = strdup(getvariablename(p));
  i = strcspn(name,"<");
  name[i]=0;
  shortname = strdup(name);
  free(name);

  return (shortname);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
addNode(tNode **tnode, int n, void *p, int t)
{
  if (!(*tnode)) {
    (*tnode) = (tNode *) malloc(n * sizeof(tNode));
  } else {
    (*tnode) = (tNode *) realloc((*tnode), n * sizeof(tNode));
  }
  (*tnode)[n-1].n = n;
  (*tnode)[n-1].p = p;
  (*tnode)[n-1].t = t;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
findNode(tNode *tnode, int n, void *p, int t)
{
  int i;

  i=0;
  while (i<n) {
    if ((tnode[i].p == p) && (tnode[i].t == t)) {
      return tnode[i].n;
    }
    i++;
  }

  return -1;
}
