00001
00021 #ifndef __RES_INT_H__
00022 #define __RES_INT_H__
00023
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif
00027
00031
00032 #include "res.h"
00033
00037
00041
00042 typedef struct Res_Win_t_ Res_Win_t;
00043 struct Res_Win_t_
00044 {
00045
00046 Abc_Obj_t * pNode;
00047 int nWinTfiMax;
00048 int nWinTfoMax;
00049 int nLevDivMax;
00050
00051 int nFanoutLimit;
00052 int nLevTfiMinus;
00053
00054 int nLevLeafMin;
00055 int nLevTravMin;
00056 int nDivsPlus;
00057
00058 Vec_Ptr_t * vRoots;
00059 Vec_Ptr_t * vLeaves;
00060 Vec_Ptr_t * vBranches;
00061 Vec_Ptr_t * vNodes;
00062 Vec_Ptr_t * vDivs;
00063
00064 Vec_Vec_t * vMatrix;
00065 };
00066
00067 typedef struct Res_Sim_t_ Res_Sim_t;
00068 struct Res_Sim_t_
00069 {
00070 Abc_Ntk_t * pAig;
00071 int nTruePis;
00072 int fConst0;
00073 int fConst1;
00074
00075 int nWords;
00076 int nPats;
00077 int nWordsIn;
00078 int nPatsIn;
00079 int nBytesIn;
00080 int nWordsOut;
00081 int nPatsOut;
00082
00083 Vec_Ptr_t * vPats;
00084 Vec_Ptr_t * vPats0;
00085 Vec_Ptr_t * vPats1;
00086 Vec_Ptr_t * vOuts;
00087 int nPats0;
00088 int nPats1;
00089
00090 Vec_Vec_t * vCands;
00091
00092 int timeSat;
00093 };
00094
00098
00102
00103
00104 extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
00105 extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
00106 extern int Res_WinVisitMffc( Abc_Obj_t * pNode );
00107
00108 extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea );
00109 extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax );
00110
00111 extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
00112 extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
00113
00114 extern Res_Sim_t * Res_SimAlloc( int nWords );
00115 extern void Res_SimFree( Res_Sim_t * p );
00116 extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
00117
00118 extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
00119
00120 extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
00121
00122 extern Res_Win_t * Res_WinAlloc();
00123 extern void Res_WinFree( Res_Win_t * p );
00124 extern int Res_WinIsTrivial( Res_Win_t * p );
00125 extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
00126
00127
00128 #ifdef __cplusplus
00129 }
00130 #endif
00131
00132 #endif
00133
00137