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

%pdra: isolated the procedure for checking comb. unsat

This commit is contained in:
Yen-Sheng Ho 2017-03-18 14:23:09 -07:00
parent eff11d95d2
commit 7713e94a1a
1 changed files with 49 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

86
src/base/wlc/wlcAbs.c
View File

@ -1251,6 +1251,54 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs )
return pAig;
}
int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig )
{
Pdr_Man_t * pPdr;
abctime clk;
int RetValue = -1;
if ( Aig_ManAndNum( pAig ) <= 20000 )
{
Aig_Man_t * pAigScorr;
Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
int nAnds;
clk = Abc_Clock();
Ssw_ManSetDefaultParams( pScorrPars );
pScorrPars->fStopWhenGone = 1;
pScorrPars->nFramesK = 1;
pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
assert ( pAigScorr );
nAnds = Aig_ManAndNum( pAigScorr);
Aig_ManStop( pAigScorr );
if ( nAnds == 0 )
{
if ( pWla->pPars->fVerbose )
Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk );
return 1;
}
else if ( pWla->pPars->fVerbose )
{
Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
clk = Abc_Clock();
pWla->pPdrPars->fVerbose = 0;
pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL );
RetValue = IPdr_ManCheckCombUnsat( pPdr );
Pdr_ManStop( pPdr );
pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose;
pWla->tPdr += Abc_Clock() - clk;
return RetValue;
}
int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
{
abctime clk;
@ -1259,45 +1307,9 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat )
{
if ( Aig_ManAndNum( pAig ) <= 20000 )
{
Aig_Man_t * pAigScorr;
Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
int nAnds;
clk = Abc_Clock();
Ssw_ManSetDefaultParams( pScorrPars );
pScorrPars->fStopWhenGone = 1;
pScorrPars->nFramesK = 1;
pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
assert ( pAigScorr );
nAnds = Aig_ManAndNum( pAigScorr);
Aig_ManStop( pAigScorr );
if ( nAnds == 0 )
{
if ( pWla->pPars->fVerbose )
Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk );
return 1;
}
else if ( pWla->pPars->fVerbose )
{
Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
clk = Abc_Clock();
pWla->pPdrPars->fVerbose = 0;
pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL );
RetValue = IPdr_ManCheckCombUnsat( pPdr );
Pdr_ManStop( pPdr );
pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose;
pWla->tPdr += Abc_Clock() - clk;
RetValue = Wla_ManCheckCombUnsat( pWla, pAig );
if ( RetValue == 1 )
{
if ( pWla->pPars->fVerbose )