abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb4Cluster.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb2Cluster.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Non-linear quantification scheduling.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Find good static variable ordering.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
46 {
47  Aig_Obj_t * pFanin0, * pFanin1;
48  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
49  return;
50  Aig_ObjSetTravIdCurrent( pAig, pObj );
51  assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
52  if ( Aig_ObjIsCi(pObj) )
53  {
54  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
55  return;
56  }
57  // try fanins with higher level first
58  pFanin0 = Aig_ObjFanin0(pObj);
59  pFanin1 = Aig_ObjFanin1(pObj);
60 // if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
61  if ( pFanin0->Level > pFanin1->Level )
62  {
63  Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
64  Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
65  }
66  else
67  {
68  Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
69  Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
70  }
71  if ( pObj->fMarkA )
72  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Find good static variable ordering.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter )
87 {
88  Vec_Int_t * vNodes = NULL;
89  Vec_Int_t * vOrder;
90  Aig_Obj_t * pObj;
91  int i, Counter = 0;
92  // mark nodes to exclude: AND with low level and CO drivers
93  Aig_ManCleanMarkA( pAig );
94  Aig_ManForEachNode( pAig, pObj, i )
95  if ( Aig_ObjLevel(pObj) > 3 )
96  pObj->fMarkA = 1;
97  Aig_ManForEachCo( pAig, pObj, i )
98  Aig_ObjFanin0(pObj)->fMarkA = 0;
99 
100  // collect nodes in the order
101  vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
102  Aig_ManIncrementTravId( pAig );
103  Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
104 // Aig_ManForEachCo( pAig, pObj, i )
105  Saig_ManForEachLi( pAig, pObj, i )
106  {
107  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
108  Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
109  }
110  Aig_ManForEachCi( pAig, pObj, i )
111  if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
112  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
113  Aig_ManCleanMarkA( pAig );
114  Vec_IntFreeP( &vNodes );
115 // assert( Counter == Aig_ManObjNum(pAig) - 1 );
116 
117 /*
118  Saig_ManForEachPi( pAig, pObj, i )
119  printf( "pi%d ", Llb_ObjBddVar(vOrder, pObj) );
120  printf( "\n" );
121  Saig_ManForEachLo( pAig, pObj, i )
122  printf( "lo%d ", Llb_ObjBddVar(vOrder, pObj) );
123  printf( "\n" );
124  Saig_ManForEachPo( pAig, pObj, i )
125  printf( "po%d ", Llb_ObjBddVar(vOrder, pObj) );
126  printf( "\n" );
127  Saig_ManForEachLi( pAig, pObj, i )
128  printf( "li%d ", Llb_ObjBddVar(vOrder, pObj) );
129  printf( "\n" );
130  Aig_ManForEachNode( pAig, pObj, i )
131  printf( "n%d ", Llb_ObjBddVar(vOrder, pObj) );
132  printf( "\n" );
133 */
134  if ( pCounter )
135  *pCounter = Counter;
136  return vOrder;
137 }
138 
139 /**Function*************************************************************
140 
141  Synopsis [Derives BDDs for the partitions.]
142 
143  Description []
144 
145  SideEffects []
146 
147  SeeAlso []
148 
149 ***********************************************************************/
150 DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots )
151 {
152  DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
153  if ( Aig_ObjIsConst1(pObj) )
154  return Cudd_ReadOne(dd);
155  if ( Aig_ObjIsCi(pObj) )
156  return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
157  if ( pObj->pData )
158  return (DdNode *)pObj->pData;
159  if ( Aig_ObjIsCo(pObj) )
160  {
161  bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
162  bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart );
163  Vec_PtrPush( vRoots, bPart );
164  return NULL;
165  }
166  bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
167  bBdd1 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
168  bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
169  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
170  {
171  vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
172  bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart );
173  Vec_PtrPush( vRoots, bPart );
174  Cudd_RecursiveDeref( dd, bBdd );
175  bBdd = vVar; Cudd_Ref( vVar );
176  }
177  pObj->pData = bBdd;
178  return bBdd;
179 }
180 
181 /**Function*************************************************************
182 
183  Synopsis [Derives BDDs for the partitions.]
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fOutputs )
193 {
194  Vec_Ptr_t * vRoots;
195  Aig_Obj_t * pObj;
196  int i;
197  Aig_ManCleanData( pAig );
198  vRoots = Vec_PtrAlloc( 100 );
199  if ( fOutputs )
200  {
201  Saig_ManForEachPo( pAig, pObj, i )
202  Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
203  }
204  else
205  {
206  Saig_ManForEachLi( pAig, pObj, i )
207  Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
208  }
209  Aig_ManForEachNode( pAig, pObj, i )
210  if ( pObj->pData )
211  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
212  return vRoots;
213 }
214 
215 /**Function*************************************************************
216 
217  Synopsis [Creates quantifiable variables for both types of traversal.]
218 
219  Description []
220 
221  SideEffects []
222 
223  SeeAlso []
224 
225 ***********************************************************************/
226 Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
227 {
228  Vec_Int_t * vVars2Q;
229  Aig_Obj_t * pObj;
230  int i;
231  vVars2Q = Vec_IntAlloc( 0 );
232  Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
233  Saig_ManForEachLo( pAig, pObj, i )
234  Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
235 // Aig_ManForEachCo( pAig, pObj, i )
236  Saig_ManForEachLi( pAig, pObj, i )
237  Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
238  return vVars2Q;
239 }
240 
241 /**Function*************************************************************
242 
243  Synopsis [Creates quantifiable variables for both types of traversal.]
244 
245  Description []
246 
247  SideEffects []
248 
249  SeeAlso []
250 
251 ***********************************************************************/
252 int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
253 {
254  DdNode * bSupp;
255  Aig_Obj_t * pObj;
256  int i, Counter = 0;
257  bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
258  if ( !fCo && !fFlop )
259  {
260  Saig_ManForEachPi( pAig, pObj, i )
261  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
262  Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
263  }
264  else if ( fCo && !fFlop )
265  {
266  Saig_ManForEachPo( pAig, pObj, i )
267  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
268  Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
269  }
270  else if ( !fCo && fFlop )
271  {
272  Saig_ManForEachLo( pAig, pObj, i )
273  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
274  Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
275  }
276  else if ( fCo && fFlop )
277  {
278  Saig_ManForEachLi( pAig, pObj, i )
279  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
280  Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
281  }
282  Cudd_RecursiveDeref( dd, bSupp );
283  return Counter;
284 }
285 
286 /**Function*************************************************************
287 
288  Synopsis [Creates quantifiable variables for both types of traversal.]
289 
290  Description []
291 
292  SideEffects []
293 
294  SeeAlso []
295 
296 ***********************************************************************/
297 void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
298 {
299  DdNode * bTemp;
300  int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
301  Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
302  {
303 //Extra_bddPrintSupport(dd, bTemp); printf("\n" );
304  nSuppAll = Cudd_SupportSize(dd,bTemp);
305  nSuppPi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
306  nSuppPo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
307  nSuppLi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
308  nSuppLo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
309  nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
310 
311  if ( Cudd_DagSize(bTemp) <= 10 )
312  continue;
313 
314  printf( "%4d : bdd =%6d supp =%3d ", i, Cudd_DagSize(bTemp), nSuppAll );
315  printf( "pi =%3d ", nSuppPi );
316  printf( "po =%3d ", nSuppPo );
317  printf( "lo =%3d ", nSuppLo );
318  printf( "li =%3d ", nSuppLi );
319  printf( "and =%3d", nSuppAnd );
320  printf( "\n" );
321  }
322 }
323 
324 /**Function*************************************************************
325 
326  Synopsis [Creates quantifiable variables for both types of traversal.]
327 
328  Description []
329 
330  SideEffects []
331 
332  SeeAlso []
333 
334 ***********************************************************************/
335 void Llb_Nonlin4PrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
336 {
337  Aig_Obj_t * pObj;
338  int i, * pSupp;
339  int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
340 
341  pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
342  Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
343 
344  Aig_ManForEachObj( pAig, pObj, i )
345  {
346  if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
347  continue;
348  // remove variables that do not participate
349  if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
350  {
351  if ( Aig_ObjIsNode(pObj) )
352  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
353  continue;
354  }
355  nSuppAll++;
356  if ( Saig_ObjIsPi(pAig, pObj) )
357  nSuppPi++;
358  else if ( Saig_ObjIsLo(pAig, pObj) )
359  nSuppLo++;
360  else if ( Saig_ObjIsPo(pAig, pObj) )
361  nSuppPo++;
362  else if ( Saig_ObjIsLi(pAig, pObj) )
363  nSuppLi++;
364  else
365  nSuppAnd++;
366  }
367  ABC_FREE( pSupp );
368 
369  printf( "Groups =%3d ", Vec_PtrSize(vGroups) );
370  printf( "Variables: all =%4d ", nSuppAll );
371  printf( "pi =%4d ", nSuppPi );
372  printf( "po =%4d ", nSuppPo );
373  printf( "lo =%4d ", nSuppLo );
374  printf( "li =%4d ", nSuppLi );
375  printf( "and =%4d", nSuppAnd );
376  printf( "\n" );
377 }
378 
379 /**Function*************************************************************
380 
381  Synopsis []
382 
383  Description []
384 
385  SideEffects []
386 
387  SeeAlso []
388 
389 ***********************************************************************/
390 void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose )
391 {
392  DdManager * dd;
393  Vec_Int_t * vOrder, * vVars2Q;
394  Vec_Ptr_t * vParts, * vGroups;
395  DdNode * bTemp;
396  int i, nVarNum;
397 
398  // create the BDD manager
399  vOrder = Llb_Nonlin4FindOrder( pAig, &nVarNum );
400  dd = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
401 // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
402 
403  vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
404  vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder, 0 );
405 
406  vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax );
407  Vec_IntFree( vVars2Q );
408 
409  Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
410  Cudd_RecursiveDeref( dd, bTemp );
411  Vec_PtrFree( vParts );
412 
413 
414 // if ( fVerbose )
415  Llb_Nonlin4PrintSuppProfile( dd, pAig, vOrder, vGroups );
416  if ( fVerbose )
417  printf( "Before reordering\n" );
418  if ( fVerbose )
419  Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
420 
421 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
422 // printf( "After reordering\n" );
423 // Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
424 
425  if ( pvOrder )
426  *pvOrder = vOrder;
427  else
428  Vec_IntFree( vOrder );
429 
430  if ( pvGroups )
431  *pvGroups = vGroups;
432  else
433  {
434  Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
435  Cudd_RecursiveDeref( dd, bTemp );
436  Vec_PtrFree( vGroups );
437  }
438 
439  if ( pdd )
440  *pdd = dd;
441  else
442  Extra_StopManager( dd );
443 // Cudd_Quit( dd );
444 }
445 
446 ////////////////////////////////////////////////////////////////////////
447 /// END OF FILE ///
448 ////////////////////////////////////////////////////////////////////////
449 
450 
451 ABC_NAMESPACE_IMPL_END
452 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Llb_Nonlin4PrintGroups
void Llb_Nonlin4PrintGroups(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups)
Definition: llb4Cluster.c:297
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
Extra_VectorSupportArray
int * Extra_VectorSupportArray(DdManager *dd, DdNode **F, int n, int *support)
Definition: extraBddMisc.c:572
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Llb_Nonlin4FindOrder_rec
ABC_NAMESPACE_IMPL_START void Llb_Nonlin4FindOrder_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter)
DECLARATIONS ///.
Definition: llb4Cluster.c:45
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Llb_Nonlin4Cluster
void Llb_Nonlin4Cluster(Aig_Man_t *pAig, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int nBddMax, int fVerbose)
Definition: llb4Cluster.c:390
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Llb_Nonlin4FindPartitions
Vec_Ptr_t * Llb_Nonlin4FindPartitions(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fOutputs)
Definition: llb4Cluster.c:192
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Llb_Nonlin4Group
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition: llb4Image.c:806
Saig_ObjIsPo
static int Saig_ObjIsPo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:83
Llb_Nonlin4FindPartitions_rec
DdNode * Llb_Nonlin4FindPartitions_rec(DdManager *dd, Aig_Obj_t *pObj, Vec_Int_t *vOrder, Vec_Ptr_t *vRoots)
Definition: llb4Cluster.c:150
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_Obj_t_
Definition: aig.h:69
Llb_Nonlin4CountTerms
int Llb_Nonlin4CountTerms(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, DdNode *bFunc, int fCo, int fFlop)
Definition: llb4Cluster.c:252
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Llb_Nonlin4PrintSuppProfile
void Llb_Nonlin4PrintSuppProfile(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups)
Definition: llb4Cluster.c:335
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Llb_ObjBddVar
static int Llb_ObjBddVar(Vec_Int_t *vOrder, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: llbInt.h:109
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Llb_Nonlin4FindVars2Q
Vec_Int_t * Llb_Nonlin4FindVars2Q(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder)
Definition: llb4Cluster.c:226
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Aig_ObjLevel
static int Aig_ObjLevel(Aig_Obj_t *pObj)
Definition: aig.h:323
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Llb_Nonlin4FindOrder
Vec_Int_t * Llb_Nonlin4FindOrder(Aig_Man_t *pAig, int *pCounter)
Definition: llb4Cluster.c:86
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91