abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
aigMffc.c File Reference
#include "aig.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec (Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
 DECLARATIONS ///. More...
 
int Aig_NodeRef_rec (Aig_Obj_t *pNode, unsigned LevelMin)
 
int Aig_NodeRefLabel_rec (Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin)
 
void Aig_NodeMffcSupp_rec (Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin, Vec_Ptr_t *vSupp, int fTopmost, Aig_Obj_t *pObjSkip)
 
int Aig_NodeMffcSupp (Aig_Man_t *p, Aig_Obj_t *pNode, int LevelMin, Vec_Ptr_t *vSupp)
 
int Aig_NodeMffcLabel (Aig_Man_t *p, Aig_Obj_t *pNode, float *pPower)
 
int Aig_NodeMffcLabelCut (Aig_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vLeaves)
 
int Aig_NodeMffcExtendCut (Aig_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vResult)
 

Function Documentation

ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec ( Aig_Obj_t pNode,
unsigned  LevelMin,
float *  pPower,
float *  pProbs 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [aigMffc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Computation of MFFCs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:
aigMffc.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Dereferences the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file aigMffc.c.

46 {
47  float Power0 = 0.0, Power1 = 0.0;
48  Aig_Obj_t * pFanin;
49  int Counter = 0;
50  if ( pProbs )
51  *pPower = 0.0;
52  if ( Aig_ObjIsCi(pNode) )
53  return 0;
54  // consider the first fanin
55  pFanin = Aig_ObjFanin0(pNode);
56  assert( pFanin->nRefs > 0 );
57  if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
58  Counter += Aig_NodeDeref_rec( pFanin, LevelMin, &Power0, pProbs );
59  if ( pProbs )
60  *pPower += Power0 + 2.0 * pProbs[pFanin->Id] * (1.0 - pProbs[pFanin->Id]);
61  // skip the buffer
62  if ( Aig_ObjIsBuf(pNode) )
63  return Counter;
64  assert( Aig_ObjIsNode(pNode) );
65  // consider the second fanin
66  pFanin = Aig_ObjFanin1(pNode);
67  assert( pFanin->nRefs > 0 );
68  if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
69  Counter += Aig_NodeDeref_rec( pFanin, LevelMin, &Power1, pProbs );
70  if ( pProbs )
71  *pPower += Power1 + 2.0 * pProbs[pFanin->Id] * (1.0 - pProbs[pFanin->Id]);
72  return Counter + 1;
73 }
unsigned Level
Definition: aig.h:82
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
Definition: aig.h:69
static int Counter
#define assert(ex)
Definition: util_old.h:213
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
int Id
Definition: aig.h:85
unsigned int nRefs
Definition: aig.h:81
int Aig_NodeMffcExtendCut ( Aig_Man_t p,
Aig_Obj_t pNode,
Vec_Ptr_t vLeaves,
Vec_Ptr_t vResult 
)

Function*************************************************************

Synopsis [Expands the cut by adding the most closely related node.]

Description [Returns 1 if the cut exists.]

SideEffects []

SeeAlso []

Definition at line 265 of file aigMffc.c.

266 {
267  Aig_Obj_t * pObj, * pLeafBest;
268  int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
269  // dereference the current cut
270  LevelMax = 0;
271  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
272  LevelMax = Abc_MaxInt( LevelMax, (int)pObj->Level );
273  if ( LevelMax == 0 )
274  return 0;
275  // dereference the cut
276  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
277  // try expanding each node in the boundary
278  ConeBest = ABC_INFINITY;
279  pLeafBest = NULL;
280  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
281  {
282  if ( (int)pObj->Level != LevelMax )
283  continue;
284  ConeCur1 = Aig_NodeDeref_rec( pObj, 0, NULL, NULL );
285  if ( ConeBest > ConeCur1 )
286  {
287  ConeBest = ConeCur1;
288  pLeafBest = pObj;
289  }
290  ConeCur2 = Aig_NodeRef_rec( pObj, 0 );
291  assert( ConeCur1 == ConeCur2 );
292  }
293  assert( pLeafBest != NULL );
294  assert( Aig_ObjIsNode(pLeafBest) );
295  // deref the best leaf
296  ConeCur1 = Aig_NodeDeref_rec( pLeafBest, 0, NULL, NULL );
297  // collect the cut nodes
298  Vec_PtrClear( vResult );
300  Aig_NodeMffcSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
301  // ref the nodes
302  ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
303  assert( ConeCur1 == ConeCur2 );
304  // ref the original node
305  ConeSize2 = Aig_NodeRef_rec( pNode, 0 );
306  assert( ConeSize1 == ConeSize2 );
307  return 1;
308 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
int Aig_NodeRef_rec(Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:86
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
void Aig_NodeMffcSupp_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin, Vec_Ptr_t *vSupp, int fTopmost, Aig_Obj_t *pObjSkip)
Definition: aigMffc.c:150
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Aig_NodeMffcLabel ( Aig_Man_t p,
Aig_Obj_t pNode,
float *  pPower 
)

Function*************************************************************

Synopsis [Labels the nodes in the MFFC.]

Description [Returns the number of internal nodes in the MFFC.]

SideEffects []

SeeAlso []

Definition at line 211 of file aigMffc.c.

212 {
213  int ConeSize1, ConeSize2;
214  assert( (pPower != NULL) == (p->vProbs != NULL) );
215  assert( !Aig_IsComplement(pNode) );
216  assert( Aig_ObjIsNode(pNode) );
218  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, pPower, p->vProbs? (float *)p->vProbs->pArray : NULL );
219  ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
220  assert( ConeSize1 == ConeSize2 );
221  assert( ConeSize1 > 0 );
222  return ConeSize1;
223 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int Aig_NodeRefLabel_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:118
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
#define assert(ex)
Definition: util_old.h:213
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
int Aig_NodeMffcLabelCut ( Aig_Man_t p,
Aig_Obj_t pNode,
Vec_Ptr_t vLeaves 
)

Function*************************************************************

Synopsis [Labels the nodes in the MFFC.]

Description [Returns the number of internal nodes in the MFFC.]

SideEffects []

SeeAlso []

Definition at line 236 of file aigMffc.c.

237 {
238  Aig_Obj_t * pObj;
239  int i, ConeSize1, ConeSize2;
240  assert( !Aig_IsComplement(pNode) );
241  assert( Aig_ObjIsNode(pNode) );
243  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
244  pObj->nRefs++;
245  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
246  ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
247  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
248  pObj->nRefs--;
249  assert( ConeSize1 == ConeSize2 );
250  assert( ConeSize1 > 0 );
251  return ConeSize1;
252 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int Aig_NodeRefLabel_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:118
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Definition: aig.h:69
#define assert(ex)
Definition: util_old.h:213
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Aig_NodeMffcSupp ( Aig_Man_t p,
Aig_Obj_t pNode,
int  LevelMin,
Vec_Ptr_t vSupp 
)

Function*************************************************************

Synopsis [Collects the support of depth-limited MFFC.]

Description [Returns the number of internal nodes in the MFFC.]

SideEffects []

SeeAlso []

Definition at line 179 of file aigMffc.c.

180 {
181  int ConeSize1, ConeSize2;
182  if ( vSupp ) Vec_PtrClear( vSupp );
183  if ( !Aig_ObjIsNode(pNode) )
184  {
185  if ( Aig_ObjIsCi(pNode) && vSupp )
186  Vec_PtrPush( vSupp, pNode );
187  return 0;
188  }
189  assert( !Aig_IsComplement(pNode) );
190  assert( Aig_ObjIsNode(pNode) );
192  ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL );
193  Aig_NodeMffcSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
194  ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
195  assert( ConeSize1 == ConeSize2 );
196  assert( ConeSize1 > 0 );
197  return ConeSize1;
198 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
int Aig_NodeRef_rec(Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:86
void Aig_NodeMffcSupp_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin, Vec_Ptr_t *vSupp, int fTopmost, Aig_Obj_t *pObjSkip)
Definition: aigMffc.c:150
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Aig_NodeMffcSupp_rec ( Aig_Man_t p,
Aig_Obj_t pNode,
unsigned  LevelMin,
Vec_Ptr_t vSupp,
int  fTopmost,
Aig_Obj_t pObjSkip 
)

Function*************************************************************

Synopsis [Collects the internal and boundary nodes in the derefed MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file aigMffc.c.

151 {
152  // skip visited nodes
153  if ( Aig_ObjIsTravIdCurrent(p, pNode) )
154  return;
155  Aig_ObjSetTravIdCurrent(p, pNode);
156  // add to the new support nodes
157  if ( !fTopmost && pNode != pObjSkip && (Aig_ObjIsCi(pNode) || pNode->nRefs > 0 || pNode->Level <= LevelMin) )
158  {
159  if ( vSupp ) Vec_PtrPush( vSupp, pNode );
160  return;
161  }
162  assert( Aig_ObjIsNode(pNode) );
163  // recur on the children
164  Aig_NodeMffcSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
165  Aig_NodeMffcSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
166 }
unsigned Level
Definition: aig.h:82
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
void Aig_NodeMffcSupp_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin, Vec_Ptr_t *vSupp, int fTopmost, Aig_Obj_t *pObjSkip)
Definition: aigMffc.c:150
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
unsigned int nRefs
Definition: aig.h:81
int Aig_NodeRef_rec ( Aig_Obj_t pNode,
unsigned  LevelMin 
)

Function*************************************************************

Synopsis [References the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file aigMffc.c.

87 {
88  Aig_Obj_t * pFanin;
89  int Counter = 0;
90  if ( Aig_ObjIsCi(pNode) )
91  return 0;
92  // consider the first fanin
93  pFanin = Aig_ObjFanin0(pNode);
94  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
95  Counter += Aig_NodeRef_rec( pFanin, LevelMin );
96  // skip the buffer
97  if ( Aig_ObjIsBuf(pNode) )
98  return Counter;
99  assert( Aig_ObjIsNode(pNode) );
100  // consider the second fanin
101  pFanin = Aig_ObjFanin1(pNode);
102  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
103  Counter += Aig_NodeRef_rec( pFanin, LevelMin );
104  return Counter + 1;
105 }
unsigned Level
Definition: aig.h:82
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
int Aig_NodeRef_rec(Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:86
Definition: aig.h:69
static int Counter
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
unsigned int nRefs
Definition: aig.h:81
int Aig_NodeRefLabel_rec ( Aig_Man_t p,
Aig_Obj_t pNode,
unsigned  LevelMin 
)

Function*************************************************************

Synopsis [References the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file aigMffc.c.

119 {
120  Aig_Obj_t * pFanin;
121  int Counter = 0;
122  if ( Aig_ObjIsCi(pNode) )
123  return 0;
124  Aig_ObjSetTravIdCurrent( p, pNode );
125  // consider the first fanin
126  pFanin = Aig_ObjFanin0(pNode);
127  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
128  Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
129  if ( Aig_ObjIsBuf(pNode) )
130  return Counter;
131  assert( Aig_ObjIsNode(pNode) );
132  // consider the second fanin
133  pFanin = Aig_ObjFanin1(pNode);
134  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
135  Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
136  return Counter + 1;
137 }
unsigned Level
Definition: aig.h:82
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
int Aig_NodeRefLabel_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:118
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
Definition: aig.h:69
static int Counter
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
unsigned int nRefs
Definition: aig.h:81