Skip to content

A
abc
Commit 5bb7dd60 by Alan Mishchenko
Options

Other improvements to bmc2 and bmc3.

parent d3c8c3da
Showing with 45 additions and 23 deletions
src/aig/saig/saigBmc2.c
...@@ -787,7 +787,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax ...@@ -787,7 +787,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved ); RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
if ( fVerbose ) 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 ); 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( "%4.0f Mb", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
......
src/aig/saig/saigBmc3.c
...@@ -995,7 +995,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in ...@@ -995,7 +995,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
assert( fAddClauses ); assert( fAddClauses );
iLit = Saig_ManBmcLiteral( p, pObj, iFrame ); iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
if ( iLit != ~0 ) if ( iLit != ~0 )
return iLit; return iLit;
assert( iFrame >= 0 ); assert( iFrame >= 0 );
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
{ {
...@@ -1032,19 +1032,41 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in ...@@ -1032,19 +1032,41 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
// create CNF // create CNF
if ( fAddClauses ) if ( fAddClauses )
{ {
iLit = toLit( p->nSatVars++ );
Saig_ManBmcAddClauses( p, uTruth, Lits, iLit );
if ( uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA || if ( uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC || uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 || uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00 ) 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])) || 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[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) ||
(Lits[2] > 1 && (Lits[2] == Lits[3])) ) (Lits[2] > 1 && (Lits[2] == Lits[3])) )
p->nDupNum++; p->nDupNum++;
}
} }
else else
...@@ -1324,21 +1346,21 @@ clkOther += clock() - clk2; ...@@ -1324,21 +1346,21 @@ clkOther += clock() - clk2;
{ {
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
printf( "Var =%8.0f. ", (double)p->nSatVars ); printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts ); printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// ABC_PRT( "Time", clock() - clk ); // ABC_PRT( "Time", clock() - clk );
printf( "%4.0f Mb", 4.25*(f+1)*p->nObjNums /(1<<20) ); 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( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); 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( "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 ); // 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( "S =%6d. ", p->nBufNum );
// printf( "Dups = %6d. ", p->nDupNum ); printf( "D =%6d. ", p->nDupNum );
// printf( "\n" ); printf( "\n" );
fflush( stdout ); fflush( stdout );
} }
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
...@@ -1387,7 +1409,7 @@ clkOther += clock() - clk2; ...@@ -1387,7 +1409,7 @@ clkOther += clock() - clk2;
fFirst = 0; fFirst = 0;
// printf( "Outputs of frames up to %d are trivially UNSAT.\n", f ); // 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( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
...@@ -1397,12 +1419,12 @@ clkOther += clock() - clk2; ...@@ -1397,12 +1419,12 @@ clkOther += clock() - clk2;
printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) ); 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( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); 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( "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 ); // 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( "Simples = %6d. ", p->nBufNum );
// printf( "Dups = %6d. ", p->nDupNum ); printf( "Dups = %6d. ", p->nDupNum );
// printf( "\n" ); printf( "\n" );
fflush( stdout ); fflush( stdout );
} }
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment