diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-22 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-22 08:01:00 -0700 |
commit | 28467823812f63a40f9a322b1fefc7decce4b766 (patch) | |
tree | 8e7d9849119d106ebafd58e02e640338ffddacf3 /src/aig/fra/fraSim.c | |
parent | c8a25de8e411409b60f3677f70eab0860070b462 (diff) | |
download | abc-28467823812f63a40f9a322b1fefc7decce4b766.tar.gz abc-28467823812f63a40f9a322b1fefc7decce4b766.tar.bz2 abc-28467823812f63a40f9a322b1fefc7decce4b766.zip |
Version abc70822
Diffstat (limited to 'src/aig/fra/fraSim.c')
-rw-r--r-- | src/aig/fra/fraSim.c | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index b31fcb7f..3463ee0d 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -200,6 +200,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) Aig_InfoSetBit( p->pPatWords, i ); /* + if ( p->vCex ) + { + Vec_IntClear( p->vCex ); + for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + } +*/ + +/* printf( "Pattern: " ); Aig_ManForEachPi( p->pManFraig, pObj, i ) printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) ); @@ -601,7 +612,7 @@ clk = clock(); if ( p->pCla->vImps ) nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); p->timeRef += clock() - clk; - if ( nChanges < 1 ) + if ( !p->pPars->nFramesK && nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); // assert( nChanges >= 1 ); //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); |