Skip to content

A
abc
Commit df3e23ae by Alan Mishchenko
Options

Enabled skipping random decisions in PBA, which are performed by default.

parent fa96b8d7
Showing with 24 additions and 9 deletions
src/aig/gia/giaAbs.c
......@@ -379,7 +379,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
***********************************************************************/
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
{
extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
Aig_Man_t * pAig;
......@@ -397,7 +397,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
vGateClasses = Aig_Gla1ManTest( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
Aig_ManStop( pAig );
// update the map
......@@ -419,7 +419,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
***********************************************************************/
int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
{
extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Aig_Man_t * pAig;
......@@ -440,7 +440,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
}
// perform abstraction
vGateClasses = Aig_Gla2ManTest( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
Aig_ManStop( pAig );
// update the BMC depth
......
src/aig/saig/saig.h
......@@ -68,6 +68,7 @@ struct Saig_ParBmc_t_
int fSolveAll; // does not stop at the first SAT output
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions
int fVerbose; // verbose
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
......
src/aig/saig/saigGlaCba.c
......@@ -676,7 +676,7 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
{
Vec_Int_t * vResult = NULL;
Aig_Gla1Man_t * p;
......
src/aig/saig/saigGlaPba.c
......@@ -553,7 +553,7 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
{
Aig_Gla2Man_t * p;
Vec_Int_t * vCore, * vResult;
......@@ -578,6 +578,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
Aig_Gla2ManStop( p );
return NULL;
}
sat_solver_set_random( p->pSat, fSkipRand );
p->timePre += Abc_Clock(1,0);
// set runtime limit
......
src/base/abci/abc.c
......@@ -29093,8 +29093,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 10; //pPars->nStart + 10;
pPars->nConfLimit = 0;
pPars->fSkipRand = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrvh" ) ) != EOF )
{
switch ( c )
{
......@@ -29142,6 +29143,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'r':
pPars->fSkipRand ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -29185,12 +29189,13 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-r : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......
src/sat/bsat/satSolver.c
......@@ -967,7 +967,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
int* levels = s->levels;
double var_decay = 0.95;
double clause_decay = 0.999;
double random_var_freq = 0.02;
double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
ABC_INT64_T conflictC = 0;
veci learnt_clause;
......
src/sat/bsat/satSolver.h
......@@ -175,6 +175,7 @@ struct sat_solver_t
Sat_MmStep_t * pMem;
int fSkipSimplify; // set to one to skip simplification of the clause database
int fNotUseRandom; // do not allow random decisions with a fixed probability
int * pGlobalVars; // for experiments with global vars during interpolation
// clause store
......@@ -228,6 +229,13 @@ static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
return nRuntimeLimit;
}
static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
{
int fNotUseRandomOld = s->fNotUseRandom;
s->fNotUseRandom = fNotUseRandom;
return fNotUseRandomOld;
}
ABC_NAMESPACE_HEADER_END
#endif
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