luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

New command 'testnpn' to compare semi-canonical forms.

This commit is contained in:
Alan Mishchenko 2012-08-08 01:41:42 -07:00
parent c4b4ac7052
commit 094bdc0572
2 changed files with 32 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/aig/gia/giaAbsGla2.c
View File

@ -396,7 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Vec_IntPush( p->vAbs, 0 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
// p->pRf2 = Rf2_ManStart( pGia );
p->pRf2 = Rf2_ManStart( pGia );
// SAT solver and variables
p->vId2Lit = Vec_PtrAlloc( 1000 );
// temporaries
@ -459,7 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
Rnm_ManStop( p->pRnm, p->pPars->fVerbose );
// Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
ABC_FREE( p->pTable );
ABC_FREE( p->pSopSizes );
ABC_FREE( p->pSops[1] );
@ -1216,7 +1216,7 @@ Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
}
return pCex;
}
}
Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
{
Abc_Cex_t * pCex;
@ -1224,8 +1224,11 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
Gia_Obj_t * pObj;
int i;
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
// printf( "Refinement %d\n", Vec_IntSize(vVec) );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
{

32
src/aig/gia/giaAbsRef2.c
View File

@ -385,8 +385,9 @@ void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFani
return;
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
assert( pObj->fPhase );
pObj = Gia_ObjRoToRi(p->pGia, pObj);
Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth, RootId, 0 );
Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 );
}
else if ( Gia_ObjIsAnd(pObj) )
{
@ -397,9 +398,10 @@ void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFani
}
void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
{
Vec_Int_t * vUsed;
Vec_Int_t * vVec;
Gia_Obj_t * pObj;
int i;
int i, k, Entry;
// mark PPIs
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
{
@ -416,24 +418,40 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
Gia_ManIncrementTravId( p->pGia );
Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 );
}
vUsed = Vec_IntStart( Vec_IntSize(p->vMap) );
// evaluate collected
printf( "\nMap: " );
printf( "\nMap (%d): ", Vec_IntSize(p->vMap) );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
{
vVec = Rf2_ObjVec( p, pObj );
printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
if ( Vec_IntSize(vVec) > 1 )
printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
Vec_IntForEachEntryStart( vVec, Entry, k, 1 )
Vec_IntAddToEntry( vUsed, Entry, 1 );
Vec_IntClear( vVec );
}
printf( "\n" );
// evaluate internal
printf( "Int: " );
printf( "Int (%d): ", Vec_IntSize(p->vFanins) );
Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
{
vVec = Rf2_ObjVec( p, pObj );
printf( "%d=%d ", i, Vec_IntSize(vVec) );
if ( Vec_IntSize(vVec) > 1 )
printf( "%d=%d ", i, Vec_IntSize(vVec) );
if ( Vec_IntSize(vVec) > 1 )
Vec_IntForEachEntry( vVec, Entry, k )
Vec_IntAddToEntry( vUsed, Entry, 1 );
Vec_IntClear( vVec );
}
printf( "\n" );
// evaluate PPIs
Vec_IntForEachEntry( vUsed, Entry, k )
printf( "%d ", Entry );
printf( "\n" );
Vec_IntFree( vUsed );
}
@ -461,7 +479,7 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
// collects used objects
Rf2_ManCollect( p );
// collect reconvergence points
Rf2_ManGatherFanins( p, 1 );
Rf2_ManGatherFanins( p, 2 );
// propagate justification IDs
// select the result