From 5cd1396b3d752c968cd558f02625ce5f12688415 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 24 Oct 2012 12:22:46 -0700
Subject: Creating dedicated choice representation for GIA.
---
src/aig/gia/gia.h | 4 +++
src/aig/gia/giaAig.c | 77 ++++++++++++++++++++++++++++++++++-------------
src/aig/gia/giaAig.h | 1 +
src/aig/gia/giaMan.c | 32 ++++++++++++++++++++
src/aig/gia/giaUtil.c | 25 +++++++++++++++
src/proof/dch/dchChoice.c | 2 +-
src/proof/dch/dchCore.c | 4 ++-
7 files changed, 122 insertions(+), 23 deletions(-)
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d573afdc..4473921c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -117,6 +117,7 @@ struct Gia_Man_t_
int * pReprsOld; // representatives (for CIs and ANDs)
Gia_Rpr_t * pReprs; // representatives (for CIs and ANDs)
int * pNexts; // next nodes in the equivalence classes
+ int * pSibls; // next nodes in the choice nodes
int * pIso; // pairs of structurally isomorphic nodes
int nTerLoop; // the state where loop begins
int nTerStates; // the total number of ternary states
@@ -570,6 +571,8 @@ static inline void Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ a
static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; }
static inline int Gia_ObjHasRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr != GIA_VOID; }
static inline int Gia_ObjReprSelf( Gia_Man_t * p, int Id ) { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id; }
+static inline int Gia_ObjSibl( Gia_Man_t * p, int Id ) { return p->pSibls ? p->pSibls[Id] : 0; }
+static inline Gia_Obj_t * Gia_ObjSiblObj( Gia_Man_t * p, int Id ) { return (p->pSibls && p->pSibls[Id]) ? Gia_ManObj(p, p->pSibls[Id]) : NULL; }
static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
@@ -920,6 +923,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
+extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 224d3bda..5dcc6038 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -42,7 +42,7 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
/**Function*************************************************************
- Synopsis [Derives combinational miter of the two AIGs.]
+ Synopsis [Duplicates AIG in the DFS order.]
Description []
@@ -70,6 +70,34 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
pNew->pNexts[iObjNew] = iNextNew;
}
}
+Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Gia_ManStart( Aig_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ pNew->nConstrs = p->nConstrs;
+ // create room to store equivalences
+ if ( p->pEquivs )
+ pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->iData = 1;
+ Aig_ManForEachCi( p, pObj, i )
+ pObj->iData = Gia_ManAppendCi( pNew );
+ // add logic for the POs
+ Aig_ManForEachCo( p, pObj, i )
+ Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ Aig_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+ if ( pNew->pNexts )
+ Gia_ManDeriveReprs( pNew );
+ return pNew;
+}
/**Function*************************************************************
@@ -82,19 +110,38 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( pObj == NULL || pObj->iData )
+ return;
+ assert( Aig_ObjIsNode(pObj) );
+ Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
+ Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
+ pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+ if ( Aig_ObjEquiv(p, pObj) )
+ {
+ int iObjNew, iNextNew;
+ iObjNew = Abc_Lit2Var(pObj->iData);
+ iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
+ assert( iObjNew > iNextNew );
+ assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
+ pNew->pSibls[iObjNew] = iNextNew;
+ }
+}
+Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
{
Gia_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
+ assert( p->pEquivs != NULL );
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// create room to store equivalences
- if ( p->pEquivs )
- pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+ pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->iData = 1;
@@ -102,12 +149,11 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
pObj->iData = Gia_ManAppendCi( pNew );
// add logic for the POs
Aig_ManForEachCo( p, pObj, i )
- Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
- if ( pNew->pNexts )
- Gia_ManDeriveReprs( pNew );
+ assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
return pNew;
}
@@ -195,7 +241,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Derives combinational miter of the two AIGs.]
+ Synopsis [Duplicates AIG in the DFS order.]
Description []
@@ -228,18 +274,6 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);
}
}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates AIG in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
{
Aig_Man_t * pNew;
@@ -541,7 +575,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
Aig_Man_t * pNew;
pNew = Gia_ManToAig( p, 0 );
pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
- pGia = Gia_ManFromAig( pNew );
+// pGia = Gia_ManFromAig( pNew );
+ pGia = Gia_ManFromAigChoices( pNew );
Aig_ManStop( pNew );
return pGia;
}
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index b72f6415..6498ec52 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -51,6 +51,7 @@ ABC_NAMESPACE_HEADER_START
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 494f9a1c..f82e7952 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -107,6 +107,7 @@ void Gia_ManStop( Gia_Man_t * p )
ABC_FREE( p->pReprsOld );
ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts );
+ ABC_FREE( p->pSibls );
ABC_FREE( p->pRefs );
// ABC_FREE( p->pNodeRefs );
ABC_FREE( p->pHTable );
@@ -249,6 +250,35 @@ void Gia_ManPrintTents( Gia_Man_t * p )
// Gia_ObjPrint( p, pObj );
}
+/**Function*************************************************************
+
+ Synopsis [Prints stats for the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManPrintChoiceStats( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i, nEquivs = 0, nChoices = 0;
+ Gia_ManMarkFanoutDrivers( p );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjSibl(p, i) )
+ continue;
+ nEquivs++;
+ if ( pObj->fMark0 )
+ nChoices++;
+ assert( !Gia_ObjSiblObj(p, i)->fMark0 );
+ assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
+ }
+ Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
+}
+
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
@@ -289,6 +319,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
// Gia_ManSatExperiment( p );
if ( p->pReprs && p->pNexts )
Gia_ManEquivPrintClasses( p, 0, 0.0 );
+ if ( p->pSibls )
+ Gia_ManPrintChoiceStats( p );
if ( p->pMapping )
Gia_ManPrintMappingStats( p );
if ( p->pPlacement )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index b0f25864..8389a9b0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1243,6 +1243,31 @@ int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Marks nodes that appear as faninis of other nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManCleanMark0( p );
+ Gia_ManForEachObj( p, pObj, i )
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ Gia_ObjFanin0(pObj)->fMark0 = 1;
+ Gia_ObjFanin1(pObj)->fMark0 = 1;
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ Gia_ObjFanin0(pObj)->fMark0 = 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 783202e2..3f097ecc 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -95,7 +95,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
pEquiv = Aig_ObjEquiv( pAig, pObj );
if ( pEquiv == NULL )
continue;
- assert( pEquiv->Id > pObj->Id );
+ assert( pEquiv->Id < pObj->Id );
nEquivs++;
}
return nEquivs;
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0d2e8c0d..b92de8a6 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -111,7 +111,9 @@ p->timeTotal = clock() - clkTotal;
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
// count the number of representatives
if ( pPars->fVerbose )
- Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
+ Abc_Print( 1, "STATS: Ands:%8d ->%8d. Reprs:%7d ->%7d. Choices =%7d.\n",
+ Aig_ManNodeNum(pAig),
+ Aig_ManNodeNum(pResult),
Dch_DeriveChoiceCountReprs( pAig ),
Dch_DeriveChoiceCountEquivs( pResult ),
Aig_ManChoiceNum( pResult ) );
--
cgit v1.2.3