00001 00021 #ifndef __RWT_H__ 00022 #define __RWT_H__ 00023 00024 #ifdef __cplusplus 00025 extern "C" { 00026 #endif 00027 00031 00032 #include "mem.h" 00033 #include "extra.h" 00034 #include "vec.h" 00035 00039 00043 00044 #define RWT_LIMIT 1048576/4 // ((1 << 20) 00045 #define RWT_MIN(a,b) (((a) < (b))? (a) : (b)) 00046 #define RWT_MAX(a,b) (((a) > (b))? (a) : (b)) 00047 00048 typedef struct Rwt_Man_t_ Rwt_Man_t; 00049 typedef struct Rwt_Node_t_ Rwt_Node_t; 00050 00051 struct Rwt_Man_t_ 00052 { 00053 // internal lookups 00054 int nFuncs; // number of four var functions 00055 unsigned short * puCanons; // canonical forms 00056 char * pPhases; // canonical phases 00057 char * pPerms; // canonical permutations 00058 unsigned char * pMap; // mapping of functions into class numbers 00059 unsigned short * pMapInv; // mapping of classes into functions 00060 char * pPractical; // practical NPN classes 00061 char ** pPerms4; // four-var permutations 00062 // node space 00063 Vec_Ptr_t * vForest; // all the nodes 00064 Rwt_Node_t ** pTable; // the hash table of nodes by their canonical form 00065 Vec_Vec_t * vClasses; // the nodes of the equivalence classes 00066 Mem_Fixed_t * pMmNode; // memory for nodes and cuts 00067 // statistical variables 00068 int nTravIds; // the counter of traversal IDs 00069 int nConsidered; // the number of nodes considered 00070 int nAdded; // the number of nodes added to lists 00071 int nClasses; // the number of NN classes 00072 // the result of resynthesis 00073 int fCompl; // indicates if the output of FF should be complemented 00074 void * pCut; // the decomposition tree (temporary) 00075 void * pGraph; // the decomposition tree (temporary) 00076 char * pPerm; // permutation used for the best cut 00077 Vec_Ptr_t * vFanins; // the fanins array (temporary) 00078 Vec_Ptr_t * vFaninsCur; // the fanins array (temporary) 00079 Vec_Int_t * vLevNums; // the array of levels (temporary) 00080 Vec_Ptr_t * vNodesTemp; // the nodes in MFFC (temporary) 00081 // node statistics 00082 int nNodesConsidered; 00083 int nNodesRewritten; 00084 int nNodesGained; 00085 int nScores[222]; 00086 int nCutsGood; 00087 int nCutsBad; 00088 int nSubgraphs; 00089 // runtime statistics 00090 int timeStart; 00091 int timeTruth; 00092 int timeCut; 00093 int timeRes; 00094 int timeEval; 00095 int timeMffc; 00096 int timeUpdate; 00097 int timeTotal; 00098 }; 00099 00100 struct Rwt_Node_t_ // 24 bytes 00101 { 00102 int Id; // ID 00103 int TravId; // traversal ID 00104 unsigned uTruth : 16; // truth table 00105 unsigned Volume : 8; // volume 00106 unsigned Level : 6; // level 00107 unsigned fUsed : 1; // mark 00108 unsigned fExor : 1; // mark 00109 Rwt_Node_t * p0; // first child 00110 Rwt_Node_t * p1; // second child 00111 Rwt_Node_t * pNext; // next in the table 00112 }; 00113 00114 // manipulation of complemented attributes 00115 static inline int Rwt_IsComplement( Rwt_Node_t * p ) { return (int)(((unsigned long)p) & 01); } 00116 static inline Rwt_Node_t * Rwt_Regular( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) & ~01); } 00117 static inline Rwt_Node_t * Rwt_Not( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) ^ 01); } 00118 static inline Rwt_Node_t * Rwt_NotCond( Rwt_Node_t * p, int c ) { return (Rwt_Node_t *)((unsigned long)(p) ^ (c)); } 00119 00123 00127 00128 /*=== rwrDec.c ========================================================*/ 00129 extern void Rwt_ManPreprocess( Rwt_Man_t * p ); 00130 /*=== rwrMan.c ========================================================*/ 00131 extern Rwt_Man_t * Rwt_ManStart( int fPrecompute ); 00132 extern void Rwt_ManStop( Rwt_Man_t * p ); 00133 extern void Rwt_ManPrintStats( Rwt_Man_t * p ); 00134 extern void Rwt_ManPrintStatsFile( Rwt_Man_t * p ); 00135 extern void * Rwt_ManReadDecs( Rwt_Man_t * p ); 00136 extern Vec_Ptr_t * Rwt_ManReadLeaves( Rwt_Man_t * p ); 00137 extern int Rwt_ManReadCompl( Rwt_Man_t * p ); 00138 extern void Rwt_ManAddTimeCuts( Rwt_Man_t * p, int Time ); 00139 extern void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, int Time ); 00140 extern void Rwt_ManAddTimeTotal( Rwt_Man_t * p, int Time ); 00141 /*=== rwrUtil.c ========================================================*/ 00142 extern void Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose ); 00143 extern char * Rwt_ManGetPractical( Rwt_Man_t * p ); 00144 extern Rwt_Node_t * Rwt_ManAddVar( Rwt_Man_t * p, unsigned uTruth, int fPrecompute ); 00145 extern void Rwt_ManIncTravId( Rwt_Man_t * p ); 00146 00147 #ifdef __cplusplus 00148 } 00149 #endif 00150 00151 #endif 00152 00156