summaryrefslogtreecommitdiffstats
path: root/src/proof/abs
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-10-01 22:55:01 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-10-01 22:55:01 -0700
commit60ad1765ff847ba609500385e4a73c84e37ecdc1 (patch)
tree2c01bd81c2b92c7bac67f22aaf875ecf9fde2e11 /src/proof/abs
parenta287bcd2e21adb35409d1225bd20df920515af9b (diff)
downloadabc-60ad1765ff847ba609500385e4a73c84e37ecdc1.tar.gz
abc-60ad1765ff847ba609500385e4a73c84e37ecdc1.tar.bz2
abc-60ad1765ff847ba609500385e4a73c84e37ecdc1.zip
Structural reparametrization.
Diffstat (limited to 'src/proof/abs')
-rw-r--r--src/proof/abs/absRpm.c340
1 files changed, 312 insertions, 28 deletions
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c
index dbd3b628..7ef314ea 100644
--- a/src/proof/abs/absRpm.c
+++ b/src/proof/abs/absRpm.c
@@ -26,12 +26,190 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+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_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
+static int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis [Collects non-trivial internal dominators of the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
+{
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj;
+ int Level, LevelMax = 2;
+ int i, iDom, iDomNext;
+ vNodes = Vec_IntAlloc( 100 );
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ if ( !pObj->fMark0 )
+ continue;
+ iDom = Gia_ObjDom(p, pObj);
+ if ( iDom == Gia_ObjId(p, pObj) )
+ continue;
+ for ( Level = 0; Level < LevelMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Level++ )
+ {
+ Vec_IntPush( vNodes, iDom );
+ iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom) );
+ if ( iDomNext == iDom )
+ break;
+ iDom = iDomNext;
+ }
+ }
+ Vec_IntUniqify( vNodes );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes one-node dominators.]
+
+ Description [For each node, computes the closest one-node dominator,
+ which can be the node itself if the node has no other dominators.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManAddDom( Gia_Man_t * p, Gia_Obj_t * pObj, int iDom0 )
+{
+ int iDom1, iDomNext;
+ if ( Gia_ObjDom(p, pObj) == -1 )
+ {
+ Gia_ObjSetDom( p, pObj, iDom0 );
+ return;
+ }
+ iDom1 = Gia_ObjDom( p, pObj );
+ while ( 1 )
+ {
+ if ( iDom0 > iDom1 )
+ {
+ iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom1) );
+ if ( iDomNext == iDom1 )
+ break;
+ iDom1 = iDomNext;
+ continue;
+ }
+ if ( iDom1 > iDom0 )
+ {
+ iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom0) );
+ if ( iDomNext == iDom0 )
+ break;
+ iDom0 = iDomNext;
+ continue;
+ }
+ assert( iDom0 == iDom1 );
+ Gia_ObjSetDom( p, pObj, iDom0 );
+ return;
+ }
+ Gia_ObjSetDom( p, pObj, Gia_ObjId(p, pObj) );
+}
+void Gia_ManComputeDoms( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ if ( p->vDoms == NULL )
+ p->vDoms = Vec_IntAlloc( 0 );
+ Vec_IntFill( p->vDoms, Gia_ManObjNum(p), -1 );
+ Gia_ManForEachObjReverse( p, pObj, i )
+ {
+ if ( i == 0 || Gia_ObjIsCi(pObj) )
+ continue;
+ if ( pObj->fMark0 || (p->pRefs && Gia_ObjRefs(p, pObj) == 0) )
+ continue;
+ if ( Gia_ObjIsCo(pObj) )
+ {
+ Gia_ObjSetDom( p, pObj, i );
+ Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
+ continue;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
+ Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i );
+ }
+}
+void Gia_ManTestDoms2( Gia_Man_t * p )
+{
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj, * pDom;
+ clock_t clk = clock();
+ int i;
+ assert( p->vDoms == NULL );
+ Gia_ManComputeDoms( p );
+/*
+ Gia_ManForEachPi( p, pObj, i )
+ if ( Gia_ObjId(p, pObj) != Gia_ObjDom(p, pObj) )
+ printf( "PI =%6d Id =%8d. Dom =%8d.\n", i, Gia_ObjId(p, pObj), Gia_ObjDom(p, pObj) );
+*/
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
+ Gia_ManCleanMark0( p );
+ Gia_ManForEachPi( p, pObj, i )
+ pObj->fMark0 = 1;
+ vNodes = Vec_IntAlloc( 100 );
+ Gia_ManCreateRefs( p );
+ Gia_ManForEachPi( p, pObj, i )
+ {
+ if ( Gia_ObjId(p, pObj) == Gia_ObjDom(p, pObj) )
+ continue;
+
+ pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj));
+ if ( Gia_ObjIsCo(pDom) )
+ {
+ assert( Gia_ObjFanin0(pDom) == pObj );
+ continue;
+ }
+ assert( Gia_ObjIsAnd(pDom) );
+ Abs_GiaObjDeref_rec( p, pDom );
+ Abs_ManSupport( p, pDom, vNodes );
+ Abs_GiaObjRef_rec( p, pDom );
+
+ if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) == -1 )
+ printf( "FAILURE.\n" );
+// else
+// printf( "Success.\n" );
+ }
+ Vec_IntFree( vNodes );
+ Gia_ManCleanMark0( p );
+}
+
+void Gia_ManTestDoms( Gia_Man_t * p )
+{
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj;
+ int i;
+ assert( p->vDoms == NULL );
+ Gia_ManComputeDoms( p );
+ // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
+ Gia_ManCleanMark0( p );
+ Gia_ManForEachPi( p, pObj, i )
+ pObj->fMark0 = 1;
+ vNodes = Gia_ManCollectDoms( p );
+// Vec_IntPrint( vNodes );
+ printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) );
+ Vec_IntFree( vNodes );
+ Gia_ManCleanMark0( p );
+}
+
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -41,22 +219,22 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnPis, int * pnNodes )
+void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPis, Vec_Int_t * vAnds )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( pObj->fMark0 )
{
- (*pnPis)++;
+ Vec_IntPush( vPis, Gia_ObjId(p, pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
- Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes );
- Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), pnPis, pnNodes );
- (*pnNodes)++;
+ Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds );
+ Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), vPis, vAnds );
+ Vec_IntPush( vAnds, Gia_ObjId(p, pObj) );
}
-void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
+void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds )
{
Gia_Obj_t * pObj;
int i;
@@ -66,9 +244,10 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
// count PIs and internal nodes reachable from COs
- *pnPis = *pnNodes = 0;
+ Vec_IntClear( vPis );
+ Vec_IntClear( vAnds );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes );
+ Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds );
}
/**Function*************************************************************
@@ -82,7 +261,7 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
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;
@@ -93,6 +272,40 @@ void Abs_ManSupport_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 );
+}
+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_ManSupport2_rec( p, pObj, vSupp );
+ return Vec_IntSize(vSupp);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ if ( pObj->fMark0 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 )
+ {
+ Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
}
@@ -101,7 +314,8 @@ int Abs_ManSupport( 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, pObj, vSupp );
+ Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
+ Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
return Vec_IntSize(vSupp);
}
@@ -167,7 +381,10 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * 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->fMark0 );
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
@@ -296,16 +513,18 @@ word Abs_GiaComputeTruth( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Ve
***********************************************************************/
void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
{
- Vec_Int_t * vSupp;
+ Vec_Int_t * vSupp, * vPis, * vAnds;
Vec_Wrd_t * vTruths;
Gia_Obj_t * pObj;
word uTruth;
- int Iter, i, nPis, nNodes, nSize0;
+ int Iter, i, nSize0;
int fChanges = 1;
Gia_ManCreateRefs( p );
Gia_ManCleanMark0( p );
Gia_ManForEachPi( p, pObj, i )
pObj->fMark0 = 1;
+ vPis = Vec_IntAlloc( 100 );
+ vAnds = Vec_IntAlloc( 100 );
vSupp = Vec_IntAlloc( 100 );
vTruths = Vec_WrdAlloc( 100 );
for ( Iter = 0; fChanges; Iter++ )
@@ -313,16 +532,16 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
// count the number of PIs and internal nodes
if ( fVerbose )
{
- Gia_ManCountPisNodes( p, &nPis, &nNodes );
+ Gia_ManCountPisNodes( p, vPis, vAnds );
printf( "Iter %3d : ", Iter );
- printf( "PI = %5d ", nPis );
- printf( "And = %6d ", nNodes );
+ printf( "PI = %5d ", Vec_IntSize(vPis) );
+ printf( "And = %6d ", Vec_IntSize(vAnds) );
printf( "\n" );
}
fChanges = 0;
Gia_ManCleanMark1( p );
-// pObj = Gia_ObjFanin0( Gia_ManPo(p, 0) );
+// pObj = Gia_ObjFanin0( Gia_ManPo(p, 1) );
Gia_ManForEachAnd( p, pObj, i )
{
if ( pObj->fMark0 )
@@ -334,18 +553,22 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
pObj->fMark1 = 1;
continue;
}
- if ( Abs_ManSupport(p, pObj, vSupp) > nCutMax )
+
+ // dereference nodes
+ Abs_GiaObjDeref_rec( p, pObj );
+ // compute support
+ Abs_ManSupport( p, pObj, vSupp );
+ // check support size
+ if ( Vec_IntSize(vSupp) > nCutMax )
{
+ Abs_GiaObjRef_rec( p, pObj );
pObj->fMark1 = 1;
continue;
}
-
- // pObj has structural support no more than nCutMax
- Abs_GiaObjDeref_rec( p, pObj );
- // sort support nodes by ref count
+ // order nodes by their ref counts
nSize0 = Abs_GiaSortNodes( p, vSupp );
- // check how many support nodes have ref count 0
- if ( nSize0 == 0 )
+ // quit if there is no removable or too many
+ if ( nSize0 == 0 || nSize0 > nCutMax )
{
Abs_GiaObjRef_rec( p, pObj );
continue;
@@ -358,30 +581,91 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
if ( !Abs_GiaCheckTruth( &uTruth, Vec_IntSize(vSupp), nSize0 ) ) // has const
{
Abs_GiaObjRef_rec( p, pObj );
-// printf( " no\n" );
+/*
+ if ( Iter == 1 )
+ {
+ printf( "Node = %8d Supp = %2d Supp0 = %2d ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 );
+ Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) );
+ printf( " no\n" );
+ }
+*/
continue;
}
+/*
printf( "Node = %8d Supp = %2d Supp0 = %2d ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 );
Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) );
printf( " yes\n" );
-
+*/
// pObj can be reparamed
pObj->fMark0 = 1;
fChanges = 1;
}
}
+ Vec_IntFree( vPis );
+ Vec_IntFree( vAnds );
Vec_IntFree( vSupp );
Vec_WrdFree( vTruths );
ABC_FREE( p->pRefs );
- Gia_ManCleanMark0( p ); // temp
+// Gia_ManCleanMark0( p ); // temp
Gia_ManCleanMark1( p );
}
+/**Function*************************************************************
+
+ Synopsis [Assumed that fMark0 marks the internal PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p )
+{
+ Vec_Int_t * vPis, * vAnds;
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ vPis = Vec_IntAlloc( 100 );
+ vAnds = Vec_IntAlloc( 100 );
+ Gia_ManCountPisNodes( p, vPis, vAnds );
+
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ // create PIs
+ Gia_ManForEachObjVec( vPis, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ // create flops
+ Gia_ManForEachRo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ // create internal nodes
+ Gia_ManForEachObjVec( vAnds, p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // create COs
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+
+ Vec_IntFree( vPis );
+ Vec_IntFree( vAnds );
+ return pNew;
+}
+
Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose )
{
-// Abs_GiaTest( p, nCutMax, fVerbose );
- Abs_RpmPerformMark( p, nCutMax, 1 );
+ Gia_Man_t * pNew;
+
+ Gia_ManTestDoms( p );
return NULL;
+
+ Abs_RpmPerformMark( p, nCutMax, 1 );
+ pNew = Gia_ManDupRpm( p );
+ Gia_ManCleanMark0( p );
+ return pNew;
}
////////////////////////////////////////////////////////////////////////