Commit 8b0302cd by Alan Mishchenko

Changing default conflict limits in bmc2 and bmc3 to be 0 (no limit).

parent 3c43fbba
...@@ -1221,7 +1221,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) ...@@ -1221,7 +1221,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
memset( p, 0, sizeof(Saig_ParBmc_t) ); memset( p, 0, sizeof(Saig_ParBmc_t) );
p->nStart = 0; // maximum number of timeframes p->nStart = 0; // maximum number of timeframes
p->nFramesMax = 0; // maximum number of timeframes p->nFramesMax = 0; // maximum number of timeframes
p->nConfLimit = 2000; // maximum number of conflicts at a node p->nConfLimit = 0; // maximum number of conflicts at a node
p->nConfLimitJump = 0; // maximum number of conflicts after jumping p->nConfLimitJump = 0; // maximum number of conflicts after jumping
p->nFramesJump = 0; // the number of tiemframes to jump p->nFramesJump = 0; // the number of tiemframes to jump
p->nTimeOut = 0; // approximate timeout in seconds p->nTimeOut = 0; // approximate timeout in seconds
...@@ -1260,8 +1260,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1260,8 +1260,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n", printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) ); Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) );
printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", printf( "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",
pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll ); pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
} }
pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY; pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
// set runtime limit // set runtime limit
......
...@@ -19629,13 +19629,13 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19629,13 +19629,13 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
nStart = 0; nStart = 0;
nFrames = 0; nFrames = 0;
nSizeMax = 200000; nSizeMax = 200000;
nBTLimit = 2000; nBTLimit = 0;
nBTLimitAll = 2000000; nBTLimitAll = 0;
nNodeDelta = 2000; nNodeDelta = 2000;
nTimeOut = 0; nTimeOut = 0;
fRewrite = 0; fRewrite = 0;
fNewAlgo = 0; fNewAlgo = 0;
fOrDecomp = 1; fOrDecomp = 0;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDLruvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDLruvh" ) ) != EOF )
......
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