MACRO DEFINITIONS ///.
222 int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
230 if ( nFaninsMax > 8 )
239 fprintf( stdout,
"Converting to BDD has failed.\n" );
259 if ( pObj->
Id > nNodesOld )
264 RetValue =
Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
270 if ( p->pPars->fVeryVerbose )
272 printf(
"%5d (lev=%2d) : ", pObj->
Id, pObj->
Level );
273 printf(
"Win = %3d/%3d/%4d/%3d ",
289 if ( p->pPars->fVeryVerbose )
292 printf(
"D+ = %3d ", p->pWin->nDivsPlus );
301 if ( p->pPars->fVeryVerbose )
318 if ( p->pSim->fConst0 || p->pSim->fConst1 )
333 if ( p->pPars->fArea )
334 RetValue =
Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
336 RetValue =
Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
338 p->nCandSets += RetValue;
356 if ( p->pCnf == NULL )
401 p->timeSatSim += p->pSim->timeSat;
402 p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
415 fprintf( stdout,
"Abc_NtkResynthesize(): Network check has failed.\n" );
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
int Int_ManInterpolate(Int_Man_t *p, Sto_Man_t *pCnf, int fVerbose, unsigned **ppResult)
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
static Hop_Obj_t * Hop_ManConst1(Hop_Man_t *p)
int Res_WinIsTrivial(Res_Win_t *p)
void Res_WinDivisors(Res_Win_t *p, int nLevDivMax)
FUNCTION DEFINITIONS ///.
Abc_Ntk_t * Res_WndStrash(Res_Win_t *p)
FUNCTION DEFINITIONS ///.
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
void Res_ManFree(Res_Man_t *p)
int Res_WinCompute(Abc_Obj_t *pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t *p)
int Res_SimPrepare(Res_Sim_t *p, Abc_Ntk_t *pAig, int nTruePis, int fVerbose)
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
static abctime Abc_Clock()
static int Vec_PtrSize(Vec_Ptr_t *p)
ABC_DLL int Abc_NtkGetTotalFanins(Abc_Ntk_t *pNtk)
Res_Man_t * Res_ManAlloc(Res_Par_t *pPars)
FUNCTION DEFINITIONS ///.
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Hop_Obj_t * Kit_GraphToHop(Hop_Man_t *pMan, Kit_Graph_t *pGraph)
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
ABC_DLL int Abc_ObjRequiredLevel(Abc_Obj_t *pObj)
void Kit_GraphFree(Kit_Graph_t *pGraph)
void Res_UpdateNetwork(Abc_Obj_t *pObj, Vec_Ptr_t *vFanins, Hop_Obj_t *pFunc, Vec_Vec_t *vLevels)
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
typedefABC_NAMESPACE_IMPL_START struct Res_Man_t_ Res_Man_t
DECLARATIONS ///.
void * Res_SatProveUnsat(Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
FUNCTION DEFINITIONS ///.
void Sto_ManFree(Sto_Man_t *p)
ABC_DLL int Abc_NtkSweep(Abc_Ntk_t *pNtk, int fVerbose)
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)
FUNCTION DEFINITIONS ///.
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
static void Vec_PtrClear(Vec_Ptr_t *p)
static int Abc_NtkHasAig(Abc_Ntk_t *pNtk)
static Hop_Obj_t * Hop_ManConst0(Hop_Man_t *p)
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.