diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-15 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-15 08:01:00 -0700 |
| commit | 74ff01bfb54e9f0a68ac88b827521a422269a144 (patch) | |
| tree | 240c07b87e355dba9caa1e6187d6673b92996eac /src/aig/saig | |
| parent | 37b6c727f1276d9d97a79a8f40271aee446a4ba4 (diff) | |
| download | abc-74ff01bfb54e9f0a68ac88b827521a422269a144.tar.gz abc-74ff01bfb54e9f0a68ac88b827521a422269a144.tar.bz2 abc-74ff01bfb54e9f0a68ac88b827521a422269a144.zip | |
Version abc80515
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigInter.c | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index f6a42c8b..952094ce 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -182,7 +182,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; int status, clk, Lit, i, RetValue = 1; - *piFrame = -1; // derive the timeframes clk = clock(); if ( nSizeMax > 0 ) @@ -192,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else pFrames = Saig_ManFramesBmc( pAig, nFrames ); + *piFrame = nFrames; if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index 3adcc568..889e6298 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -178,6 +178,7 @@ Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) { pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); +// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); Aig_ObjCreatePo( pNew, pObj ); } Aig_ManCleanup( pNew ); @@ -566,10 +567,10 @@ p->timeCnf += clock() - clk; // iterate the interpolation procedure for ( i = 0; ; i++ ) { - if ( p->nFrames + i >= 100 ) + if ( p->nFrames + i >= 75 ) { if ( fVerbose ) - printf( "Reached limit (%d) on the number of timeframes.\n", 100 ); + printf( "Reached limit (%d) on the number of timeframes.\n", 75 ); p->timeTotal = clock() - clkTotal; Saig_ManagerFree( p ); return -1; |