00001
00021 #ifndef __DAR_INT_H__
00022 #define __DAR_INT_H__
00023
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif
00027
00031
00032 #include <stdio.h>
00033 #include <stdlib.h>
00034 #include <string.h>
00035 #include <assert.h>
00036 #include <time.h>
00037
00038
00039 #include "vec.h"
00040 #include "aig.h"
00041 #include "dar.h"
00042
00046
00050
00051 typedef struct Dar_Man_t_ Dar_Man_t;
00052 typedef struct Dar_Cut_t_ Dar_Cut_t;
00053
00054
00055 struct Dar_Cut_t_
00056 {
00057 unsigned uSign;
00058 unsigned uTruth : 16;
00059 unsigned Value : 11;
00060 unsigned fBest : 1;
00061 unsigned fUsed : 1;
00062 unsigned nLeaves : 3;
00063 int pLeaves[4];
00064 };
00065
00066
00067 struct Dar_Man_t_
00068 {
00069
00070 Dar_RwrPar_t * pPars;
00071 Aig_Man_t * pAig;
00072
00073 Aig_MmFixed_t * pMemCuts;
00074 void * pManCnf;
00075
00076 Vec_Ptr_t * vLeavesBest;
00077 int OutBest;
00078 int OutNumBest;
00079 int GainBest;
00080 int LevelBest;
00081 int ClassBest;
00082
00083 int nTotalSubgs;
00084 int ClassTimes[222];
00085 int ClassGains[222];
00086 int ClassSubgs[222];
00087 int nCutMemUsed;
00088
00089 int nNodesInit;
00090 int nNodesTried;
00091 int nCutsAll;
00092 int nCutsTried;
00093 int nCutsUsed;
00094 int nCutsBad;
00095 int nCutsGood;
00096 int nCutsSkipped;
00097
00098 int timeCuts;
00099 int timeEval;
00100 int timeOther;
00101 int timeTotal;
00102 int time1;
00103 int time2;
00104 };
00105
00106 static inline Dar_Cut_t * Dar_ObjCuts( Aig_Obj_t * pObj ) { return pObj->pData; }
00107 static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts; }
00108
00112
00116
00117
00118 #define Dar_ObjForEachCutAll( pObj, pCut, i ) \
00119 for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )
00120 #define Dar_ObjForEachCut( pObj, pCut, i ) \
00121 for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else
00122
00123 #define Dar_CutForEachLeaf( p, pCut, pLeaf, i ) \
00124 for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )
00125
00129
00130
00131
00132
00133 extern void Dar_ManCutsStart( Dar_Man_t * p );
00134 extern void Dar_ManCutsFree( Dar_Man_t * p );
00135 extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
00136 extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
00137
00138 extern Vec_Int_t * Dar_LibReadNodes();
00139 extern Vec_Int_t * Dar_LibReadOuts();
00140 extern Vec_Int_t * Dar_LibReadPrios();
00141
00142 extern void Dar_LibStart();
00143 extern void Dar_LibStop();
00144 extern void Dar_LibPrepare( int nSubgraphs );
00145 extern void Dar_LibReturnCanonicals( unsigned * pCanons );
00146 extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
00147 extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
00148
00149 extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
00150 extern void Dar_ManStop( Dar_Man_t * p );
00151 extern void Dar_ManPrintStats( Dar_Man_t * p );
00152
00153 extern char ** Dar_Permutations( int n );
00154 extern void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
00155
00156 #ifdef __cplusplus
00157 }
00158 #endif
00159
00160 #endif
00161
00165