diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-04 21:14:47 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-04 21:14:47 -0700 |
| commit | 2071d9a732d0e0bf58a47466cf3570e9fe26fa6c (patch) | |
| tree | 34c45ad6384a22eb8ec0a5fec5a9ee095788502f /src | |
| parent | 8e12b60b66c74b5e706fa931d68729986ddc315f (diff) | |
| download | abc-2071d9a732d0e0bf58a47466cf3570e9fe26fa6c.tar.gz abc-2071d9a732d0e0bf58a47466cf3570e9fe26fa6c.tar.bz2 abc-2071d9a732d0e0bf58a47466cf3570e9fe26fa6c.zip | |
Enabling additinal printouts.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 2c6c5b18..7cd6abb4 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1216,6 +1216,68 @@ Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis ) } return pCex; } +void Ga2_ManRefinePrint( Ga2_Man_t * p, Vec_Int_t * vVec ) +{ + Gia_Obj_t * pObj, * pFanin; + int i, k; + printf( "\n Unsat core: \n" ); + Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) + { + Vec_Int_t * vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + printf( "%12d : ", i ); + printf( "Obj =%6d ", Gia_ObjId(p->pGia, pObj) ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + printf( "ff " ); + else + printf( " " ); + if ( Ga2_ObjIsAbs0(p, pObj) ) + printf( "a " ); + else if ( Ga2_ObjIsLeaf0(p, pObj) ) + printf( "l " ); + else + printf( " " ); + printf( "Fanins: " ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + { + printf( "%6d ", Gia_ObjId(p->pGia, pFanin) ); + if ( Gia_ObjIsRo(p->pGia, pFanin) ) + printf( "ff " ); + else + printf( " " ); + if ( Ga2_ObjIsAbs0(p, pFanin) ) + printf( "a " ); + else if ( Ga2_ObjIsLeaf0(p, pFanin) ) + printf( "l " ); + else + printf( " " ); + } + printf( "\n" ); + } +} +void Ga2_ManRefinePrintPPis( Ga2_Man_t * p ) +{ + Vec_Int_t * vVec = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) + { + if ( !i ) continue; + if ( Ga2_ObjIsAbs(p, pObj) ) + continue; + assert( pObj->fPhase ); + assert( Ga2_ObjIsLeaf(p, pObj) ); + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) ); + Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) ); + } + printf( " Current PPIs (%d): ", Vec_IntSize(vVec) ); + Vec_IntSort( vVec, 1 ); + Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) + printf( "%d ", Gia_ObjId(p->pGia, pObj) ); + printf( "\n" ); + Vec_IntFree( vVec ); +} + + Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) { Abc_Cex_t * pCex; @@ -1536,6 +1598,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) if ( c == 0 ) { +// Ga2_ManRefinePrintPPis( p ); // create bookmark to be used for rollback assert( nVarsOld == p->pSat->size ); sat_solver2_bookmark( p->pSat ); @@ -1627,6 +1690,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } Ga2_ManAddToAbs( p, vCore ); +// Ga2_ManRefinePrint( p, vCore ); Vec_IntFree( vCore ); break; } |