summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-09-05 20:40:50 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-09-05 20:40:50 -0700
commit23879f92000601db485d2ea226711df88c6266b9 (patch)
tree6c8ffe04300dbbcae032cda66e372b40cef7c721 /src/sat/bmc
parent9d14b0c094cc0509bf167166e6fbddeb0f8ba954 (diff)
downloadabc-23879f92000601db485d2ea226711df88c6266b9.tar.gz
abc-23879f92000601db485d2ea226711df88c6266b9.tar.bz2
abc-23879f92000601db485d2ea226711df88c6266b9.zip
Unifying parameters for the &ps command.
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmcBmcAnd.c2
-rw-r--r--src/sat/bmc/bmcCexDepth.c8
-rw-r--r--src/sat/bmc/bmcCexMin2.c4
-rw-r--r--src/sat/bmc/bmcCexTools.c4
-rw-r--r--src/sat/bmc/bmcUnroll.c4
5 files changed, 11 insertions, 11 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 29f5ffa5..d3998c10 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -345,7 +345,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// report statistics
if ( pPars->fVerbose )
{
- printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f Mb ",
+ printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames) );
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index 7bdfd0ad..3a6584b1 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -148,14 +148,14 @@ Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
{
printf( "%3d : ", i );
if ( i % Gia_ManPiNum(p) == 0 )
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
pNew = Gia_ManDupExist( pTemp = pNew, i );
Gia_ManStop( pTemp );
}
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) );
Gia_ManStop( pTemp );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
Gia_ManStop( pNew );
Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
@@ -352,7 +352,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
{
printf( "Frame %5d : ", i );
pNew = Bmc_CexBuildNetwork2_( p, pCex, i );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
Vec_PtrPush( vCones, pNew );
}
pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
index 7301c3e4..b8514601 100644
--- a/src/sat/bmc/bmcCexMin2.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -332,7 +332,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
{
pNew = Gia_ManCreateUnate( p, pCex, iFrameStart, nRealPis, fUseAll );
printf( "%3d : ", iFrameStart );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
if ( fVerbose )
Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
Gia_ManStop( pNew );
@@ -343,7 +343,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
{
pNew = Gia_ManCreateUnate( p, pCex, f, -1, fUseAll );
printf( "%3d : ", f );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
if ( fVerbose )
Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
Gia_ManStop( pNew );
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 0260b537..811a90b7 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -172,7 +172,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
Gia_Man_t * pNew;
abctime clk = Abc_Clock();
pNew = Bmc_CexPerformUnrolling( p, pCex );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
@@ -284,7 +284,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
Gia_Man_t * pNew;
abctime clk = Abc_Clock();
pNew = Bmc_CexBuildNetwork( p, pCex );
- Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_ManPrintStats( pNew, NULL );
Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index a1b51471..0ad9271b 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -487,8 +487,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
pFrames1 = Unr_ManUnrollSimple( pGia, nFrames );
Abc_PrintTime( 1, "UnrollS", Abc_Clock() - clk );
-Gia_ManPrintStats( pFrames0, 0, 0, 0 );
-Gia_ManPrintStats( pFrames1, 0, 0, 0 );
+Gia_ManPrintStats( pFrames0, NULL );
+Gia_ManPrintStats( pFrames1, NULL );
Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );