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 | |
parent | 243cb29e561d9ae4808f9ba27f980ea64a466881 (diff) | |
download | abc-81b51657f5c502e45418630614fd56e5e1506230.tar.gz abc-81b51657f5c502e45418630614fd56e5e1506230.tar.bz2 abc-81b51657f5c502e45418630614fd56e5e1506230.zip |
Version abc90313
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigBmc2.c | 12 |
2 files changed, 11 insertions, 3 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 3db3e396..f11345eb 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -92,7 +92,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { /*=== sswAbs.c ==========================================================*/ extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ); /*=== saigBmc.c ==========================================================*/ -extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); 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); |