#include <time.h>#include "absInt.h"
Include dependency graph for absUtil.c:
Go to the source code of this file.
Functions | |
| static void | VertexPrintDotRecur (FILE *fp, AbsVertexInfo_t *vertex, st_table *visited) |
| static char * | VertexTypeToString (AbsVertexInfo_t *vertex) |
| void | AbsVertexPrintDot (FILE *fp, array_t *vertexArray) |
| void | AbsVertexPrint (AbsVertexInfo_t *vertexPtr, st_table *visitedSF, boolean recur, long verbosity) |
| void | AbsBddPrintMinterms (mdd_t *function) |
| void | AbsFormulaSetConstantBit (AbsVertexInfo_t *vertexPtr) |
| boolean | AbsFormulaSanityCheck (AbsVertexInfo_t *vertexPtr, st_table *rootTable) |
| boolean | AbsIteratesSanityCheck (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| void | AbsStatsPrintReport (FILE *fp, AbsStats_t *stats) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: absUtil.c,v 1.17 2005/04/16 04:22:21 fabio Exp $" |
Function Documentation
| void AbsBddPrintMinterms | ( | mdd_t * | function | ) |
Function********************************************************************
Synopsis [Function to print the cubes of a BDD.]
SideEffects []
Definition at line 357 of file absUtil.c.
{
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 */
Here is the caller graph for this function:
| boolean AbsFormulaSanityCheck | ( | AbsVertexInfo_t * | vertexPtr, |
| st_table * | rootTable | ||
| ) |
Function********************************************************************
Synopsis [Standard tests to check if the graph represenging a formula is correctly built]
SideEffects []
SeeAlso [AbsVertexInfo]
Definition at line 457 of file absUtil.c.
{
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 */
Here is the caller graph for this function:
| void AbsFormulaSetConstantBit | ( | AbsVertexInfo_t * | vertexPtr | ) |
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]
Definition at line 410 of file absUtil.c.
{
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 */
Here is the caller graph for this function:
| boolean AbsIteratesSanityCheck | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) |
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 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 []
Definition at line 598 of file absUtil.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsStatsPrintReport | ( | FILE * | fp, |
| AbsStats_t * | stats | ||
| ) |
Function********************************************************************
Synopsis [Print the statistics report]
SideEffects []
Definition at line 638 of file absUtil.c.
{
(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 */
Here is the caller graph for this function:
| void AbsVertexPrint | ( | AbsVertexInfo_t * | vertexPtr, |
| st_table * | visitedSF, | ||
| boolean | recur, | ||
| long | verbosity | ||
| ) |
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]
Definition at line 119 of file absUtil.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsVertexPrintDot | ( | FILE * | fp, |
| array_t * | vertexArray | ||
| ) |
AutomaticEnd 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 http://www.research.att.com/orgs/ssr/book/reuse.]
SideEffects []
SeeAlso [AbsVertexInfo]
Definition at line 65 of file absUtil.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void VertexPrintDotRecur | ( | FILE * | fp, |
| AbsVertexInfo_t * | vertex, | ||
| st_table * | visited | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Prints the vertex content in DOT format.]
SideEffects []
SeeAlso [AbsVertexPrintDot]
Definition at line 711 of file absUtil.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| static char * VertexTypeToString | ( | AbsVertexInfo_t * | vertex | ) | [static] |
Function********************************************************************
Synopsis [Returns the string representing a vertex type.]
SideEffects []
Definition at line 789 of file absUtil.c.
{
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 */
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: absUtil.c,v 1.17 2005/04/16 04:22:21 fabio Exp $" [static] |
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.]
