diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-03-13 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-03-13 08:01:00 -0700 |
| commit | 81b51657f5c502e45418630614fd56e5e1506230 (patch) | |
| tree | 4fcda87840fb9cca09ac3b31b13aa73abce29a08 /src/aig/saig/saigBmc2.c | |
| parent | 243cb29e561d9ae4808f9ba27f980ea64a466881 (diff) | |
| download | abc-81b51657f5c502e45418630614fd56e5e1506230.tar.gz abc-81b51657f5c502e45418630614fd56e5e1506230.tar.bz2 abc-81b51657f5c502e45418630614fd56e5e1506230.zip | |
Version abc90313
Diffstat (limited to 'src/aig/saig/saigBmc2.c')
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 8ba02528..f8799e38 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -173,16 +173,24 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ) { + extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ); sat_solver * pSat; Cnf_Dat_t * pCnf; Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; int status, clk, Lit, i, RetValue = 1; + // derive the timeframes clk = clock(); - if ( nSizeMax > 0 ) + if ( nCofFanLit ) + { + pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit ); + if ( pFrames == NULL ) + return -1; + } + else if ( nSizeMax > 0 ) { pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); |