00001 00019 #ifndef __DSD_INT_H__ 00020 #define __DSD_INT_H__ 00021 00022 #include "extra.h" 00023 #include "dsd.h" 00024 00028 00029 typedef unsigned char byte; 00030 00034 00035 // DSD manager 00036 struct Dsd_Manager_t_ 00037 { 00038 DdManager * dd; // the BDD manager 00039 st_table * Table; // the mapping of BDDs into their DEs 00040 int nInputs; // the number of primary inputs 00041 int nRoots; // the number of primary outputs 00042 int nRootsAlloc;// the number of primary outputs 00043 Dsd_Node_t ** pInputs; // the primary input nodes 00044 Dsd_Node_t ** pRoots; // the primary output nodes 00045 Dsd_Node_t * pConst1; // the constant node 00046 int fVerbose; // the verbosity level 00047 }; 00048 00049 // DSD node 00050 struct Dsd_Node_t_ 00051 { 00052 Dsd_Type_t Type; // decomposition type 00053 DdNode * G; // function of the node 00054 DdNode * S; // support of this function 00055 Dsd_Node_t ** pDecs; // pointer to structures for formal inputs 00056 int Mark; // the mark used by CASE 4 of disjoint decomposition 00057 short nDecs; // the number of formal inputs 00058 short nVisits; // the counter of visits 00059 }; 00060 00064 00065 #define MAXINPUTS 1000 00066 00070 00074 00075 /*=== dsdCheck.c =======================================================*/ 00076 extern void Dsd_CheckCacheAllocate( int nEntries ); 00077 extern void Dsd_CheckCacheDeallocate(); 00078 extern void Dsd_CheckCacheClear(); 00079 extern int Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ); 00080 /*=== dsdTree.c =======================================================*/ 00081 extern Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum ); 00082 extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ); 00083 extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan ); 00084 extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ); 00085 00086 #endif 00087 00091