abc70930: src/opt/rwr/rwr.h Source File

00001 
00021 #ifndef __RWR_H__
00022 #define __RWR_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif
00027 
00031 
00032 #include "abc.h"
00033 #include "cut.h"
00034 
00038 
00042  
00043 #define RWR_LIMIT  1048576/4  // ((1 << 20) 
00044 
00045 typedef struct Rwr_Man_t_   Rwr_Man_t;
00046 typedef struct Rwr_Node_t_  Rwr_Node_t;
00047 
00048 struct Rwr_Man_t_
00049 {
00050     // internal lookups
00051     int                nFuncs;           // number of four var functions
00052     unsigned short *   puCanons;         // canonical forms
00053     char *             pPhases;          // canonical phases
00054     char *             pPerms;           // canonical permutations
00055     unsigned char *    pMap;             // mapping of functions into class numbers
00056     unsigned short *   pMapInv;          // mapping of classes into functions
00057     char *             pPractical;       // practical NPN classes
00058     char **            pPerms4;          // four-var permutations
00059     // node space
00060     Vec_Ptr_t *        vForest;          // all the nodes
00061     Rwr_Node_t **      pTable;           // the hash table of nodes by their canonical form
00062     Vec_Vec_t *        vClasses;         // the nodes of the equivalence classes
00063     Extra_MmFixed_t *  pMmNode;          // memory for nodes and cuts
00064     // statistical variables
00065     int                nTravIds;         // the counter of traversal IDs
00066     int                nConsidered;      // the number of nodes considered
00067     int                nAdded;           // the number of nodes added to lists
00068     int                nClasses;         // the number of NN classes
00069     // the result of resynthesis
00070     int                fCompl;           // indicates if the output of FF should be complemented
00071     void *             pGraph;           // the decomposition tree (temporary)
00072     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
00073     Vec_Ptr_t *        vFaninsCur;       // the fanins array (temporary)
00074     Vec_Int_t *        vLevNums;         // the array of levels (temporary)
00075     Vec_Ptr_t *        vNodesTemp;       // the nodes in MFFC (temporary)
00076     // node statistics
00077     int                nNodesConsidered;
00078     int                nNodesRewritten;
00079     int                nNodesGained;
00080     int                nNodesBeg;
00081     int                nNodesEnd;
00082     int                nScores[222];
00083     int                nCutsGood;
00084     int                nCutsBad;
00085     int                nSubgraphs;
00086     // runtime statistics
00087     int                timeStart;
00088     int                timeCut;
00089     int                timeRes;
00090     int                timeEval;
00091     int                timeMffc;
00092     int                timeUpdate;
00093     int                timeTotal;
00094 };
00095 
00096 struct Rwr_Node_t_ // 24 bytes
00097 {
00098     int                Id;               // ID 
00099     int                TravId;           // traversal ID
00100     short              nScore;
00101     short              nGain;
00102     short              nAdded;
00103     unsigned           uTruth : 16;      // truth table
00104     unsigned           Volume :  8;      // volume
00105     unsigned           Level  :  6;      // level
00106     unsigned           fUsed  :  1;      // mark
00107     unsigned           fExor  :  1;      // mark
00108     Rwr_Node_t *       p0;               // first child
00109     Rwr_Node_t *       p1;               // second child
00110     Rwr_Node_t *       pNext;            // next in the table
00111 };
00112 
00113 // manipulation of complemented attributes
00114 static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned long)p) & 01);           }
00115 static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned long)(p) & ~01);  }
00116 static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned long)(p) ^  01);  }
00117 static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned long)(p) ^ (c));  }
00118 
00122 
00126 
00127 /*=== rwrDec.c ========================================================*/
00128 extern void              Rwr_ManPreprocess( Rwr_Man_t * p );
00129 /*=== rwrEva.c ========================================================*/
00130 extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable );
00131 extern void              Rwr_ScoresClean( Rwr_Man_t * p );
00132 extern void              Rwr_ScoresReport( Rwr_Man_t * p );
00133 /*=== rwrLib.c ========================================================*/
00134 extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
00135 extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
00136 extern Rwr_Node_t *      Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
00137 extern int               Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 );
00138 extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
00139 /*=== rwrMan.c ========================================================*/
00140 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
00141 extern void              Rwr_ManStop( Rwr_Man_t * p );
00142 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
00143 extern void              Rwr_ManPrintStatsFile( Rwr_Man_t * p );
00144 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
00145 extern Vec_Ptr_t *       Rwr_ManReadLeaves( Rwr_Man_t * p );
00146 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
00147 extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
00148 extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );
00149 extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
00150 /*=== rwrPrint.c ========================================================*/
00151 extern void              Rwr_ManPrint( Rwr_Man_t * p );
00152 /*=== rwrUtil.c ========================================================*/
00153 extern void              Rwr_ManWriteToArray( Rwr_Man_t * p );
00154 extern void              Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose );
00155 extern void              Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName );
00156 extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
00157 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
00158 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
00159 
00160 #ifdef __cplusplus
00161 }
00162 #endif
00163 
00164 #endif
00165 
00169