summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h16
-rw-r--r--src/aig/fra/fraBmc.c28
-rw-r--r--src/aig/fra/fraCec.c36
-rw-r--r--src/aig/fra/fraClass.c36
-rw-r--r--src/aig/fra/fraClau.c20
-rw-r--r--src/aig/fra/fraClaus.c78
-rw-r--r--src/aig/fra/fraCnf.c4
-rw-r--r--src/aig/fra/fraHot.c2
-rw-r--r--src/aig/fra/fraImp.c33
-rw-r--r--src/aig/fra/fraInd.c18
-rw-r--r--src/aig/fra/fraIndVer.c2
-rw-r--r--src/aig/fra/fraLcr.c38
-rw-r--r--src/aig/fra/fraMan.c46
-rw-r--r--src/aig/fra/fraPart.c20
-rw-r--r--src/aig/fra/fraSat.c14
-rw-r--r--src/aig/fra/fraSec.c60
-rw-r--r--src/aig/fra/fraSim.c13
17 files changed, 234 insertions, 230 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index e7cd0550..a2c10367 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -21,10 +21,6 @@
#ifndef __FRA_H__
#define __FRA_H__
-#ifdef __cplusplus
-extern "C" {
-#endif
-
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -45,6 +41,10 @@ extern "C" {
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
+#ifdef __cplusplus
+extern "C" {
+#endif
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@@ -215,8 +215,8 @@ struct Fra_Man_t_
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
Vec_Ptr_t * vPiVars; // the PIs of the cone used
- sint64 nBTLimitGlobal; // resource limit
- sint64 nInsLimitGlobal; // resource limit
+ ABC_INT64_T nBTLimitGlobal; // resource limit
+ ABC_INT64_T nInsLimitGlobal; // resource limit
Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes
int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes
int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins
@@ -290,7 +290,7 @@ static inline int Fra_ImpCreate( int Left, int Right )
////////////////////////////////////////////////////////////////////////
/*=== fraCec.c ========================================================*/
-extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
@@ -376,7 +376,7 @@ extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit );
extern void Fra_SmlResimulate( Fra_Man_t * p );
extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Fra_SmlStop( Fra_Sml_t * p );
-extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 411ca2c1..689d7d67 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -188,13 +188,13 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
{
Fra_Bmc_t * p;
- p = ALLOC( Fra_Bmc_t, 1 );
+ p = ABC_ALLOC( Fra_Bmc_t, 1 );
memset( p, 0, sizeof(Fra_Bmc_t) );
p->pAig = pAig;
p->nPref = nPref;
p->nDepth = nDepth;
p->nFramesAll = nPref + nDepth;
- p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
+ p->pObjToFrames = ABC_ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
return p;
}
@@ -215,9 +215,9 @@ void Fra_BmcStop( Fra_Bmc_t * p )
Aig_ManStop( p->pAigFrames );
if ( p->pAigFraig )
Aig_ManStop( p->pAigFraig );
- free( p->pObjToFrames );
- free( p->pObjToFraig );
- free( p );
+ ABC_FREE( p->pObjToFrames );
+ ABC_FREE( p->pObjToFraig );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -253,7 +253,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
// add timeframes
- pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+ pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
for ( f = 0; f < p->nFramesAll; f++ )
{
// add internal nodes of this frame
@@ -275,7 +275,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
assert( k == Aig_ManRegNum(p->pAig) );
}
- free( pLatches );
+ ABC_FREE( pLatches );
if ( fKeepPos )
{
for ( f = 0; f < p->nFramesAll; f++ )
@@ -333,7 +333,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ",
Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll,
Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
printf( "Before BMC: " );
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
@@ -360,7 +360,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
- // free the BMC manager
+ // ABC_FREE the BMC manager
Fra_BmcStop( p->pBmc );
p->pBmc = NULL;
}
@@ -397,7 +397,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
nFrames, Aig_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames),
Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
if ( fRewrite )
{
@@ -408,7 +408,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
{
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
}
clk = clock();
@@ -422,7 +422,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
if ( pBmc->pAigFraig->pData )
{
pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
- FREE( pBmc->pAigFraig->pData );
+ ABC_FREE( pBmc->pAigFraig->pData );
}
else if ( iOutput >= 0 )
pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
@@ -432,10 +432,10 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
printf( "Fraiged init frames: Node = %6d. Lev = %5d. ",
pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
Fra_BmcStop( pBmc );
- free( pTemp );
+ ABC_FREE( pTemp );
}
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 2cdf203d..0cc6748c 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -40,7 +40,7 @@
SeeAlso []
***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
@@ -91,13 +91,13 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
+// ABC_PRT( "Time", clock() - clk );
// simplify the problem
clk = clock();
status = sat_solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
+// ABC_PRT( "Time", clock() - clk );
if ( status == 0 )
{
Vec_IntFree( vCiIds );
@@ -110,7 +110,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
clk = clock();
if ( fVerbose )
pSat->verbosity = 1;
- status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
+ status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
@@ -128,7 +128,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
}
else
assert( 0 );
-// PRT( "SAT sat_solver time", clock() - clk );
+// ABC_PRT( "SAT sat_solver time", clock() - clk );
// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
// if the problem is SAT, get the counterexample
@@ -136,7 +136,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
{
pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
}
- // free the sat_solver
+ // ABC_FREE the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
//sat_solver_store_write( pSat, "trace.cnf" );
@@ -176,18 +176,18 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
// assert( RetValue == -1 );
if ( RetValue == 0 )
{
- pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) );
+ pAig->pData = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
return RetValue;
}
// if SAT only, solve without iteration
clk = clock();
- RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 );
+ RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0 );
if ( fVerbose )
{
printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
if ( RetValue >= 0 )
return RetValue;
@@ -199,7 +199,7 @@ clk = clock();
if ( fVerbose )
{
printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
// perform the loop
@@ -218,7 +218,7 @@ clk = clock();
if ( fVerbose )
{
printf( "Fraiging (i=%d): Nodes = %6d. ", i+1, Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
// check the miter status
@@ -233,7 +233,7 @@ clk = clock();
if ( fVerbose )
{
printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
// check the miter status
@@ -251,11 +251,11 @@ PRT( "Time", clock() - clk );
if ( RetValue == -1 )
{
clk = clock();
- RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 );
+ RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0 );
if ( fVerbose )
{
printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -318,7 +318,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
fflush( stdout );
}
- // free intermediate results
+ // ABC_FREE intermediate results
Vec_PtrForEachEntry( vParts, pAig, i )
Aig_ManStop( pAig );
Vec_PtrFree( vParts );
@@ -373,17 +373,17 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
else
{
printf( "Networks are UNDECIDED. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
fflush( stdout );
return RetValue;
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 064d2b9c..8554b312 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -57,10 +57,10 @@ static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb
Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
{
Fra_Cla_t * p;
- p = ALLOC( Fra_Cla_t, 1 );
+ p = ABC_ALLOC( Fra_Cla_t, 1 );
memset( p, 0, sizeof(Fra_Cla_t) );
p->pAig = pAig;
- p->pMemRepr = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+ p->pMemRepr = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 );
@@ -86,15 +86,15 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
***********************************************************************/
void Fra_ClassesStop( Fra_Cla_t * p )
{
- FREE( p->pMemClasses );
- FREE( p->pMemRepr );
+ ABC_FREE( p->pMemClasses );
+ ABC_FREE( p->pMemRepr );
if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
if ( p->vClasses ) Vec_PtrFree( p->vClasses );
if ( p->vImps ) Vec_IntFree( p->vImps );
- free( p );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -278,8 +278,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
// allocate the hash table hashing simulation info into nodes
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
- ppTable = ALLOC( Aig_Obj_t *, nTableSize );
- ppNexts = ALLOC( Aig_Obj_t *, nTableSize );
+ ppTable = ABC_ALLOC( Aig_Obj_t *, nTableSize );
+ ppNexts = ABC_ALLOC( Aig_Obj_t *, nTableSize );
memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
// add all the nodes to the hash table
@@ -338,7 +338,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
}
// allocate room for classes
- p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+ p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
p->pMemClassesFree = p->pMemClasses + 2*nEntries;
// copy the entries into storage in the topological order
@@ -374,8 +374,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
// increment the number of entries
nEntries += k;
}
- free( ppTable );
- free( ppNexts );
+ ABC_FREE( ppTable );
+ ABC_FREE( ppNexts );
// now it is time to refine the classes
Fra_ClassesRefine( p );
// Fra_ClassesPrint( p, 0 );
@@ -587,7 +587,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
{
Aig_Obj_t ** pClass;
- p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
+ p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
pClass = p->pMemClasses;
assert( Id1 < Id2 );
pClass[0] = Aig_ManObj( p->pAig, Id1 );
@@ -620,7 +620,7 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
}
// allocate room for classes
- p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
+ p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}
@@ -644,7 +644,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
// perform combinational simulation
pComb = Fra_SmlSimulateComb( p->pAig, 32 );
// compute the weight of each node in the classes
- pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
@@ -686,7 +686,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
Vec_PtrShrink( p->vClasses, k );
printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
- free( pWeights );
+ ABC_FREE( pWeights );
}
/**Function*************************************************************
@@ -804,13 +804,13 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
// allocate place for the node mapping
- ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
+ ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
// create latches for the first frame
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
// add timeframes
- pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+ pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
for ( f = 0; f < nFramesAll; f++ )
{
// create PIs for this frame
@@ -839,8 +839,8 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
}
- free( pLatches );
- free( ppEquivs );
+ ABC_FREE( pLatches );
+ ABC_FREE( ppEquivs );
// mark the asserts
assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
printf( "Assert miters = %6d. Output miters = %6d.\n",
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
index 919d0000..96d06380 100644
--- a/src/aig/fra/fraClau.c
+++ b/src/aig/fra/fraClau.c
@@ -152,7 +152,7 @@ int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, i
{
int * pMapping, Var, i;
assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
- pMapping = ALLOC( int, nVarsMax );
+ pMapping = ABC_ALLOC( int, nVarsMax );
for ( i = 0; i < nVarsMax; i++ )
pMapping[i] = -1;
Vec_IntForEachEntry( vSatVarsFrom, Var, i )
@@ -174,10 +174,10 @@ int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, i
***********************************************************************/
void Fra_ClauStop( Cla_Man_t * p )
{
- free( p->pMapCsMainToCsTest );
- free( p->pMapCsTestToCsMain );
- free( p->pMapCsTestToNsTest );
- free( p->pMapCsTestToNsBmc );
+ ABC_FREE( p->pMapCsMainToCsTest );
+ ABC_FREE( p->pMapCsTestToCsMain );
+ ABC_FREE( p->pMapCsTestToNsTest );
+ ABC_FREE( p->pMapCsTestToNsBmc );
Vec_IntFree( p->vSatVarsMainCs );
Vec_IntFree( p->vSatVarsTestCs );
Vec_IntFree( p->vSatVarsTestNs );
@@ -191,7 +191,7 @@ void Fra_ClauStop( Cla_Man_t * p )
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
- free( p );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -217,7 +217,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
// start the manager
- p = ALLOC( Cla_Man_t, 1 );
+ p = ABC_ALLOC( Cla_Man_t, 1 );
memset( p, 0, sizeof(Cla_Man_t) );
p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) );
@@ -362,7 +362,7 @@ int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
int nBTLimit = 0;
int RetValue, iVar, i;
sat_solver_act_var_clear( p->pSatMain );
- RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Vec_IntClear( vCex );
if ( RetValue == l_False )
return 1;
@@ -396,7 +396,7 @@ int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
int nBTLimit = 0;
int RetValue;
RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause),
- (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
return 1;
assert( RetValue == l_True );
@@ -458,7 +458,7 @@ int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
// try to solve
RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm),
- (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( vCex )
Vec_IntClear( vCex );
if ( RetValue == l_False )
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 91b70702..e5fe3f40 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -98,7 +98,7 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
for ( i = 0; i < p->nPref + p->nFrames; i++ )
{
Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
- RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue != l_False )
return 0;
}
@@ -121,14 +121,14 @@ int Fra_ClausRunSat( Clu_Man_t * p )
Aig_Obj_t * pObj;
int * pLits;
int i, RetValue;
- pLits = ALLOC( int, p->nFrames + 1 );
+ pLits = ABC_ALLOC( int, p->nFrames + 1 );
// set the output literals
pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i <= p->nFrames; i++ )
pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
// try to solve the problem
- RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- free( pLits );
+ RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ ABC_FREE( pLits );
if ( RetValue == l_False )
return 1;
// get the counter-example
@@ -153,7 +153,7 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
int Lits[2], RetValue;
pObj = Aig_ManPo(p->pAig, 0);
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
- RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
return 1;
return 0;
@@ -350,7 +350,7 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
// count how many implications have each cost
CostMax = p->nSimWords * 32 + 1;
- pCostCount = ALLOC( int, CostMax );
+ pCostCount = ABC_ALLOC( int, CostMax );
memset( pCostCount, 0, sizeof(int) * CostMax );
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
@@ -380,7 +380,7 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
}
Vec_IntWriteEntry( p->vCosts, i, -1 );
}
- free( pCostCount );
+ ABC_FREE( pCostCount );
p->nClauses = nClauCount;
if ( p->fVerbose )
printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
@@ -608,7 +608,7 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
clk = clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
- pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+ pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
if ( p->fTarget && pSeq->fNonConstOut )
{
printf( "Property failed after sequential simulation!\n" );
@@ -617,7 +617,7 @@ clk = clock();
}
if ( p->fVerbose )
{
-PRT( "Sim-seq", clock() - clk );
+ABC_PRT( "Sim-seq", clock() - clk );
}
@@ -627,7 +627,7 @@ clk = clock();
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
-PRT( "Lat-cla", clock() - clk );
+ABC_PRT( "Lat-cla", clock() - clk );
}
}
@@ -638,7 +638,7 @@ clk = clock();
// pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
if ( p->fVerbose )
{
-PRT( "Cuts ", clock() - clk );
+ABC_PRT( "Cuts ", clock() - clk );
}
// collect sequential info for each cut
@@ -656,7 +656,7 @@ clk = clock();
}
if ( p->fVerbose )
{
-PRT( "Infoseq", clock() - clk );
+ABC_PRT( "Infoseq", clock() - clk );
}
Fra_SmlStop( pSeq );
@@ -667,7 +667,7 @@ clk = clock();
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
-PRT( "Sim-cmb", clock() - clk );
+ABC_PRT( "Sim-cmb", clock() - clk );
}
// collect combinational info for each cut
@@ -692,7 +692,7 @@ clk = clock();
// Aig_ManCutStop( pManCut );
if ( p->fVerbose )
{
-PRT( "Infocmb", clock() - clk );
+ABC_PRT( "Infocmb", clock() - clk );
}
if ( p->fVerbose )
@@ -732,7 +732,7 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
clk = clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
- pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+ pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
if ( p->fTarget && pSeq->fNonConstOut )
{
printf( "Property failed after sequential simulation!\n" );
@@ -741,7 +741,7 @@ clk = clock();
}
if ( p->fVerbose )
{
-//PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", clock() - clk );
}
// perform combinational simulation
@@ -751,7 +751,7 @@ clk = clock();
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
-//PRT( "Sim-cmb", clock() - clk );
+//ABC_PRT( "Sim-cmb", clock() - clk );
}
@@ -761,7 +761,7 @@ clk = clock();
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
-//PRT( "Lat-cla", clock() - clk );
+//ABC_PRT( "Lat-cla", clock() - clk );
}
}
@@ -772,7 +772,7 @@ clk = clock();
pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
if ( p->fVerbose )
{
-//PRT( "Cuts ", clock() - clk );
+//ABC_PRT( "Cuts ", clock() - clk );
}
// collect combinational info for each cut
@@ -805,7 +805,7 @@ clk = clock();
{
printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
- PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
+ ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
}
// filter out clauses that are contained in the already proven clauses
@@ -852,7 +852,7 @@ clk = clock();
// check the clause
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
- RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
// the clause holds
@@ -924,7 +924,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
- RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
@@ -1292,7 +1292,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
- RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
@@ -1359,7 +1359,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
- p = ALLOC( Clu_Man_t, 1 );
+ p = ABC_ALLOC( Clu_Man_t, 1 );
memset( p, 0, sizeof(Clu_Man_t) );
p->pAig = pAig;
p->nFrames = nFrames;
@@ -1412,7 +1412,7 @@ void Fra_ClausFree( Clu_Man_t * p )
if ( p->pCnf ) Cnf_DataFree( p->pCnf );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
- free( p );
+ ABC_FREE( p );
}
@@ -1540,7 +1540,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
int * pStart, * pVar2Id;
int Beg, End, i, k;
// create mapping from SAT vars to node IDs
- pVar2Id = ALLOC( int, p->pCnf->nVars );
+ pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
if ( p->pCnf->pVarNums[i] >= 0 )
@@ -1564,7 +1564,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
Aig_ObjCreatePo( pNew, pClause );
Beg = End;
}
- free( pVar2Id );
+ ABC_FREE( pVar2Id );
Aig_ManCleanup( pNew );
pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
@@ -1624,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
// create mapping from SAT vars to node IDs
- pVar2Id = ALLOC( int, p->pCnf->nVars );
+ pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
if ( p->pCnf->pVarNums[i] >= 0 )
@@ -1654,11 +1654,11 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
for ( w = 0; w < nCombSimWords; w++ )
nCovered += Aig_WordCountOnes( pResultTot[w] );
Fra_SmlStop( pComb );
- free( pVar2Id );
+ ABC_FREE( pVar2Id );
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
@@ -1686,7 +1686,7 @@ if ( p->fVerbose )
{
printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
-//PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", clock() - clk );
}
assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
@@ -1700,7 +1700,7 @@ clk = clock();
// p->pAig->nRegs--;
if ( fVerbose )
{
-//PRT( "CNF ", clock() - clk );
+//ABC_PRT( "CNF ", clock() - clk );
}
// check BMC
@@ -1720,7 +1720,7 @@ clk = clock();
}
if ( fVerbose )
{
-//PRT( "SAT-bmc", clock() - clk );
+//ABC_PRT( "SAT-bmc", clock() - clk );
}
// start the SAT solver
@@ -1751,7 +1751,7 @@ clk = clock();
}
if ( fVerbose )
{
-// PRT( "SAT-ind", clock() - clk );
+// ABC_PRT( "SAT-ind", clock() - clk );
}
// collect the candidate inductive clauses using 4-cuts
@@ -1763,7 +1763,7 @@ clk = clock();
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
nClausesBeg = p->nClauses;
- //PRT( "Clauses", clock() - clk );
+ //ABC_PRT( "Clauses", clock() - clk );
// check clauses using BMC
@@ -1775,7 +1775,7 @@ clk = clock();
if ( fVerbose )
{
printf( "BMC disproved %d clauses. ", Counter );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
}
@@ -1794,7 +1794,7 @@ clk = clock();
{
printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
// printf( "\n" );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
clk = clock();
}
@@ -1809,14 +1809,14 @@ clk = clock();
printf( "Property FAILS during refinement. " );
else
printf( "Property HOLDS inductively after strengthening. " );
- PRT( "Time ", clock() - clkTotal );
+ ABC_PRT( "Time ", clock() - clkTotal );
if ( !p->fFail )
break;
}
else
{
printf( "Finished proving inductive clauses. " );
- PRT( "Time ", clock() - clkTotal );
+ ABC_PRT( "Time ", clock() - clkTotal );
}
}
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index d96fe8a1..27da3fc5 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -131,7 +131,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
assert( Aig_ObjIsNode( pNode ) );
// create storage for literals
nLits = Vec_PtrSize(vSuper) + 1;
- pLits = ALLOC( int, nLits );
+ pLits = ABC_ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
Vec_PtrForEachEntry( vSuper, pFanin, i )
@@ -147,7 +147,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
assert( RetValue );
- free( pLits );
+ ABC_FREE( pLits );
}
/**Function*************************************************************
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index b2156193..c4472121 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -378,7 +378,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
/**Function*************************************************************
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index e2bee834..d579146e 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -64,7 +64,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
int i, * pnBits;
- pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
pnBits[i] = Fra_SmlCountOnesOne( p, i );
@@ -159,7 +159,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
// count number of nodes having that many 1s
nNodes = 0;
nBits = p->nWordsTotal * 32;
- pnNodes = ALLOC( int, nBits + 1 );
+ pnNodes = ABC_ALLOC( int, nBits + 1 );
memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
@@ -183,7 +183,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
nNodes++;
}
// allocate memory for all the nodes
- pMemory = ALLOC( int, nNodes + nBits + 1 );
+ pMemory = ABC_ALLOC( int, nNodes + nBits + 1 );
// markup the memory for each node
vNodes = Vec_PtrAlloc( nBits + 1 );
Vec_PtrPush( vNodes, pMemory );
@@ -222,8 +222,8 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
nTotal += pnNodes[i];
}
assert( nTotal == nNodes + nBits + 1 );
- free( pnNodes );
- free( pnBits );
+ ABC_FREE( pnNodes );
+ ABC_FREE( pnBits );
return vNodes;
}
@@ -244,7 +244,7 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
int * pCostCount, nImpCount, Imp, i, c;
assert( Vec_IntSize(vImps) >= nImpLimit );
// count how many implications have each cost
- pCostCount = ALLOC( int, nCostMax + 1 );
+ pCostCount = ABC_ALLOC( int, nCostMax + 1 );
memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
for ( i = 0; i < Vec_IntSize(vImps); i++ )
{
@@ -271,7 +271,7 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
if ( Vec_IntSize( vImpsNew ) == nImpLimit )
break;
}
- free( pCostCount );
+ ABC_FREE( pCostCount );
if ( pCostRange )
*pCostRange = c;
return vImpsNew;
@@ -329,7 +329,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
- pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
// get the nodes sorted by the number of 1s
vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
// count the total number of implications
@@ -340,7 +340,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
nImpsTotal++;
// compute implications and their costs
- pImpCosts = ALLOC( int, nImpMaxLimit );
+ pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
vImps = Vec_IntAlloc( nImpMaxLimit );
for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
for ( i = k - 1; i > 0; i-- )
@@ -384,8 +384,11 @@ finish:
}
// dealloc
- free( pImpCosts );
- free( Vec_PtrEntry(vNodes, 0) );
+ ABC_FREE( pImpCosts );
+ {
+ void * pTemp = Vec_PtrEntry(vNodes, 0);
+ ABC_FREE( pTemp );
+ }
Vec_PtrFree( vNodes );
// reorder implications topologically
qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int),
@@ -396,7 +399,7 @@ printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
CostMin, CostRange, CostMax );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
return vImps;
}
@@ -665,9 +668,9 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return 0;
// simulate the AIG manager with combinational patterns
- pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1 );
// go through the implications and check how many of them do not hold
- pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
+ pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
{
@@ -679,7 +682,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
Counter = 0;
for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
Counter += pfFails[i];
- free( pfFails );
+ ABC_FREE( pfFails );
Fra_SmlStop( pSeq );
return Counter;
}
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index c8b35b28..4f3812c6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,7 +198,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
pObj->pData = pObj;
// iterate and add objects
nNodesOld = Aig_ManObjNumMax(p);
- pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
+ pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
for ( f = 0; f < nFrames; f++ )
{
// clean latch inputs and outputs
@@ -230,7 +230,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
pObj->pData = NULL;
}
}
- free( pLatches );
+ ABC_FREE( pLatches );
}
@@ -308,7 +308,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
Aig_ManStop( pTemp );
- free( pMapBack );
+ ABC_FREE( pMapBack );
}
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
@@ -320,7 +320,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
- PRT( "Total time", clock() - clk );
+ ABC_PRT( "Total time", clock() - clk );
}
return pNew;
}
@@ -420,10 +420,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
// refine the classes with more simulation rounds
if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
- p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );
+ p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 );
if ( pPars->fVerbose )
{
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
@@ -556,7 +556,7 @@ clk2 = clock();
Fra_FraigSweep( p );
if ( pPars->fVerbose )
{
- PRT( "T", clock() - clk3 );
+ ABC_PRT( "T", clock() - clk3 );
}
// Sat_SolverPrintStats( stdout, p->pSat );
@@ -589,7 +589,7 @@ clk2 = clock();
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
}
*/
@@ -629,7 +629,7 @@ p->timeTotal = clock() - clk;
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
- // free the manager
+ // ABC_FREE the manager
finish:
Fra_ManStop( p );
// check the output
diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c
index efc516c9..71faa346 100644
--- a/src/aig/fra/fraIndVer.c
+++ b/src/aig/fra/fraIndVer.c
@@ -150,7 +150,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
if ( CounterBase || CounterInd )
return 0;
printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) );
- PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", clock() - clk );
return 1;
}
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index d3be9842..16912f46 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -77,12 +77,12 @@ struct Fra_Lcr_t_
Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
{
Fra_Lcr_t * p;
- p = ALLOC( Fra_Lcr_t, 1 );
+ p = ABC_ALLOC( Fra_Lcr_t, 1 );
memset( p, 0, sizeof(Fra_Lcr_t) );
p->pAig = pAig;
- p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
+ p->pInToOutPart = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
- p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
+ p->pInToOutNum = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
p->vFraigs = Vec_PtrAlloc( 1000 );
return p;
@@ -106,12 +106,12 @@ void Lcr_ManPrint( Fra_Lcr_t * p )
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
- PRT( "AIG simulation ", p->timeSim );
- PRT( "AIG partitioning", p->timePart );
- PRT( "AIG rebuiding ", p->timeTrav );
- PRT( "FRAIGing ", p->timeFraig );
- PRT( "AIG updating ", p->timeUpdate );
- PRT( "TOTAL RUNTIME ", p->timeTotal );
+ ABC_PRT( "AIG simulation ", p->timeSim );
+ ABC_PRT( "AIG partitioning", p->timePart );
+ ABC_PRT( "AIG rebuiding ", p->timeTrav );
+ ABC_PRT( "FRAIGing ", p->timeFraig );
+ ABC_PRT( "AIG updating ", p->timeUpdate );
+ ABC_PRT( "TOTAL RUNTIME ", p->timeTotal );
}
/**Function*************************************************************
@@ -136,9 +136,9 @@ void Lcr_ManFree( Fra_Lcr_t * p )
Vec_PtrFree( p->vFraigs );
if ( p->pCla ) Fra_ClassesStop( p->pCla );
if ( p->vParts ) Vec_VecFree( (Vec_Vec_t *)p->vParts );
- free( p->pInToOutPart );
- free( p->pInToOutNum );
- free( p );
+ ABC_FREE( p->pInToOutPart );
+ ABC_FREE( p->pInToOutNum );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -157,7 +157,7 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
Fra_Man_t * p;
Aig_Obj_t * pObj;
int i;
- p = ALLOC( Fra_Man_t, 1 );
+ p = ABC_ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
// Aig_ManForEachPi( pAig, pObj, i )
Aig_ManForEachObj( pAig, pObj, i )
@@ -550,10 +550,10 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
clk2 = clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
- pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 );
+ pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1 );
if ( fVerbose )
{
-PRT( "Time", clock() - clk2 );
+ABC_PRT( "Time", clock() - clk2 );
}
timeSim = clock() - clk2;
@@ -592,7 +592,7 @@ printf( "Partitioning AIG ... " );
Aig_ManStop( pAigPart );
if ( fVerbose )
{
-PRT( "Time", clock() - clk2 );
+ABC_PRT( "Time", clock() - clk2 );
p->timePart += clock() - clk2;
}
@@ -636,7 +636,7 @@ p->timeFraig += clock() - clk2;
Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
}
printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) );
-PRT( "Time", clock() - clk3 );
+ABC_PRT( "Time", clock() - clk3 );
*/
Aig_ManStop( pAigPart );
@@ -648,7 +648,7 @@ PRT( "Time", clock() - clk3 );
printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
- PRT( "T", clock() - clk3 );
+ ABC_PRT( "T", clock() - clk3 );
}
// refine the classes
Fra_LcrAigPrepareTwo( p->pAig, pTemp );
@@ -690,7 +690,7 @@ p->timeTotal = clock() - clk;
p->nNodesEnd = Aig_ManNodeNum(pAigNew);
p->nRegsEnd = Aig_ManRegNum(pAigNew);
finish:
- free( pTemp );
+ ABC_FREE( pTemp );
Lcr_ManFree( p );
if ( pnIter ) *pnIter = nIter;
return pAigNew;
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index b8cf13c5..8bdd147d 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -104,7 +104,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
Aig_Obj_t * pObj;
int i;
// allocate the fraiging manager
- p = ALLOC( Fra_Man_t, 1 );
+ p = ABC_ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars;
p->pManAig = pManAig;
@@ -112,12 +112,12 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
p->nFramesAll = pPars->nFramesK + 1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
- p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
p->vPiVars = Vec_PtrAlloc( 100 );
// equivalence classes
p->pCla = Fra_ClassesStart( pManAig );
// allocate other members
- p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
+ p->pMemFraig = ABC_ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
// set random number generator
// srand( 0xABCABC );
@@ -150,8 +150,8 @@ void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
if ( p->nMemAlloc < nNodesMax )
{
int nMemAllocNew = nNodesMax + 5000;
- p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
- p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
+ p->pMemFanins = ABC_REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
+ p->pMemSatNums = ABC_REALLOC( int, p->pMemSatNums, nMemAllocNew );
p->nMemAlloc = nMemAllocNew;
}
// prepare for the new run
@@ -191,9 +191,9 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
pObj->pData = p;
// allocate memory for mapping FRAIG nodes into SAT numbers and fanins
p->nMemAlloc = p->nSizeAlloc;
- p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
+ p->pMemFanins = ABC_ALLOC( Vec_Ptr_t *, p->nMemAlloc );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
- p->pMemSatNums = ALLOC( int, p->nMemAlloc );
+ p->pMemSatNums = ABC_ALLOC( int, p->nMemAlloc );
memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
@@ -242,7 +242,7 @@ void Fra_ManStop( Fra_Man_t * p )
if ( p->pManAig )
{
if ( p->pManAig->pObjCopies )
- free( p->pManAig->pObjCopies );
+ ABC_FREE( p->pManAig->pObjCopies );
p->pManAig->pObjCopies = p->pMemFraig;
p->pMemFraig = NULL;
}
@@ -254,11 +254,11 @@ void Fra_ManStop( Fra_Man_t * p )
if ( p->pSml ) Fra_SmlStop( p->pSml );
if ( p->vCex ) Vec_IntFree( p->vCex );
if ( p->vOneHots ) Vec_IntFree( p->vOneHots );
- FREE( p->pMemFraig );
- FREE( p->pMemFanins );
- FREE( p->pMemSatNums );
- FREE( p->pPatWords );
- free( p );
+ ABC_FREE( p->pMemFraig );
+ ABC_FREE( p->pMemFanins );
+ ABC_FREE( p->pMemSatNums );
+ ABC_FREE( p->pPatWords );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -284,19 +284,19 @@ void Fra_ManPrint( Fra_Man_t * p )
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
if ( p->pPars->fUse1Hot ) Fra_OneHotEstimateCoverage( p, p->vOneHots );
- PRT( "AIG simulation ", p->pSml->timeSim );
- PRT( "AIG traversal ", p->timeTrav );
+ ABC_PRT( "AIG simulation ", p->pSml->timeSim );
+ ABC_PRT( "AIG traversal ", p->timeTrav );
if ( p->timeRwr )
{
- PRT( "AIG rewriting ", p->timeRwr );
+ ABC_PRT( "AIG rewriting ", p->timeRwr );
}
- PRT( "SAT solving ", p->timeSat );
- PRT( " Unsat ", p->timeSatUnsat );
- PRT( " Sat ", p->timeSatSat );
- PRT( " Fail ", p->timeSatFail );
- PRT( "Class refining ", p->timeRef );
- PRT( "TOTAL RUNTIME ", p->timeTotal );
- if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
+ ABC_PRT( "SAT solving ", p->timeSat );
+ ABC_PRT( " Unsat ", p->timeSatUnsat );
+ ABC_PRT( " Sat ", p->timeSatSat );
+ ABC_PRT( " Fail ", p->timeSatFail );
+ ABC_PRT( "Class refining ", p->timeRef );
+ ABC_PRT( "TOTAL RUNTIME ", p->timeTotal );
+ if ( p->time1 ) { ABC_PRT( "time1 ", p->time1 ); }
if ( p->nSpeculs )
printf( "Speculations = %d.\n", p->nSpeculs );
fflush( stdout );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index 1766b978..6dfbd2e9 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -59,7 +59,7 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
// compute supports
clk = clock();
vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", clock() - clk );
// remove last entry
Aig_ManForEachPo( p, pObj, i )
{
@@ -76,9 +76,9 @@ clk = clock();
{
vSup = Vec_VecEntry( vSupps, i );
Vec_IntForEachEntry( vSup, Entry, k )
- Vec_VecPush( vSuppsIn, Entry, (void *)(PORT_PTRUINT_T)i );
+ Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
}
-PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", clock() - clk );
clk = clock();
// compute extended supports
@@ -153,7 +153,7 @@ clk = clock();
*/
}
// Bar_ProgressStop( pProgress );
-PRT( "Scanning", clock() - clk );
+ABC_PRT( "Scanning", clock() - clk );
// print cumulative statistics
printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
@@ -193,7 +193,7 @@ void Fra_ManPartitionTest2( Aig_Man_t * p )
// compute supports
clk = clock();
vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", clock() - clk );
// remove last entry
Aig_ManForEachPo( p, pObj, i )
{
@@ -212,13 +212,13 @@ clk = clock();
break;
vSup = Vec_VecEntry( vSupps, i );
Vec_IntForEachEntry( vSup, Entry, k )
- Vec_VecPush( vSuppsIn, Entry, (void *)(PORT_PTRUINT_T)i );
+ Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
}
-PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", clock() - clk );
// create affective supports
clk = clock();
- pSupp = ALLOC( char, Aig_ManPiNum(p) );
+ pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) );
Aig_ManForEachPo( p, pObj, i )
{
if ( i % 50 != 0 )
@@ -248,9 +248,9 @@ clk = clock();
printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
}
printf( "\n" );
-PRT( "Extension ", clock() - clk );
+ABC_PRT( "Extension ", clock() - clk );
- free( pSupp );
+ ABC_FREE( pSupp );
Vec_VecFree( vSupps );
Vec_VecFree( vSuppsIn );
}
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 8332fa77..c2eaf453 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -101,7 +101,7 @@ clk = clock();
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (sint64)nBTLimit, (sint64)0,
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -145,7 +145,7 @@ clk = clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (sint64)nBTLimit, (sint64)0,
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -177,12 +177,12 @@ p->timeSatFail += clock() - clk;
// check BDD proof
{
int RetVal;
- PRT( "Sat", clock() - clk2 );
+ ABC_PRT( "Sat", clock() - clk2 );
clk2 = clock();
RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
// printf( "%d ", RetVal );
assert( RetVal );
- PRT( "Bdd", clock() - clk2 );
+ ABC_PRT( "Bdd", clock() - clk2 );
printf( "\n" );
}
*/
@@ -263,7 +263,7 @@ clk = clock();
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (sint64)nBTLimit, (sint64)0,
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -370,7 +370,7 @@ clk = clock();
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (sint64)nBTLimit, (sint64)0,
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -447,7 +447,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
clk = clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
- (sint64)p->pPars->nBTLimitMiter, (sint64)0,
+ (ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 7545059f..a97af278 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -121,7 +121,7 @@ clk = clock();
{
printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue >= 0 )
@@ -140,7 +140,7 @@ clk = clock();
{
printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -155,7 +155,7 @@ clk = clock();
{
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -199,9 +199,9 @@ clk = clock();
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
- FREE( p->pSeqModel );
+ ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
- FREE( pTemp->pSeqModel );
+ ABC_FREE( pTemp->pSeqModel );
}
}
if ( pNew == NULL )
@@ -212,12 +212,12 @@ clk = clock();
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
Aig_ManStop( pTemp );
return RetValue;
@@ -233,7 +233,7 @@ PRT( "Time", clock() - clkTotal );
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
/*
@@ -261,7 +261,7 @@ clk = clock();
{
printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -302,7 +302,7 @@ clk = clock();
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -370,7 +370,7 @@ clk = clock();
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
break;
@@ -392,9 +392,9 @@ clk = clock();
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
- }
+ABC_PRT( "Time", clock() - clk );
}
+ }
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
@@ -410,19 +410,19 @@ clk = clock();
{
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
// perform sequential simulation
if ( pNew->nRegs )
{
clk = clock();
- pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) );
+ pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1 );
if ( pParSec->fVerbose )
{
printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
if ( pSml->fNonConstOut )
{
@@ -432,9 +432,9 @@ PRT( "Time", clock() - clk );
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
- FREE( p->pSeqModel );
+ ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
- FREE( pNew->pSeqModel );
+ ABC_FREE( pNew->pSeqModel );
}
Fra_SmlStop( pSml );
@@ -443,12 +443,12 @@ PRT( "Time", clock() - clk );
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
return RetValue;
}
@@ -481,7 +481,7 @@ clk = clock();
if ( pNewOrpos->pSeqModel )
{
Ssw_Cex_t * pCex;
- FREE( pNew->pSeqModel );
+ ABC_FREE( pNew->pSeqModel );
pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
}
@@ -498,7 +498,7 @@ clk = clock();
printf( "Property UNDECIDED after interpolation. " );
else
assert( 0 );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
}
}
@@ -518,12 +518,12 @@ finish:
if ( !pParSec->fSilent )
{
printf( "Networks are equivalent. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: PASS " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
}
else if ( RetValue == 0 )
@@ -531,12 +531,12 @@ PRT( "Time", clock() - clkTotal );
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
}
else
@@ -544,12 +544,12 @@ PRT( "Time", clock() - clkTotal );
if ( !pParSec->fSilent )
{
printf( "Networks are UNDECIDED. " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: UNDECIDED " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
}
if ( !TimeOut && !pParSec->fSilent )
{
@@ -566,9 +566,9 @@ PRT( "Time", clock() - clkTotal );
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
- FREE( p->pSeqModel );
+ ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
- FREE( pNew->pSeqModel );
+ ABC_FREE( pNew->pSeqModel );
}
}
if ( ppResult != NULL )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d1d73a03..aff21219 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -293,7 +293,7 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
- pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+ pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
Aig_ManForEachPi( p->pManAig, pObjPi, i )
{
pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
@@ -804,7 +804,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
Fra_Sml_t * p;
- p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
+ p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
p->pAig = pAig;
p->nPref = nPref;
@@ -828,7 +828,7 @@ Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
***********************************************************************/
void Fra_SmlStop( Fra_Sml_t * p )
{
- free( p );
+ ABC_FREE( p );
}
@@ -863,12 +863,13 @@ Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
SeeAlso []
***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
+Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter )
{
Fra_Sml_t * p;
p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
Fra_SmlInitialize( p, 1 );
Fra_SmlSimulateOne( p );
+ if ( fCheckMiter )
p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
return p;
}
@@ -888,7 +889,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Fra_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
- pCex = (Fra_Cex_t *)malloc( sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+ pCex = (Fra_Cex_t *)ABC_ALLOC( char, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
@@ -909,7 +910,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
***********************************************************************/
void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
{
- free( pCex );
+ ABC_FREE( pCex );
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 05:35:53 +0000