VIS
|
00001 00019 #include <time.h> 00020 #include "absInt.h" 00021 00022 static char rcsid[] UNUSED = "$Id: absUtil.c,v 1.17 2005/04/16 04:22:21 fabio Exp $"; 00023 00024 /*---------------------------------------------------------------------------*/ 00025 /* Macro declarations */ 00026 /*---------------------------------------------------------------------------*/ 00027 00028 00031 /*---------------------------------------------------------------------------*/ 00032 /* Static function prototypes */ 00033 /*---------------------------------------------------------------------------*/ 00034 00035 static void VertexPrintDotRecur(FILE *fp, AbsVertexInfo_t *vertex, st_table *visited); 00036 static char * VertexTypeToString(AbsVertexInfo_t *vertex); 00037 00041 /*---------------------------------------------------------------------------*/ 00042 /* Definition of exported functions */ 00043 /*---------------------------------------------------------------------------*/ 00044 00045 /*---------------------------------------------------------------------------*/ 00046 /* Definition of internal functions */ 00047 /*---------------------------------------------------------------------------*/ 00048 00064 void 00065 AbsVertexPrintDot( 00066 FILE *fp, 00067 array_t *vertexArray) 00068 { 00069 AbsVertexInfo_t *vertexPtr; 00070 st_table *visited; 00071 struct tm *nowStructPtr; 00072 char *nowTxt; 00073 time_t now; 00074 int i; 00075 00076 /* Initialize some variables */ 00077 now = time(0); 00078 nowStructPtr = localtime(&now); 00079 nowTxt = asctime(nowStructPtr); 00080 visited = st_init_table(st_ptrcmp, st_ptrhash); 00081 00082 /* 00083 * Write out the header for the output file. 00084 */ 00085 (void) fprintf(fp, "# %s\n", Vm_VisReadVersion()); 00086 (void) fprintf(fp, "# generated: %s", nowTxt); 00087 (void) fprintf(fp, "#\n"); 00088 00089 (void) fprintf(fp, "digraph \"Formula\" {\n rotate=90;\n"); 00090 (void) fprintf(fp, " margin=0.5;\n label=\"Formula\";\n"); 00091 (void) fprintf(fp, " size=\"10,7.5\";\n ratio=\"fill\";\n"); 00092 00093 arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vertexPtr) { 00094 VertexPrintDotRecur(fp, vertexPtr, visited); 00095 } 00096 00097 (void) fprintf(fp, "}\n"); 00098 st_free_table(visited); 00099 00100 return; 00101 } /* End of AbsVertexPrintDot */ 00102 00103 00118 void 00119 AbsVertexPrint( 00120 AbsVertexInfo_t *vertexPtr, 00121 st_table *visitedSF, 00122 boolean recur, 00123 long verbosity) 00124 { 00125 st_table *newVisitedSF; 00126 00127 newVisitedSF = NIL(st_table); 00128 if (recur && visitedSF == NIL(st_table)) { 00129 newVisitedSF = st_init_table(st_ptrcmp, st_ptrhash); 00130 (void) fprintf(vis_stdout, "ABS:----------------------------------"); 00131 (void) fprintf(vis_stdout, "-------------------\n"); 00132 } 00133 else { 00134 newVisitedSF = visitedSF; 00135 } 00136 00137 if (newVisitedSF != NIL(st_table)) { 00138 if (st_is_member(newVisitedSF, (char *)vertexPtr)) { 00139 return; 00140 } 00141 st_insert(newVisitedSF, (char *)vertexPtr, NIL(char)); 00142 } 00143 00144 /* Print the type of vertex */ 00145 (void) fprintf(vis_stdout, "ABS: Vertex(%3d)-(", 00146 AbsVertexReadId(vertexPtr)); 00147 switch(AbsVertexReadType(vertexPtr)) { 00148 case identifier_c: 00149 (void) fprintf(vis_stdout, "Identifier "); 00150 break; 00151 case false_c: 00152 (void) fprintf(vis_stdout, " FALSE "); 00153 break; 00154 case variable_c: 00155 (void) fprintf(vis_stdout, " Variable "); 00156 break; 00157 case fixedPoint_c: 00158 (void) fprintf(vis_stdout, "Fixed Point"); 00159 break; 00160 case preImage_c: 00161 (void) fprintf(vis_stdout, " PreImage "); 00162 break; 00163 case not_c: 00164 (void) fprintf(vis_stdout, " Not "); 00165 break; 00166 case and_c: 00167 (void) fprintf(vis_stdout, " and "); 00168 break; 00169 case xor_c: 00170 (void) fprintf(vis_stdout, " xor "); 00171 break; 00172 case xnor_c: 00173 (void) fprintf(vis_stdout, " xnor "); 00174 break; 00175 default: fail("Encountered unknown type of Vertex\n"); 00176 } 00177 (void) fprintf(vis_stdout, ") (%p)-> ", (void *) vertexPtr); 00178 00179 /* Print pointer to kids */ 00180 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00181 (void) fprintf(vis_stdout, "(%p)/", 00182 (void *) AbsVertexReadLeftKid(vertexPtr)); 00183 } 00184 else { 00185 (void) fprintf(vis_stdout, "(---NIL---)/"); 00186 } 00187 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00188 (void) fprintf(vis_stdout, "(%p)\n", 00189 (void *) AbsVertexReadRightKid(vertexPtr)); 00190 } 00191 else { 00192 (void) fprintf(vis_stdout, "(---NIL---)\n"); 00193 } 00194 00195 /* Print Sat */ 00196 if (AbsVertexReadType(vertexPtr) != variable_c) { 00197 (void) fprintf(vis_stdout, "ABS: Sat -> "); 00198 if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) { 00199 (void) fprintf(vis_stdout, "%d Nodes\n", 00200 mdd_size(AbsVertexReadSat(vertexPtr))); 00201 if (verbosity & ABS_VB_SCUBE) { 00202 AbsBddPrintMinterms(AbsVertexReadSat(vertexPtr)); 00203 } 00204 } 00205 else { 00206 (void) fprintf(vis_stdout, "NIL\n"); 00207 } 00208 } 00209 00210 /* Print refs, served, polarity, depth, localApprox and globalApprox */ 00211 (void) fprintf(vis_stdout, 00212 "ABS: Rfs Svd Plrty Dpth LclApp GlblApp Cnt Ref\n"); 00213 (void) fprintf(vis_stdout, "ABS: %3d %3d %3d %6d %4d %6d %5d %3d\n", 00214 AbsVertexReadRefs(vertexPtr), AbsVertexReadServed(vertexPtr), 00215 AbsVertexReadPolarity(vertexPtr), 00216 AbsVertexReadDepth(vertexPtr), 00217 AbsVertexReadLocalApprox(vertexPtr), 00218 AbsVertexReadGlobalApprox(vertexPtr), 00219 AbsVertexReadConstant(vertexPtr), 00220 AbsVertexReadTrueRefine(vertexPtr)); 00221 00222 /* Print the parents */ 00223 (void) fprintf(vis_stdout, "ABS: Parents-> "); 00224 if (lsLength(AbsVertexReadParent(vertexPtr)) != 0) { 00225 AbsVertexInfo_t *parent; 00226 lsList parentList; 00227 lsGen listGen; 00228 00229 parentList = AbsVertexReadParent(vertexPtr); 00230 lsForEachItem(parentList, listGen, parent) { 00231 if (parent == NIL(AbsVertexInfo_t)) { 00232 (void) fprintf(vis_stdout, "(---NIL---) "); 00233 } 00234 else { 00235 (void) fprintf(vis_stdout, "%p ", (void *) parent); 00236 } 00237 } 00238 (void) fprintf(vis_stdout, "\n"); 00239 } 00240 else { 00241 (void) fprintf(vis_stdout, "---NIL--\n"); 00242 } 00243 00244 /* Print Sub-systems*/ 00245 if (AbsVertexReadType(vertexPtr) == preImage_c) { 00246 (void) fprintf(vis_stdout, "ABS: Solutions-> "); 00247 if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) { 00248 AbsEvalCacheEntry_t *entry; 00249 st_generator *stgen; 00250 array_t *units; 00251 bdd_node *key; 00252 00253 units = array_alloc(mdd_t *, 0); 00254 st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key, &entry) { 00255 array_insert_last(mdd_t *, units, 00256 AbsEvalCacheEntryReadResult(entry)); 00257 } 00258 (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n", 00259 array_n(units), mdd_size_multiple(units)); 00260 array_free(units); 00261 } 00262 else { 00263 (void) fprintf(vis_stdout, "---NIL--\n"); 00264 } 00265 } 00266 00267 /* Print the localId */ 00268 if (AbsVertexReadType(vertexPtr) == variable_c) { 00269 (void) fprintf(vis_stdout, "ABS: Variable Id-> %d\n", 00270 AbsVertexReadVarId(vertexPtr)); 00271 } 00272 00273 if (AbsVertexReadType(vertexPtr) == fixedPoint_c) { 00274 /* Print the variable vertex */ 00275 (void) fprintf(vis_stdout, "ABS: Variable Vertex-> %p\n", 00276 (void *) AbsVertexReadFpVar(vertexPtr)); 00277 00278 /* Print the rings */ 00279 (void) fprintf(vis_stdout, "ABS: Rings->"); 00280 if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) { 00281 (void) fprintf(vis_stdout, "%d elements with size %ld Nodes.\n", 00282 array_n(AbsVertexReadRings(vertexPtr)), 00283 mdd_size_multiple(AbsVertexReadRings(vertexPtr))); 00284 } 00285 else { 00286 (void) fprintf(vis_stdout, " NIL\n"); 00287 } 00288 /* Print the approximation flags */ 00289 (void) fprintf(vis_stdout, "ABS: ApproxRings-> "); 00290 if (AbsVertexReadRingApprox(vertexPtr) != NIL(array_t)) { 00291 int unit; 00292 int i; 00293 00294 arrayForEachItem(int, AbsVertexReadRingApprox(vertexPtr), i, unit) { 00295 (void) fprintf(vis_stdout, "%d,", unit); 00296 } 00297 (void) fprintf(vis_stdout, "\n"); 00298 } 00299 else { 00300 (void) fprintf(vis_stdout, " NIL\n"); 00301 } 00302 00303 /* Print the sub-approximation flags */ 00304 (void) fprintf(vis_stdout, "ABS: SubApproxRings-> "); 00305 if (AbsVertexReadSubApprox(vertexPtr) != NIL(array_t)) { 00306 int unit; 00307 int i; 00308 00309 arrayForEachItem(int, AbsVertexReadSubApprox(vertexPtr), i, unit) { 00310 (void) fprintf(vis_stdout, "%d,", unit); 00311 } 00312 (void) fprintf(vis_stdout, "\n"); 00313 } 00314 else { 00315 (void) fprintf(vis_stdout, " NIL\n"); 00316 } 00317 } 00318 00319 /* Print name and value of the identifier */ 00320 if (AbsVertexReadType(vertexPtr) == identifier_c) { 00321 (void) fprintf(vis_stdout, "ABS: Name/Value-> %s/%s\n", 00322 AbsVertexReadName(vertexPtr), AbsVertexReadValue(vertexPtr)); 00323 } 00324 00325 (void) fprintf(vis_stdout, "ABS:----------------------------------"); 00326 (void) fprintf(vis_stdout, "-------------------\n"); 00327 00328 /* Print the sub-formulas recursively if enabled */ 00329 if (recur) { 00330 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00331 AbsVertexPrint(AbsVertexReadLeftKid(vertexPtr), newVisitedSF, recur, 00332 verbosity); 00333 } 00334 00335 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00336 AbsVertexPrint(AbsVertexReadRightKid(vertexPtr), newVisitedSF, recur, 00337 verbosity); 00338 } 00339 } 00340 00341 /* Clean up */ 00342 if (visitedSF != newVisitedSF) { 00343 st_free_table(newVisitedSF); 00344 } 00345 00346 return; 00347 } /* End of AbsVertexPrint */ 00348 00356 void 00357 AbsBddPrintMinterms( 00358 mdd_t *function) 00359 { 00360 bdd_gen *gen; 00361 array_t *cube; 00362 int i; 00363 int literal; 00364 00365 if (mdd_is_tautology(function, 1)) { 00366 (void) fprintf(vis_stdout, "Tautology\n"); 00367 return; 00368 } 00369 00370 if (mdd_is_tautology(function, 0)) { 00371 (void) fprintf(vis_stdout, "EmptyBdd\n"); 00372 return; 00373 } 00374 00375 /* Allocate the generator and start the iteration */ 00376 gen = bdd_first_cube(function, &cube); 00377 00378 do { 00379 arrayForEachItem(int, cube, i, literal) { 00380 if (literal == 2) { 00381 (void) fprintf(vis_stdout, "-"); 00382 } 00383 else { 00384 (void) fprintf(vis_stdout, "%1d", literal); 00385 } 00386 } 00387 (void) fprintf(vis_stdout, "\n"); 00388 } while (bdd_next_cube(gen, &cube)); 00389 00390 /* Clean Up */ 00391 bdd_gen_free(gen); 00392 } /* End of AbsBddPrintMinterms */ 00393 00409 void 00410 AbsFormulaSetConstantBit( 00411 AbsVertexInfo_t *vertexPtr) 00412 { 00413 boolean leftCntBit; 00414 boolean rightCntBit; 00415 00416 if (AbsVertexReadType(vertexPtr) == identifier_c) { 00417 AbsVertexSetConstant(vertexPtr, TRUE); 00418 return; 00419 } 00420 00421 if (AbsVertexReadType(vertexPtr) == variable_c) { 00422 AbsVertexSetConstant(vertexPtr, FALSE); 00423 return; 00424 } 00425 00426 leftCntBit = TRUE; 00427 rightCntBit = TRUE; 00428 00429 /* Recursive call in the left kid */ 00430 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00431 AbsFormulaSetConstantBit(AbsVertexReadLeftKid(vertexPtr)); 00432 leftCntBit = AbsVertexReadConstant(AbsVertexReadLeftKid(vertexPtr)); 00433 } 00434 00435 /* Recursive call in the right kid */ 00436 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00437 AbsFormulaSetConstantBit(AbsVertexReadRightKid(vertexPtr)); 00438 rightCntBit = AbsVertexReadConstant(AbsVertexReadRightKid(vertexPtr)); 00439 } 00440 00441 AbsVertexSetConstant(vertexPtr, leftCntBit && rightCntBit); 00442 00443 return; 00444 } /* End of AbsFormulaSetConstantBit */ 00445 00456 boolean 00457 AbsFormulaSanityCheck( 00458 AbsVertexInfo_t *vertexPtr, 00459 st_table *rootTable) 00460 { 00461 AbsVertexInfo_t *aux; 00462 boolean result; 00463 lsGen listGen; 00464 int leftDepth; 00465 int rightDepth; 00466 00467 result = TRUE; 00468 00469 /* Check the type */ 00470 if (AbsVertexReadType(vertexPtr) == false_c) { 00471 result = FALSE; 00472 (void) fprintf(vis_stdout, "** abs error: Illegal formula type.\n"); 00473 } 00474 00475 /* Check the refs and the served fields */ 00476 if (AbsVertexReadRefs(vertexPtr) < 0 || AbsVertexReadServed(vertexPtr) < 0 || 00477 AbsVertexReadRefs(vertexPtr) < AbsVertexReadServed(vertexPtr)) { 00478 result = FALSE; 00479 (void) fprintf(vis_stdout, "** abs error: Illegal value on reference count.\n"); 00480 } 00481 00482 /* Check the depth */ 00483 leftDepth = AbsVertexReadDepth(vertexPtr) - 1; 00484 rightDepth = AbsVertexReadDepth(vertexPtr) - 1; 00485 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00486 leftDepth = AbsVertexReadDepth(AbsVertexReadLeftKid(vertexPtr)); 00487 } 00488 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00489 rightDepth = AbsVertexReadDepth(AbsVertexReadRightKid(vertexPtr)); 00490 } 00491 if (leftDepth + 1 != AbsVertexReadDepth(vertexPtr) && 00492 rightDepth + 1 != AbsVertexReadDepth(vertexPtr)) { 00493 result = FALSE; 00494 (void) fprintf(vis_stdout, "** abs error: Illegal depth value.\n"); 00495 } 00496 00497 /* Check if the parent pointers are correctly set */ 00498 lsForEachItem(AbsVertexReadParent(vertexPtr), listGen, aux) { 00499 if (AbsVertexReadLeftKid(aux) != vertexPtr && 00500 AbsVertexReadRightKid(aux) != vertexPtr) { 00501 lsFinish(listGen); 00502 result = FALSE; 00503 (void) fprintf(vis_stdout, "** abs error: Illegal parent pointer.\n"); 00504 } 00505 } 00506 00507 /* Check if number of parents and ref agree */ 00508 if ((lsLength(AbsVertexReadParent(vertexPtr)) + 00509 st_is_member(rootTable, (char *) vertexPtr)) != 00510 AbsVertexReadRefs(vertexPtr)) { 00511 result = FALSE; 00512 (void) fprintf(vis_stdout, "** abs error: Illegal number of parents.\n"); 00513 } 00514 00515 /* Check if the constant flag is properly set */ 00516 if (AbsVertexReadConstant(vertexPtr)) { 00517 if (AbsVertexReadType(vertexPtr) == variable_c) { 00518 result = FALSE; 00519 (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n"); 00520 } 00521 else { 00522 AbsVertexInfo_t *leftKid; 00523 AbsVertexInfo_t *rightKid; 00524 00525 leftKid = AbsVertexReadLeftKid(vertexPtr); 00526 rightKid = AbsVertexReadRightKid(vertexPtr); 00527 00528 if (leftKid != NIL(AbsVertexInfo_t) && !AbsVertexReadConstant(leftKid)) { 00529 result = FALSE; 00530 (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n"); 00531 } 00532 if (rightKid != NIL(AbsVertexInfo_t) && 00533 !AbsVertexReadConstant(rightKid)) { 00534 result = FALSE; 00535 (void) fprintf(vis_stdout, "** abs error: Illegal constant flag.\n"); 00536 } 00537 } 00538 } 00539 00540 /* Check the polarity labeling */ 00541 if (AbsVertexReadType(vertexPtr) == not_c) { 00542 if (AbsVertexReadPolarity(vertexPtr) == 00543 AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) { 00544 result = FALSE; 00545 (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n"); 00546 } 00547 } 00548 else { 00549 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t) && 00550 AbsVertexReadPolarity(vertexPtr) != 00551 AbsVertexReadPolarity(AbsVertexReadLeftKid(vertexPtr))) { 00552 result = FALSE; 00553 (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n"); 00554 } 00555 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) && 00556 AbsVertexReadPolarity(vertexPtr) != 00557 AbsVertexReadPolarity(AbsVertexReadRightKid(vertexPtr))) { 00558 result = FALSE; 00559 (void) fprintf(vis_stdout, "** abs error: Illegal polarity labeling.\n"); 00560 } 00561 } 00562 00563 if (!result) { 00564 return result; 00565 } 00566 00567 /* Recur over the sub-formulas */ 00568 if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { 00569 result = AbsFormulaSanityCheck(AbsVertexReadLeftKid(vertexPtr), rootTable); 00570 } 00571 00572 if (!result) { 00573 return result; 00574 } 00575 00576 if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t) && 00577 AbsVertexReadType(vertexPtr) != fixedPoint_c) { 00578 result = AbsFormulaSanityCheck(AbsVertexReadRightKid(vertexPtr), rootTable); 00579 } 00580 00581 return result; 00582 } /* End of AbsFormulaSanityCheck */ 00583 00597 boolean 00598 AbsIteratesSanityCheck( 00599 Abs_VerificationInfo_t *absInfo, 00600 AbsVertexInfo_t *vertexPtr) 00601 { 00602 array_t *rings; 00603 mdd_t *element; 00604 mdd_t *previous; 00605 mdd_t *careSet; 00606 boolean result; 00607 int index; 00608 00609 /* Variable initialization */ 00610 careSet = AbsVerificationInfoReadCareSet(absInfo); 00611 result = TRUE; 00612 rings = AbsVertexReadRings(vertexPtr); 00613 element = NIL(mdd_t); 00614 previous = NIL(mdd_t); 00615 00616 arrayForEachItem(mdd_t *, rings, index, element) { 00617 if (previous != NIL(mdd_t)) { 00618 result = result && AbsMddLEqualModCareSet(previous, element, careSet); 00619 if (AbsMddEqualModCareSet(previous, element, careSet) && 00620 index != array_n(rings) - 1) { 00621 result = FALSE; 00622 } 00623 } 00624 previous = element; 00625 } 00626 00627 return result; 00628 } /* End of AbsIteratesSanityCheck */ 00629 00637 void 00638 AbsStatsPrintReport( 00639 FILE *fp, 00640 AbsStats_t *stats) 00641 { 00642 (void) fprintf(fp, "ABS: ------- Statistics Begin Report -------\n"); 00643 (void) fprintf(fp, "ABS: FixedPoint Evaluated %6d times\n", 00644 AbsStatsReadEvalFixedPoint(stats)); 00645 (void) fprintf(fp, "ABS: Refined %6d times\n", 00646 AbsStatsReadRefineFixedPoint(stats)); 00647 (void) fprintf(fp, "ABS: And Evaluated %6d times\n", 00648 AbsStatsReadEvalAnd(stats)); 00649 (void) fprintf(fp, "ABS: Refined %6d times\n", 00650 AbsStatsReadRefineAnd(stats)); 00651 (void) fprintf(fp, "ABS: Not Evaluated %6d times\n", 00652 AbsStatsReadEvalNot(stats)); 00653 (void) fprintf(fp, "ABS: Refined %6d times\n", 00654 AbsStatsReadRefineNot(stats)); 00655 (void) fprintf(fp, "ABS: PreImage Evaluated %6d times\n", 00656 AbsStatsReadEvalPreImage(stats)); 00657 (void) fprintf(fp, "ABS: Refined %6d times\n", 00658 AbsStatsReadRefinePreImage(stats)); 00659 (void) fprintf(fp, "ABS: Identifier Evaluated %6d times\n", 00660 AbsStatsReadEvalIdentifier(stats)); 00661 (void) fprintf(fp, "ABS: Refined %6d times\n", 00662 AbsStatsReadRefineIdentifier(stats)); 00663 (void) fprintf(fp, "ABS: Variable Evaluated %6d times\n", 00664 AbsStatsReadEvalVariable(stats)); 00665 (void) fprintf(fp, "ABS: Refined %6d times\n", 00666 AbsStatsReadRefineVariable(stats)); 00667 (void) fprintf(fp, "ABS: ---------------------------------------\n"); 00668 (void) fprintf(fp, "ABS: Preimage Exact %6d times\n", 00669 AbsStatsReadExactPreImage(stats)); 00670 (void) fprintf(fp, "ABS: Approx. %6d times\n", 00671 AbsStatsReadApproxPreImage(stats)); 00672 (void) fprintf(fp, "ABS: Image Exact %6d times\n", 00673 AbsStatsReadExactImage(stats)); 00674 (void) fprintf(fp, "ABS: ---------------------------------------\n"); 00675 (void) fprintf(fp, "ABS: PreImg CacheEntries %6d entries\n", 00676 AbsStatsReadPreImageCacheEntries(stats)); 00677 (void) fprintf(fp, "ABS: Img CacheEntries %6d entries\n", 00678 AbsStatsReadImageCacheEntries(stats)); 00679 (void) fprintf(fp, "ABS: ---------------------------------------\n"); 00680 (void) fprintf(fp, "ABS: PreImg Cpu Time %7.1f seconds\n", 00681 AbsStatsReadPreImageCpuTime(stats)/1000.0); 00682 (void) fprintf(fp, "ABS: AppPre Cpu Time %7.1f seconds\n", 00683 AbsStatsReadAppPreCpuTime(stats)/1000.0); 00684 (void) fprintf(fp, "ABS: Image Cpu Time %7.1f seconds\n", 00685 AbsStatsReadImageCpuTime(stats)/1000.0); 00686 (void) fprintf(fp, "ABS: ---------------------------------------\n"); 00687 (void) fprintf(fp, "ABS: Reordering Invoked %6d times\n", 00688 AbsStatsReadNumReorderings(stats)); 00689 (void) fprintf(fp, "ABS: ---------------------------------------\n"); 00690 util_print_cpu_stats(vis_stdout); 00691 (void) fprintf(fp, "ABS: ------- Statistics End Report -------\n"); 00692 00693 return; 00694 } /* End of AbsStatsPrintReport */ 00695 00696 00697 /*---------------------------------------------------------------------------*/ 00698 /* Definition of static functions */ 00699 /*---------------------------------------------------------------------------*/ 00700 00710 static void 00711 VertexPrintDotRecur( 00712 FILE *fp, 00713 AbsVertexInfo_t *vertex, 00714 st_table *visited) 00715 { 00716 AbsVertexInfo_t *leftKid; 00717 AbsVertexInfo_t *rightKid; 00718 00719 /* Check the cache */ 00720 if (st_is_member(visited, (char *)vertex)) { 00721 return; 00722 } 00723 00724 /* Recur in the left kid if needed */ 00725 leftKid = AbsVertexReadLeftKid(vertex); 00726 if (leftKid != NIL(AbsVertexInfo_t)) { 00727 VertexPrintDotRecur(fp, AbsVertexReadLeftKid(vertex), visited); 00728 00729 if (AbsVertexReadType(leftKid) != identifier_c) { 00730 (void) fprintf(fp, " \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 00731 VertexTypeToString(vertex), 00732 AbsVertexReadId(vertex), 00733 AbsVertexReadPolarity(vertex)?'+':'-', 00734 VertexTypeToString(leftKid), 00735 AbsVertexReadId(leftKid), 00736 AbsVertexReadPolarity(leftKid)?'+':'-'); 00737 } 00738 else { 00739 (void) fprintf(fp, " \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n", 00740 VertexTypeToString(vertex), 00741 AbsVertexReadId(vertex), 00742 AbsVertexReadPolarity(vertex)?'+':'-', 00743 AbsVertexReadName(leftKid), 00744 AbsVertexReadValue(leftKid), 00745 AbsVertexReadId(leftKid), 00746 AbsVertexReadPolarity(leftKid)?'+':'-'); 00747 } 00748 } 00749 00750 /* Recur in the right kid if needed */ 00751 rightKid = AbsVertexReadRightKid(vertex); 00752 if (rightKid != NIL(AbsVertexInfo_t)) { 00753 VertexPrintDotRecur(fp, AbsVertexReadRightKid(vertex), visited); 00754 00755 if (AbsVertexReadType(rightKid) != identifier_c) { 00756 (void) fprintf(fp, " \"%s(%d)%c\" -> \"%s(%d)%c\";\n", 00757 VertexTypeToString(vertex), 00758 AbsVertexReadId(vertex), 00759 AbsVertexReadPolarity(vertex)?'+':'-', 00760 VertexTypeToString(rightKid), 00761 AbsVertexReadId(rightKid), 00762 AbsVertexReadPolarity(rightKid)?'+':'-'); 00763 } 00764 else { 00765 (void) fprintf(fp, " \"%s(%d)%c\" -> \"%s=%s(%d)%c\"\n", 00766 VertexTypeToString(vertex), 00767 AbsVertexReadId(vertex), 00768 AbsVertexReadPolarity(vertex)?'+':'-', 00769 AbsVertexReadName(rightKid), 00770 AbsVertexReadValue(rightKid), 00771 AbsVertexReadId(rightKid), 00772 AbsVertexReadPolarity(rightKid)?'+':'-'); 00773 } 00774 } 00775 00776 st_insert(visited, (char *)vertex, NIL(char)); 00777 00778 return; 00779 } /* End of VertexPrintDotRecur */ 00780 00788 static char * 00789 VertexTypeToString( 00790 AbsVertexInfo_t *vertex) 00791 { 00792 char *typeStr; 00793 00794 switch (AbsVertexReadType(vertex)) { 00795 case fixedPoint_c: 00796 typeStr = "LFP"; 00797 break; 00798 case and_c: 00799 typeStr = "AND"; 00800 break; 00801 case xor_c: 00802 typeStr = "XOR"; 00803 break; 00804 case xnor_c: 00805 typeStr = "XNOR"; 00806 break; 00807 case not_c: 00808 typeStr = "NOT"; 00809 break; 00810 case preImage_c: 00811 typeStr = "Pre"; 00812 break; 00813 case identifier_c: 00814 typeStr = "Id"; 00815 break; 00816 case variable_c: 00817 typeStr = "VAR"; 00818 break; 00819 case false_c: 00820 typeStr = "FALSE"; 00821 break; 00822 default: 00823 fail("Unknown vertex type."); 00824 break; 00825 } 00826 00827 return typeStr; 00828 } /* End of VertexTypeToString */ 00829