Skip to content

A
abc
Commit 49267fd3 by Alan Mishchenko
Options

Structural reparametrization.

parent aeb7f7ea
Showing with 235 additions and 81 deletions
src/base/abci/abc.c
......@@ -26737,10 +26737,10 @@ usage:
int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, nCutMax = 6;
int fUseOldAlgo = 0;
int fVerbose = 0;
int fVeryVerbose = 0;
int c, nCutMax = 16;
int fUseOldAlgo = 0;
int fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cavwh" ) ) != EOF )
{
......
src/proof/abs/absRpm.c
......@@ -19,7 +19,6 @@
***********************************************************************/
#include "abs.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
......@@ -30,7 +29,7 @@ ABC_NAMESPACE_IMPL_START
static inline int Gia_ObjDom( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vDoms, Gia_ObjId(p, pObj)); }
static inline void Gia_ObjSetDom( Gia_Man_t * p, Gia_Obj_t * pObj, int d ) { Vec_IntWriteEntry(p->vDoms, Gia_ObjId(p, pObj), d); }
static int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp );
static int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp );
static int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
static int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
......@@ -140,7 +139,7 @@ void Gia_ManTestDoms2( Gia_Man_t * p )
}
assert( Gia_ObjIsAnd(pDom) );
Abs_GiaObjDeref_rec( p, pDom );
Abs_ManSupport( p, pDom, vNodes );
Abs_ManSupport2( p, pDom, vNodes );
Abs_GiaObjRef_rec( p, pDom );
if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) == -1 )
......@@ -174,6 +173,8 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
{
if ( !pObj->fMark1 )
continue;
if ( p->pRefs && Gia_ObjRefs(p, pObj) == 0 )
continue;
iDom = Gia_ObjDom(p, pObj);
if ( iDom == -1 )
continue;
......@@ -221,6 +222,30 @@ void Gia_ManTestDoms( Gia_Man_t * p )
/**Function*************************************************************
Synopsis [Counts flops without fanout.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCountFanoutlessFlops( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
int Counter = 0;
Gia_ManCreateRefs( p );
Gia_ManForEachRo( p, pObj, i )
if ( Gia_ObjRefs(p, pObj) == 0 )
Counter++;
printf( "Fanoutless flops = %d.\n", Counter );
ABC_FREE( p->pRefs );
}
/**Function*************************************************************
Synopsis []
Description []
......@@ -263,6 +288,83 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Abs_GiaObjDeref_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Abs_GiaObjDeref_rec( p, pFanin );
return Counter + 1;
}
int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Abs_GiaObjRef_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Abs_GiaObjRef_rec( p, pFanin );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Returns the number of nodes with zero refs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
{
Gia_Obj_t * pObj;
int nSize = Vec_IntSize(vSupp);
int i, RetValue;
Gia_ManForEachObjVec( vSupp, p, pObj, i )
if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves
{
assert( pObj->fMark1 );
Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
}
RetValue = Vec_IntSize(vSupp) - nSize;
Gia_ManForEachObjVec( vSupp, p, pObj, i )
if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves
Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
assert( Vec_IntSize(vSupp) == 2 * nSize );
memmove( Vec_IntArray(vSupp), Vec_IntArray(vSupp) + nSize, sizeof(int) * nSize );
Vec_IntShrink( vSupp, nSize );
return RetValue;
}
/**Function*************************************************************
Synopsis [Computes support in terms of PIs and flops.]
Description []
......@@ -272,7 +374,7 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds )
SeeAlso []
***********************************************************************/
void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
void Abs_ManSupport1_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
......@@ -283,15 +385,15 @@ void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
return;
}
assert( Gia_ObjIsAnd(pObj) );
Abs_ManSupport2_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport2_rec( p, Gia_ObjFanin1(pObj), vSupp );
Abs_ManSupport1_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport1_rec( p, Gia_ObjFanin1(pObj), vSupp );
}
int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
int Abs_ManSupport1( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
{
assert( Gia_ObjIsAnd(pObj) );
Vec_IntClear( vSupp );
Gia_ManIncrementTravId( p );
Abs_ManSupport2_rec( p, pObj, vSupp );
Abs_ManSupport1_rec( p, pObj, vSupp );
return Vec_IntSize(vSupp);
}
......@@ -306,7 +408,7 @@ int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
SeeAlso []
***********************************************************************/
void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
......@@ -317,23 +419,23 @@ void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
return;
}
assert( Gia_ObjIsAnd(pObj) );
Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
Abs_ManSupport2_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport2_rec( p, Gia_ObjFanin1(pObj), vSupp );
}
int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
{
assert( Gia_ObjIsAnd(pObj) );
Vec_IntClear( vSupp );
Gia_ManIncrementTravId( p );
Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
Abs_ManSupport2_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport2_rec( p, Gia_ObjFanin1(pObj), vSupp );
Gia_ObjSetTravIdCurrent(p, pObj);
return Vec_IntSize(vSupp);
}
/**Function*************************************************************
Synopsis []
Synopsis [Computes support of the extended MFFC.]
Description []
......@@ -342,42 +444,64 @@ int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
SeeAlso []
***********************************************************************/
int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
int Abs_ManSupport3( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Abs_GiaObjDeref_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Abs_GiaObjDeref_rec( p, pFanin );
return Counter + 1;
}
int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Abs_GiaObjRef_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Abs_GiaObjRef_rec( p, pFanin );
return Counter + 1;
Gia_Obj_t * pTemp, * pFan0, * pFan1;
int i, nSize0;
// collect MFFC
Abs_ManSupport2( p, pObj, vSupp );
// move dominated to the front
nSize0 = Abs_GiaSortNodes( p, vSupp );
assert( nSize0 > 0 );
// consider remaining nodes
while ( 1 )
{
int fChanges = 0;
Gia_ManForEachObjVec( vSupp, p, pTemp, i )
{
if ( i < nSize0 )
continue;
if ( !Gia_ObjIsAnd(pTemp) )
continue;
assert( !pTemp->fMark1 );
assert( Gia_ObjRefs(p, pTemp) > 0 );
pFan0 = Gia_ObjFanin0(pTemp);
pFan1 = Gia_ObjFanin1(pTemp);
if ( Gia_ObjIsTravIdCurrent(p, pFan0) && Gia_ObjIsTravIdCurrent(p, pFan1) )
{
Vec_IntRemove( vSupp, Gia_ObjId(p, pTemp) );
fChanges = 1;
break;
}
if ( Gia_ObjIsTravIdCurrent(p, pFan0) )
{
Vec_IntRemove( vSupp, Gia_ObjId(p, pTemp) );
Vec_IntPush( vSupp, Gia_ObjId(p, pFan1) );
assert( !Gia_ObjIsTravIdCurrent(p, pFan1) );
Gia_ObjSetTravIdCurrent(p, pFan1);
fChanges = 1;
break;
}
if ( Gia_ObjIsTravIdCurrent(p, pFan1) )
{
Vec_IntRemove( vSupp, Gia_ObjId(p, pTemp) );
Vec_IntPush( vSupp, Gia_ObjId(p, pFan0) );
assert( !Gia_ObjIsTravIdCurrent(p, pFan0) );
Gia_ObjSetTravIdCurrent(p, pFan0);
fChanges = 1;
break;
}
}
if ( !fChanges )
break;
}
return Vec_IntSize(vSupp);
}
/**Function*************************************************************
Synopsis [Returns the number of nodes with zero refs.]
Synopsis []
Description []
......@@ -386,25 +510,27 @@ int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
SeeAlso []
***********************************************************************/
int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
int Abs_GiaCofPrint( word * pTruth, int nSize, int nSize0, int Res )
{
Gia_Obj_t * pObj;
int nSize = Vec_IntSize(vSupp);
int i, RetValue;
Gia_ManForEachObjVec( vSupp, p, pObj, i )
if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves
int i, Bit;
int nBits = (1 << nSize);
int nStep = (1 << nSize0);
int Mark[2] = {1,1};
for ( i = 0; i < nBits; i++ )
{
if ( i % nStep == 0 )
{
assert( pObj->fMark1 );
Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
printf( " " );
assert( Res || (Mark[0] && Mark[1]) );
Mark[0] = Mark[1] = 0;
}
RetValue = Vec_IntSize(vSupp) - nSize;
Gia_ManForEachObjVec( vSupp, p, pObj, i )
if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves
Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
assert( Vec_IntSize(vSupp) == 2 * nSize );
memmove( Vec_IntArray(vSupp), Vec_IntArray(vSupp) + nSize, sizeof(int) * nSize );
Vec_IntShrink( vSupp, nSize );
return RetValue;
Bit = Abc_InfoHasBit((unsigned *)pTruth, i);
Mark[Bit] = 1;
printf( "%d", Bit );
}
printf( "\n" );
assert( Res || (Mark[0] && Mark[1]) );
return 1;
}
/**Function*************************************************************
......@@ -412,7 +538,7 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
Synopsis [Returns 1 if truth table has no const cofactors.]
Description [The cofactoring variables are the (nSize-nSize0)
most significant vars. Each factors depends on nSize0 vars.]
most significant vars. Each cofactor depends on nSize0 vars.]
SideEffects []
......@@ -421,7 +547,7 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
***********************************************************************/
int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 )
{
char * pStr = (char *)pTruth;
unsigned char * pStr = (unsigned char *)pTruth;
int nStr = (nSize >= 3 ? (1 << (nSize - 3)) : 1);
int i, k, nSteps;
assert( nSize0 > 0 && nSize0 <= nSize );
......@@ -472,10 +598,11 @@ int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 )
***********************************************************************/
void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose )
{
Vec_Int_t * vSupp, * vPis, * vAnds, * vDoms;
Vec_Int_t * vPis, * vAnds, * vDoms;
Vec_Int_t * vSupp, * vSupp1, * vSupp2;
Gia_Obj_t * pObj;
word * pTruth;
int Iter, i, nSize0;
int Iter, i, nSize0, nNodes;
int fHasConst, fChanges = 1;
Gia_ManCreateRefs( p );
Gia_ManCleanMark1( p );
......@@ -483,7 +610,8 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
pObj->fMark1 = 1;
vPis = Vec_IntAlloc( 100 );
vAnds = Vec_IntAlloc( 100 );
vSupp = Vec_IntAlloc( 100 );
vSupp1 = Vec_IntAlloc( 100 );
vSupp2 = Vec_IntAlloc( 100 );
for ( Iter = 0; fChanges; Iter++ )
{
fChanges = 0;
......@@ -493,9 +621,9 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
{
Gia_ManCountPisNodes( p, vPis, vAnds );
printf( "Iter %3d : ", Iter );
printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) );
printf( "PI = %5d (%6.2f %%) ", Vec_IntSize(vPis), 100.0 * Vec_IntSize(vPis) / Gia_ManPiNum(p) );
printf( "And = %6d (%6.2f %%) ", Vec_IntSize(vAnds), 100.0 * Vec_IntSize(vAnds) / Gia_ManAndNum(p) );
printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) );
printf( "\n" );
}
// pObj = Gia_ObjFanin0( Gia_ManPo(p, 1) );
......@@ -504,13 +632,35 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
assert( !pObj->fMark1 );
assert( Gia_ObjRefs( p, pObj ) > 0 );
// dereference root node
Abs_GiaObjDeref_rec( p, pObj );
// check support size
if ( Abs_ManSupport(p, pObj, vSupp) > nCutMax )
nNodes = Abs_GiaObjDeref_rec( p, pObj );
/*
// compute support of full cone
if ( Abs_ManSupport1(p, pObj, vSupp1) > nCutMax )
// if ( 1 )
{
// check support of MFFC
if ( Abs_ManSupport2(p, pObj, vSupp2) > nCutMax )
// if ( 1 )
{
Abs_GiaObjRef_rec( p, pObj );
continue;
}
vSupp = vSupp2;
// printf( "-" );
}
else
{
vSupp = vSupp1;
// printf( "+" );
}
*/
if ( Abs_ManSupport2(p, pObj, vSupp2) > nCutMax )
{
Abs_GiaObjRef_rec( p, pObj );
continue;
}
vSupp = vSupp2;
// order nodes by their ref counts
nSize0 = Abs_GiaSortNodes( p, vSupp );
assert( nSize0 > 0 && nSize0 <= nCutMax );
......@@ -519,8 +669,11 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
fHasConst = !Abs_GiaCheckTruth( pTruth, Vec_IntSize(vSupp), nSize0 );
if ( fVeryVerbose )
{
printf( "Node = %8d Supp = %2d Supp0 = %2d Res = %4s ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0, fHasConst? "no":"yes" );
Extra_PrintHex( stdout, (unsigned *)pTruth, Vec_IntSize(vSupp) ); printf( "\n" );
printf( "Nodes =%3d ", nNodes );
printf( "Size =%3d ", Vec_IntSize(vSupp) );
printf( "Size0 =%3d ", nSize0 );
printf( "%3s", fHasConst ? "yes" : "no" );
Abs_GiaCofPrint( pTruth, Vec_IntSize(vSupp), nSize0, fHasConst );
}
if ( fHasConst )
{
......@@ -532,23 +685,24 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
fChanges = 1;
}
Vec_IntFree( vDoms );
// break;
}
// count the number of PIs and internal nodes
if ( fVeryVerbose )
{
Gia_ManCountPisNodes( p, vPis, vAnds );
printf( "Iter %3d : ", Iter );
printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) );
printf( "PI = %5d (%6.2f %%) ", Vec_IntSize(vPis), 100.0 * Vec_IntSize(vPis) / Gia_ManPiNum(p) );
printf( "And = %6d (%6.2f %%) ", Vec_IntSize(vAnds), 100.0 * Vec_IntSize(vAnds) / Gia_ManAndNum(p) );
// printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) );
printf( "\n" );
}
// cleanup
Vec_IntFree( vPis );
Vec_IntFree( vAnds );
Vec_IntFree( vSupp );
Vec_IntFree( vSupp1 );
Vec_IntFree( vSupp2 );
// Gia_ManCleanMark1( p ); // this will erase markings
ABC_FREE( p->pRefs );
// Gia_ManCleanMark1( p ); // temp
}
/**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment