abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb3Image.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb3Image.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Computes image using partitioned structure.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb3Image.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 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 typedef struct Llb_Var_t_ Llb_Var_t;
30 struct Llb_Var_t_
31 {
32  int iVar; // variable number
33  int nScore; // variable score
34  Vec_Int_t * vParts; // partitions
35 };
36 
37 typedef struct Llb_Prt_t_ Llb_Prt_t;
38 struct Llb_Prt_t_
39 {
40  int iPart; // partition number
41  int nSize; // the number of BDD nodes
42  DdNode * bFunc; // the partition
43  Vec_Int_t * vVars; // support
44 };
45 
46 typedef struct Llb_Mgr_t_ Llb_Mgr_t;
47 struct Llb_Mgr_t_
48 {
49  Aig_Man_t * pAig; // AIG manager
50  Vec_Ptr_t * vLeaves; // leaves in the AIG manager
51  Vec_Ptr_t * vRoots; // roots in the AIG manager
52  DdManager * dd; // working BDD manager
53  int * pVars2Q; // variables to quantify
54  // internal
55  Llb_Prt_t ** pParts; // partitions
56  Llb_Var_t ** pVars; // variables
57  int iPartFree; // next free partition
58  int nVars; // the number of BDD variables
59  int nSuppMax; // maximum support size
60  // temporary
61  int * pSupp; // temporary support storage
62 };
63 
64 static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i ) { return p->pVars[i]; }
65 static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pParts[i]; }
66 
67 // iterator over vars
68 #define Llb_MgrForEachVar( p, pVar, i ) \
69  for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
70 // iterator over parts
71 #define Llb_MgrForEachPart( p, pPart, i ) \
72  for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
73 
74 // iterator over vars of one partition
75 #define Llb_PartForEachVar( p, pPart, pVar, i ) \
76  for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
77 // iterator over parts of one variable
78 #define Llb_VarForEachPart( p, pVar, pPart, i ) \
79  for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
80 
81 // statistics
82 abctime timeBuild, timeAndEx, timeOther;
83 int nSuppMax;
84 
85 ////////////////////////////////////////////////////////////////////////
86 /// FUNCTION DEFINITIONS ///
87 ////////////////////////////////////////////////////////////////////////
88 
89 /**Function*************************************************************
90 
91  Synopsis [Removes one variable.]
92 
93  Description []
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
100 void Llb_NonlinRemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
101 {
102  assert( p->pVars[pVar->iVar] == pVar );
103  p->pVars[pVar->iVar] = NULL;
104  Vec_IntFree( pVar->vParts );
105  ABC_FREE( pVar );
106 }
107 
108 /**Function*************************************************************
109 
110  Synopsis [Removes one partition.]
111 
112  Description []
113 
114  SideEffects []
115 
116  SeeAlso []
117 
118 ***********************************************************************/
119 void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
120 {
121  assert( p->pParts[pPart->iPart] == pPart );
122  p->pParts[pPart->iPart] = NULL;
123  Vec_IntFree( pPart->vVars );
124  Cudd_RecursiveDeref( p->dd, pPart->bFunc );
125  ABC_FREE( pPart );
126 }
127 
128 /**Function*************************************************************
129 
130  Synopsis [Create cube with singleton variables.]
131 
132  Description []
133 
134  SideEffects []
135 
136  SeeAlso []
137 
138 ***********************************************************************/
139 DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
140 {
141  DdNode * bCube, * bTemp;
142  Llb_Var_t * pVar;
143  int i;
144  abctime TimeStop;
145  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
146  bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
147  Llb_PartForEachVar( p, pPart, pVar, i )
148  {
149  assert( Vec_IntSize(pVar->vParts) > 0 );
150  if ( Vec_IntSize(pVar->vParts) != 1 )
151  continue;
152  assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
153  bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
154  Cudd_RecursiveDeref( p->dd, bTemp );
155  }
156  Cudd_Deref( bCube );
157  p->dd->TimeStop = TimeStop;
158  return bCube;
159 }
160 
161 /**Function*************************************************************
162 
163  Synopsis [Create cube of variables appearing only in two partitions.]
164 
165  Description []
166 
167  SideEffects []
168 
169  SeeAlso []
170 
171 ***********************************************************************/
172 DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
173 {
174  DdNode * bCube, * bTemp;
175  Llb_Var_t * pVar;
176  int i;
177  abctime TimeStop;
178  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
179  bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
180  Llb_PartForEachVar( p, pPart1, pVar, i )
181  {
182  assert( Vec_IntSize(pVar->vParts) > 0 );
183  if ( Vec_IntSize(pVar->vParts) != 2 )
184  continue;
185  if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
186  (Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
187  {
188  bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
189  Cudd_RecursiveDeref( p->dd, bTemp );
190  }
191  }
192  Cudd_Deref( bCube );
193  p->dd->TimeStop = TimeStop;
194  return bCube;
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis [Returns 1 if partition has singleton variables.]
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 int Llb_NonlinHasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
209 {
210  Llb_Var_t * pVar;
211  int i;
212  Llb_PartForEachVar( p, pPart, pVar, i )
213  if ( Vec_IntSize(pVar->vParts) == 1 )
214  return 1;
215  return 0;
216 }
217 
218 /**Function*************************************************************
219 
220  Synopsis [Returns 1 if partition has singleton variables.]
221 
222  Description []
223 
224  SideEffects []
225 
226  SeeAlso []
227 
228 ***********************************************************************/
229 void Llb_NonlinPrint( Llb_Mgr_t * p )
230 {
231  Llb_Prt_t * pPart;
232  Llb_Var_t * pVar;
233  int i, k;
234  printf( "\n" );
235  Llb_MgrForEachVar( p, pVar, i )
236  {
237  printf( "Var %3d : ", i );
238  Llb_VarForEachPart( p, pVar, pPart, k )
239  printf( "%d ", pPart->iPart );
240  printf( "\n" );
241  }
242  Llb_MgrForEachPart( p, pPart, i )
243  {
244  printf( "Part %3d : ", i );
245  Llb_PartForEachVar( p, pPart, pVar, k )
246  printf( "%d ", pVar->iVar );
247  printf( "\n" );
248  }
249 }
250 
251 /**Function*************************************************************
252 
253  Synopsis [Quantifies singles belonging to one partition.]
254 
255  Description []
256 
257  SideEffects []
258 
259  SeeAlso []
260 
261 ***********************************************************************/
262 int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
263 {
264  Llb_Var_t * pVar;
265  Llb_Prt_t * pTemp;
266  Vec_Ptr_t * vSingles;
267  DdNode * bCube, * bTemp;
268  int i, RetValue, nSizeNew;
269  if ( fSubset )
270  {
271  int Length;
272 // int nSuppSize = Cudd_SupportSize( p->dd, pPart->bFunc );
273 // pPart->bFunc = Cudd_SubsetHeavyBranch( p->dd, bTemp = pPart->bFunc, nSuppSize, 3*pPart->nSize/4 ); Cudd_Ref( pPart->bFunc );
274  pPart->bFunc = Cudd_LargestCube( p->dd, bTemp = pPart->bFunc, &Length ); Cudd_Ref( pPart->bFunc );
275 
276  printf( "Subsetting %3d : ", pPart->iPart );
277  printf( "(Supp =%3d Node =%5d) -> ", Cudd_SupportSize(p->dd, bTemp), Cudd_DagSize(bTemp) );
278  printf( "(Supp =%3d Node =%5d)\n", Cudd_SupportSize(p->dd, pPart->bFunc), Cudd_DagSize(pPart->bFunc) );
279 
280  RetValue = (Cudd_DagSize(bTemp) == Cudd_DagSize(pPart->bFunc));
281 
282  Cudd_RecursiveDeref( p->dd, bTemp );
283 
284  if ( RetValue )
285  return 1;
286  }
287  else
288  {
289  // create cube to be quantified
290  bCube = Llb_NonlinCreateCube1( p, pPart ); Cudd_Ref( bCube );
291 // assert( !Cudd_IsConstant(bCube) );
292  // derive new function
293  pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc );
294  Cudd_RecursiveDeref( p->dd, bTemp );
295  Cudd_RecursiveDeref( p->dd, bCube );
296  }
297  // get support
298  vSingles = Vec_PtrAlloc( 0 );
299  nSizeNew = Cudd_DagSize(pPart->bFunc);
300  Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
301  Llb_PartForEachVar( p, pPart, pVar, i )
302  if ( p->pSupp[pVar->iVar] )
303  {
304  assert( Vec_IntSize(pVar->vParts) > 1 );
305  pVar->nScore -= pPart->nSize - nSizeNew;
306  }
307  else
308  {
309  RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
310  assert( RetValue );
311  pVar->nScore -= pPart->nSize;
312  if ( Vec_IntSize(pVar->vParts) == 0 )
313  Llb_NonlinRemoveVar( p, pVar );
314  else if ( Vec_IntSize(pVar->vParts) == 1 )
315  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
316  }
317 
318  // update partition
319  pPart->nSize = nSizeNew;
320  Vec_IntClear( pPart->vVars );
321  for ( i = 0; i < p->nVars; i++ )
322  if ( p->pSupp[i] && p->pVars2Q[i] )
323  Vec_IntPush( pPart->vVars, i );
324  // remove other variables
325  Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
326  Llb_NonlinQuantify1( p, pTemp, 0 );
327  Vec_PtrFree( vSingles );
328  return 0;
329 }
330 
331 /**Function*************************************************************
332 
333  Synopsis [Quantifies singles belonging to one partition.]
334 
335  Description []
336 
337  SideEffects []
338 
339  SeeAlso []
340 
341 ***********************************************************************/
342 int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
343 {
344  int fVerbose = 0;
345  Llb_Var_t * pVar;
346  Llb_Prt_t * pTemp;
347  Vec_Ptr_t * vSingles;
348  DdNode * bCube, * bFunc;
349  int i, RetValue, nSuppSize;
350 // int iPart1 = pPart1->iPart;
351 // int iPart2 = pPart2->iPart;
352 
353  // create cube to be quantified
354  bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
355 if ( fVerbose )
356 {
357 printf( "\n" );
358 printf( "\n" );
359 Llb_NonlinPrint( p );
360 printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
361 Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
362 }
363 
364  // derive new function
365 // bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); Cudd_Ref( bFunc );
366 /*
367  bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );
368  if ( bFunc == NULL )
369  {
370  int RetValue;
371  Cudd_RecursiveDeref( p->dd, bCube );
372  if ( pPart1->nSize < pPart2->nSize )
373  RetValue = Llb_NonlinQuantify1( p, pPart1, 1 );
374  else
375  RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
376  if ( RetValue )
377  Limit = Limit + 1000;
378  Llb_NonlinQuantify2( p, pPart1, pPart2 );
379  return 0;
380  }
381  Cudd_Ref( bFunc );
382 */
383 
384 // bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut );
385  bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );
386  if ( bFunc == NULL )
387  {
388  Cudd_RecursiveDeref( p->dd, bCube );
389  return 0;
390  }
391  Cudd_Ref( bFunc );
392  Cudd_RecursiveDeref( p->dd, bCube );
393 
394  // create new partition
395  pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
396  pTemp->iPart = p->iPartFree++;
397  pTemp->nSize = Cudd_DagSize(bFunc);
398  pTemp->bFunc = bFunc;
399  pTemp->vVars = Vec_IntAlloc( 8 );
400  // update variables
401  Llb_PartForEachVar( p, pPart1, pVar, i )
402  {
403  RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
404  assert( RetValue );
405  pVar->nScore -= pPart1->nSize;
406  }
407  // update variables
408  Llb_PartForEachVar( p, pPart2, pVar, i )
409  {
410  RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
411  assert( RetValue );
412  pVar->nScore -= pPart2->nSize;
413  }
414  // add variables to the new partition
415  nSuppSize = 0;
416  Extra_SupportArray( p->dd, bFunc, p->pSupp );
417  for ( i = 0; i < p->nVars; i++ )
418  {
419  nSuppSize += p->pSupp[i];
420  if ( p->pSupp[i] && p->pVars2Q[i] )
421  {
422  pVar = Llb_MgrVar( p, i );
423  pVar->nScore += pTemp->nSize;
424  Vec_IntPush( pVar->vParts, pTemp->iPart );
425  Vec_IntPush( pTemp->vVars, i );
426  }
427  }
428  p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
429  // remove variables and collect partitions with singleton variables
430  vSingles = Vec_PtrAlloc( 0 );
431  Llb_PartForEachVar( p, pPart1, pVar, i )
432  {
433  if ( Vec_IntSize(pVar->vParts) == 0 )
434  Llb_NonlinRemoveVar( p, pVar );
435  else if ( Vec_IntSize(pVar->vParts) == 1 )
436  {
437  if ( fVerbose )
438  printf( "Adding partition %d because of var %d.\n",
439  Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
440  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
441  }
442  }
443  Llb_PartForEachVar( p, pPart2, pVar, i )
444  {
445  if ( pVar == NULL )
446  continue;
447  if ( Vec_IntSize(pVar->vParts) == 0 )
448  Llb_NonlinRemoveVar( p, pVar );
449  else if ( Vec_IntSize(pVar->vParts) == 1 )
450  {
451  if ( fVerbose )
452  printf( "Adding partition %d because of var %d.\n",
453  Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
454  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
455  }
456  }
457  // remove partitions
458  Llb_NonlinRemovePart( p, pPart1 );
459  Llb_NonlinRemovePart( p, pPart2 );
460  // remove other variables
461 if ( fVerbose )
462 Llb_NonlinPrint( p );
463  Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
464  {
465 if ( fVerbose )
466 printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
467  Llb_NonlinQuantify1( p, pTemp, 0 );
468  }
469 if ( fVerbose )
470 Llb_NonlinPrint( p );
471  Vec_PtrFree( vSingles );
472  return 1;
473 }
474 
475 /**Function*************************************************************
476 
477  Synopsis [Computes volume of the cut.]
478 
479  Description []
480 
481  SideEffects []
482 
483  SeeAlso []
484 
485 ***********************************************************************/
486 void Llb_NonlinCutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
487 {
488  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
489  return;
490  Aig_ObjSetTravIdCurrent(p, pObj);
491  if ( Saig_ObjIsLi(p, pObj) )
492  {
493  Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
494  return;
495  }
496  if ( Aig_ObjIsConst1(pObj) )
497  return;
498  assert( Aig_ObjIsNode(pObj) );
499  Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
500  Llb_NonlinCutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
501  Vec_PtrPush( vNodes, pObj );
502 }
503 
504 /**Function*************************************************************
505 
506  Synopsis [Computes volume of the cut.]
507 
508  Description []
509 
510  SideEffects []
511 
512  SeeAlso []
513 
514 ***********************************************************************/
515 Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
516 {
517  Vec_Ptr_t * vNodes;
518  Aig_Obj_t * pObj;
519  int i;
520  // mark the lower cut with the traversal ID
521  Aig_ManIncrementTravId(p);
522  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
523  Aig_ObjSetTravIdCurrent( p, pObj );
524  // count the upper cut
525  vNodes = Vec_PtrAlloc( 100 );
526  Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
527  Llb_NonlinCutNodes_rec( p, pObj, vNodes );
528  return vNodes;
529 }
530 
531 /**Function*************************************************************
532 
533  Synopsis [Returns array of BDDs for the roots in terms of the leaves.]
534 
535  Description []
536 
537  SideEffects []
538 
539  SeeAlso []
540 
541 ***********************************************************************/
542 Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
543 {
544  Vec_Ptr_t * vNodes, * vResult;
545  Aig_Obj_t * pObj;
546  DdNode * bBdd0, * bBdd1, * bProd;
547  int i, k;
548 
549  Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
550  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
551  pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
552 
553  vNodes = Llb_NonlinCutNodes( p, vLower, vUpper );
554  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
555  {
556  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
557  bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
558 // pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
559  pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
560  if ( pObj->pData == NULL )
561  {
562  Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
563  if ( pObj->pData )
564  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
565  Vec_PtrFree( vNodes );
566  return NULL;
567  }
568  Cudd_Ref( (DdNode *)pObj->pData );
569  }
570 
571  vResult = Vec_PtrAlloc( 100 );
572  Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
573  {
574  if ( Aig_ObjIsNode(pObj) )
575  {
576  bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
577  }
578  else
579  {
580  assert( Saig_ObjIsLi(p, pObj) );
581  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
582  bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), bBdd0 ); Cudd_Ref( bProd );
583  }
584  Vec_PtrPush( vResult, bProd );
585  }
586  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
587  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
588 
589  Vec_PtrFree( vNodes );
590  return vResult;
591 }
592 
593 /**Function*************************************************************
594 
595  Synopsis [Starts non-linear quantification scheduling.]
596 
597  Description []
598 
599  SideEffects []
600 
601  SeeAlso []
602 
603 ***********************************************************************/
604 void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
605 {
606  if ( p->pVars[iVar] == NULL )
607  {
608  p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
609  p->pVars[iVar]->iVar = iVar;
610  p->pVars[iVar]->nScore = 0;
611  p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
612  }
613  Vec_IntPush( p->pVars[iVar]->vParts, iPart );
614  Vec_IntPush( p->pParts[iPart]->vVars, iVar );
615 }
616 
617 /**Function*************************************************************
618 
619  Synopsis [Starts non-linear quantification scheduling.]
620 
621  Description []
622 
623  SideEffects []
624 
625  SeeAlso []
626 
627 ***********************************************************************/
628 void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
629 {
630  int k, nSuppSize;
631  assert( !Cudd_IsConstant(bFunc) );
632  // create partition
633  p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
634  p->pParts[i]->iPart = i;
635  p->pParts[i]->bFunc = bFunc;
636  p->pParts[i]->vVars = Vec_IntAlloc( 8 );
637  // add support dependencies
638  nSuppSize = 0;
639  Extra_SupportArray( p->dd, bFunc, p->pSupp );
640  for ( k = 0; k < p->nVars; k++ )
641  {
642  nSuppSize += p->pSupp[k];
643  if ( p->pSupp[k] && p->pVars2Q[k] )
644  Llb_NonlinAddPair( p, bFunc, i, k );
645  }
646  p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
647 }
648 
649 /**Function*************************************************************
650 
651  Synopsis [Starts non-linear quantification scheduling.]
652 
653  Description []
654 
655  SideEffects []
656 
657  SeeAlso []
658 
659 ***********************************************************************/
660 int Llb_NonlinStart( Llb_Mgr_t * p )
661 {
662  Vec_Ptr_t * vRootBdds;
663  DdNode * bFunc;
664  int i;
665  // create and collect BDDs
666  vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
667  if ( vRootBdds == NULL )
668  return 0;
669  // add pairs (refs are consumed inside)
670  Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
671  Llb_NonlinAddPartition( p, i, bFunc );
672  Vec_PtrFree( vRootBdds );
673  return 1;
674 }
675 
676 /**Function*************************************************************
677 
678  Synopsis [Checks that each var appears in at least one partition.]
679 
680  Description []
681 
682  SideEffects []
683 
684  SeeAlso []
685 **********************************************************************/
686 void Llb_NonlinCheckVars( Llb_Mgr_t * p )
687 {
688  Llb_Var_t * pVar;
689  int i;
690  Llb_MgrForEachVar( p, pVar, i )
691  assert( Vec_IntSize(pVar->vParts) > 1 );
692 }
693 
694 /**Function*************************************************************
695 
696  Synopsis [Find next partition to quantify]
697 
698  Description []
699 
700  SideEffects []
701 
702  SeeAlso []
703 
704 ***********************************************************************/
705 int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
706 {
707  Llb_Var_t * pVar, * pVarBest = NULL;
708  Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
709  int i;
710  Llb_NonlinCheckVars( p );
711  // find variable with minimum score
712  Llb_MgrForEachVar( p, pVar, i )
713  if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
714  pVarBest = pVar;
715  if ( pVarBest == NULL )
716  return 0;
717  // find two partitions with minimum size
718  Llb_VarForEachPart( p, pVarBest, pPart, i )
719  {
720  if ( pPart1Best == NULL )
721  pPart1Best = pPart;
722  else if ( pPart2Best == NULL )
723  pPart2Best = pPart;
724  else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
725  {
726  if ( pPart1Best->nSize > pPart2Best->nSize )
727  pPart1Best = pPart;
728  else
729  pPart2Best = pPart;
730  }
731  }
732  *ppPart1 = pPart1Best;
733  *ppPart2 = pPart2Best;
734  return 1;
735 }
736 
737 /**Function*************************************************************
738 
739  Synopsis [Reorders BDDs in the working manager.]
740 
741  Description []
742 
743  SideEffects []
744 
745  SeeAlso []
746 
747 ***********************************************************************/
748 void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose )
749 {
750  abctime clk = Abc_Clock();
751  if ( fVerbose )
752  Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
753  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
754  if ( fVerbose )
755  Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
756  if ( fTwice )
757  {
758  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
759  if ( fVerbose )
760  Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
761  }
762  if ( fVerbose )
763  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
764 }
765 
766 /**Function*************************************************************
767 
768  Synopsis [Recomputes scores after variable reordering.]
769 
770  Description []
771 
772  SideEffects []
773 
774  SeeAlso []
775 
776 ***********************************************************************/
777 void Llb_NonlinRecomputeScores( Llb_Mgr_t * p )
778 {
779  Llb_Prt_t * pPart;
780  Llb_Var_t * pVar;
781  int i, k;
782  Llb_MgrForEachPart( p, pPart, i )
783  pPart->nSize = Cudd_DagSize(pPart->bFunc);
784  Llb_MgrForEachVar( p, pVar, i )
785  {
786  pVar->nScore = 0;
787  Llb_VarForEachPart( p, pVar, pPart, k )
788  pVar->nScore += pPart->nSize;
789  }
790 }
791 
792 /**Function*************************************************************
793 
794  Synopsis [Recomputes scores after variable reordering.]
795 
796  Description []
797 
798  SideEffects []
799 
800  SeeAlso []
801 
802 ***********************************************************************/
803 void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
804 {
805  Llb_Prt_t * pPart;
806  Llb_Var_t * pVar;
807  int i, k, nScore;
808  Llb_MgrForEachPart( p, pPart, i )
809  assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
810  Llb_MgrForEachVar( p, pVar, i )
811  {
812  nScore = 0;
813  Llb_VarForEachPart( p, pVar, pPart, k )
814  nScore += pPart->nSize;
815  assert( nScore == pVar->nScore );
816  }
817 }
818 
819 /**Function*************************************************************
820 
821  Synopsis [Starts non-linear quantification scheduling.]
822 
823  Description []
824 
825  SideEffects []
826 
827  SeeAlso []
828 
829 ***********************************************************************/
830 Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd )
831 {
832  Llb_Mgr_t * p;
833  p = ABC_CALLOC( Llb_Mgr_t, 1 );
834  p->pAig = pAig;
835  p->vLeaves = vLeaves;
836  p->vRoots = vRoots;
837  p->dd = dd;
838  p->pVars2Q = pVars2Q;
839  p->nVars = Cudd_ReadSize(dd);
840  p->iPartFree = Vec_PtrSize(vRoots);
841  p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
842  p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
843  p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) );
844  return p;
845 }
846 
847 /**Function*************************************************************
848 
849  Synopsis [Stops non-linear quantification scheduling.]
850 
851  Description []
852 
853  SideEffects []
854 
855  SeeAlso []
856 
857 ***********************************************************************/
858 void Llb_NonlinFree( Llb_Mgr_t * p )
859 {
860  Llb_Prt_t * pPart;
861  Llb_Var_t * pVar;
862  int i;
863  Llb_MgrForEachVar( p, pVar, i )
864  Llb_NonlinRemoveVar( p, pVar );
865  Llb_MgrForEachPart( p, pPart, i )
866  Llb_NonlinRemovePart( p, pPart );
867  ABC_FREE( p->pVars );
868  ABC_FREE( p->pParts );
869  ABC_FREE( p->pSupp );
870  ABC_FREE( p );
871 }
872 
873 /**Function*************************************************************
874 
875  Synopsis [Performs image computation.]
876 
877  Description [Computes image of BDDs (vFuncs).]
878 
879  SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
880 
881  SeeAlso []
882 
883 ***********************************************************************/
884 DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
885  DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder )
886 {
887  Llb_Prt_t * pPart, * pPart1, * pPart2;
888  Llb_Mgr_t * p;
889  DdNode * bFunc, * bTemp;
890  int i, nReorders, timeInside;
891  abctime clk = Abc_Clock(), clk2;
892  // start the manager
893  clk2 = Abc_Clock();
894  p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
895  if ( !Llb_NonlinStart( p ) )
896  {
897  Llb_NonlinFree( p );
898  return NULL;
899  }
900  // add partition
901  Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
902  // remove singles
903  Llb_MgrForEachPart( p, pPart, i )
904  if ( Llb_NonlinHasSingletonVars(p, pPart) )
905  Llb_NonlinQuantify1( p, pPart, 0 );
906  timeBuild += Abc_Clock() - clk2;
907  timeInside = Abc_Clock() - clk2;
908  // compute scores
909  Llb_NonlinRecomputeScores( p );
910  // save permutation
911  if ( pOrder )
912  memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
913  // iteratively quantify variables
914  while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
915  {
916  clk2 = Abc_Clock();
917  nReorders = Cudd_ReadReorderings(dd);
918  if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
919  {
920  Llb_NonlinFree( p );
921  return NULL;
922  }
923  timeAndEx += Abc_Clock() - clk2;
924  timeInside += Abc_Clock() - clk2;
925  if ( nReorders < Cudd_ReadReorderings(dd) )
926  Llb_NonlinRecomputeScores( p );
927 // else
928 // Llb_NonlinVerifyScores( p );
929  }
930  // load partitions
931  bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
932  Llb_MgrForEachPart( p, pPart, i )
933  {
934  bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
935  Cudd_RecursiveDeref( p->dd, bTemp );
936  }
937  nSuppMax = p->nSuppMax;
938  Llb_NonlinFree( p );
939  // reorder variables
940  if ( fReorder )
941  Llb_NonlinReorder( dd, 0, fVerbose );
942  timeOther += Abc_Clock() - clk - timeInside;
943  // return
944  Cudd_Deref( bFunc );
945  return bFunc;
946 }
947 
948 
949 
950 static Llb_Mgr_t * p = NULL;
951 
952 /**Function*************************************************************
953 
954  Synopsis [Starts image computation manager.]
955 
956  Description []
957 
958  SideEffects []
959 
960  SeeAlso []
961 
962 ***********************************************************************/
963 DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, abctime TimeTarget )
964 {
965  DdManager * dd;
966  abctime clk = Abc_Clock();
967  assert( p == NULL );
968  // start a new manager (disable reordering)
969  dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
970  dd->TimeStop = TimeTarget;
971  Cudd_ShuffleHeap( dd, pOrder );
972 // if ( fFirst )
973  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
974  // start the manager
975  p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
976  if ( !Llb_NonlinStart( p ) )
977  {
978  Llb_NonlinFree( p );
979  p = NULL;
980  return NULL;
981  }
982  timeBuild += Abc_Clock() - clk;
983 // if ( !fFirst )
984 // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
985  return dd;
986 }
987 
988 /**Function*************************************************************
989 
990  Synopsis [Performs image computation.]
991 
992  Description []
993 
994  SideEffects []
995 
996  SeeAlso []
997 
998 ***********************************************************************/
999 DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder )
1000 {
1001  Llb_Prt_t * pPart, * pPart1, * pPart2;
1002  DdNode * bFunc, * bTemp;
1003  int i, nReorders, timeInside = 0;
1004  abctime clk = Abc_Clock(), clk2;
1005 
1006  // add partition
1007  Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
1008  // remove singles
1009  Llb_MgrForEachPart( p, pPart, i )
1010  if ( Llb_NonlinHasSingletonVars(p, pPart) )
1011  Llb_NonlinQuantify1( p, pPart, 0 );
1012  // reorder
1013  if ( fReorder )
1014  Llb_NonlinReorder( p->dd, 0, 0 );
1015  // save permutation
1016  memcpy( pOrder, p->dd->invperm, sizeof(int) * p->dd->size );
1017 
1018  // compute scores
1019  Llb_NonlinRecomputeScores( p );
1020  // iteratively quantify variables
1021  while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
1022  {
1023  clk2 = Abc_Clock();
1024  nReorders = Cudd_ReadReorderings(p->dd);
1025  if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
1026  {
1027  Llb_NonlinFree( p );
1028  return NULL;
1029  }
1030  timeAndEx += Abc_Clock() - clk2;
1031  timeInside += Abc_Clock() - clk2;
1032  if ( nReorders < Cudd_ReadReorderings(p->dd) )
1033  Llb_NonlinRecomputeScores( p );
1034 // else
1035 // Llb_NonlinVerifyScores( p );
1036  }
1037  // load partitions
1038  bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
1039  Llb_MgrForEachPart( p, pPart, i )
1040  {
1041  bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );
1042  if ( bFunc == NULL )
1043  {
1044  Cudd_RecursiveDeref( p->dd, bTemp );
1045  Llb_NonlinFree( p );
1046  return NULL;
1047  }
1048  Cudd_Ref( bFunc );
1049  Cudd_RecursiveDeref( p->dd, bTemp );
1050  }
1051  nSuppMax = p->nSuppMax;
1052  // reorder variables
1053 // if ( fReorder )
1054 // Llb_NonlinReorder( p->dd, 0, fVerbose );
1055  // save permutation
1056 // memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) );
1057 
1058  timeOther += Abc_Clock() - clk - timeInside;
1059  // return
1060  Cudd_Deref( bFunc );
1061  return bFunc;
1062 }
1063 
1064 /**Function*************************************************************
1065 
1066  Synopsis [Quits image computation manager.]
1067 
1068  Description []
1069 
1070  SideEffects []
1071 
1072  SeeAlso []
1073 
1074 ***********************************************************************/
1075 void Llb_NonlinImageQuit()
1076 {
1077  DdManager * dd;
1078  if ( p == NULL )
1079  return;
1080  dd = p->dd;
1081  Llb_NonlinFree( p );
1082  if ( dd->bFunc )
1083  Cudd_RecursiveDeref( dd, dd->bFunc );
1084  Extra_StopManager( dd );
1085 // Cudd_Quit ( dd );
1086  p = NULL;
1087 }
1088 
1089 ////////////////////////////////////////////////////////////////////////
1090 /// END OF FILE ///
1091 ////////////////////////////////////////////////////////////////////////
1092 
1093 
1094 ABC_NAMESPACE_IMPL_END
1095 
Llb_Mgr_t_::pParts
Llb_Prt_t ** pParts
Definition: llb3Image.c:55
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
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Llb_NonlinImageStart
DdManager * Llb_NonlinImageStart(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, int *pOrder, int fFirst, abctime TimeTarget)
Definition: llb3Image.c:963
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Llb_Prt_t_
Definition: llb3Image.c:38
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
Llb_Var_t_
Definition: llb3Image.c:30
Llb_MgrPart
static Llb_Prt_t * Llb_MgrPart(Llb_Mgr_t *p, int i)
Definition: llb3Image.c:65
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Llb_NonlinImageQuit
void Llb_NonlinImageQuit()
Definition: llb3Image.c:1075
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Llb_Var_t_::iVar
int iVar
Definition: llb3Image.c:32
Llb_NonlinQuantify2
int Llb_NonlinQuantify2(Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
Definition: llb3Image.c:342
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
timeAndEx
abctime timeAndEx
Definition: llb3Image.c:82
Llb_NonlinCreateCube1
DdNode * Llb_NonlinCreateCube1(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb3Image.c:139
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_ReadReorderings
int Cudd_ReadReorderings(DdManager *dd)
Definition: cuddAPI.c:1696
Llb_Mgr_t_::pVars2Q
int * pVars2Q
Definition: llb3Image.c:53
DdManager::size
int size
Definition: cuddInt.h:361
Llb_Mgr_t_::pSupp
int * pSupp
Definition: llb3Image.c:61
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Llb_NonlinAddPair
void Llb_NonlinAddPair(Llb_Mgr_t *p, DdNode *bFunc, int iPart, int iVar)
Definition: llb3Image.c:604
timeBuild
abctime timeBuild
Definition: llb3Image.c:82
Extra_bddPrintSupport
void Extra_bddPrintSupport(DdManager *dd, DdNode *F)
Definition: extraBddMisc.c:302
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Llb_Mgr_t_::vRoots
Vec_Ptr_t * vRoots
Definition: llb3Image.c:51
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Llb_NonlinRecomputeScores
void Llb_NonlinRecomputeScores(Llb_Mgr_t *p)
Definition: llb3Image.c:777
memcpy
char * memcpy()
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
timeOther
abctime timeOther
Definition: llb3Image.c:82
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Llb_NonlinRemovePart
void Llb_NonlinRemovePart(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb3Image.c:119
Llb_Mgr_t_::nSuppMax
int nSuppMax
Definition: llb3Image.c:59
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
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
nSuppMax
int nSuppMax
Definition: llb3Image.c:83
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Llb_NonlinCreateCube2
DdNode * Llb_NonlinCreateCube2(Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
Definition: llb3Image.c:172
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_MgrVar
static Llb_Var_t * Llb_MgrVar(Llb_Mgr_t *p, int i)
Definition: llb3Image.c:64
Cudd_LargestCube
DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length)
Definition: cuddSat.c:285
Llb_MgrForEachVar
#define Llb_MgrForEachVar(p, pVar, i)
Definition: llb3Image.c:68
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Llb_NonlinPrint
void Llb_NonlinPrint(Llb_Mgr_t *p)
Definition: llb3Image.c:229
Llb_NonlinAlloc
Llb_Mgr_t * Llb_NonlinAlloc(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd)
Definition: llb3Image.c:830
Llb_Prt_t_::nSize
int nSize
Definition: llb3Image.c:41
Llb_Var_t
typedefABC_NAMESPACE_IMPL_START struct Llb_Var_t_ Llb_Var_t
DECLARATIONS ///.
Definition: llb3Image.c:29
Llb_NonlinHasSingletonVars
int Llb_NonlinHasSingletonVars(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb3Image.c:208
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cudd_ShuffleHeap
int Cudd_ShuffleHeap(DdManager *table, int *permutation)
Definition: cuddReorder.c:338
Llb_NonlinBuildBdds
Vec_Ptr_t * Llb_NonlinBuildBdds(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, DdManager *dd)
Definition: llb3Image.c:542
Extra_SupportArray
int * Extra_SupportArray(DdManager *dd, DdNode *F, int *support)
Definition: extraBddMisc.c:537
Llb_NonlinCutNodes_rec
void Llb_NonlinCutNodes_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: llb3Image.c:486
Llb_NonlinCheckVars
void Llb_NonlinCheckVars(Llb_Mgr_t *p)
Definition: llb3Image.c:686
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Llb_MgrForEachPart
#define Llb_MgrForEachPart(p, pPart, i)
Definition: llb3Image.c:71
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Llb_Mgr_t_::pVars
Llb_Var_t ** pVars
Definition: llb3Image.c:56
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
Llb_Var_t_::nScore
int nScore
Definition: llb3Image.c:33
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Llb_VarForEachPart
#define Llb_VarForEachPart(p, pVar, pPart, i)
Definition: llb3Image.c:78
Llb_Mgr_t_::iPartFree
int iPartFree
Definition: llb3Image.c:57
Llb_NonlinImage
DdNode * Llb_NonlinImage(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd, DdNode *bCurrent, int fReorder, int fVerbose, int *pOrder)
Definition: llb3Image.c:884
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Llb_NonlinNextPartitions
int Llb_NonlinNextPartitions(Llb_Mgr_t *p, Llb_Prt_t **ppPart1, Llb_Prt_t **ppPart2)
Definition: llb3Image.c:705
Vec_IntRemove
static int Vec_IntRemove(Vec_Int_t *p, int Entry)
Definition: vecInt.h:915
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_Prt_t_::iPart
int iPart
Definition: llb3Image.c:40
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Llb_Mgr_t_::vLeaves
Vec_Ptr_t * vLeaves
Definition: llb3Image.c:50
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Llb_Prt_t_::bFunc
DdNode * bFunc
Definition: llb3Image.c:42
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition: vecPtr.h:59
Llb_PartForEachVar
#define Llb_PartForEachVar(p, pPart, pVar, i)
Definition: llb3Image.c:75
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
Llb_NonlinFree
void Llb_NonlinFree(Llb_Mgr_t *p)
Definition: llb3Image.c:858
Llb_NonlinCutNodes
Vec_Ptr_t * Llb_NonlinCutNodes(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
Definition: llb3Image.c:515
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
Llb_Var_t_::vParts
Vec_Int_t * vParts
Definition: llb3Image.c:34
Llb_NonlinQuantify1
int Llb_NonlinQuantify1(Llb_Mgr_t *p, Llb_Prt_t *pPart, int fSubset)
Definition: llb3Image.c:262
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_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Llb_NonlinStart
int Llb_NonlinStart(Llb_Mgr_t *p)
Definition: llb3Image.c:660
Llb_NonlinReorder
void Llb_NonlinReorder(DdManager *dd, int fTwice, int fVerbose)
Definition: llb3Image.c:748
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
Llb_NonlinAddPartition
void Llb_NonlinAddPartition(Llb_Mgr_t *p, int i, DdNode *bFunc)
Definition: llb3Image.c:628
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
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
Llb_NonlinRemoveVar
void Llb_NonlinRemoveVar(Llb_Mgr_t *p, Llb_Var_t *pVar)
FUNCTION DEFINITIONS ///.
Definition: llb3Image.c:100
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Llb_NonlinImageCompute
DdNode * Llb_NonlinImageCompute(DdNode *bCurrent, int fReorder, int fDrop, int fVerbose, int *pOrder)
Definition: llb3Image.c:999
Llb_Prt_t_::vVars
Vec_Int_t * vVars
Definition: llb3Image.c:43
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Llb_Mgr_t_::nVars
int nVars
Definition: llb3Image.c:58
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Llb_Mgr_t_
Definition: llb3Image.c:47
Llb_NonlinVerifyScores
void Llb_NonlinVerifyScores(Llb_Mgr_t *p)
Definition: llb3Image.c:803