diff options
Diffstat (limited to 'src/opt/mfs')
-rw-r--r-- | src/opt/mfs/mfs.h | 8 | ||||
-rw-r--r-- | src/opt/mfs/mfsCore.c | 28 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 10 | ||||
-rw-r--r-- | src/opt/mfs/mfsInter.c | 4 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 18 | ||||
-rw-r--r-- | src/opt/mfs/mfsResub.c | 17 | ||||
-rw-r--r-- | src/opt/mfs/mfsSat.c | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsStrash.c | 8 |
8 files changed, 44 insertions, 51 deletions
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index bddb9328..375f93b7 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -21,10 +21,6 @@ #ifndef __MFS_H__ #define __MFS_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +29,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index e8820acd..456b5d71 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -63,16 +63,15 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars ) int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Abc_Obj_t * pFanin; - float * pProbab = (float *)p->vProbs->pArray; int i; // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) { - if ( pProbab[pFanin->Id] >= 0.4 ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.4 ) { if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) return 1; - } else if ( pProbab[pFanin->Id] >= 0.3 ) + } else if ( Abc_MfsObjProb(p, pFanin) >= 0.3 ) { if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) return 1; @@ -86,7 +85,6 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode) { // int clk; // Abc_Obj_t * pFanin; - float * pProbab = (float *)p->vProbs->pArray; // int i; p->nNodesTried++; @@ -120,7 +118,6 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { int clk; Abc_Obj_t * pFanin; - float * pProbab = (float *)p->vProbs->pArray; int i; if (Abc_WinNode(p, pNode) // something wrong @@ -130,11 +127,11 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) // Abc_NtkMfsEdgePower( p, pNode ); // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) return 1; Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) return 1; if ( Abc_ObjFaninNum(pNode) == p->nFaninMax ) @@ -142,7 +139,7 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) // try replacing area critical fanins while adding two new fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) return 1; } return 0; @@ -157,7 +154,6 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars) Abc_Obj_t *pFanin, *pNode; Abc_Ntk_t *pNtk = p->pNtk; int nFaninMax = Abc_NtkGetFaninMax(p->pNtk); - float * pProbab = (float *)p->vProbs->pArray; Abc_NtkForEachNode( pNtk, pNode, k ) { @@ -172,7 +168,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars) // Abc_NtkMfsEdgePower( p, pNode ); // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) continue; } @@ -189,7 +185,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars) // Abc_NtkMfsEdgePower( p, pNode ); // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) continue; } @@ -203,7 +199,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars) continue; Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) continue; } /* @@ -217,7 +213,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars) continue; Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) continue; } */ @@ -456,7 +452,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) if ( p->pCare ) { Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pData = (void *)(PORT_PTRUINT_T)i; + pObj->pData = (void *)(ABC_PTRUINT_T)i; } // compute levels @@ -531,7 +527,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes), 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes), 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) ); - PRT( "Time", clock() - clk2 ); + ABC_PRT( "Time", clock() - clk2 ); */ } } @@ -571,7 +567,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) #endif } - // free the manager + // ABC_FREE the manager p->timeTotal = clock() - clk; Mfs_ManStop( p ); return 1; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 9eb6e4a4..13f0bce2 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -21,10 +21,6 @@ #ifndef __MFS_INT_H__ #define __MFS_INT_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -41,6 +37,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + #define MFS_FANIN_MAX 12 typedef struct Mfs_Man_t_ Mfs_Man_t; @@ -116,6 +116,8 @@ struct Mfs_Man_t_ int timeTotal; }; +static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; } + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 6e50d444..8fc30056 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -239,7 +239,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert ); // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status != l_False ) { p->nTimeOuts++; @@ -339,7 +339,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 ); // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status != l_False ) { p->nTimeOuts++; diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 9a043ed8..e947bd52 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -43,7 +43,7 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) { Mfs_Man_t * p; // start the manager - p = ALLOC( Mfs_Man_t, 1 ); + p = ABC_ALLOC( Mfs_Man_t, 1 ); memset( p, 0, sizeof(Mfs_Man_t) ); p->pPars = pPars; p->vProjVars = Vec_IntAlloc( 100 ); @@ -158,13 +158,13 @@ void Mfs_ManPrint( Mfs_Man_t * p ) p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); } /* - PRTP( "Win", p->timeWin , p->timeTotal ); - PRTP( "Div", p->timeDiv , p->timeTotal ); - PRTP( "Aig", p->timeAig , p->timeTotal ); - PRTP( "Cnf", p->timeCnf , p->timeTotal ); - PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); - PRTP( "Int", p->timeInt , p->timeTotal ); - PRTP( "ALL", p->timeTotal , p->timeTotal ); + ABC_PRTP( "Win", p->timeWin , p->timeTotal ); + ABC_PRTP( "Div", p->timeDiv , p->timeTotal ); + ABC_PRTP( "Aig", p->timeAig , p->timeTotal ); + ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal ); + ABC_PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); + ABC_PRTP( "Int", p->timeInt , p->timeTotal ); + ABC_PRTP( "ALL", p->timeTotal , p->timeTotal ); */ } @@ -201,7 +201,7 @@ void Mfs_ManStop( Mfs_Man_t * p ) Vec_IntFree( p->vProjVars ); Vec_IntFree( p->vDivLits ); Vec_PtrFree( p->vDivCexes ); - free( p ); + ABC_FREE( p ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index e9ea2c40..e49fd61d 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -100,7 +100,7 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) unsigned * pData; int RetValue, iVar, i; p->nSatCalls++; - RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); // assert( RetValue == l_False || RetValue == l_True ); if ( RetValue == l_False ) return 1; @@ -209,8 +209,6 @@ p->timeInt += clock() - clk; iVar = -1; while ( 1 ) { - float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL); - assert( (pProbab != NULL) == p->pPars->fPower ); if ( fVeryVerbose ) { printf( "%3d: %2d ", p->nCexes, iVar ); @@ -231,7 +229,7 @@ p->timeInt += clock() - clk; { Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar); // only accept the divisor if it is "cool" - if ( pProbab[Abc_ObjId(pDiv)] >= 0.15 ) + if ( Abc_MfsObjProb(p, pDiv) >= 0.15 ) continue; } pData = Vec_PtrEntry( p->vDivCexes, iVar ); @@ -355,8 +353,6 @@ p->timeInt += clock() - clk; while ( 1 ) { #if 1 // sjang - float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL); - assert( (pProbab != NULL) == p->pPars->fPower ); #endif if ( fVeryVerbose ) { @@ -381,7 +377,7 @@ p->timeInt += clock() - clk; { Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar); // only accept the divisor if it is "cool" - if ( pProbab[Abc_ObjId(pDiv)] >= 0.12 ) + if ( Abc_MfsObjProb(p, pDiv) >= 0.12 ) continue; } #endif @@ -393,7 +389,7 @@ p->timeInt += clock() - clk; { Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar2); // only accept the divisor if it is "cool" - if ( pProbab[Abc_ObjId(pDiv)] >= 0.12 ) + if ( Abc_MfsObjProb(p, pDiv) >= 0.12 ) continue; } #endif @@ -477,16 +473,15 @@ int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ) int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Abc_Obj_t * pFanin; - float * pProbab = (float *)p->vProbs->pArray; int i; // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) { - if ( pProbab[pFanin->Id] >= 0.35 ) + if ( Abc_MfsObjProb(p, pFanin) >= 0.35 ) { if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) return 1; - } else if ( pProbab[pFanin->Id] >= 0.25 ) // sjang + } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang { if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) return 1; diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index 6cc0f0fd..a35d67e4 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -46,7 +46,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts ) return -1; nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0; - RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False ); if ( RetValue == l_Undef ) return -1; diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index 1153e4fd..578c2fbe 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -193,14 +193,14 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_ManIncrementTravId( p->pCare ); Vec_PtrForEachEntry( p->vSupp, pFanin, i ) { - pPi = Aig_ManPi( p->pCare, (int)(PORT_PTRUINT_T)pFanin->pData ); + pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData ); Aig_ObjSetTravIdCurrent( p->pCare, pPi ); pPi->pData = pFanin->pCopy; } // construct the constraints Vec_PtrForEachEntry( p->vSupp, pFanin, i ) { - vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(PORT_PTRUINT_T)pFanin->pData ); + vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData ); Vec_IntForEachEntry( vOuts, iOut, k ) { pPo = Aig_ManPo( p->pCare, iOut ); @@ -280,7 +280,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_ManIncrementTravId( p->pCare ); Vec_PtrForEachEntry( p->vSupp, pFanin, i ) { - pPi = Aig_ManPi( p->pCare, (int)(PORT_PTRUINT_T)pFanin->pData ); + pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData ); Aig_ObjSetTravIdCurrent( p->pCare, pPi ); pPi->pData = Aig_ObjCreatePi(pMan); } @@ -288,7 +288,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode ) pObjRoot = Aig_ManConst1(pMan); Vec_PtrForEachEntry( p->vSupp, pFanin, i ) { - vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(PORT_PTRUINT_T)pFanin->pData ); + vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData ); Vec_IntForEachEntry( vOuts, iOut, k ) { pPo = Aig_ManPo( p->pCare, iOut ); |