luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

SAT variable profiling.

This commit is contained in:
Alan Mishchenko 2013-05-18 11:03:32 -07:00
parent 0328488bdf
commit f9da2c790f
5 changed files with 53 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/base/abci/abc.c
View File

@ -21246,7 +21246,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJILaxdruvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLaxdruvzh" ) ) != EOF )
{
switch ( c )
{
@ -21349,6 +21349,39 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nPisAbstract < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedStart < 0 )
goto usage;
break;
case 'Q':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedDelta = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedDelta < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedPerce = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedPerce < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
@ -21433,7 +21466,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJI num] [-L file] [-axduvzh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-L file] [-axduvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@ -21444,6 +21477,9 @@ usage:
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );

3
src/sat/bmc/bmc.h
View File

@ -56,6 +56,9 @@ struct Saig_ParBmc_t_
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions
int nLearnedStart; // starting learned clause limit
int nLearnedDelta; // delta of learned clause limit
int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
int iFrame; // explored up to this frame

10
src/sat/bmc/bmcBmc3.c
View File

@ -1314,6 +1314,9 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->nPisAbstract = 0; // the number of PIs to abstract
p->fSolveAll = 0; // stops on the first SAT instance
p->fDropSatOuts = 0; // replace sat outputs by constant 0
p->nLearnedStart = 10000; // starting learned clause limit
p->nLearnedDelta = 2000; // delta of learned clause limit
p->nLearnedPerce = 80; // ratio of learned clause limit
p->fVerbose = 0; // verbose
p->fNotVerbose = 0; // skip line-by-line print-out
p->iFrame = -1; // explored up to this frame
@ -1404,6 +1407,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
p->pPars = pPars;
p->pSat->nLearntStart = p->pPars->nLearnedStart;
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
if ( pPars->fVerbose )
{
printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n",
@ -1636,9 +1642,9 @@ nTimeUndec += clock() - clk2;
}
printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Var2 =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Cnf =%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( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
if ( pPars->fSolveAll )

4
src/sat/bsat/satClause.h
View File

@ -35,8 +35,8 @@ ABC_NAMESPACE_HEADER_START
//#define LEARNT_MAX_START_DEFAULT 0
#define LEARNT_MAX_START_DEFAULT 10000
#define LEARNT_MAX_INCRE_DEFAULT 2000
#define LEARNT_MAX_RATIO_DEFAULT 80
#define LEARNT_MAX_INCRE_DEFAULT 1000
#define LEARNT_MAX_RATIO_DEFAULT 50
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///

4
src/sat/bsat/satSolver.c
View File

@ -1039,7 +1039,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
#endif
s->pFreqs = ABC_REALLOC(char, s->tags, s->cap);
s->pFreqs = ABC_REALLOC(char, s->pFreqs, s->cap);
if ( s->factors )
s->factors = ABC_REALLOC(double, s->factors, s->cap);
@ -1331,7 +1331,7 @@ void sat_solver_reducedb(sat_solver* s)
// report the results
TimeTotal += clock() - clk;
// if ( s->fVerbose )
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );