abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb4Image.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  DdManager * dd; // working BDD manager
50  Vec_Int_t * vVars2Q; // variables to quantify
51  int nSizeMax; // maximum size of the cluster
52  // internal
53  Llb_Prt_t ** pParts; // partitions
54  Llb_Var_t ** pVars; // variables
55  int iPartFree; // next free partition
56  int nVars; // the number of BDD variables
57  int nSuppMax; // maximum support size
58  // temporary
59  int * pSupp; // temporary support storage
60 };
61 
62 static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i ) { return p->pVars[i]; }
63 static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pParts[i]; }
64 
65 // iterator over vars
66 #define Llb_MgrForEachVar( p, pVar, i ) \
67  for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
68 // iterator over parts
69 #define Llb_MgrForEachPart( p, pPart, i ) \
70  for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
71 
72 // iterator over vars of one partition
73 #define Llb_PartForEachVar( p, pPart, pVar, i ) \
74  for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
75 // iterator over parts of one variable
76 #define Llb_VarForEachPart( p, pVar, pPart, i ) \
77  for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
78 
79 // statistics
80 //abctime timeBuild, timeAndEx, timeOther;
81 //int nSuppMax;
82 
83 ////////////////////////////////////////////////////////////////////////
84 /// FUNCTION DEFINITIONS ///
85 ////////////////////////////////////////////////////////////////////////
86 
87 /**Function*************************************************************
88 
89  Synopsis [Removes one variable.]
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 void Llb_Nonlin4RemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
99 {
100  assert( p->pVars[pVar->iVar] == pVar );
101  p->pVars[pVar->iVar] = NULL;
102  Vec_IntFree( pVar->vParts );
103  ABC_FREE( pVar );
104 }
105 
106 /**Function*************************************************************
107 
108  Synopsis [Removes one partition.]
109 
110  Description []
111 
112  SideEffects []
113 
114  SeeAlso []
115 
116 ***********************************************************************/
117 void Llb_Nonlin4RemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
118 {
119 //printf( "Removing %d\n", pPart->iPart );
120  assert( p->pParts[pPart->iPart] == pPart );
121  p->pParts[pPart->iPart] = NULL;
122  Vec_IntFree( pPart->vVars );
123  Cudd_RecursiveDeref( p->dd, pPart->bFunc );
124  ABC_FREE( pPart );
125 }
126 
127 /**Function*************************************************************
128 
129  Synopsis [Create cube with singleton variables.]
130 
131  Description []
132 
133  SideEffects []
134 
135  SeeAlso []
136 
137 ***********************************************************************/
138 DdNode * Llb_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
139 {
140  DdNode * bCube, * bTemp;
141  Llb_Var_t * pVar;
142  int i;
143  abctime TimeStop;
144  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
145  bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
146  Llb_PartForEachVar( p, pPart, pVar, i )
147  {
148  assert( Vec_IntSize(pVar->vParts) > 0 );
149  if ( Vec_IntSize(pVar->vParts) != 1 )
150  continue;
151  assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
152  bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
153  Cudd_RecursiveDeref( p->dd, bTemp );
154  }
155  Cudd_Deref( bCube );
156  p->dd->TimeStop = TimeStop;
157  return bCube;
158 }
159 
160 /**Function*************************************************************
161 
162  Synopsis [Create cube of variables appearing only in two partitions.]
163 
164  Description []
165 
166  SideEffects []
167 
168  SeeAlso []
169 
170 ***********************************************************************/
171 DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
172 {
173  DdNode * bCube, * bTemp;
174  Llb_Var_t * pVar;
175  int i;
176  abctime TimeStop;
177  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
178  bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
179  Llb_PartForEachVar( p, pPart1, pVar, i )
180  {
181  assert( Vec_IntSize(pVar->vParts) > 0 );
182  if ( Vec_IntSize(pVar->vParts) != 2 )
183  continue;
184  if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
185  (Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
186  {
187  bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
188  Cudd_RecursiveDeref( p->dd, bTemp );
189  }
190  }
191  Cudd_Deref( bCube );
192  p->dd->TimeStop = TimeStop;
193  return bCube;
194 }
195 
196 /**Function*************************************************************
197 
198  Synopsis [Returns 1 if partition has singleton variables.]
199 
200  Description []
201 
202  SideEffects []
203 
204  SeeAlso []
205 
206 ***********************************************************************/
207 int Llb_Nonlin4HasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
208 {
209  Llb_Var_t * pVar;
210  int i;
211  Llb_PartForEachVar( p, pPart, pVar, i )
212  if ( Vec_IntSize(pVar->vParts) == 1 )
213  return 1;
214  return 0;
215 }
216 
217 /**Function*************************************************************
218 
219  Synopsis [Returns 1 if partition has singleton variables.]
220 
221  Description []
222 
223  SideEffects []
224 
225  SeeAlso []
226 
227 ***********************************************************************/
228 void Llb_Nonlin4Print( Llb_Mgr_t * p )
229 {
230  Llb_Prt_t * pPart;
231  Llb_Var_t * pVar;
232  int i, k;
233  printf( "\n" );
234  Llb_MgrForEachVar( p, pVar, i )
235  {
236  printf( "Var %3d : ", i );
237  Llb_VarForEachPart( p, pVar, pPart, k )
238  printf( "%d ", pPart->iPart );
239  printf( "\n" );
240  }
241  Llb_MgrForEachPart( p, pPart, i )
242  {
243  printf( "Part %3d : ", i );
244  Llb_PartForEachVar( p, pPart, pVar, k )
245  printf( "%d ", pVar->iVar );
246  printf( "\n" );
247  }
248 }
249 
250 /**Function*************************************************************
251 
252  Synopsis [Quantifies singles belonging to one partition.]
253 
254  Description []
255 
256  SideEffects []
257 
258  SeeAlso []
259 
260 ***********************************************************************/
261 int Llb_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
262 {
263  Llb_Var_t * pVar;
264  Llb_Prt_t * pTemp;
265  Vec_Ptr_t * vSingles;
266  DdNode * bCube, * bTemp;
267  int i, RetValue, nSizeNew;
268  // create cube to be quantified
269  bCube = Llb_Nonlin4CreateCube1( p, pPart ); Cudd_Ref( bCube );
270 // assert( !Cudd_IsConstant(bCube) );
271  // derive new function
272  pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc );
273  Cudd_RecursiveDeref( p->dd, bTemp );
274  Cudd_RecursiveDeref( p->dd, bCube );
275  // get support
276  vSingles = Vec_PtrAlloc( 0 );
277  nSizeNew = Cudd_DagSize(pPart->bFunc);
278  Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
279  Llb_PartForEachVar( p, pPart, pVar, i )
280  if ( p->pSupp[pVar->iVar] )
281  {
282  assert( Vec_IntSize(pVar->vParts) > 1 );
283  pVar->nScore -= pPart->nSize - nSizeNew;
284  }
285  else
286  {
287  RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
288  assert( RetValue );
289  pVar->nScore -= pPart->nSize;
290  if ( Vec_IntSize(pVar->vParts) == 0 )
291  Llb_Nonlin4RemoveVar( p, pVar );
292  else if ( Vec_IntSize(pVar->vParts) == 1 )
293  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
294  }
295 
296  // update partition
297  pPart->nSize = nSizeNew;
298  Vec_IntClear( pPart->vVars );
299  for ( i = 0; i < p->nVars; i++ )
300  if ( p->pSupp[i] && Vec_IntEntry(p->vVars2Q, i) )
301  Vec_IntPush( pPart->vVars, i );
302  // remove other variables
303  Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
304  Llb_Nonlin4Quantify1( p, pTemp );
305  Vec_PtrFree( vSingles );
306  return 0;
307 }
308 
309 /**Function*************************************************************
310 
311  Synopsis [Quantifies singles belonging to one partition.]
312 
313  Description []
314 
315  SideEffects []
316 
317  SeeAlso []
318 
319 ***********************************************************************/
320 int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
321 {
322  int fVerbose = 0;
323  Llb_Var_t * pVar;
324  Llb_Prt_t * pTemp;
325  Vec_Ptr_t * vSingles;
326  DdNode * bCube, * bFunc;
327  int i, RetValue, nSuppSize;
328 // int iPart1 = pPart1->iPart;
329 // int iPart2 = pPart2->iPart;
330  int liveBeg, liveEnd;
331 
332  // create cube to be quantified
333  bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
334 
335 //printf( "Quantifying " ); Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
336 
337 if ( fVerbose )
338 {
339 printf( "\n" );
340 printf( "\n" );
341 Llb_Nonlin4Print( p );
342 printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
343 Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
344 }
345 liveBeg = p->dd->keys - p->dd->dead;
346  bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );
347 liveEnd = p->dd->keys - p->dd->dead;
348 //printf( "%d ", liveEnd-liveBeg );
349 
350  if ( bFunc == NULL )
351  {
352  Cudd_RecursiveDeref( p->dd, bCube );
353  return 0;
354  }
355  Cudd_Ref( bFunc );
356  Cudd_RecursiveDeref( p->dd, bCube );
357 
358 //printf( "Creating part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc ); printf( "\n" );
359 
360 //printf( "Creating %d\n", p->iPartFree );
361 
362  // create new partition
363  pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
364  pTemp->iPart = p->iPartFree++;
365  pTemp->nSize = Cudd_DagSize(bFunc);
366  pTemp->bFunc = bFunc;
367  pTemp->vVars = Vec_IntAlloc( 8 );
368  // update variables
369  Llb_PartForEachVar( p, pPart1, pVar, i )
370  {
371  RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
372  assert( RetValue );
373  pVar->nScore -= pPart1->nSize;
374  }
375  // update variables
376  Llb_PartForEachVar( p, pPart2, pVar, i )
377  {
378  RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
379  assert( RetValue );
380  pVar->nScore -= pPart2->nSize;
381  }
382  // add variables to the new partition
383  nSuppSize = 0;
384  Extra_SupportArray( p->dd, bFunc, p->pSupp );
385  for ( i = 0; i < p->nVars; i++ )
386  {
387  nSuppSize += p->pSupp[i];
388  if ( p->pSupp[i] && Vec_IntEntry(p->vVars2Q, i) )
389  {
390  pVar = Llb_MgrVar( p, i );
391  pVar->nScore += pTemp->nSize;
392  Vec_IntPush( pVar->vParts, pTemp->iPart );
393  Vec_IntPush( pTemp->vVars, i );
394  }
395  }
396  p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
397  // remove variables and collect partitions with singleton variables
398  vSingles = Vec_PtrAlloc( 0 );
399  Llb_PartForEachVar( p, pPart1, pVar, i )
400  {
401  if ( Vec_IntSize(pVar->vParts) == 0 )
402  Llb_Nonlin4RemoveVar( p, pVar );
403  else if ( Vec_IntSize(pVar->vParts) == 1 )
404  {
405  if ( fVerbose )
406  printf( "Adding partition %d because of var %d.\n",
407  Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
408  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
409  }
410  }
411  Llb_PartForEachVar( p, pPart2, pVar, i )
412  {
413  if ( pVar == NULL )
414  continue;
415  if ( Vec_IntSize(pVar->vParts) == 0 )
416  Llb_Nonlin4RemoveVar( p, pVar );
417  else if ( Vec_IntSize(pVar->vParts) == 1 )
418  {
419  if ( fVerbose )
420  printf( "Adding partition %d because of var %d.\n",
421  Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
422  Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
423  }
424  }
425  // remove partitions
426  Llb_Nonlin4RemovePart( p, pPart1 );
427  Llb_Nonlin4RemovePart( p, pPart2 );
428  // remove other variables
429 if ( fVerbose )
430 Llb_Nonlin4Print( p );
431  Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
432  {
433 if ( fVerbose )
434 printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
435  Llb_Nonlin4Quantify1( p, pTemp );
436  }
437 if ( fVerbose )
438 Llb_Nonlin4Print( p );
439  Vec_PtrFree( vSingles );
440  return 1;
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Computes volume of the cut.]
446 
447  Description []
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 void Llb_Nonlin4CutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
455 {
456  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
457  return;
458  Aig_ObjSetTravIdCurrent(p, pObj);
459  if ( Saig_ObjIsLi(p, pObj) )
460  {
461  Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
462  return;
463  }
464  if ( Aig_ObjIsConst1(pObj) )
465  return;
466  assert( Aig_ObjIsNode(pObj) );
467  Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
468  Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
469  Vec_PtrPush( vNodes, pObj );
470 }
471 
472 /**Function*************************************************************
473 
474  Synopsis [Computes volume of the cut.]
475 
476  Description []
477 
478  SideEffects []
479 
480  SeeAlso []
481 
482 ***********************************************************************/
483 Vec_Ptr_t * Llb_Nonlin4CutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
484 {
485  Vec_Ptr_t * vNodes;
486  Aig_Obj_t * pObj;
487  int i;
488  // mark the lower cut with the traversal ID
489  Aig_ManIncrementTravId(p);
490  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
491  Aig_ObjSetTravIdCurrent( p, pObj );
492  // count the upper cut
493  vNodes = Vec_PtrAlloc( 100 );
494  Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
495  Llb_Nonlin4CutNodes_rec( p, pObj, vNodes );
496  return vNodes;
497 }
498 
499 /**Function*************************************************************
500 
501  Synopsis [Starts non-linear quantification scheduling.]
502 
503  Description []
504 
505  SideEffects []
506 
507  SeeAlso []
508 
509 ***********************************************************************/
510 void Llb_Nonlin4AddPair( Llb_Mgr_t * p, int iPart, int iVar )
511 {
512  if ( p->pVars[iVar] == NULL )
513  {
514  p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
515  p->pVars[iVar]->iVar = iVar;
516  p->pVars[iVar]->nScore = 0;
517  p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
518  }
519  Vec_IntPush( p->pVars[iVar]->vParts, iPart );
520  Vec_IntPush( p->pParts[iPart]->vVars, iVar );
521 }
522 
523 /**Function*************************************************************
524 
525  Synopsis [Starts non-linear quantification scheduling.]
526 
527  Description []
528 
529  SideEffects []
530 
531  SeeAlso []
532 
533 ***********************************************************************/
534 void Llb_Nonlin4AddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
535 {
536  int k, nSuppSize;
537  assert( !Cudd_IsConstant(bFunc) );
538 //printf( "Creating init %d\n", i );
539  // create partition
540  p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
541  p->pParts[i]->iPart = i;
542  p->pParts[i]->bFunc = bFunc; Cudd_Ref( bFunc );
543  p->pParts[i]->vVars = Vec_IntAlloc( 8 );
544  // add support dependencies
545  nSuppSize = 0;
546  Extra_SupportArray( p->dd, bFunc, p->pSupp );
547  for ( k = 0; k < p->nVars; k++ )
548  {
549  nSuppSize += p->pSupp[k];
550  if ( p->pSupp[k] && Vec_IntEntry(p->vVars2Q, k) )
551  Llb_Nonlin4AddPair( p, i, k );
552  }
553  p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
554 }
555 
556 /**Function*************************************************************
557 
558  Synopsis [Checks that each var appears in at least one partition.]
559 
560  Description []
561 
562  SideEffects []
563 
564  SeeAlso []
565 **********************************************************************/
566 void Llb_Nonlin4CheckVars( Llb_Mgr_t * p )
567 {
568  Llb_Var_t * pVar;
569  int i;
570  Llb_MgrForEachVar( p, pVar, i )
571  assert( Vec_IntSize(pVar->vParts) > 1 );
572 }
573 
574 /**Function*************************************************************
575 
576  Synopsis [Find next partition to quantify]
577 
578  Description []
579 
580  SideEffects []
581 
582  SeeAlso []
583 
584 ***********************************************************************/
585 int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
586 {
587  Llb_Var_t * pVar, * pVarBest = NULL;
588  Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
589  int i;
590  Llb_Nonlin4CheckVars( p );
591  // find variable with minimum score
592  Llb_MgrForEachVar( p, pVar, i )
593  {
594  if ( p->nSizeMax && pVar->nScore > p->nSizeMax )
595  continue;
596 // if ( pVarBest == NULL || Vec_IntSize(pVarBest->vParts) * pVarBest->nScore > Vec_IntSize(pVar->vParts) * pVar->nScore )
597  if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
598  pVarBest = pVar;
599 // printf( "%d ", pVar->nScore );
600  }
601 //printf( "\n" );
602  if ( pVarBest == NULL )
603  return 0;
604  // find two partitions with minimum size
605  Llb_VarForEachPart( p, pVarBest, pPart, i )
606  {
607  if ( pPart1Best == NULL )
608  pPart1Best = pPart;
609  else if ( pPart2Best == NULL )
610  pPart2Best = pPart;
611  else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
612  {
613  if ( pPart1Best->nSize > pPart2Best->nSize )
614  pPart1Best = pPart;
615  else
616  pPart2Best = pPart;
617  }
618  }
619 //printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
620 //Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
621 //Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
622 
623  *ppPart1 = pPart1Best;
624  *ppPart2 = pPart2Best;
625  return 1;
626 }
627 
628 /**Function*************************************************************
629 
630  Synopsis [Recomputes scores after variable reordering.]
631 
632  Description []
633 
634  SideEffects []
635 
636  SeeAlso []
637 
638 ***********************************************************************/
639 void Llb_Nonlin4RecomputeScores( Llb_Mgr_t * p )
640 {
641  Llb_Prt_t * pPart;
642  Llb_Var_t * pVar;
643  int i, k;
644  Llb_MgrForEachPart( p, pPart, i )
645  pPart->nSize = Cudd_DagSize(pPart->bFunc);
646  Llb_MgrForEachVar( p, pVar, i )
647  {
648  pVar->nScore = 0;
649  Llb_VarForEachPart( p, pVar, pPart, k )
650  pVar->nScore += pPart->nSize;
651  }
652 }
653 
654 /**Function*************************************************************
655 
656  Synopsis [Recomputes scores after variable reordering.]
657 
658  Description []
659 
660  SideEffects []
661 
662  SeeAlso []
663 
664 ***********************************************************************/
665 void Llb_Nonlin4VerifyScores( Llb_Mgr_t * p )
666 {
667  Llb_Prt_t * pPart;
668  Llb_Var_t * pVar;
669  int i, k, nScore;
670  Llb_MgrForEachPart( p, pPart, i )
671  assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
672  Llb_MgrForEachVar( p, pVar, i )
673  {
674  nScore = 0;
675  Llb_VarForEachPart( p, pVar, pPart, k )
676  nScore += pPart->nSize;
677  assert( nScore == pVar->nScore );
678  }
679 }
680 
681 /**Function*************************************************************
682 
683  Synopsis [Starts non-linear quantification scheduling.]
684 
685  Description []
686 
687  SideEffects []
688 
689  SeeAlso []
690 
691 ***********************************************************************/
692 Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q, int nSizeMax )
693 {
694  Llb_Mgr_t * p;
695  DdNode * bFunc;
696  int i;
697  p = ABC_CALLOC( Llb_Mgr_t, 1 );
698  p->dd = dd;
699  p->nSizeMax = nSizeMax;
700  p->vVars2Q = vVars2Q;
701  p->nVars = Cudd_ReadSize(dd);
702  p->iPartFree = Vec_PtrSize(vParts);
703  p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
704  p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
705  p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) );
706  // add pairs (refs are consumed inside)
707  Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
708  Llb_Nonlin4AddPartition( p, i, bFunc );
709  // add partition
710  if ( bCurrent )
711  Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
712  return p;
713 }
714 
715 /**Function*************************************************************
716 
717  Synopsis [Stops non-linear quantification scheduling.]
718 
719  Description []
720 
721  SideEffects []
722 
723  SeeAlso []
724 
725 ***********************************************************************/
726 void Llb_Nonlin4Free( Llb_Mgr_t * p )
727 {
728  Llb_Prt_t * pPart;
729  Llb_Var_t * pVar;
730  int i;
731  Llb_MgrForEachVar( p, pVar, i )
732  Llb_Nonlin4RemoveVar( p, pVar );
733  Llb_MgrForEachPart( p, pPart, i )
734  Llb_Nonlin4RemovePart( p, pPart );
735  ABC_FREE( p->pVars );
736  ABC_FREE( p->pParts );
737  ABC_FREE( p->pSupp );
738  ABC_FREE( p );
739 }
740 
741 /**Function*************************************************************
742 
743  Synopsis []
744 
745  Description []
746 
747  SideEffects []
748 
749  SeeAlso []
750 
751 ***********************************************************************/
752 DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
753 {
754  Llb_Prt_t * pPart, * pPart1, * pPart2;
755  Llb_Mgr_t * p;
756  DdNode * bFunc, * bTemp;
757  int i, nReorders;
758  // start the manager
759  p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q, 0 );
760  // remove singles
761  Llb_MgrForEachPart( p, pPart, i )
762  if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
763  Llb_Nonlin4Quantify1( p, pPart );
764  // compute scores
765  Llb_Nonlin4RecomputeScores( p );
766  // iteratively quantify variables
767  while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
768  {
769  nReorders = Cudd_ReadReorderings(dd);
770  if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
771  {
772  Llb_Nonlin4Free( p );
773  return NULL;
774  }
775  if ( nReorders < Cudd_ReadReorderings(dd) )
776  Llb_Nonlin4RecomputeScores( p );
777 // else
778 // Llb_Nonlin4VerifyScores( p );
779  }
780  // load partitions
781  bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
782  Llb_MgrForEachPart( p, pPart, i )
783  {
784  bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
785  Cudd_RecursiveDeref( p->dd, bTemp );
786  }
787 // nSuppMax = p->nSuppMax;
788  Llb_Nonlin4Free( p );
789 //printf( "\n" );
790  // return
791  Cudd_Deref( bFunc );
792  return bFunc;
793 }
794 
795 /**Function*************************************************************
796 
797  Synopsis []
798 
799  Description []
800 
801  SideEffects []
802 
803  SeeAlso []
804 
805 ***********************************************************************/
806 Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax )
807 {
808  Vec_Ptr_t * vGroups;
809  Llb_Prt_t * pPart, * pPart1, * pPart2;
810  Llb_Mgr_t * p;
811  int i, nReorders;//, clk = Abc_Clock();
812  // start the manager
813  p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
814  // remove singles
815  Llb_MgrForEachPart( p, pPart, i )
816  if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
817  Llb_Nonlin4Quantify1( p, pPart );
818  // compute scores
819  Llb_Nonlin4RecomputeScores( p );
820  // iteratively quantify variables
821  while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
822  {
823  nReorders = Cudd_ReadReorderings(dd);
824  if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
825  {
826  Llb_Nonlin4Free( p );
827  return NULL;
828  }
829  if ( nReorders < Cudd_ReadReorderings(dd) )
830  Llb_Nonlin4RecomputeScores( p );
831 // else
832 // Llb_Nonlin4VerifyScores( p );
833  }
834  // load partitions
835  vGroups = Vec_PtrAlloc( 1000 );
836  Llb_MgrForEachPart( p, pPart, i )
837  {
838 //printf( "Iteration %d ", pPart->iPart );
839  if ( Cudd_IsConstant(pPart->bFunc) )
840  {
841 //printf( "Constant\n" );
842  assert( !Cudd_IsComplement(pPart->bFunc) );
843  continue;
844  }
845 //printf( "\n" );
846  Vec_PtrPush( vGroups, pPart->bFunc );
847  Cudd_Ref( pPart->bFunc );
848 //printf( "Part %d ", pPart->iPart );
849 //Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
850  }
851  Llb_Nonlin4Free( p );
852 //Abc_PrintTime( 1, "Reparametrization time", Abc_Clock() - clk );
853  return vGroups;
854 }
855 
856 
857 ////////////////////////////////////////////////////////////////////////
858 /// END OF FILE ///
859 ////////////////////////////////////////////////////////////////////////
860 
861 
862 ABC_NAMESPACE_IMPL_END
863 
Llb_Nonlin4CreateCube1
DdNode * Llb_Nonlin4CreateCube1(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb4Image.c:138
Llb_Nonlin4Free
void Llb_Nonlin4Free(Llb_Mgr_t *p)
Definition: llb4Image.c:726
Llb_Nonlin4RemovePart
void Llb_Nonlin4RemovePart(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb4Image.c:117
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
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
Llb_Nonlin4CutNodes_rec
void Llb_Nonlin4CutNodes_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: llb4Image.c:454
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
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Llb_Var_t_::iVar
int iVar
Definition: llb3Image.c:32
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
Llb_MgrVar
static Llb_Var_t * Llb_MgrVar(Llb_Mgr_t *p, int i)
Definition: llb4Image.c:62
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_::pSupp
int * pSupp
Definition: llb3Image.c:61
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
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
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Llb_Nonlin4AddPartition
void Llb_Nonlin4AddPartition(Llb_Mgr_t *p, int i, DdNode *bFunc)
Definition: llb4Image.c:534
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Llb_Mgr_t_::nSuppMax
int nSuppMax
Definition: llb3Image.c:59
Llb_Mgr_t_::nSizeMax
int nSizeMax
Definition: llb4Image.c:51
Llb_Nonlin4VerifyScores
void Llb_Nonlin4VerifyScores(Llb_Mgr_t *p)
Definition: llb4Image.c:665
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
Llb_MgrPart
static Llb_Prt_t * Llb_MgrPart(Llb_Mgr_t *p, int i)
Definition: llb4Image.c:63
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
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Llb_Nonlin4RemoveVar
void Llb_Nonlin4RemoveVar(Llb_Mgr_t *p, Llb_Var_t *pVar)
FUNCTION DEFINITIONS ///.
Definition: llb4Image.c:98
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
Llb_Prt_t_::nSize
int nSize
Definition: llb3Image.c:41
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Llb_Var_t
typedefABC_NAMESPACE_IMPL_START struct Llb_Var_t_ Llb_Var_t
DECLARATIONS ///.
Definition: llb3Image.c:29
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
Extra_SupportArray
int * Extra_SupportArray(DdManager *dd, DdNode *F, int *support)
Definition: extraBddMisc.c:537
Llb_Nonlin4NextPartitions
int Llb_Nonlin4NextPartitions(Llb_Mgr_t *p, Llb_Prt_t **ppPart1, Llb_Prt_t **ppPart2)
Definition: llb4Image.c:585
Llb_Nonlin4Group
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition: llb4Image.c:806
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
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
Llb_Mgr_t_::vVars2Q
Vec_Int_t * vVars2Q
Definition: llb4Image.c:50
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_Nonlin4RecomputeScores
void Llb_Nonlin4RecomputeScores(Llb_Mgr_t *p)
Definition: llb4Image.c:639
Llb_Var_t_::nScore
int nScore
Definition: llb3Image.c:33
Llb_Nonlin4Image
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Definition: llb4Image.c:752
Llb_MgrForEachVar
#define Llb_MgrForEachVar(p, pVar, i)
Definition: llb4Image.c:66
Llb_Mgr_t_::iPartFree
int iPartFree
Definition: llb3Image.c:57
Llb_Nonlin4Alloc
Llb_Mgr_t * Llb_Nonlin4Alloc(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q, int nSizeMax)
Definition: llb4Image.c:692
Vec_IntRemove
static int Vec_IntRemove(Vec_Int_t *p, int Entry)
Definition: vecInt.h:915
Llb_Prt_t_::iPart
int iPart
Definition: llb3Image.c:40
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
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_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Llb_MgrForEachPart
#define Llb_MgrForEachPart(p, pPart, i)
Definition: llb4Image.c:69
Llb_Nonlin4Quantify1
int Llb_Nonlin4Quantify1(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb4Image.c:261
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
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
Llb_Nonlin4AddPair
void Llb_Nonlin4AddPair(Llb_Mgr_t *p, int iPart, int iVar)
Definition: llb4Image.c:510
Llb_Var_t_::vParts
Vec_Int_t * vParts
Definition: llb3Image.c:34
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Llb_VarForEachPart
#define Llb_VarForEachPart(p, pVar, pPart, i)
Definition: llb4Image.c:76
assert
#define assert(ex)
Definition: util_old.h:213
Llb_Nonlin4Print
void Llb_Nonlin4Print(Llb_Mgr_t *p)
Definition: llb4Image.c:228
Llb_Nonlin4HasSingletonVars
int Llb_Nonlin4HasSingletonVars(Llb_Mgr_t *p, Llb_Prt_t *pPart)
Definition: llb4Image.c:207
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
Llb_Nonlin4Quantify2
int Llb_Nonlin4Quantify2(Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
Definition: llb4Image.c:320
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Llb_PartForEachVar
#define Llb_PartForEachVar(p, pPart, pVar, i)
Definition: llb4Image.c:73
Llb_Nonlin4CreateCube2
DdNode * Llb_Nonlin4CreateCube2(Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
Definition: llb4Image.c:171
Llb_Nonlin4CheckVars
void Llb_Nonlin4CheckVars(Llb_Mgr_t *p)
Definition: llb4Image.c:566
Llb_Prt_t_::vVars
Vec_Int_t * vVars
Definition: llb3Image.c:43
Llb_Nonlin4CutNodes
Vec_Ptr_t * Llb_Nonlin4CutNodes(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
Definition: llb4Image.c:483
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