/**CFile***********************************************************************

  FileName    [absUtil.c]

  PackageName [abs]

  Synopsis [Some miscelaneous functions for non-critical tasks such as printing
  information, sanity checks, etc]

  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#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                                                        */
/*---------------------------------------------------------------------------*/


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

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

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

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


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

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

/**Function********************************************************************

  Synopsis [Print recursively the sub-graph from a given vertex in DOT format.]

  Description [The function receives a pointer to a vertex and a file
  descriptor. It prints the sub-graph starting with the given vertex in DOT
  format. The DOT format can be found in the graph visualization package in <a
  href="http://www.research.att.com/orgs/ssr/book/reuse">
  http://www.research.att.com/orgs/ssr/book/reuse</a>.]

  SideEffects        []

  SeeAlso            [AbsVertexInfo]

******************************************************************************/
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 */


/**Function********************************************************************

  Synopsis [Function to print the information stored in a vertex.]

  Description [The function receives a pointer to a vertex, a table with
  vertices already visited and a variable to enable recursion. If the vertex is
  already in the table, it is not printed. Otherwise, its contents is printed,
  and if recur is true, the sub-formulas are recursively printed.]

  SideEffects        []

  SeeAlso            [AbsVertexInfo]

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis           [Function to print the cubes of a BDD.]

  SideEffects        []

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis [Function to detect portions of a formula that need to be evaluated
  only once]

  Description [This procedure detects portions of a formula that need to be
  evaluated only once. This amounts basically to detect if there is any vertex
  representing a variable in a fix-point. If not, after the formula has been
  evaluated it is declared constant and no further evaluation is required.]

  SideEffects        [required]

  SeeAlso            [optional]

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis [Standard tests to check if the graph represenging a formula is
  correctly built]

  SideEffects        []

  SeeAlso            [AbsVertexInfo]

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis           [Sanity check for the set of iterates in a fixed point]

  Description [This function verifies the property that in the sequence of
  iterates of a fixed point s_1,...,s_n, if i<j then s_i\subseteq s_j. If the
  condition is not satisfied it returns a FALSE. Its use is recommended inside
  an assert clause, that way, whenever the property is not satisfied, the
  program aborts]

  SideEffects        []

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis           [Print the statistics report]

  SideEffects        []

******************************************************************************/
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                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis           [Prints the vertex content in DOT format.]

  SideEffects        []

  SeeAlso            [AbsVertexPrintDot]

******************************************************************************/
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 */

/**Function********************************************************************

  Synopsis           [Returns the string representing a vertex type.]

  SideEffects        []

******************************************************************************/
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 */