abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb1Group.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb1Group.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Initial partition computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb1Group.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis []
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
46 {
47  Llb_Grp_t * p;
48  p = ABC_CALLOC( Llb_Grp_t, 1 );
49  p->pMan = pMan;
50  p->vIns = Vec_PtrAlloc( 8 );
51  p->vOuts = Vec_PtrAlloc( 8 );
52  p->Id = Vec_PtrSize( pMan->vGroups );
53  Vec_PtrPush( pMan->vGroups, p );
54  return p;
55 }
56 
57 /**Function*************************************************************
58 
59  Synopsis []
60 
61  Description []
62 
63  SideEffects []
64 
65  SeeAlso []
66 
67 ***********************************************************************/
69 {
70  if ( p == NULL )
71  return;
72  Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
73  Vec_PtrFreeP( &p->vIns );
74  Vec_PtrFreeP( &p->vOuts );
75  Vec_PtrFreeP( &p->vNodes );
76  ABC_FREE( p );
77 }
78 
79 
80 /**Function*************************************************************
81 
82  Synopsis []
83 
84  Description []
85 
86  SideEffects []
87 
88  SeeAlso []
89 
90 ***********************************************************************/
91 void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
92 {
93  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
94  return;
95  Aig_ObjSetTravIdCurrent(pAig, pObj);
96  if ( Aig_ObjIsConst1(pObj) )
97  return;
98  if ( Aig_ObjIsCo(pObj) )
99  {
100  Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
101  return;
102  }
103  assert( Aig_ObjIsAnd(pObj) );
104  Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
105  Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes );
106  Vec_PtrPush( vNodes, pObj );
107 }
108 
109 /**Function*************************************************************
110 
111  Synopsis [Collects the support of MFFC.]
112 
113  Description [Returns the number of internal nodes in the MFFC.]
114 
115  SideEffects []
116 
117  SeeAlso []
118 
119 ***********************************************************************/
121 {
122  Vec_Ptr_t * vNodes;
123  Aig_Obj_t * pObj;
124  int i;
125  vNodes = Vec_PtrAlloc( 100 );
126  Aig_ManIncrementTravId( pGroup->pMan->pAig );
127  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
128  Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj );
129  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
130  Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj );
131  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
132  Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes );
133  return vNodes;
134 }
135 
136 /**Function*************************************************************
137 
138  Synopsis []
139 
140  Description []
141 
142  SideEffects []
143 
144  SeeAlso []
145 
146 ***********************************************************************/
147 void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
148 {
149  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
150  return;
151  Aig_ObjSetTravIdCurrent(pAig, pObj);
152  if ( Aig_ObjIsConst1(pObj) )
153  return;
154  if ( pObj->fMarkA )
155  {
156  Vec_PtrPush( vSupp, pObj );
157  return;
158  }
159  assert( Aig_ObjIsAnd(pObj) );
160  Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp );
161  Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp );
162 }
163 
164 /**Function*************************************************************
165 
166  Synopsis []
167 
168  Description []
169 
170  SideEffects []
171 
172  SeeAlso []
173 
174 ***********************************************************************/
176 {
177  Llb_Grp_t * p;
178  assert( pObj->fMarkA == 1 );
179  // derive group
180  p = Llb_ManGroupAlloc( pMan );
181  Vec_PtrPush( p->vOuts, pObj );
182  Aig_ManIncrementTravId( pMan->pAig );
183  if ( Aig_ObjIsCo(pObj) )
184  Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
185  else
186  {
187  Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
188  Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns );
189  }
190  // derive internal objects
191  assert( p->vNodes == NULL );
192  p->vNodes = Llb_ManGroupCollect( p );
193  return p;
194 }
195 
196 /**Function*************************************************************
197 
198  Synopsis []
199 
200  Description []
201 
202  SideEffects []
203 
204  SeeAlso []
205 
206 ***********************************************************************/
208 {
209  Llb_Grp_t * p;
210  Aig_Obj_t * pObj;
211  int i;
212  p = Llb_ManGroupAlloc( pMan );
213  Saig_ManForEachLo( pMan->pAig, pObj, i )
214  Vec_PtrPush( p->vOuts, pObj );
215  return p;
216 }
217 
218 /**Function*************************************************************
219 
220  Synopsis []
221 
222  Description []
223 
224  SideEffects []
225 
226  SeeAlso []
227 
228 ***********************************************************************/
230 {
231  Llb_Grp_t * p;
232  Aig_Obj_t * pObj;
233  int i;
234  p = Llb_ManGroupAlloc( pMan );
235  Saig_ManForEachLi( pMan->pAig, pObj, i )
236  Vec_PtrPush( p->vIns, pObj );
237  return p;
238 }
239 
240 /**Function*************************************************************
241 
242  Synopsis []
243 
244  Description []
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
252 {
253  Llb_Grp_t * p;
254  Aig_Obj_t * pObj;
255  int i;
256  p = Llb_ManGroupAlloc( p1->pMan );
257  // create inputs
258  Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
259  Vec_PtrPush( p->vIns, pObj );
260  Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
261  Vec_PtrPushUnique( p->vIns, pObj );
262  // create outputs
263  Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
264  Vec_PtrPush( p->vOuts, pObj );
265  Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
266  Vec_PtrPushUnique( p->vOuts, pObj );
267 
268  // derive internal objects
269  assert( p->vNodes == NULL );
270  p->vNodes = Llb_ManGroupCollect( p );
271  return p;
272 }
273 
274 
275 /**Function*************************************************************
276 
277  Synopsis []
278 
279  Description []
280 
281  SideEffects []
282 
283  SeeAlso []
284 
285 ***********************************************************************/
287 {
288  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
289  return;
290  if ( Aig_ObjIsTravIdPrevious(p, pObj) )
291  {
292  Aig_ObjSetTravIdCurrent(p, pObj);
293  return;
294  }
295  Aig_ObjSetTravIdCurrent(p, pObj);
296  assert( Aig_ObjIsNode(pObj) );
299 }
300 
301 /**Function*************************************************************
302 
303  Synopsis [Creates group from two cuts derived by the flow computation.]
304 
305  Description []
306 
307  SideEffects []
308 
309  SeeAlso []
310 
311 ***********************************************************************/
313 {
314  Llb_Grp_t * p;
315  Aig_Obj_t * pObj;
316  int i;
317  p = Llb_ManGroupAlloc( pMan );
318 
319  // mark Cut1
320  Aig_ManIncrementTravId( pMan->pAig );
321  Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
322  Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
323  // collect unmarked Cut2
324  Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
325  if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
326  Vec_PtrPush( p->vOuts, pObj );
327 
328  // mark nodes reachable from Cut2
329  Aig_ManIncrementTravId( pMan->pAig );
330  Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
331  Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
332  // collect marked Cut1
333  Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
334  if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
335  Vec_PtrPush( p->vIns, pObj );
336 
337  // derive internal objects
338  assert( p->vNodes == NULL );
339  p->vNodes = Llb_ManGroupCollect( p );
340  return p;
341 }
342 
343 
344 
345 /**Function*************************************************************
346 
347  Synopsis []
348 
349  Description []
350 
351  SideEffects []
352 
353  SeeAlso []
354 
355 ***********************************************************************/
357 {
358  Aig_Obj_t * pObj;
359  int i;
360  assert( pMan->vGroups == NULL );
361  pMan->vGroups = Vec_PtrAlloc( 1000 );
362  Llb_ManGroupCreateFirst( pMan );
363  Aig_ManForEachNode( pMan->pAig, pObj, i )
364  {
365  if ( pObj->fMarkA )
366  Llb_ManGroupCreate( pMan, pObj );
367  }
368  Saig_ManForEachLi( pMan->pAig, pObj, i )
369  {
370  if ( pObj->fMarkA )
371  Llb_ManGroupCreate( pMan, pObj );
372  }
373  Llb_ManGroupCreateLast( pMan );
374 }
375 
376 /**Function*************************************************************
377 
378  Synopsis []
379 
380  Description []
381 
382  SideEffects []
383 
384  SeeAlso []
385 
386 ***********************************************************************/
388 {
389  Llb_Grp_t * pGroup;
390  Aig_Obj_t * pVar;
391  int i, k, Span = 0, SpanMax = 0;
392  Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
393  {
394  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
395  if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
396  Span++;
397  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
398  if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
399  Span++;
400 
401  SpanMax = Abc_MaxInt( SpanMax, Span );
402 printf( "%d ", Span );
403 
404  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
405  if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
406  Span--;
407  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
408  if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
409  Span--;
410  }
411 printf( "\n" );
412 printf( "Max = %d\n", SpanMax );
413 }
414 
415 /**Function*************************************************************
416 
417  Synopsis []
418 
419  Description []
420 
421  SideEffects []
422 
423  SeeAlso []
424 
425 ***********************************************************************/
426 int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar )
427 {
428  Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup );
429  Aig_Obj_t * pObj;
430  int i;
431  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
432  if ( pObj->Id == iVar )
433  return 1;
434  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
435  if ( pObj->Id == iVar )
436  return 1;
437  return 0;
438 }
439 
440 /**Function*************************************************************
441 
442  Synopsis []
443 
444  Description []
445 
446  SideEffects []
447 
448  SeeAlso []
449 
450 ***********************************************************************/
452 {
453  Aig_Obj_t * pObj;
454  int i, k;
455  Aig_ManForEachObj( p->pAig, pObj, i )
456  {
457  if ( Vec_IntEntry(p->vObj2Var, i) < 0 )
458  continue;
459  printf( "%3d :", i );
460  for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ )
461  printf( " " );
462  for ( ; k <= Vec_IntEntry(p->vVarEnds, i); k++ )
463  printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' );
464  printf( "\n" );
465  }
466 }
467 
468 ////////////////////////////////////////////////////////////////////////
469 /// END OF FILE ///
470 ////////////////////////////////////////////////////////////////////////
471 
472 
474 
static int Aig_ObjIsTravIdPrevious(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:296
void Llb_ManGroupStop(Llb_Grp_t *p)
Definition: llb1Group.c:68
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Llb_Man_t * pMan
Definition: llbInt.h:100
void Llb_ManGroupCollect_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: llb1Group.c:91
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Llb_Grp_t * Llb_ManGroupCreate(Llb_Man_t *pMan, Aig_Obj_t *pObj)
Definition: llb1Group.c:175
Vec_Ptr_t * vNodes
Definition: llbInt.h:99
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
unsigned int fMarkA
Definition: aig.h:79
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
ABC_NAMESPACE_IMPL_START Llb_Grp_t * Llb_ManGroupAlloc(Llb_Man_t *pMan)
DECLARATIONS ///.
Definition: llb1Group.c:45
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Llb_Grp_t * Llb_ManGroupsCombine(Llb_Grp_t *p1, Llb_Grp_t *p2)
Definition: llb1Group.c:251
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Llb_ManGroupMarkNodes_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: llb1Group.c:286
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
void Llb_ManPrintHisto(Llb_Man_t *p)
Definition: llb1Group.c:451
int Llb_ManGroupHasVar(Llb_Man_t *p, int iGroup, int iVar)
Definition: llb1Group.c:426
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Llb_Grp_t * Llb_ManGroupCreateLast(Llb_Man_t *pMan)
Definition: llb1Group.c:229
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
static void Aig_ObjSetTravIdPrevious(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:294
void Llb_ManPrepareGroups(Llb_Man_t *pMan)
Definition: llb1Group.c:356
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
void Llb_ManGroupCreate_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Ptr_t *vSupp)
Definition: llb1Group.c:147
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Vec_Ptr_t * Llb_ManGroupCollect(Llb_Grp_t *pGroup)
Definition: llb1Group.c:120
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
#define assert(ex)
Definition: util_old.h:213
void Llb_ManPrintSpan(Llb_Man_t *p)
Definition: llb1Group.c:387
int Id
Definition: llbInt.h:96
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Id
Definition: aig.h:85
typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t
INCLUDES ///.
Definition: llbInt.h:46
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Vec_Ptr_t * vOuts
Definition: llbInt.h:98
Vec_Ptr_t * vIns
Definition: llbInt.h:97
static int Aig_ObjIsAnd(Aig_Obj_t *pObj)
Definition: aig.h:278
Llb_Grp_t * Llb_ManGroupCreateFromCuts(Llb_Man_t *pMan, Vec_Int_t *vCut1, Vec_Int_t *vCut2)
Definition: llb1Group.c:312
Llb_Grp_t * Llb_ManGroupCreateFirst(Llb_Man_t *pMan)
Definition: llb1Group.c:207