/**CFile*********************************************************************** FileName [absCatalog.c] PackageName [abs] Synopsis [Functions to handle a catalog of sub-formulas to detect common sub-expressions] Author [Abelardo Pardo ] 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 "absInt.h" static char rcsid[] UNUSED = "$Id: absCatalog.c,v 1.8 2005/04/16 04:22:21 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [A struct to keep list of subformulas to detect common subexpressions] SeeAlso [AbsVerificationInfo] ******************************************************************************/ struct AbsVertexCatalog { lsList fixedPoints; lsList booleanOps; lsList negations; lsList preImages; lsList identifiers; lsList variables; }; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Macro to read the fixedPoints field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadFixedPoints(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->fixedPoints) /**Macro*********************************************************************** Synopsis [Macro to read the booleanOps field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadBooleanOps(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->booleanOps) /**Macro*********************************************************************** Synopsis [Macro to read the negations field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadNegations(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->negations) /**Macro*********************************************************************** Synopsis [Macro to read the preImages field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadPreImages(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->preImages) /**Macro*********************************************************************** Synopsis [Macro to read the identifiers field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadIdentifiers(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->identifiers) /**Macro*********************************************************************** Synopsis [Macro to read the variables field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogReadVariables(\ /* AbsVertexCatalog_t * */ cPtr \ ) \ (cPtr->variables) /**Macro*********************************************************************** Synopsis [Macro to set the fixedPoints field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogSetFixedPoints(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->fixedPoints) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the booleanOps field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogSetBooleanOps(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->booleanOps) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the negations field from a AbsVertexCatalog_t structure] SideEffects [AbsVertexCatalog] SeeAlso [] ******************************************************************************/ #define AbsVertexCatalogSetNegations(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->negations) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the preImages field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogSetPreImages(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->preImages) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the identifiers field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogSetIdentifiers(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->identifiers) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the variables field from a AbsVertexCatalog_t structure] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ #define AbsVertexCatalogSetVariables(\ /* AbsVertexCatalog_t * */ cPtr, \ /* lsList */ data \ ) \ (cPtr->variables) = (data) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static AbsVertexInfo_t * LookUpBooleanOp(lsList vertexList, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid); static AbsVertexInfo_t * LookUpFixedPoint(lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid, int localId); static AbsVertexInfo_t * LookUpIdentifier(lsList vertexList, boolean polarity, char *name, char *value); static AbsVertexInfo_t * LookUpPreImage(lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid); static AbsVertexInfo_t * LookUpVariable(lsList vertexList, boolean polarity, int localId); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Allocate the structure to store the catalog of vertices] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ AbsVertexCatalog_t * AbsVertexCatalogInitialize(void) { AbsVertexCatalog_t *result; result = ALLOC(AbsVertexCatalog_t, 1); AbsVertexCatalogSetFixedPoints(result, lsCreate()); AbsVertexCatalogSetBooleanOps(result, lsCreate()); AbsVertexCatalogSetNegations(result, lsCreate()); AbsVertexCatalogSetPreImages(result, lsCreate()); AbsVertexCatalogSetIdentifiers(result, lsCreate()); AbsVertexCatalogSetVariables(result, lsCreate()); return result; } /* End of AbsVertexCatalogInitialize */ /**Function******************************************************************** Synopsis [Deallocate the structure storing the catalog vertices] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ void AbsVertexCatalogFree( AbsVertexCatalog_t *c) { lsDestroy(AbsVertexCatalogReadFixedPoints(c), (void (*)(lsGeneric))0); lsDestroy(AbsVertexCatalogReadBooleanOps(c), (void (*)(lsGeneric))0); lsDestroy(AbsVertexCatalogReadNegations(c), (void (*)(lsGeneric))0); lsDestroy(AbsVertexCatalogReadPreImages(c), (void (*)(lsGeneric))0); lsDestroy(AbsVertexCatalogReadIdentifiers(c), (void (*)(lsGeneric))0); lsDestroy(AbsVertexCatalogReadVariables(c), (void (*)(lsGeneric))0); FREE(c); return; } /* End of AbsVertexCatalogFree */ /**Function******************************************************************** Synopsis [Find or create the vertex with the given sub-formula in the vertex catalog] SideEffects [] SeeAlso [AbsVertexCatalog] ******************************************************************************/ AbsVertexInfo_t * AbsVertexCatalogFindOrAdd( AbsVertexCatalog_t *catalog, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid, int localId, char *idName, char *idValue ) { if (type == fixedPoint_c) { return LookUpFixedPoint(AbsVertexCatalogReadFixedPoints(catalog), polarity, leftKid, localId); } if (type == and_c || type == xor_c || type == xnor_c) { return LookUpBooleanOp(AbsVertexCatalogReadBooleanOps(catalog), type, polarity, leftKid, rightKid); } if (type == not_c) { return LookUpPreImage(AbsVertexCatalogReadNegations(catalog), polarity, leftKid); } if (type == preImage_c) { return LookUpPreImage(AbsVertexCatalogReadPreImages(catalog), polarity, leftKid); } if (type == identifier_c) { return LookUpIdentifier(AbsVertexCatalogReadIdentifiers(catalog), polarity, idName, idValue); } if (type == variable_c) { return LookUpVariable(AbsVertexCatalogReadVariables(catalog), polarity, localId); } (void) fprintf(vis_stderr, "** abs error: Unknown vertex type in function "); (void) fprintf(vis_stderr, "AbsVertexCatalogFindOrAdd.\n"); return NIL(AbsVertexInfo_t); } /* End of AbsVertexCatalogFindOrAdd */ /**Function******************************************************************** Synopsis [Delete a vertex from the catalog] SideEffects [] SeeAlso [AbsVertexFree] ******************************************************************************/ void AbsCatalogDelete( AbsVertexCatalog_t *catalog, AbsVertexInfo_t *vertex) { AbsVertex_t type; AbsVertexInfo_t *result; lsList vertexList; lsGen listGen; lsHandle item; lsGeneric userData; vertexList = 0; type = AbsVertexReadType(vertex); /* Select the proper list from the catalog */ if (type == fixedPoint_c) { vertexList = AbsVertexCatalogReadFixedPoints(catalog); } if (type == and_c || type == xor_c || type == xnor_c) { vertexList = AbsVertexCatalogReadBooleanOps(catalog); } if (type == not_c) { vertexList = AbsVertexCatalogReadNegations(catalog); } if (type == preImage_c) { vertexList = AbsVertexCatalogReadPreImages(catalog); } if (type == identifier_c) { vertexList = AbsVertexCatalogReadIdentifiers(catalog); } if (type == variable_c) { vertexList = AbsVertexCatalogReadVariables(catalog); } listGen = lsStart(vertexList); while(lsNext(listGen, &result, &item) == LS_OK) { if (result == vertex) { lsRemoveItem(item, &userData); assert(vertex == (AbsVertexInfo_t *)userData); lsFinish(listGen); return; } } (void) fprintf(vis_stderr, "** abs error: Removing non-existent vertex from"); (void) fprintf(vis_stderr, " catalog\n"); return; } /* End of AbsCatalogDelete */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Find or add a vertex to the list of boolean ops] SideEffects [] SeeAlso [AbsVertexCatalogFindOrAdd] ******************************************************************************/ static AbsVertexInfo_t * LookUpBooleanOp( lsList vertexList, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid) { lsGen listGen; AbsVertexInfo_t *result; /* Start the generator and traverse the list */ listGen = lsStart(vertexList); while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) { if (AbsVertexReadType(result) == type && AbsVertexReadLeftKid(result) == leftKid && AbsVertexReadRightKid(result) == rightKid && AbsVertexReadPolarity(result) == polarity) { AbsVertexReadRefs(result)++; lsFinish(listGen); return result; } } /* Item has not been found */ lsFinish(listGen); result = AbsVertexInitialize(); lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle)); return result; } /* End of LookUpBooleanOp */ /**Function******************************************************************** Synopsis [Find or add a vertex to the list of fixedpoints] SideEffects [] SeeAlso [AbsVertexCatalogFindOrAdd] ******************************************************************************/ static AbsVertexInfo_t * LookUpFixedPoint( lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid, int localId) { lsGen listGen; AbsVertexInfo_t *result; /* Start the generator and traverse the list */ listGen = lsStart(vertexList); while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) { if (AbsVertexReadLeftKid(result) == leftKid && AbsVertexReadPolarity(result) == polarity && AbsVertexReadVarId(AbsVertexReadFpVar(result)) == localId) { AbsVertexReadRefs(result)++; lsFinish(listGen); return result; } } /* Item has not been found */ lsFinish(listGen); result = AbsVertexInitialize(); lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle)); return result; } /* End of LookUpFixedPoint */ /**Function******************************************************************** Synopsis [Find or add a vertex to the list of identifiers] SideEffects [] SeeAlso [AbsVertexCatalogFindOrAdd] ******************************************************************************/ static AbsVertexInfo_t * LookUpIdentifier( lsList vertexList, boolean polarity, char *name, char *value) { lsGen listGen; AbsVertexInfo_t *result; /* Start the generator and traverse the list */ listGen = lsStart(vertexList); while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) { if (AbsVertexReadPolarity(result) == polarity && strcmp(AbsVertexReadName(result), name) == 0 && strcmp(AbsVertexReadValue(result), value) == 0) { AbsVertexReadRefs(result)++; lsFinish(listGen); return result; } } /* Item has not been found */ lsFinish(listGen); result = AbsVertexInitialize(); lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle)); return result; } /* End of LookUpIdentifier */ /**Function******************************************************************** Synopsis [Find or add a vertex to the list of preimages] SideEffects [] SeeAlso [AbsVertexCatalogFindOrAdd] ******************************************************************************/ static AbsVertexInfo_t * LookUpPreImage( lsList vertexList, boolean polarity, AbsVertexInfo_t *leftKid) { lsGen listGen; AbsVertexInfo_t *result; /* Start the generator and traverse the list */ listGen = lsStart(vertexList); while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) { if (AbsVertexReadLeftKid(result) == leftKid && AbsVertexReadPolarity(result) == polarity) { AbsVertexReadRefs(result)++; lsFinish(listGen); return result; } } /* Item has not been found */ lsFinish(listGen); result = AbsVertexInitialize(); lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle)); return result; } /* End of LookUpPreImage */ /**Function******************************************************************** Synopsis [Find or add a vertex to the list of variables] SideEffects [] SeeAlso [AbsVertexCatalogFindOrAdd] ******************************************************************************/ static AbsVertexInfo_t * LookUpVariable( lsList vertexList, boolean polarity, int localId) { lsGen listGen; AbsVertexInfo_t *result; /* Start the generator and traverse the list */ listGen = lsStart(vertexList); while(lsNext(listGen, &result, NIL(lsHandle)) == LS_OK) { if (AbsVertexReadPolarity(result) == polarity && AbsVertexReadVarId(result) == localId) { AbsVertexReadRefs(result)++; lsFinish(listGen); return result; } } /* Item has not been found */ lsFinish(listGen); result = AbsVertexInitialize(); lsNewBegin(vertexList, (lsGeneric)result, NIL(lsHandle)); return result; } /* End of LookUpVariable */