From c1e54b8b761b38f0c0fc715bce44dbd0b97fe55a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 19 Mar 2014 22:26:52 -0700 Subject: Experiments with recent ideas. --- src/sat/bmc/bmcLilac.c | 7 +++---- src/sat/bmc/bmcTulip.c | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/sat/bmc/bmcLilac.c b/src/sat/bmc/bmcLilac.c index 1d41312b..c17668c5 100644 --- a/src/sat/bmc/bmcLilac.c +++ b/src/sat/bmc/bmcLilac.c @@ -219,13 +219,11 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int else Vec_IntPush( vMiters, -1 ); assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) ); - if ( fVerbose ) - printf( "Frame %4d : ", f ); if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 ) { if ( fVerbose ) - printf( "Trivial\n" ); - continue; + printf( "Reached a fixed point after %d frames. \n", f+1 ); + break; } // create new part pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); @@ -288,6 +286,7 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int } if ( fVerbose ) { + printf( "Frame %4d : ", f+1 ); printf( "Vars =%7d ", nSatVars ); printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c index 8c32d699..cce3becd 100644 --- a/src/sat/bmc/bmcTulip.c +++ b/src/sat/bmc/bmcTulip.c @@ -239,7 +239,7 @@ Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, Gia_ManForEachPi( pM, pObj, i ) if ( i == Gia_ManRegNum(p) ) break; - else if ( (Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) ) + else if ( (Vec_IntEntry(vLits, i) & 2) && Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) ) Vec_IntWriteEntry( vLits, i, (Vec_IntEntry(vLits, i) & 1) ); Vec_IntFree( vMap ); -- cgit v1.2.3