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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Vec_Ptr_t * 		Llb_ManCutNodes (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
 DECLARATIONS ///. More...
 
Vec_Ptr_t * Llb_ManCutRange (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
 
Vec_Ptr_t * Llb_ImgSupports (Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
 FUNCTION DEFINITIONS ///. More...
 
void Llb_ImgSchedule (Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
 
DdManager * Llb_ImgPartition (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
 
DdNode * Llb_ImgComputeCube (Aig_Man_t *pAig, Vec_Int_t *vNodeIds, DdManager *dd)
 
void Llb_ImgQuantifyFirst (Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
 
void Llb_ImgQuantifyReset (Vec_Ptr_t *vDdMans)
 
DdNode * Llb_ImgComputeImage (Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
 

Function Documentation

DdNode* Llb_ImgComputeCube ( Aig_Man_t *  pAig,
Vec_Int_t *  vNodeIds,
DdManager *  dd 
)

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

Synopsis [Derives positive cube composed of nodes IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file llb2Image.c.

260 {
261  DdNode * bProd, * bTemp;
262  Aig_Obj_t * pObj;
263  int i;
264  abctime TimeStop;
265  TimeStop = dd->TimeStop; dd->TimeStop = 0;
266  bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd );
267  Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i )
268  {
269  bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd );
270  Cudd_RecursiveDeref( dd, bTemp );
271  }
272  Cudd_Deref( bProd );
273  dd->TimeStop = TimeStop;
274  return bProd;
275 }
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Aig_Obj_t_
Definition: aig.h:69
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
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
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
DdNode* Llb_ImgComputeImage ( Aig_Man_t *  pAig,
Vec_Ptr_t *  vDdMans,
DdManager *  dd,
DdNode *  bInit,
Vec_Ptr_t *  vQuant0,
Vec_Ptr_t *  vQuant1,
Vec_Int_t *  vDriRefs,
abctime  TimeTarget,
int  fBackward,
int  fReorder,
int  fVerbose 
)

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

Synopsis [Computes image of the initial set of states.]

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file llb2Image.c.

367 {
368 // int fCheckSupport = 0;
369  DdManager * ddPart;
370  DdNode * bImage, * bGroup, * bCube, * bTemp;
371  int i;
372  abctime clk, clk0 = Abc_Clock();
373 
374  bImage = bInit; Cudd_Ref( bImage );
375  if ( fBackward )
376  {
377  // change polarity
378  bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
379  bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
380  Cudd_RecursiveDeref( dd, bTemp );
381  Cudd_RecursiveDeref( dd, bCube );
382  }
383  else
384  {
385  // quantify unique vriables
386  bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
387  bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );
388  if ( bImage == NULL )
389  {
390  Cudd_RecursiveDeref( dd, bTemp );
391  Cudd_RecursiveDeref( dd, bCube );
392  return NULL;
393  }
394  Cudd_Ref( bImage );
395  Cudd_RecursiveDeref( dd, bTemp );
396  Cudd_RecursiveDeref( dd, bCube );
397  }
398  // perform image computation
399  Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i )
400  {
401  clk = Abc_Clock();
402 if ( fVerbose )
403 printf( " %2d : ", i );
404  // transfer the BDD from the group manager to the main manager
405  bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc );
406  if ( bGroup == NULL )
407  return NULL;
408  Cudd_Ref( bGroup );
409 if ( fVerbose )
410 printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
411  // perform partial product
412  bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
413 // bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );
414 // bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );
415  bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );
416  if ( bImage == NULL )
417  {
418  Cudd_RecursiveDeref( dd, bTemp );
419  Cudd_RecursiveDeref( dd, bCube );
420  Cudd_RecursiveDeref( dd, bGroup );
421  return NULL;
422  }
423  Cudd_Ref( bImage );
424 
425 if ( fVerbose )
426 printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
427 //printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n");
428  Cudd_RecursiveDeref( dd, bTemp );
429  Cudd_RecursiveDeref( dd, bCube );
430  Cudd_RecursiveDeref( dd, bGroup );
431 
432 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
433 // Abc_Print( 1, "Reo =%6d. ", Cudd_DagSize(bImage) );
434 
435 if ( fVerbose )
436 printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
437 if ( fVerbose )
438 Abc_PrintTime( 1, "T", Abc_Clock() - clk );
439  }
440 
441  if ( !fBackward )
442  {
443  // change polarity
444  bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
445  bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
446  Cudd_RecursiveDeref( dd, bTemp );
447  Cudd_RecursiveDeref( dd, bCube );
448  }
449  else
450  {
451  // quantify unique vriables
452  bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
453  bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
454  Cudd_RecursiveDeref( dd, bTemp );
455  Cudd_RecursiveDeref( dd, bCube );
456  }
457 
458  if ( fReorder )
459  {
460  if ( fVerbose )
461  Abc_Print( 1, " Reordering... Before =%5d. ", Cudd_DagSize(bImage) );
462  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
463  if ( fVerbose )
464  Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
465 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
466 // Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
467  if ( fVerbose )
468  Abc_PrintTime( 1, "Time", Abc_Clock() - clk0 );
469 // Abc_Print( 1, "\n" );
470  }
471 
472  Cudd_Deref( bImage );
473  return bImage;
474 }
Llb_ImgComputeCube
DdNode * Llb_ImgComputeCube(Aig_Man_t *pAig, Vec_Int_t *vNodeIds, DdManager *dd)
Definition: llb2Image.c:259
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Cudd_bddTransfer
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Llb_DriverPhaseCube
DdNode * Llb_DriverPhaseCube(Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
Definition: llb2Driver.c:128
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Extra_bddChangePolarity
DdNode * Extra_bddChangePolarity(DdManager *dd, DdNode *bFunc, DdNode *bVars)
Definition: extraBddMisc.c:1029
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
DdManager* Llb_ImgPartition ( Aig_Man_t *  p,
Vec_Ptr_t *  vLower,
Vec_Ptr_t *  vUpper,
abctime  TimeTarget 
)

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

Synopsis [Computes one partition in a separate BDD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file llb2Image.c.

184 {
185  Vec_Ptr_t * vNodes, * vRange;
186  Aig_Obj_t * pObj;
187  DdManager * dd;
188  DdNode * bBdd0, * bBdd1, * bProd, * bRes, * bTemp;
189  int i;
190 
191  dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
192  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
193  dd->TimeStop = TimeTarget;
194 
195  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
196  pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
197 
198  vNodes = Llb_ManCutNodes( p, vLower, vUpper );
199  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
200  {
201  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
202  bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
203 // pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
204 // pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );
205  pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
206  if ( pObj->pData == NULL )
207  {
208  Cudd_Quit( dd );
209  Vec_PtrFree( vNodes );
210  return NULL;
211  }
212  Cudd_Ref( (DdNode *)pObj->pData );
213  }
214 
215  vRange = Llb_ManCutRange( p, vLower, vUpper );
216  bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes );
217  Vec_PtrForEachEntry( Aig_Obj_t *, vRange, pObj, i )
218  {
219  assert( Aig_ObjIsNode(pObj) );
220  bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
221 // bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
222 // bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );
223  bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd );
224  if ( bRes == NULL )
225  {
226  Cudd_Quit( dd );
227  Vec_PtrFree( vRange );
228  Vec_PtrFree( vNodes );
229  return NULL;
230  }
231  Cudd_Ref( bRes );
232  Cudd_RecursiveDeref( dd, bTemp );
233  Cudd_RecursiveDeref( dd, bProd );
234  }
235  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
236  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
237 
238  Vec_PtrFree( vRange );
239  Vec_PtrFree( vNodes );
240  Cudd_AutodynDisable( dd );
241 // Cudd_RecursiveDeref( dd, bRes );
242 // Extra_StopManager( dd );
243  dd->bFunc = bRes;
244  dd->TimeStop = 0;
245  return dd;
246 }
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
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
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_Obj_t_
Definition: aig.h:69
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
Llb_ManCutNodes
ABC_NAMESPACE_IMPL_START Vec_Ptr_t * Llb_ManCutNodes(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
DECLARATIONS ///.
Definition: llb2Flow.c:374
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
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
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
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
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Llb_ManCutRange
Vec_Ptr_t * Llb_ManCutRange(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
Definition: llb2Flow.c:436
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Llb_ImgQuantifyFirst ( Aig_Man_t *  pAig,
Vec_Ptr_t *  vDdMans,
Vec_Ptr_t *  vQuant0,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file llb2Image.c.

289 {
290  DdManager * dd;
291  DdNode * bProd, * bRes, * bTemp;
292  int i;
293  abctime clk = Abc_Clock();
294  Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
295  {
296  // remember unquantified ones
297  assert( dd->bFunc2 == NULL );
298  dd->bFunc2 = dd->bFunc; Cudd_Ref( dd->bFunc2 );
299 
300  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
301 
302  bRes = dd->bFunc;
303  if ( fVerbose )
304  Abc_Print( 1, "Part %2d : Init =%5d. ", i, Cudd_DagSize(bRes) );
305  bProd = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, i+1), dd ); Cudd_Ref( bProd );
306  bRes = Cudd_bddExistAbstract( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
307  Cudd_RecursiveDeref( dd, bTemp );
308  Cudd_RecursiveDeref( dd, bProd );
309  dd->bFunc = bRes;
310 
311  Cudd_AutodynDisable( dd );
312 
313  if ( fVerbose )
314  Abc_Print( 1, "Quant =%5d. ", Cudd_DagSize(bRes) );
315  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
316  if ( fVerbose )
317  Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
318  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
319  if ( fVerbose )
320  Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
321  if ( fVerbose )
322  Abc_Print( 1, "Supp = %3d. ", Cudd_SupportSize(dd, bRes) );
323  if ( fVerbose )
324  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
325 
326  }
327 }
Llb_ImgComputeCube
DdNode * Llb_ImgComputeCube(Aig_Man_t *pAig, Vec_Int_t *vNodeIds, DdManager *dd)
Definition: llb2Image.c:259
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
DdManager::bFunc2
DdNode * bFunc2
Definition: cuddInt.h:488
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
assert
#define assert(ex)
Definition: util_old.h:213
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
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
void Llb_ImgQuantifyReset ( Vec_Ptr_t *  vDdMans)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file llb2Image.c.

341 {
342  DdManager * dd;
343  int i;
344  Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
345  {
346  assert( dd->bFunc2 != NULL );
347  Cudd_RecursiveDeref( dd, dd->bFunc );
348  dd->bFunc = dd->bFunc2;
349  dd->bFunc2 = NULL;
350  }
351 }
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
DdManager::bFunc2
DdNode * bFunc2
Definition: cuddInt.h:488
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Llb_ImgSchedule ( Vec_Ptr_t *  vSupps,
Vec_Ptr_t **  pvQuant0,
Vec_Ptr_t **  pvQuant1,
int  fVerbose 
)

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

Synopsis [Computes quantification schedule.]

Description [Input array contains supports: 0=starting, ... intermediate... N-1=final. Output arrays contain immediately quantifiable vars (vQuant0) and vars that should be quantified after conjunction (vQuant1).]

SideEffects []

SeeAlso []

Definition at line 122 of file llb2Image.c.

123 {
124  Vec_Int_t * vOne;
125  int nVarsAll, Counter, iSupp = -1, Entry, i, k;
126  // start quantification arrays
127  *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
128  *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
129  Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
130  {
131  Vec_PtrPush( *pvQuant0, Vec_IntAlloc(16) );
132  Vec_PtrPush( *pvQuant1, Vec_IntAlloc(16) );
133  }
134  // count how many times each var appears
135  nVarsAll = Vec_IntSize( (Vec_Int_t *)Vec_PtrEntry(vSupps, 0) );
136  for ( i = 0; i < nVarsAll; i++ )
137  {
138  Counter = 0;
139  Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
140  if ( Vec_IntEntry(vOne, i) )
141  {
142  iSupp = k;
143  Counter++;
144  }
145  if ( Counter == 0 )
146  continue;
147  if ( Counter == 1 )
148  Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, iSupp), i );
149  else // if ( Counter > 1 )
150  Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, iSupp), i );
151  }
152 
153  if ( fVerbose )
154  for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
155  {
156  printf( "%2d : Quant0 = ", i );
157  Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, i), Entry, k )
158  printf( "%d ", Entry );
159  printf( "\n" );
160  }
161 
162  if ( fVerbose )
163  for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
164  {
165  printf( "%2d : Quant1 = ", i );
166  Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, i), Entry, k )
167  printf( "%d ", Entry );
168  printf( "\n" );
169  }
170 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
for
for(p=first;p->value< newval;p=p->next)
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if
if(last==0)
Definition: sparse_int.h:34
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
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
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Ptr_t* Llb_ImgSupports ( Aig_Man_t *  p,
Vec_Ptr_t *  vDdMans,
Vec_Int_t *  vStart,
Vec_Int_t *  vStop,
int  fAddPis,
int  fVerbose 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes supports of the partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file llb2Image.c.

49 {
50  Vec_Ptr_t * vSupps;
51  Vec_Int_t * vOne;
52  Aig_Obj_t * pObj;
53  DdManager * dd;
54  DdNode * bSupp, * bTemp;
55  int i, Entry, nSize;
56  nSize = Cudd_ReadSize( (DdManager *)Vec_PtrEntry( vDdMans, 0 ) );
57  vSupps = Vec_PtrAlloc( 100 );
58  // create initial
59  vOne = Vec_IntStart( nSize );
60  Vec_IntForEachEntry( vStart, Entry, i )
61  Vec_IntWriteEntry( vOne, Entry, 1 );
62  Vec_PtrPush( vSupps, vOne );
63  // create intermediate
64  Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
65  {
66  vOne = Vec_IntStart( nSize );
67  bSupp = Cudd_Support( dd, dd->bFunc ); Cudd_Ref( bSupp );
68  for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
69  Vec_IntWriteEntry( vOne, bTemp->index, 1 );
70  Cudd_RecursiveDeref( dd, bSupp );
71  Vec_PtrPush( vSupps, vOne );
72  }
73  // create final
74  vOne = Vec_IntStart( nSize );
75  Vec_IntForEachEntry( vStop, Entry, i )
76  Vec_IntWriteEntry( vOne, Entry, 1 );
77  if ( fAddPis )
78  Saig_ManForEachPi( p, pObj, i )
79  Vec_IntWriteEntry( vOne, Aig_ObjId(pObj), 1 );
80  Vec_PtrPush( vSupps, vOne );
81 
82  // print supports
83  assert( nSize == Aig_ManObjNumMax(p) );
84  if ( !fVerbose )
85  return vSupps;
86  Aig_ManForEachObj( p, pObj, i )
87  {
88  int k, Counter = 0;
89  Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
90  Counter += Vec_IntEntry(vOne, i);
91  if ( Counter == 0 )
92  continue;
93  printf( "Obj = %4d : ", i );
94  if ( Saig_ObjIsPi(p,pObj) )
95  printf( "pi " );
96  else if ( Saig_ObjIsLo(p,pObj) )
97  printf( "lo " );
98  else if ( Saig_ObjIsLi(p,pObj) )
99  printf( "li " );
100  else if ( Aig_ObjIsNode(pObj) )
101  printf( "and " );
102  Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
103  printf( "%d", Vec_IntEntry(vOne, i) );
104  printf( "\n" );
105  }
106  return vSupps;
107 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
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
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
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_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
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
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
DdNode::index
DdHalfWord index
Definition: cudd.h:279
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
ABC_NAMESPACE_IMPL_START Vec_Ptr_t* Llb_ManCutNodes ( Aig_Man_t *  p,
Vec_Ptr_t *  vLower,
Vec_Ptr_t *  vUpper 
)

DECLARATIONS ///.

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

FileName [llb2Image.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Computes image using partitioned structure.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
llb2Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

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

Synopsis [Computes volume of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 374 of file llb2Flow.c.

375 {
376  Vec_Ptr_t * vNodes;
377  Aig_Obj_t * pObj;
378  int i;
379  // mark the lower cut with the traversal ID
380  Aig_ManIncrementTravId(p);
381  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
382  Aig_ObjSetTravIdCurrent( p, pObj );
383  // count the upper cut
384  vNodes = Vec_PtrAlloc( 100 );
385  Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
386  Llb_ManCutNodes_rec( p, pObj, vNodes );
387  return vNodes;
388 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Llb_ManCutNodes_rec
void Llb_ManCutNodes_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: llb2Flow.c:352
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_Obj_t_
Definition: aig.h:69
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_Ptr_t* Llb_ManCutRange ( Aig_Man_t *  p,
Vec_Ptr_t *  vLower,
Vec_Ptr_t *  vUpper 
)

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

Synopsis [Computes volume of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 436 of file llb2Flow.c.

437 {
438  Vec_Ptr_t * vRange;
439  Aig_Obj_t * pObj;
440  int i;
441  // mark the lower cut with the traversal ID
442  Aig_ManIncrementTravId(p);
443  Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
444  Aig_ObjSetTravIdCurrent( p, pObj );
445  // collect the upper ones that are not marked
446  vRange = Vec_PtrAlloc( 100 );
447  Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
448  if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
449  Vec_PtrPush( vRange, pObj );
450  return vRange;
451 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55