From 5bb7dd60739b44b6683fea5caaa2a1fc46a2b5da Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 1 Jul 2012 12:43:22 -0700 Subject: Other improvements to bmc2 and bmc3. --- src/aig/saig/saigBmc2.c | 2 +- src/aig/saig/saigBmc3.c | 66 ++++++++++++++++++++++++++++++++----------------- 2 files changed, 45 insertions(+), 23 deletions(-) (limited to 'src/aig') diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index ea37b4a7..4a95bdbc 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -787,7 +787,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved ); if ( fVerbose ) { - printf( "%3d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ", + printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ", Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts ); printf( "%4.0f Mb", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) ); printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 27a03120..5b36c01a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -995,7 +995,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in assert( fAddClauses ); iLit = Saig_ManBmcLiteral( p, pObj, iFrame ); if ( iLit != ~0 ) - return iLit; + return iLit; assert( iFrame >= 0 ); if ( Aig_ObjIsCi(pObj) ) { @@ -1032,19 +1032,41 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in // create CNF if ( fAddClauses ) { - iLit = toLit( p->nSatVars++ ); - Saig_ManBmcAddClauses( p, uTruth, Lits, iLit ); - if ( uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA || uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC || uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 || uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00 ) - p->nBufNum++; + { + p->nBufNum++; + + if ( uTruth == 0xAAAA ) + iLit = Lits[0]; + else if ( uTruth == 0xCCCC ) + iLit = Lits[1]; + else if ( uTruth == 0xF0F0 ) + iLit = Lits[2]; + else if ( uTruth == 0xFF00 ) + iLit = Lits[3]; + else if ( (0xffff & ~uTruth) == 0xAAAA ) + iLit = Abc_LitNot(Lits[0]); + else if ( (0xffff & ~uTruth) == 0xCCCC ) + iLit = Abc_LitNot(Lits[1]); + else if ( (0xffff & ~uTruth) == 0xF0F0 ) + iLit = Abc_LitNot(Lits[2]); + else if ( (0xffff & ~uTruth) == 0xFF00 ) + iLit = Abc_LitNot(Lits[3]); + + } + else + { + iLit = toLit( p->nSatVars++ ); + Saig_ManBmcAddClauses( p, uTruth, Lits, iLit ); - if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3])) || - (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) || - (Lits[2] > 1 && (Lits[2] == Lits[3])) ) - p->nDupNum++; + if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3])) || + (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) || + (Lits[2] > 1 && (Lits[2] == Lits[3])) ) + p->nDupNum++; + } } else @@ -1324,21 +1346,21 @@ clkOther += clock() - clk2; { if ( pPars->fVerbose ) { - printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); + printf( "%4d %s : ", f, fUnfinished ? "-" : "+" ); printf( "Var =%8.0f. ", (double)p->nSatVars ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%4.0f Mb", 4.25*(f+1)*p->nObjNums /(1<<20) ); - printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); - printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "\n" ); + printf( "%4.0f Mb", 4.25*(f+1)*p->nObjNums /(1<<20) ); + printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); +// printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRMn( "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( "S =%6d. ", p->nBufNum ); + printf( "D =%6d. ", p->nDupNum ); + printf( "\n" ); fflush( stdout ); } ABC_FREE( pAig->pSeqModel ); @@ -1387,7 +1409,7 @@ clkOther += clock() - clk2; fFirst = 0; // printf( "Outputs of frames up to %d are trivially UNSAT.\n", f ); } - printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); + printf( "%4d %s : ", f, fUnfinished ? "-" : "+" ); printf( "Var =%8.0f. ", (double)p->nSatVars ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); @@ -1397,12 +1419,12 @@ clkOther += clock() - clk2; printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) ); printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "\n" ); +// printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRMn( "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( "Simples = %6d. ", p->nBufNum ); + printf( "Dups = %6d. ", p->nDupNum ); + printf( "\n" ); fflush( stdout ); } } -- cgit v1.2.3