abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dauTree.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dauTree.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware unmapping.]
8 
9  Synopsis [Canonical DSD package.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: dauTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "dauInt.h"
22 #include "misc/mem/mem.h"
23 #include "misc/util/utilTruth.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 typedef struct Dss_Fun_t_ Dss_Fun_t;
32 struct Dss_Fun_t_
33 {
34  unsigned iDsd : 26; // DSD literal
35  unsigned nFans : 6; // fanin count
36  unsigned char pFans[0]; // fanins
37 };
38 
39 typedef struct Dss_Ent_t_ Dss_Ent_t;
40 struct Dss_Ent_t_
41 {
42  Dss_Fun_t * pFunc;
43  Dss_Ent_t * pNext;
44  unsigned iDsd0 : 27; // dsd entry
45  unsigned nWords : 5; // total word count (struct + shared)
46  unsigned iDsd1 : 27; // dsd entry
47  unsigned nShared: 5; // shared count
48  unsigned char pShared[0]; // shared literals
49 };
50 
51 typedef struct Dss_Obj_t_ Dss_Obj_t;
52 struct Dss_Obj_t_
53 {
54  unsigned Id; // node ID
55  unsigned Type : 3; // node type
56  unsigned nSupp : 8; // variable
57  unsigned iVar : 8; // variable
58  unsigned nWords : 6; // variable
59  unsigned fMark0 : 1; // user mark
60  unsigned fMark1 : 1; // user mark
61  unsigned nFans : 5; // fanin count
62  unsigned pFans[0]; // fanins
63 };
64 
65 typedef struct Dss_Ntk_t_ Dss_Ntk_t;
66 struct Dss_Ntk_t_
67 {
68  int nVars; // the number of variables
69  int nMem; // memory used
70  int nMemAlloc; // memory allocated
71  word * pMem; // memory array
72  Dss_Obj_t * pRoot; // root node
73  Vec_Ptr_t * vObjs; // internal nodes
74 };
75 
76 struct Dss_Man_t_
77 {
78  int nVars; // variable number
79  int nNonDecLimit; // limit on non-dec size
80  int nBins; // table size
81  unsigned * pBins; // hash table
82  Mem_Flex_t * pMem; // memory for nodes
83  Vec_Ptr_t * vObjs; // objects
84  Vec_Int_t * vNexts; // next pointers
85  Vec_Int_t * vLeaves; // temp
86  Vec_Int_t * vCopies; // temp
87  word ** pTtElems; // elementary TTs
88  Dss_Ent_t ** pCache; // decomposition cache
89  int nCache; // size of decomposition cache
90  Mem_Flex_t * pMemEnts; // memory for cache entries
91  int nCacheHits[2];
92  int nCacheMisses[2];
93  int nCacheEntries[2];
94  abctime timeBeg;
95  abctime timeDec;
96  abctime timeLook;
97  abctime timeEnd;
98 };
99 
100 static inline Dss_Obj_t * Dss_Regular( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
101 static inline Dss_Obj_t * Dss_Not( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
102 static inline Dss_Obj_t * Dss_NotCond( Dss_Obj_t * p, int c ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
103 static inline int Dss_IsComplement( Dss_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
104 
105 static inline int Dss_EntWordNum( Dss_Ent_t * p ) { return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0); }
106 static inline int Dss_FunWordNum( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0); }
107 static inline int Dss_ObjWordNum( int nFans ) { return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
108 static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)pObj + pObj->nWords; }
109 
110 static inline void Dss_ObjClean( Dss_Obj_t * pObj ) { memset( pObj, 0, sizeof(Dss_Obj_t) ); }
111 static inline int Dss_ObjId( Dss_Obj_t * pObj ) { return pObj->Id; }
112 static inline int Dss_ObjType( Dss_Obj_t * pObj ) { return pObj->Type; }
113 static inline int Dss_ObjSuppSize( Dss_Obj_t * pObj ) { return pObj->nSupp; }
114 static inline int Dss_ObjFaninNum( Dss_Obj_t * pObj ) { return pObj->nFans; }
115 static inline int Dss_ObjFaninC( Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); }
116 
117 static inline Dss_Obj_t * Dss_VecObj( Vec_Ptr_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p, Id); }
118 static inline Dss_Obj_t * Dss_VecConst0( Vec_Ptr_t * p ) { return Dss_VecObj( p, 0 ); }
119 static inline Dss_Obj_t * Dss_VecVar( Vec_Ptr_t * p, int v ) { return Dss_VecObj( p, v+1 ); }
120 static inline int Dss_VecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return Dss_VecObj( p, Abc_Lit2Var(iLit) )->nSupp; }
121 
122 static inline int Dss_Obj2Lit( Dss_Obj_t * pObj ) { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj)); }
123 static inline Dss_Obj_t * Dss_Lit2Obj( Vec_Ptr_t * p, int iLit ) { return Dss_NotCond(Dss_VecObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); }
124 static inline Dss_Obj_t * Dss_ObjFanin( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_VecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
125 static inline Dss_Obj_t * Dss_ObjChild( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]); }
126 
127 #define Dss_VecForEachObj( vVec, pObj, i ) \
128  Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )
129 #define Dss_VecForEachObjVec( vLits, vVec, pObj, i ) \
130  for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
131 #define Dss_VecForEachNode( vVec, pObj, i ) \
132  Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i ) \
133  if ( pObj->Type == DAU_DSD_CONST0 || pObj->Type == DAU_DSD_VAR ) {} else
134 #define Dss_ObjForEachFanin( vVec, pObj, pFanin, i ) \
135  for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(vVec, pObj, i)); i++ )
136 #define Dss_ObjForEachChild( vVec, pObj, pFanin, i ) \
137  for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(vVec, pObj, i)); i++ )
138 
139 static inline int Dss_WordCountOnes( unsigned uWord )
140 {
141  uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
142  uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
143  uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
144  uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
145  return (uWord & 0x0000FFFF) + (uWord>>16);
146 }
147 
148 static inline int Dss_Lit2Lit( int * pMapLit, int Lit ) { return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) ); }
149 
150 ////////////////////////////////////////////////////////////////////////
151 /// FUNCTION DEFINITIONS ///
152 ////////////////////////////////////////////////////////////////////////
153 
154 #if 0
155 
156 /**Function*************************************************************
157 
158  Synopsis [Check decomposability for 666.]
159 
160  Description []
161 
162  SideEffects []
163 
164  SeeAlso []
165 
166 ***********************************************************************/
167 // recursively collects 6-feasible supports
168 int Dss_ObjCheck666_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, Vec_Int_t * vSupps )
169 {
170  Dss_Obj_t * pFanin;
171  int i, uSupp = 0;
172  assert( !Dss_IsComplement(pObj) );
173  if ( pObj->Type == DAU_DSD_VAR )
174  {
175  assert( pObj->iVar >= 0 && pObj->iVar < 30 );
176  return (1 << pObj->iVar);
177  }
178  if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
179  {
180  int c0, c1, c2, uSuppTemp;
181  int uSuppVars[16];
182  int nSuppVars = 0;
183  int nFanins = Dss_ObjFaninNum(pObj);
184  int uSupps[16], nSuppSizes[16];
185  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
186  {
187  uSupps[i] = Dss_ObjCheck666_rec( p, pFanin, vSupps );
188  nSuppSizes[i] = Dss_WordCountOnes( uSupps[i] );
189  uSupp |= uSupps[i];
190  if ( nSuppSizes[i] == 1 )
191  uSuppVars[nSuppVars++] = uSupps[i];
192  }
193  // iterate through the permutations
194  for ( c0 = 0; c0 < nFanins; c0++ )
195  if ( nSuppSizes[c0] > 1 && nSuppSizes[c0] < 6 )
196  {
197  uSuppTemp = uSupps[c0];
198  for ( i = 0; i < nSuppVars; i++ )
199  if ( nSuppSizes[c0] + i < 6 )
200  uSuppTemp |= uSuppVars[i];
201  else
202  break;
203  if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
204  Vec_IntPush( vSupps, uSuppTemp );
205 
206  for ( c1 = c0 + 1; c1 < nFanins; c1++ )
207  if ( nSuppSizes[c1] > 1 && nSuppSizes[c1] < 6 )
208  {
209  if ( nSuppSizes[c0] + nSuppSizes[c1] <= 6 )
210  Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] );
211 
212  uSuppTemp = uSupps[c0] | uSupps[c1];
213  for ( i = 0; i < nSuppVars; i++ )
214  if ( nSuppSizes[c0] + nSuppSizes[c1] + i < 6 )
215  uSuppTemp |= uSuppVars[i];
216  else
217  break;
218  if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
219  Vec_IntPush( vSupps, uSuppTemp );
220 
221  for ( c2 = c1 + 1; c2 < nFanins; c2++ )
222  if ( nSuppSizes[c2] > 1 && nSuppSizes[c2] < 6 )
223  {
224  if ( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] <= 6 )
225  Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] | uSupps[c2] );
226  assert( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] >= 6 );
227  }
228  }
229  }
230  if ( nSuppVars > 1 && nSuppVars <= 6 )
231  {
232  uSuppTemp = 0;
233  for ( i = 0; i < nSuppVars; i++ )
234  uSuppTemp |= uSuppVars[i];
235  Vec_IntPush( vSupps, uSuppTemp );
236  }
237  else if ( nSuppVars > 6 && nSuppVars <= 12 )
238  {
239  uSuppTemp = 0;
240  for ( i = 0; i < 6; i++ )
241  uSuppTemp |= uSuppVars[i];
242  Vec_IntPush( vSupps, uSuppTemp );
243 
244  uSuppTemp = 0;
245  for ( i = 6; i < nSuppVars; i++ )
246  uSuppTemp |= uSuppVars[i];
247  Vec_IntPush( vSupps, uSuppTemp );
248  }
249  }
250  else if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
251  {
252  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
253  uSupp |= Dss_ObjCheck666_rec( p, pFanin, vSupps );
254  }
255  if ( Dss_WordCountOnes( uSupp ) <= 6 )
256  Vec_IntPush( vSupps, uSupp );
257  return uSupp;
258 }
259 int Dss_ObjCheck666( Dss_Ntk_t * p )
260 {
261  Vec_Int_t * vSupps;
262  int i, k, SuppI, SuppK;
263  int nSupp = Dss_ObjSuppSize(Dss_Regular(p->pRoot));
264  if ( nSupp <= 6 )
265  return 1;
266  // compute supports
267  vSupps = Vec_IntAlloc( 100 );
268  Dss_ObjCheck666_rec( p, Dss_Regular(p->pRoot), vSupps );
269  Vec_IntUniqify( vSupps );
270  Vec_IntForEachEntry( vSupps, SuppI, i )
271  {
272  k = Dss_WordCountOnes(SuppI);
273  assert( k > 0 && k <= 6 );
274 /*
275  for ( k = 0; k < 16; k++ )
276  if ( (SuppI >> k) & 1 )
277  printf( "%c", 'a' + k );
278  else
279  printf( "-" );
280  printf( "\n" );
281 */
282  }
283  // consider support pairs
284  Vec_IntForEachEntry( vSupps, SuppI, i )
285  Vec_IntForEachEntryStart( vSupps, SuppK, k, i+1 )
286  {
287  if ( SuppI & SuppK )
288  continue;
289  if ( Dss_WordCountOnes(SuppI | SuppK) + 4 >= nSupp )
290  {
291  Vec_IntFree( vSupps );
292  return 1;
293  }
294  }
295  Vec_IntFree( vSupps );
296  return 0;
297 }
298 void Dau_DsdTest_()
299 {
300 /*
301  extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
302  extern void Dss_NtkFree( Dss_Ntk_t * p );
303 
304 // char * pDsd = "(!(amn!(bh))[cdeij]!(fklg)o)";
305  char * pDsd = "<[(ab)(cd)(ef)][(gh)(ij)(kl)](mn)>";
306  Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, 16, NULL );
307  int Status = Dss_ObjCheck666( pNtk );
308  Dss_NtkFree( pNtk );
309 */
310 }
311 
312 abctime if_dec_time;
313 
314 void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
315 {
316  extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
317  extern void Dss_NtkFree( Dss_Ntk_t * p );
318 
319  static abctime timeTt = 0;
320  static abctime timeDsd = 0;
321  abctime clkTt, clkDsd;
322 
323  char pDsd[1000];
324  word Truth[1024];
325  Dss_Ntk_t * pNtk;
326  int Status, nNonDec;
327 
328  if ( pTruth == NULL )
329  {
330  Abc_PrintTime( 1, "TT runtime", timeTt );
331  Abc_PrintTime( 1, "DSD runtime", timeDsd );
332  Abc_PrintTime( 1, "Total ", if_dec_time );
333 
334  if_dec_time = 0;
335  timeTt = 0;
336  timeDsd = 0;
337  return;
338  }
339 
340  Abc_TtCopy( Truth, pTruth, Abc_TtWordNum(nVars), 0 );
341  nNonDec = Dau_DsdDecompose( Truth, nVars, 0, 0, pDsd );
342  if ( nNonDec > 0 )
343  return;
344 
345  pNtk = Dss_NtkCreate( pDsd, 16, NULL );
346 
347  // measure DSD runtime
348  clkDsd = Abc_Clock();
349  Status = Dss_ObjCheck666( pNtk );
350  timeDsd += Abc_Clock() - clkDsd;
351 
352  Dss_NtkFree( pNtk );
353 
354  // measure TT runtime
355  clkTt = Abc_Clock();
356  {
357  #define CLU_VAR_MAX 16
358 
359  // decomposition
360  typedef struct If_Grp_t_ If_Grp_t;
361  struct If_Grp_t_
362  {
363  char nVars;
364  char nMyu;
365  char pVars[CLU_VAR_MAX];
366  };
367 
368 
369  int nLutLeaf = 6;
370  int nLutLeaf2 = 6;
371  int nLutRoot = 6;
372 
373  If_Grp_t G;
374  If_Grp_t G2, R;
375  word Func0, Func1, Func2;
376 
377  {
378  extern If_Grp_t If_CluCheck3( void * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
379  If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 );
380  G = If_CluCheck3( NULL, pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 );
381  }
382 
383  }
384  timeTt += Abc_Clock() - clkTt;
385 }
386 
387 #endif
388 
389 
390 /**Function*************************************************************
391 
392  Synopsis [Elementary truth tables.]
393 
394  Description []
395 
396  SideEffects []
397 
398  SeeAlso []
399 
400 ***********************************************************************/
401 static inline word ** Dss_ManTtElems()
402 {
403  static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
404  if ( pTtElems[0] == NULL )
405  {
406  int v;
407  for ( v = 0; v <= DAU_MAX_VAR; v++ )
408  pTtElems[v] = TtElems[v];
409  Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
410  }
411  return pTtElems;
412 }
413 
414 /**Function*************************************************************
415 
416  Synopsis [Creating DSD network.]
417 
418  Description []
419 
420  SideEffects []
421 
422  SeeAlso []
423 
424 ***********************************************************************/
425 Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars )
426 {
427  Dss_Obj_t * pObj;
428  pObj = (Dss_Obj_t *)(p->pMem + p->nMem);
429  Dss_ObjClean( pObj );
430  pObj->nFans = nFans;
431  pObj->nWords = Dss_ObjWordNum( nFans );
432  pObj->Type = Type;
433  pObj->Id = Vec_PtrSize( p->vObjs );
434  pObj->iVar = 31;
435  Vec_PtrPush( p->vObjs, pObj );
436  p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
437  assert( p->nMem < p->nMemAlloc );
438  return pObj;
439 }
440 Dss_Obj_t * Dss_ObjCreateNtk( Dss_Ntk_t * p, int Type, Vec_Int_t * vFaninLits )
441 {
442  Dss_Obj_t * pObj;
443  int i, Entry;
444  pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
445  Vec_IntForEachEntry( vFaninLits, Entry, i )
446  {
447  pObj->pFans[i] = Entry;
448  pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
449  }
450  assert( i == (int)pObj->nFans );
451  return pObj;
452 }
453 Dss_Ntk_t * Dss_NtkAlloc( int nVars )
454 {
455  Dss_Ntk_t * p;
456  Dss_Obj_t * pObj;
457  int i;
458  p = ABC_CALLOC( Dss_Ntk_t, 1 );
459  p->nVars = nVars;
460  p->nMemAlloc = DAU_MAX_STR;
461  p->pMem = ABC_ALLOC( word, p->nMemAlloc );
462  p->vObjs = Vec_PtrAlloc( 100 );
463  Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 );
464  for ( i = 0; i < nVars; i++ )
465  {
466  pObj = Dss_ObjAllocNtk( p, DAU_DSD_VAR, 0, 0 );
467  pObj->iVar = i;
468  pObj->nSupp = 1;
469  }
470  return p;
471 }
472 void Dss_NtkFree( Dss_Ntk_t * p )
473 {
474  Vec_PtrFree( p->vObjs );
475  ABC_FREE( p->pMem );
476  ABC_FREE( p );
477 }
478 void Dss_NtkPrint_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj )
479 {
480  char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
481  char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
482  Dss_Obj_t * pFanin;
483  int i;
484  assert( !Dss_IsComplement(pObj) );
485  if ( pObj->Type == DAU_DSD_VAR )
486  { printf( "%c", 'a' + pObj->iVar ); return; }
487  if ( pObj->Type == DAU_DSD_PRIME )
488  Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
489  printf( "%c", OpenType[pObj->Type] );
490  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
491  {
492  printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
493  Dss_NtkPrint_rec( p, pFanin );
494  }
495  printf( "%c", CloseType[pObj->Type] );
496 }
497 void Dss_NtkPrint( Dss_Ntk_t * p )
498 {
499  if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
500  printf( "%d", Dss_IsComplement(p->pRoot) );
501  else
502  {
503  printf( "%s", Dss_IsComplement(p->pRoot) ? "!":"" );
504  if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_VAR )
505  printf( "%c", 'a' + Dss_Regular(p->pRoot)->iVar );
506  else
507  Dss_NtkPrint_rec( p, Dss_Regular(p->pRoot) );
508  }
509  printf( "\n" );
510 }
511 
512 /**Function*************************************************************
513 
514  Synopsis [Creating DSD network from SOP.]
515 
516  Description []
517 
518  SideEffects []
519 
520  SeeAlso []
521 
522 ***********************************************************************/
523 static inline void Dau_DsdMergeMatches( char * pDsd, int * pMatches )
524 {
525  int pNested[DAU_MAX_VAR];
526  int i, nNested = 0;
527  for ( i = 0; pDsd[i]; i++ )
528  {
529  pMatches[i] = 0;
530  if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
531  pNested[nNested++] = i;
532  else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
533  pMatches[pNested[--nNested]] = i;
534  assert( nNested < DAU_MAX_VAR );
535  }
536  assert( nNested == 0 );
537 }
538 int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk, word * pTruth )
539 {
540  int fCompl = 0;
541  if ( **p == '!' )
542  {
543  fCompl = 1;
544  (*p)++;
545  }
546  while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
547  (*p)++;
548 /*
549  if ( **p == '<' )
550  {
551  char * q = pStr + pMatches[ *p - pStr ];
552  if ( *(q+1) == '{' )
553  *p = q+1;
554  }
555 */
556  if ( **p >= 'a' && **p <= 'z' ) // var
557  return Abc_Var2Lit( Dss_ObjId(Dss_VecVar(pNtk->vObjs, **p - 'a')), fCompl );
558  if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
559  {
560  Dss_Obj_t * pObj;
561  Vec_Int_t * vFaninLits = Vec_IntAlloc( 10 );
562  char * q = pStr + pMatches[ *p - pStr ];
563  int Type;
564  if ( **p == '(' )
565  Type = DAU_DSD_AND;
566  else if ( **p == '[' )
567  Type = DAU_DSD_XOR;
568  else if ( **p == '<' )
569  Type = DAU_DSD_MUX;
570  else if ( **p == '{' )
571  Type = DAU_DSD_PRIME;
572  else assert( 0 );
573  assert( *q == **p + 1 + (**p != '(') );
574  for ( (*p)++; *p < q; (*p)++ )
575  Vec_IntPush( vFaninLits, Dss_NtkCreate_rec(pStr, p, pMatches, pNtk, pTruth) );
576  assert( *p == q );
577  if ( Type == DAU_DSD_PRIME )
578  {
579  Vec_Int_t * vFaninLitsNew;
580  word pTemp[DAU_MAX_WORD];
581  char pCanonPerm[DAU_MAX_VAR];
582  int i, uCanonPhase, nFanins = Vec_IntSize(vFaninLits);
583  Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nFanins), 0 );
584  uCanonPhase = Abc_TtCanonicize( pTemp, nFanins, pCanonPerm );
585  fCompl = (uCanonPhase >> nFanins) & 1;
586  vFaninLitsNew = Vec_IntAlloc( nFanins );
587  for ( i = 0; i < nFanins; i++ )
588  Vec_IntPush( vFaninLitsNew, Abc_LitNotCond(Vec_IntEntry(vFaninLits, pCanonPerm[i]), (uCanonPhase>>i)&1) );
589  pObj = Dss_ObjCreateNtk( pNtk, DAU_DSD_PRIME, vFaninLitsNew );
590  Abc_TtCopy( Dss_ObjTruth(pObj), pTemp, Abc_TtWordNum(nFanins), 0 );
591  Vec_IntFree( vFaninLitsNew );
592  }
593  else
594  pObj = Dss_ObjCreateNtk( pNtk, Type, vFaninLits );
595  Vec_IntFree( vFaninLits );
596  return Abc_LitNotCond( Dss_Obj2Lit(pObj), fCompl );
597  }
598  assert( 0 );
599  return -1;
600 }
601 Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth )
602 {
603  int fCompl = 0;
604  Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars );
605  if ( *pDsd == '!' )
606  pDsd++, fCompl = 1;
607  if ( Dau_DsdIsConst(pDsd) )
608  pNtk->pRoot = Dss_VecConst0(pNtk->vObjs);
609  else if ( Dau_DsdIsVar(pDsd) )
610  pNtk->pRoot = Dss_VecVar(pNtk->vObjs, Dau_DsdReadVar(pDsd));
611  else
612  {
613  int iLit, pMatches[DAU_MAX_STR];
614  Dau_DsdMergeMatches( pDsd, pMatches );
615  iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk, pTruth );
616  pNtk->pRoot = Dss_Lit2Obj( pNtk->vObjs, iLit );
617  }
618  if ( fCompl )
619  pNtk->pRoot = Dss_Not(pNtk->pRoot);
620  return pNtk;
621 }
622 
623 /**Function*************************************************************
624 
625  Synopsis [Comparing two DSD nodes.]
626 
627  Description []
628 
629  SideEffects []
630 
631  SeeAlso []
632 
633 ***********************************************************************/
634 int Dss_ObjCompare( Vec_Ptr_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i )
635 {
636  Dss_Obj_t * p0 = Dss_Regular(p0i);
637  Dss_Obj_t * p1 = Dss_Regular(p1i);
638  Dss_Obj_t * pChild0, * pChild1;
639  int i, Res;
640  if ( Dss_ObjType(p0) < Dss_ObjType(p1) )
641  return -1;
642  if ( Dss_ObjType(p0) > Dss_ObjType(p1) )
643  return 1;
644  if ( Dss_ObjType(p0) < DAU_DSD_AND )
645  return 0;
646  if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) )
647  return -1;
648  if ( Dss_ObjFaninNum(p0) > Dss_ObjFaninNum(p1) )
649  return 1;
650  for ( i = 0; i < Dss_ObjFaninNum(p0); i++ )
651  {
652  pChild0 = Dss_ObjChild( p, p0, i );
653  pChild1 = Dss_ObjChild( p, p1, i );
654  Res = Dss_ObjCompare( p, pChild0, pChild1 );
655  if ( Res != 0 )
656  return Res;
657  }
658  if ( Dss_IsComplement(p0i) < Dss_IsComplement(p1i) )
659  return -1;
660  if ( Dss_IsComplement(p0i) > Dss_IsComplement(p1i) )
661  return 1;
662  return 0;
663 }
664 void Dss_ObjSort( Vec_Ptr_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm )
665 {
666  int i, j, best_i;
667  for ( i = 0; i < nNodes-1; i++ )
668  {
669  best_i = i;
670  for ( j = i+1; j < nNodes; j++ )
671  if ( Dss_ObjCompare(p, pNodes[best_i], pNodes[j]) == 1 )
672  best_i = j;
673  if ( i == best_i )
674  continue;
675  ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] );
676  if ( pPerm )
677  ABC_SWAP( int, pPerm[i], pPerm[best_i] );
678  }
679 }
680 
681 /**Function*************************************************************
682 
683  Synopsis []
684 
685  Description []
686 
687  SideEffects []
688 
689  SeeAlso []
690 
691 ***********************************************************************/
692 void Dss_NtkCheck( Dss_Ntk_t * p )
693 {
694  Dss_Obj_t * pObj, * pFanin;
695  int i, k;
696  Dss_VecForEachNode( p->vObjs, pObj, i )
697  {
698  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, k )
699  {
700  if ( pObj->Type == DAU_DSD_AND && pFanin->Type == DAU_DSD_AND )
701  assert( Dss_ObjFaninC(pObj, k) );
702  else if ( pObj->Type == DAU_DSD_XOR )
703  assert( pFanin->Type != DAU_DSD_XOR );
704  else if ( pObj->Type == DAU_DSD_MUX )
705  assert( !Dss_ObjFaninC(pObj, 0) );
706  }
707  }
708 }
709 int Dss_NtkCollectPerm_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, int * pPermDsd, int * pnPerms )
710 {
711  Dss_Obj_t * pChild;
712  int k, fCompl = Dss_IsComplement(pObj);
713  pObj = Dss_Regular( pObj );
714  if ( pObj->Type == DAU_DSD_VAR )
715  {
716  pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl);
717  pObj->iVar = (*pnPerms)++;
718  return fCompl;
719  }
720  Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
721  if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) )
722  pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]);
723  return 0;
724 }
725 void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd )
726 {
727  Dss_Obj_t * pChildren[DAU_MAX_VAR];
728  Dss_Obj_t * pObj, * pChild;
729  int i, k, nPerms;
730  if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
731  return;
732  Dss_VecForEachNode( p->vObjs, pObj, i )
733  {
734  if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
735  continue;
736  Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
737  pChildren[k] = pChild;
738  Dss_ObjSort( p->vObjs, pChildren, Dss_ObjFaninNum(pObj), NULL );
739  for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ )
740  pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] );
741  }
742  nPerms = 0;
743  if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) )
744  p->pRoot = Dss_Regular(p->pRoot);
745  assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp );
746 }
747 
748 
749 /**Function*************************************************************
750 
751  Synopsis []
752 
753  Description []
754 
755  SideEffects []
756 
757  SeeAlso []
758 
759 ***********************************************************************/
760 Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars )
761 {
762  int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
763  Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
764  Dss_ObjClean( pObj );
765  pObj->Type = Type;
766  pObj->nFans = nFans;
767  pObj->nWords = Dss_ObjWordNum(nFans);
768  pObj->Id = Vec_PtrSize( p->vObjs );
769  pObj->iVar = 31;
770  Vec_PtrPush( p->vObjs, pObj );
771  Vec_IntPush( p->vNexts, 0 );
772  return pObj;
773 }
774 Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
775 {
776  Dss_Obj_t * pObj, * pFanin, * pPrev = NULL;
777  int i, Entry;
778  // check structural canonicity
779  assert( Type != DAU_DSD_MUX || Vec_IntSize(vFaninLits) == 3 );
780  assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 0)) );
781  assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 1)) || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 2)) );
782  // check that leaves are in good order
783  if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
784  Dss_VecForEachObjVec( vFaninLits, p->vObjs, pFanin, i )
785  {
786  assert( Type != DAU_DSD_AND || Abc_LitIsCompl(Vec_IntEntry(vFaninLits, i)) || Dss_ObjType(pFanin) != DAU_DSD_AND );
787  assert( Type != DAU_DSD_XOR || Dss_ObjType(pFanin) != DAU_DSD_XOR );
788  assert( pPrev == NULL || Dss_ObjCompare(p->vObjs, pPrev, pFanin) <= 0 );
789  pPrev = pFanin;
790  }
791  // create new node
792  pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
793  if ( Type == DAU_DSD_PRIME )
794  Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 );
795  assert( pObj->nSupp == 0 );
796  Vec_IntForEachEntry( vFaninLits, Entry, i )
797  {
798  pObj->pFans[i] = Entry;
799  pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
800  }
801 /*
802  {
803  extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits );
804  Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
805  }
806 */
807  return pObj;
808 }
809 
810 /**Function*************************************************************
811 
812  Synopsis []
813 
814  Description []
815 
816  SideEffects []
817 
818  SeeAlso []
819 
820 ***********************************************************************/
821 void Dss_ManHashProfile( Dss_Man_t * p )
822 {
823  Dss_Obj_t * pObj;
824  unsigned * pSpot;
825  int i, Counter;
826  for ( i = 0; i < p->nBins; i++ )
827  {
828  Counter = 0;
829  for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
830  pObj = Dss_VecObj( p->vObjs, *pSpot );
831  if ( Counter )
832  printf( "%d ", Counter );
833  }
834  printf( "\n" );
835 }
836 static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
837 {
838  static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
839  int i, Entry;
840  unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147;
841  Vec_IntForEachEntry( vFaninLits, Entry, i )
842  uHash += Entry * s_Primes[i & 0x7];
843  assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) );
844  if ( pTruth )
845  {
846  unsigned char * pTruthC = (unsigned char *)pTruth;
847  int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits));
848  for ( i = 0; i < nBytes; i++ )
849  uHash += pTruthC[i] * s_Primes[i & 0x7];
850  }
851  return uHash % p->nBins;
852 }
853 unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
854 {
855  Dss_Obj_t * pObj;
856  unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth);
857  for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id) )
858  {
859  pObj = Dss_VecObj( p->vObjs, *pSpot );
860  if ( (int)pObj->Type == Type &&
861  (int)pObj->nFans == Vec_IntSize(vFaninLits) &&
862  !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) &&
863  (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, Abc_TtByteNum(pObj->nFans))) ) // equal
864  return pSpot;
865  }
866  return pSpot;
867 }
868 Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
869 {
870  Dss_Obj_t * pObj;
871  unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth );
872  if ( *pSpot )
873  return Dss_VecObj( p->vObjs, *pSpot );
874  *pSpot = Vec_PtrSize( p->vObjs );
875  pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth );
876  return pObj;
877 }
878 
879 /**Function*************************************************************
880 
881  Synopsis [Cache for decomposition calls.]
882 
883  Description []
884 
885  SideEffects []
886 
887  SeeAlso []
888 
889 ***********************************************************************/
890 void Dss_ManCacheAlloc( Dss_Man_t * p )
891 {
892  assert( p->nCache == 0 );
893  p->nCache = Abc_PrimeCudd( 100000 );
894  p->pCache = ABC_CALLOC( Dss_Ent_t *, p->nCache );
895 }
896 void Dss_ManCacheFree( Dss_Man_t * p )
897 {
898  if ( p->pCache == NULL )
899  return;
900  assert( p->nCache != 0 );
901  p->nCache = 0;
902  ABC_FREE( p->pCache );
903 }
904 static inline unsigned Dss_ManCacheHashKey( Dss_Man_t * p, Dss_Ent_t * pEnt )
905 {
906  static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
907  int i;
908  unsigned uHash = pEnt->nShared * 7103 + pEnt->iDsd0 * 7873 + pEnt->iDsd1 * 8147;
909  for ( i = 0; i < 2*(int)pEnt->nShared; i++ )
910  uHash += pEnt->pShared[i] * s_Primes[i & 0x7];
911  return uHash % p->nCache;
912 }
913 void Dss_ManCacheProfile( Dss_Man_t * p )
914 {
915  Dss_Ent_t ** pSpot;
916  int i, Counter;
917  for ( i = 0; i < p->nCache; i++ )
918  {
919  Counter = 0;
920  for ( pSpot = p->pCache + i; *pSpot; pSpot = &(*pSpot)->pNext, Counter++ )
921  ;
922  if ( Counter )
923  printf( "%d ", Counter );
924  }
925  printf( "\n" );
926 }
927 Dss_Ent_t ** Dss_ManCacheLookup( Dss_Man_t * p, Dss_Ent_t * pEnt )
928 {
929  Dss_Ent_t ** pSpot = p->pCache + Dss_ManCacheHashKey( p, pEnt );
930  for ( ; *pSpot; pSpot = &(*pSpot)->pNext )
931  {
932  if ( (*pSpot)->iDsd0 == pEnt->iDsd0 &&
933  (*pSpot)->iDsd1 == pEnt->iDsd1 &&
934  (*pSpot)->nShared == pEnt->nShared &&
935  !memcmp((*pSpot)->pShared, pEnt->pShared, sizeof(char)*2*pEnt->nShared) ) // equal
936  {
937  p->nCacheHits[pEnt->nShared!=0]++;
938  return pSpot;
939  }
940  }
941  p->nCacheMisses[pEnt->nShared!=0]++;
942  return pSpot;
943 }
944 Dss_Ent_t * Dss_ManCacheCreate( Dss_Man_t * p, Dss_Ent_t * pEnt0, Dss_Fun_t * pFun0 )
945 {
946  Dss_Ent_t * pEnt = (Dss_Ent_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * pEnt0->nWords );
947  Dss_Fun_t * pFun = (Dss_Fun_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * Dss_FunWordNum(pFun0) );
948  memcpy( pEnt, pEnt0, sizeof(word) * pEnt0->nWords );
949  memcpy( pFun, pFun0, sizeof(word) * Dss_FunWordNum(pFun0) );
950  pEnt->pFunc = pFun;
951  pEnt->pNext = NULL;
952  p->nCacheEntries[pEnt->nShared!=0]++;
953  return pEnt;
954 }
955 
956 /**Function*************************************************************
957 
958  Synopsis []
959 
960  Description []
961 
962  SideEffects []
963 
964  SeeAlso []
965 
966 ***********************************************************************/
967 Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit )
968 {
969  Dss_Man_t * p;
970  p = ABC_CALLOC( Dss_Man_t, 1 );
971  p->nVars = nVars;
972  p->nNonDecLimit = nNonDecLimit;
973  p->nBins = Abc_PrimeCudd( 1000000 );
974  p->pBins = ABC_CALLOC( unsigned, p->nBins );
975  p->pMem = Mem_FlexStart();
976  p->vObjs = Vec_PtrAlloc( 10000 );
977  p->vNexts = Vec_IntAlloc( 10000 );
978  Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 );
979  Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 )->nSupp = 1;
980  p->vLeaves = Vec_IntAlloc( 32 );
981  p->vCopies = Vec_IntAlloc( 32 );
982  p->pTtElems = Dss_ManTtElems();
983  p->pMemEnts = Mem_FlexStart();
984 // Dss_ManCacheAlloc( p );
985  return p;
986 }
987 void Dss_ManFree( Dss_Man_t * p )
988 {
989  Abc_PrintTime( 1, "Time begin ", p->timeBeg );
990  Abc_PrintTime( 1, "Time decomp", p->timeDec );
991  Abc_PrintTime( 1, "Time lookup", p->timeLook );
992  Abc_PrintTime( 1, "Time end ", p->timeEnd );
993 
994 // Dss_ManCacheProfile( p );
995  Dss_ManCacheFree( p );
996  Mem_FlexStop( p->pMemEnts, 0 );
997  Vec_IntFreeP( &p->vCopies );
998  Vec_IntFreeP( &p->vLeaves );
999  Vec_IntFreeP( &p->vNexts );
1000  Vec_PtrFreeP( &p->vObjs );
1001  Mem_FlexStop( p->pMem, 0 );
1002  ABC_FREE( p->pBins );
1003  ABC_FREE( p );
1004 }
1005 void Dss_ManPrint_rec( FILE * pFile, Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits, int * pnSupp )
1006 {
1007  char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
1008  char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
1009  Dss_Obj_t * pFanin;
1010  int i;
1011  assert( !Dss_IsComplement(pObj) );
1012  if ( pObj->Type == DAU_DSD_CONST0 )
1013  { fprintf( pFile, "0" ); return; }
1014  if ( pObj->Type == DAU_DSD_VAR )
1015  {
1016  int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
1017  fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
1018  return;
1019  }
1020  if ( pObj->Type == DAU_DSD_PRIME )
1021  Abc_TtPrintHexRev( pFile, Dss_ObjTruth(pObj), pObj->nFans );
1022  fprintf( pFile, "%c", OpenType[pObj->Type] );
1023  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1024  {
1025  fprintf( pFile, "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
1026  Dss_ManPrint_rec( pFile, p, pFanin, pPermLits, pnSupp );
1027  }
1028  fprintf( pFile, "%c", CloseType[pObj->Type] );
1029 }
1030 void Dss_ManPrintOne( FILE * pFile, Dss_Man_t * p, int iDsdLit, int * pPermLits )
1031 {
1032  int nSupp = 0;
1033  fprintf( pFile, "%6d : ", Abc_Lit2Var(iDsdLit) );
1034  fprintf( pFile, "%2d ", Dss_VecLitSuppSize(p->vObjs, iDsdLit) );
1035  fprintf( pFile, "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" );
1036  Dss_ManPrint_rec( pFile, p, Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit)), pPermLits, &nSupp );
1037  fprintf( pFile, "\n" );
1038  assert( nSupp == (int)Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit))->nSupp );
1039 }
1040 int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
1041 {
1042  Dss_Obj_t * pFanin;
1043  int i;
1044  assert( !Dss_IsComplement(pObj) );
1045  if ( pObj->Type == DAU_DSD_CONST0 )
1046  return 0;
1047  if ( pObj->Type == DAU_DSD_VAR )
1048  return 0;
1049  if ( pObj->Type == DAU_DSD_PRIME )
1050  return 1;
1051  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1052  if ( Dss_ManCheckNonDec_rec( p, pFanin ) )
1053  return 1;
1054  return 0;
1055 }
1056 void Dss_ManDump( Dss_Man_t * p )
1057 {
1058  char * pFileName = "dss_tts.txt";
1059  FILE * pFile;
1060  word Temp[DAU_MAX_WORD];
1061  Dss_Obj_t * pObj;
1062  int i;
1063  pFile = fopen( pFileName, "wb" );
1064  if ( pFile == NULL )
1065  {
1066  printf( "Cannot open file \"%s\".\n", pFileName );
1067  return;
1068  }
1069  Dss_VecForEachObj( p->vObjs, pObj, i )
1070  {
1071  if ( pObj->Type != DAU_DSD_PRIME )
1072  continue;
1073  Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 );
1074  Abc_TtStretch6( Temp, pObj->nFans, p->nVars );
1075  fprintf( pFile, "0x" );
1076  Abc_TtPrintHexRev( pFile, Temp, p->nVars );
1077  fprintf( pFile, "\n" );
1078 
1079 // printf( "%6d : ", i );
1080 // Abc_TtPrintHexRev( stdout, Temp, p->nVars );
1081 // printf( " " );
1082 // Dau_DsdPrintFromTruth( stdout, Temp, p->nVars );
1083  }
1084  fclose( pFile );
1085 }
1086 void Dss_ManPrint( char * pFileName, Dss_Man_t * p )
1087 {
1088  Dss_Obj_t * pObj;
1089  int CountNonDsd = 0, CountNonDsdStr = 0;
1090  int i, clk = Abc_Clock();
1091  FILE * pFile;
1092  pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
1093  if ( pFileName && pFile == NULL )
1094  {
1095  printf( "cannot open output file\n" );
1096  return;
1097  }
1098  Dss_VecForEachObj( p->vObjs, pObj, i )
1099  {
1100  CountNonDsd += (pObj->Type == DAU_DSD_PRIME);
1101  CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj );
1102  }
1103  fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) );
1104  fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", p->nNonDecLimit, CountNonDsd );
1105  fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr );
1106  fprintf( pFile, "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
1107  fprintf( pFile, "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
1108  fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
1109  fprintf( pFile, "Memory used for cache = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMemEnts)/(1<<20) );
1110  fprintf( pFile, "Cache hits = %8d %8d\n", p->nCacheHits[0], p->nCacheHits[1] );
1111  fprintf( pFile, "Cache misses = %8d %8d\n", p->nCacheMisses[0], p->nCacheMisses[1] );
1112  fprintf( pFile, "Cache entries = %8d %8d\n", p->nCacheEntries[0], p->nCacheEntries[1] );
1113  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1114 // Dss_ManHashProfile( p );
1115 // Dss_ManDump( p );
1116 // return;
1117  Dss_VecForEachObj( p->vObjs, pObj, i )
1118  {
1119  if ( i == 50 )
1120  break;
1121  Dss_ManPrintOne( pFile, p, Dss_Obj2Lit(pObj), NULL );
1122  }
1123  fprintf( pFile, "\n" );
1124  if ( pFileName )
1125  fclose( pFile );
1126 }
1127 
1128 /**Function*************************************************************
1129 
1130  Synopsis []
1131 
1132  Description []
1133 
1134  SideEffects []
1135 
1136  SeeAlso []
1137 
1138 ***********************************************************************/
1139 void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits, int * pnSupp )
1140 {
1141  Dss_Obj_t * pChild;
1142  int nWords = Abc_TtWordNum(nVars);
1143  int i, fCompl = Dss_IsComplement(pObj);
1144  pObj = Dss_Regular(pObj);
1145  if ( pObj->Type == DAU_DSD_VAR )
1146  {
1147  int iPermLit = pPermLits[(*pnSupp)++];
1148  assert( (*pnSupp) <= nVars );
1149  Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
1150  return;
1151  }
1152  if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
1153  {
1154  word pTtTemp[DAU_MAX_WORD];
1155  if ( pObj->Type == DAU_DSD_AND )
1156  Abc_TtConst1( pRes, nWords );
1157  else
1158  Abc_TtConst0( pRes, nWords );
1159  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1160  {
1161  Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits, pnSupp );
1162  if ( pObj->Type == DAU_DSD_AND )
1163  Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
1164  else
1165  Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
1166  }
1167  if ( fCompl ) Abc_TtNot( pRes, nWords );
1168  return;
1169  }
1170  if ( pObj->Type == DAU_DSD_MUX ) // mux
1171  {
1172  word pTtTemp[3][DAU_MAX_WORD];
1173  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1174  Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits, pnSupp );
1175  assert( i == 3 );
1176  Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
1177  if ( fCompl ) Abc_TtNot( pRes, nWords );
1178  return;
1179  }
1180  if ( pObj->Type == DAU_DSD_PRIME ) // function
1181  {
1182  word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
1183  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1184  Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits, pnSupp );
1185  Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords );
1186  if ( fCompl ) Abc_TtNot( pRes, nWords );
1187  return;
1188  }
1189  assert( 0 );
1190 
1191 }
1192 word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits )
1193 {
1194  Dss_Obj_t * pObj = Dss_Lit2Obj(p->vObjs, iDsd);
1195  word * pRes = p->pTtElems[DAU_MAX_VAR];
1196  int nWords = Abc_TtWordNum( nVars );
1197  int nSupp = 0;
1198  assert( nVars <= DAU_MAX_VAR );
1199  if ( iDsd == 0 )
1200  Abc_TtConst0( pRes, nWords );
1201  else if ( iDsd == 1 )
1202  Abc_TtConst1( pRes, nWords );
1203  else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR )
1204  {
1205  int iPermLit = pPermLits[nSupp++];
1206  Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
1207  }
1208  else
1209  Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits, &nSupp );
1210  assert( nSupp == (int)Dss_Regular(pObj)->nSupp );
1211  return pRes;
1212 }
1213 
1214 
1215 /**Function*************************************************************
1216 
1217  Synopsis []
1218 
1219  Description []
1220 
1221  SideEffects []
1222 
1223  SeeAlso []
1224 
1225 ***********************************************************************/
1226 // returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl
1227 int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj )
1228 {
1229  Dss_Obj_t * pChildren[DAU_MAX_VAR];
1230  Dss_Obj_t * pChild, * pObjNew;
1231  int i, k, fCompl = Dss_IsComplement(pObj);
1232  pObj = Dss_Regular(pObj);
1233  if ( pObj->Type == DAU_DSD_VAR )
1234  return Abc_Var2Lit( 1, fCompl );
1235  Dss_ObjForEachChild( pNtk->vObjs, pObj, pChild, k )
1236  {
1237  pChildren[k] = Dss_Lit2Obj( p->vObjs, Dss_NtkRebuild_rec( p, pNtk, pChild ) );
1238  if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) )
1239  pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1;
1240  }
1241  // normalize MUX
1242  if ( pObj->Type == DAU_DSD_MUX )
1243  {
1244  if ( Dss_IsComplement(pChildren[0]) )
1245  {
1246  pChildren[0] = Dss_Not(pChildren[0]);
1247  ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] );
1248  }
1249  if ( Dss_IsComplement(pChildren[1]) )
1250  {
1251  pChildren[1] = Dss_Not(pChildren[1]);
1252  pChildren[2] = Dss_Not(pChildren[2]);
1253  fCompl ^= 1;
1254  }
1255  }
1256  // shift subgraphs
1257  Vec_IntClear( p->vLeaves );
1258  for ( i = 0; i < k; i++ )
1259  Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
1260  // create new graph
1261  pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
1262  return Abc_Var2Lit( pObjNew->Id, fCompl );
1263 }
1264 int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
1265 {
1266  assert( p->nVars == pNtk->nVars );
1267  if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
1268  return Dss_IsComplement(pNtk->pRoot);
1269  if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
1270  return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar + 1, Dss_IsComplement(pNtk->pRoot) );
1271  return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot );
1272 }
1273 
1274 /**Function*************************************************************
1275 
1276  Synopsis [Performs DSD operation on the two literals.]
1277 
1278  Description [Returns the perm of the resulting literals. The perm size
1279  is equal to the number of support variables. The perm variables are 0-based
1280  numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
1281 
1282  SideEffects []
1283 
1284  SeeAlso []
1285 
1286 ***********************************************************************/
1287 int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
1288 {
1289  Dss_Obj_t * pChildren[DAU_MAX_VAR];
1290  Dss_Obj_t * pObj, * pChild;
1291  int i, k, nChildren = 0, fCompl = 0, fComplFan;
1292 
1293  assert( Type == DAU_DSD_AND || pPerm == NULL );
1294  if ( Type == DAU_DSD_AND && pPerm != NULL )
1295  {
1296  int pBegEnd[DAU_MAX_VAR];
1297  int j, nSSize = 0;
1298  for ( k = 0; k < nLits; k++ )
1299  {
1300  pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
1301  if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
1302  {
1303  fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj));
1304  if ( fComplFan )
1305  pObj = Dss_Regular(pObj);
1306  pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pObj)->nSupp);
1307  nSSize += Dss_Regular(pObj)->nSupp;
1308  pChildren[nChildren++] = pObj;
1309  }
1310  else
1311  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1312  {
1313  fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild));
1314  if ( fComplFan )
1315  pChild = Dss_Regular(pChild);
1316  pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp);
1317  nSSize += Dss_Regular(pChild)->nSupp;
1318  pChildren[nChildren++] = pChild;
1319  }
1320  }
1321  Dss_ObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
1322  // create permutation
1323  for ( j = i = 0; i < nChildren; i++ )
1324  for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
1325  pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 );
1326  assert( j == nSSize );
1327  }
1328  else if ( Type == DAU_DSD_AND )
1329  {
1330  for ( k = 0; k < nLits; k++ )
1331  {
1332  pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
1333  if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
1334  pChildren[nChildren++] = pObj;
1335  else
1336  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1337  pChildren[nChildren++] = pChild;
1338  }
1339  Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
1340  }
1341  else if ( Type == DAU_DSD_XOR )
1342  {
1343  for ( k = 0; k < nLits; k++ )
1344  {
1345  fCompl ^= Abc_LitIsCompl(pLits[k]);
1346  pObj = Dss_Lit2Obj(p->vObjs, Abc_LitRegular(pLits[k]));
1347  if ( pObj->Type != DAU_DSD_XOR )
1348  pChildren[nChildren++] = pObj;
1349  else
1350  Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1351  {
1352  assert( !Dss_IsComplement(pChild) );
1353  pChildren[nChildren++] = pChild;
1354  }
1355  }
1356  Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
1357  }
1358  else if ( Type == DAU_DSD_MUX )
1359  {
1360  if ( Abc_LitIsCompl(pLits[0]) )
1361  {
1362  pLits[0] = Abc_LitNot(pLits[0]);
1363  ABC_SWAP( int, pLits[1], pLits[2] );
1364  }
1365  if ( Abc_LitIsCompl(pLits[1]) )
1366  {
1367  pLits[1] = Abc_LitNot(pLits[1]);
1368  pLits[2] = Abc_LitNot(pLits[2]);
1369  fCompl ^= 1;
1370  }
1371  for ( k = 0; k < nLits; k++ )
1372  pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
1373  }
1374  else if ( Type == DAU_DSD_PRIME )
1375  {
1376  for ( k = 0; k < nLits; k++ )
1377  pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
1378  }
1379  else assert( 0 );
1380 
1381  // shift subgraphs
1382  Vec_IntClear( p->vLeaves );
1383  for ( i = 0; i < nChildren; i++ )
1384  Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
1385  // create new graph
1386  pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth );
1387  return Abc_Var2Lit( pObj->Id, fCompl );
1388 }
1389 Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int nFansTot )
1390 {
1391  static char Buffer[100];
1392  Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
1393  pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL );
1394 //printf( "%d %d -> %d ", iDsd[0], iDsd[1], pFun->iDsd );
1395  pFun->nFans = nFansTot;
1396  assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1397  return pFun;
1398 }
1399 
1400 /**Function*************************************************************
1401 
1402  Synopsis []
1403 
1404  Description []
1405 
1406  SideEffects []
1407 
1408  SeeAlso []
1409 
1410 ***********************************************************************/
1411 void Dss_EntPrint( Dss_Ent_t * p, Dss_Fun_t * pFun )
1412 {
1413  int i;
1414  printf( "%d %d ", p->iDsd0, p->iDsd1 );
1415  for ( i = 0; i < (int)p->nShared; i++ )
1416  printf( "%d=%d ", p->pShared[2*i], p->pShared[2*i+1] );
1417  printf( "-> %d ", pFun->iDsd );
1418 }
1419 
1420 /**Function*************************************************************
1421 
1422  Synopsis [Performs AND on two DSD functions with support overlap.]
1423 
1424  Description [Returns the perm of the resulting literals. The perm size
1425  is equal to the number of support variables. The perm variables are 0-based
1426  numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
1427 
1428  SideEffects []
1429 
1430  SeeAlso []
1431 
1432 ***********************************************************************/
1433 Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int Counter )
1434 {
1435  static char Buffer[100];
1436  Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
1437  Dss_Ntk_t * pNtk;
1438  word * pTruthOne, pTruth[DAU_MAX_WORD];
1439  char pDsd[DAU_MAX_STR];
1440  int pMapDsd2Truth[DAU_MAX_VAR];
1441  int pPermLits[DAU_MAX_VAR];
1442  int pPermDsd[DAU_MAX_VAR];
1443  int i, nNonDec, nSuppSize = 0;
1444  int nFans[2];
1445  nFans[0] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd0 );
1446  nFans[1] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd1 );
1447  // create first truth table
1448  for ( i = 0; i < nFans[0]; i++ )
1449  {
1450  pMapDsd2Truth[nSuppSize] = i;
1451  pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
1452  }
1453  pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
1454  Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
1455 if ( Counter )
1456 {
1457 //Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1458 }
1459  // create second truth table
1460  for ( i = 0; i < nFans[1]; i++ )
1461  pPermLits[i] = -1;
1462  for ( i = 0; i < (int)pEnt->nShared; i++ )
1463  pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1];
1464  for ( i = 0; i < nFans[1]; i++ )
1465  if ( pPermLits[i] == -1 )
1466  {
1467  pMapDsd2Truth[nSuppSize] = nFans[0] + i;
1468  pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
1469  }
1470  pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
1471 if ( Counter )
1472 {
1473 //Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1474 }
1475  Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
1476  // perform decomposition
1477  nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd );
1478  if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit )
1479  return NULL;
1480  // derive network and convert it into the manager
1481  pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL );
1482 //Dss_NtkPrint( pNtk );
1483  Dss_NtkCheck( pNtk );
1484  Dss_NtkTransform( pNtk, pPermDsd );
1485 //Dss_NtkPrint( pNtk );
1486  pFun->iDsd = Dss_NtkRebuild( p, pNtk );
1487  Dss_NtkFree( pNtk );
1488  // pPermDsd maps vars of iDsdRes into literals of pTruth
1489  // translate this map into the one that maps vars of iDsdRes into literals of cut
1490  pFun->nFans = Dss_VecLitSuppSize( p->vObjs, pFun->iDsd );
1491  for ( i = 0; i < (int)pFun->nFans; i++ )
1492  pFun->pFans[i] = (unsigned char)Abc_Lit2LitV( pMapDsd2Truth, pPermDsd[i] );
1493 
1494 // Dss_EntPrint( pEnt, pFun );
1495  return pFun;
1496 }
1497 
1498 /**Function*************************************************************
1499 
1500  Synopsis []
1501 
1502  Description []
1503 
1504  SideEffects []
1505 
1506  SeeAlso []
1507 
1508 ***********************************************************************/
1509 // returns mapping of variables of dsd1 into literals of dsd0
1510 Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask )
1511 {
1512  static char Buffer[100];
1513  Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
1514  pEnt->iDsd0 = iDsd[0];
1515  pEnt->iDsd1 = iDsd[1];
1516  pEnt->nShared = 0;
1517  if ( uSharedMask )
1518  {
1519  int i, g, pMapGtoL[DAU_MAX_VAR] = {-1};
1520  for ( i = 0; i < nFans[0]; i++ )
1521  pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) );
1522  for ( i = 0; i < nFans[1]; i++ )
1523  {
1524  g = Abc_Lit2Var( pFans[1][i] );
1525  if ( (uSharedMask >> g) & 1 )
1526  {
1527  assert( pMapGtoL[g] >= 0 );
1528  pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i;
1529  pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) );
1530  pEnt->nShared++;
1531  }
1532  }
1533  }
1534  pEnt->nWords = Dss_EntWordNum( pEnt );
1535  return pEnt;
1536 }
1537 
1538 // merge two DSD functions
1539 int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes, word * pTruth )
1540 {
1541  int fVerbose = 0;
1542  int fCheck = 0;
1543  static int Counter = 0;
1544 // word pTtTemp[DAU_MAX_WORD];
1545  word * pTruthOne;
1546  int pPermResInt[DAU_MAX_VAR];
1547  Dss_Ent_t * pEnt, ** ppSpot;
1548  Dss_Fun_t * pFun;
1549  int i;
1550  abctime clk;
1551  Counter++;
1552  if ( DAU_MAX_VAR < nKLutSize )
1553  {
1554  printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
1555  return -1;
1556  }
1557  assert( iDsd[0] <= iDsd[1] );
1558 
1559 if ( fVerbose )
1560 {
1561 Dss_ManPrintOne( stdout, p, iDsd[0], pFans[0] );
1562 Dss_ManPrintOne( stdout, p, iDsd[1], pFans[1] );
1563 }
1564 
1565  // constant argument
1566  if ( iDsd[0] == 0 ) return 0;
1567  if ( iDsd[0] == 1 ) return iDsd[1];
1568  if ( iDsd[1] == 0 ) return 0;
1569  if ( iDsd[1] == 1 ) return iDsd[0];
1570 
1571  // no overlap
1572 clk = Abc_Clock();
1573  assert( nFans[0] == Dss_VecLitSuppSize(p->vObjs, iDsd[0]) );
1574  assert( nFans[1] == Dss_VecLitSuppSize(p->vObjs, iDsd[1]) );
1575  assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
1576  // create map of shared variables
1577  pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
1578 p->timeBeg += Abc_Clock() - clk;
1579  // check cache
1580  if ( p->pCache == NULL )
1581  {
1582 clk = Abc_Clock();
1583  if ( uSharedMask == 0 )
1584  pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
1585  else
1586  pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1587  if ( pFun == NULL )
1588  return -1;
1589  assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1590  assert( (int)pFun->nFans <= nKLutSize );
1591 p->timeDec += Abc_Clock() - clk;
1592  }
1593  else
1594  {
1595 clk = Abc_Clock();
1596  ppSpot = Dss_ManCacheLookup( p, pEnt );
1597 p->timeLook += Abc_Clock() - clk;
1598 clk = Abc_Clock();
1599  if ( *ppSpot == NULL )
1600  {
1601  if ( uSharedMask == 0 )
1602  pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
1603  else
1604  pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1605  if ( pFun == NULL )
1606  return -1;
1607  assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1608  assert( (int)pFun->nFans <= nKLutSize );
1609  // create cache entry
1610  *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
1611  }
1612  pFun = (*ppSpot)->pFunc;
1613 p->timeDec += Abc_Clock() - clk;
1614  }
1615 
1616 clk = Abc_Clock();
1617  for ( i = 0; i < (int)pFun->nFans; i++ )
1618  if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
1619  pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
1620  else
1621  pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] );
1622  // perform support minimization
1623  if ( uSharedMask && pFun->nFans > 1 )
1624  {
1625  int pVarPres[DAU_MAX_VAR];
1626  int nSupp = 0;
1627  for ( i = 0; i < p->nVars; i++ )
1628  pVarPres[i] = -1;
1629  for ( i = 0; i < (int)pFun->nFans; i++ )
1630  pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i;
1631  for ( i = 0; i < p->nVars; i++ )
1632  if ( pVarPres[i] >= 0 )
1633  pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) );
1634  assert( nSupp == (int)pFun->nFans );
1635  }
1636 
1637  for ( i = 0; i < (int)pFun->nFans; i++ )
1638  pPermResInt[i] = pPermRes[i];
1639 p->timeEnd += Abc_Clock() - clk;
1640 
1641 if ( fVerbose )
1642 {
1643 Dss_ManPrintOne( stdout, p, pFun->iDsd, pPermResInt );
1644 printf( "\n" );
1645 }
1646 
1647 if ( Counter == 43418 )
1648 {
1649 // int s = 0;
1650 // Dss_ManPrint( NULL, p );
1651 }
1652 
1653 
1654  if ( fCheck )
1655  {
1656  pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
1657  if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
1658  {
1659  int s;
1660  // Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1661  // Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" );
1662  printf( "Verification failed.\n" );
1663  s = 0;
1664  }
1665  }
1666  return pFun->iDsd;
1667 }
1668 
1669 
1670 /**Function*************************************************************
1671 
1672  Synopsis []
1673 
1674  Description []
1675 
1676  SideEffects []
1677 
1678  SeeAlso []
1679 
1680 ***********************************************************************/
1681 Dss_Ent_t * Dss_ManSharedMapDerive( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared )
1682 {
1683  static char Buffer[100];
1684  Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
1685  pEnt->iDsd0 = iDsd0;
1686  pEnt->iDsd1 = iDsd1;
1687  pEnt->nShared = Vec_StrSize(vShared)/2;
1688  memcpy( pEnt->pShared, (unsigned char *)Vec_StrArray(vShared), sizeof(char) * Vec_StrSize(vShared) );
1689  pEnt->nWords = Dss_EntWordNum( pEnt );
1690  return pEnt;
1691 }
1692 
1693 int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, int * pPerm, int * pnLeaves )
1694 {
1695  int fVerbose = 0;
1696 // int fCheck = 0;
1697  Dss_Ent_t * pEnt, ** ppSpot;
1698  Dss_Fun_t * pFun;
1699  int iDsd[2] = { iDsd0, iDsd1 };
1700  int i;
1701  abctime clk;
1702 
1703  assert( iDsd0 <= iDsd1 );
1704  if ( DAU_MAX_VAR < *pnLeaves )
1705  {
1706  printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
1707  return -1;
1708  }
1709  if ( fVerbose )
1710  {
1711  Dss_ManPrintOne( stdout, p, iDsd0, NULL );
1712  Dss_ManPrintOne( stdout, p, iDsd1, NULL );
1713  }
1714 
1715 clk = Abc_Clock();
1716  pEnt = Dss_ManSharedMapDerive( p, iDsd0, iDsd1, vShared );
1717  ppSpot = Dss_ManCacheLookup( p, pEnt );
1718 p->timeLook += Abc_Clock() - clk;
1719 
1720 clk = Abc_Clock();
1721  if ( *ppSpot == NULL )
1722  {
1723  if ( Vec_StrSize(vShared) == 0 )
1724  pFun = Dss_ManOperationFun( p, iDsd, *pnLeaves );
1725  else
1726  pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1727  if ( pFun == NULL )
1728  return -1;
1729  assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1730  assert( (int)pFun->nFans <= *pnLeaves );
1731  // create cache entry
1732  *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
1733  }
1734  pFun = (*ppSpot)->pFunc;
1735 p->timeDec += Abc_Clock() - clk;
1736 
1737  *pnLeaves = (int)pFun->nFans;
1738  for ( i = 0; i < (int)pFun->nFans; i++ )
1739  pPerm[i] = (int)pFun->pFans[i];
1740 
1741  if ( fVerbose )
1742  {
1743  Dss_ManPrintOne( stdout, p, pFun->iDsd, NULL );
1744  printf( "\n" );
1745  }
1746 
1747 /*
1748  if ( fCheck )
1749  {
1750  pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
1751  if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
1752  {
1753  int s;
1754  // Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1755  // Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" );
1756  printf( "Verification failed.\n" );
1757  s = 0;
1758  }
1759  }
1760 */
1761  return pFun->iDsd;
1762 }
1763 
1764 
1765 /**Function*************************************************************
1766 
1767  Synopsis []
1768 
1769  Description []
1770 
1771  SideEffects []
1772 
1773  SeeAlso []
1774 
1775 ***********************************************************************/
1776 int Dss_ObjCheckTransparent( Dss_Man_t * p, Dss_Obj_t * pObj )
1777 {
1778  Dss_Obj_t * pFanin;
1779  int i;
1780  if ( pObj->Type == DAU_DSD_VAR )
1781  return 1;
1782  if ( pObj->Type == DAU_DSD_AND )
1783  return 0;
1784  if ( pObj->Type == DAU_DSD_XOR )
1785  {
1786  Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1787  if ( Dss_ObjCheckTransparent( p, pFanin ) )
1788  return 1;
1789  return 0;
1790  }
1791  if ( pObj->Type == DAU_DSD_MUX )
1792  {
1793  pFanin = Dss_ObjFanin( p->vObjs, pObj, 1 );
1794  if ( !Dss_ObjCheckTransparent(p, pFanin) )
1795  return 0;
1796  pFanin = Dss_ObjFanin( p->vObjs, pObj, 2 );
1797  if ( !Dss_ObjCheckTransparent(p, pFanin) )
1798  return 0;
1799  return 1;
1800  }
1801  assert( pObj->Type == DAU_DSD_PRIME );
1802  return 0;
1803 }
1804 
1805 /**Function*************************************************************
1806 
1807  Synopsis []
1808 
1809  Description []
1810 
1811  SideEffects []
1812 
1813  SeeAlso []
1814 
1815 ***********************************************************************/
1816 void Dau_DsdTest__()
1817 {
1818  int nVars = 8;
1819 // char * pDsd = "[(ab)(cd)]";
1820  char * pDsd = "(!(a!(bh))[cde]!(fg))";
1821  Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL );
1822 // Dss_NtkPrint( pNtk );
1823 // Dss_NtkCheck( pNtk );
1824 // Dss_NtkTransform( pNtk );
1825 // Dss_NtkPrint( pNtk );
1826  Dss_NtkFree( pNtk );
1827  nVars = 0;
1828 }
1829 
1830 /**Function*************************************************************
1831 
1832  Synopsis []
1833 
1834  Description []
1835 
1836  SideEffects []
1837 
1838  SeeAlso []
1839 
1840 ***********************************************************************/
1841 void Dau_DsdTest()
1842 {
1843  int nVars = 8;
1844  Vec_Vec_t * vFuncs;
1845  Vec_Int_t * vOne, * vTwo, * vRes;//, * vThree;
1846  Dss_Man_t * p;
1847  int pEntries[3];
1848  int iLit, e0, e1;//, e2;
1849  int i, k, s;//, j;
1850 
1851  return;
1852 
1853  vFuncs = Vec_VecStart( nVars+1 );
1854  assert( nVars < DAU_MAX_VAR );
1855  p = Dss_ManAlloc( nVars, 0 );
1856 
1857  // init
1858  Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_VecVar(p->vObjs,0)) );
1859 
1860  // enumerate
1861  for ( s = 2; s <= nVars; s++ )
1862  {
1863  vRes = Vec_VecEntryInt( vFuncs, s );
1864  for ( i = 1; i < s; i++ )
1865  for ( k = i; k < s; k++ )
1866  if ( i + k == s )
1867  {
1868  vOne = Vec_VecEntryInt( vFuncs, i );
1869  vTwo = Vec_VecEntryInt( vFuncs, k );
1870  Vec_IntForEachEntry( vOne, pEntries[0], e0 )
1871  Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
1872  {
1873  int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
1874  int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
1875 
1876  iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1877  assert( !Abc_LitIsCompl(iLit) );
1878  Vec_IntPush( vRes, iLit );
1879 
1880  if ( fAddInv0 )
1881  {
1882  pEntries[0] = Abc_LitNot( pEntries[0] );
1883  iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1884  pEntries[0] = Abc_LitNot( pEntries[0] );
1885  assert( !Abc_LitIsCompl(iLit) );
1886  Vec_IntPush( vRes, iLit );
1887  }
1888 
1889  if ( fAddInv1 )
1890  {
1891  pEntries[1] = Abc_LitNot( pEntries[1] );
1892  iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1893  pEntries[1] = Abc_LitNot( pEntries[1] );
1894  assert( !Abc_LitIsCompl(iLit) );
1895  Vec_IntPush( vRes, iLit );
1896  }
1897 
1898  if ( fAddInv0 && fAddInv1 )
1899  {
1900  pEntries[0] = Abc_LitNot( pEntries[0] );
1901  pEntries[1] = Abc_LitNot( pEntries[1] );
1902  iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1903  pEntries[0] = Abc_LitNot( pEntries[0] );
1904  pEntries[1] = Abc_LitNot( pEntries[1] );
1905  assert( !Abc_LitIsCompl(iLit) );
1906  Vec_IntPush( vRes, iLit );
1907  }
1908 
1909  iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL );
1910  assert( !Abc_LitIsCompl(iLit) );
1911  Vec_IntPush( vRes, Abc_LitRegular(iLit) );
1912  }
1913  }
1914 /*
1915  for ( i = 1; i < s; i++ )
1916  for ( k = 1; k < s; k++ )
1917  for ( j = 1; j < s; j++ )
1918  if ( i + k + j == s )
1919  {
1920  vOne = Vec_VecEntryInt( vFuncs, i );
1921  vTwo = Vec_VecEntryInt( vFuncs, k );
1922  vThree = Vec_VecEntryInt( vFuncs, j );
1923  Vec_IntForEachEntry( vOne, pEntries[0], e0 )
1924  Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
1925  Vec_IntForEachEntry( vThree, pEntries[2], e2 )
1926  {
1927  int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
1928  int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
1929  int fAddInv2 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[2])) );
1930 
1931  if ( !fAddInv0 && k > j )
1932  continue;
1933 
1934  iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1935  assert( !Abc_LitIsCompl(iLit) );
1936  Vec_IntPush( vRes, iLit );
1937 
1938  if ( fAddInv1 )
1939  {
1940  pEntries[1] = Abc_LitNot( pEntries[1] );
1941  iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1942  pEntries[1] = Abc_LitNot( pEntries[1] );
1943  assert( !Abc_LitIsCompl(iLit) );
1944  Vec_IntPush( vRes, iLit );
1945  }
1946 
1947  if ( fAddInv2 )
1948  {
1949  pEntries[2] = Abc_LitNot( pEntries[2] );
1950  iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1951  pEntries[2] = Abc_LitNot( pEntries[2] );
1952  assert( !Abc_LitIsCompl(iLit) );
1953  Vec_IntPush( vRes, iLit );
1954  }
1955  }
1956  }
1957 */
1958  Vec_IntUniqify( vRes );
1959  }
1960  Dss_ManPrint( "_npn/npn/dsdcanon.txt", p );
1961 
1962  Dss_ManFree( p );
1963  Vec_VecFree( vFuncs );
1964 }
1965 
1966 
1967 /**Function*************************************************************
1968 
1969  Synopsis []
1970 
1971  Description []
1972 
1973  SideEffects []
1974 
1975  SeeAlso []
1976 
1977 ***********************************************************************/
1978 void Dau_DsdTest444()
1979 {
1980  Dss_Man_t * p = Dss_ManAlloc( 6, 0 );
1981  int iLit1[3] = { 2, 4 };
1982  int iLit2[3] = { 2, 4, 6 };
1983  int iRes[5];
1984  int nFans[2] = { 4, 3 };
1985  int pPermLits1[4] = { 0, 2, 5, 6 };
1986  int pPermLits2[5] = { 2, 9, 10 };
1987  int * pPermLits[2] = { pPermLits1, pPermLits2 };
1988  unsigned char pPermRes[6];
1989  int pPermResInt[6];
1990  unsigned uMaskShared = 2;
1991  int i;
1992 
1993  iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, NULL );
1994  iRes[1] = iRes[0];
1995  iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL );
1996  iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL );
1997 
1998  Dss_ManPrintOne( stdout, p, iRes[0], NULL );
1999  Dss_ManPrintOne( stdout, p, iRes[2], NULL );
2000  Dss_ManPrintOne( stdout, p, iRes[3], NULL );
2001 
2002  Dss_ManPrintOne( stdout, p, iRes[2], pPermLits1 );
2003  Dss_ManPrintOne( stdout, p, iRes[3], pPermLits2 );
2004 
2005  iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL );
2006 
2007  for ( i = 0; i < 6; i++ )
2008  pPermResInt[i] = pPermRes[i];
2009 
2010  Dss_ManPrintOne( stdout, p, iRes[4], NULL );
2011  Dss_ManPrintOne( stdout, p, iRes[4], pPermResInt );
2012 
2013  Dss_ManFree( p );
2014 }
2015 
2016 ////////////////////////////////////////////////////////////////////////
2017 /// END OF FILE ///
2018 ////////////////////////////////////////////////////////////////////////
2019 
2020 
2021 ABC_NAMESPACE_IMPL_END
2022 
Dss_VecForEachNode
#define Dss_VecForEachNode(vVec, pObj, i)
Definition: dauTree.c:131
Dss_NtkPrint_rec
void Dss_NtkPrint_rec(Dss_Ntk_t *p, Dss_Obj_t *pObj)
Definition: dauTree.c:478
memset
char * memset()
Dss_ManFree
void Dss_ManFree(Dss_Man_t *p)
Definition: dauTree.c:987
Dss_ManPrint
void Dss_ManPrint(char *pFileName, Dss_Man_t *p)
Definition: dauTree.c:1086
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Dss_EntWordNum
static int Dss_EntWordNum(Dss_Ent_t *p)
Definition: dauTree.c:105
Dss_NtkTransform
void Dss_NtkTransform(Dss_Ntk_t *p, int *pPermDsd)
Definition: dauTree.c:725
Dss_Lit2Obj
static Dss_Obj_t * Dss_Lit2Obj(Vec_Ptr_t *p, int iLit)
Definition: dauTree.c:123
Dss_ManBooleanAnd
Dss_Fun_t * Dss_ManBooleanAnd(Dss_Man_t *p, Dss_Ent_t *pEnt, int Counter)
Definition: dauTree.c:1433
Dss_Man_t_::vNexts
Vec_Int_t * vNexts
Definition: dauTree.c:84
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Dss_FunWordNum
static int Dss_FunWordNum(Dss_Fun_t *p)
Definition: dauTree.c:106
Dss_VecVar
static Dss_Obj_t * Dss_VecVar(Vec_Ptr_t *p, int v)
Definition: dauTree.c:119
Dss_Ntk_t_::nVars
int nVars
Definition: dauTree.c:68
Abc_Lit2LitV
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
Dss_Man_t_::vLeaves
Vec_Int_t * vLeaves
Definition: dauTree.c:85
Dss_Man_t_::pTtElems
word ** pTtElems
Definition: dauTree.c:87
Dss_ManComputeTruth
word * Dss_ManComputeTruth(Dss_Man_t *p, int iDsd, int nVars, int *pPermLits)
Definition: dauTree.c:1192
Dss_Ent_t
struct Dss_Ent_t_ Dss_Ent_t
Definition: dauTree.c:39
Dss_Man_t_::timeLook
abctime timeLook
Definition: dauTree.c:96
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Dss_ManCacheProfile
void Dss_ManCacheProfile(Dss_Man_t *p)
Definition: dauTree.c:913
Dss_IsComplement
static int Dss_IsComplement(Dss_Obj_t *p)
Definition: dauTree.c:103
Dss_ManCheckNonDec_rec
int Dss_ManCheckNonDec_rec(Dss_Man_t *p, Dss_Obj_t *pObj)
Definition: dauTree.c:1040
Dss_Fun_t_::nFans
unsigned nFans
Definition: dauTree.c:35
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
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Dss_Man_t_::nVars
int nVars
Definition: dauTree.c:78
Dss_Ent_t_::iDsd1
unsigned iDsd1
Definition: dauTree.c:46
Dss_ObjAlloc
Dss_Obj_t * Dss_ObjAlloc(Dss_Man_t *p, int Type, int nFans, int nTruthVars)
Definition: dauTree.c:760
Dss_Man_t_::nCache
int nCache
Definition: dauTree.c:89
Dau_DsdReadVar
static int Dau_DsdReadVar(char *p)
Definition: dau.h:71
Dss_ObjFanin
static Dss_Obj_t * Dss_ObjFanin(Vec_Ptr_t *p, Dss_Obj_t *pObj, int i)
Definition: dauTree.c:124
Abc_TtPrintHexRev
static void Abc_TtPrintHexRev(FILE *pFile, word *pTruth, int nVars)
Definition: utilTruth.h:789
Dss_Man_t_::vObjs
Vec_Ptr_t * vObjs
Definition: dauTree.c:83
Dss_Ent_t_::nShared
unsigned nShared
Definition: dauTree.c:47
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Dss_ManSharedMapDerive
Dss_Ent_t * Dss_ManSharedMapDerive(Dss_Man_t *p, int iDsd0, int iDsd1, Vec_Str_t *vShared)
Definition: dauTree.c:1681
Dss_Ntk_t_::vObjs
Vec_Ptr_t * vObjs
Definition: dauTree.c:73
Dss_Fun_t_::iDsd
unsigned iDsd
Definition: dauTree.c:34
Dau_DsdTest444
void Dau_DsdTest444()
Definition: dauTree.c:1978
memcpy
char * memcpy()
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition: dauDsd.c:1912
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Dss_ObjFindOrAdd
Dss_Obj_t * Dss_ObjFindOrAdd(Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
Definition: dauTree.c:868
Dss_Ent_t_::pFunc
Dss_Fun_t * pFunc
Definition: dauTree.c:42
Mem_Flex_t_
Definition: mem.c:55
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Dss_ObjCheckTransparent
int Dss_ObjCheckTransparent(Dss_Man_t *p, Dss_Obj_t *pObj)
Definition: dauTree.c:1776
Dss_Man_t_::nCacheEntries
int nCacheEntries[2]
Definition: dauTree.c:93
If_CluCheck3
If_Grp_t If_CluCheck3(If_Man_t *p, word *pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, If_Grp_t *pR, If_Grp_t *pG2, word *pFunc0, word *pFunc1, word *pFunc2)
Definition: ifDec16.c:1909
Dss_ManCacheAlloc
void Dss_ManCacheAlloc(Dss_Man_t *p)
Definition: dauTree.c:890
Dss_ObjId
static int Dss_ObjId(Dss_Obj_t *pObj)
Definition: dauTree.c:111
Dau_DsdIsConst
static int Dau_DsdIsConst(char *p)
MACRO DEFINITIONS ///.
Definition: dau.h:67
Dss_ObjWordNum
static int Dss_ObjWordNum(int nFans)
Definition: dauTree.c:107
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Dss_Man_t_::timeEnd
abctime timeEnd
Definition: dauTree.c:97
Dss_ManComputeTruth_rec
void Dss_ManComputeTruth_rec(Dss_Man_t *p, Dss_Obj_t *pObj, int nVars, word *pRes, int *pPermLits, int *pnSupp)
Definition: dauTree.c:1139
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Dss_ManPrintOne
void Dss_ManPrintOne(FILE *pFile, Dss_Man_t *p, int iDsdLit, int *pPermLits)
Definition: dauTree.c:1030
Dss_Ntk_t_
Definition: dauTree.c:66
Dss_Obj_t_::Type
unsigned Type
Definition: dauTree.c:55
nWords
int nWords
Definition: abcNpn.c:127
Dss_Man_t_::pMem
Mem_Flex_t * pMem
Definition: dauTree.c:82
Abc_TtConst1
static void Abc_TtConst1(word *pIn1, int nWords)
Definition: utilTruth.h:315
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Dss_ObjHashLookup
unsigned * Dss_ObjHashLookup(Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
Definition: dauTree.c:853
for
for(p=first;p->value< newval;p=p->next)
Dss_Ntk_t_::pRoot
Dss_Obj_t * pRoot
Definition: dauTree.c:72
Abc_TtByteNum
static int Abc_TtByteNum(int nVars)
Definition: utilTruth.h:170
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Mem_FlexEntryFetch
char * Mem_FlexEntryFetch(Mem_Flex_t *p, int nBytes)
Definition: mem.c:372
Dss_Man_t_::timeDec
abctime timeDec
Definition: dauTree.c:95
Dss_Obj_t
struct Dss_Obj_t_ Dss_Obj_t
Definition: dauTree.c:51
Dss_Obj_t_::nSupp
unsigned nSupp
Definition: dauTree.c:56
Dss_VecConst0
static Dss_Obj_t * Dss_VecConst0(Vec_Ptr_t *p)
Definition: dauTree.c:118
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Dss_Obj_t_::pFans
unsigned pFans[0]
Definition: dauTree.c:62
Dss_Lit2Lit
static int Dss_Lit2Lit(int *pMapLit, int Lit)
Definition: dauTree.c:148
Mem_FlexStart
Mem_Flex_t * Mem_FlexStart()
Definition: mem.c:311
DAU_MAX_STR
#define DAU_MAX_STR
Definition: dau.h:43
Dss_ManSharedMap
Dss_Ent_t * Dss_ManSharedMap(Dss_Man_t *p, int *iDsd, int *nFans, int **pFans, unsigned uSharedMask)
Definition: dauTree.c:1510
Dss_Ent_t_::pShared
unsigned char pShared[0]
Definition: dauTree.c:48
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Dss_ObjClean
static void Dss_ObjClean(Dss_Obj_t *pObj)
Definition: dauTree.c:110
Dss_ObjCreateNtk
Dss_Obj_t * Dss_ObjCreateNtk(Dss_Ntk_t *p, int Type, Vec_Int_t *vFaninLits)
Definition: dauTree.c:440
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Vec_VecPushInt
static void Vec_VecPushInt(Vec_Vec_t *p, int Level, int Entry)
Definition: vecVec.h:468
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Dss_Regular
static Dss_Obj_t * Dss_Regular(Dss_Obj_t *p)
Definition: dauTree.c:100
DAU_MAX_VAR
#define DAU_MAX_VAR
INCLUDES ///.
Definition: dau.h:42
If_Grp_t_::nMyu
char nMyu
Definition: ifDec16.c:41
Dss_ManHashProfile
void Dss_ManHashProfile(Dss_Man_t *p)
Definition: dauTree.c:821
Dss_ObjFaninC
static int Dss_ObjFaninC(Dss_Obj_t *pObj, int i)
Definition: dauTree.c:115
Dss_NtkRebuild_rec
int Dss_NtkRebuild_rec(Dss_Man_t *p, Dss_Ntk_t *pNtk, Dss_Obj_t *pObj)
Definition: dauTree.c:1227
Dss_Ent_t_::iDsd0
unsigned iDsd0
Definition: dauTree.c:44
Dss_Obj_t_::iVar
unsigned iVar
Definition: dauTree.c:57
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Dss_ObjAllocNtk
Dss_Obj_t * Dss_ObjAllocNtk(Dss_Ntk_t *p, int Type, int nFans, int nTruthVars)
Definition: dauTree.c:425
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Dss_ObjTruth
static word * Dss_ObjTruth(Dss_Obj_t *pObj)
Definition: dauTree.c:108
Dss_ManCacheLookup
Dss_Ent_t ** Dss_ManCacheLookup(Dss_Man_t *p, Dss_Ent_t *pEnt)
Definition: dauTree.c:927
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
CLU_VAR_MAX
#define CLU_VAR_MAX
DECLARATIONS ///.
Definition: ifDec16.c:31
Dau_DsdTest__
void Dau_DsdTest__()
Definition: dauTree.c:1816
Dss_Man_t_::pCache
Dss_Ent_t ** pCache
Definition: dauTree.c:88
if
if(last==0)
Definition: sparse_int.h:34
Abc_TtStretch6
static void Abc_TtStretch6(word *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:693
memcmp
int memcmp()
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Dau_DsdTruthCompose_rec
void Dau_DsdTruthCompose_rec(word *pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word *pRes, int nVars, int nWordsR)
Definition: dauDsd.c:501
Dss_Man_t_
Definition: dauTree.c:76
Dss_ManPrint_rec
void Dss_ManPrint_rec(FILE *pFile, Dss_Man_t *p, Dss_Obj_t *pObj, int *pPermLits, int *pnSupp)
Definition: dauTree.c:1005
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Dau_DsdMergeMatches
static void Dau_DsdMergeMatches(char *pDsd, int *pMatches)
Definition: dauTree.c:523
Counter
static int Counter
Definition: extraBddMisc.c:1877
Dss_Obj_t_::fMark1
unsigned fMark1
Definition: dauTree.c:60
Dss_ObjCreate
Dss_Obj_t * Dss_ObjCreate(Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
Definition: dauTree.c:774
Dss_Man_t_::nBins
int nBins
Definition: dauTree.c:80
Vec_VecStart
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
Dss_Man_t_::nNonDecLimit
int nNonDecLimit
Definition: dauTree.c:79
Dss_Man_t_::vCopies
Vec_Int_t * vCopies
Definition: dauTree.c:86
Dss_ManCacheCreate
Dss_Ent_t * Dss_ManCacheCreate(Dss_Man_t *p, Dss_Ent_t *pEnt0, Dss_Fun_t *pFun0)
Definition: dauTree.c:944
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Mpm_FuncCompute
int Mpm_FuncCompute(Dss_Man_t *p, int iDsd0, int iDsd1, Vec_Str_t *vShared, int *pPerm, int *pnLeaves)
Definition: dauTree.c:1693
Dss_Fun_t
typedefABC_NAMESPACE_IMPL_START struct Dss_Fun_t_ Dss_Fun_t
DECLARATIONS ///.
Definition: dauTree.c:31
Dss_ObjSort
void Dss_ObjSort(Vec_Ptr_t *p, Dss_Obj_t **pNodes, int nNodes, int *pPerm)
Definition: dauTree.c:664
Dss_Not
static Dss_Obj_t * Dss_Not(Dss_Obj_t *p)
Definition: dauTree.c:101
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Dss_Ntk_t_::nMemAlloc
int nMemAlloc
Definition: dauTree.c:70
Dss_ObjForEachFanin
#define Dss_ObjForEachFanin(vVec, pObj, pFanin, i)
Definition: dauTree.c:134
Vec_PtrCap
static int Vec_PtrCap(Vec_Ptr_t *p)
Definition: vecPtr.h:311
Dss_NtkCheck
void Dss_NtkCheck(Dss_Ntk_t *p)
Definition: dauTree.c:692
Dss_ManTtElems
static word ** Dss_ManTtElems()
FUNCTION DEFINITIONS ///.
Definition: dauTree.c:401
Dss_ObjChild
static Dss_Obj_t * Dss_ObjChild(Vec_Ptr_t *p, Dss_Obj_t *pObj, int i)
Definition: dauTree.c:125
Dss_Obj_t_::nWords
unsigned nWords
Definition: dauTree.c:58
Mem_FlexStop
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition: mem.c:343
Vec_VecEntryInt
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
Dss_VecLitSuppSize
static int Dss_VecLitSuppSize(Vec_Ptr_t *p, int iLit)
Definition: dauTree.c:120
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Dss_Ent_t_
Definition: dauTree.c:40
Dss_Man_t_::nCacheHits
int nCacheHits[2]
Definition: dauTree.c:91
Dss_ManCacheHashKey
static unsigned Dss_ManCacheHashKey(Dss_Man_t *p, Dss_Ent_t *pEnt)
Definition: dauTree.c:904
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition: dau.h:44
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Dss_Ntk_t_::pMem
word * pMem
Definition: dauTree.c:71
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
If_Grp_t_::pVars
char pVars[CLU_VAR_MAX]
Definition: ifDec16.c:42
Dss_Obj_t_::fMark0
unsigned fMark0
Definition: dauTree.c:59
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Dss_ObjCompare
int Dss_ObjCompare(Vec_Ptr_t *p, Dss_Obj_t *p0i, Dss_Obj_t *p1i)
Definition: dauTree.c:634
Dss_WordCountOnes
static int Dss_WordCountOnes(unsigned uWord)
Definition: dauTree.c:139
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Dss_NotCond
static Dss_Obj_t * Dss_NotCond(Dss_Obj_t *p, int c)
Definition: dauTree.c:102
Dss_NtkCreate
Dss_Ntk_t * Dss_NtkCreate(char *pDsd, int nVars, word *pTruth)
Definition: dauTree.c:601
Vec_Str_t_
Definition: bblif.c:47
Dss_ObjSuppSize
static int Dss_ObjSuppSize(Dss_Obj_t *pObj)
Definition: dauTree.c:113
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_TtMux
static void Abc_TtMux(word *pOut, word *pCtrl, word *pIn1, word *pIn0, int nWords)
Definition: utilTruth.h:263
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
Abc_TtConst0
static void Abc_TtConst0(word *pIn1, int nWords)
Definition: utilTruth.h:309
Mem_FlexReadMemUsage
int Mem_FlexReadMemUsage(Mem_Flex_t *p)
Definition: mem.c:445
Dss_Ntk_t_::nMem
int nMem
Definition: dauTree.c:69
Dss_ManOperationFun
Dss_Fun_t * Dss_ManOperationFun(Dss_Man_t *p, int *iDsd, int nFansTot)
Definition: dauTree.c:1389
Dss_ObjFaninNum
static int Dss_ObjFaninNum(Dss_Obj_t *pObj)
Definition: dauTree.c:114
Dss_ObjHashKey
static unsigned Dss_ObjHashKey(Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
Definition: dauTree.c:836
Dss_ManAlloc
Dss_Man_t * Dss_ManAlloc(int nVars, int nNonDecLimit)
Definition: dauTree.c:967
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Dss_ObjForEachChild
#define Dss_ObjForEachChild(vVec, pObj, pFanin, i)
Definition: dauTree.c:136
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition: dauCanon.c:895
If_Grp_t_::nVars
char nVars
Definition: ifDec16.c:40
Dss_ManCacheFree
void Dss_ManCacheFree(Dss_Man_t *p)
Definition: dauTree.c:896
Vec_PtrFreeP
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
Dau_DsdTest
void Dau_DsdTest()
Definition: dauTree.c:1841
Dss_NtkCreate_rec
int Dss_NtkCreate_rec(char *pStr, char **p, int *pMatches, Dss_Ntk_t *pNtk, word *pTruth)
Definition: dauTree.c:538
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
Dss_Man_t_::timeBeg
abctime timeBeg
Definition: dauTree.c:94
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
Dss_Ent_t_::nWords
unsigned nWords
Definition: dauTree.c:45
If_Grp_t_
Definition: ifDec16.c:38
Dau_DsdIsVar
static int Dau_DsdIsVar(char *p)
Definition: dau.h:70
Dss_Obj2Lit
static int Dss_Obj2Lit(Dss_Obj_t *pObj)
Definition: dauTree.c:122
Dss_Fun_t_
Definition: dauTree.c:32
Dss_EntPrint
void Dss_EntPrint(Dss_Ent_t *p, Dss_Fun_t *pFun)
Definition: dauTree.c:1411
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
Dss_Obj_t_
Definition: dauTree.c:52
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Dss_NtkFree
void Dss_NtkFree(Dss_Ntk_t *p)
Definition: dauTree.c:472
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Dss_Man_t_::nCacheMisses
int nCacheMisses[2]
Definition: dauTree.c:92
Dss_NtkRebuild
int Dss_NtkRebuild(Dss_Man_t *p, Dss_Ntk_t *pNtk)
Definition: dauTree.c:1264
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Dss_VecForEachObj
#define Dss_VecForEachObj(vVec, pObj, i)
Definition: dauTree.c:127
Dss_NtkAlloc
Dss_Ntk_t * Dss_NtkAlloc(int nVars)
Definition: dauTree.c:453
Dss_ManOperation
int Dss_ManOperation(Dss_Man_t *p, int Type, int *pLits, int nLits, unsigned char *pPerm, word *pTruth)
Definition: dauTree.c:1287
Dss_ManMerge
int Dss_ManMerge(Dss_Man_t *p, int *iDsd, int *nFans, int **pFans, unsigned uSharedMask, int nKLutSize, unsigned char *pPermRes, word *pTruth)
Definition: dauTree.c:1539
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Dss_Man_t_::pBins
unsigned * pBins
Definition: dauTree.c:81
Dss_Man_t_::pMemEnts
Mem_Flex_t * pMemEnts
Definition: dauTree.c:90
Dss_NtkPrint
void Dss_NtkPrint(Dss_Ntk_t *p)
Definition: dauTree.c:497
Abc_TtElemInit
static void Abc_TtElemInit(word **pTtElems, int nVars)
Definition: utilTruth.h:333
Dss_ObjType
static int Dss_ObjType(Dss_Obj_t *pObj)
Definition: dauTree.c:112
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
Dss_Obj_t_::nFans
unsigned nFans
Definition: dauTree.c:61
Dss_VecForEachObjVec
#define Dss_VecForEachObjVec(vLits, vVec, pObj, i)
Definition: dauTree.c:129
Dss_Ent_t_::pNext
Dss_Ent_t * pNext
Definition: dauTree.c:43
Dss_Obj_t_::Id
unsigned Id
Definition: dauTree.c:54
Dss_VecObj
static Dss_Obj_t * Dss_VecObj(Vec_Ptr_t *p, int Id)
Definition: dauTree.c:117
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Dss_ManDump
void Dss_ManDump(Dss_Man_t *p)
Definition: dauTree.c:1056
Dss_NtkCollectPerm_rec
int Dss_NtkCollectPerm_rec(Dss_Ntk_t *p, Dss_Obj_t *pObj, int *pPermDsd, int *pnPerms)
Definition: dauTree.c:709
Dss_Fun_t_::pFans
unsigned char pFans[0]
Definition: dauTree.c:36