src/synth/synthWrite.c

Go to the documentation of this file.

#include "synthInt.h"

static char rcsid[] UNUSED = "$Id: synthWrite.c,v 1.43 2005/05/11 20:18:39 hhhan Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


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

typedef struct TruthTableLine {
  char *values;    /* string of 1, 0, and - */
  struct TruthTableLine *next; /* pointer to next table line */
} TruthTableLine;


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

static  char            *DefaultPrefix = "_n";
static  char            *InternalNodePrefix;
static  st_table        *NodeNameTable; /* to keep all node names for
                                         * primary input, primary output 
                                         * latch input and output
                                         */

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

static void WriteMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
static void WriteLeafMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
static void WriteBlifBinary(bdd_manager *dd, bdd_node *node, char *name, FILE *fout, int *support);
static void WriteEqnOfTree(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs);
static int GetEqnOfTree(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, char *eq, bdd_node **ofuncs);
static void WriteMlTreeBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, char *func_name, int ref);
static void WriteMultiLevelBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no);
static TruthTableLine * GetMultiLevelBlifRecur(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static int GetMultiLevelNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static int GetLeafNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static TruthTableLine * GetTautologyLine(int ni);
static TruthTableLine * GetLeafLines(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static TruthTableLine * GetBlifBinary(TruthTableLine *line, bdd_manager *dd, bdd_node *node, char *values, int *support, int ni);
static TruthTableLine * GetComplementOneLine(TruthTableLine *line, int ni, int flag);
static TruthTableLine * GetComplementLines(TruthTableLine *lines, int ni, int flag);
static TruthTableLine * GetAndLines(TruthTableLine *line1, TruthTableLine *line2, int ni, int flag);
static bdd_node * GetDdNodeOfMlTree(MlTree *tree, int comp);
static int GetMlTreeName(Ntk_Network_t *net, bdd_node **ofuncs, MlTree *tree, char *name);
static char ** GetAllVarNameArray(bdd_manager *dd);

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


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


int
SynthStringCompare(char **a,
                   char **b)
{
  char  *pa, *pb;

  pa = *a;
  pb = *b;

  if (*pa == '\0') {
    if (*pb == '\0')
      return(0);
    else
      return(-1);
  } else if (*pb == '\0')
    return(1);
  while (*pa != '\0' && *pb != '\0') {
    if (*pa > *pb)
      return(1);
    if (*pa < *pb)
      return(-1);
    pa++;
    pb++;
    if (*pa == '\0') {
      if (*pb == '\0')
        return(0);
      else
        return(-1);
    } else if (*pb == '\0')
      return(1);
  }
  return(0);
}


void
SynthWriteBlifFile(Ntk_Network_t *net,
                   bdd_manager *dd,
                   MlTree **tree,
                   char *filename,
                   int no,
                   bdd_node **ofuncs,
                   int *initStates,
                   int ml_mode,
                   int verbosity)
{
  FILE          *fout;
  int           i, j;
  int           *oflags;
  char          out_name[MAX_NAME_LEN], name[MAX_NAME_LEN];
  lsGen         gen;
  Ntk_Node_t    *node;
  char          **sorted_name;
  int           ni, po;
  int           polarity;

  fout = Cmd_FileOpen(filename, "w", NIL(char *), 0);
  if (!fout) {
    (void)fprintf(vis_stdout,
                  "** synth error: Error in opening file [%s]\n", filename);
    return;
  }

  fprintf(fout, ".model %s\n", Ntk_NetworkReadName(net));
  fprintf(fout, ".inputs");

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
        (int (*)(const void *, const void *)) SynthStringCompare);
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);

  fprintf(fout, "\n");
  fprintf(fout, ".outputs");

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);
  fprintf(fout, "\n");

  /* Print list of latches. */
  i = 0;
  Ntk_NetworkForEachLatch(net, gen, node) {
    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
    fprintf(fout, " %s", Ntk_NodeReadName(node));
    fprintf(fout, " %d\n", initStates[i]);
    i++;
  }

  oflags = ALLOC(int, no);
  (void)memset((void *)oflags, 0, no * sizeof(int));
  for (i = 0; i < no; i++) {
    if (!tree[i])
      continue;
    if (bdd_is_constant(tree[i]->node)) {
      if (tree[i]->comp) {
        for (j = 0; j < no; j++) {
          if (tree[i]->complement == ofuncs[j] && oflags[j] == 0) {
            sprintf(out_name, "%s", SynthGetIthOutputName(j));
            break;
          }
        }
      } else {
        for (j = 0; j < no; j++) {
          if (tree[i]->node == ofuncs[j] && oflags[j] == 0) {
            sprintf(out_name, "%s", SynthGetIthOutputName(j));
            break;
          }
        }
      }
      if (j == no)
        SynthGetInternalNodeName(out_name, tree[i]->id);
      else {
        if (oflags[j])
          continue;
        else
          oflags[j] = 1;
      }
      fprintf(fout, "\n.names %s\n", out_name);
      if (tree[i]->node == bdd_read_one(dd)) {
        if (tree[i]->comp)
          fprintf(fout, "0\n");
        else
          fprintf(fout, "1\n");
      } else {
        if (tree[i]->comp)
          fprintf(fout, "1\n");
        else
          fprintf(fout, "0\n");
      }
      continue;
    } else if (tree[i]->ref) {
      for (j = 0; j < no; j++) {
        if ((((tree[i]->comp == 0 && tree[i]->node == ofuncs[j]) ||
              (tree[i]->comp && tree[i]->complement == ofuncs[j]))) &&
            oflags[j] == 0) {
          sprintf(out_name, "%s", SynthGetIthOutputName(j));
          break;
        }
      }
      if (j == no)
        SynthGetInternalNodeName(out_name, tree[i]->id);
      else {
        if (oflags[j])
          continue;
        else
          oflags[j] = 1;
      }
      polarity = GetMlTreeName(net, ofuncs, tree[i], name);
      if (strcmp(out_name, name) == 0)
        SynthGetPrimaryNodeName(net, tree[i]->node, name);
      fprintf(fout, "\n.names %s %s\n", name, out_name);
      if (polarity == 0) {
        if (tree[i]->comp)
          fprintf(fout, "0 1\n");
        else
          fprintf(fout, "1 1\n");
      } else {
        if (tree[i]->comp)
          fprintf(fout, "1 1\n");
        else
          fprintf(fout, "0 1\n");
      }
      continue;
    }
    if (ml_mode == 0) {
      if (tree[i]->pi) {
        tree[i]->pi = 0;
        WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
        tree[i]->pi = 1;
      } else {
        WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
      }
    } else {
      for (j = 0; j < no; j++) {
        if (tree[i]->node == ofuncs[j]) {
          if (oflags[j])
            continue;
          else
            oflags[j] = 1;
          sprintf(out_name, "%s", SynthGetIthOutputName(j));
          break;
        }
      }
      if (j == no)
        SynthGetInternalNodeName(out_name, tree[i]->id);
      if (tree[i]->pi) {
        tree[i]->pi = 0;
        WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
        tree[i]->pi = 1;
      } else {
        WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
      }
    }
  }
  FREE(oflags);

  fprintf(fout, "\n.end\n");
  fclose(fout);
}


void
SynthWriteEqnHeader(FILE *fout,
                  Ntk_Network_t *net,
                  bdd_manager *dd)
{
  int           i;
  lsGen         gen;
  Ntk_Node_t    *node;
  char          **sorted_name;
  int           ni, po;

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  fprintf(fout, "INORDER");
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  fprintf(fout, "\n");
  FREE(sorted_name);

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  fprintf(fout, "OUTORDER");
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  fprintf(fout, "\n");
  FREE(sorted_name);
}


void
SynthWriteEqn(FILE *fout,
              Ntk_Network_t *net,
              bdd_manager *dd,
              MlTree *tree,
              bdd_node **ofuncs,
              char *func_name,
              int ref)
{
  char  name[MAX_NAME_LEN];
  int   polarity = 0;

  if (tree->top || tree->shared) {
    if (ref) {
      /* If tree is shared we print the name of the original function
       * unless it is a constant.
       */
      if (tree->ref) {
        if (tree->node == bdd_read_zero(dd))
          sprintf(name, "zero");
        else if (tree->node == bdd_read_one(dd))
          sprintf(name, "one");
        else
          polarity = GetMlTreeName(net, ofuncs, tree, name);
        if (polarity == 0) {
          if (tree->comp)
            SynthMakeComplementString(name);
        } else {
          if (!tree->comp)
            SynthMakeComplementString(name);
        }
        fprintf(fout, "%s = %s\n", func_name, name);
        return;
      }
    }
    WriteEqnOfTree(fout, net, dd, tree, ofuncs);
  }

  if (tree->leaf) {
    return;
  }

  if (tree->q_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->q, ofuncs, NULL, ref);
  if (tree->d_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->d, ofuncs, NULL, ref);
  if (tree->r_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->r, ofuncs, NULL, ref);
}


void
SynthSetInternalNodePrefix(char *prefix)
{
  if (prefix)
    InternalNodePrefix = prefix;
  else
    InternalNodePrefix = DefaultPrefix;
}


void
SynthSetupNodeNameTable(Ntk_Network_t *net)
{
  lsGen         gen;
  Ntk_Node_t    *node;

  if (NodeNameTable) {
    (void)fprintf(vis_stdout,
        "** synth warning: table already exists in SynthSetupNodeNameTable.\n");
    st_free_table(NodeNameTable);
  }

  NodeNameTable = st_init_table(strcmp, st_strhash);

  /* Register all primary input node names. */
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }

  /* Register all primary output node names. */
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }

  /* Register all latch input and output node names. */
  Ntk_NetworkForEachLatch(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(Ntk_LatchReadDataInput(node)),
              (char *)NULL);
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }
}


void
SynthFreeNodeNameTable(void)
{
  st_free_table(NodeNameTable);
  NodeNameTable = NIL(st_table);
}


void
SynthGetInternalNodeName(char *name, int id)
{
  sprintf(name, "%s%d", InternalNodePrefix, id);
  if (NodeNameTable) {
    if (st_lookup(NodeNameTable, name, NIL(char *))) {
      int       pos;

      sprintf(name, "_synth_%s%d", InternalNodePrefix, id);
      pos = 7; /* _synth_ */
      while (st_lookup(NodeNameTable, name, NIL(char *))) {
        sprintf(&name[pos], "_%s%d", InternalNodePrefix, id);
        pos++;
      }
    }
  } else {
    (void)fprintf(vis_stdout,
                  "** synth warning: skipping internal node name checking.\n");
  }
}


void
SynthDumpBlif(Ntk_Network_t *net,
              bdd_manager *dd,
              int no,
              bdd_node **ofuncs,
              char **onames,
              int *initStates,
              char *model)
{
  int           size;
  bdd_node      **bdds;
  FILE          *fout;
  char          **inames;
  char          filename[MAX_NAME_LEN];
  int           i;
  lsGen         gen;
  Ntk_Node_t    *node;
  char          **sorted_name;
  int           ni, po;

  sprintf(filename, "%s.debug.blif", model);
  fout = fopen(filename, "w");
  if (!fout) {
    (void)fprintf(vis_stderr,
                  "** synth error: Can't open the file %s.\n", filename);
    return;
  }

  fprintf(fout, ".model %s\n", model);
  fprintf(fout, ".inputs");

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);

  fprintf(fout, "\n");
  fprintf(fout, ".outputs");

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);
  fprintf(fout, "\n");

  /* Print list of latches. */
  i = 0;
  Ntk_NetworkForEachLatch(net, gen, node) {
    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
    fprintf(fout, " %s", Ntk_NodeReadName(node));
    fprintf(fout, " %d\n", initStates[i]);
    i++;
  }

  bdds = ALLOC(bdd_node *, no);

  for (i = 0; i < no; i++) {
    bdds[i] = bdd_make_bdd_from_zdd_cover(dd, ofuncs[i]);
    bdd_ref(bdds[i]);
  }

  inames = GetAllVarNameArray(dd);
  if (!inames) {
    for (i = 0; i < no; i++)
      bdd_recursive_deref(dd, bdds[i]);
    FREE(bdds);
    fclose(fout);
    (void)fprintf(vis_stderr, "** synth error: Out of memory.\n");
    return;
  }

  bdd_dump_blif_body(dd, no, bdds, inames, onames, fout);
  fprintf(fout, ".end\n");

  size = bdd_num_vars(dd);
  for (i = 0; i < size; i++)
    FREE(inames[i]);
  FREE(inames);

  for (i = 0; i < no; i++)
    bdd_recursive_deref(dd, bdds[i]);

  FREE(bdds);
  fclose(fout);
}


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

static void
WriteMlBlif(Ntk_Network_t *net,
            bdd_manager *dd,
            MlTree *tree,
            FILE *fout,
            int no,
            bdd_node **ofuncs,
            int *oflags,
            int top_flag,
            int verbosity)
{
  int           i;
  char          name[MAX_NAME_LEN], q_name[MAX_NAME_LEN];
  char          d_name[MAX_NAME_LEN], r_name[MAX_NAME_LEN];
  char          eq[MAX_EQ_LEN];
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  char          q, d, r;
  int           comp;

  if (tree->leaf) {
    WriteLeafMlBlif(net, dd, tree, fout, no, ofuncs, oflags, top_flag,
                    verbosity);
    return;
  }

  if (!tree->ref) {
    if (!tree->q_ref)
      WriteMlBlif(net, dd, tree->q, fout, no, ofuncs, oflags, 0, verbosity);
    if (!tree->d_ref)
      WriteMlBlif(net, dd, tree->d, fout, no, ofuncs, oflags, 0, verbosity);
    if (!tree->r_ref)
      WriteMlBlif(net, dd, tree->r, fout, no, ofuncs, oflags, 0, verbosity);
  }

  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      if (top_flag == 0)
        return;

      if (oflags[i])
        continue;
      else
        oflags[i] = 1;
      sprintf(name, "%s",  SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no)
    SynthGetInternalNodeName(name, tree->id);

  fprintf(fout, "\n");
  if (verbosity > 2) {
    SynthGetChildMlTreeWithName(net, dd, tree, eq);
    (void)fprintf(fout, "# %s\n", eq);
  }

  if (tree->q->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->q->node, q_name);

    if (comp)
      q = '0';
    else
      q = '1';
    if (tree->q_comp) {
      if (q == '0')
        q = '1';
      else
        q = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->q->node == ofuncs[i]) {
        sprintf(q_name, "%s",  SynthGetIthOutputName(i));
        break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(q_name, tree->q->id);
    if (tree->q_comp)
      q = '0';
    else
      q = '1';
  }
  if (tree->d->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->d->node, d_name);

    if (comp)
      d = '0';
    else
      d = '1';
    if (tree->d_comp) {
      if (d == '0')
        d = '1';
      else
        d = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->d->node == ofuncs[i]) {
        sprintf(d_name, "%s", SynthGetIthOutputName(i));
        break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(d_name, tree->d->id);
    if (tree->d_comp)
      d = '0';
    else
      d = '1';
  }
  if (tree->r->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->r->node, r_name);

    if (comp)
      r = '0';
    else
      r = '1';
    if (tree->r_comp) {
      if (r == '0')
        r = '1';
      else
        r = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->r->node == ofuncs[i]) {
        sprintf(r_name, "%s", SynthGetIthOutputName(i));
        break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(r_name, tree->r->id);
    if (tree->r_comp)
      r = '0';
    else
      r = '1';
  }

  if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero ||
      GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "0\n");
    } else {
      fprintf(fout, ".names %s %s\n", r_name, name);
      fprintf(fout, "%c 1\n", r);
    }
  } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
    if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "0\n");
      } else {
        fprintf(fout, ".names %s %s\n", r_name, name);
        fprintf(fout, "%c 1\n", r);
      }
    } else {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
        fprintf(fout, ".names %s %s\n", d_name, name);
        fprintf(fout, "%c 1\n", d);
      } else {
        fprintf(fout, ".names %s %s %s\n", d_name, r_name,
                name);
        fprintf(fout, "%c- 1\n", d);
        fprintf(fout, "-%c 1\n", r);
      }
    }
  } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
    if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero) {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "0\n");
      } else {
        fprintf(fout, ".names %s %s\n", r_name, name);
        fprintf(fout, "%c 1\n", r);
      }
    } else {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
        fprintf(fout, ".names %s\n", name);
        fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
        fprintf(fout, ".names %s %s\n", q_name, name);
        fprintf(fout, "%c 1\n", q);
      } else {
        fprintf(fout, ".names %s %s %s\n", q_name, r_name, name);
        fprintf(fout, "%c- 1\n", q);
        fprintf(fout, "-%c 1\n", r);
      }
    }
  } else {
    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
      fprintf(fout, ".names %s %s %s\n", q_name, d_name, name);
      fprintf(fout, "%c%c 1\n", q, d);
    } else {
      fprintf(fout, ".names %s %s %s %s\n", q_name, d_name, r_name, name);
      fprintf(fout, "%c%c- 1\n", q, d);
      fprintf(fout, "--%c 1\n", r);
    }
  }
}

static void
WriteLeafMlBlif(Ntk_Network_t *net,
                bdd_manager *dd,
                MlTree *tree,
                FILE *fout,
                int no,
                bdd_node **ofuncs,
                int *oflags,
                int top_flag,
                int verbosity)
{
  int           i, count, *support;
  char          name[MAX_EQ_LEN];
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  char          out_name[MAX_NAME_LEN];
  bdd_node      *node;
  Ntk_Node_t    *ntk_node;
  int           sizeZ;

  sizeZ = bdd_num_zdd_vars(dd);

  if (tree->node == one || tree->node == zero || tree->pi)
    return;

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;
  for (i = 0; i < no; i++) {
    if (node == ofuncs[i]) {
      if (top_flag == 0)
        return;

      if (oflags[i])
        continue;
      else
        oflags[i] = 1;
      sprintf(out_name, "%s", SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no)
    SynthGetInternalNodeName(out_name, tree->id);
  else {
    ntk_node = Ntk_NetworkFindNodeByName(net, out_name);
    if (Ntk_NodeTestIsLatch(ntk_node))
      return;
  }

  fprintf(fout, "\n");
  if (verbosity > 2) {
    SynthGetChildMlTreeWithName(net, dd, tree, name);
    fprintf(fout, "# %s\n", name);
  }
  fprintf(fout, ".names ");

  support = ALLOC(int, sizeZ);
  if (!support)
    return;
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  count = 0;
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      fprintf(fout, "%s ", name);
      if (i % 2 == 0) {
        support[i] = count;
        i++;
        if (support[i])
          support[i] = count;
      } else {
        support[i] = count;
      }
      count++;
    }
  }
  fprintf(fout, "%s\n", out_name);

  for (i = 0; i < count; i++)
    name[i] = '-';
  name[count] = '\0';
  WriteBlifBinary(dd, node, name, fout, support);
  FREE(support);
}


static void
WriteBlifBinary(bdd_manager *dd,
                bdd_node *node,
                char *name,
                FILE *fout,
                int *support)
{
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  int           id = bdd_node_read_index(node);

  if (node == zero)
    return;

  if (node == one) {
    fprintf(fout, "%s 1\n", name);
    return;
  }

  if (id % 2 == 0)
    name[support[id]] = '1';
  else
    name[support[id]] = '0';
  WriteBlifBinary(dd, bdd_bdd_T(node), name, fout, support);
  name[support[id]] = '-';
  WriteBlifBinary(dd, bdd_bdd_E(node), name, fout, support);
  name[support[id]] = '-';
}


static void
WriteEqnOfTree(FILE *fout,
               Ntk_Network_t *net,
               bdd_manager *dd,
               MlTree *tree,
               bdd_node **ofuncs)
{
  char  eq[MAX_EQ_LEN];
  char  name[MAX_NAME_LEN];
  int   polarity = 0;

  polarity = GetMlTreeName(net, ofuncs, tree, name);
  eq[0] = '\0';
  GetEqnOfTree(net, dd, tree, tree, eq, ofuncs);
  if (polarity)
    SynthMakeComplementString(eq);
  fprintf(fout, "%s = %s\n", name, eq);
}


static int
GetEqnOfTree(Ntk_Network_t *net,
             bdd_manager *dd,
             MlTree *top,
             MlTree *tree,
             char *eq,
             bdd_node **ofuncs)
{
  char          q_eq[MAX_EQ_LEN];
  char          d_eq[MAX_EQ_LEN];
  char          r_eq[MAX_EQ_LEN];
  char          qd_eq[MAX_EQ_LEN];
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *f;
  int           flag;
  int           polarity = 0;

  if (tree != top && tree->shared) {
    polarity = GetMlTreeName(net, ofuncs, tree, eq);
    if (polarity)
      SynthMakeComplementString(eq);
    return(0);
  }

  f = tree->node;
  if (tree->leaf) {
    flag = SynthGetChildTreeWithName(net, dd, f, eq);
    return(flag);
  }

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  q_eq[0] = d_eq[0] = r_eq[0] = '\0';
  flag = GetEqnOfTree(net, dd, top, tree->q, q_eq, ofuncs);
  if (tree->q_comp)
    SynthMakeComplementString(q_eq);
  if (flag)
    return(1);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
    d_eq[0] = '\0';
  else {
    flag = GetEqnOfTree(net, dd, top, tree->d, d_eq, ofuncs);
    if (tree->d_comp)
      SynthMakeComplementString(d_eq);
    if (flag)
      return(1);
  }
  flag = GetEqnOfTree(net, dd, top, tree->r, r_eq, ofuncs);
  if (tree->r_comp)
    SynthMakeComplementString(r_eq);
  if (flag)
    return(1);

  if (strcmp(q_eq, "one") == 0)
    sprintf(qd_eq, "%s", d_eq);
  else if (strcmp(q_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else if (strcmp(d_eq, "one") == 0)
    sprintf(qd_eq, "%s", q_eq);
  else if (strcmp(d_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else {
    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", q_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
        eq[MAX_EQ_LEN - 1] = '\0';
      } else {
        eq[strlen(eq)] = '#'; /* truncated */
        eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(qd_eq, "%s %s", q_eq, d_eq);
  }

  if (strcmp(r_eq, "zero") == 0)
    sprintf(eq, "%s", qd_eq);
  else {
    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", qd_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
        eq[MAX_EQ_LEN - 1] = '\0';
      } else {
        eq[strlen(eq)] = '#'; /* truncated */
        eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
  }
  return(0);
}


static void
WriteMlTreeBlif(FILE *fout,
                Ntk_Network_t *net,
                bdd_manager *dd,
                MlTree *tree,
                bdd_node **ofuncs,
                int no,
                char *func_name,
                int ref)
{
  char  name[MAX_NAME_LEN];
  int   polarity = 0;

  if (tree->top || tree->shared) {
    if (ref) {
      if (tree->ref) {
        polarity = GetMlTreeName(net, ofuncs, tree, name);
        fprintf(fout, "\n.names %s %s\n", name, func_name);
        if (polarity == 0) {
          if (tree->comp)
            fprintf(fout, "0 1\n");
          else
            fprintf(fout, "1 1\n");
        } else {
          if (tree->comp)
            fprintf(fout, "1 1\n");
          else
            fprintf(fout, "0 1\n");
        }
        return;
      }
    }
    WriteMultiLevelBlif(fout, net, dd, tree, ofuncs, no);
  }

  if (tree->leaf)
    return;

  if (tree->q_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->q, ofuncs, no, NULL, ref);
  if (tree->d_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->d, ofuncs, no, NULL, ref);
  if (tree->r_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->r, ofuncs, no, NULL, ref);
}


static void
WriteMultiLevelBlif(FILE *fout,
                    Ntk_Network_t *net,
                    bdd_manager *dd,
                    MlTree *tree,
                    bdd_node **ofuncs,
                    int no)
{
  int                   i, ni;
  char                  name[MAX_NAME_LEN];
  TruthTableLine        *lines, *cur, *next;
  st_table              *table;
  char                  **sorted_name, *key;
  st_generator          *gen;
  int                   pos;
  Ntk_Node_t            *ntk_node;
  int                   polarity = 0;

  polarity = GetMlTreeName(net, ofuncs, tree, name);
  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      ntk_node = Ntk_NetworkFindNodeByName(net, name);
      if (Ntk_NodeTestIsLatch(ntk_node))
        return;
    }
  }

  table = st_init_table(strcmp, st_strhash);
  ni = 0;
  ni = GetMultiLevelNodes(net, dd, tree, tree, ofuncs, no, table, ni);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  st_foreach_item_int(table, gen, (char **)&key, &pos) {
    sorted_name[i] = key;
    i++;
  }
  qsort(sorted_name, ni, sizeof(char *),
        (int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < ni; i++) {
    st_insert(table, (char *)sorted_name[i], (char *)(long)i);
  }
  lines = GetMultiLevelBlifRecur(net, dd, tree, tree, ofuncs, no, table, ni);
  fprintf(fout, "\n.names");
  for (i = 0; i < ni; i++)
    fprintf(fout, " %s", sorted_name[i]);
  fprintf(fout, " %s\n", name);
  cur = lines;
  while (cur) {
    next = cur->next;
    if (polarity == 0)
      fprintf(fout, "%s 1\n", cur->values);
    else
      fprintf(fout, "%s 0\n", cur->values);
    FREE(cur->values);
    FREE(cur);
    cur = next;
  }
  st_free_table(table);
  for (i = 0; i < ni; i++)
    FREE(sorted_name[i]);
  FREE(sorted_name);
}


static TruthTableLine *
GetMultiLevelBlifRecur(Ntk_Network_t *net,
                       bdd_manager *dd,
                       MlTree *top,
                       MlTree *tree,
                       bdd_node **ofuncs,
                       int no,
                       st_table *table,
                       int ni)
{
  bdd_node              *one = bdd_read_one(dd);
  bdd_node              *zero = bdd_read_zero(dd);
  bdd_node              *f;
  TruthTableLine        *line;
  TruthTableLine        *cur, *q_line, *d_line, *r_line;
  int                   pos;
  char                  name[MAX_NAME_LEN];
  int                   polarity = 0;

  line = (TruthTableLine *)NULL;

  if (tree != top && tree->shared) {
    polarity = GetMlTreeName(net, ofuncs, tree, name);
    line = GetTautologyLine(ni);
    if (st_lookup_int(table, (char *)name, (int *)(&pos))) {
      if (polarity == 0)
        line->values[pos] = '1';
      else
        line->values[pos] = '0';
    }
    return(line);
  }

  f = tree->node;
  if (tree->leaf) {
    line = GetLeafLines(net, dd, tree, ofuncs, no, table, ni);
    return(line);
  }

  if (f == one || f == zero)
    return(line);

  q_line = GetMultiLevelBlifRecur(net, dd, top, tree->q, ofuncs,
                                  no, table, ni);
  if (q_line && tree->q_comp)
    q_line = GetComplementLines(q_line, ni, 1);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
    d_line = (TruthTableLine *)NULL;
  else {
    d_line = GetMultiLevelBlifRecur(net, dd, top, tree->d, ofuncs, no,
                                    table, ni);
    if (d_line && tree->d_comp)
      d_line = GetComplementLines(d_line, ni, 1);
  }
  if (q_line && d_line)
    line = GetAndLines(q_line, d_line, ni, 1);
  else if (q_line)
    line = q_line;
  else if (d_line)
    line = d_line;
  r_line = GetMultiLevelBlifRecur(net, dd, top, tree->r, ofuncs, no, table, ni);
  if (r_line && tree->r_comp)
    r_line = GetComplementLines(r_line, ni, 1);
  if (r_line) {
    cur = line;
    while (cur) {
      if (!cur->next) {
        cur->next = r_line;
        break;
      }
      cur = cur->next;
    }
  }

  return(line);
}


static int
GetMultiLevelNodes(Ntk_Network_t *net,
                   bdd_manager *dd,
                   MlTree *top,
                   MlTree *tree,
                   bdd_node **ofuncs,
                   int no,
                   st_table *table,
                   int ni)
{
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *f;
  char          name[MAX_NAME_LEN], *st_name;
  int           pos;

  if (tree != top && tree->shared) {
    (void) GetMlTreeName(net, ofuncs, tree, name);
    if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
      st_name = ALLOC(char, strlen(name) + 1);
      strcpy(st_name, name);
      st_insert(table, (char *)st_name, (char *)(long)ni);
      ni++;
    }
    return(ni);
  }

  f = tree->node;
  if (tree->leaf) {
    ni = GetLeafNodes(net, dd, tree, ofuncs, no, table, ni);
    return(ni);
  }

  if (f == one || f == zero)
    return(ni);

  ni = GetMultiLevelNodes(net, dd, top, tree->q, ofuncs, no, table, ni);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) != one)
    ni = GetMultiLevelNodes(net, dd, top, tree->d, ofuncs, no, table, ni);
  ni = GetMultiLevelNodes(net, dd, top, tree->r, ofuncs, no, table, ni);

  return(ni);
}


static int
GetLeafNodes(Ntk_Network_t *net,
             bdd_manager *dd,
             MlTree *tree,
             bdd_node **ofuncs,
             int no,
             st_table *table,
             int ni)
{
  int           i, *support;
  char          name[MAX_NAME_LEN], *st_name;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *node;
  int           pos, sizeZ = bdd_num_zdd_vars(dd);

  if (tree->node == one || tree->node == zero)
    return(ni);

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;

  support = ALLOC(int, sizeZ);
  if (!support)
    return(ni);
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
        st_name = ALLOC(char, strlen(name) + 1);
        strcpy(st_name, name);
        st_insert(table, (char *)st_name, (char *)(long)ni);
        ni++;
      }
    }
  }
  FREE(support);
  return(ni);
}


static TruthTableLine *
GetTautologyLine(int ni)
{
  int                   i;
  TruthTableLine        *line;

  line = ALLOC(TruthTableLine, 1);
  (void)memset((void *)line, 0, sizeof(TruthTableLine));
  line->values = (char *)malloc(ni + 1);
  for (i = 0; i < ni; i++)
    line->values[i] = '-';
  line->values[ni] = '\0';
  return(line);
}


static TruthTableLine *
GetLeafLines(Ntk_Network_t *net,
             bdd_manager *dd,
             MlTree *tree,
             bdd_node **ofuncs,
             int no,
             st_table *table,
             int ni)
{
  int                   i, *support;
  char                  values[MAX_EQ_LEN];
  bdd_node              *one = bdd_read_one(dd);
  bdd_node              *zero = bdd_read_zero(dd);
  bdd_node              *node;
  TruthTableLine        *line;
  int                   pos, sizeZ = bdd_num_zdd_vars(dd);
  char                  name[MAX_NAME_LEN];

  line = (TruthTableLine *)NULL;

  if (tree->node == one || tree->node == zero)
    return(line);

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;

  support = ALLOC(int, sizeZ);
  if (!support)
    return(line);
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
        fprintf(vis_stdout,
                "** synth error: Failed to find %s in hash.\n", name);
      }
      support[i] = pos;
    }
  }

  for (i = 0; i < ni; i++)
    values[i] = '-';
  values[ni] = '\0';
  line = GetBlifBinary(line, dd, node, values, support, ni);
  FREE(support);
  return(line);
}


static TruthTableLine *
GetBlifBinary(TruthTableLine *line,
              bdd_manager *dd,
              bdd_node *node,
              char *values,
              int *support,
              int ni)
{
  bdd_node              *one = bdd_read_one(dd);
  bdd_node              *zero = bdd_read_zero(dd);
  TruthTableLine        *new_, *cur;
  int                   id = bdd_node_read_index(node);

  if (node == zero)
    return(line);

  if (node == one) {
    new_ = ALLOC(TruthTableLine, 1);
    (void)memset((void *)new_, 0, sizeof(TruthTableLine));
    new_->values = ALLOC(char,ni+1);
    strcpy(new_->values, values);
    if (line) {
      cur = line;
      while (cur->next)
        cur = cur->next;
      cur->next = new_;
    } else
      line = new_;
    return(line);
  }

  if (id % 2 == 0)
    values[support[id]] = '1';
  else
    values[support[id]] = '0';
  line = GetBlifBinary(line, dd, bdd_bdd_T(node), values, support, ni);
  values[support[id]] = '-';
  line = GetBlifBinary(line, dd, bdd_bdd_E(node), values, support, ni);
  values[support[id]] = '-';
  return(line);
}


static TruthTableLine *
GetComplementOneLine(TruthTableLine *line,
                     int ni,
                     int flag)
{
  int                   i;
  TruthTableLine        *new_line, *start, *last;

  start = last = (TruthTableLine *)NULL;

  for (i = 0; i < ni; i++) {
    if (line->values[i] != '-') {
      new_line = GetTautologyLine(ni);
      if (line->values[i] == '1')
        new_line->values[i] = '0';
      else
        new_line->values[i] = '1';
      if (last) {
        last->next = new_line;
        last = new_line;
      } else
        start = last = new_line;
    }
  }

  if (flag) {
    FREE(line->values);
    FREE(line);
  }

  return(start);
}


static TruthTableLine *
GetComplementLines(TruthTableLine *lines,
                   int ni,
                   int flag)
{
  TruthTableLine        *first, *cur, *next;

  if (!lines)
    return(lines);

  first = lines;
  cur = first->next;
  first = GetComplementOneLine(first, ni, flag);
  while (cur) {
    next = cur->next;
    cur = GetComplementOneLine(cur, ni, flag);
    first = GetAndLines(first, cur, ni, flag);
    cur = next;
  }
  return(first);
}


static TruthTableLine *
GetAndLines(TruthTableLine *line1,
            TruthTableLine *line2,
            int ni,
            int flag)
{
  int                   i;
  TruthTableLine        *cur1, *cur2, *next1, *next2;
  TruthTableLine        *start, *last;
  TruthTableLine        *new_line;

  start = last = (TruthTableLine *)NULL;

  cur1 = line1;
  while (cur1) {
    next1 = cur1->next;
    cur2 = line2;
    while (cur2) {
      new_line = GetTautologyLine(ni);
      strcpy(new_line->values, cur1->values);
      for (i = 0; i < ni; i++) {
        if (cur2->values[i] != '-')
          new_line->values[i] = cur2->values[i];
      }
      if (last) {
        last->next = new_line;
        last = new_line;
      } else {
        start = last = new_line;
      }
      cur2 = cur2->next;
    }
    if (flag) {
      FREE(cur1->values);
      FREE(cur1);
    }
    cur1 = next1;
  }

  if (flag) {
    cur2 = line2;
    while (cur2) {
      next2 = cur2->next;
      FREE(cur2->values);
      FREE(cur2);
      cur2 = next2;
    }
  }

  return(start);
}


static bdd_node *
GetDdNodeOfMlTree(MlTree *tree,
                  int comp)
{
  if (comp)
    return(tree->complement);
  return(tree->node);
}

static int
GetMlTreeName(Ntk_Network_t *net,
              bdd_node **ofuncs,
              MlTree *tree,
              char *name)
{
  int   i, no;
  int   polarity = 0; /* positive */

  no = Ntk_NetworkReadNumCombOutputs(net) - Ntk_NetworkReadNumLatches(net);
  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      sprintf(name, "%s", SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no) {
    if (tree->pi)
      polarity = SynthGetPrimaryNodeName(net, tree->node, name);
    else
      SynthGetInternalNodeName(name, tree->id);
  }

  return(polarity);
}

static char **
GetAllVarNameArray(bdd_manager *dd)
{
  int           size, i, j;
  mvar_type     var;
  char          **nameArray, *name;

  size = bdd_num_vars(dd);
  nameArray = ALLOC(char *, size);
  if (!nameArray)
    return(NIL(char *));

  for (i = 0; i < size; i++) {
    var = mdd_get_var_by_id(dd, i);
    name = ALLOC(char, strlen(var.name) + 1);
    if (!name) {
      for (j = 0; j < i; j++)
        FREE(nameArray[j]);
      FREE(nameArray);
      return(NIL(char *));
    }
    strcpy(name, var.name);
    nameArray[i] = name;
  }
  
  return(nameArray);
}