summaryrefslogtreecommitdiffstats
path: root/src/aig/mfx
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/mfx')
-rw-r--r--src/aig/mfx/mfx.h8
-rw-r--r--src/aig/mfx/mfxCore.c4
-rw-r--r--src/aig/mfx/mfxInt.h8
-rw-r--r--src/aig/mfx/mfxInter.c4
-rw-r--r--src/aig/mfx/mfxMan.c18
-rw-r--r--src/aig/mfx/mfxResub.c2
-rw-r--r--src/aig/mfx/mfxSat.c2
7 files changed, 23 insertions, 23 deletions
diff --git a/src/aig/mfx/mfx.h b/src/aig/mfx/mfx.h
index aae9e625..09c4f039 100644
--- a/src/aig/mfx/mfx.h
+++ b/src/aig/mfx/mfx.h
@@ -21,10 +21,6 @@
#ifndef __MFX_H__
#define __MFX_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/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index f67fb520..c0d3b650 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -355,7 +355,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
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 );
}
}
@@ -371,7 +371,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
if ( pPars->fPower )
printf( "Total switching after = %7.2f.\n", Nwl_ManComputeTotalSwitching(pNtk) );
- // free the manager
+ // ABC_FREE the manager
p->timeTotal = clock() - clk;
Mfx_ManStop( p );
diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
index 9095c8ce..4263724c 100644
--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -21,10 +21,6 @@
#ifndef __MFX_INT_H__
#define __MFX_INT_H__
-#ifdef __cplusplus
-extern "C" {
-#endif
-
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -41,6 +37,10 @@ extern "C" {
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
+#ifdef __cplusplus
+extern "C" {
+#endif
+
#define MFX_FANIN_MAX 12
typedef struct Mfx_Man_t_ Mfx_Man_t;
diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c
index a42e02fe..3e1e3de2 100644
--- a/src/aig/mfx/mfxInter.c
+++ b/src/aig/mfx/mfxInter.c
@@ -222,7 +222,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn
pSat = Mfx_CreateSolverResub( 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++;
@@ -322,7 +322,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands )
pSat = Mfx_CreateSolverResub( 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/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
index b8361a20..2af3d573 100644
--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -43,7 +43,7 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars )
{
Mfx_Man_t * p;
// start the manager
- p = ALLOC( Mfx_Man_t, 1 );
+ p = ABC_ALLOC( Mfx_Man_t, 1 );
memset( p, 0, sizeof(Mfx_Man_t) );
p->pPars = pPars;
p->vProjVars = Vec_IntAlloc( 100 );
@@ -135,13 +135,13 @@ void Mfx_ManPrint( Mfx_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 );
*/
}
@@ -178,7 +178,7 @@ void Mfx_ManStop( Mfx_Man_t * p )
Vec_IntFree( p->vProjVars );
Vec_IntFree( p->vDivLits );
Vec_PtrFree( p->vDivCexes );
- free( p );
+ ABC_FREE( p );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 312ae226..a9ed23a0 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -97,7 +97,7 @@ int Mfx_TryResubOnce( Mfx_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;
diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c
index 9dd42e8c..ce8d580b 100644
--- a/src/aig/mfx/mfxSat.c
+++ b/src/aig/mfx/mfxSat.c
@@ -46,7 +46,7 @@ int Mfx_SolveSat_iter( Mfx_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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-01 08:02:25 +0000