src/abs/absUtil.c

Go to the documentation of this file.

#include <time.h>
#include "absInt.h" 

static char rcsid[] UNUSED = "$Id: absUtil.c,v 1.17 2005/04/16 04:22:21 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


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

static void VertexPrintDotRecur(FILE *fp, AbsVertexInfo_t *vertex, st_table *visited);
static char * VertexTypeToString(AbsVertexInfo_t *vertex);

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

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

void
AbsVertexPrintDot(
  FILE *fp,
  array_t *vertexArray)
{
  AbsVertexInfo_t *vertexPtr;
  st_table        *visited;
  struct tm       *nowStructPtr;
  char            *nowTxt;
  time_t          now;
  int i;

  /* Initialize some variables */
  now = time(0);
  nowStructPtr = localtime(&now);
  nowTxt = asctime(nowStructPtr);
  visited = st_init_table(st_ptrcmp, st_ptrhash);

  /*
   * Write out the header for the output file.
   */
  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
  (void) fprintf(fp, "# generated: %s", nowTxt);
  (void) fprintf(fp, "#\n");

  (void) fprintf(fp, "digraph \"Formula\" {\n  rotate=90;\n");
  (void) fprintf(fp, "  margin=0.5;\n  label=\"Formula\";\n");
  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vertexPtr) {
    VertexPrintDotRecur(fp, vertexPtr, visited);
  }

  (void) fprintf(fp, "}\n");
  st_free_table(visited);

  return;
} /* End of AbsVertexPrintDot */


void
AbsVertexPrint(
  AbsVertexInfo_t *vertexPtr,
  st_table *visitedSF,
  boolean recur,
  long verbosity)
{
  st_table *newVisitedSF;

  newVisitedSF = NIL(st_table);
  if (recur && visitedSF == NIL(st_table)) {
    newVisitedSF = st_init_table(st_ptrcmp, st_ptrhash);
    (void) fprintf(vis_stdout, "ABS:----------------------------------");
    (void) fprintf(vis_stdout, "-------------------\n");
  }
  else {
    newVisitedSF = visitedSF;
  }

  if (newVisitedSF != NIL(st_table)) {
    if (st_is_member(newVisitedSF, (char *)vertexPtr)) {
      return;
    }
    st_insert(newVisitedSF, (char *)vertexPtr, NIL(char));
  }

  /* Print the type of vertex */
  (void) fprintf(vis_stdout, "ABS: Vertex(%3d)-(",
                 AbsVertexReadId(vertexPtr));
  switch(AbsVertexReadType(vertexPtr)) {
    case identifier_c:
      (void) fprintf(vis_stdout, "Identifier ");
      break;
    case false_c:
      (void) fprintf(vis_stdout, "   FALSE   ");
      break;
    case variable_c:
      (void) fprintf(vis_stdout, " Variable  ");
      break;
    case fixedPoint_c:
      (void) fprintf(vis_stdout, "Fixed Point");
      break;
    case preImage_c:
      (void) fprintf(vis_stdout, " PreImage  ");
      break;
    case not_c:
      (void) fprintf(vis_stdout, "    Not    ");
      break;
    case and_c: 
      (void) fprintf(vis_stdout, "    and    ");
      break;
    case xor_c:
      (void) fprintf(vis_stdout, "    xor    ");
      break;
    case xnor_c:
      (void) fprintf(vis_stdout, "    xnor   ");
      break;
    default: fail("Encountered unknown type of Vertex\n");
  }
  (void) fprintf(vis_stdout, ") (%p)-> ", (void *) vertexPtr);

  /* Print pointer to kids  */
  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    (void) fprintf(vis_stdout, "(%p)/",
                   (void *) AbsVertexReadLeftKid(vertexPtr));
  }
  else {
    (void) fprintf(vis_stdout, "(---NIL---)/");
  }
  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    (void) fprintf(vis_stdout, "(%p)\n",
                   (void *) AbsVertexReadRightKid(vertexPtr));
  }
  else {
    (void) fprintf(vis_stdout, "(---NIL---)\n");
  }

  /* Print Sat */
  if (AbsVertexReadType(vertexPtr) != variable_c) {
    (void) fprintf(vis_stdout, "ABS: Sat  -> ");
    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
      (void) fprintf(vis_stdout, "%d Nodes\n", 
                     mdd_size(AbsVertexReadSat(vertexPtr)));
      if (verbosity & ABS_VB_SCUBE) {
        AbsBddPrintMinterms(AbsVertexReadSat(vertexPtr));
      }
    }
    else {
      (void) fprintf(vis_stdout, "NIL\n");
    }
  }

  /* Print refs, served, polarity, depth, localApprox and globalApprox */
  (void) fprintf(vis_stdout, 
                 "ABS: Rfs Svd Plrty Dpth LclApp GlblApp Cnt Ref\n");
  (void) fprintf(vis_stdout, "ABS: %3d %3d %3d %6d %4d %6d %5d %3d\n",
                 AbsVertexReadRefs(vertexPtr), AbsVertexReadServed(vertexPtr),
                 AbsVertexReadPolarity(vertexPtr), 
                 AbsVertexReadDepth(vertexPtr),
                 AbsVertexReadLocalApprox(vertexPtr),
                 AbsVertexReadGlobalApprox(vertexPtr),
                 AbsVertexReadConstant(vertexPtr),
                 AbsVertexReadTrueRefine(vertexPtr));

  /* Print the parents */
  (void) fprintf(vis_stdout, "ABS: Parents-> ");
  if (lsLength(AbsVertexReadParent(vertexPtr)) != 0) {
    AbsVertexInfo_t *parent;
    lsList parentList;
    lsGen listGen;

    parentList = AbsVertexReadParent(vertexPtr);
    lsForEachItem(parentList, listGen, parent) {
      if (parent == NIL(AbsVertexInfo_t)) {
        (void) fprintf(vis_stdout, "(---NIL---) ");
      }
      else {
        (void) fprintf(vis_stdout, "%p ", (void *) parent);
      }
    }
    (void) fprintf(vis_stdout, "\n");
  }
  else {
    (void) fprintf(vis_stdout, "---NIL--\n");
  }

  /* Print Sub-systems*/
  if (AbsVertexReadType(vertexPtr) == preImage_c) {
    (void) fprintf(vis_stdout, "ABS: Solutions-> ");
    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
      AbsEvalCacheEntry_t *entry;
      st_generator        *stgen;
      array_t             *units;
      bdd_node            *key;

      units = array_alloc(mdd_t *, 0);
      st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key, &entry) {
        array_insert_last(mdd_t *, units, 
                          AbsEvalCacheEntryReadResult(entry));
      }
      (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n",
                     array_n(units), mdd_size_multiple(units));
      array_free(units);
    }
    else {
      (void) fprintf(vis_stdout, "---NIL--\n");
    }
  }

  /* Print the localId */
  if (AbsVertexReadType(vertexPtr) == variable_c) {
    (void) fprintf(vis_stdout, "ABS: Variable Id-> %d\n",
                   AbsVertexReadVarId(vertexPtr));
  }

  if (AbsVertexReadType(vertexPtr) == fixedPoint_c) {
    /* Print the variable vertex  */
    (void) fprintf(vis_stdout, "ABS: Variable Vertex-> %p\n", 
                   (void *) AbsVertexReadFpVar(vertexPtr));
    
    /* Print the rings */
    (void) fprintf(vis_stdout, "ABS: Rings->");
    if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) {
      (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n",
                     array_n(AbsVertexReadRings(vertexPtr)),
                     mdd_size_multiple(AbsVertexReadRings(vertexPtr)));
    }
    else {
      (void) fprintf(vis_stdout, " NIL\n");
    }
    /* Print the approximation flags */
    (void) fprintf(vis_stdout, "ABS: ApproxRings-> ");
    if (AbsVertexReadRingApprox(vertexPtr) != NIL(array_t)) {
      int unit;
      int i;
      
      arrayForEachItem(int, AbsVertexReadRingApprox(vertexPtr), i, unit) {
        (void) fprintf(vis_stdout, "%d,", unit);
      }
      (void) fprintf(vis_stdout, "\n");
    }
    else {
      (void) fprintf(vis_stdout, " NIL\n");
    }
    
    /* Print the sub-approximation flags */
    (void) fprintf(vis_stdout, "ABS: SubApproxRings-> ");
    if (AbsVertexReadSubApprox(vertexPtr) != NIL(array_t)) {
      int unit;
      int i;
      
      arrayForEachItem(int, AbsVertexReadSubApprox(vertexPtr), i, unit) {
        (void) fprintf(vis_stdout, "%d,", unit);
      }
      (void) fprintf(vis_stdout, "\n");
    }
    else {
      (void) fprintf(vis_stdout, " NIL\n");
    }
  }

  /* Print name and value of the identifier */
  if (AbsVertexReadType(vertexPtr) == identifier_c) {
    (void) fprintf(vis_stdout, "ABS: Name/Value-> %s/%s\n",
                   AbsVertexReadName(vertexPtr), AbsVertexReadValue(vertexPtr));
  }

  (void) fprintf(vis_stdout, "ABS:----------------------------------");
  (void) fprintf(vis_stdout, "-------------------\n");

  /* Print the sub-formulas recursively if enabled */
  if (recur) {
    if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
      AbsVertexPrint(AbsVertexReadLeftKid(vertexPtr), newVisitedSF, recur,
                     verbosity);
    }
    
    if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
      AbsVertexPrint(AbsVertexReadRightKid(vertexPtr), newVisitedSF, recur,
                     verbosity);
    }
  }

  /* Clean up */
  if (visitedSF != newVisitedSF) {
    st_free_table(newVisitedSF);
  }

  return;
} /* End of AbsVertexPrint */

void
AbsBddPrintMinterms(
  mdd_t *function)
{
  bdd_gen *gen;
  array_t *cube;
  int i;
  int literal;

  if (mdd_is_tautology(function, 1)) {
    (void) fprintf(vis_stdout, "Tautology\n");
    return;
  }

  if (mdd_is_tautology(function, 0)) {
    (void) fprintf(vis_stdout, "EmptyBdd\n");
    return;
  }

  /* Allocate the generator and start the iteration */
  gen = bdd_first_cube(function, &cube);

  do {
    arrayForEachItem(int, cube, i, literal) {
      if (literal == 2) {
        (void) fprintf(vis_stdout, "-");
      }
      else {
        (void) fprintf(vis_stdout, "%1d", literal);
      }
    }
    (void) fprintf(vis_stdout, "\n");
  } while (bdd_next_cube(gen, &cube));

  /* Clean Up */
  bdd_gen_free(gen);
} /* End of AbsBddPrintMinterms */

void
AbsFormulaSetConstantBit(
  AbsVertexInfo_t *vertexPtr)
{
  boolean leftCntBit;
  boolean rightCntBit;

  if (AbsVertexReadType(vertexPtr) == identifier_c) {
    AbsVertexSetConstant(vertexPtr, TRUE);
    return;
  }

  if (AbsVertexReadType(vertexPtr) == variable_c) {
    AbsVertexSetConstant(vertexPtr, FALSE);
    return;
  }

  leftCntBit = TRUE;
  rightCntBit = TRUE;

  /* Recursive call in the left kid */
  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    AbsFormulaSetConstantBit(AbsVertexReadLeftKid(vertexPtr));
    leftCntBit = AbsVertexReadConstant(AbsVertexReadLeftKid(vertexPtr));
  }

  /* Recursive call in the right kid */
  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    AbsFormulaSetConstantBit(AbsVertexReadRightKid(vertexPtr));
    rightCntBit = AbsVertexReadConstant(AbsVertexReadRightKid(vertexPtr));
  }

  AbsVertexSetConstant(vertexPtr, leftCntBit && rightCntBit);

  return;
} /* End of AbsFormulaSetConstantBit */

boolean
AbsFormulaSanityCheck(
  AbsVertexInfo_t *vertexPtr,
  st_table *rootTable)
{
  AbsVertexInfo_t *aux;
  boolean result;
  lsGen listGen;
  int leftDepth;
  int rightDepth;

  result = TRUE;

  /* Check the type */
  if (AbsVertexReadType(vertexPtr) == false_c) {
    result = FALSE;
    (void) fprintf(vis_stdout, "** abs error: Illegal formula type.\n");
  }

  /* Check the refs and the served fields */
  if (AbsVertexReadRefs(vertexPtr) < 0 || AbsVertexReadServed(vertexPtr) < 0 ||
      AbsVertexReadRefs(vertexPtr) < AbsVertexReadServed(vertexPtr)) {
    result = FALSE;
    (void) fprintf(vis_stdout, "** abs error: Illegal value on reference count.\n");
  }

  /* Check the depth */
  leftDepth = AbsVertexReadDepth(vertexPtr) - 1;
  rightDepth = AbsVertexReadDepth(vertexPtr) - 1;
  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    leftDepth = AbsVertexReadDepth(AbsVertexReadLeftKid(vertexPtr));
  }
  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    rightDepth = AbsVertexReadDepth(AbsVertexReadRightKid(vertexPtr));
  }
  if (leftDepth + 1 != AbsVertexReadDepth(vertexPtr) &&
      rightDepth + 1 != AbsVertexReadDepth(vertexPtr)) {
    result = FALSE;
    (void) fprintf(vis_stdout, "** abs error: Illegal depth value.\n");
  }

  /* Check if the parent pointers are correctly set */
  lsForEachItem(AbsVertexReadParent(vertexPtr), listGen, aux) {
    if (AbsVertexReadLeftKid(aux) != vertexPtr && 
        AbsVertexReadRightKid(aux) != vertexPtr) {
      lsFinish(listGen);
      result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal parent pointer.\n");
    }
  }
  
  /* Check if number of parents and ref agree */
  if ((lsLength(AbsVertexReadParent(vertexPtr)) +
       st_is_member(rootTable, (char *) vertexPtr)) !=
      AbsVertexReadRefs(vertexPtr)) {
    result = FALSE;
    (void) fprintf(vis_stdout, "** abs error: Illegal number of parents.\n");
  }

  /* Check if the constant flag is properly set */
  if (AbsVertexReadConstant(vertexPtr)) {
    if (AbsVertexReadType(vertexPtr) == variable_c) {
      result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
    }
    else {
      AbsVertexInfo_t *leftKid;
      AbsVertexInfo_t *rightKid;

      leftKid = AbsVertexReadLeftKid(vertexPtr);
      rightKid = AbsVertexReadRightKid(vertexPtr);

      if (leftKid != NIL(AbsVertexInfo_t)  && !AbsVertexReadConstant(leftKid)) {
        result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
      }
      if (rightKid != NIL(AbsVertexInfo_t) && 
          !AbsVertexReadConstant(rightKid)) {
        result = FALSE;
        (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
      }
    }
  }

  /* Check the polarity labeling */
  if (AbsVertexReadType(vertexPtr) == not_c) {
    if (AbsVertexReadPolarity(vertexPtr) == 
        AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) {
      result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
    }
  }
  else {
    if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t) &&
        AbsVertexReadPolarity(vertexPtr) !=
        AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) {
      result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
    }
    if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) &&
        AbsVertexReadPolarity(vertexPtr) !=
        AbsVertexReadPolarity(AbsVertexReadRightKid(vertexPtr))) {
      result = FALSE;
      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
    }
  }
  
  if (!result) {
    return result;
  }

  /* Recur over the sub-formulas */
  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    result = AbsFormulaSanityCheck(AbsVertexReadLeftKid(vertexPtr), rootTable);
  }
  
  if (!result) {
    return result;
  }

  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) && 
      AbsVertexReadType(vertexPtr) != fixedPoint_c) {
    result = AbsFormulaSanityCheck(AbsVertexReadRightKid(vertexPtr), rootTable);
  }
  
  return result;
} /* End of AbsFormulaSanityCheck */

boolean
AbsIteratesSanityCheck(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  array_t *rings;
  mdd_t *element;
  mdd_t *previous;
  mdd_t *careSet;
  boolean result;
  int index;

  /* Variable initialization */
  careSet = AbsVerificationInfoReadCareSet(absInfo);
  result = TRUE;
  rings = AbsVertexReadRings(vertexPtr);
  element = NIL(mdd_t);
  previous = NIL(mdd_t);

  arrayForEachItem(mdd_t *, rings, index, element) {
    if (previous != NIL(mdd_t)) {
      result = result && AbsMddLEqualModCareSet(previous, element, careSet);
      if (AbsMddEqualModCareSet(previous, element, careSet) &&
          index != array_n(rings) - 1) {
        result = FALSE;
      }
    }
    previous = element;
  }

  return result;
} /* End of AbsIteratesSanityCheck */

void
AbsStatsPrintReport(
  FILE *fp,
  AbsStats_t *stats)
{
  (void) fprintf(fp, "ABS: ------- Statistics Begin Report -------\n");
  (void) fprintf(fp, "ABS: FixedPoint Evaluated %6d times\n",
                 AbsStatsReadEvalFixedPoint(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefineFixedPoint(stats));
  (void) fprintf(fp, "ABS: And        Evaluated %6d times\n",
                 AbsStatsReadEvalAnd(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefineAnd(stats));
  (void) fprintf(fp, "ABS: Not        Evaluated %6d times\n",
                 AbsStatsReadEvalNot(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefineNot(stats));
  (void) fprintf(fp, "ABS: PreImage   Evaluated %6d times\n",
                 AbsStatsReadEvalPreImage(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefinePreImage(stats));
  (void) fprintf(fp, "ABS: Identifier Evaluated %6d times\n",
                 AbsStatsReadEvalIdentifier(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefineIdentifier(stats));
  (void) fprintf(fp, "ABS: Variable   Evaluated %6d times\n",
                 AbsStatsReadEvalVariable(stats));
  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
                 AbsStatsReadRefineVariable(stats));
  (void) fprintf(fp, "ABS: ---------------------------------------\n");
  (void) fprintf(fp, "ABS: Preimage Exact       %6d times\n",
                 AbsStatsReadExactPreImage(stats));
  (void) fprintf(fp, "ABS:          Approx.     %6d times\n",
                 AbsStatsReadApproxPreImage(stats));
  (void) fprintf(fp, "ABS: Image    Exact       %6d times\n",
                 AbsStatsReadExactImage(stats));
  (void) fprintf(fp, "ABS: ---------------------------------------\n");
  (void) fprintf(fp, "ABS: PreImg CacheEntries  %6d entries\n",
                 AbsStatsReadPreImageCacheEntries(stats));
  (void) fprintf(fp, "ABS: Img    CacheEntries  %6d entries\n",
                 AbsStatsReadImageCacheEntries(stats));
  (void) fprintf(fp, "ABS: ---------------------------------------\n");
  (void) fprintf(fp, "ABS: PreImg Cpu Time     %7.1f seconds\n",
                 AbsStatsReadPreImageCpuTime(stats)/1000.0);
  (void) fprintf(fp, "ABS: AppPre Cpu Time     %7.1f seconds\n",
                 AbsStatsReadAppPreCpuTime(stats)/1000.0);
  (void) fprintf(fp, "ABS: Image  Cpu Time     %7.1f seconds\n",
                 AbsStatsReadImageCpuTime(stats)/1000.0);
  (void) fprintf(fp, "ABS: ---------------------------------------\n");
  (void) fprintf(fp, "ABS: Reordering Invoked   %6d times\n",
                 AbsStatsReadNumReorderings(stats));
  (void) fprintf(fp, "ABS: ---------------------------------------\n");
  util_print_cpu_stats(vis_stdout);
  (void) fprintf(fp, "ABS: -------  Statistics End Report  -------\n");

  return;
} /* End of AbsStatsPrintReport */


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

static void
VertexPrintDotRecur(
  FILE *fp,
  AbsVertexInfo_t *vertex,
  st_table *visited)
{
  AbsVertexInfo_t *leftKid;
  AbsVertexInfo_t *rightKid;

  /* Check the cache */
  if (st_is_member(visited, (char *)vertex)) {
    return;
  }

  /* Recur in the left kid if needed */
  leftKid = AbsVertexReadLeftKid(vertex);
  if (leftKid != NIL(AbsVertexInfo_t)) {
    VertexPrintDotRecur(fp, AbsVertexReadLeftKid(vertex), visited);
    
    if (AbsVertexReadType(leftKid) != identifier_c) {
      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 
                     VertexTypeToString(vertex),
                     AbsVertexReadId(vertex),
                     AbsVertexReadPolarity(vertex)?'+':'-', 
                     VertexTypeToString(leftKid),
                     AbsVertexReadId(leftKid),
                     AbsVertexReadPolarity(leftKid)?'+':'-');
    }
    else {
      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n",
                     VertexTypeToString(vertex),
                     AbsVertexReadId(vertex),
                     AbsVertexReadPolarity(vertex)?'+':'-',
                     AbsVertexReadName(leftKid),
                     AbsVertexReadValue(leftKid),
                     AbsVertexReadId(leftKid),
                     AbsVertexReadPolarity(leftKid)?'+':'-');
    }
  }
    
  /* Recur in the right kid if needed */
  rightKid = AbsVertexReadRightKid(vertex);
  if (rightKid != NIL(AbsVertexInfo_t)) {
    VertexPrintDotRecur(fp, AbsVertexReadRightKid(vertex), visited);

    if (AbsVertexReadType(rightKid) != identifier_c) {
      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 
                     VertexTypeToString(vertex),
                     AbsVertexReadId(vertex),
                     AbsVertexReadPolarity(vertex)?'+':'-', 
                     VertexTypeToString(rightKid),
                     AbsVertexReadId(rightKid),
                     AbsVertexReadPolarity(rightKid)?'+':'-');
    }
    else {
      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n",
                     VertexTypeToString(vertex),
                     AbsVertexReadId(vertex),
                     AbsVertexReadPolarity(vertex)?'+':'-',
                     AbsVertexReadName(rightKid),
                     AbsVertexReadValue(rightKid),
                     AbsVertexReadId(rightKid),
                     AbsVertexReadPolarity(rightKid)?'+':'-');
    }
  }

  st_insert(visited, (char *)vertex, NIL(char));
  
  return;
} /* End of VertexPrintDotRecur */

static char *
VertexTypeToString(
  AbsVertexInfo_t *vertex)
{
  char *typeStr;

  switch (AbsVertexReadType(vertex)) {
    case fixedPoint_c:
      typeStr = "LFP";
      break;
    case and_c:
      typeStr = "AND";
      break;
    case xor_c:
      typeStr = "XOR";
      break;
    case xnor_c:
      typeStr = "XNOR";
      break;
    case not_c:
      typeStr = "NOT";
      break;
    case preImage_c:
      typeStr = "Pre";
      break;
    case identifier_c:
      typeStr = "Id";
      break;
    case variable_c:
      typeStr = "VAR";
      break;
    case false_c:
      typeStr = "FALSE";
      break;
    default:
      fail("Unknown vertex type.");
      break;
  }

  return typeStr;
} /* End of VertexTypeToString */