diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-01 11:47:13 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-01 11:47:13 +0700 |
| commit | 48f3db0b2dece88c09b169393604b1a8634d32d7 (patch) | |
| tree | d865d4044aa44fcb50fd8326e02081b1198606cb | |
| parent | ab3c537072854a95c7da6e1dcc7f155c808fb837 (diff) | |
| download | abc-48f3db0b2dece88c09b169393604b1a8634d32d7.tar.gz abc-48f3db0b2dece88c09b169393604b1a8634d32d7.tar.bz2 abc-48f3db0b2dece88c09b169393604b1a8634d32d7.zip | |
Reducing print-out in 'bmc3'.
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 18 |
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; |