summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-08-01 11:47:13 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-08-01 11:47:13 +0700
commit48f3db0b2dece88c09b169393604b1a8634d32d7 (patch)
treed865d4044aa44fcb50fd8326e02081b1198606cb
parentab3c537072854a95c7da6e1dcc7f155c808fb837 (diff)
downloadabc-48f3db0b2dece88c09b169393604b1a8634d32d7.tar.gz
abc-48f3db0b2dece88c09b169393604b1a8634d32d7.tar.bz2
abc-48f3db0b2dece88c09b169393604b1a8634d32d7.zip
Reducing print-out in 'bmc3'.
-rw-r--r--src/aig/saig/saigBmc3.c18
1 files changed, 9 insertions, 9 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 508a46c1..b984844e 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -567,7 +567,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
int i;
- assert( Aig_ManRegNum(pAig) > 0 );
+// assert( Aig_ManRegNum(pAig) > 0 );
p = ABC_CALLOC( Gia_ManBmc_t, 1 );
p->pAig = pAig;
// create mapping
@@ -1236,11 +1236,11 @@ clkOther += clock() - clk2;
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
ABC_PRT( "Time", clock() - clk );
- ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
- ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
- printf( "Simples = %6d. ", p->nBufNum );
+// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
+// ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
+// printf( "Simples = %6d. ", p->nBufNum );
// printf( "Dups = %6d. ", p->nDupNum );
- printf( "\n" );
+// printf( "\n" );
fflush( stdout );
}
ABC_FREE( pAig->pSeqModel );
@@ -1292,11 +1292,11 @@ clkOther += clock() - clk2;
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
{
- ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
- ABC_PRM( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
- printf( "Simples = %6d. ", p->nBufNum );
+// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
+// ABC_PRM( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
+// printf( "Simples = %6d. ", p->nBufNum );
// printf( "Dups = %6d. ", p->nDupNum );
- printf( "\n" );
+// printf( "\n" );
}
Saig_Bmc3ManStop( p );
return RetValue;