summaryrefslogtreecommitdiffstats
path: root/src/opt/mfs
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/mfs')
-rw-r--r--src/opt/mfs/mfs.h8
-rw-r--r--src/opt/mfs/mfsCore.c28
-rw-r--r--src/opt/mfs/mfsInt.h10
-rw-r--r--src/opt/mfs/mfsInter.c4
-rw-r--r--src/opt/mfs/mfsMan.c18
-rw-r--r--src/opt/mfs/mfsResub.c17
-rw-r--r--src/opt/mfs/mfsSat.c2
-rw-r--r--src/opt/mfs/mfsStrash.c8
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 );