diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-08 10:24:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-08 10:24:00 -0700 |
| commit | 68566713da1f5eaf712caf06b3750d2e6f92ee43 (patch) | |
| tree | 3f379b7c73e1c5574cbea235a4bbe20ece593882 /src | |
| parent | e7e21b00fe979b5a8f91341c83caa21809e8b105 (diff) | |
| download | abc-68566713da1f5eaf712caf06b3750d2e6f92ee43.tar.gz abc-68566713da1f5eaf712caf06b3750d2e6f92ee43.tar.bz2 abc-68566713da1f5eaf712caf06b3750d2e6f92ee43.zip | |
Bug fix in the sweeper.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 6 | ||||
| -rw-r--r-- | src/proof/ssc/sscCore.c | 4 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 1b1abece..5ff05a37 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -959,7 +959,7 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * else assert( Gia_ManPiNum(pDst) == Gia_ManPiNum(pSrc) ); Gia_ManForEachPi( pSrc, pObj, i ) - pObj->Value = Gia_SweeperProbeLit( pDst, vProbes ? Vec_IntEntry(vProbes, i) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i)) ); + pObj->Value = vProbes ? Gia_SweeperProbeLit(pDst, Vec_IntEntry(vProbes, i)) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i)); Gia_ManForEachAnd( pSrc, pObj, i ) pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) ); @@ -996,6 +996,9 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); Gia_ManSetPhase( pGiaOuts ); + // if there is no conditions, define constant true constrain (constant 0 output) + if ( Gia_ManPoNum(pGiaCond) == 0 ) + Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() ); // perform sweeping under constraints pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars ); Gia_ManStop( pGiaCond ); @@ -1083,6 +1086,7 @@ Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int return pGia; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index 1a57a47c..1ba5cf04 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -216,7 +216,7 @@ int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj ) Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) { Ssc_Man_t * p; - Gia_Man_t * pResult; + Gia_Man_t * pResult, * pTemp; Gia_Obj_t * pObj, * pRepr; clock_t clk, clkTotal = clock(); int i, fCompl, nRefined, status; @@ -341,6 +341,8 @@ p->timeSimSat += clock() - clk; ABC_FREE( pAig->pNexts ); pResult = Gia_ManDup( pAig ); } + pResult = Gia_ManCleanup( pTemp = pResult ); + Gia_ManStop( pTemp ); p->timeTotal = clock() - clkTotal; if ( pPars->fVerbose ) Ssc_ManPrintStats( p ); |