abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcDsd.c File Reference
#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"
#include "bdd/dsd/dsd.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
Abc_Ntk_t
Abc_NtkDsdInternal (Abc_Ntk_t *pNtk, int fVerbose, int fPrint, int fShort)
 DECLARATIONS ///. More...
 
static void Abc_NtkDsdConstruct (Dsd_Manager_t *pManDsd, Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
 
static Abc_Obj_tAbc_NtkDsdConstructNode (Dsd_Manager_t *pManDsd, Dsd_Node_t *pNodeDsd, Abc_Ntk_t *pNtkNew, int *pCounters)
 
static Vec_Ptr_tAbc_NtkCollectNodesForDsd (Abc_Ntk_t *pNtk)
 
static void Abc_NodeDecompDsdAndMux (Abc_Obj_t *pNode, Vec_Ptr_t *vNodes, Dsd_Manager_t *pManDsd, int fRecursive, int *pCounters)
 
static int Abc_NodeIsForDsd (Abc_Obj_t *pNode)
 
static int Abc_NodeFindMuxVar (DdManager *dd, DdNode *bFunc, int nVars)
 
Abc_Ntk_tAbc_NtkDsdGlobal (Abc_Ntk_t *pNtk, int fVerbose, int fPrint, int fShort)
 FUNCTION DEFINITIONS ///. More...
 
int Abc_NtkDsdLocal (Abc_Ntk_t *pNtk, int fVerbose, int fRecursive)
 
DdNodeExtra_bddComputeSum (DdManager *dd, DdNode **pbCubes, int nCubes)
 
DdNodeAbc_NtkSparsifyInternalOne (DdManager *ddNew, DdNode *bFunc, int nFanins, int nPerc)
 
Abc_Ntk_tAbc_NtkSparsifyInternal (Abc_Ntk_t *pNtk, int nPerc, int fVerbose)
 
Abc_Ntk_tAbc_NtkSparsify (Abc_Ntk_t *pNtk, int nPerc, int fVerbose)
 

Function Documentation

void Abc_NodeDecompDsdAndMux ( Abc_Obj_t pNode,
Vec_Ptr_t vNodes,
Dsd_Manager_t pManDsd,
int  fRecursive,
int *  pCounters 
)
static

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

Synopsis [Performs decomposition of one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 395 of file abcDsd.c.

396 {
397  DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
398  Abc_Obj_t * pRoot = NULL, * pFanin, * pNode1, * pNode2, * pNodeC;
399  Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
400  int i, nNodesDsd, iVar, fCompl;
401 
402  // try disjoint support decomposition
403  pNodeDsd = Dsd_DecomposeOne( pManDsd, (DdNode *)pNode->pData );
404  fCompl = Dsd_IsComplement( pNodeDsd );
405  pNodeDsd = Dsd_Regular( pNodeDsd );
406 
407  // determine what decomposition to use
408  if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
409  { // perform DSD
410 
411  // set the inputs
412  Abc_ObjForEachFanin( pNode, pFanin, i )
413  {
414  pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
415  Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin );
416  }
417 
418  // construct the intermediate nodes
419  ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
420  for ( i = 0; i < nNodesDsd; i++ )
421  {
422  pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk, pCounters );
423  if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
424  Vec_PtrPush( vNodes, pRoot );
425  }
426  ABC_FREE( ppNodesDsd );
427  assert(pRoot);
428 
429  // remove the current fanins
430  Abc_ObjRemoveFanins( pNode );
431  // add fanin to the root
432  Abc_ObjAddFanin( pNode, pRoot );
433  // update the function to be that of buffer
434  Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
435  pNode->pData = Cudd_NotCond( (DdNode *)dd->vars[0], fCompl ); Cudd_Ref( (DdNode *)pNode->pData );
436  }
437  else // perform MUX-decomposition
438  {
439  // get the cofactoring variable
440  iVar = Abc_NodeFindMuxVar( dd, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode) );
441  pNodeC = Abc_ObjFanin( pNode, iVar );
442 
443  // get the negative cofactor
444  pNode1 = Abc_NtkCloneObj( pNode );
445  pNode1->pData = Cudd_Cofactor( dd, (DdNode *)pNode->pData, Cudd_Not(dd->vars[iVar]) ); Cudd_Ref( (DdNode *)pNode1->pData );
446  Abc_NodeMinimumBase( pNode1 );
447  if ( Abc_NodeIsForDsd(pNode1) )
448  Vec_PtrPush( vNodes, pNode1 );
449 
450  // get the positive cofactor
451  pNode2 = Abc_NtkCloneObj( pNode );
452  pNode2->pData = Cudd_Cofactor( dd, (DdNode *)pNode->pData, dd->vars[iVar] ); Cudd_Ref( (DdNode *)pNode2->pData );
453  Abc_NodeMinimumBase( pNode2 );
454  if ( Abc_NodeIsForDsd(pNode2) )
455  Vec_PtrPush( vNodes, pNode2 );
456 
457  // remove the current fanins
458  Abc_ObjRemoveFanins( pNode );
459  // add new fanins
460  Abc_ObjAddFanin( pNode, pNodeC );
461  Abc_ObjAddFanin( pNode, pNode2 );
462  Abc_ObjAddFanin( pNode, pNode1 );
463  // update the function to be that of MUX
464  Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
465  pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] ); Cudd_Ref( (DdNode *)pNode->pData );
466  }
467 }
static int Abc_NodeFindMuxVar(DdManager *dd, DdNode *bFunc, int nVars)
Definition: abcDsd.c:519
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
static Abc_Obj_t * Abc_NtkDsdConstructNode(Dsd_Manager_t *pManDsd, Dsd_Node_t *pNodeDsd, Abc_Ntk_t *pNtkNew, int *pCounters)
Definition: abcDsd.c:212
Dsd_Node_t * Dsd_ManagerReadInput(Dsd_Manager_t *pMan, int i)
Definition: dsdApi.c:94
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
int Dsd_NodeReadDecsNum(Dsd_Node_t *p)
Definition: dsdApi.c:58
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_DLL Abc_Obj_t * Abc_NtkCloneObj(Abc_Obj_t *pNode)
Definition: abcObj.c:434
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
void * pManFunc
Definition: abc.h:191
static int Abc_NodeIsForDsd(Abc_Obj_t *pNode)
Definition: abcDsd.c:480
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pNode, int *pnNodes)
Definition: dsdTree.c:585
#define Dsd_Regular(p)
Definition: dsd.h:69
ABC_DLL void Abc_ObjRemoveFanins(Abc_Obj_t *pObj)
Definition: abcFanio.c:141
#define Dsd_IsComplement(p)
MACRO DEFINITIONS ///.
Definition: dsd.h:68
Abc_Ntk_t * pNtk
Definition: abc.h:130
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode ** vars
Definition: cuddInt.h:390
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
#define assert(ex)
Definition: util_old.h:213
void * pData
Definition: abc.h:145
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
static Abc_Obj_t * Abc_ObjFanin(Abc_Obj_t *pObj, int i)
Definition: abc.h:372
Dsd_Node_t * Dsd_DecomposeOne(Dsd_Manager_t *pDsdMan, DdNode *bFunc)
Definition: dsdProc.c:230
void Dsd_NodeSetMark(Dsd_Node_t *p, int Mark)
Definition: dsdApi.c:77
ABC_DLL int Abc_NodeMinimumBase(Abc_Obj_t *pNode)
Definition: abcMinBase.c:70
int Abc_NodeFindMuxVar ( DdManager dd,
DdNode bFunc,
int  nVars 
)
static

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

Synopsis [Determines a cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 519 of file abcDsd.c.

520 {
521  DdNode * bVar, * bCof0, * bCof1;
522  int SuppSumMin = 1000000;
523  int i, nSSD, nSSQ, iVar;
524 
525 // printf( "\n\nCofactors:\n\n" );
526  iVar = -1;
527  for ( i = 0; i < nVars; i++ )
528  {
529  bVar = dd->vars[i];
530 
531  bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof0 );
532  bCof1 = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof1 );
533 
534 // nodD = Cudd_DagSize(bCof0);
535 // nodQ = Cudd_DagSize(bCof1);
536 // printf( "+%02d: D=%2d. Q=%2d. ", i, nodD, nodQ );
537 // printf( "S=%2d. D=%2d. ", nodD + nodQ, abs(nodD-nodQ) );
538 
539  nSSD = Cudd_SupportSize( dd, bCof0 );
540  nSSQ = Cudd_SupportSize( dd, bCof1 );
541 
542 // printf( "SD=%2d. SQ=%2d. ", nSSD, nSSQ );
543 // printf( "S=%2d. D=%2d. ", nSSD + nSSQ, abs(nSSD - nSSQ) );
544 // printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) );
545 // printf( "\n" );
546 
547  Cudd_RecursiveDeref( dd, bCof0 );
548  Cudd_RecursiveDeref( dd, bCof1 );
549 
550  if ( SuppSumMin > nSSD + nSSQ )
551  {
552  SuppSumMin = nSSD + nSSQ;
553  iVar = i;
554  }
555  }
556  return iVar;
557 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
DdNode ** vars
Definition: cuddInt.h:390
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
int Abc_NodeIsForDsd ( Abc_Obj_t pNode)
static

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

Synopsis [Checks if the node should be decomposed by DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file abcDsd.c.

481 {
482 // DdManager * dd = pNode->pNtk->pManFunc;
483 // DdNode * bFunc, * bFunc0, * bFunc1;
484  assert( Abc_ObjIsNode(pNode) );
485 // if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
486 // return 1;
487 // return 0;
488 
489 /*
490  // this does not catch things like a(b+c), which should be decomposed
491  for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); )
492  {
493  bFunc0 = Cudd_Regular( cuddE(bFunc) );
494  bFunc1 = cuddT(bFunc);
495  if ( bFunc0 == b1 )
496  bFunc = bFunc1;
497  else if ( bFunc1 == b1 || bFunc0 == bFunc1 )
498  bFunc = bFunc0;
499  else
500  return 1;
501  }
502 */
503  if ( Abc_ObjFaninNum(pNode) > 2 )
504  return 1;
505  return 0;
506 }
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
#define assert(ex)
Definition: util_old.h:213
Vec_Ptr_t * Abc_NtkCollectNodesForDsd ( Abc_Ntk_t pNtk)
static

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

Synopsis [Collects the nodes that may need decomposition.]

Description [The nodes that do not need decomposition are those whose BDD has more internal nodes than the support size.]

SideEffects []

SeeAlso []

Definition at line 370 of file abcDsd.c.

371 {
372  Vec_Ptr_t * vNodes;
373  Abc_Obj_t * pNode;
374  int i;
375  vNodes = Vec_PtrAlloc( 100 );
376  Abc_NtkForEachNode( pNtk, pNode, i )
377  {
378  if ( Abc_NodeIsForDsd(pNode) )
379  Vec_PtrPush( vNodes, pNode );
380  }
381  return vNodes;
382 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Abc_NodeIsForDsd(Abc_Obj_t *pNode)
Definition: abcDsd.c:480
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void Abc_NtkDsdConstruct ( Dsd_Manager_t pManDsd,
Abc_Ntk_t pNtk,
Abc_Ntk_t pNtkNew 
)
static

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

Synopsis [Constructs the decomposed network.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file abcDsd.c.

165 {
166  Dsd_Node_t ** ppNodesDsd;
167  Dsd_Node_t * pNodeDsd;
168  Abc_Obj_t * pNode, * pNodeNew, * pDriver;
169  int i, nNodesDsd;
170 
171  // save the CI nodes in the DSD nodes
172  Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew);
173  Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew );
174  Abc_NtkForEachCi( pNtk, pNode, i )
175  {
176  pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
177  Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy );
178  }
179 
180  // collect DSD nodes in DFS order (leaves and const1 are not collected)
181  ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
182  for ( i = 0; i < nNodesDsd; i++ )
183  Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL );
184  ABC_FREE( ppNodesDsd );
185 
186  // set the pointers to the CO drivers
187  Abc_NtkForEachCo( pNtk, pNode, i )
188  {
189  pDriver = Abc_ObjFanin0( pNode );
190  if ( !Abc_ObjIsNode(pDriver) )
191  continue;
192  if ( !Abc_AigNodeIsAnd(pDriver) )
193  continue;
194  pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
195  pNodeNew = (Abc_Obj_t *)(ABC_PTRINT_T)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
196  assert( !Abc_ObjIsComplement(pNodeNew) );
197  pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
198  }
199 }
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static Abc_Obj_t * Abc_NtkDsdConstructNode(Dsd_Manager_t *pManDsd, Dsd_Node_t *pNodeDsd, Abc_Ntk_t *pNtkNew, int *pCounters)
Definition: abcDsd.c:212
Dsd_Node_t ** Dsd_TreeCollectNodesDfs(Dsd_Manager_t *dMan, int *pnNodes)
Definition: dsdTree.c:555
Dsd_Node_t * Dsd_ManagerReadInput(Dsd_Manager_t *pMan, int i)
Definition: dsdApi.c:94
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Definition: abcObj.c:633
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Dsd_Node_t * Dsd_ManagerReadRoot(Dsd_Manager_t *pMan, int i)
Definition: dsdApi.c:93
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
Dsd_Node_t * Dsd_ManagerReadConst1(Dsd_Manager_t *pMan)
Definition: dsdApi.c:95
Abc_Obj_t * pCopy
Definition: abc.h:148
static int Abc_AigNodeIsAnd(Abc_Obj_t *pNode)
Definition: abc.h:397
#define Dsd_Regular(p)
Definition: dsd.h:69
#define Dsd_IsComplement(p)
MACRO DEFINITIONS ///.
Definition: dsd.h:68
int Dsd_NodeReadMark(Dsd_Node_t *p)
Definition: dsdApi.c:59
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
#define ABC_FREE(obj)
Definition: abc_global.h:232
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
#define assert(ex)
Definition: util_old.h:213
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
void Dsd_NodeSetMark(Dsd_Node_t *p, int Mark)
Definition: dsdApi.c:77
Abc_Obj_t * Abc_NtkDsdConstructNode ( Dsd_Manager_t pManDsd,
Dsd_Node_t pNodeDsd,
Abc_Ntk_t pNtkNew,
int *  pCounters 
)
static

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

Synopsis [Performs DSD using the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file abcDsd.c.

213 {
214  DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
215  DdManager * ddNew = (DdManager *)pNtkNew->pManFunc;
216  Dsd_Node_t * pFaninDsd;
217  Abc_Obj_t * pNodeNew, * pFanin;
218  DdNode * bLocal, * bTemp, * bVar;
219  Dsd_Type_t Type;
220  int i, nDecs;
221 
222  // create the new node
223  pNodeNew = Abc_NtkCreateNode( pNtkNew );
224  // add the fanins
225  Type = Dsd_NodeReadType( pNodeDsd );
226  nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
227  assert( nDecs > 1 );
228  for ( i = 0; i < nDecs; i++ )
229  {
230  pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
231  pFanin = (Abc_Obj_t *)(ABC_PTRINT_T)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
232  Abc_ObjAddFanin( pNodeNew, pFanin );
233  assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
234  }
235 
236  // create the local function depending on the type of the node
237  ddNew = (DdManager *)pNtkNew->pManFunc;
238  switch ( Type )
239  {
240  case DSD_NODE_CONST1:
241  {
242  bLocal = ddNew->one; Cudd_Ref( bLocal );
243  break;
244  }
245  case DSD_NODE_OR:
246  {
247  bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
248  for ( i = 0; i < nDecs; i++ )
249  {
250  pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
251  bVar = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) );
252  bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar ); Cudd_Ref( bLocal );
253  Cudd_RecursiveDeref( ddNew, bTemp );
254  }
255  break;
256  }
257  case DSD_NODE_EXOR:
258  {
259  bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
260  for ( i = 0; i < nDecs; i++ )
261  {
262  bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] ); Cudd_Ref( bLocal );
263  Cudd_RecursiveDeref( ddNew, bTemp );
264  }
265  break;
266  }
267  case DSD_NODE_PRIME:
268  {
269  if ( pCounters )
270  {
271  if ( nDecs < 10 )
272  pCounters[nDecs]++;
273  else
274  pCounters[10]++;
275  }
276  bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd ); Cudd_Ref( bLocal );
277  bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
278 /*
279 if ( nDecs == 3 )
280 {
281 Extra_bddPrint( ddDsd, bTemp );
282 printf( "\n" );
283 }
284 */
285  Cudd_RecursiveDeref( ddDsd, bTemp );
286  // bLocal is now in the new BDD manager
287  break;
288  }
289  default:
290  {
291  assert( 0 );
292  break;
293  }
294  }
295  pNodeNew->pData = bLocal;
296  Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew );
297  return pNodeNew;
298 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
DdManager * Dsd_ManagerReadDd(Dsd_Manager_t *pMan)
Definition: dsdApi.c:96
int Dsd_NodeReadDecsNum(Dsd_Node_t *p)
Definition: dsdApi.c:58
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
void * pManFunc
Definition: abc.h:191
DdNode * Extra_TransferLevelByLevel(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: extraBddMisc.c:112
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
#define Dsd_Regular(p)
Definition: dsd.h:69
#define Dsd_IsComplement(p)
MACRO DEFINITIONS ///.
Definition: dsd.h:68
DdNode * Dsd_TreeGetPrimeFunction(DdManager *dd, Dsd_Node_t *pNode)
FUNCTION DEFINITIONS ///.
Definition: dsdLocal.c:54
int Dsd_NodeReadMark(Dsd_Node_t *p)
Definition: dsdApi.c:59
DdNode ** vars
Definition: cuddInt.h:390
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
DdNode * one
Definition: cuddInt.h:345
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
#define assert(ex)
Definition: util_old.h:213
enum Dsd_Type_t_ Dsd_Type_t
Definition: dsd.h:61
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Dsd_Type_t Dsd_NodeReadType(Dsd_Node_t *p)
FUNCTION DEFINITIONS ///.
Definition: dsdApi.c:53
Dsd_Node_t * Dsd_NodeReadDec(Dsd_Node_t *p, int i)
Definition: dsdApi.c:57
void Dsd_NodeSetMark(Dsd_Node_t *p, int Mark)
Definition: dsdApi.c:77
Abc_Ntk_t* Abc_NtkDsdGlobal ( Abc_Ntk_t pNtk,
int  fVerbose,
int  fPrint,
int  fShort 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Derives the DSD network.]

Description [Takes the strashed network (pNtk), derives global BDDs for the combinational outputs of this network, and decomposes these BDDs using disjoint support decomposition. Finally, constructs and return a new network, which is topologically equivalent to the decomposition tree. Allocates and frees a new BDD manager and a new DSD manager.]

SideEffects []

SeeAlso []

Definition at line 60 of file abcDsd.c.

61 {
62  DdManager * dd;
63  Abc_Ntk_t * pNtkNew;
64  assert( Abc_NtkIsStrash(pNtk) );
65  dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
66  if ( dd == NULL )
67  return NULL;
68  if ( fVerbose )
69  printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
70  // transform the result of mapping into a BDD network
71  pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
72  Extra_StopManager( dd );
73  if ( pNtkNew == NULL )
74  return NULL;
75  // copy EXDC network
76  if ( pNtk->pExdc )
77  pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
78  if ( !Abc_NtkCheck( pNtkNew ) )
79  {
80  printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
81  Abc_NtkDelete( pNtkNew );
82  return NULL;
83  }
84  return pNtkNew;
85 }
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Abc_Ntk_t * pExdc
Definition: abc.h:201
static ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkDsdInternal(Abc_Ntk_t *pNtk, int fVerbose, int fPrint, int fShort)
DECLARATIONS ///.
Definition: abcDsd.c:98
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
#define assert(ex)
Definition: util_old.h:213
ABC_DLL void * Abc_NtkBuildGlobalBdds(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: abcNtbdd.c:251
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
Abc_Ntk_t * Abc_NtkDsdInternal ( Abc_Ntk_t pNtk,
int  fVerbose,
int  fPrint,
int  fShort 
)
static

DECLARATIONS ///.

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

FileName [abcDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Decomposes the network using disjoint-support decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

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

Synopsis [Constructs the decomposed network.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file abcDsd.c.

99 {
100  char ** ppNamesCi, ** ppNamesCo;
101  Vec_Ptr_t * vFuncsGlob;
102  Dsd_Manager_t * pManDsd;
103  Abc_Ntk_t * pNtkNew;
104  DdManager * dd;
105  Abc_Obj_t * pObj;
106  int i;
107 
108  // complement the global functions
109  vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
110  Abc_NtkForEachCo( pNtk, pObj, i )
111  Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) );
112 
113  // perform the decomposition
114  dd = (DdManager *)Abc_NtkGlobalBddMan(pNtk);
115  pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
116  if ( pManDsd == NULL )
117  {
118  Vec_PtrFree( vFuncsGlob );
119  Cudd_Quit( dd );
120  return NULL;
121  }
122  Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
123  Vec_PtrFree( vFuncsGlob );
124  Abc_NtkFreeGlobalBdds( pNtk, 0 );
125 
126  // start the new network
127  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
128  // make sure the new manager has enough inputs
129  Cudd_bddIthVar( (DdManager *)pNtkNew->pManFunc, dd->size-1 );
130  // put the results into the new network (save new CO drivers in old CO drivers)
131  Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
132  // finalize the new network
133  Abc_NtkFinalize( pNtk, pNtkNew );
134  // fix the problem with complemented and duplicated CO edges
135  Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
136  if ( fPrint )
137  {
138  ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
139  ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
140  if ( fVerbose )
141  Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
142  else
143  Dsd_TreePrint2( stdout, pManDsd, ppNamesCi, ppNamesCo, -1 );
144  ABC_FREE( ppNamesCi );
145  ABC_FREE( ppNamesCo );
146  }
147 
148  // stop the DSD manager
149  Dsd_ManagerStop( pManDsd );
150  return pNtkNew;
151 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Definition: cudd.h:278
void Dsd_ManagerStop(Dsd_Manager_t *dMan)
Definition: dsdMan.c:100
static void Abc_NtkDsdConstruct(Dsd_Manager_t *pManDsd, Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
Definition: abcDsd.c:164
int size
Definition: cuddInt.h:361
void Dsd_TreePrint2(FILE *pFile, Dsd_Manager_t *dMan, char *pInputNames[], char *pOutputNames[], int Output)
Definition: dsdTree.c:917
ABC_DLL char ** Abc_NtkCollectCioNames(Abc_Ntk_t *pNtk, int fCollectCos)
Definition: abcNames.c:278
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
ABC_DLL void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
Definition: abcNtbdd.c:476
void * pManFunc
Definition: abc.h:191
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:106
if(last==0)
Definition: sparse_int.h:34
ABC_DLL void Abc_NtkFinalize(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
Definition: abcNtk.c:302
STRUCTURE DEFINITIONS ///.
Definition: dsdInt.h:40
Dsd_Manager_t * Dsd_ManagerStart(DdManager *dd, int nSuppMax, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition: dsdMan.c:47
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
Definition: abcUtil.c:1047
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static void * Abc_NtkGlobalBddMan(Abc_Ntk_t *pNtk)
Definition: abc.h:429
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
void Dsd_Decompose(Dsd_Manager_t *dMan, DdNode **pbFuncs, int nFuncs)
DECOMPOSITION FUNCTIONS ///.
Definition: dsdProc.c:113
void Dsd_TreePrint(FILE *pFile, Dsd_Manager_t *dMan, char *pInputNames[], char *pOutputNames[], int fShortNames, int Output)
Definition: dsdTree.c:641
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Abc_NtkDsdLocal ( Abc_Ntk_t pNtk,
int  fVerbose,
int  fRecursive 
)

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

Synopsis [Recursively decomposes internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file abcDsd.c.

317 {
318  Dsd_Manager_t * pManDsd;
319  DdManager * dd = (DdManager *)pNtk->pManFunc;
320  Vec_Ptr_t * vNodes;
321  int i;
322  int pCounters[11] = {0};
323 
324  assert( Abc_NtkIsBddLogic(pNtk) );
325 
326  // make the network minimum base
327  Abc_NtkMinimumBase( pNtk );
328 
329  // start the DSD manager
330  pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
331 
332  // collect nodes for decomposition
333  vNodes = Abc_NtkCollectNodesForDsd( pNtk );
334  for ( i = 0; i < vNodes->nSize; i++ )
335  Abc_NodeDecompDsdAndMux( (Abc_Obj_t *)vNodes->pArray[i], vNodes, pManDsd, fRecursive, pCounters );
336  Vec_PtrFree( vNodes );
337 
338  if ( fVerbose )
339  {
340  printf( "Number of non-decomposable functions:\n" );
341  for ( i = 3; i < 10; i++ )
342  printf( "Inputs = %d. Functions = %6d.\n", i, pCounters[i] );
343  printf( "Inputs > %d. Functions = %6d.\n", 9, pCounters[10] );
344  }
345 
346  // stop the DSD manager
347  Dsd_ManagerStop( pManDsd );
348 
349  // make sure everything is okay
350  if ( !Abc_NtkCheck( pNtk ) )
351  {
352  printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
353  return 0;
354  }
355  return 1;
356 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Dsd_ManagerStop(Dsd_Manager_t *dMan)
Definition: dsdMan.c:100
ABC_DLL int Abc_NtkMinimumBase(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcMinBase.c:48
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
static Vec_Ptr_t * Abc_NtkCollectNodesForDsd(Abc_Ntk_t *pNtk)
Definition: abcDsd.c:370
void * pManFunc
Definition: abc.h:191
STRUCTURE DEFINITIONS ///.
Definition: dsdInt.h:40
Dsd_Manager_t * Dsd_ManagerStart(DdManager *dd, int nSuppMax, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition: dsdMan.c:47
static void Abc_NodeDecompDsdAndMux(Abc_Obj_t *pNode, Vec_Ptr_t *vNodes, Dsd_Manager_t *pManDsd, int fRecursive, int *pCounters)
Definition: abcDsd.c:395
static int Abc_NtkIsBddLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:265
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Abc_Ntk_t* Abc_NtkSparsify ( Abc_Ntk_t pNtk,
int  nPerc,
int  fVerbose 
)

Definition at line 674 of file abcDsd.c.

675 {
676  Abc_Ntk_t * pNtkNew;
677  assert( Abc_NtkIsComb(pNtk) );
678  assert( Abc_NtkIsBddLogic(pNtk) );
679  pNtkNew = Abc_NtkSparsifyInternal( pNtk, nPerc, fVerbose );
680  if ( pNtkNew == NULL )
681  return NULL;
682  if ( !Abc_NtkCheck( pNtkNew ) )
683  {
684  printf( "Abc_NtkSparsify: The network check has failed.\n" );
685  Abc_NtkDelete( pNtkNew );
686  return NULL;
687  }
688  return pNtkNew;
689 }
Abc_Ntk_t * Abc_NtkSparsifyInternal(Abc_Ntk_t *pNtk, int nPerc, int fVerbose)
Definition: abcDsd.c:611
static int Abc_NtkIsComb(Abc_Ntk_t *pNtk)
Definition: abc.h:297
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
static int Abc_NtkIsBddLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:265
#define assert(ex)
Definition: util_old.h:213
Abc_Ntk_t* Abc_NtkSparsifyInternal ( Abc_Ntk_t pNtk,
int  nPerc,
int  fVerbose 
)

Definition at line 611 of file abcDsd.c.

612 {
613  Abc_Ntk_t * pNtkNew;
614  Abc_Obj_t * pObj, * pDriver, * pFanin;
615  DdNode * bFunc, * bFuncOld;
616  DdManager * ddNew;
617  int i, k, c;
618  // start the new network
619  pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
620  Abc_NtkForEachCi( pNtk, pObj, i )
621  Abc_NtkDupObj( pNtkNew, pObj, 1 );
622  // duplicate the name and the spec
623  pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
624  pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
625  // make sure the new manager has enough inputs
626  ddNew = (DdManager *)pNtkNew->pManFunc;
627  Cudd_bddIthVar( ddNew, Abc_NtkCiNum(pNtk)-1 );
628  // go through the outputs
629  Abc_NtkForEachCo( pNtk, pObj, i )
630  {
631  pDriver = Abc_ObjFanin0( pObj );
632  if ( Abc_ObjIsCi(pDriver) )
633  {
634  Abc_NtkDupObj( pNtkNew, pObj, 0 );
635  Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(pDriver->pCopy, Abc_ObjFaninC0(pObj)) );
636  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_on" );
637 
638  Abc_NtkDupObj( pNtkNew, pObj, 0 );
639  Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(pDriver->pCopy, !Abc_ObjFaninC0(pObj)) );
640  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_off" );
641  continue;
642  }
643  if ( Abc_ObjFaninNum(pDriver) == 0 )
644  {
645  Abc_NtkDupObj( pNtkNew, pObj, 0 );
646  Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFaninC0(pObj) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew) );
647  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_on" );
648 
649  Abc_NtkDupObj( pNtkNew, pObj, 0 );
650  Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFaninC0(pObj) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew) );
651  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_off" );
652  continue;
653  }
654  assert( Abc_ObjFaninNum(pObj) > 0 );
655  // onset/offset
656  for ( c = 0; c < 2; c++ )
657  {
658  Cudd_Srandom( 0 );
659  Abc_NtkDupObj( pNtkNew, pDriver, 0 );
660  Abc_ObjForEachFanin( pDriver, pFanin, k )
661  Abc_ObjAddFanin( pDriver->pCopy, pFanin->pCopy );
662  bFuncOld = Cudd_NotCond( (DdNode *)pDriver->pCopy->pData, c );
663  bFunc = Abc_NtkSparsifyInternalOne( ddNew, bFuncOld, Abc_ObjFaninNum(pDriver), nPerc ); Cudd_Ref( bFunc );
664  Cudd_RecursiveDeref( ddNew, bFuncOld );
665  pDriver->pCopy->pData = bFunc;
666  Abc_NtkDupObj( pNtkNew, pObj, 0 );
667  Abc_ObjAddFanin( pObj->pCopy, pDriver->pCopy );
668  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), c ? "_off" : "_on" );
669  }
670  }
671  Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
672  return pNtkNew;
673 }
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
void Cudd_Srandom(long seed)
Definition: cuddUtil.c:2764
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
ABC_DLL Abc_Obj_t * Abc_NtkDupObj(Abc_Ntk_t *pNtkNew, Abc_Obj_t *pObj, int fCopyName)
Definition: abcObj.c:337
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Definition: abcObj.c:633
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
char * Extra_UtilStrsav(const char *s)
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
Abc_Obj_t * pCopy
Definition: abc.h:148
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
Definition: abcUtil.c:1047
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst0(Abc_Ntk_t *pNtk)
Definition: abcObj.c:604
DdNode * Abc_NtkSparsifyInternalOne(DdManager *ddNew, DdNode *bFunc, int nFanins, int nPerc)
Definition: abcDsd.c:596
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DdNode* Abc_NtkSparsifyInternalOne ( DdManager ddNew,
DdNode bFunc,
int  nFanins,
int  nPerc 
)

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

Synopsis [Derives network with the given percentage of on-set and off-set minterms.]

Description []

SideEffects []

SeeAlso []

Definition at line 596 of file abcDsd.c.

597 {
598  int nSpace = (int)Cudd_CountMinterm( ddNew, bFunc, nFanins );
599  int i, nMints = Abc_MaxInt( 1, (int)(0.01 * nPerc * nSpace) );
600  DdNode ** pbMints = Cudd_bddPickArbitraryMinterms( ddNew, bFunc, ddNew->vars, nFanins, nMints );
601  DdNode * bRes;
602  for ( i = 0; i < nMints; i++ )
603  Cudd_Ref( pbMints[i] );
604  bRes = Extra_bddComputeSum( ddNew, pbMints, nMints ); Cudd_Ref( bRes );
605  for ( i = 0; i < nMints; i++ )
606  Cudd_RecursiveDeref( ddNew, pbMints[i] );
607  Cudd_Deref( bRes );
608  ABC_FREE( pbMints );
609  return bRes;
610 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
Definition: cudd.h:278
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdNode ** Cudd_bddPickArbitraryMinterms(DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
Definition: cuddUtil.c:1393
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode ** vars
Definition: cuddInt.h:390
DdNode * Extra_bddComputeSum(DdManager *dd, DdNode **pbCubes, int nCubes)
Definition: abcDsd.c:571
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DdNode* Extra_bddComputeSum ( DdManager dd,
DdNode **  pbCubes,
int  nCubes 
)

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

Synopsis [Computes the positive polarty cube composed of the first vars in the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 571 of file abcDsd.c.

572 {
573  DdNode * bRes, * bTemp;
574  int i;
575  bRes = b0; Cudd_Ref( bRes );
576  for ( i = 0; i < nCubes; i++ )
577  {
578  bRes = Cudd_bddOr( dd, bTemp = bRes, pbCubes[i] ); Cudd_Ref( bRes );
579  Cudd_RecursiveDeref( dd, bTemp );
580  }
581  Cudd_Deref( bRes );
582  return bRes;
583 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
#define b0
Definition: extraBdd.h:75
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129