source: vis_dev/vis-2.3/src/abs/absUtil.c @ 50

Last change on this file since 50 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 25.7 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [absUtil.c]
4
5  PackageName [abs]
6
7  Synopsis [Some miscelaneous functions for non-critical tasks such as printing
8  information, sanity checks, etc]
9
10  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
11
12  Copyright   [This file was created at the University of Colorado at
13  Boulder.  The University of Colorado at Boulder makes no warranty
14  about the suitability of this software for any purpose.  It is
15  presented on an AS IS basis.]
16
17******************************************************************************/
18
19#include <time.h>
20#include "absInt.h"
21
22static char rcsid[] UNUSED = "$Id: absUtil.c,v 1.17 2005/04/16 04:22:21 fabio Exp $";
23
24/*---------------------------------------------------------------------------*/
25/* Macro declarations                                                        */
26/*---------------------------------------------------------------------------*/
27
28
29/**AutomaticStart*************************************************************/
30
31/*---------------------------------------------------------------------------*/
32/* Static function prototypes                                                */
33/*---------------------------------------------------------------------------*/
34
35static void VertexPrintDotRecur(FILE *fp, AbsVertexInfo_t *vertex, st_table *visited);
36static char * VertexTypeToString(AbsVertexInfo_t *vertex);
37
38/**AutomaticEnd***************************************************************/
39
40
41/*---------------------------------------------------------------------------*/
42/* Definition of exported functions                                          */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Definition of internal functions                                          */
47/*---------------------------------------------------------------------------*/
48
49/**Function********************************************************************
50
51  Synopsis [Print recursively the sub-graph from a given vertex in DOT format.]
52
53  Description [The function receives a pointer to a vertex and a file
54  descriptor. It prints the sub-graph starting with the given vertex in DOT
55  format. The DOT format can be found in the graph visualization package in <a
56  href="http://www.research.att.com/orgs/ssr/book/reuse">
57  http://www.research.att.com/orgs/ssr/book/reuse</a>.]
58
59  SideEffects        []
60
61  SeeAlso            [AbsVertexInfo]
62
63******************************************************************************/
64void
65AbsVertexPrintDot(
66  FILE *fp,
67  array_t *vertexArray)
68{
69  AbsVertexInfo_t *vertexPtr;
70  st_table        *visited;
71  struct tm       *nowStructPtr;
72  char            *nowTxt;
73  time_t          now;
74  int i;
75
76  /* Initialize some variables */
77  now = time(0);
78  nowStructPtr = localtime(&now);
79  nowTxt = asctime(nowStructPtr);
80  visited = st_init_table(st_ptrcmp, st_ptrhash);
81
82  /*
83   * Write out the header for the output file.
84   */
85  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
86  (void) fprintf(fp, "# generated: %s", nowTxt);
87  (void) fprintf(fp, "#\n");
88
89  (void) fprintf(fp, "digraph \"Formula\" {\n  rotate=90;\n");
90  (void) fprintf(fp, "  margin=0.5;\n  label=\"Formula\";\n");
91  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
92
93  arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vertexPtr) {
94    VertexPrintDotRecur(fp, vertexPtr, visited);
95  }
96
97  (void) fprintf(fp, "}\n");
98  st_free_table(visited);
99
100  return;
101} /* End of AbsVertexPrintDot */
102
103
104/**Function********************************************************************
105
106  Synopsis [Function to print the information stored in a vertex.]
107
108  Description [The function receives a pointer to a vertex, a table with
109  vertices already visited and a variable to enable recursion. If the vertex is
110  already in the table, it is not printed. Otherwise, its contents is printed,
111  and if recur is true, the sub-formulas are recursively printed.]
112
113  SideEffects        []
114
115  SeeAlso            [AbsVertexInfo]
116
117******************************************************************************/
118void
119AbsVertexPrint(
120  AbsVertexInfo_t *vertexPtr,
121  st_table *visitedSF,
122  boolean recur,
123  long verbosity)
124{
125  st_table *newVisitedSF;
126
127  newVisitedSF = NIL(st_table);
128  if (recur && visitedSF == NIL(st_table)) {
129    newVisitedSF = st_init_table(st_ptrcmp, st_ptrhash);
130    (void) fprintf(vis_stdout, "ABS:----------------------------------");
131    (void) fprintf(vis_stdout, "-------------------\n");
132  }
133  else {
134    newVisitedSF = visitedSF;
135  }
136
137  if (newVisitedSF != NIL(st_table)) {
138    if (st_is_member(newVisitedSF, (char *)vertexPtr)) {
139      return;
140    }
141    st_insert(newVisitedSF, (char *)vertexPtr, NIL(char));
142  }
143
144  /* Print the type of vertex */
145  (void) fprintf(vis_stdout, "ABS: Vertex(%3d)-(",
146                 AbsVertexReadId(vertexPtr));
147  switch(AbsVertexReadType(vertexPtr)) {
148    case identifier_c:
149      (void) fprintf(vis_stdout, "Identifier ");
150      break;
151    case false_c:
152      (void) fprintf(vis_stdout, "   FALSE   ");
153      break;
154    case variable_c:
155      (void) fprintf(vis_stdout, " Variable  ");
156      break;
157    case fixedPoint_c:
158      (void) fprintf(vis_stdout, "Fixed Point");
159      break;
160    case preImage_c:
161      (void) fprintf(vis_stdout, " PreImage  ");
162      break;
163    case not_c:
164      (void) fprintf(vis_stdout, "    Not    ");
165      break;
166    case and_c: 
167      (void) fprintf(vis_stdout, "    and    ");
168      break;
169    case xor_c:
170      (void) fprintf(vis_stdout, "    xor    ");
171      break;
172    case xnor_c:
173      (void) fprintf(vis_stdout, "    xnor   ");
174      break;
175    default: fail("Encountered unknown type of Vertex\n");
176  }
177  (void) fprintf(vis_stdout, ") (%p)-> ", (void *) vertexPtr);
178
179  /* Print pointer to kids  */
180  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
181    (void) fprintf(vis_stdout, "(%p)/",
182                   (void *) AbsVertexReadLeftKid(vertexPtr));
183  }
184  else {
185    (void) fprintf(vis_stdout, "(---NIL---)/");
186  }
187  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
188    (void) fprintf(vis_stdout, "(%p)\n",
189                   (void *) AbsVertexReadRightKid(vertexPtr));
190  }
191  else {
192    (void) fprintf(vis_stdout, "(---NIL---)\n");
193  }
194
195  /* Print Sat */
196  if (AbsVertexReadType(vertexPtr) != variable_c) {
197    (void) fprintf(vis_stdout, "ABS: Sat  -> ");
198    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
199      (void) fprintf(vis_stdout, "%d Nodes\n", 
200                     mdd_size(AbsVertexReadSat(vertexPtr)));
201      if (verbosity & ABS_VB_SCUBE) {
202        AbsBddPrintMinterms(AbsVertexReadSat(vertexPtr));
203      }
204    }
205    else {
206      (void) fprintf(vis_stdout, "NIL\n");
207    }
208  }
209
210  /* Print refs, served, polarity, depth, localApprox and globalApprox */
211  (void) fprintf(vis_stdout, 
212                 "ABS: Rfs Svd Plrty Dpth LclApp GlblApp Cnt Ref\n");
213  (void) fprintf(vis_stdout, "ABS: %3d %3d %3d %6d %4d %6d %5d %3d\n",
214                 AbsVertexReadRefs(vertexPtr), AbsVertexReadServed(vertexPtr),
215                 AbsVertexReadPolarity(vertexPtr), 
216                 AbsVertexReadDepth(vertexPtr),
217                 AbsVertexReadLocalApprox(vertexPtr),
218                 AbsVertexReadGlobalApprox(vertexPtr),
219                 AbsVertexReadConstant(vertexPtr),
220                 AbsVertexReadTrueRefine(vertexPtr));
221
222  /* Print the parents */
223  (void) fprintf(vis_stdout, "ABS: Parents-> ");
224  if (lsLength(AbsVertexReadParent(vertexPtr)) != 0) {
225    AbsVertexInfo_t *parent;
226    lsList parentList;
227    lsGen listGen;
228
229    parentList = AbsVertexReadParent(vertexPtr);
230    lsForEachItem(parentList, listGen, parent) {
231      if (parent == NIL(AbsVertexInfo_t)) {
232        (void) fprintf(vis_stdout, "(---NIL---) ");
233      }
234      else {
235        (void) fprintf(vis_stdout, "%p ", (void *) parent);
236      }
237    }
238    (void) fprintf(vis_stdout, "\n");
239  }
240  else {
241    (void) fprintf(vis_stdout, "---NIL--\n");
242  }
243
244  /* Print Sub-systems*/
245  if (AbsVertexReadType(vertexPtr) == preImage_c) {
246    (void) fprintf(vis_stdout, "ABS: Solutions-> ");
247    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
248      AbsEvalCacheEntry_t *entry;
249      st_generator        *stgen;
250      array_t             *units;
251      bdd_node            *key;
252
253      units = array_alloc(mdd_t *, 0);
254      st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key, &entry) {
255        array_insert_last(mdd_t *, units, 
256                          AbsEvalCacheEntryReadResult(entry));
257      }
258      (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n",
259                     array_n(units), mdd_size_multiple(units));
260      array_free(units);
261    }
262    else {
263      (void) fprintf(vis_stdout, "---NIL--\n");
264    }
265  }
266
267  /* Print the localId */
268  if (AbsVertexReadType(vertexPtr) == variable_c) {
269    (void) fprintf(vis_stdout, "ABS: Variable Id-> %d\n",
270                   AbsVertexReadVarId(vertexPtr));
271  }
272
273  if (AbsVertexReadType(vertexPtr) == fixedPoint_c) {
274    /* Print the variable vertex  */
275    (void) fprintf(vis_stdout, "ABS: Variable Vertex-> %p\n", 
276                   (void *) AbsVertexReadFpVar(vertexPtr));
277   
278    /* Print the rings */
279    (void) fprintf(vis_stdout, "ABS: Rings->");
280    if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) {
281      (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n",
282                     array_n(AbsVertexReadRings(vertexPtr)),
283                     mdd_size_multiple(AbsVertexReadRings(vertexPtr)));
284    }
285    else {
286      (void) fprintf(vis_stdout, " NIL\n");
287    }
288    /* Print the approximation flags */
289    (void) fprintf(vis_stdout, "ABS: ApproxRings-> ");
290    if (AbsVertexReadRingApprox(vertexPtr) != NIL(array_t)) {
291      int unit;
292      int i;
293     
294      arrayForEachItem(int, AbsVertexReadRingApprox(vertexPtr), i, unit) {
295        (void) fprintf(vis_stdout, "%d,", unit);
296      }
297      (void) fprintf(vis_stdout, "\n");
298    }
299    else {
300      (void) fprintf(vis_stdout, " NIL\n");
301    }
302   
303    /* Print the sub-approximation flags */
304    (void) fprintf(vis_stdout, "ABS: SubApproxRings-> ");
305    if (AbsVertexReadSubApprox(vertexPtr) != NIL(array_t)) {
306      int unit;
307      int i;
308     
309      arrayForEachItem(int, AbsVertexReadSubApprox(vertexPtr), i, unit) {
310        (void) fprintf(vis_stdout, "%d,", unit);
311      }
312      (void) fprintf(vis_stdout, "\n");
313    }
314    else {
315      (void) fprintf(vis_stdout, " NIL\n");
316    }
317  }
318
319  /* Print name and value of the identifier */
320  if (AbsVertexReadType(vertexPtr) == identifier_c) {
321    (void) fprintf(vis_stdout, "ABS: Name/Value-> %s/%s\n",
322                   AbsVertexReadName(vertexPtr), AbsVertexReadValue(vertexPtr));
323  }
324
325  (void) fprintf(vis_stdout, "ABS:----------------------------------");
326  (void) fprintf(vis_stdout, "-------------------\n");
327
328  /* Print the sub-formulas recursively if enabled */
329  if (recur) {
330    if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
331      AbsVertexPrint(AbsVertexReadLeftKid(vertexPtr), newVisitedSF, recur,
332                     verbosity);
333    }
334   
335    if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
336      AbsVertexPrint(AbsVertexReadRightKid(vertexPtr), newVisitedSF, recur,
337                     verbosity);
338    }
339  }
340
341  /* Clean up */
342  if (visitedSF != newVisitedSF) {
343    st_free_table(newVisitedSF);
344  }
345
346  return;
347} /* End of AbsVertexPrint */
348
349/**Function********************************************************************
350
351  Synopsis           [Function to print the cubes of a BDD.]
352
353  SideEffects        []
354
355******************************************************************************/
356void
357AbsBddPrintMinterms(
358  mdd_t *function)
359{
360  bdd_gen *gen;
361  array_t *cube;
362  int i;
363  int literal;
364
365  if (mdd_is_tautology(function, 1)) {
366    (void) fprintf(vis_stdout, "Tautology\n");
367    return;
368  }
369
370  if (mdd_is_tautology(function, 0)) {
371    (void) fprintf(vis_stdout, "EmptyBdd\n");
372    return;
373  }
374
375  /* Allocate the generator and start the iteration */
376  gen = bdd_first_cube(function, &cube);
377
378  do {
379    arrayForEachItem(int, cube, i, literal) {
380      if (literal == 2) {
381        (void) fprintf(vis_stdout, "-");
382      }
383      else {
384        (void) fprintf(vis_stdout, "%1d", literal);
385      }
386    }
387    (void) fprintf(vis_stdout, "\n");
388  } while (bdd_next_cube(gen, &cube));
389
390  /* Clean Up */
391  bdd_gen_free(gen);
392} /* End of AbsBddPrintMinterms */
393
394/**Function********************************************************************
395
396  Synopsis [Function to detect portions of a formula that need to be evaluated
397  only once]
398
399  Description [This procedure detects portions of a formula that need to be
400  evaluated only once. This amounts basically to detect if there is any vertex
401  representing a variable in a fix-point. If not, after the formula has been
402  evaluated it is declared constant and no further evaluation is required.]
403
404  SideEffects        [required]
405
406  SeeAlso            [optional]
407
408******************************************************************************/
409void
410AbsFormulaSetConstantBit(
411  AbsVertexInfo_t *vertexPtr)
412{
413  boolean leftCntBit;
414  boolean rightCntBit;
415
416  if (AbsVertexReadType(vertexPtr) == identifier_c) {
417    AbsVertexSetConstant(vertexPtr, TRUE);
418    return;
419  }
420
421  if (AbsVertexReadType(vertexPtr) == variable_c) {
422    AbsVertexSetConstant(vertexPtr, FALSE);
423    return;
424  }
425
426  leftCntBit = TRUE;
427  rightCntBit = TRUE;
428
429  /* Recursive call in the left kid */
430  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
431    AbsFormulaSetConstantBit(AbsVertexReadLeftKid(vertexPtr));
432    leftCntBit = AbsVertexReadConstant(AbsVertexReadLeftKid(vertexPtr));
433  }
434
435  /* Recursive call in the right kid */
436  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
437    AbsFormulaSetConstantBit(AbsVertexReadRightKid(vertexPtr));
438    rightCntBit = AbsVertexReadConstant(AbsVertexReadRightKid(vertexPtr));
439  }
440
441  AbsVertexSetConstant(vertexPtr, leftCntBit && rightCntBit);
442
443  return;
444} /* End of AbsFormulaSetConstantBit */
445
446/**Function********************************************************************
447
448  Synopsis [Standard tests to check if the graph represenging a formula is
449  correctly built]
450
451  SideEffects        []
452
453  SeeAlso            [AbsVertexInfo]
454
455******************************************************************************/
456boolean
457AbsFormulaSanityCheck(
458  AbsVertexInfo_t *vertexPtr,
459  st_table *rootTable)
460{
461  AbsVertexInfo_t *aux;
462  boolean result;
463  lsGen listGen;
464  int leftDepth;
465  int rightDepth;
466
467  result = TRUE;
468
469  /* Check the type */
470  if (AbsVertexReadType(vertexPtr) == false_c) {
471    result = FALSE;
472    (void) fprintf(vis_stdout, "** abs error: Illegal formula type.\n");
473  }
474
475  /* Check the refs and the served fields */
476  if (AbsVertexReadRefs(vertexPtr) < 0 || AbsVertexReadServed(vertexPtr) < 0 ||
477      AbsVertexReadRefs(vertexPtr) < AbsVertexReadServed(vertexPtr)) {
478    result = FALSE;
479    (void) fprintf(vis_stdout, "** abs error: Illegal value on reference count.\n");
480  }
481
482  /* Check the depth */
483  leftDepth = AbsVertexReadDepth(vertexPtr) - 1;
484  rightDepth = AbsVertexReadDepth(vertexPtr) - 1;
485  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
486    leftDepth = AbsVertexReadDepth(AbsVertexReadLeftKid(vertexPtr));
487  }
488  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
489    rightDepth = AbsVertexReadDepth(AbsVertexReadRightKid(vertexPtr));
490  }
491  if (leftDepth + 1 != AbsVertexReadDepth(vertexPtr) &&
492      rightDepth + 1 != AbsVertexReadDepth(vertexPtr)) {
493    result = FALSE;
494    (void) fprintf(vis_stdout, "** abs error: Illegal depth value.\n");
495  }
496
497  /* Check if the parent pointers are correctly set */
498  lsForEachItem(AbsVertexReadParent(vertexPtr), listGen, aux) {
499    if (AbsVertexReadLeftKid(aux) != vertexPtr && 
500        AbsVertexReadRightKid(aux) != vertexPtr) {
501      lsFinish(listGen);
502      result = FALSE;
503      (void) fprintf(vis_stdout, "** abs error: Illegal parent pointer.\n");
504    }
505  }
506 
507  /* Check if number of parents and ref agree */
508  if ((lsLength(AbsVertexReadParent(vertexPtr)) +
509       st_is_member(rootTable, (char *) vertexPtr)) !=
510      AbsVertexReadRefs(vertexPtr)) {
511    result = FALSE;
512    (void) fprintf(vis_stdout, "** abs error: Illegal number of parents.\n");
513  }
514
515  /* Check if the constant flag is properly set */
516  if (AbsVertexReadConstant(vertexPtr)) {
517    if (AbsVertexReadType(vertexPtr) == variable_c) {
518      result = FALSE;
519      (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
520    }
521    else {
522      AbsVertexInfo_t *leftKid;
523      AbsVertexInfo_t *rightKid;
524
525      leftKid = AbsVertexReadLeftKid(vertexPtr);
526      rightKid = AbsVertexReadRightKid(vertexPtr);
527
528      if (leftKid != NIL(AbsVertexInfo_t)  && !AbsVertexReadConstant(leftKid)) {
529        result = FALSE;
530      (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
531      }
532      if (rightKid != NIL(AbsVertexInfo_t) && 
533          !AbsVertexReadConstant(rightKid)) {
534        result = FALSE;
535        (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n");
536      }
537    }
538  }
539
540  /* Check the polarity labeling */
541  if (AbsVertexReadType(vertexPtr) == not_c) {
542    if (AbsVertexReadPolarity(vertexPtr) == 
543        AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) {
544      result = FALSE;
545      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
546    }
547  }
548  else {
549    if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t) &&
550        AbsVertexReadPolarity(vertexPtr) !=
551        AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) {
552      result = FALSE;
553      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
554    }
555    if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) &&
556        AbsVertexReadPolarity(vertexPtr) !=
557        AbsVertexReadPolarity(AbsVertexReadRightKid(vertexPtr))) {
558      result = FALSE;
559      (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n");
560    }
561  }
562 
563  if (!result) {
564    return result;
565  }
566
567  /* Recur over the sub-formulas */
568  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
569    result = AbsFormulaSanityCheck(AbsVertexReadLeftKid(vertexPtr), rootTable);
570  }
571 
572  if (!result) {
573    return result;
574  }
575
576  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) && 
577      AbsVertexReadType(vertexPtr) != fixedPoint_c) {
578    result = AbsFormulaSanityCheck(AbsVertexReadRightKid(vertexPtr), rootTable);
579  }
580 
581  return result;
582} /* End of AbsFormulaSanityCheck */
583
584/**Function********************************************************************
585
586  Synopsis           [Sanity check for the set of iterates in a fixed point]
587
588  Description [This function verifies the property that in the sequence of
589  iterates of a fixed point s_1,...,s_n, if i<j then s_i\subseteq s_j. If the
590  condition is not satisfied it returns a FALSE. Its use is recommended inside
591  an assert clause, that way, whenever the property is not satisfied, the
592  program aborts]
593
594  SideEffects        []
595
596******************************************************************************/
597boolean
598AbsIteratesSanityCheck(
599  Abs_VerificationInfo_t *absInfo,
600  AbsVertexInfo_t *vertexPtr)
601{
602  array_t *rings;
603  mdd_t *element;
604  mdd_t *previous;
605  mdd_t *careSet;
606  boolean result;
607  int index;
608
609  /* Variable initialization */
610  careSet = AbsVerificationInfoReadCareSet(absInfo);
611  result = TRUE;
612  rings = AbsVertexReadRings(vertexPtr);
613  element = NIL(mdd_t);
614  previous = NIL(mdd_t);
615
616  arrayForEachItem(mdd_t *, rings, index, element) {
617    if (previous != NIL(mdd_t)) {
618      result = result && AbsMddLEqualModCareSet(previous, element, careSet);
619      if (AbsMddEqualModCareSet(previous, element, careSet) &&
620          index != array_n(rings) - 1) {
621        result = FALSE;
622      }
623    }
624    previous = element;
625  }
626
627  return result;
628} /* End of AbsIteratesSanityCheck */
629
630/**Function********************************************************************
631
632  Synopsis           [Print the statistics report]
633
634  SideEffects        []
635
636******************************************************************************/
637void
638AbsStatsPrintReport(
639  FILE *fp,
640  AbsStats_t *stats)
641{
642  (void) fprintf(fp, "ABS: ------- Statistics Begin Report -------\n");
643  (void) fprintf(fp, "ABS: FixedPoint Evaluated %6d times\n",
644                 AbsStatsReadEvalFixedPoint(stats));
645  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
646                 AbsStatsReadRefineFixedPoint(stats));
647  (void) fprintf(fp, "ABS: And        Evaluated %6d times\n",
648                 AbsStatsReadEvalAnd(stats));
649  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
650                 AbsStatsReadRefineAnd(stats));
651  (void) fprintf(fp, "ABS: Not        Evaluated %6d times\n",
652                 AbsStatsReadEvalNot(stats));
653  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
654                 AbsStatsReadRefineNot(stats));
655  (void) fprintf(fp, "ABS: PreImage   Evaluated %6d times\n",
656                 AbsStatsReadEvalPreImage(stats));
657  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
658                 AbsStatsReadRefinePreImage(stats));
659  (void) fprintf(fp, "ABS: Identifier Evaluated %6d times\n",
660                 AbsStatsReadEvalIdentifier(stats));
661  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
662                 AbsStatsReadRefineIdentifier(stats));
663  (void) fprintf(fp, "ABS: Variable   Evaluated %6d times\n",
664                 AbsStatsReadEvalVariable(stats));
665  (void) fprintf(fp, "ABS:            Refined   %6d times\n",
666                 AbsStatsReadRefineVariable(stats));
667  (void) fprintf(fp, "ABS: ---------------------------------------\n");
668  (void) fprintf(fp, "ABS: Preimage Exact       %6d times\n",
669                 AbsStatsReadExactPreImage(stats));
670  (void) fprintf(fp, "ABS:          Approx.     %6d times\n",
671                 AbsStatsReadApproxPreImage(stats));
672  (void) fprintf(fp, "ABS: Image    Exact       %6d times\n",
673                 AbsStatsReadExactImage(stats));
674  (void) fprintf(fp, "ABS: ---------------------------------------\n");
675  (void) fprintf(fp, "ABS: PreImg CacheEntries  %6d entries\n",
676                 AbsStatsReadPreImageCacheEntries(stats));
677  (void) fprintf(fp, "ABS: Img    CacheEntries  %6d entries\n",
678                 AbsStatsReadImageCacheEntries(stats));
679  (void) fprintf(fp, "ABS: ---------------------------------------\n");
680  (void) fprintf(fp, "ABS: PreImg Cpu Time     %7.1f seconds\n",
681                 AbsStatsReadPreImageCpuTime(stats)/1000.0);
682  (void) fprintf(fp, "ABS: AppPre Cpu Time     %7.1f seconds\n",
683                 AbsStatsReadAppPreCpuTime(stats)/1000.0);
684  (void) fprintf(fp, "ABS: Image  Cpu Time     %7.1f seconds\n",
685                 AbsStatsReadImageCpuTime(stats)/1000.0);
686  (void) fprintf(fp, "ABS: ---------------------------------------\n");
687  (void) fprintf(fp, "ABS: Reordering Invoked   %6d times\n",
688                 AbsStatsReadNumReorderings(stats));
689  (void) fprintf(fp, "ABS: ---------------------------------------\n");
690  util_print_cpu_stats(vis_stdout);
691  (void) fprintf(fp, "ABS: -------  Statistics End Report  -------\n");
692
693  return;
694} /* End of AbsStatsPrintReport */
695
696
697/*---------------------------------------------------------------------------*/
698/* Definition of static functions                                            */
699/*---------------------------------------------------------------------------*/
700
701/**Function********************************************************************
702
703  Synopsis           [Prints the vertex content in DOT format.]
704
705  SideEffects        []
706
707  SeeAlso            [AbsVertexPrintDot]
708
709******************************************************************************/
710static void
711VertexPrintDotRecur(
712  FILE *fp,
713  AbsVertexInfo_t *vertex,
714  st_table *visited)
715{
716  AbsVertexInfo_t *leftKid;
717  AbsVertexInfo_t *rightKid;
718
719  /* Check the cache */
720  if (st_is_member(visited, (char *)vertex)) {
721    return;
722  }
723
724  /* Recur in the left kid if needed */
725  leftKid = AbsVertexReadLeftKid(vertex);
726  if (leftKid != NIL(AbsVertexInfo_t)) {
727    VertexPrintDotRecur(fp, AbsVertexReadLeftKid(vertex), visited);
728   
729    if (AbsVertexReadType(leftKid) != identifier_c) {
730      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 
731                     VertexTypeToString(vertex),
732                     AbsVertexReadId(vertex),
733                     AbsVertexReadPolarity(vertex)?'+':'-', 
734                     VertexTypeToString(leftKid),
735                     AbsVertexReadId(leftKid),
736                     AbsVertexReadPolarity(leftKid)?'+':'-');
737    }
738    else {
739      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n",
740                     VertexTypeToString(vertex),
741                     AbsVertexReadId(vertex),
742                     AbsVertexReadPolarity(vertex)?'+':'-',
743                     AbsVertexReadName(leftKid),
744                     AbsVertexReadValue(leftKid),
745                     AbsVertexReadId(leftKid),
746                     AbsVertexReadPolarity(leftKid)?'+':'-');
747    }
748  }
749   
750  /* Recur in the right kid if needed */
751  rightKid = AbsVertexReadRightKid(vertex);
752  if (rightKid != NIL(AbsVertexInfo_t)) {
753    VertexPrintDotRecur(fp, AbsVertexReadRightKid(vertex), visited);
754
755    if (AbsVertexReadType(rightKid) != identifier_c) {
756      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 
757                     VertexTypeToString(vertex),
758                     AbsVertexReadId(vertex),
759                     AbsVertexReadPolarity(vertex)?'+':'-', 
760                     VertexTypeToString(rightKid),
761                     AbsVertexReadId(rightKid),
762                     AbsVertexReadPolarity(rightKid)?'+':'-');
763    }
764    else {
765      (void) fprintf(fp, "  \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n",
766                     VertexTypeToString(vertex),
767                     AbsVertexReadId(vertex),
768                     AbsVertexReadPolarity(vertex)?'+':'-',
769                     AbsVertexReadName(rightKid),
770                     AbsVertexReadValue(rightKid),
771                     AbsVertexReadId(rightKid),
772                     AbsVertexReadPolarity(rightKid)?'+':'-');
773    }
774  }
775
776  st_insert(visited, (char *)vertex, NIL(char));
777 
778  return;
779} /* End of VertexPrintDotRecur */
780
781/**Function********************************************************************
782
783  Synopsis           [Returns the string representing a vertex type.]
784
785  SideEffects        []
786
787******************************************************************************/
788static char *
789VertexTypeToString(
790  AbsVertexInfo_t *vertex)
791{
792  char *typeStr;
793
794  switch (AbsVertexReadType(vertex)) {
795    case fixedPoint_c:
796      typeStr = "LFP";
797      break;
798    case and_c:
799      typeStr = "AND";
800      break;
801    case xor_c:
802      typeStr = "XOR";
803      break;
804    case xnor_c:
805      typeStr = "XNOR";
806      break;
807    case not_c:
808      typeStr = "NOT";
809      break;
810    case preImage_c:
811      typeStr = "Pre";
812      break;
813    case identifier_c:
814      typeStr = "Id";
815      break;
816    case variable_c:
817      typeStr = "VAR";
818      break;
819    case false_c:
820      typeStr = "FALSE";
821      break;
822    default:
823      fail("Unknown vertex type.");
824      break;
825  }
826
827  return typeStr;
828} /* End of VertexTypeToString */
829
Note: See TracBrowser for help on using the repository browser.