abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ifDsd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ifDsd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [FPGA mapping based on priority cuts.]
8 
9  Synopsis [Computation of DSD representation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 21, 2006.]
16 
17  Revision [$Id: ifTruth.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <math.h>
22 #include "if.h"
23 #include "ifCount.h"
24 #include "misc/extra/extra.h"
25 #include "sat/bsat/satSolver.h"
26 #include "aig/gia/gia.h"
27 #include "bool/kit/kit.h"
28 
29 #ifdef ABC_USE_PTHREADS
30 
31 #ifdef _WIN32
32 #include "../lib/pthread.h"
33 #else
34 #include <pthread.h>
35 #include <unistd.h>
36 #endif
37 
38 #endif
39 
40 ABC_NAMESPACE_IMPL_START
41 
42 
43 ////////////////////////////////////////////////////////////////////////
44 /// DECLARATIONS ///
45 ////////////////////////////////////////////////////////////////////////
46 
47 // network types
48 typedef enum {
49  IF_DSD_NONE = 0, // 0: unknown
50  IF_DSD_CONST0, // 1: constant
51  IF_DSD_VAR, // 2: variable
52  IF_DSD_AND, // 3: AND
53  IF_DSD_XOR, // 4: XOR
54  IF_DSD_MUX, // 5: MUX
55  IF_DSD_PRIME // 6: PRIME
56 } If_DsdType_t;
57 
58 typedef struct If_DsdObj_t_ If_DsdObj_t;
59 struct If_DsdObj_t_
60 {
61  unsigned Id; // node ID
62  unsigned Type : 3; // node type
63  unsigned nSupp : 5; // variable
64  unsigned fMark : 1; // user mark
65  unsigned Count : 18; // variable
66  unsigned nFans : 5; // fanin count
67  unsigned pFans[0]; // fanins
68 };
69 
70 struct If_DsdMan_t_
71 {
72  char * pStore; // input/output file
73  int nVars; // max var number
74  int LutSize; // LUT size
75  int nWords; // word number
76  int nBins; // table size
77  unsigned * pBins; // hash table
78  Mem_Flex_t * pMem; // memory for nodes
79  Vec_Ptr_t vObjs; // objects
80  Vec_Int_t vNexts; // next pointers
81  Vec_Int_t vTruths; // truth IDs of prime nodes
82  Vec_Int_t * vTemp1; // temp
83  Vec_Int_t * vTemp2; // temp
84  word ** pTtElems; // elementary TTs
85  Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
86  Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
87  Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function
88  int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules
89  Vec_Wrd_t * vPerms; // permutations
90  Gia_Man_t * pTtGia; // GIA to represent truth tables
91  Vec_Int_t * vCover; // temporary memory
92  void * pSat; // SAT solver
93  char * pCellStr; // symbolic cell description
94  int nObjsPrev; // previous number of objects
95  int fNewAsUseless; // set new as useless
96  int nUniqueHits; // statistics
97  int nUniqueMisses; // statistics
98  abctime timeDsd; // statistics
99  abctime timeCanon; // statistics
100  abctime timeCheck; // statistics
101  abctime timeCheck2; // statistics
102  abctime timeVerify; // statistics
103 };
104 
105 static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
106 static inline int If_DsdObjTruthId( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return (pObj->Type == IF_DSD_PRIME && pObj->nFans > 2) ? Vec_IntEntry(&p->vTruths, pObj->Id) : -1; }
107 static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem[pObj->nFans], If_DsdObjTruthId(p, pObj)); }
108 static inline void If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); Vec_IntWriteEntry(&p->vTruths, pObj->Id, Id); }
109 
110 static inline void If_DsdObjClean( If_DsdObj_t * pObj ) { memset( pObj, 0, sizeof(If_DsdObj_t) ); }
111 static inline int If_DsdObjId( If_DsdObj_t * pObj ) { return pObj->Id; }
112 static inline int If_DsdObjType( If_DsdObj_t * pObj ) { return pObj->Type; }
113 static inline int If_DsdObjIsVar( If_DsdObj_t * pObj ) { return (int)(pObj->Type == IF_DSD_VAR); }
114 static inline int If_DsdObjSuppSize( If_DsdObj_t * pObj ) { return pObj->nSupp; }
115 static inline int If_DsdObjFaninNum( If_DsdObj_t * pObj ) { return pObj->nFans; }
116 static inline int If_DsdObjFaninC( If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); }
117 static inline int If_DsdObjFaninLit( If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return pObj->pFans[i]; }
118 
119 static inline If_DsdObj_t * If_DsdVecObj( Vec_Ptr_t * p, int Id ) { return (If_DsdObj_t *)Vec_PtrEntry(p, Id); }
120 static inline If_DsdObj_t * If_DsdVecConst0( Vec_Ptr_t * p ) { return If_DsdVecObj( p, 0 ); }
121 static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v ) { return If_DsdVecObj( p, v+1 ); }
122 static inline int If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->nSupp; }
123 static inline int If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) ); }
124 static inline int If_DsdVecObjRef( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->Count; }
125 static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x3FFFF ) If_DsdVecObj( p, iObj )->Count++; }
126 static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
127 static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; }
128 static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; }
129 static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 0; }
130 
131 #define If_DsdVecForEachObj( vVec, pObj, i ) \
132  Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
133 #define If_DsdVecForEachObjStart( vVec, pObj, i, Start ) \
134  Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, Start )
135 #define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \
136  for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ )
137 #define If_DsdVecForEachNode( vVec, pObj, i ) \
138  Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, 2 )
139 #define If_DsdObjForEachFanin( vVec, pObj, pFanin, i ) \
140  for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((pFanin) = If_DsdObjFanin(vVec, pObj, i)); i++ )
141 #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \
142  for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ )
143 
144 extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
145 
146 ////////////////////////////////////////////////////////////////////////
147 /// FUNCTION DEFINITIONS ///
148 ////////////////////////////////////////////////////////////////////////
149 
150 /**Function*************************************************************
151 
152  Synopsis []
153 
154  Description []
155 
156  SideEffects []
157 
158  SeeAlso []
159 
160 ***********************************************************************/
161 char * If_DsdManFileName( If_DsdMan_t * p )
162 {
163  return p->pStore;
164 }
165 int If_DsdManVarNum( If_DsdMan_t * p )
166 {
167  return p->nVars;
168 }
169 int If_DsdManObjNum( If_DsdMan_t * p )
170 {
171  return Vec_PtrSize( &p->vObjs );
172 }
173 int If_DsdManLutSize( If_DsdMan_t * p )
174 {
175  return p->LutSize;
176 }
177 void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize )
178 {
179  p->LutSize = nLutSize;
180 }
181 int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd )
182 {
183  return If_DsdVecLitSuppSize( &p->vObjs, iDsd );
184 }
185 int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
186 {
187  return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
188 }
189 int If_DsdManReadMark( If_DsdMan_t * p, int iDsd )
190 {
191  return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
192 }
193 void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
194 {
195  if ( p->nObjsPrev == 0 )
196  p->nObjsPrev = If_DsdManObjNum(p);
197  p->fNewAsUseless = 1;
198 }
199 word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd )
200 {
201  return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0;
202 }
203 char * If_DsdManGetCellStr( If_DsdMan_t * p )
204 {
205  return p->pCellStr;
206 }
207 
208 /**Function*************************************************************
209 
210  Synopsis [DSD manager.]
211 
212  Description []
213 
214  SideEffects []
215 
216  SeeAlso []
217 
218 ***********************************************************************/
219 static inline word ** If_ManDsdTtElems()
220 {
221  static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
222  if ( pTtElems[0] == NULL )
223  {
224  int v;
225  for ( v = 0; v <= DAU_MAX_VAR; v++ )
226  pTtElems[v] = TtElems[v];
227  Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
228  }
229  return pTtElems;
230 }
231 If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
232 {
233  int nWords = If_DsdObjWordNum( nFans );
234  If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
235  If_DsdObjClean( pObj );
236  pObj->Type = Type;
237  pObj->nFans = nFans;
238  pObj->Id = Vec_PtrSize( &p->vObjs );
239  pObj->fMark = p->fNewAsUseless;
240  pObj->Count = 0;
241  Vec_PtrPush( &p->vObjs, pObj );
242  Vec_IntPush( &p->vNexts, 0 );
243  Vec_IntPush( &p->vTruths, -1 );
244  assert( Vec_IntSize(&p->vNexts) == Vec_PtrSize(&p->vObjs) );
245  assert( Vec_IntSize(&p->vTruths) == Vec_PtrSize(&p->vObjs) );
246  return pObj;
247 }
248 If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
249 {
250  If_DsdMan_t * p; int v;
251  char pFileName[10];
252  assert( nVars <= DAU_MAX_VAR );
253  sprintf( pFileName, "%02d.dsd", nVars );
254  p = ABC_CALLOC( If_DsdMan_t, 1 );
255  p->pStore = Abc_UtilStrsav( pFileName );
256  p->nVars = nVars;
257  p->LutSize = LutSize;
258  p->nWords = Abc_TtWordNum( nVars );
259  p->nBins = Abc_PrimeCudd( 100000 );
260  p->pBins = ABC_CALLOC( unsigned, p->nBins );
261  p->pMem = Mem_FlexStart();
262  Vec_PtrGrow( &p->vObjs, 10000 );
263  Vec_IntGrow( &p->vNexts, 10000 );
264  Vec_IntGrow( &p->vTruths, 10000 );
265  If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
266  If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
267  p->vTemp1 = Vec_IntAlloc( 32 );
268  p->vTemp2 = Vec_IntAlloc( 32 );
269  p->pTtElems = If_ManDsdTtElems();
270  for ( v = 3; v <= nVars; v++ )
271  {
272  p->vTtMem[v] = Vec_MemAlloc( Abc_TtWordNum(v), 12 );
273  Vec_MemHashAlloc( p->vTtMem[v], 10000 );
274  p->vTtDecs[v] = Vec_PtrAlloc( 1000 );
275  }
276 /*
277  p->pTtGia = Gia_ManStart( nVars );
278  Gia_ManHashAlloc( p->pTtGia );
279  for ( v = 0; v < nVars; v++ )
280  Gia_ManAppendCi( p->pTtGia );
281 */
282  for ( v = 2; v < nVars; v++ )
283  p->pSched[v] = Extra_GreyCodeSchedule( v );
284  if ( LutSize )
285  p->pSat = If_ManSatBuildXY( LutSize );
286  p->vCover = Vec_IntAlloc( 0 );
287  return p;
288 }
289 void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize )
290 {
291  Vec_Int_t * vLevel;
292  int v, i, fCompl;
293  word * pTruth;
294  if ( p->vIsops[3] != NULL )
295  return;
296  if ( Vec_PtrSize(&p->vObjs) > 2 )
297  printf( "Warning: DSD manager is already started without ISOPs.\n" );
298  for ( v = 3; v <= nLutSize; v++ )
299  {
300  p->vIsops[v] = Vec_WecAlloc( 100 );
301  Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
302  {
303  vLevel = Vec_WecPushLevel( p->vIsops[v] );
304  fCompl = Kit_TruthIsop( (unsigned *)pTruth, v, p->vCover, 1 );
305  if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
306  {
307  Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
308  Vec_IntAppend( vLevel, p->vCover );
309  if ( fCompl )
310  vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
311  }
312  }
313  assert( Vec_WecSize(p->vIsops[v]) == Vec_MemEntryNum(p->vTtMem[v]) );
314  }
315 }
316 void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
317 {
318  int v;
319 // If_DsdManDumpDsd( p );
320  if ( fVerbose )
321  If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 );
322  if ( fVerbose )
323  {
324  char FileName[10];
325  for ( v = 3; v <= p->nVars; v++ )
326  {
327  sprintf( FileName, "dumpdsd%02d", v );
328  Vec_MemDumpTruthTables( p->vTtMem[v], FileName, v );
329  }
330  }
331  for ( v = 2; v < p->nVars; v++ )
332  ABC_FREE( p->pSched[v] );
333  for ( v = 3; v <= p->nVars; v++ )
334  {
335  Vec_MemHashFree( p->vTtMem[v] );
336  Vec_MemFree( p->vTtMem[v] );
337  Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) );
338  if ( p->vIsops[v] )
339  Vec_WecFree( p->vIsops[v] );
340  }
341  Vec_WrdFreeP( &p->vPerms );
342  Vec_IntFreeP( &p->vTemp1 );
343  Vec_IntFreeP( &p->vTemp2 );
344  ABC_FREE( p->vObjs.pArray );
345  ABC_FREE( p->vNexts.pArray );
346  ABC_FREE( p->vTruths.pArray );
347  Mem_FlexStop( p->pMem, 0 );
348  Gia_ManStopP( &p->pTtGia );
349  Vec_IntFreeP( &p->vCover );
350  If_ManSatUnbuild( p->pSat );
351  ABC_FREE( p->pCellStr );
352  ABC_FREE( p->pStore );
353  ABC_FREE( p->pBins );
354  ABC_FREE( p );
355 }
356 void If_DsdManDumpDsd( If_DsdMan_t * p, int Support )
357 {
358  char * pFileName = "tts_nondsd.txt";
359  If_DsdObj_t * pObj;
360  Vec_Int_t * vMap;
361  FILE * pFile = fopen( pFileName, "wb" );
362  int v, i;
363  if ( pFile == NULL )
364  {
365  printf( "Cannot open file \"%s\".\n", pFileName );
366  return;
367  }
368  for ( v = 3; v <= p->nVars; v++ )
369  {
370  vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem[v]) );
371  If_DsdVecForEachObj( &p->vObjs, pObj, i )
372  {
373  if ( Support && Support != If_DsdObjSuppSize(pObj) )
374  continue;
375  if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
376  continue;
377  if ( Vec_IntEntry(vMap, If_DsdObjTruthId(p, pObj)) )
378  continue;
379  Vec_IntWriteEntry(vMap, If_DsdObjTruthId(p, pObj), 1);
380  fprintf( pFile, "0x" );
381  Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : v );
382  fprintf( pFile, "\n" );
383  //printf( " " );
384  //Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
385  }
386  Vec_IntFree( vMap );
387  }
388  fclose( pFile );
389 }
390 void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
391 {
392  extern word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits );
393  char * pFileName = "tts_all.txt";
394  If_DsdObj_t * pObj;
395  word * pRes; int i;
396  FILE * pFile = fopen( pFileName, "wb" );
397  if ( pFile == NULL )
398  {
399  printf( "Cannot open file \"%s\".\n", pFileName );
400  return;
401  }
402  If_DsdVecForEachObj( &p->vObjs, pObj, i )
403  {
404  if ( Support && Support != If_DsdObjSuppSize(pObj) )
405  continue;
406  pRes = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
407  fprintf( pFile, "0x" );
408  Abc_TtPrintHexRev( pFile, pRes, Support ? Abc_MaxInt(Support, 6) : p->nVars );
409  fprintf( pFile, "\n" );
410 // printf( " " );
411 // Dau_DsdPrintFromTruth( pRes, p->nVars );
412  }
413  fclose( pFile );
414 }
415 int If_DsdManHasMarks( If_DsdMan_t * p )
416 {
417  If_DsdObj_t * pObj;
418  int i;
419  If_DsdVecForEachObj( &p->vObjs, pObj, i )
420  if ( pObj->fMark )
421  return 1;
422  return 0;
423 }
424 
425 /**Function*************************************************************
426 
427  Synopsis [Printing.]
428 
429  Description []
430 
431  SideEffects []
432 
433  SeeAlso []
434 
435 ***********************************************************************/
436 void If_DsdManHashProfile( If_DsdMan_t * p )
437 {
438  If_DsdObj_t * pObj;
439  unsigned * pSpot;
440  int i, Counter;
441  for ( i = 0; i < p->nBins; i++ )
442  {
443  Counter = 0;
444  for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(&p->vNexts, pObj->Id), Counter++ )
445  pObj = If_DsdVecObj( &p->vObjs, *pSpot );
446 // if ( Counter > 5 )
447 // printf( "%d ", Counter );
448 // if ( i > 10000 )
449 // break;
450  }
451 // printf( "\n" );
452 }
453 int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id )
454 {
455  If_DsdObj_t * pObj;
456  int i, iFanin;
457  pObj = If_DsdVecObj( &p->vObjs, Id );
458  if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
459  return 0;
460  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
461  return 0;
462  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
463  return 1;
464  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
465  if ( If_DsdManCheckNonDec_rec( p, Abc_Lit2Var(iFanin) ) )
466  return 1;
467  return 0;
468 }
469 void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned char * pPermLits, int * pnSupp )
470 {
471  char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
472  char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
473  If_DsdObj_t * pObj;
474  int i, iFanin;
475  fprintf( pFile, "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" );
476  pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsdLit) );
477  if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
478  { fprintf( pFile, "0" ); return; }
479  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
480  {
481  int iPermLit = pPermLits ? (int)pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
482  fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
483  return;
484  }
485  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
486  Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), If_DsdObjFaninNum(pObj) );
487  fprintf( pFile, "%c", OpenType[If_DsdObjType(pObj)] );
488  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
489  If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp );
490  fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] );
491 }
492 void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits, int fNewLine )
493 {
494  int nSupp = 0;
495  fprintf( pFile, "%6d : ", iObjId );
496  fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(&p->vObjs, iObjId) );
497  fprintf( pFile, "%8d ", If_DsdVecObjRef(&p->vObjs, iObjId) );
498  fprintf( pFile, "%d ", If_DsdVecObjMark(&p->vObjs, iObjId) );
499  If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
500  if ( fNewLine )
501  fprintf( pFile, "\n" );
502  assert( nSupp == If_DsdVecObjSuppSize(&p->vObjs, iObjId) );
503 }
504 #define DSD_ARRAY_LIMIT 16
505 void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p )
506 {
507  Vec_Int_t * vDecs;
508  int i, k, v, nSuppSize, nDecMax = 0;
509  int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0};
510  int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0};
511  int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0};
512  int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}};
513  word * pTruth;
514  for ( v = 3; v <= p->nVars; v++ )
515  {
516  assert( Vec_MemEntryNum(p->vTtMem[v]) == Vec_PtrSize(p->vTtDecs[v]) );
517  // find max number of decompositions
518  Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
519  {
520  pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
521  nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
522  pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) );
523  nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) );
524  }
525  // fill up
526  Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
527  {
528  pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
529  nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
530  pCountsAll[nSuppSize]++;
531  pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs);
532  pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++;
533  // pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++;
534  /*
535  if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] )
536  {
537  fprintf( pFile, "0x" );
538  Abc_TtPrintHex( pTruth, nSuppSize );
539  Dau_DecPrintSets( vDecs, nSuppSize );
540  }
541  */
542  }
543  }
544  // print header
545  fprintf( pFile, " N : " );
546  fprintf( pFile, " Total " );
547  for ( k = 0; k <= DSD_ARRAY_LIMIT; k++ )
548  fprintf( pFile, "%6d", k );
549  fprintf( pFile, " " );
550  fprintf( pFile, " More" );
551  fprintf( pFile, " Ave" );
552  fprintf( pFile, " Max" );
553  fprintf( pFile, "\n" );
554  // print rows
555  for ( i = 0; i <= p->nVars; i++ )
556  {
557  fprintf( pFile, "%2d : ", i );
558  fprintf( pFile, "%6d ", pCountsAll[i] );
559  for ( k = 0; k <= DSD_ARRAY_LIMIT; k++ )
560 // fprintf( pFile, "%6d", pCounts[i][k] );
561  fprintf( pFile, "%6.1f", 100.0*pCounts[i][k]/Abc_MaxInt(1,pCountsAll[i]) );
562  fprintf( pFile, " " );
563 // fprintf( pFile, "%6d", pCounts[i][k] );
564  fprintf( pFile, "%6.1f", 100.0*pCounts[i][k]/Abc_MaxInt(1,pCountsAll[i]) );
565  fprintf( pFile, " " );
566  fprintf( pFile, "%6.1f", 1.0*pCountsSSizes[i]/Abc_MaxInt(1,pCountsAll[i]) );
567  fprintf( pFile, " " );
568  fprintf( pFile, "%6d", pDecMax[i] );
569  fprintf( pFile, "\n" );
570  }
571 }
572 void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p )
573 {
574  char Buffer[100];
575  If_DsdObj_t * pObj;
576  Vec_Int_t * vOccurs;
577  int nOccurs, nOccursMax, nOccursAll;
578  int i, k, nSizeMax, Counter = 0;
579  // determine the largest fanin and fanout
580  nOccursMax = nOccursAll = 0;
581  If_DsdVecForEachNode( &p->vObjs, pObj, i )
582  {
583  nOccurs = pObj->Count;
584  nOccursAll += nOccurs;
585  nOccursMax = Abc_MaxInt( nOccursMax, nOccurs );
586  }
587  // allocate storage for fanin/fanout numbers
588  nSizeMax = 10 * (Abc_Base10Log(nOccursMax) + 1);
589  vOccurs = Vec_IntStart( nSizeMax );
590  // count the number of fanins and fanouts
591  If_DsdVecForEachNode( &p->vObjs, pObj, i )
592  {
593  nOccurs = pObj->Count;
594  if ( nOccurs < 10 )
595  Vec_IntAddToEntry( vOccurs, nOccurs, 1 );
596  else if ( nOccurs < 100 )
597  Vec_IntAddToEntry( vOccurs, 10 + nOccurs/10, 1 );
598  else if ( nOccurs < 1000 )
599  Vec_IntAddToEntry( vOccurs, 20 + nOccurs/100, 1 );
600  else if ( nOccurs < 10000 )
601  Vec_IntAddToEntry( vOccurs, 30 + nOccurs/1000, 1 );
602  else if ( nOccurs < 100000 )
603  Vec_IntAddToEntry( vOccurs, 40 + nOccurs/10000, 1 );
604  else if ( nOccurs < 1000000 )
605  Vec_IntAddToEntry( vOccurs, 50 + nOccurs/100000, 1 );
606  else if ( nOccurs < 10000000 )
607  Vec_IntAddToEntry( vOccurs, 60 + nOccurs/1000000, 1 );
608  }
609  fprintf( pFile, "The distribution of object occurrences:\n" );
610  for ( k = 0; k < nSizeMax; k++ )
611  {
612  if ( Vec_IntEntry(vOccurs, k) == 0 )
613  continue;
614  if ( k < 10 )
615  fprintf( pFile, "%15d : ", k );
616  else
617  {
618  sprintf( Buffer, "%d - %d", (int)pow((double)10, k/10) * (k%10), (int)pow((double)10, k/10) * (k%10+1) - 1 );
619  fprintf( pFile, "%15s : ", Buffer );
620  }
621  fprintf( pFile, "%12d ", Vec_IntEntry(vOccurs, k) );
622  Counter += Vec_IntEntry(vOccurs, k);
623  fprintf( pFile, "(%6.2f %%)", 100.0*Counter/Vec_PtrSize(&p->vObjs) );
624  fprintf( pFile, "\n" );
625  }
626  Vec_IntFree( vOccurs );
627  fprintf( pFile, "Fanins: Max = %d. Ave = %.2f.\n", nOccursMax, 1.0*nOccursAll/Vec_PtrSize(&p->vObjs) );
628 }
629 
630 void If_DsdManPrintDistrib( If_DsdMan_t * p )
631 {
632  If_DsdObj_t * pObj; int i;
633  int CountObj[IF_MAX_FUNC_LUTSIZE+2] = {0};
634  int CountObjNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
635  int CountObjNpn[IF_MAX_FUNC_LUTSIZE+2] = {0};
636  int CountStr[IF_MAX_FUNC_LUTSIZE+2] = {0};
637  int CountStrNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
638  int CountMarked[IF_MAX_FUNC_LUTSIZE+2] = {0};
639  for ( i = 3; i <= p->nVars; i++ )
640  {
641  CountObjNpn[i] = Vec_MemEntryNum(p->vTtMem[i]);
642  CountObjNpn[p->nVars+1] += Vec_MemEntryNum(p->vTtMem[i]);
643  }
644  If_DsdVecForEachObj( &p->vObjs, pObj, i )
645  {
646  CountObj[If_DsdObjFaninNum(pObj)]++, CountObj[p->nVars+1]++;
647  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
648  CountObjNon[If_DsdObjFaninNum(pObj)]++, CountObjNon[p->nVars+1]++;
649  CountStr[If_DsdObjSuppSize(pObj)]++, CountStr[p->nVars+1]++;
650  if ( If_DsdManCheckNonDec_rec(p, i) )
651  CountStrNon[If_DsdObjSuppSize(pObj)]++, CountStrNon[p->nVars+1]++;
652  if ( If_DsdVecObjMark(&p->vObjs, i) )
653  CountMarked[If_DsdObjSuppSize(pObj)]++, CountMarked[p->nVars+1]++;
654  }
655  printf( "***** DSD MANAGER STATISTICS *****\n" );
656  printf( "Support " );
657  printf( "Obj " );
658  printf( "ObjNDSD " );
659  printf( "NPNNDSD " );
660  printf( "Str " );
661  printf( "StrNDSD " );
662  printf( "Marked " );
663  printf( "\n" );
664  for ( i = 0; i <= p->nVars + 1; i++ )
665  {
666  if ( i == p->nVars + 1 )
667  printf( "All : " );
668  else
669  printf( "%3d : ", i );
670  printf( "%9d ", CountObj[i] );
671  printf( "%9d ", CountObjNon[i] );
672  printf( "%6.2f %% ", 100.0 * CountObjNon[i] / Abc_MaxInt(1, CountObj[i]) );
673  printf( "%9d ", CountObjNpn[i] );
674  printf( "%6.2f %% ", 100.0 * CountObjNpn[i] / Abc_MaxInt(1, CountObj[i]) );
675  printf( " " );
676  printf( "%9d ", CountStr[i] );
677  printf( "%9d ", CountStrNon[i] );
678  printf( "%6.2f %% ", 100.0 * CountStrNon[i] / Abc_MaxInt(1, CountStr[i]) );
679  printf( "%9d ", CountMarked[i] );
680  printf( "%6.2f %%", 100.0 * CountMarked[i] / Abc_MaxInt(1, CountStr[i]) );
681  printf( "\n" );
682  }
683 }
684 void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose )
685 {
686  If_DsdObj_t * pObj;
687  Vec_Int_t * vStructs, * vCounts;
688  int CountUsed = 0, CountNonDsd = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0;
689  int i, v, * pPerm, DsdMax = 0, MemSizeTTs = 0, MemSizeDecs = 0;
690  FILE * pFile;
691  pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
692  if ( pFileName && pFile == NULL )
693  {
694  printf( "cannot open output file\n" );
695  return;
696  }
697  if ( fVerbose )
698  {
699  fprintf( pFile, "***** NOTATIONS USED BELOW *****\n" );
700  fprintf( pFile, "Support -- the support size\n" );
701  fprintf( pFile, "Obj -- the number of nodes in the DSD manager for each support size\n" );
702  fprintf( pFile, " (the constant node and the primary input node have no support)\n" );
703  fprintf( pFile, "ObjNDSD -- the number of prime nodes (that is, nodes whose function has no DSD)\n" );
704  fprintf( pFile, " (percentage is relative to the number of all nodes of that size)\n" );
705  fprintf( pFile, "NPNNDSD -- the number of different NPN classes of prime nodes\n" );
706  fprintf( pFile, " (Each NPN class may appear more than once. For example: F1 = 17(ab(cd))\n" );
707  fprintf( pFile, " and F2 = 17(ab[cd]) both have prime majority node (hex TT is 17),\n" );
708  fprintf( pFile, " but in one case the majority node is fed by AND, and in another by XOR.\n" );
709  fprintf( pFile, " These two majority nodes are different nodes in the DSD manager\n" );
710  fprintf( pFile, "Str -- the number of structures for each support size\n" );
711  fprintf( pFile, " (each structure is composed of one or more nodes)\n" );
712  fprintf( pFile, "StrNDSD -- the number of DSD structures containing at least one prime node\n" );
713  fprintf( pFile, "Marked -- the number of DSD structures matchable with the LUT structure (say, \"44\")\n" );
714  }
715  If_DsdVecForEachObj( &p->vObjs, pObj, i )
716  {
717  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
718  DsdMax = Abc_MaxInt( DsdMax, pObj->nFans );
719  CountPrime += If_DsdObjType(pObj) == IF_DSD_PRIME;
720  CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
721  CountUsed += ( If_DsdVecObjRef(&p->vObjs, pObj->Id) > 0 );
722  CountMarked += If_DsdVecObjMark( &p->vObjs, i );
723  }
724  for ( v = 3; v <= p->nVars; v++ )
725  {
726  CountNonDsd += Vec_MemEntryNum(p->vTtMem[v]);
727  MemSizeTTs += Vec_MemEntrySize(p->vTtMem[v]) * Vec_MemEntryNum(p->vTtMem[v]);
728  MemSizeDecs += (int)Vec_VecMemoryInt((Vec_Vec_t *)(p->vTtDecs[v]));
729  }
730  If_DsdManPrintDistrib( p );
731  printf( "Number of inputs = %d. LUT size = %d. Marks = %s. NewAsUseless = %s. Bookmark = %d.\n",
732  p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev );
733  if ( p->pCellStr )
734  printf( "Symbolic cell description: %s\n", p->pCellStr );
735  if ( p->pTtGia )
736  fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) );
737  fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses );
738  fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits );
739  fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
740  fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(MemSizeTTs+sizeof(int)*Vec_IntCap(&p->vTruths))/(1<<20) );
741  fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(&p->vNexts))/(1<<20) );
742  fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", 1.0*MemSizeDecs/(1<<20) );
743  fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(&p->vObjs)/(1<<20) );
744  if ( p->pTtGia )
745  fprintf( pFile, "Memory used for AIG = %8.2f MB.\n", 8.0*Gia_ManAndNum(p->pTtGia)/(1<<20) );
746  if ( p->timeDsd )
747  {
748  Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
749  Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck );
750  Abc_PrintTime( 1, "Time check ", p->timeCheck );
751  Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
752  Abc_PrintTime( 1, "Time verify", p->timeVerify );
753  }
754  if ( fOccurs )
755  If_DsdManPrintOccurs( stdout, p );
756 // If_DsdManHashProfile( p );
757  if ( fTtDump )
758  If_DsdManDumpDsd( p, Support );
759  if ( fTtDump )
760  If_DsdManDumpAll( p, Support );
761 // If_DsdManPrintDecs( stdout, p );
762  if ( !fVerbose )
763  return;
764  vStructs = Vec_IntAlloc( 1000 );
765  vCounts = Vec_IntAlloc( 1000 );
766  If_DsdVecForEachObj( &p->vObjs, pObj, i )
767  {
768  if ( Number && i % Number )
769  continue;
770  if ( Support && Support != If_DsdObjSuppSize(pObj) )
771  continue;
772  Vec_IntPush( vStructs, i );
773  Vec_IntPush( vCounts, -(int)pObj->Count );
774 // If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
775  }
776 // fprintf( pFile, "\n" );
777  pPerm = Abc_MergeSortCost( Vec_IntArray(vCounts), Vec_IntSize(vCounts) );
778  for ( i = 0; i < Abc_MinInt(Vec_IntSize(vCounts), 20); i++ )
779  {
780  printf( "%2d : ", i+1 );
781  pObj = If_DsdVecObj( &p->vObjs, Vec_IntEntry(vStructs, pPerm[i]) );
782  If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
783  }
784  ABC_FREE( pPerm );
785  Vec_IntFree( vStructs );
786  Vec_IntFree( vCounts );
787  if ( pFileName )
788  fclose( pFile );
789 }
790 
791 /**Function*************************************************************
792 
793  Synopsis [Check if the function is non-trivial.]
794 
795  Description []
796 
797  SideEffects []
798 
799  SeeAlso []
800 
801 ***********************************************************************/
802 int If_DsdManCheckNonTriv( If_DsdMan_t * p, int Id, int nVars, int iVarMax )
803 {
804  If_DsdObj_t * pObj; int i, iFanin;
805  pObj = If_DsdVecObj( &p->vObjs, Id );
806  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
807  return 1;
808  if ( If_DsdObjFaninNum(pObj) == nVars )
809  return 0;
810  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
811  if ( Abc_Lit2Var(iFanin) == 1 && i == iVarMax )
812  return 0;
813  return 1;
814 }
815 
816 /**Function*************************************************************
817 
818  Synopsis [Sorting DSD literals.]
819 
820  Description []
821 
822  SideEffects []
823 
824  SeeAlso []
825 
826 ***********************************************************************/
827 int If_DsdObjCompare( If_DsdMan_t * pMan, Vec_Ptr_t * p, int iLit0, int iLit1 )
828 {
829  If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
830  If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
831  int i, Res;
832  if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
833  return -1;
834  if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
835  return 1;
836  if ( If_DsdObjType(p0) < IF_DSD_AND )
837  return 0;
838  if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
839  return -1;
840  if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
841  return 1;
842  if ( If_DsdObjType(p0) == IF_DSD_PRIME )
843  {
844  if ( If_DsdObjTruthId(pMan, p0) < If_DsdObjTruthId(pMan, p1) )
845  return -1;
846  if ( If_DsdObjTruthId(pMan, p0) > If_DsdObjTruthId(pMan, p1) )
847  return 1;
848  }
849  for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
850  {
851  Res = If_DsdObjCompare( pMan, p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
852  if ( Res != 0 )
853  return Res;
854  }
855  if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
856  return -1;
857  if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
858  return 1;
859  assert( iLit0 == iLit1 );
860  return 0;
861 }
862 void If_DsdObjSort( If_DsdMan_t * pMan, Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
863 {
864  int i, j, best_i;
865  for ( i = 0; i < nLits-1; i++ )
866  {
867  best_i = i;
868  for ( j = i+1; j < nLits; j++ )
869  if ( If_DsdObjCompare(pMan, p, pLits[best_i], pLits[j]) == 1 )
870  best_i = j;
871  if ( i == best_i )
872  continue;
873  ABC_SWAP( int, pLits[i], pLits[best_i] );
874  if ( pPerm )
875  ABC_SWAP( int, pPerm[i], pPerm[best_i] );
876  }
877 }
878 
879 /**Function*************************************************************
880 
881  Synopsis []
882 
883  Description []
884 
885  SideEffects []
886 
887  SeeAlso []
888 
889 ***********************************************************************/
890 static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
891 {
892  static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909,
893  3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281,
894  5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
895  int i;
896  unsigned uHash = Type * 7873 + nLits * 8147;
897  for ( i = 0; i < nLits; i++ )
898  uHash += pLits[i] * s_Primes[i & 0xF];
899  if ( Type == IF_DSD_PRIME )
900  uHash += truthId * s_Primes[i & 0xF];
901  return uHash % p->nBins;
902 }
903 unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
904 {
905  If_DsdObj_t * pObj;
906  unsigned * pSpot = p->pBins + If_DsdObjHashKey(p, Type, pLits, nLits, truthId);
907  for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(&p->vNexts, pObj->Id) )
908  {
909  pObj = If_DsdVecObj( &p->vObjs, *pSpot );
910  if ( If_DsdObjType(pObj) == Type &&
911  If_DsdObjFaninNum(pObj) == nLits &&
912  !memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) &&
913  truthId == If_DsdObjTruthId(p, pObj) )
914  {
915  p->nUniqueHits++;
916  return pSpot;
917  }
918  }
919  p->nUniqueMisses++;
920  return pSpot;
921 }
922 static void If_DsdObjHashResize( If_DsdMan_t * p )
923 {
924  If_DsdObj_t * pObj;
925  unsigned * pSpot;
926  int i, Prev = p->nUniqueMisses;
927  p->nBins = Abc_PrimeCudd( 2 * p->nBins );
928  p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
929  memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
930  Vec_IntFill( &p->vNexts, Vec_PtrSize(&p->vObjs), 0 );
931  If_DsdVecForEachNode( &p->vObjs, pObj, i )
932  {
933  pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
934  assert( *pSpot == 0 );
935  *pSpot = pObj->Id;
936  }
937  assert( p->nUniqueMisses - Prev == Vec_PtrSize(&p->vObjs) - 2 );
938  p->nUniqueMisses = Prev;
939 }
940 
941 int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
942 {
943  If_DsdObj_t * pObj, * pFanin;
944  int i, iPrev = -1;
945  // check structural canonicity
946  assert( Type != DAU_DSD_MUX || nLits == 3 );
947 // assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
948  assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
949  // check that leaves are in good order
950  if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
951  {
952  for ( i = 0; i < nLits; i++ )
953  {
954  pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[i]) );
955  assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
956  assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
957  assert( iPrev == -1 || If_DsdObjCompare(p, &p->vObjs, iPrev, pLits[i]) <= 0 );
958  iPrev = pLits[i];
959  }
960  }
961  // create new node
962  pObj = If_DsdObjAlloc( p, Type, nLits );
963  if ( Type == DAU_DSD_PRIME )
964  If_DsdObjSetTruth( p, pObj, truthId );
965  assert( pObj->nSupp == 0 );
966  for ( i = 0; i < nLits; i++ )
967  {
968  pObj->pFans[i] = pLits[i];
969  pObj->nSupp += If_DsdVecLitSuppSize(&p->vObjs, pLits[i]);
970  }
971  // check decomposability
972  if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0, 0, 0) )
973  If_DsdVecObjSetMark( &p->vObjs, pObj->Id );
974  return pObj->Id;
975 }
976 int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
977 {
978  int PrevSize = (Type == IF_DSD_PRIME) ? Vec_MemEntryNum( p->vTtMem[nLits] ) : -1;
979  int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
980  unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
981 //abctime clk;
982  if ( *pSpot )
983  return (int)*pSpot;
984 //clk = Abc_Clock();
985  if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
986  {
987  Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
988  assert( truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 );
989  Vec_PtrPush( p->vTtDecs[nLits], vSets );
990 // Dau_DecPrintSets( vSets, nLits );
991  }
992  if ( p->vIsops[nLits] && truthId >= 0 && PrevSize != Vec_MemEntryNum(p->vTtMem[nLits]) )
993  {
994  Vec_Int_t * vLevel = Vec_WecPushLevel( p->vIsops[nLits] );
995  int fCompl = Kit_TruthIsop( (unsigned *)pTruth, nLits, p->vCover, 1 );
996  if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
997  {
998  Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
999  Vec_IntAppend( vLevel, p->vCover );
1000  if ( fCompl )
1001  vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
1002  }
1003  assert( Vec_WecSize(p->vIsops[nLits]) == Vec_MemEntryNum(p->vTtMem[nLits]) );
1004  }
1005  if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 )
1006  {
1007 // int nObjOld = Gia_ManAndNum(p->pTtGia);
1008  int Lit = Kit_TruthToGia( p->pTtGia, (unsigned *)pTruth, nLits, p->vCover, NULL, 1 );
1009 // printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
1010  Gia_ManAppendCo( p->pTtGia, Lit );
1011  }
1012 //p->timeCheck += Abc_Clock() - clk;
1013  *pSpot = Vec_PtrSize( &p->vObjs );
1014  objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
1015  if ( Vec_PtrSize(&p->vObjs) > p->nBins )
1016  If_DsdObjHashResize( p );
1017  return objId;
1018 }
1019 
1020 
1021 /**Function*************************************************************
1022 
1023  Synopsis [Saving/loading DSD manager.]
1024 
1025  Description []
1026 
1027  SideEffects []
1028 
1029  SeeAlso []
1030 
1031 ***********************************************************************/
1032 void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
1033 {
1034  If_DsdObj_t * pObj;
1035  Vec_Int_t * vSets;
1036  char * pBuffer = "dsd0";
1037  word * pTruth;
1038  int i, v, Num;
1039  FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
1040  if ( pFile == NULL )
1041  {
1042  printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
1043  return;
1044  }
1045  fwrite( pBuffer, 4, 1, pFile );
1046  Num = p->nVars;
1047  fwrite( &Num, 4, 1, pFile );
1048  Num = p->LutSize;
1049  fwrite( &Num, 4, 1, pFile );
1050  Num = Vec_PtrSize(&p->vObjs);
1051  fwrite( &Num, 4, 1, pFile );
1052  Vec_PtrForEachEntryStart( If_DsdObj_t *, &p->vObjs, pObj, i, 2 )
1053  {
1054  Num = If_DsdObjWordNum( pObj->nFans );
1055  fwrite( &Num, 4, 1, pFile );
1056  fwrite( pObj, sizeof(word)*Num, 1, pFile );
1057  if ( pObj->Type == IF_DSD_PRIME )
1058  fwrite( Vec_IntEntryP(&p->vTruths, i), 4, 1, pFile );
1059  }
1060  for ( v = 3; v <= p->nVars; v++ )
1061  {
1062  int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
1063  Num = Vec_MemEntryNum(p->vTtMem[v]);
1064  fwrite( &Num, 4, 1, pFile );
1065  Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
1066  fwrite( pTruth, nBytes, 1, pFile );
1067  Num = Vec_PtrSize(p->vTtDecs[v]);
1068  fwrite( &Num, 4, 1, pFile );
1069  Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vSets, i )
1070  {
1071  Num = Vec_IntSize(vSets);
1072  fwrite( &Num, 4, 1, pFile );
1073  fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
1074  }
1075  }
1076  Num = p->vPerms ? Vec_WrdSize(p->vPerms) : 0;
1077  fwrite( &Num, 4, 1, pFile );
1078  if ( Num )
1079  fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
1080  Num = p->pCellStr ? strlen(p->pCellStr) : 0;
1081  fwrite( &Num, 4, 1, pFile );
1082  if ( Num )
1083  fwrite( p->pCellStr, sizeof(char)*Num, 1, pFile );
1084  fclose( pFile );
1085 }
1086 If_DsdMan_t * If_DsdManLoad( char * pFileName )
1087 {
1088  If_DsdMan_t * p;
1089  If_DsdObj_t * pObj;
1090  Vec_Int_t * vSets;
1091  char pBuffer[10];
1092  unsigned * pSpot;
1093  word * pTruth;
1094  int i, v, Num, Num2, RetValue;
1095  FILE * pFile = fopen( pFileName, "rb" );
1096  if ( pFile == NULL )
1097  {
1098  printf( "Reading DSD manager file \"%s\" has failed.\n", pFileName );
1099  return NULL;
1100  }
1101  RetValue = fread( pBuffer, 4, 1, pFile );
1102  if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' )
1103  {
1104  printf( "Unrecognized format of file \"%s\".\n", pFileName );
1105  return NULL;
1106  }
1107  RetValue = fread( &Num, 4, 1, pFile );
1108  p = If_DsdManAlloc( Num, 0 );
1109  ABC_FREE( p->pStore );
1110  p->pStore = Abc_UtilStrsav( pFileName );
1111  RetValue = fread( &Num, 4, 1, pFile );
1112  p->LutSize = Num;
1113  p->pSat = If_ManSatBuildXY( p->LutSize );
1114  RetValue = fread( &Num, 4, 1, pFile );
1115  assert( Num >= 2 );
1116  Vec_PtrFillExtra( &p->vObjs, Num, NULL );
1117  Vec_IntFill( &p->vNexts, Num, 0 );
1118  Vec_IntFill( &p->vTruths, Num, -1 );
1119  p->nBins = Abc_PrimeCudd( 2*Num );
1120  p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
1121  memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
1122  for ( i = 2; i < Vec_PtrSize(&p->vObjs); i++ )
1123  {
1124  RetValue = fread( &Num, 4, 1, pFile );
1125  pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
1126  RetValue = fread( pObj, sizeof(word)*Num, 1, pFile );
1127  Vec_PtrWriteEntry( &p->vObjs, i, pObj );
1128  if ( pObj->Type == IF_DSD_PRIME )
1129  {
1130  RetValue = fread( &Num, 4, 1, pFile );
1131  Vec_IntWriteEntry( &p->vTruths, i, Num );
1132  }
1133  pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
1134  assert( *pSpot == 0 );
1135  *pSpot = pObj->Id;
1136  }
1137  assert( p->nUniqueMisses == Vec_PtrSize(&p->vObjs) - 2 );
1138  p->nUniqueMisses = 0;
1139  pTruth = ABC_ALLOC( word, p->nWords );
1140  for ( v = 3; v <= p->nVars; v++ )
1141  {
1142  int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
1143  RetValue = fread( &Num, 4, 1, pFile );
1144  for ( i = 0; i < Num; i++ )
1145  {
1146  RetValue = fread( pTruth, nBytes, 1, pFile );
1147  Vec_MemHashInsert( p->vTtMem[v], pTruth );
1148  }
1149  assert( Num == Vec_MemEntryNum(p->vTtMem[v]) );
1150  RetValue = fread( &Num2, 4, 1, pFile );
1151  for ( i = 0; i < Num2; i++ )
1152  {
1153  RetValue = fread( &Num, 4, 1, pFile );
1154  vSets = Vec_IntAlloc( Num );
1155  RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
1156  vSets->nSize = Num;
1157  Vec_PtrPush( p->vTtDecs[v], vSets );
1158  }
1159  assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) );
1160  }
1161  ABC_FREE( pTruth );
1162  RetValue = fread( &Num, 4, 1, pFile );
1163  if ( RetValue && Num )
1164  {
1165  p->vPerms = Vec_WrdStart( Num );
1166  RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
1167  }
1168  RetValue = fread( &Num, 4, 1, pFile );
1169  if ( RetValue && Num )
1170  {
1171  p->pCellStr = ABC_CALLOC( char, Num + 1 );
1172  RetValue = fread( p->pCellStr, sizeof(char)*Num, 1, pFile );
1173  }
1174  fclose( pFile );
1175  return p;
1176 }
1177 void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
1178 {
1179  If_DsdObj_t * pObj;
1180  Vec_Int_t * vMap;
1181  int pFanins[DAU_MAX_VAR];
1182  int i, k, iFanin, Id;
1183  if ( p->nVars < pNew->nVars )
1184  {
1185  printf( "The number of variables should be the same or smaller.\n" );
1186  return;
1187  }
1188  if ( p->LutSize != pNew->LutSize )
1189  {
1190  printf( "LUT size should be the same.\n" );
1191  return;
1192  }
1193  if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) )
1194  printf( "Warning! Old manager has %smarks while new manager has %smarks.\n",
1195  If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " );
1196  vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) );
1197  Vec_IntPush( vMap, 0 );
1198  Vec_IntPush( vMap, 1 );
1199  if ( p->vPerms && pNew->vPerms )
1200  Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs), 0 );
1201  If_DsdVecForEachNode( &pNew->vObjs, pObj, i )
1202  {
1203  If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k )
1204  pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
1205  Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL );
1206  if ( pObj->fMark )
1207  If_DsdVecObjSetMark( &p->vObjs, Id );
1208  if ( p->vPerms && pNew->vPerms && i < Vec_WrdSize(pNew->vPerms) )
1209  Vec_WrdFillExtra( p->vPerms, Id, Vec_WrdEntry(pNew->vPerms, i) );
1210  Vec_IntPush( vMap, Id );
1211  }
1212  assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
1213  Vec_IntFree( vMap );
1214  if ( p->vPerms && pNew->vPerms )
1215  Vec_WrdShrink( p->vPerms, Vec_PtrSize(&p->vObjs) );
1216 }
1217 void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose )
1218 {
1219  If_DsdObj_t * pObj;
1220  int i;
1221  If_DsdVecForEachObj( &p->vObjs, pObj, i )
1222  pObj->Count = 0;
1223 }
1224 void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
1225 {
1226  If_DsdObj_t * pObj;
1227  int i;
1228  ABC_FREE( p->pCellStr );
1229  Vec_WrdFreeP( &p->vPerms );
1230  If_DsdVecForEachObj( &p->vObjs, pObj, i )
1231  pObj->fMark = 0;
1232 }
1233 void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose )
1234 {
1235  If_DsdObj_t * pObj;
1236  int i;
1237  ABC_FREE( p->pCellStr );
1238  Vec_WrdFreeP( &p->vPerms );
1239  If_DsdVecForEachObj( &p->vObjs, pObj, i )
1240  pObj->fMark = !pObj->fMark;
1241 }
1242 void If_DsdManFilter_rec( If_DsdMan_t * pNew, If_DsdMan_t * p, int i, Vec_Int_t * vMap )
1243 {
1244  If_DsdObj_t * pObj;
1245  int pFanins[DAU_MAX_VAR];
1246  int k, iFanin, Id;
1247  if ( Vec_IntEntry(vMap, i) >= 0 )
1248  return;
1249  // call recursively
1250  pObj = If_DsdVecObj( &p->vObjs, i );
1251  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
1252  If_DsdManFilter_rec( pNew, p, Abc_Lit2Var(iFanin), vMap );
1253  // duplicate this one
1254  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
1255  pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
1256  Id = If_DsdObjFindOrAdd( pNew, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(p, pObj) : NULL );
1257  if ( pObj->fMark )
1258  If_DsdVecObjSetMark( &pNew->vObjs, Id );
1259  If_DsdVecObj( &pNew->vObjs, Id )->Count = pObj->Count;
1260  // save the result
1261  Vec_IntWriteEntry( vMap, i, Id );
1262 }
1263 If_DsdMan_t * If_DsdManFilter( If_DsdMan_t * p, int Limit )
1264 {
1265  If_DsdMan_t * pNew = If_DsdManAlloc( p->nVars, p->LutSize );
1266  If_DsdObj_t * pObj;
1267  Vec_Int_t * vMap;
1268  int i;
1269  vMap = Vec_IntStartFull( Vec_PtrSize(&p->vObjs) );
1270  Vec_IntWriteEntry( vMap, 0, 0 );
1271  Vec_IntWriteEntry( vMap, 1, 1 );
1272  If_DsdVecForEachNode( &p->vObjs, pObj, i )
1273  if ( (int)pObj->Count >= Limit )
1274  If_DsdManFilter_rec( pNew, p, i, vMap );
1275  Vec_IntFree( vMap );
1276  return pNew;
1277 }
1278 
1279 /**Function*************************************************************
1280 
1281  Synopsis [Collect nodes of the tree.]
1282 
1283  Description []
1284 
1285  SideEffects []
1286 
1287  SeeAlso []
1288 
1289 ***********************************************************************/
1290 void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts, int * pnSupp )
1291 {
1292  int i, iFanin, iFirst;
1293  If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
1294  if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
1295  return;
1296  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1297  {
1298  (*pnSupp)++;
1299  return;
1300  }
1301  iFirst = *pnSupp;
1302  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1303  If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes, vFirsts, pnSupp );
1304  Vec_IntPush( vNodes, Id );
1305  Vec_IntPush( vFirsts, iFirst );
1306 }
1307 void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts )
1308 {
1309  int nSupp = 0;
1310  Vec_IntClear( vNodes );
1311  Vec_IntClear( vFirsts );
1312  If_DsdManCollect_rec( p, Id, vNodes, vFirsts, &nSupp );
1313 }
1314 
1315 /**Function*************************************************************
1316 
1317  Synopsis []
1318 
1319  Description []
1320 
1321  SideEffects []
1322 
1323  SeeAlso []
1324 
1325 ***********************************************************************/
1326 void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned char * pPermLits, int * pnSupp )
1327 {
1328  int i, iFanin, fCompl = Abc_LitIsCompl(iDsd);
1329  If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1330  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1331  {
1332  int iPermLit = pPermLits ? (int)pPermLits[*pnSupp] : Abc_Var2Lit(*pnSupp, 0);
1333  (*pnSupp)++;
1334  assert( (*pnSupp) <= p->nVars );
1335  Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
1336  return;
1337  }
1338  if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR )
1339  {
1340  word pTtTemp[DAU_MAX_WORD];
1341  if ( If_DsdObjType(pObj) == IF_DSD_AND )
1342  Abc_TtConst1( pRes, p->nWords );
1343  else
1344  Abc_TtConst0( pRes, p->nWords );
1345  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1346  {
1347  If_DsdManComputeTruth_rec( p, iFanin, pTtTemp, pPermLits, pnSupp );
1348  if ( If_DsdObjType(pObj) == IF_DSD_AND )
1349  Abc_TtAnd( pRes, pRes, pTtTemp, p->nWords, 0 );
1350  else
1351  Abc_TtXor( pRes, pRes, pTtTemp, p->nWords, 0 );
1352  }
1353  if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1354  return;
1355  }
1356  if ( If_DsdObjType(pObj) == IF_DSD_MUX ) // mux
1357  {
1358  word pTtTemp[3][DAU_MAX_WORD];
1359  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1360  If_DsdManComputeTruth_rec( p, iFanin, pTtTemp[i], pPermLits, pnSupp );
1361  assert( i == 3 );
1362  Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], p->nWords );
1363  if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1364  return;
1365  }
1366  if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) // function
1367  {
1368  word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
1369  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1370  If_DsdManComputeTruth_rec( p, iFanin, pFanins[i], pPermLits, pnSupp );
1371  Dau_DsdTruthCompose_rec( If_DsdObjTruth(p, pObj), pFanins, pRes, pObj->nFans, p->nWords );
1372  if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1373  return;
1374  }
1375  assert( 0 );
1376 
1377 }
1378 void If_DsdManComputeTruthPtr( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits, word * pRes )
1379 {
1380  int nSupp = 0;
1381  If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1382  if ( iDsd == 0 )
1383  Abc_TtConst0( pRes, p->nWords );
1384  else if ( iDsd == 1 )
1385  Abc_TtConst1( pRes, p->nWords );
1386  else if ( pObj->Type == IF_DSD_VAR )
1387  {
1388  int iPermLit = pPermLits ? (int)pPermLits[nSupp] : Abc_Var2Lit(nSupp, 0);
1389  nSupp++;
1390  Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
1391  }
1392  else
1393  If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp );
1394  assert( nSupp == If_DsdVecLitSuppSize(&p->vObjs, iDsd) );
1395 }
1396 word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits )
1397 {
1398  word * pRes = p->pTtElems[DAU_MAX_VAR];
1399  If_DsdManComputeTruthPtr( p, iDsd, pPermLits, pRes );
1400  return pRes;
1401 }
1402 
1403 /**Function*************************************************************
1404 
1405  Synopsis [Procedures to propagate the invertor.]
1406 
1407  Description []
1408 
1409  SideEffects []
1410 
1411  SeeAlso []
1412 
1413 ***********************************************************************/
1414 int If_DsdManCheckInv_rec( If_DsdMan_t * p, int iLit )
1415 {
1416  If_DsdObj_t * pObj;
1417  int i, iFanin;
1418  pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLit) );
1419  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1420  return 1;
1421  if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_PRIME )
1422  return 0;
1423  if ( If_DsdObjType(pObj) == IF_DSD_XOR )
1424  {
1425  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1426  if ( If_DsdManCheckInv_rec(p, iFanin) )
1427  return 1;
1428  return 0;
1429  }
1430  if ( If_DsdObjType(pObj) == IF_DSD_MUX )
1431  return If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]);
1432  assert( 0 );
1433  return 0;
1434 }
1435 int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
1436 {
1437  If_DsdObj_t * pObj;
1438  int i, iFanin;
1439  pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLit) );
1440  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1441  pPerm[0] = (unsigned char)Abc_LitNot((int)pPerm[0]);
1442  else if ( If_DsdObjType(pObj) == IF_DSD_XOR )
1443  {
1444  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1445  {
1446  if ( If_DsdManCheckInv_rec(p, iFanin) )
1447  {
1448  If_DsdManPushInv_rec( p, iFanin, pPerm );
1449  break;
1450  }
1451  pPerm += If_DsdVecLitSuppSize(&p->vObjs, iFanin);
1452  }
1453  }
1454  else if ( If_DsdObjType(pObj) == IF_DSD_MUX )
1455  {
1456  assert( If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]) );
1457  pPerm += If_DsdVecLitSuppSize(&p->vObjs, pObj->pFans[0]);
1458  If_DsdManPushInv_rec(p, pObj->pFans[1], pPerm);
1459  pPerm += If_DsdVecLitSuppSize(&p->vObjs, pObj->pFans[1]);
1460  If_DsdManPushInv_rec(p, pObj->pFans[2], pPerm);
1461  }
1462  else assert( 0 );
1463  return 1;
1464 }
1465 int If_DsdManPushInv( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
1466 {
1467  if ( Abc_LitIsCompl(iLit) && If_DsdManCheckInv_rec(p, iLit) )
1468  return If_DsdManPushInv_rec( p, iLit, pPerm );
1469  return 0;
1470 }
1471 
1472 /**Function*************************************************************
1473 
1474  Synopsis [Performs DSD operation.]
1475 
1476  Description []
1477 
1478  SideEffects []
1479 
1480  SeeAlso []
1481 
1482 ***********************************************************************/
1483 int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
1484 {
1485  int i, nSSize = 0;
1486  for ( i = 0; i < nLits; i++ )
1487  {
1488  pFirsts[i] = nSSize;
1489  nSSize += If_DsdVecLitSuppSize(&p->vObjs, pLits[i]);
1490  }
1491  return nSSize;
1492 }
1493 int If_DsdManComputeFirst( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pFirsts )
1494 {
1495  return If_DsdManComputeFirstArray( p, (int *)pObj->pFans, pObj->nFans, pFirsts );
1496 }
1497 int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
1498 {
1499  If_DsdObj_t * pObj, * pFanin;
1500  unsigned char pPermNew[DAU_MAX_VAR], * pPermStart = pPerm;
1501  int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
1502  int i, k, j, Id, iFanin, fCompl = 0, nSSize = 0;
1503  if ( Type == IF_DSD_AND || Type == IF_DSD_XOR )
1504  {
1505  for ( k = 0; k < nLits; k++ )
1506  {
1507  if ( Type == IF_DSD_XOR && Abc_LitIsCompl(pLits[k]) )
1508  {
1509  pLits[k] = Abc_LitNot(pLits[k]);
1510  fCompl ^= 1;
1511  }
1512  pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1513  if ( Type == If_DsdObjType(pObj) && (Type == IF_DSD_XOR || !Abc_LitIsCompl(pLits[k])) )
1514  {
1515  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1516  {
1517  assert( Type == IF_DSD_AND || !Abc_LitIsCompl(iFanin) );
1518  pChildren[nChildren] = iFanin;
1519  pBegEnd[nChildren++] = (nSSize << 16) | (nSSize + If_DsdVecLitSuppSize(&p->vObjs, iFanin));
1520  nSSize += If_DsdVecLitSuppSize(&p->vObjs, iFanin);
1521  }
1522  }
1523  else
1524  {
1525  pChildren[nChildren] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1526  pBegEnd[nChildren++] = (nSSize << 16) | (nSSize + If_DsdObjSuppSize(pObj));
1527  nSSize += If_DsdObjSuppSize(pObj);
1528  }
1529  pPermStart += If_DsdObjSuppSize(pObj);
1530  }
1531  If_DsdObjSort( p, &p->vObjs, pChildren, nChildren, pBegEnd );
1532  // create permutation
1533  for ( j = i = 0; i < nChildren; i++ )
1534  for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
1535  pPermNew[j++] = pPerm[k];
1536  assert( j == nSSize );
1537  for ( j = 0; j < nSSize; j++ )
1538  pPerm[j] = pPermNew[j];
1539  }
1540  else if ( Type == IF_DSD_MUX )
1541  {
1542  int RetValue;
1543  assert( nLits == 3 );
1544  for ( k = 0; k < nLits; k++ )
1545  {
1546  pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1547  pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1548  pPermStart += pFanin->nSupp;
1549  }
1550  RetValue = If_DsdObjCompare( p, &p->vObjs, pLits[1], pLits[2] );
1551  if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) )
1552  {
1553  int nSupp0 = If_DsdVecLitSuppSize( &p->vObjs, pLits[0] );
1554  int nSupp1 = If_DsdVecLitSuppSize( &p->vObjs, pLits[1] );
1555  int nSupp2 = If_DsdVecLitSuppSize( &p->vObjs, pLits[2] );
1556  pLits[0] = Abc_LitNot(pLits[0]);
1557  ABC_SWAP( int, pLits[1], pLits[2] );
1558  for ( j = k = 0; k < nSupp0; k++ )
1559  pPermNew[j++] = pPerm[k];
1560  for ( k = 0; k < nSupp2; k++ )
1561  pPermNew[j++] = pPerm[nSupp0 + nSupp1 + k];
1562  for ( k = 0; k < nSupp1; k++ )
1563  pPermNew[j++] = pPerm[nSupp0 + k];
1564  for ( j = 0; j < nSupp0 + nSupp1 + nSupp2; j++ )
1565  pPerm[j] = pPermNew[j];
1566  }
1567  if ( Abc_LitIsCompl(pLits[1]) )
1568  {
1569  pLits[1] = Abc_LitNot(pLits[1]);
1570  pLits[2] = Abc_LitNot(pLits[2]);
1571  fCompl ^= 1;
1572  }
1573  pPermStart = pPerm;
1574  for ( k = 0; k < nLits; k++ )
1575  {
1576  pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1577  pChildren[nChildren++] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1578  pPermStart += pFanin->nSupp;
1579  }
1580  }
1581  else if ( Type == IF_DSD_PRIME )
1582  {
1583  char pCanonPerm[DAU_MAX_VAR];
1584  int i, uCanonPhase, pFirsts[DAU_MAX_VAR];
1585  uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm );
1586  fCompl = ((uCanonPhase >> nLits) & 1);
1587  nSSize = If_DsdManComputeFirstArray( p, pLits, nLits, pFirsts );
1588  for ( j = i = 0; i < nLits; i++ )
1589  {
1590  int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) );
1591  pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLitNew) );
1592  pPermStart = pPerm + pFirsts[(int)pCanonPerm[i]];
1593  pChildren[nChildren++] = Abc_LitNotCond( iLitNew, If_DsdManPushInv(p, iLitNew, pPermStart) );
1594  for ( k = 0; k < (int)pFanin->nSupp; k++ )
1595  pPermNew[j++] = pPermStart[k];
1596  }
1597  assert( j == nSSize );
1598  for ( j = 0; j < nSSize; j++ )
1599  pPerm[j] = pPermNew[j];
1600  Abc_TtStretch6( pTruth, nLits, p->nVars );
1601  }
1602  else assert( 0 );
1603  // create new graph
1604  Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, pTruth );
1605  return Abc_Var2Lit( Id, fCompl );
1606 }
1607 
1608 /**Function*************************************************************
1609 
1610  Synopsis [Creating DSD network from SOP.]
1611 
1612  Description []
1613 
1614  SideEffects []
1615 
1616  SeeAlso []
1617 
1618 ***********************************************************************/
1619 static inline void If_DsdMergeMatches( char * pDsd, int * pMatches )
1620 {
1621  int pNested[DAU_MAX_VAR];
1622  int i, nNested = 0;
1623  for ( i = 0; pDsd[i]; i++ )
1624  {
1625  pMatches[i] = 0;
1626  if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
1627  pNested[nNested++] = i;
1628  else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
1629  pMatches[pNested[--nNested]] = i;
1630  assert( nNested < DAU_MAX_VAR );
1631  }
1632  assert( nNested == 0 );
1633 }
1634 int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm, int * pnSupp )
1635 {
1636  unsigned char * pPermStart = pPerm + *pnSupp;
1637  int iRes = -1, fCompl = 0;
1638  if ( **p == '!' )
1639  {
1640  fCompl = 1;
1641  (*p)++;
1642  }
1643  if ( **p >= 'a' && **p <= 'z' ) // var
1644  {
1645  pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
1646  return 2;
1647  }
1648  if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
1649  {
1650  int Type, nLits = 0, pLits[DAU_MAX_VAR];
1651  char * q = pStr + pMatches[ *p - pStr ];
1652  if ( **p == '(' )
1653  Type = DAU_DSD_AND;
1654  else if ( **p == '[' )
1655  Type = DAU_DSD_XOR;
1656  else if ( **p == '<' )
1657  Type = DAU_DSD_MUX;
1658  else if ( **p == '{' )
1659  Type = DAU_DSD_PRIME;
1660  else assert( 0 );
1661  assert( *q == **p + 1 + (**p != '(') );
1662  for ( (*p)++; *p < q; (*p)++ )
1663  pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
1664  assert( *p == q );
1665  iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth );
1666  return Abc_LitNotCond( iRes, fCompl );
1667  }
1668  if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
1669  {
1670  word pFunc[DAU_MAX_WORD];
1671  int nLits = 0, pLits[DAU_MAX_VAR];
1672  char * q;
1673  int i, nVarsF = Abc_TtReadHex( pFunc, *p );
1674  *p += Abc_TtHexDigitNum( nVarsF );
1675  q = pStr + pMatches[ *p - pStr ];
1676  assert( **p == '{' && *q == '}' );
1677  for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
1678  pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
1679  assert( i == nVarsF );
1680  assert( *p == q );
1681  iRes = If_DsdManOperation( pMan, DAU_DSD_PRIME, pLits, nLits, pPermStart, pFunc );
1682  return Abc_LitNotCond( iRes, fCompl );
1683  }
1684  assert( 0 );
1685  return -1;
1686 }
1687 int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm, int * pnSupp )
1688 {
1689  int iRes = -1, fCompl = 0;
1690  if ( *pDsd == '!' )
1691  pDsd++, fCompl = 1;
1692  if ( Dau_DsdIsConst0(pDsd) )
1693  iRes = 0;
1694  else if ( Dau_DsdIsConst1(pDsd) )
1695  iRes = 1;
1696  else if ( Dau_DsdIsVar(pDsd) )
1697  {
1698  pPerm[(*pnSupp)++] = Dau_DsdReadVar(pDsd);
1699  iRes = 2;
1700  }
1701  else
1702  {
1703  int pMatches[DAU_MAX_STR];
1704  If_DsdMergeMatches( pDsd, pMatches );
1705  iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm, pnSupp );
1706  }
1707  return Abc_LitNotCond( iRes, fCompl );
1708 }
1709 
1710 /**Function*************************************************************
1711 
1712  Synopsis [Returns 1 if XY-decomposability holds to this LUT size.]
1713 
1714  Description []
1715 
1716  SideEffects []
1717 
1718  SeeAlso []
1719 
1720 ***********************************************************************/
1721 // create signature of the support of the node
1722 unsigned If_DsdSign_rec( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pnSupp )
1723 {
1724  unsigned uSign = 0; int i;
1725  If_DsdObj_t * pFanin;
1726  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1727  return (1 << (2*(*pnSupp)++));
1728  If_DsdObjForEachFanin( &p->vObjs, pObj, pFanin, i )
1729  uSign |= If_DsdSign_rec( p, pFanin, pnSupp );
1730  return uSign;
1731 }
1732 unsigned If_DsdSign( If_DsdMan_t * p, If_DsdObj_t * pObj, int iFan, int iFirst, int fShared )
1733 {
1734  If_DsdObj_t * pFanin = If_DsdObjFanin( &p->vObjs, pObj, iFan );
1735  unsigned uSign = If_DsdSign_rec( p, pFanin, &iFirst );
1736  return fShared ? (uSign << 1) | uSign : uSign;
1737 }
1738 // collect supports of the node
1739 void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
1740 {
1741  If_DsdObj_t * pFanin; int i;
1742  If_DsdObjForEachFanin( &p->vObjs, pObj, pFanin, i )
1743  pSSizes[i] = If_DsdObjSuppSize(pFanin);
1744 }
1745 // checks if there is a way to package some fanins
1746 unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1747 {
1748  int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
1749  int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
1750  unsigned uRes;
1751  assert( pObj->nFans > 2 );
1752  assert( If_DsdObjSuppSize(pObj) > LutSize );
1753  If_DsdManGetSuppSizes( p, pObj, pSSizes );
1754  LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
1755  assert( LimitOut < LutSize );
1756  for ( i[0] = 0; i[0] < nFans; i[0]++ )
1757  for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1758  {
1759  SizeIn = pSSizes[i[0]] + pSSizes[i[1]];
1760  SizeOut = pObj->nSupp - SizeIn;
1761  if ( SizeIn > LutSize || SizeOut > LimitOut )
1762  continue;
1763  if ( !fDerive )
1764  return ~0;
1765  If_DsdManComputeFirst( p, pObj, pFirsts );
1766  uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1767  If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0);
1768  if ( uRes & uMaskNot )
1769  continue;
1770  return uRes;
1771  }
1772  if ( pObj->nFans == 3 )
1773  return 0;
1774  for ( i[0] = 0; i[0] < nFans; i[0]++ )
1775  for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1776  for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
1777  {
1778  SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]];
1779  SizeOut = pObj->nSupp - SizeIn;
1780  if ( SizeIn > LutSize || SizeOut > LimitOut )
1781  continue;
1782  if ( !fDerive )
1783  return ~0;
1784  If_DsdManComputeFirst( p, pObj, pFirsts );
1785  uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1786  If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
1787  If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0);
1788  if ( uRes & uMaskNot )
1789  continue;
1790  return uRes;
1791  }
1792  if ( pObj->nFans == 4 )
1793  return 0;
1794  for ( i[0] = 0; i[0] < nFans; i[0]++ )
1795  for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1796  for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
1797  for ( i[3] = i[2]+1; i[3] < nFans; i[3]++ )
1798  {
1799  SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]] + pSSizes[i[3]];
1800  SizeOut = pObj->nSupp - SizeIn;
1801  if ( SizeIn > LutSize || SizeOut > LimitOut )
1802  continue;
1803  if ( !fDerive )
1804  return ~0;
1805  If_DsdManComputeFirst( p, pObj, pFirsts );
1806  uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1807  If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
1808  If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0) |
1809  If_DsdSign(p, pObj, i[3], iFirst + pFirsts[i[3]], 0);
1810  if ( uRes & uMaskNot )
1811  continue;
1812  return uRes;
1813  }
1814  return 0;
1815 }
1816 // checks if there is a way to package some fanins
1817 unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1818 {
1819  int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
1820  unsigned uRes;
1821  assert( If_DsdObjFaninNum(pObj) == 3 );
1822  assert( If_DsdObjSuppSize(pObj) > LutSize );
1823  If_DsdManGetSuppSizes( p, pObj, pSSizes );
1824  LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
1825  assert( LimitOut < LutSize );
1826  // first input
1827  SizeIn = pSSizes[0] + pSSizes[1];
1828  SizeOut = pSSizes[0] + pSSizes[2] + 1;
1829  if ( SizeIn <= LutSize && SizeOut <= LimitOut )
1830  {
1831  if ( !fDerive )
1832  return ~0;
1833  If_DsdManComputeFirst( p, pObj, pFirsts );
1834  uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0);
1835  if ( (uRes & uMaskNot) == 0 )
1836  return uRes;
1837  }
1838  // second input
1839  SizeIn = pSSizes[0] + pSSizes[2];
1840  SizeOut = pSSizes[0] + pSSizes[1] + 1;
1841  if ( SizeIn <= LutSize && SizeOut <= LimitOut )
1842  {
1843  if ( !fDerive )
1844  return ~0;
1845  If_DsdManComputeFirst( p, pObj, pFirsts );
1846  uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0);
1847  if ( (uRes & uMaskNot) == 0 )
1848  return uRes;
1849  }
1850  return 0;
1851 }
1852 // checks if there is a way to package some fanins
1853 unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1854 {
1855  int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
1856  int truthId = If_DsdObjTruthId(p, pObj);
1857  int nFans = If_DsdObjFaninNum(pObj);
1858  Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs[pObj->nFans], truthId);
1859 if ( fVerbose )
1860 printf( "\n" );
1861 if ( fVerbose )
1862 Dau_DecPrintSets( vSets, nFans );
1863  assert( If_DsdObjFaninNum(pObj) > 2 );
1864  assert( If_DsdObjSuppSize(pObj) > LutSize );
1865  If_DsdManGetSuppSizes( p, pObj, pSSizes );
1866  LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
1867  assert( LimitOut < LutSize );
1868  Vec_IntForEachEntry( vSets, set, i )
1869  {
1870  SizeIn = SizeOut = 0;
1871  for ( v = 0; v < nFans; v++ )
1872  {
1873  int Value = ((set >> (v << 1)) & 3);
1874  if ( Value == 0 )
1875  SizeOut += pSSizes[v];
1876  else if ( Value == 1 )
1877  SizeIn += pSSizes[v];
1878  else if ( Value == 3 )
1879  {
1880  SizeIn += pSSizes[v];
1881  SizeOut += pSSizes[v];
1882  }
1883  else assert( 0 );
1884  if ( SizeIn > LutSize || SizeOut > LimitOut )
1885  break;
1886  }
1887  if ( v == nFans )
1888  {
1889  unsigned uRes = 0;
1890  if ( !fDerive )
1891  return ~0;
1892  If_DsdManComputeFirst( p, pObj, pFirsts );
1893  for ( v = 0; v < nFans; v++ )
1894  {
1895  int Value = ((set >> (v << 1)) & 3);
1896  if ( Value == 0 )
1897  {}
1898  else if ( Value == 1 )
1899  uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0);
1900  else if ( Value == 3 )
1901  uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1);
1902  else assert( 0 );
1903  }
1904  if ( uRes & uMaskNot )
1905  continue;
1906  return uRes;
1907  }
1908  }
1909  return 0;
1910 }
1911 unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fVerbose )
1912 {
1913  If_DsdObj_t * pObj, * pTemp;
1914  int i, Mask, iFirst;
1915  unsigned uRes;
1916  pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1917  if ( fVerbose )
1918  If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
1919  if ( If_DsdObjSuppSize(pObj) <= LutSize )
1920  {
1921  if ( fVerbose )
1922  printf( " Trivial\n" );
1923  return ~0;
1924  }
1925  If_DsdManCollect( p, pObj->Id, p->vTemp1, p->vTemp2 );
1926  If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1927  if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
1928  {
1929  if ( fVerbose )
1930  printf( " Dec using node " );
1931  if ( fVerbose )
1932  If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
1933  iFirst = Vec_IntEntry(p->vTemp2, i);
1934  uRes = If_DsdSign_rec(p, pTemp, &iFirst);
1935  if ( uRes & uMaskNot )
1936  continue;
1937  return uRes;
1938  }
1939  If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1940  if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
1941  {
1942  if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
1943  {
1944  if ( fVerbose )
1945  printf( " " );
1946  if ( fVerbose )
1947  Abc_TtPrintBinary( (word *)&Mask, 4 );
1948  if ( fVerbose )
1949  printf( " Using multi-input AND/XOR node\n" );
1950  return Mask;
1951  }
1952  }
1953  If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1954  if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
1955  {
1956  if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
1957  {
1958  if ( fVerbose )
1959  printf( " " );
1960  if ( fVerbose )
1961  Abc_TtPrintBinary( (word *)&Mask, 4 );
1962  if ( fVerbose )
1963  printf( " Using multi-input MUX node\n" );
1964  return Mask;
1965  }
1966  }
1967  If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1968  if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
1969  {
1970  if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
1971  {
1972  if ( fVerbose )
1973  printf( " " );
1974  if ( fVerbose )
1975  Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
1976  if ( fVerbose )
1977  printf( " Using prime node\n" );
1978  return Mask;
1979  }
1980  }
1981  if ( fVerbose )
1982  printf( " UNDEC\n" );
1983 // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
1984  return 0;
1985 }
1986 unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose )
1987 {
1988  unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, uMaskNot, fVerbose );
1989  if ( uSet == 0 && fHighEffort )
1990  {
1991 // abctime clk = Abc_Clock();
1992  int nVars = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
1993  word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
1994  uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
1995  if ( uSet )
1996  {
1997 // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
1998 // Dau_DecPrintSet( uSet, nVars, 1 );
1999  }
2000 // p->timeCheck2 += Abc_Clock() - clk;
2001  }
2002  return uSet;
2003 }
2004 
2005 /**Function*************************************************************
2006 
2007  Synopsis [Checks existence of decomposition.]
2008 
2009  Description []
2010 
2011  SideEffects []
2012 
2013  SeeAlso []
2014 
2015 ***********************************************************************/
2016 unsigned If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
2017 {
2018  return ~0;
2019 }
2020 
2021 /**Function*************************************************************
2022 
2023  Synopsis [Add the function to the DSD manager.]
2024 
2025  Description []
2026 
2027  SideEffects []
2028 
2029  SeeAlso []
2030 
2031 ***********************************************************************/
2032 int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct )
2033 {
2034  word pCopy[DAU_MAX_WORD], * pRes;
2035  char pDsd[DAU_MAX_STR];
2036  int iDsd, nSizeNonDec, nSupp = 0;
2037  int nWords = Abc_TtWordNum(nLeaves);
2038 // abctime clk = 0;
2039  assert( nLeaves <= DAU_MAX_VAR );
2040  Abc_TtCopy( pCopy, pTruth, nWords, 0 );
2041 //clk = Abc_Clock();
2042  nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
2043 //p->timeDsd += Abc_Clock() - clk;
2044  if ( nSizeNonDec > 0 )
2045  Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
2046  memset( pPerm, 0xFF, nLeaves );
2047 //clk = Abc_Clock();
2048  iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
2049 //p->timeCanon += Abc_Clock() - clk;
2050  assert( nSupp == nLeaves );
2051  // verify the result
2052 //clk = Abc_Clock();
2053  pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
2054 //p->timeVerify += Abc_Clock() - clk;
2055  if ( !Abc_TtEqual(pRes, pTruth, nWords) )
2056  {
2057 // If_DsdManPrint( p, NULL );
2058  printf( "\n" );
2059  printf( "Verification failed!\n" );
2060  printf( "%s\n", pDsd );
2061  Dau_DsdPrintFromTruth( pTruth, nLeaves );
2062  Dau_DsdPrintFromTruth( pRes, nLeaves );
2063  If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
2064  printf( "\n" );
2065  }
2066  If_DsdVecObjIncRef( &p->vObjs, Abc_Lit2Var(iDsd) );
2067  assert( If_DsdVecLitSuppSize(&p->vObjs, iDsd) == nLeaves );
2068  return iDsd;
2069 }
2070 
2071 /**Function*************************************************************
2072 
2073  Synopsis [Checks existence of decomposition.]
2074 
2075  Description []
2076 
2077  SideEffects []
2078 
2079  SeeAlso []
2080 
2081 ***********************************************************************/
2082 void If_DsdManTest()
2083 {
2084  Vec_Int_t * vSets;
2085  word t = 0x5277;
2086  t = Abc_Tt6Stretch( t, 4 );
2087 // word t = 0xD9D900D900D900001010001000100000;
2088  vSets = Dau_DecFindSets( &t, 6 );
2089  Vec_IntFree( vSets );
2090 }
2091 
2092 
2093 /**Function*************************************************************
2094 
2095  Synopsis [Compute pin delays.]
2096 
2097  Description []
2098 
2099  SideEffects []
2100 
2101  SeeAlso []
2102 
2103 ***********************************************************************/
2104 int If_CutDsdBalancePinDelays_rec( If_DsdMan_t * p, int Id, int * pTimes, word * pRes, int * pnSupp, int nSuppAll, char * pPermLits )
2105 {
2106  If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
2107  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
2108  {
2109  int iCutVar = Abc_Lit2Var(pPermLits[(*pnSupp)++]);
2110  *pRes = If_CutPinDelayInit(iCutVar);
2111  return pTimes[iCutVar];
2112  }
2113  if ( If_DsdObjType(pObj) == IF_DSD_MUX )
2114  {
2115  word pFaninRes[3], Res0, Res1;
2116  int i, iFanin, Delays[3];
2117  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2118  Delays[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2119  Res0 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[1], nSuppAll, 1 );
2120  Res1 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[2], nSuppAll, 1 );
2121  *pRes = If_CutPinDelayMax( Res0, Res1, nSuppAll, 1 );
2122  return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
2123  }
2124  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
2125  {
2126  word pFaninRes[IF_MAX_FUNC_LUTSIZE];
2127  int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE];
2128  Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
2129  assert( Vec_IntSize(vCover) > 0 );
2130  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2131  Delays[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2132  return If_CutSopBalancePinDelaysInt( vCover, Delays, pFaninRes, nSuppAll, pRes );
2133  }
2134  assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
2135  {
2136  word pFaninRes[IF_MAX_FUNC_LUTSIZE];
2137  int i, iFanin, Delay, Result = 0;
2138  int fXor = 0;//(If_DsdObjType(pObj) == IF_DSD_XOR);
2139  int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE];
2140  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2141  {
2142  Delay = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2143  Result = If_LogCounterPinDelays( pCounter, &nCounter, pFaninRes, Delay, pFaninRes[i], nSuppAll, fXor );
2144  }
2145  assert( nCounter > 0 );
2146  if ( fXor )
2147  Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
2148  *pRes = If_LogPinDelaysMulti( pFaninRes, nCounter, nSuppAll, fXor );
2149  return Result;
2150  }
2151 }
2152 int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
2153 {
2154  if ( pCut->nLeaves == 0 ) // const
2155  return 0;
2156  if ( pCut->nLeaves == 1 ) // variable
2157  {
2158  pPerm[0] = 0;
2159  return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
2160  }
2161  else
2162  {
2163  word Result = 0;
2164  int i, Delay, nSupp = 0, pTimes[IF_MAX_FUNC_LUTSIZE];
2165  for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2166  pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay;
2167  Delay = If_CutDsdBalancePinDelays_rec( p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)), pTimes, &Result, &nSupp, If_CutLeaveNum(pCut), If_CutDsdPerm(p, pCut) );
2168  assert( nSupp == If_CutLeaveNum(pCut) );
2169  If_CutPinDelayTranslate( Result, If_CutLeaveNum(pCut), pPerm );
2170  return Delay;
2171  }
2172 }
2173 
2174 
2175 /**Function*************************************************************
2176 
2177  Synopsis []
2178 
2179  Description []
2180 
2181  SideEffects []
2182 
2183  SeeAlso []
2184 
2185 ***********************************************************************/
2186 int If_CutDsdPermLitMax( char * pPermLits, int nVars, int iVar )
2187 {
2188  int i;
2189  assert( iVar >= 0 && iVar < nVars );
2190  for ( i = 0; i < nVars; i++ )
2191  if ( iVar == Abc_Lit2Var((int)pPermLits[i]) )
2192  return i;
2193  assert( 0 );
2194  return -1;
2195 }
2196 
2197 /**Function*************************************************************
2198 
2199  Synopsis [Evaluate delay using DSD balancing.]
2200 
2201  Description []
2202 
2203  SideEffects []
2204 
2205  SeeAlso []
2206 
2207 ***********************************************************************/
2208 int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSupp, Vec_Int_t * vAig, int * piLit, int nSuppAll, int * pArea, char * pPermLits )
2209 {
2210  If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
2211  if ( If_DsdObjType(pObj) == IF_DSD_VAR )
2212  {
2213  int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] );
2214  if ( vAig )
2215  *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) );
2216  (*pnSupp)++;
2217  return pTimes[iCutVar];
2218  }
2219  if ( If_DsdObjType(pObj) == IF_DSD_MUX )
2220  {
2221  int i, iFanin, Delays[3], pFaninLits[3];
2222  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2223  {
2224  Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2225  if ( Delays[i] == -1 )
2226  return -1;
2227  pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2228  }
2229  if ( vAig )
2230  *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll );
2231  else
2232  *pArea += 3;
2233  return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
2234  }
2235  if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
2236  {
2237  int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
2238  Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
2239  if ( Vec_IntSize(vCover) == 0 )
2240  return -1;
2241  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2242  {
2243  Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2244  if ( Delays[i] == -1 )
2245  return -1;
2246  pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2247  }
2248  return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea );
2249  }
2250  assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
2251  {
2252  int i, iFanin, Delay, Result = 0;
2253  int fXor = 0;//(If_DsdObjType(pObj) == IF_DSD_XOR);
2254  int fXorFunc = (If_DsdObjType(pObj) == IF_DSD_XOR);
2255  int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
2256  If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2257  {
2258  Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2259  if ( Delay == -1 )
2260  return -1;
2261  pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2262  Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, pFaninLits[i], vAig, nSuppAll, fXor, fXorFunc );
2263  }
2264  assert( nCounter > 0 );
2265  if ( fXor )
2266  Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
2267  if ( vAig )
2268  *piLit = If_LogCreateAndXorMulti( vAig, pFaninLits, nCounter, nSuppAll, fXorFunc );
2269  else
2270  *pArea += (pObj->nFans - 1) * (1 + 2 * fXor);
2271  return Result;
2272  }
2273 }
2274 int If_CutDsdBalanceEvalInt( If_DsdMan_t * p, int iDsd, int * pTimes, Vec_Int_t * vAig, int * pArea, char * pPermLits )
2275 {
2276  int nSupp = 0, iLit = 0;
2277  int nSuppAll = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
2278  int Res = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iDsd), pTimes, &nSupp, vAig, &iLit, nSuppAll, pArea, pPermLits );
2279  if ( Res == -1 )
2280  return -1;
2281  assert( nSupp == nSuppAll );
2282  assert( vAig == NULL || Abc_Lit2Var(iLit) == nSupp + Abc_Lit2Var(Vec_IntSize(vAig)) - 1 );
2283  if ( vAig )
2284  Vec_IntPush( vAig, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(iDsd) );
2285  assert( vAig == NULL || (Vec_IntSize(vAig) & 1) );
2286  return Res;
2287 }
2288 int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
2289 {
2290  int fUseCofs = 0;
2291  pCut->fUser = 1;
2292  if ( vAig )
2293  Vec_IntClear( vAig );
2294  if ( pCut->nLeaves == 0 ) // const
2295  {
2296  assert( Abc_Lit2Var(If_CutDsdLit(p, pCut)) == 0 );
2297  if ( vAig )
2298  Vec_IntPush( vAig, Abc_LitIsCompl(If_CutDsdLit(p, pCut)) );
2299  pCut->Cost = 0;
2300  return 0;
2301  }
2302  if ( pCut->nLeaves == 1 ) // variable
2303  {
2304  assert( Abc_Lit2Var(If_CutDsdLit(p, pCut)) == 1 );
2305  if ( vAig )
2306  Vec_IntPush( vAig, 0 );
2307  if ( vAig )
2308  Vec_IntPush( vAig, Abc_LitIsCompl(If_CutDsdLit(p, pCut)) );
2309  pCut->Cost = 0;
2310  return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
2311  }
2312  else
2313  {
2314  int fVerbose = 0;
2315  int i, pTimes[IF_MAX_FUNC_LUTSIZE];
2316  int Delay, Area = 0;
2317  char * pPermLits = If_CutDsdPerm(p, pCut);
2318  for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2319  pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay;
2320  Delay = If_CutDsdBalanceEvalInt( p->pIfDsdMan, Abc_LitNotCond(If_CutDsdLit(p, pCut), pCut->fCompl), pTimes, vAig, &Area, If_CutDsdPerm(p, pCut) );
2321  pCut->Cost = Area;
2322  // try cofactoring
2323  if ( fUseCofs )
2324  {
2325  // count how many times the max one appears
2326  int iMax = 0, nCountMax = 1;
2327  for ( i = 1; i < If_CutLeaveNum(pCut); i++ )
2328  if ( pTimes[i] > pTimes[iMax] )
2329  iMax = i, nCountMax = 1;
2330  else if ( pTimes[i] == pTimes[iMax] )
2331  nCountMax++;
2332  // decide when to try the decomposition
2333  if ( nCountMax == 1 && pTimes[iMax] + 2 < Delay && If_DsdManCheckNonTriv( p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)),
2334  If_CutLeaveNum(pCut), If_CutDsdPermLitMax(pPermLits, If_CutLeaveNum(pCut), iMax)) )
2335  {
2336 // fVerbose = 1;
2337  Delay = pTimes[iMax] + 2;
2338  }
2339  }
2340  // report the result
2341  if ( fVerbose )
2342  {
2343 /*
2344  int Max = 0, Two = 0;
2345  for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2346  Max = Abc_MaxInt( Max, pTimes[i] );
2347  for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2348  if ( pTimes[i] != Max )
2349  Two = Abc_MaxInt( Two, pTimes[i] );
2350  if ( Two + 2 < Max && Max + 3 < Delay )
2351 */
2352  {
2353  for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2354  printf( "%3d ", pTimes[Abc_Lit2Var(pPermLits[i])] );
2355  for ( ; i < p->pPars->nLutSize; i++ )
2356  printf( " " );
2357  printf( "-> %3d ", Delay );
2358  If_DsdManPrintOne( stdout, p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)), NULL, 0 );
2359  printf( "\n" );
2360  }
2361  }
2362  return Delay;
2363  }
2364 }
2365 
2366 /**Function*************************************************************
2367 
2368  Synopsis []
2369 
2370  Description []
2371 
2372  SideEffects []
2373 
2374  SeeAlso []
2375 
2376 ***********************************************************************/
2377 void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose )
2378 {
2379  ProgressBar * pProgress = NULL;
2380  sat_solver * pSat = NULL;
2381  If_DsdObj_t * pObj;
2382  Vec_Int_t * vLits;
2383  int i, Value, nVars;
2384  word * pTruth;
2385  if ( !fAdd || !LutSize )
2386  If_DsdVecForEachObj( &p->vObjs, pObj, i )
2387  pObj->fMark = 0;
2388  if ( LutSize == 0 )
2389  return;
2390  vLits = Vec_IntAlloc( 1000 );
2391  pSat = (sat_solver *)If_ManSatBuildXY( LutSize );
2392  pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2393  If_DsdVecForEachObj( &p->vObjs, pObj, i )
2394  {
2395  Extra_ProgressBarUpdate( pProgress, i, NULL );
2396  nVars = If_DsdObjSuppSize(pObj);
2397  if ( nVars <= LutSize )
2398  continue;
2399  if ( fAdd && !pObj->fMark )
2400  continue;
2401  pObj->fMark = 0;
2402  if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0, 0, 0) )
2403  continue;
2404  if ( fFast )
2405  Value = 0;
2406  else
2407  {
2408  pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2409  Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
2410  }
2411  if ( Value )
2412  continue;
2413  If_DsdVecObjSetMark( &p->vObjs, i );
2414  }
2415  Extra_ProgressBarStop( pProgress );
2416  If_ManSatUnbuild( pSat );
2417  Vec_IntFree( vLits );
2418  if ( fVerbose )
2419  If_DsdManPrintDistrib( p );
2420 }
2421 
2422 
2423 
2424 /**Function*************************************************************
2425 
2426  Synopsis []
2427 
2428  Description []
2429 
2430  SideEffects []
2431 
2432  SeeAlso []
2433 
2434 ***********************************************************************/
2435 void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose )
2436 {
2437  int fVeryVerbose = 0;
2438  ProgressBar * pProgress = NULL;
2439  If_DsdObj_t * pObj;
2440  word * pTruth, Perm;
2441  int i, nVars, Value, LutSize;
2442  abctime clk = Abc_Clock();
2443  // parse the structure
2444  Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct );
2445  if ( pNtk == NULL )
2446  return;
2447  if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
2448  {
2449  printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2450  ABC_FREE( pNtk );
2451  return;
2452  }
2453  ABC_FREE( p->pCellStr );
2454  p->pCellStr = Abc_UtilStrsav( pStruct );
2455  if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
2456  printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2457  LutSize = Ifn_NtkLutSizeMax(pNtk);
2458  // print
2459  if ( fVerbose )
2460  {
2461  printf( "Considering programmable cell: " );
2462  Ifn_NtkPrint( pNtk );
2463  printf( "Largest LUT size = %d.\n", LutSize );
2464  }
2465  if ( p->nObjsPrev > 0 )
2466  printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2467  // clean the attributes
2468  If_DsdVecForEachObj( &p->vObjs, pObj, i )
2469  if ( i >= p->nObjsPrev )
2470  pObj->fMark = 0;
2471  if ( p->vPerms == NULL )
2472  p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
2473  else
2474  Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
2475  pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2476  If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
2477  {
2478  if ( (i & 0xFF) == 0 )
2479  Extra_ProgressBarUpdate( pProgress, i, NULL );
2480  nVars = If_DsdObjSuppSize(pObj);
2481  if ( nVars <= LutSize )
2482  continue;
2483  pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2484  if ( fVeryVerbose )
2485  Dau_DsdPrintFromTruth( pTruth, nVars );
2486  if ( fVerbose )
2487  printf( "%6d : %2d ", i, nVars );
2488  Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, &Perm );
2489  if ( fVeryVerbose )
2490  printf( "\n" );
2491  if ( Value == 0 )
2492  If_DsdVecObjSetMark( &p->vObjs, i );
2493  else
2494  Vec_WrdWriteEntry( p->vPerms, i, Perm );
2495  }
2496  p->nObjsPrev = 0;
2497  p->LutSize = 0;
2498  Extra_ProgressBarStop( pProgress );
2499  printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2500  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2501  if ( fVeryVerbose )
2502  If_DsdManPrintDistrib( p );
2503  ABC_FREE( pNtk );
2504 }
2505 
2506 
2507 /**Function*************************************************************
2508 
2509  Synopsis []
2510 
2511  Description []
2512 
2513  SideEffects []
2514 
2515  SeeAlso []
2516 
2517 ***********************************************************************/
2518 #ifndef ABC_USE_PTHREADS
2519 void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose )
2520 {
2521  Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
2522 }
2523 #else // pthreads are used
2524 
2525 
2526 #define PAR_THR_MAX 100
2527 typedef struct Ifn_ThData_t_
2528 {
2529  Ifn_Ntk_t * pNtk; // network
2530  word pTruth[DAU_MAX_WORD];
2531  int nVars; // support
2532  int Id; // object
2533  int nConfls; // conflicts
2534  int Result; // result
2535  int Status; // state
2536  word Perm; // permutation
2537  abctime clkUsed; // total runtime
2538 } Ifn_ThData_t;
2539 void * Ifn_WorkerThread( void * pArg )
2540 {
2541  Ifn_ThData_t * pThData = (Ifn_ThData_t *)pArg;
2542  volatile int * pPlace = &pThData->Status;
2543  abctime clk;
2544  while ( 1 )
2545  {
2546  while ( *pPlace == 0 );
2547  assert( pThData->Status == 1 );
2548  if ( pThData->Id == -1 )
2549  {
2550  pthread_exit( NULL );
2551  assert( 0 );
2552  return NULL;
2553  }
2554  clk = Abc_Clock();
2555  pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, &pThData->Perm );
2556  pThData->clkUsed += Abc_Clock() - clk;
2557  pThData->Status = 0;
2558 // printf( "Finished object %d\n", pThData->Id );
2559  }
2560  assert( 0 );
2561  return NULL;
2562 }
2563 void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose )
2564 {
2565  int fVeryVerbose = 0;
2566  ProgressBar * pProgress = NULL;
2567  int i, k, nVars, LutSize;
2568  abctime clk = Abc_Clock();
2569  Ifn_Ntk_t * pNtk;
2570  If_DsdObj_t * pObj;
2571  if ( nProcs == 1 )
2572  {
2573  Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
2574  return;
2575  }
2576  if ( nProcs > PAR_THR_MAX )
2577  {
2578  printf( "The number of processes (%d) exceeds the precompiled limit (%d).\n", nProcs, PAR_THR_MAX );
2579  return;
2580  }
2581  // parse the structure
2582  pNtk = Ifn_NtkParse( pStruct );
2583  if ( pNtk == NULL )
2584  return;
2585  if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
2586  {
2587  printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2588  ABC_FREE( pNtk );
2589  return;
2590  }
2591  ABC_FREE( p->pCellStr );
2592  p->pCellStr = Abc_UtilStrsav( pStruct );
2593  if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
2594  printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2595  // check the largest LUT
2596  LutSize = Ifn_NtkLutSizeMax(pNtk);
2597  if ( fVerbose )
2598  {
2599  printf( "Considering programmable cell: " );
2600  Ifn_NtkPrint( pNtk );
2601  printf( "Largest LUT size = %d.\n", LutSize );
2602  }
2603  ABC_FREE( pNtk );
2604  if ( p->nObjsPrev > 0 )
2605  printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2606  // clean the attributes
2607  If_DsdVecForEachObj( &p->vObjs, pObj, i )
2608  if ( i >= p->nObjsPrev )
2609  pObj->fMark = 0;
2610  if ( p->vPerms == NULL )
2611  p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
2612  else
2613  Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
2614  pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2615 
2616  // perform concurrent solving
2617  {
2618  pthread_t WorkerThread[PAR_THR_MAX];
2619  Ifn_ThData_t ThData[PAR_THR_MAX];
2620  abctime clk, clkUsed = 0;
2621  int status, fRunning = 1, iCurrentObj = p->nObjsPrev;
2622  // start the threads
2623  for ( i = 0; i < nProcs; i++ )
2624  {
2625  ThData[i].pNtk = Ifn_NtkParse( pStruct );
2626  ThData[i].nVars = -1; // support
2627  ThData[i].Id = -1; // object
2628  ThData[i].nConfls = nConfls; // conflicts
2629  ThData[i].Result = -1; // result
2630  ThData[i].Status = 0; // state
2631  ThData[i].clkUsed = 0; // total runtime
2632  status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 );
2633  }
2634  // run the threads
2635  while ( fRunning || iCurrentObj < Vec_PtrSize(&p->vObjs) )
2636  {
2637  for ( i = 0; i < nProcs; i++ )
2638  {
2639  if ( ThData[i].Status )
2640  continue;
2641  assert( ThData[i].Status == 0 );
2642  if ( ThData[i].Id >= 0 )
2643  {
2644  //printf( "Closing obj %d with Thread %d:\n", ThData[i].Id, i );
2645  assert( ThData[i].Result == 0 || ThData[i].Result == 1 );
2646  if ( ThData[i].Result == 0 )
2647  If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
2648  else
2649  Vec_WrdWriteEntry( p->vPerms, ThData[i].Id, ThData[i].Perm );
2650  ThData[i].Id = -1;
2651  ThData[i].Result = -1;
2652  }
2653  for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ )
2654  {
2655  if ( (k & 0xFF) == 0 )
2656  Extra_ProgressBarUpdate( pProgress, k, NULL );
2657  pObj = If_DsdVecObj( &p->vObjs, k );
2658  nVars = If_DsdObjSuppSize(pObj);
2659  if ( nVars <= LutSize )
2660  continue;
2661  clk = Abc_Clock();
2662  If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth );
2663  clkUsed += Abc_Clock() - clk;
2664  ThData[i].nVars = nVars;
2665  ThData[i].Id = k;
2666  ThData[i].Result = -1;
2667  ThData[i].Status = 1;
2668  //printf( "Scheduling %d for Thread %d\n", ThData[i].Id, i );
2669  iCurrentObj = k+1;
2670  break;
2671  }
2672  }
2673  fRunning = 0;
2674  for ( i = 0; i < nProcs; i++ )
2675  if ( ThData[i].Status == 1 || (ThData[i].Status == 0 && ThData[i].Id >= 0) )
2676  fRunning = 1;
2677  //printf( "fRunning %d\n", fRunning );
2678  }
2679  // stop the threads
2680  for ( i = 0; i < nProcs; i++ )
2681  {
2682  assert( ThData[i].Status == 0 );
2683  ThData[i].Id = -1;
2684  ThData[i].Status = 1;
2685  ABC_FREE( ThData[i].pNtk );
2686  }
2687  if ( fVerbose )
2688  {
2689  printf( "Main : " );
2690  Abc_PrintTime( 1, "Time", clkUsed );
2691  for ( i = 0; i < nProcs; i++ )
2692  {
2693  printf( "Thread %d : ", i );
2694  Abc_PrintTime( 1, "Time", ThData[i].clkUsed );
2695  }
2696  }
2697  }
2698 
2699  p->nObjsPrev = 0;
2700  p->LutSize = 0;
2701  Extra_ProgressBarStop( pProgress );
2702  printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2703  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2704  if ( fVeryVerbose )
2705  If_DsdManPrintDistrib( p );
2706 }
2707 
2708 #endif // pthreads are used
2709 
2710 /**Function*************************************************************
2711 
2712  Synopsis []
2713 
2714  Description []
2715 
2716  SideEffects []
2717 
2718  SeeAlso []
2719 
2720 ***********************************************************************/
2721 void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose )
2722 {
2723  extern int Extra_ThreshCheck( word * t, int nVars, int * pW );
2724  int fVeryVerbose = 0;
2725  int pW[16];
2726  ProgressBar * pProgress = NULL;
2727  If_DsdObj_t * pObj;
2728  word * pTruth, Perm;
2729  int i, nVars, Value;
2730  abctime clk = Abc_Clock();
2731  assert( fUnate != fThresh );
2732  if ( p->nObjsPrev > 0 )
2733  printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2734  // clean the attributes
2735  If_DsdVecForEachObj( &p->vObjs, pObj, i )
2736  if ( i >= p->nObjsPrev )
2737  pObj->fMark = 0;
2738  if ( p->vPerms == NULL )
2739  p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
2740  else
2741  Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
2742  pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2743  If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
2744  {
2745  if ( (i & 0xFF) == 0 )
2746  Extra_ProgressBarUpdate( pProgress, i, NULL );
2747  nVars = If_DsdObjSuppSize(pObj);
2748  if ( nVars > 8 )
2749  continue;
2750  pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2751  if ( fVeryVerbose )
2752  Dau_DsdPrintFromTruth( pTruth, nVars );
2753  if ( fVerbose )
2754  printf( "%6d : %2d ", i, nVars );
2755  if ( fUnate )
2756  Value = Abc_TtIsUnate( pTruth, nVars );
2757  else if ( fThresh )
2758  Value = Extra_ThreshCheck( pTruth, nVars, pW );
2759  else
2760  Value = 0;
2761  Perm = 0;
2762  if ( fVeryVerbose )
2763  printf( "\n" );
2764  if ( Value )
2765  If_DsdVecObjSetMark( &p->vObjs, i );
2766  else
2767  Vec_WrdWriteEntry( p->vPerms, i, Perm );
2768  }
2769  p->nObjsPrev = 0;
2770  p->LutSize = 0;
2771  Extra_ProgressBarStop( pProgress );
2772  printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2773  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2774  if ( fVeryVerbose )
2775  If_DsdManPrintDistrib( p );
2776 }
2777 
2778 ////////////////////////////////////////////////////////////////////////
2779 /// END OF FILE ///
2780 ////////////////////////////////////////////////////////////////////////
2781 
2782 
2783 ABC_NAMESPACE_IMPL_END
2784 
memset
char * memset()
If_DsdManTune
void If_DsdManTune(If_DsdMan_t *p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose)
Definition: ifDsd.c:2377
If_DsdManSetNewAsUseless
void If_DsdManSetNewAsUseless(If_DsdMan_t *p)
Definition: ifDsd.c:193
If_DsdMan_t_::timeDsd
abctime timeDsd
Definition: ifDsd.c:98
If_DsdManCheckPrime
unsigned If_DsdManCheckPrime(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition: ifDsd.c:1853
If_Man_t_::pIfDsdMan
If_DsdMan_t * pIfDsdMan
Definition: if.h:243
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
If_LogCounterAddAig
static int If_LogCounterAddAig(int *pTimes, int *pnTimes, int *pFaninLits, int Num, int iLit, Vec_Int_t *vAig, int nSuppAll, int fXor, int fXorFunc)
Definition: ifCount.h:88
If_DsdObjId
static int If_DsdObjId(If_DsdObj_t *pObj)
Definition: ifDsd.c:111
If_DsdObj_t_
Definition: ifDsd.c:59
If_DsdVecObjSuppSize
static int If_DsdVecObjSuppSize(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:122
If_DsdMan_t_::vTtMem
Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]
Definition: ifDsd.c:85
If_DsdManComputeFirst
int If_DsdManComputeFirst(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pFirsts)
Definition: ifDsd.c:1493
If_DsdMan_t_::pTtElems
word ** pTtElems
Definition: ifDsd.c:84
If_DsdObjHashKey
static unsigned If_DsdObjHashKey(If_DsdMan_t *p, int Type, int *pLits, int nLits, int truthId)
Definition: ifDsd.c:890
If_DsdMan_t_::pTtGia
Gia_Man_t * pTtGia
Definition: ifDsd.c:90
If_CutDsdBalanceEval_rec
int If_CutDsdBalanceEval_rec(If_DsdMan_t *p, int Id, int *pTimes, int *pnSupp, Vec_Int_t *vAig, int *piLit, int nSuppAll, int *pArea, char *pPermLits)
Definition: ifDsd.c:2208
If_Cut_t_::nLeaves
unsigned nLeaves
Definition: if.h:289
If_DsdManCollect
void If_DsdManCollect(If_DsdMan_t *p, int Id, Vec_Int_t *vNodes, Vec_Int_t *vFirsts)
Definition: ifDsd.c:1307
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
If_DsdObj_t
struct If_DsdObj_t_ If_DsdObj_t
Definition: ifDsd.c:58
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Ifn_NtkPrint
void Ifn_NtkPrint(Ifn_Ntk_t *p)
Definition: ifTune.c:141
Vec_WecAlloc
static Vec_Wec_t * Vec_WecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWec.h:87
If_DsdMan_t_::timeCheck2
abctime timeCheck2
Definition: ifDsd.c:101
If_DsdMan_t_::vCover
Vec_Int_t * vCover
Definition: ifDsd.c:91
Abc_Lit2LitV
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition: vecWec.h:42
If_DsdVecLitSuppSize
static int If_DsdVecLitSuppSize(Vec_Ptr_t *p, int iLit)
Definition: ifDsd.c:123
If_DsdMan_t_::vTruths
Vec_Int_t vTruths
Definition: ifDsd.c:81
If_Par_t_::nLutSize
int nLutSize
Definition: if.h:103
If_CutPinDelayInit
static word If_CutPinDelayInit(int v)
Definition: ifCount.h:146
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition: extraUtilMisc.c:2169
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
If_DsdManGetFuncPerm
word If_DsdManGetFuncPerm(If_DsdMan_t *p, int iDsd)
Definition: ifDsd.c:199
If_DsdMan_t_::timeCanon
abctime timeCanon
Definition: ifDsd.c:99
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
If_DsdVecConst0
static If_DsdObj_t * If_DsdVecConst0(Vec_Ptr_t *p)
Definition: ifDsd.c:120
If_DsdManCheckDec
int If_DsdManCheckDec(If_DsdMan_t *p, int iDsd)
Definition: ifDsd.c:185
If_DsdMan_t_::vPerms
Vec_Wrd_t * vPerms
Definition: ifDsd.c:89
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
Vec_VecMemoryInt
static double Vec_VecMemoryInt(Vec_Vec_t *p)
Definition: vecVec.h:304
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
If_DsdObjIsVar
static int If_DsdObjIsVar(If_DsdObj_t *pObj)
Definition: ifDsd.c:113
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
If_CutPinDelayMax
static word If_CutPinDelayMax(word D1, word D2, int nVars, int AddOn)
Definition: ifCount.h:147
If_DsdVecObjClearMark
static void If_DsdVecObjClearMark(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:129
If_DsdManLoad
If_DsdMan_t * If_DsdManLoad(char *pFileName)
Definition: ifDsd.c:1086
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Vec_PtrGrow
static void Vec_PtrGrow(Vec_Ptr_t *p, int nCapMin)
Definition: vecPtr.h:430
If_Cut_t_
Definition: if.h:275
If_DsdManPrint
void If_DsdManPrint(If_DsdMan_t *p, char *pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose)
Definition: ifDsd.c:684
Vec_MemHashAlloc
static void Vec_MemHashAlloc(Vec_Mem_t *p, int nTableSize)
Definition: vecMem.h:305
Vec_MemForEachEntry
#define Vec_MemForEachEntry(p, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecMem.h:68
If_DsdObjWordNum
static int If_DsdObjWordNum(int nFans)
Definition: ifDsd.c:105
Dau_DsdReadVar
static int Dau_DsdReadVar(char *p)
Definition: dau.h:71
If_CutLeaveNum
static int If_CutLeaveNum(If_Cut_t *pCut)
Definition: if.h:390
Abc_TtPrintHexRev
static void Abc_TtPrintHexRev(FILE *pFile, word *pTruth, int nVars)
Definition: utilTruth.h:789
Vec_WecFree
static void Vec_WecFree(Vec_Wec_t *p)
Definition: vecWec.h:345
If_DsdManOperation
int If_DsdManOperation(If_DsdMan_t *p, int Type, int *pLits, int nLits, unsigned char *pPerm, word *pTruth)
Definition: ifDsd.c:1497
If_DsdMan_t_::nUniqueHits
int nUniqueHits
Definition: ifDsd.c:96
If_DsdMan_t_::vTtDecs
Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]
Definition: ifDsd.c:86
Vec_WecPushLevel
static Vec_Int_t * Vec_WecPushLevel(Vec_Wec_t *p)
Definition: vecWec.h:284
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_PtrFillExtra
static void Vec_PtrFillExtra(Vec_Ptr_t *p, int nSize, void *Fill)
Definition: vecPtr.h:469
If_DsdObjCompare
int If_DsdObjCompare(If_DsdMan_t *pMan, Vec_Ptr_t *p, int iLit0, int iLit1)
Definition: ifDsd.c:827
Vec_MemEntrySize
static int Vec_MemEntrySize(Vec_Mem_t *p)
Definition: vecMem.h:147
If_DsdManCleanMarks
void If_DsdManCleanMarks(If_DsdMan_t *p, int fVerbose)
Definition: ifDsd.c:1224
If_DsdManPrintDistrib
void If_DsdManPrintDistrib(If_DsdMan_t *p)
Definition: ifDsd.c:630
If_DsdObjCreate
int If_DsdObjCreate(If_DsdMan_t *p, int Type, int *pLits, int nLits, int truthId)
Definition: ifDsd.c:941
If_DsdManPrintOccurs
void If_DsdManPrintOccurs(FILE *pFile, If_DsdMan_t *p)
Definition: ifDsd.c:572
If_DsdManCheckXY
unsigned If_DsdManCheckXY(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose)
Definition: ifDsd.c:1986
If_DsdMan_t_::fNewAsUseless
int fNewAsUseless
Definition: ifDsd.c:95
Id_DsdManTuneThresh
void Id_DsdManTuneThresh(If_DsdMan_t *p, int fUnate, int fThresh, int fVerbose)
Definition: ifDsd.c:2721
Vec_Mem_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition: utilMem.c:35
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
If_DsdVecObjIncRef
static void If_DsdVecObjIncRef(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:125
If_DsdManPrintOne
void If_DsdManPrintOne(FILE *pFile, If_DsdMan_t *p, int iObjId, unsigned char *pPermLits, int fNewLine)
Definition: ifDsd.c:492
Vec_MemEntryNum
static int Vec_MemEntryNum(Vec_Mem_t *p)
Definition: vecMem.h:151
Dau_DecFindSets_int
Vec_Int_t * Dau_DecFindSets_int(word *pInit, int nVars, int *pSched[16])
Definition: dauNonDsd.c:462
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
Ifn_NtkLutSizeMax
int Ifn_NtkLutSizeMax(Ifn_Ntk_t *p)
Definition: ifTune.c:159
If_DsdManSave
void If_DsdManSave(If_DsdMan_t *p, char *pFileName)
Definition: ifDsd.c:1032
If_DsdMan_t_::pCellStr
char * pCellStr
Definition: ifDsd.c:93
Mem_Flex_t_
Definition: mem.c:55
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
If_ObjCutBest
static If_Cut_t * If_ObjCutBest(If_Obj_t *pObj)
Definition: if.h:401
If_LogPinDelaysMulti
static word If_LogPinDelaysMulti(word *pPinDels, int nFanins, int nSuppAll, int fXor)
Definition: ifCount.h:230
If_DsdVecForEachObjStart
#define If_DsdVecForEachObjStart(vVec, pObj, i, Start)
Definition: ifDsd.c:133
If_DsdMan_t_::vIsops
Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]
Definition: ifDsd.c:87
If_Cut_t_::fUser
unsigned fUser
Definition: if.h:286
Ifn_Ntk_t_
Definition: ifTune.c:69
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
If_DsdManDumpDsd
void If_DsdManDumpDsd(If_DsdMan_t *p, int Support)
Definition: ifDsd.c:356
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Vec_WrdSize
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
Vec_WrdFreeP
static void Vec_WrdFreeP(Vec_Wrd_t **p)
Definition: vecWrd.h:277
If_DsdManObjNum
int If_DsdManObjNum(If_DsdMan_t *p)
Definition: ifDsd.c:169
If_DsdMan_t_::pSat
void * pSat
Definition: ifDsd.c:92
Dau_DecFindSets
Vec_Int_t * Dau_DecFindSets(word *pInit, int nVars)
Definition: dauNonDsd.c:516
If_DsdObjTruthId
static int If_DsdObjTruthId(If_DsdMan_t *p, If_DsdObj_t *pObj)
Definition: ifDsd.c:106
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
nWords
int nWords
Definition: abcNpn.c:127
If_DsdObjTruth
static word * If_DsdObjTruth(If_DsdMan_t *p, If_DsdObj_t *pObj)
Definition: ifDsd.c:107
If_DsdManFileName
char * If_DsdManFileName(If_DsdMan_t *p)
FUNCTION DEFINITIONS ///.
Definition: ifDsd.c:161
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
If_CutDsdBalanceEvalInt
int If_CutDsdBalanceEvalInt(If_DsdMan_t *p, int iDsd, int *pTimes, Vec_Int_t *vAig, int *pArea, char *pPermLits)
Definition: ifDsd.c:2274
Vec_WecSize
static int Vec_WecSize(Vec_Wec_t *p)
Definition: vecWec.h:193
If_DsdObj_t_::nFans
unsigned nFans
Definition: ifDsd.c:66
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
If_DsdObjType
static int If_DsdObjType(If_DsdObj_t *pObj)
Definition: ifDsd.c:112
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
If_DsdVecObjRef
static int If_DsdVecObjRef(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:124
If_LogCounterPinDelays
static int If_LogCounterPinDelays(int *pTimes, int *pnTimes, word *pPinDels, int Num, word PinDel, int nSuppAll, int fXor)
Definition: ifCount.h:199
If_DsdObjHashResize
static void If_DsdObjHashResize(If_DsdMan_t *p)
Definition: ifDsd.c:922
Extra_ThreshCheck
int Extra_ThreshCheck(word *t, int nVars, int *pW)
Definition: extraUtilThresh.c:283
If_DsdObjFanin
static If_DsdObj_t * If_DsdObjFanin(Vec_Ptr_t *p, If_DsdObj_t *pObj, int i)
Definition: ifDsd.c:126
Abc_TtReadHex
static int Abc_TtReadHex(word *pTruth, char *pString)
Definition: utilTruth.h:838
Vec_IntGrow
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Abc_MergeSortCost
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition: utilSort.c:238
If_Cut_t_::Cost
unsigned Cost
Definition: if.h:284
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Mem_FlexStart
Mem_Flex_t * Mem_FlexStart()
Definition: mem.c:311
Vec_MemAlloc
static Vec_Mem_t * Vec_MemAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: utilMem.c:70
If_DsdObj_t_::Type
unsigned Type
Definition: ifDsd.c:62
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
If_DsdObjAlloc
If_DsdObj_t * If_DsdObjAlloc(If_DsdMan_t *p, int Type, int nFans)
Definition: ifDsd.c:231
DAU_MAX_STR
#define DAU_MAX_STR
Definition: dau.h:43
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Dau_DecPrintSets
void Dau_DecPrintSets(Vec_Int_t *vSets, int nVars)
Definition: dauNonDsd.c:434
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
If_DsdMan_t_::timeCheck
abctime timeCheck
Definition: ifDsd.c:100
If_CutDsdBalanceEval
int If_CutDsdBalanceEval(If_Man_t *p, If_Cut_t *pCut, Vec_Int_t *vAig)
Definition: ifDsd.c:2288
Abc_TtHexDigitNum
static int Abc_TtHexDigitNum(int nVars)
Definition: utilTruth.h:171
If_DsdObjFaninNum
static int If_DsdObjFaninNum(If_DsdObj_t *pObj)
Definition: ifDsd.c:115
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
If_DsdManComputeFirstArray
int If_DsdManComputeFirstArray(If_DsdMan_t *p, int *pLits, int nLits, int *pFirsts)
Definition: ifDsd.c:1483
If_DsdManCleanOccur
void If_DsdManCleanOccur(If_DsdMan_t *p, int fVerbose)
Definition: ifDsd.c:1217
If_DsdManAddDsd
int If_DsdManAddDsd(If_DsdMan_t *p, char *pDsd, word *pTruth, unsigned char *pPerm, int *pnSupp)
Definition: ifDsd.c:1687
If_DsdMan_t_::LutSize
int LutSize
Definition: ifDsd.c:74
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
If_DsdSign_rec
unsigned If_DsdSign_rec(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pnSupp)
Definition: ifDsd.c:1722
If_CutSopBalanceEvalInt
int If_CutSopBalanceEvalInt(Vec_Int_t *vCover, int *pTimes, int *pFaninLits, Vec_Int_t *vAig, int *piRes, int nSuppAll, int *pArea)
Definition: ifDelay.c:192
DAU_MAX_VAR
#define DAU_MAX_VAR
INCLUDES ///.
Definition: dau.h:42
If_DsdManFilter_rec
void If_DsdManFilter_rec(If_DsdMan_t *pNew, If_DsdMan_t *p, int i, Vec_Int_t *vMap)
Definition: ifDsd.c:1242
If_ManSatCheckXYall
unsigned If_ManSatCheckXYall(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition: ifSat.c:476
If_DsdMan_t_::vObjs
Vec_Ptr_t vObjs
Definition: ifDsd.c:79
If_DsdObjForEachFanin
#define If_DsdObjForEachFanin(vVec, pObj, pFanin, i)
Definition: ifDsd.c:139
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Vec_WrdShrink
static void Vec_WrdShrink(Vec_Wrd_t *p, int nSizeNew)
Definition: vecWrd.h:585
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
If_DsdVecForEachObjVec
#define If_DsdVecForEachObjVec(vNodes, vVec, pObj, i)
Definition: ifDsd.c:135
If_DsdObjHashLookup
unsigned * If_DsdObjHashLookup(If_DsdMan_t *p, int Type, int *pLits, int nLits, int truthId)
Definition: ifDsd.c:903
Vec_WrdWriteEntry
static void Vec_WrdWriteEntry(Vec_Wrd_t *p, int i, word Entry)
Definition: vecWrd.h:418
Abc_TtPrintBinary
static void Abc_TtPrintBinary(word *pTruth, int nVars)
Definition: utilTruth.h:907
If_DsdMan_t_::pStore
char * pStore
Definition: ifDsd.c:72
If_Man_t_
Definition: if.h:180
If_DsdManGetCellStr
char * If_DsdManGetCellStr(If_DsdMan_t *p)
Definition: ifDsd.c:203
If_DsdManCheckMux
unsigned If_DsdManCheckMux(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition: ifDsd.c:1817
If_DsdManDumpAll
void If_DsdManDumpAll(If_DsdMan_t *p, int Support)
Definition: ifDsd.c:390
If_DsdMan_t_::vTemp1
Vec_Int_t * vTemp1
Definition: ifDsd.c:82
If_CutLeaf
static If_Obj_t * If_CutLeaf(If_Man_t *p, If_Cut_t *pCut, int i)
Definition: if.h:392
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
If_DsdMan_t_
Definition: ifDsd.c:70
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
If_DsdMan_t_::timeVerify
abctime timeVerify
Definition: ifDsd.c:102
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
If_DsdManGetSuppSizes
void If_DsdManGetSuppSizes(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pSSizes)
Definition: ifDsd.c:1739
If_DsdObjForEachFaninLit
#define If_DsdObjForEachFaninLit(vVec, pObj, iLit, i)
Definition: ifDsd.c:141
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Abc_TtStretch6
static void Abc_TtStretch6(word *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:693
memcmp
int memcmp()
If_DsdMan_t_::nBins
int nBins
Definition: ifDsd.c:76
If_DsdManComputeTruth
word * If_DsdManComputeTruth(If_DsdMan_t *p, int iDsd, unsigned char *pPermLits)
Definition: ifDsd.c:1396
If_DsdMergeMatches
static void If_DsdMergeMatches(char *pDsd, int *pMatches)
Definition: ifDsd.c:1619
If_DsdManPrint_rec
void If_DsdManPrint_rec(FILE *pFile, If_DsdMan_t *p, int iDsdLit, unsigned char *pPermLits, int *pnSupp)
Definition: ifDsd.c:469
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition: if.h:54
If_DsdManCheckNonDec_rec
int If_DsdManCheckNonDec_rec(If_DsdMan_t *p, int Id)
Definition: ifDsd.c:453
Ifn_NtkInputNum
int Ifn_NtkInputNum(Ifn_Ntk_t *p)
Definition: ifTune.c:167
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
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
If_DsdManCheckInv_rec
int If_DsdManCheckInv_rec(If_DsdMan_t *p, int iLit)
Definition: ifDsd.c:1414
Id_DsdManTuneStr
void Id_DsdManTuneStr(If_DsdMan_t *p, char *pStruct, int nConfls, int nProcs, int fVerbose)
Definition: ifDsd.c:2519
If_DsdManPushInv_rec
int If_DsdManPushInv_rec(If_DsdMan_t *p, int iLit, unsigned char *pPerm)
Definition: ifDsd.c:1435
Vec_IntAppend
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
Definition: extraZddTrunc.c:126
sprintf
char * sprintf()
If_DsdManComputeTruthPtr
void If_DsdManComputeTruthPtr(If_DsdMan_t *p, int iDsd, unsigned char *pPermLits, word *pRes)
Definition: ifDsd.c:1378
Counter
static int Counter
Definition: extraBddMisc.c:1877
If_DsdMan_t_::vNexts
Vec_Int_t vNexts
Definition: ifDsd.c:80
If_ManSatBuildXY
void * If_ManSatBuildXY(int nLutSize)
DECLARATIONS ///.
Definition: ifSat.c:45
If_ManSatUnbuild
void If_ManSatUnbuild(void *p)
Definition: ifSat.c:85
If_DsdObjClean
static void If_DsdObjClean(If_DsdObj_t *pObj)
Definition: ifDsd.c:110
If_DsdMan_t_::nWords
int nWords
Definition: ifDsd.c:75
If_CutSopBalancePinDelaysInt
int If_CutSopBalancePinDelaysInt(Vec_Int_t *vCover, int *pTimes, word *pFaninRes, int nSuppAll, word *pRes)
Definition: ifDelay.c:120
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
If_DsdManVarNum
int If_DsdManVarNum(If_DsdMan_t *p)
Definition: ifDsd.c:165
Vec_IntCap
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
If_LogCreateMux
static int If_LogCreateMux(Vec_Int_t *vAig, int iLitC, int iLit1, int iLit0, int nSuppAll)
Definition: ifCount.h:65
Vec_MemDumpTruthTables
static void Vec_MemDumpTruthTables(Vec_Mem_t *p, char *pName, int nLutSize)
Definition: vecMem.h:402
Vec_MemFree
static void Vec_MemFree(Vec_Mem_t *p)
Definition: utilMem.c:93
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Id_DsdManTuneStr1
void Id_DsdManTuneStr1(If_DsdMan_t *p, char *pStruct, int nConfls, int fVerbose)
Definition: ifDsd.c:2435
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
If_DsdObj_t_::pFans
unsigned pFans[0]
Definition: ifDsd.c:67
If_DsdManCheckXYZ
unsigned If_DsdManCheckXYZ(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, int fVerbose)
Definition: ifDsd.c:2016
Vec_PtrCap
static int Vec_PtrCap(Vec_Ptr_t *p)
Definition: vecPtr.h:311
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
If_DsdVecVar
static If_DsdObj_t * If_DsdVecVar(Vec_Ptr_t *p, int v)
Definition: ifDsd.c:121
Mem_FlexStop
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition: mem.c:343
If_DsdManInvertMarks
void If_DsdManInvertMarks(If_DsdMan_t *p, int fVerbose)
Definition: ifDsd.c:1233
If_DsdSign
unsigned If_DsdSign(If_DsdMan_t *p, If_DsdObj_t *pObj, int iFan, int iFirst, int fShared)
Definition: ifDsd.c:1732
If_CutDsdBalancePinDelays
int If_CutDsdBalancePinDelays(If_Man_t *p, If_Cut_t *pCut, char *pPerm)
Definition: ifDsd.c:2152
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition: dauNonDsd.c:390
Vec_WecEntry
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
If_DsdManComputeTruth_rec
void If_DsdManComputeTruth_rec(If_DsdMan_t *p, int iDsd, word *pRes, unsigned char *pPermLits, int *pnSupp)
Definition: ifDsd.c:1326
If_DsdObjSetTruth
static void If_DsdObjSetTruth(If_DsdMan_t *p, If_DsdObj_t *pObj, int Id)
Definition: ifDsd.c:108
If_DsdObj_t_::fMark
unsigned fMark
Definition: ifDsd.c:64
Vec_WrdStart
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
If_DsdObj_t_::nSupp
unsigned nSupp
Definition: ifDsd.c:63
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition: dau.h:44
If_LogCreateAndXorMulti
static int If_LogCreateAndXorMulti(Vec_Int_t *vAig, int *pFaninLits, int nFanins, int nSuppAll, int fXor)
Definition: ifCount.h:80
If_DsdObjSort
void If_DsdObjSort(If_DsdMan_t *pMan, Vec_Ptr_t *p, int *pLits, int nLits, int *pPerm)
Definition: ifDsd.c:862
If_CutDsdPermLitMax
int If_CutDsdPermLitMax(char *pPermLits, int nVars, int iVar)
Definition: ifDsd.c:2186
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
If_CutDsdLit
static int If_CutDsdLit(If_Man_t *p, If_Cut_t *pCut)
Definition: if.h:424
Kit_TruthToGia
int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition: kitHop.c:80
If_Man_t_::pPars
If_Par_t * pPars
Definition: if.h:184
Dau_DsdIsConst1
static int Dau_DsdIsConst1(char *p)
Definition: dau.h:69
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
DSD_ARRAY_LIMIT
#define DSD_ARRAY_LIMIT
Definition: ifDsd.c:504
If_DsdManTest
void If_DsdManTest()
Definition: ifDsd.c:2082
If_DsdMan_t_::vTemp2
Vec_Int_t * vTemp2
Definition: ifDsd.c:83
If_DsdMan_t_::pSched
int * pSched[IF_MAX_FUNC_LUTSIZE]
Definition: ifDsd.c:88
If_DsdManPrintDecs
void If_DsdManPrintDecs(FILE *pFile, If_DsdMan_t *p)
Definition: ifDsd.c:505
If_DsdManAllocIsops
void If_DsdManAllocIsops(If_DsdMan_t *p, int nLutSize)
Definition: ifDsd.c:289
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
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
If_DsdManPushInv
int If_DsdManPushInv(If_DsdMan_t *p, int iLit, unsigned char *pPerm)
Definition: ifDsd.c:1465
If_DsdManFilter
If_DsdMan_t * If_DsdManFilter(If_DsdMan_t *p, int Limit)
Definition: ifDsd.c:1263
If_ManDsdTtElems
static word ** If_ManDsdTtElems()
Definition: ifDsd.c:219
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
If_DsdObjFaninLit
static int If_DsdObjFaninLit(If_DsdObj_t *pObj, int i)
Definition: ifDsd.c:117
Gia_Man_t_
Definition: gia.h:95
If_DsdMan_t_::pMem
Mem_Flex_t * pMem
Definition: ifDsd.c:78
Ifn_NtkMatch
int Ifn_NtkMatch(Ifn_Ntk_t *p, word *pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word *pPerm)
Definition: ifTune.c:1207
If_DsdObjFindOrAdd
int If_DsdObjFindOrAdd(If_DsdMan_t *p, int Type, int *pLits, int nLits, word *pTruth)
Definition: ifDsd.c:976
If_DsdObjFaninC
static int If_DsdObjFaninC(If_DsdObj_t *pObj, int i)
Definition: ifDsd.c:116
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
If_CutDsdBalancePinDelays_rec
int If_CutDsdBalancePinDelays_rec(If_DsdMan_t *p, int Id, int *pTimes, word *pRes, int *pnSupp, int nSuppAll, char *pPermLits)
Definition: ifDsd.c:2104
If_CutPinDelayTranslate
static void If_CutPinDelayTranslate(word D, int nVars, char *pPerm)
Definition: ifCount.h:181
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
If_DsdManAddDsd_rec
int If_DsdManAddDsd_rec(char *pStr, char **p, int *pMatches, If_DsdMan_t *pMan, word *pTruth, unsigned char *pPerm, int *pnSupp)
Definition: ifDsd.c:1634
Vec_WrdEntry
static word Vec_WrdEntry(Vec_Wrd_t *p, int i)
Definition: vecWrd.h:384
If_DsdMan_t_::nUniqueMisses
int nUniqueMisses
Definition: ifDsd.c:97
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
If_DsdManSetLutSize
void If_DsdManSetLutSize(If_DsdMan_t *p, int nLutSize)
Definition: ifDsd.c:177
If_DsdObjSuppSize
static int If_DsdObjSuppSize(If_DsdObj_t *pObj)
Definition: ifDsd.c:114
Abc_TtSupportSize
static int Abc_TtSupportSize(word *t, int nVars)
Definition: utilTruth.h:986
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition: dauCanon.c:895
If_DsdMan_t_::pBins
unsigned * pBins
Definition: ifDsd.c:77
If_DsdManHasMarks
int If_DsdManHasMarks(If_DsdMan_t *p)
Definition: ifDsd.c:415
If_DsdVecObj
static If_DsdObj_t * If_DsdVecObj(Vec_Ptr_t *p, int Id)
Definition: ifDsd.c:119
If_DsdManCheckXY_int
unsigned If_DsdManCheckXY_int(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fVerbose)
Definition: ifDsd.c:1911
If_DsdManCompute
int If_DsdManCompute(If_DsdMan_t *p, word *pTruth, int nLeaves, unsigned char *pPerm, char *pLutStruct)
Definition: ifDsd.c:2032
If_DsdMan_t_::nVars
int nVars
Definition: ifDsd.c:73
If_DsdVecForEachObj
#define If_DsdVecForEachObj(vVec, pObj, i)
Definition: ifDsd.c:131
Vec_MemHashInsert
static int Vec_MemHashInsert(Vec_Mem_t *p, word *pEntry)
Definition: vecMem.h:351
If_DsdManHashProfile
void If_DsdManHashProfile(If_DsdMan_t *p)
Definition: ifDsd.c:436
Vec_MemHashFree
static void Vec_MemHashFree(Vec_Mem_t *p)
Definition: vecMem.h:311
sat_solver_t
Definition: satSolver.h:91
If_DsdObj_t_::Count
unsigned Count
Definition: ifDsd.c:65
Abc_TtIsUnate
static int Abc_TtIsUnate(word *t, int nVars)
Definition: utilTruth.h:1667
If_DsdManCheckAndXor
unsigned If_DsdManCheckAndXor(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition: ifDsd.c:1746
If_DsdVecObjMark
static int If_DsdVecObjMark(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:127
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
strlen
int strlen()
If_DsdMan_t_::nObjsPrev
int nObjsPrev
Definition: ifDsd.c:94
If_DsdManReadMark
int If_DsdManReadMark(If_DsdMan_t *p, int iDsd)
Definition: ifDsd.c:189
Dau_DsdIsVar
static int Dau_DsdIsVar(char *p)
Definition: dau.h:70
If_LogCounterDelayXor
static int If_LogCounterDelayXor(int *pTimes, int nTimes)
Definition: ifCount.h:123
If_DsdManCheckNonTriv
int If_DsdManCheckNonTriv(If_DsdMan_t *p, int Id, int nVars, int iVarMax)
Definition: ifDsd.c:802
If_Cut_t_::fCompl
unsigned fCompl
Definition: if.h:285
If_DsdManCollect_rec
void If_DsdManCollect_rec(If_DsdMan_t *p, int Id, Vec_Int_t *vNodes, Vec_Int_t *vFirsts, int *pnSupp)
Definition: ifDsd.c:1290
Dau_DsdIsConst0
static int Dau_DsdIsConst0(char *p)
Definition: dau.h:68
If_DsdManLutSize
int If_DsdManLutSize(If_DsdMan_t *p)
Definition: ifDsd.c:173
If_DsdManSuppSize
int If_DsdManSuppSize(If_DsdMan_t *p, int iDsd)
Definition: ifDsd.c:181
Vec_MemReadEntry
static word * Vec_MemReadEntry(Vec_Mem_t *p, int i)
Definition: vecMem.h:191
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
If_DsdVecForEachNode
#define If_DsdVecForEachNode(vVec, pObj, i)
Definition: ifDsd.c:137
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_WrdFillExtra
static void Vec_WrdFillExtra(Vec_Wrd_t *p, int nSize, word Fill)
Definition: vecWrd.h:509
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
If_CutDsdPerm
static char * If_CutDsdPerm(If_Man_t *p, If_Cut_t *pCut)
Definition: if.h:426
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
If_DsdVecObjSetMark
static void If_DsdVecObjSetMark(Vec_Ptr_t *p, int iObj)
Definition: ifDsd.c:128
If_DsdType_t
If_DsdType_t
DECLARATIONS ///.
Definition: ifDsd.c:48
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Abc_TtElemInit
static void Abc_TtElemInit(word **pTtElems, int nVars)
Definition: utilTruth.h:333
If_Cut_t_::Delay
float Delay
Definition: if.h:280
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
If_DsdObj_t_::Id
unsigned Id
Definition: ifDsd.c:61
If_DsdManMerge
void If_DsdManMerge(If_DsdMan_t *p, If_DsdMan_t *pNew)
Definition: ifDsd.c:1177
If_DsdManFree
void If_DsdManFree(If_DsdMan_t *p, int fVerbose)
Definition: ifDsd.c:316
If_DsdManAlloc
If_DsdMan_t * If_DsdManAlloc(int nVars, int LutSize)
Definition: ifDsd.c:248
Ifn_NtkParse
Ifn_Ntk_t * Ifn_NtkParse(char *pStr)
Definition: ifTune.c:439