abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaJf.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaJf.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaJf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "misc/vec/vecSet.h"
23 #include "misc/vec/vecMem.h"
24 #include "misc/extra/extra.h"
25 #include "bool/kit/kit.h"
26 #include "misc/util/utilTruth.h"
27 #include "opt/dau/dau.h"
28 #include "sat/cnf/cnf.h"
29 
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// DECLARATIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 #define JF_LEAF_MAX 8
37 #define JF_WORD_MAX ((JF_LEAF_MAX > 6) ? 1 << (JF_LEAF_MAX-6) : 1)
38 #define JF_CUT_MAX 16
39 
40 typedef struct Jf_Cut_t_ Jf_Cut_t;
41 struct Jf_Cut_t_
42 {
43  word Sign; // signature
44  float Flow; // flow
45  int Time; // arrival time
46  int iFunc; // function
47  int Cost; // cut cost
48  int pCut[JF_LEAF_MAX+2]; // cut
49 };
50 
51 typedef struct Jf_Man_t_ Jf_Man_t;
52 struct Jf_Man_t_
53 {
54  Gia_Man_t * pGia; // user's manager
55  Jf_Par_t * pPars; // users parameter
56  Sdm_Man_t * pDsd; // extern DSD manager
57  Vec_Int_t * vCnfs; // costs of elementary CNFs
58  Vec_Mem_t * vTtMem; // truth table memory and hash table
59  Vec_Int_t vCuts; // cuts for each node
60  Vec_Int_t vArr; // arrival time
61  Vec_Int_t vDep; // departure time
62  Vec_Flt_t vFlow; // area flow
63  Vec_Flt_t vRefs; // ref counters
64  Vec_Set_t pMem; // cut storage
65  Vec_Int_t * vTemp; // temporary
66  float (*pCutCmp) (Jf_Cut_t *, Jf_Cut_t *);// procedure to compare cuts
67  abctime clkStart; // starting time
68  word CutCount[4]; // statistics
69  int nCoarse; // coarse nodes
70 };
71 
72 static inline int Jf_ObjIsUnit( Gia_Obj_t * p ) { return !p->fMark0; }
73 static inline void Jf_ObjCleanUnit( Gia_Obj_t * p ) { assert(Jf_ObjIsUnit(p)); p->fMark0 = 1; }
74 static inline void Jf_ObjSetUnit( Gia_Obj_t * p ) { p->fMark0 = 0; }
75 
76 static inline int Jf_ObjCutH( Jf_Man_t * p, int i ) { return Vec_IntEntry(&p->vCuts, i); }
77 static inline int * Jf_ObjCuts( Jf_Man_t * p, int i ) { return (int *)Vec_SetEntry(&p->pMem, Jf_ObjCutH(p, i)); }
78 static inline int * Jf_ObjCutBest( Jf_Man_t * p, int i ) { return Jf_ObjCuts(p, i) + 1; }
79 static inline int Jf_ObjArr( Jf_Man_t * p, int i ) { return Vec_IntEntry(&p->vArr, i); }
80 static inline int Jf_ObjDep( Jf_Man_t * p, int i ) { return Vec_IntEntry(&p->vDep, i); }
81 static inline float Jf_ObjFlow( Jf_Man_t * p, int i ) { return Vec_FltEntry(&p->vFlow, i); }
82 static inline float Jf_ObjRefs( Jf_Man_t * p, int i ) { return Vec_FltEntry(&p->vRefs, i); }
83 //static inline int Jf_ObjLit( int i, int c ) { return i; }
84 static inline int Jf_ObjLit( int i, int c ) { return Abc_Var2Lit( i, c ); }
85 
86 static inline int Jf_CutSize( int * pCut ) { return pCut[0] & 0xF; } // 4 bits
87 static inline int Jf_CutCost( int * pCut ) { return (pCut[0] >> 4) & 0xF; } // 4 bits
88 static inline int Jf_CutFunc( int * pCut ) { return ((unsigned)pCut[0] >> 8); } // 24 bits
89 static inline int Jf_CutSetAll( int f, int c, int s ) { return (f << 8) | (c << 4) | s; }
90 static inline void Jf_CutSetSize( int * pCut, int s ) { assert(s>=0 && s<16); pCut[0] ^= (Jf_CutSize(pCut) ^ s); }
91 static inline void Jf_CutSetCost( int * pCut, int c ) { assert(c>=0 && c<16); pCut[0] ^=((Jf_CutCost(pCut) ^ c) << 4); }
92 static inline void Jf_CutSetFunc( int * pCut, int f ) { assert(f>=0); pCut[0] ^=((Jf_CutFunc(pCut) ^ f) << 8); }
93 
94 static inline int Jf_CutFuncClass( int * pCut ) { return Abc_Lit2Var(Jf_CutFunc(pCut)); }
95 static inline int Jf_CutFuncCompl( int * pCut ) { return Abc_LitIsCompl(Jf_CutFunc(pCut)); }
96 static inline int * Jf_CutLits( int * pCut ) { return pCut + 1; }
97 static inline int Jf_CutLit( int * pCut, int i ) { assert(i);return pCut[i]; }
98 //static inline int Jf_CutVar( int * pCut, int i ) { assert(i); return pCut[i]; }
99 static inline int Jf_CutVar( int * pCut, int i ) { assert(i);return Abc_Lit2Var(pCut[i]); }
100 static inline int Jf_CutIsTriv( int * pCut, int i ) { return Jf_CutSize(pCut) == 1 && Jf_CutVar(pCut, 1) == i; }
101 static inline int Jf_CutCnfSizeF( Jf_Man_t * p, int f ) { return Vec_IntEntry( p->vCnfs, f ); }
102 static inline int Jf_CutCnfSize( Jf_Man_t * p, int * c ) { return Jf_CutCnfSizeF( p, Jf_CutFuncClass(c) ); }
103 
104 static inline int Jf_ObjFunc0( Gia_Obj_t * p, int * c ) { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC0(p)); }
105 static inline int Jf_ObjFunc1( Gia_Obj_t * p, int * c ) { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC1(p)); }
106 
107 #define Jf_ObjForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Jf_CutSize(pCut) + 1 )
108 #define Jf_CutForEachLit( pCut, Lit, i ) for ( i = 1; i <= Jf_CutSize(pCut) && (Lit = Jf_CutLit(pCut, i)); i++ )
109 #define Jf_CutForEachVar( pCut, Var, i ) for ( i = 1; i <= Jf_CutSize(pCut) && (Var = Jf_CutVar(pCut, i)); i++ )
110 
111 extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
112 
113 ////////////////////////////////////////////////////////////////////////
114 /// FUNCTION DEFINITIONS ///
115 ////////////////////////////////////////////////////////////////////////
116 
117 /**Function*************************************************************
118 
119  Synopsis [Derives CNF for the mapped GIA.]
120 
121  Description []
122 
123  SideEffects []
124 
125  SeeAlso []
126 
127 ***********************************************************************/
128 void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vClas, Vec_Int_t * vCover )
129 {
130  if ( uTruth == 0 || ~uTruth == 0 )
131  {
132  Vec_IntPush( vClas, Vec_IntSize(vLits) );
133  Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, (uTruth == 0)) );
134  }
135  else
136  {
137  int i, k, c, Literal, Cube;
138  assert( Vec_IntSize(vLeaves) > 0 );
139  for ( c = 0; c < 2; c ++ )
140  {
141  int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, Vec_IntSize(vLeaves), vCover, 0 );
142  assert( RetValue == 0 );
143  Vec_IntForEachEntry( vCover, Cube, i )
144  {
145  Vec_IntPush( vClas, Vec_IntSize(vLits) );
146  Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, c) );
147  for ( k = 0; k < Vec_IntSize(vLeaves); k++ )
148  {
149  Literal = 3 & (Cube >> (k << 1));
150  if ( Literal == 1 ) // '0' -> pos lit
151  Vec_IntPush( vLits, Abc_LitNotCond(Vec_IntEntry(vLeaves, k), 0) );
152  else if ( Literal == 2 ) // '1' -> neg lit
153  Vec_IntPush( vLits, Abc_LitNotCond(Vec_IntEntry(vLeaves, k), 1) );
154  else if ( Literal != 0 )
155  assert( 0 );
156  }
157  }
158  uTruth = ~uTruth;
159  }
160  }
161 }
162 Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas, int fAddOrCla )
163 {
164  Cnf_Dat_t * pCnf;
165  Gia_Obj_t * pObj;
166  int i, Entry, * pMap, nVars = 0;
167  if ( fAddOrCla )
168  {
169  Vec_IntPush( vClas, Vec_IntSize(vLits) );
170  Gia_ManForEachPo( p, pObj, i )
171  Vec_IntPush( vLits, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) );
172  }
173  // label nodes present in the mapping
174  Vec_IntForEachEntry( vLits, Entry, i )
175  Gia_ManObj(p, Abc_Lit2Var(Entry))->fMark0 = 1;
176  // create variable map
177  pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
178  Gia_ManForEachObjReverse( p, pObj, i )
179  if ( pObj->fMark0 )
180  pObj->fMark0 = 0, pMap[i] = nVars++;
181  // relabel literals
182  Vec_IntForEachEntry( vLits, Entry, i )
183  Vec_IntWriteEntry( vLits, i, Abc_Lit2LitV(pMap, Entry) );
184  // generate CNF
185  pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
186  pCnf->pMan = (Aig_Man_t *)p;
187  pCnf->nVars = nVars;
188  pCnf->nLiterals = Vec_IntSize(vLits);
189  pCnf->nClauses = Vec_IntSize(vClas);
190  pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
191  pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
192  Vec_IntForEachEntry( vClas, Entry, i )
193  pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
194  pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
195  pCnf->pVarNums = pMap;
196  return pCnf;
197 }
199 {
200  Cnf_Dat_t * pCnf;
201  int i, Entry, iOut;
202  // generate CNF
203  pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
204  pCnf->pMan = (Aig_Man_t *)p;
205  pCnf->nVars = Gia_ManObjNum(p);
206  pCnf->nLiterals = Vec_IntSize(vLits);
207  pCnf->nClauses = Vec_IntSize(vClas);
208  pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
209  pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
210  Vec_IntForEachEntry( vClas, Entry, i )
211  pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
212  pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
213  // create mapping of objects into their clauses
214  pCnf->pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p) );
215  pCnf->pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p) );
216  for ( i = 0; i < pCnf->nClauses; i++ )
217  {
218  iOut = Abc_Lit2Var(pCnf->pClauses[i][0]);
219  if ( pCnf->pObj2Clause[iOut] == -1 )
220  {
221  pCnf->pObj2Clause[iOut] = i;
222  pCnf->pObj2Count[iOut] = 1;
223  }
224  else
225  {
226  assert( pCnf->pObj2Count[iOut] > 0 );
227  pCnf->pObj2Count[iOut]++;
228  }
229  }
230  return pCnf;
231 }
232 
233 /**Function*************************************************************
234 
235  Synopsis [Computing references while discounting XOR/MUX.]
236 
237  Description []
238 
239  SideEffects []
240 
241  SeeAlso []
242 
243 ***********************************************************************/
244 float * Jf_ManInitRefs( Jf_Man_t * pMan )
245 {
246  Gia_Man_t * p = pMan->pGia;
247  Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
248  float * pRes; int i;
249  assert( p->pRefs == NULL );
250  p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
251  Gia_ManForEachAnd( p, pObj, i )
252  {
253  Gia_ObjRefFanin0Inc( p, pObj );
254  if ( Gia_ObjIsBuf(pObj) )
255  continue;
256  Gia_ObjRefFanin1Inc( p, pObj );
257  if ( !Gia_ObjIsMuxType(pObj) )
258  continue;
259  // discount XOR/MUX
260  pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
261  Gia_ObjRefDec( p, Gia_Regular(pCtrl) );
262  if ( Gia_Regular(pData1) == Gia_Regular(pData0) )
263  Gia_ObjRefDec( p, Gia_Regular(pData1) );
264  }
265  Gia_ManForEachCo( p, pObj, i )
266  Gia_ObjRefFanin0Inc( p, pObj );
267  // mark XOR/MUX internal nodes, which are not used elsewhere
268  if ( pMan->pPars->fCoarsen )
269  {
270  pMan->nCoarse = 0;
271  Gia_ManForEachAnd( p, pObj, i )
272  {
273  if ( !Gia_ObjIsMuxType(pObj) )
274  continue;
275  if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) == 1 )
276  {
279  Jf_ObjCleanUnit(Gia_ObjFanin0(pObj)), pMan->nCoarse++;
280  }
281  if ( Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) == 1 )
282  {
285  Jf_ObjCleanUnit(Gia_ObjFanin1(pObj)), pMan->nCoarse++;
286  }
287  }
288  }
289  // multiply by factor
290  pRes = ABC_ALLOC( float, Gia_ManObjNum(p) );
291  for ( i = 0; i < Gia_ManObjNum(p); i++ )
292  pRes[i] = Abc_MaxInt( 1, p->pRefs[i] );
293  return pRes;
294 }
295 
296 /**Function*************************************************************
297 
298  Synopsis []
299 
300  Description []
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
308 {
309  Gia_Obj_t * pObj;
310  int Counts[595] = {0}, Costs[595] = {0};
311  int i, iFunc, Total = 0, CostTotal = 0, Other = 0, CostOther = 0;
312  printf( "DSD classes that appear in more than %.1f %% of mapped nodes:\n", 0.1 * p->pPars->nVerbLimit );
313  Gia_ManForEachAnd( p->pGia, pObj, i )
314  if ( !Gia_ObjIsBuf(pObj) && Gia_ObjRefNumId(p->pGia, i) )
315  {
316  iFunc = Jf_CutFuncClass( Jf_ObjCutBest(p, i) );
317  assert( iFunc < 595 );
318  if ( p->pPars->fGenCnf )
319  {
320  Costs[iFunc] += Jf_CutCnfSizeF(p, iFunc);
321  CostTotal += Jf_CutCnfSizeF(p, iFunc);
322  }
323  Counts[iFunc]++;
324  Total++;
325  }
326  CostTotal = Abc_MaxInt(CostTotal, 1);
327  Total = Abc_MaxInt(Total, 1);
328  for ( i = 0; i < 595; i++ )
329  if ( Counts[i] && 100.0 * Counts[i] / Total >= 0.1 * p->pPars->nVerbLimit )
330  {
331  printf( "%5d : ", i );
332  printf( "%-20s ", Sdm_ManReadDsdStr(p->pDsd, i) );
333  printf( "%8d ", Counts[i] );
334  printf( "%5.1f %% ", 100.0 * Counts[i] / Total );
335  printf( "%8d ", Costs[i] );
336  printf( "%5.1f %%", 100.0 * Costs[i] / CostTotal );
337  printf( "\n" );
338  }
339  else
340  {
341  Other += Counts[i];
342  CostOther += Costs[i];
343  }
344  printf( "Other : " );
345  printf( "%-20s ", "" );
346  printf( "%8d ", Other );
347  printf( "%5.1f %% ", 100.0 * Other / Total );
348  printf( "%8d ", CostOther );
349  printf( "%5.1f %%", 100.0 * CostOther / CostTotal );
350  printf( "\n" );
351 }
352 
353 /**Function*************************************************************
354 
355  Synopsis [Manager manipulation.]
356 
357  Description []
358 
359  SideEffects []
360 
361  SeeAlso []
362 
363 ***********************************************************************/
365 {
366  Jf_Man_t * p;
367  assert( pPars->nLutSize <= JF_LEAF_MAX );
368  assert( pPars->nCutNum <= JF_CUT_MAX );
369  Vec_IntFreeP( &pGia->vMapping );
370  p = ABC_CALLOC( Jf_Man_t, 1 );
371  p->pGia = pGia;
372  p->pPars = pPars;
373  if ( pPars->fCutMin && !pPars->fFuncDsd )
374  p->vTtMem = Vec_MemAllocForTT( pPars->nLutSize, 0 );
375  else if ( pPars->fCutMin && pPars->fFuncDsd )
376  {
377  p->pDsd = Sdm_ManRead();
378  if ( pPars->fGenCnf )
379  {
380  p->vCnfs = Vec_IntStart( 595 );
382  }
383  }
384  Vec_IntFill( &p->vCuts, Gia_ManObjNum(pGia), 0 );
385  Vec_IntFill( &p->vArr, Gia_ManObjNum(pGia), 0 );
386  Vec_IntFill( &p->vDep, Gia_ManObjNum(pGia), 0 );
387  Vec_FltFill( &p->vFlow, Gia_ManObjNum(pGia), 0 );
388  p->vRefs.nCap = p->vRefs.nSize = Gia_ManObjNum(pGia);
389  p->vRefs.pArray = Jf_ManInitRefs( p );
390  Vec_SetAlloc_( &p->pMem, 20 );
391  p->vTemp = Vec_IntAlloc( 1000 );
392  p->clkStart = Abc_Clock();
393  return p;
394 }
396 {
397  if ( p->pPars->fVerbose && p->pDsd )
398  Sdm_ManPrintDsdStats( p->pDsd, 0 );
399  if ( p->pPars->fVerbose && p->vTtMem )
400  {
401  printf( "Unique truth tables = %d. Memory = %.2f MB ", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
402  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
403  }
404  if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && p->pPars->fFuncDsd )
406  if ( p->pPars->fCoarsen )
407  Gia_ManCleanMark0( p->pGia );
408  ABC_FREE( p->pGia->pRefs );
409  ABC_FREE( p->vCuts.pArray );
410  ABC_FREE( p->vArr.pArray );
411  ABC_FREE( p->vDep.pArray );
412  ABC_FREE( p->vFlow.pArray );
413  ABC_FREE( p->vRefs.pArray );
414  if ( p->pPars->fCutMin && !p->pPars->fFuncDsd )
415  {
416  Vec_MemHashFree( p->vTtMem );
417  Vec_MemFree( p->vTtMem );
418  }
419  Vec_IntFreeP( &p->vCnfs );
420  Vec_SetFree_( &p->pMem );
421  Vec_IntFreeP( &p->vTemp );
422  ABC_FREE( p );
423 }
424 
425 /**Function*************************************************************
426 
427  Synopsis [Cut functions.]
428 
429  Description []
430 
431  SideEffects []
432 
433  SeeAlso []
434 
435 ***********************************************************************/
436 static inline void Jf_CutPrint( int * pCut )
437 {
438  int i;
439  printf( "%d {", Jf_CutSize(pCut) );
440  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
441  printf( " %d", Jf_CutLit(pCut, i) );
442  printf( " } Func = %d\n", Jf_CutFunc(pCut) );
443 }
444 static inline void Jf_ObjCutPrint( int * pCuts )
445 {
446  int i, * pCut;
447  Jf_ObjForEachCut( pCuts, pCut, i )
448  Jf_CutPrint( pCut );
449  printf( "\n" );
450 }
451 static inline void Jf_ObjBestCutConePrint( Jf_Man_t * p, Gia_Obj_t * pObj )
452 {
453  int * pCut = Jf_ObjCutBest( p, Gia_ObjId(p->pGia, pObj) );
454  printf( "Best cut of node %d : ", Gia_ObjId(p->pGia, pObj) );
455  Jf_CutPrint( pCut );
456  Gia_ManPrintCone( p->pGia, pObj, Jf_CutLits(pCut), Jf_CutSize(pCut), p->vTemp );
457 }
458 static inline void Jf_CutCheck( int * pCut )
459 {
460  int i, k;
461  for ( i = 2; i <= Jf_CutSize(pCut); i++ )
462  for ( k = 1; k < i; k++ )
463  assert( Jf_CutLit(pCut, i) != Jf_CutLit(pCut, k) );
464 }
465 static inline int Jf_CountBitsSimple( unsigned n )
466 {
467  int i, Count = 0;
468  for ( i = 0; i < 32; i++ )
469  Count += ((n >> i) & 1);
470  return Count;
471 }
472 static inline int Jf_CountBits32( unsigned i )
473 {
474  i = i - ((i >> 1) & 0x55555555);
475  i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
476  i = ((i + (i >> 4)) & 0x0F0F0F0F);
477  return (i*(0x01010101))>>24;
478 }
479 static inline int Jf_CountBits( word i )
480 {
481  i = i - ((i >> 1) & 0x5555555555555555);
482  i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
483  i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
484  return (i*(0x0101010101010101))>>56;
485 }
486 static inline unsigned Jf_CutGetSign32( int * pCut )
487 {
488  unsigned Sign = 0; int i;
489  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
490  Sign |= 1 << (Jf_CutVar(pCut, i) & 0x1F);
491  return Sign;
492 }
493 static inline word Jf_CutGetSign( int * pCut )
494 {
495  word Sign = 0; int i;
496  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
497  Sign |= ((word)1) << (Jf_CutVar(pCut, i) & 0x3F);
498  return Sign;
499 }
500 static inline int Jf_CutArr( Jf_Man_t * p, int * pCut )
501 {
502  int i, Time = 0;
503  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
504  Time = Abc_MaxInt( Time, Jf_ObjArr(p, Jf_CutVar(pCut, i)) );
505  return Time + 1;
506 }
507 
508 static inline void Jf_ObjSetBestCut( int * pCuts, int * pCut, Vec_Int_t * vTemp )
509 {
510  assert( pCuts < pCut );
511  if ( ++pCuts < pCut )
512  {
513  int nBlock = pCut - pCuts;
514  int nSize = Jf_CutSize(pCut) + 1;
515  Vec_IntGrow( vTemp, nBlock );
516  memmove( Vec_IntArray(vTemp), pCuts, sizeof(int) * nBlock );
517  memmove( pCuts, pCut, sizeof(int) * nSize );
518  memmove( pCuts + nSize, Vec_IntArray(vTemp), sizeof(int) * nBlock );
519  }
520 }
521 static inline void Jf_CutRef( Jf_Man_t * p, int * pCut )
522 {
523  int i;
524  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
525  Gia_ObjRefIncId( p->pGia, Jf_CutVar(pCut, i) );
526 }
527 static inline void Jf_CutDeref( Jf_Man_t * p, int * pCut )
528 {
529  int i;
530  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
531  Gia_ObjRefDecId( p->pGia, Jf_CutVar(pCut, i) );
532 }
533 static inline float Jf_CutFlow( Jf_Man_t * p, int * pCut )
534 {
535  float Flow = 0; int i;
536  for ( i = 1; i <= Jf_CutSize(pCut); i++ )
537  Flow += Jf_ObjFlow( p, Jf_CutVar(pCut, i) );
538  assert( Flow >= 0 );
539  return Flow;
540 }
541 
542 /**Function*************************************************************
543 
544  Synopsis [Cut merging.]
545 
546  Description []
547 
548  SideEffects []
549 
550  SeeAlso []
551 
552 ***********************************************************************/
553 static inline int Jf_CutIsContainedOrder( int * pBase, int * pCut ) // check if pCut is contained pBase
554 {
555  int nSizeB = Jf_CutSize(pBase);
556  int nSizeC = Jf_CutSize(pCut);
557  int i, k;
558  if ( nSizeB == nSizeC )
559  {
560  for ( i = 1; i <= nSizeB; i++ )
561  if ( pBase[i] != pCut[i] )
562  return 0;
563  return 1;
564  }
565  assert( nSizeB > nSizeC );
566  for ( i = k = 1; i <= nSizeB; i++ )
567  {
568  if ( pBase[i] > pCut[k] )
569  return 0;
570  if ( pBase[i] == pCut[k] )
571  {
572  if ( k++ == nSizeC )
573  return 1;
574  }
575  }
576  return 0;
577 }
578 static inline int Jf_CutMergeOrder( int * pCut0, int * pCut1, int * pCut, int LutSize )
579 {
580  int nSize0 = Jf_CutSize(pCut0);
581  int nSize1 = Jf_CutSize(pCut1);
582  int * pC0 = pCut0 + 1;
583  int * pC1 = pCut1 + 1;
584  int * pC = pCut + 1;
585  int i, k, c, s;
586  // the case of the largest cut sizes
587  if ( nSize0 == LutSize && nSize1 == LutSize )
588  {
589  for ( i = 0; i < nSize0; i++ )
590  {
591  if ( pC0[i] != pC1[i] )
592  return 0;
593  pC[i] = pC0[i];
594  }
595  pCut[0] = LutSize;
596  return 1;
597  }
598  // compare two cuts with different numbers
599  i = k = c = s = 0;
600  if ( nSize0 == 0 ) goto FlushCut1;
601  if ( nSize1 == 0 ) goto FlushCut0;
602  while ( 1 )
603  {
604  if ( c == LutSize ) return 0;
605  if ( pC0[i] < pC1[k] )
606  {
607  pC[c++] = pC0[i++];
608  if ( i >= nSize0 ) goto FlushCut1;
609  }
610  else if ( pC0[i] > pC1[k] )
611  {
612  pC[c++] = pC1[k++];
613  if ( k >= nSize1 ) goto FlushCut0;
614  }
615  else
616  {
617  pC[c++] = pC0[i++]; k++;
618  if ( i >= nSize0 ) goto FlushCut1;
619  if ( k >= nSize1 ) goto FlushCut0;
620  }
621  }
622 
623 FlushCut0:
624  if ( c + nSize0 > LutSize + i ) return 0;
625  while ( i < nSize0 )
626  pC[c++] = pC0[i++];
627  pCut[0] = c;
628  return 1;
629 
630 FlushCut1:
631  if ( c + nSize1 > LutSize + k ) return 0;
632  while ( k < nSize1 )
633  pC[c++] = pC1[k++];
634  pCut[0] = c;
635  return 1;
636 }
637 
638 /**Function*************************************************************
639 
640  Synopsis [Cut merging.]
641 
642  Description []
643 
644  SideEffects []
645 
646  SeeAlso []
647 
648 ***********************************************************************/
649 static inline int Jf_CutFindLeaf0( int * pCut, int iObj )
650 {
651  int i, nLits = Jf_CutSize(pCut);
652  for ( i = 1; i <= nLits; i++ )
653  if ( pCut[i] == iObj )
654  return i;
655  return i;
656 }
657 static inline int Jf_CutIsContained0( int * pBase, int * pCut ) // check if pCut is contained pBase
658 {
659  int i, nLits = Jf_CutSize(pCut);
660  for ( i = 1; i <= nLits; i++ )
661  if ( Jf_CutFindLeaf0(pBase, pCut[i]) > pBase[0] )
662  return 0;
663  return 1;
664 }
665 static inline int Jf_CutMerge0( int * pCut0, int * pCut1, int * pCut, int LutSize )
666 {
667  int nSize0 = Jf_CutSize(pCut0);
668  int nSize1 = Jf_CutSize(pCut1), i;
669  pCut[0] = nSize0;
670  for ( i = 1; i <= nSize1; i++ )
671  if ( Jf_CutFindLeaf0(pCut0, pCut1[i]) > nSize0 )
672  {
673  if ( pCut[0] == LutSize )
674  return 0;
675  pCut[++pCut[0]] = pCut1[i];
676  }
677  memcpy( pCut + 1, pCut0 + 1, sizeof(int) * nSize0 );
678  return 1;
679 }
680 
681 /**Function*************************************************************
682 
683  Synopsis [Cut merging.]
684 
685  Description []
686 
687  SideEffects []
688 
689  SeeAlso []
690 
691 ***********************************************************************/
692 static inline int Jf_CutFindLeaf1( int * pCut, int iLit )
693 {
694  int i, nLits = Jf_CutSize(pCut);
695  for ( i = 1; i <= nLits; i++ )
696  if ( Abc_Lit2Var(pCut[i]) == iLit )
697  return i;
698  return i;
699 }
700 static inline int Jf_CutIsContained1( int * pBase, int * pCut ) // check if pCut is contained pBase
701 {
702  int i, nLits = Jf_CutSize(pCut);
703  for ( i = 1; i <= nLits; i++ )
704  if ( Jf_CutFindLeaf1(pBase, Abc_Lit2Var(pCut[i])) > pBase[0] )
705  return 0;
706  return 1;
707 }
708 static inline int Jf_CutMerge1( int * pCut0, int * pCut1, int * pCut, int LutSize )
709 {
710  int nSize0 = Jf_CutSize(pCut0);
711  int nSize1 = Jf_CutSize(pCut1), i;
712  pCut[0] = nSize0;
713  for ( i = 1; i <= nSize1; i++ )
714  if ( Jf_CutFindLeaf1(pCut0, Abc_Lit2Var(pCut1[i])) > nSize0 )
715  {
716  if ( pCut[0] == LutSize )
717  return 0;
718  pCut[++pCut[0]] = pCut1[i];
719  }
720  memcpy( pCut + 1, pCut0 + 1, sizeof(int) * nSize0 );
721  return 1;
722 }
723 static inline int Jf_CutMerge2( int * pCut0, int * pCut1, int * pCut, int LutSize )
724 {
725  int ConfigMask = 0x3FFFF; // 18 bits
726  int nSize0 = Jf_CutSize(pCut0);
727  int nSize1 = Jf_CutSize(pCut1);
728  int i, iPlace;
729  pCut[0] = nSize0;
730  for ( i = 1; i <= nSize1; i++ )
731  {
732  iPlace = Jf_CutFindLeaf1(pCut0, Abc_Lit2Var(pCut1[i]));
733  if ( iPlace > nSize0 )
734  {
735  if ( pCut[0] == LutSize )
736  return 0;
737  pCut[(iPlace = ++pCut[0])] = pCut1[i];
738  }
739  else if ( pCut0[iPlace] != pCut1[i] )
740  ConfigMask |= (1 << (iPlace+17));
741  ConfigMask ^= (((i-1) ^ 7) << (3*(iPlace-1)));
742  }
743  memcpy( pCut + 1, pCut0 + 1, sizeof(int) * nSize0 );
744  return ConfigMask;
745 }
746 
747 
748 /**Function*************************************************************
749 
750  Synopsis [Cut filtering.]
751 
752  Description [Returns the number of cuts after filtering and the last
753  cut in the last entry. If the cut is filtered, its size is set to -1.]
754 
755  SideEffects [This was found to be 15% slower.]
756 
757  SeeAlso []
758 
759 ***********************************************************************/
760 int Jf_ObjCutFilterBoth( Jf_Man_t * p, Jf_Cut_t ** pSto, int c )
761 {
762  int k, last;
763  // filter this cut using other cuts
764  for ( k = 0; k < c; k++ )
765  if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
766  (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
767  Jf_CutIsContained1(pSto[c]->pCut, pSto[k]->pCut) )
768  {
769  pSto[c]->pCut[0] = -1;
770  return c;
771  }
772  // filter other cuts using this cut
773  for ( k = last = 0; k < c; k++ )
774  if ( !(pSto[c]->pCut[0] < pSto[k]->pCut[0] &&
775  (pSto[c]->Sign & pSto[k]->Sign) == pSto[c]->Sign &&
776  Jf_CutIsContained1(pSto[k]->pCut, pSto[c]->pCut)) )
777  {
778  if ( last++ == k )
779  continue;
780  ABC_SWAP( Jf_Cut_t *, pSto[last-1], pSto[k] );
781  }
782  assert( last <= c );
783  if ( last < c )
784  ABC_SWAP( Jf_Cut_t *, pSto[last], pSto[c] );
785  return last;
786 }
787 int Jf_ObjCutFilter( Jf_Man_t * p, Jf_Cut_t ** pSto, int c )
788 {
789  int k;
790  if ( p->pPars->fCutMin )
791  {
792  for ( k = 0; k < c; k++ )
793  if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
794  (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
795  Jf_CutIsContained1(pSto[c]->pCut, pSto[k]->pCut) )
796  return 0;
797  }
798  else
799  {
800  for ( k = 0; k < c; k++ )
801  if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
802  (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
803  Jf_CutIsContainedOrder(pSto[c]->pCut, pSto[k]->pCut) )
804  return 0;
805  }
806  return 1;
807 }
808 
809 /**Function*************************************************************
810 
811  Synopsis [Sorting cuts by size.]
812 
813  Description []
814 
815  SideEffects [Did not really help.]
816 
817  SeeAlso []
818 
819 ***********************************************************************/
820 static inline void Jf_ObjSortCuts( Jf_Cut_t ** pSto, int nSize )
821 {
822  int i, j, best_i;
823  for ( i = 0; i < nSize-1; i++ )
824  {
825  best_i = i;
826  for ( j = i+1; j < nSize; j++ )
827  if ( pSto[j]->pCut[0] < pSto[best_i]->pCut[0] )
828  best_i = j;
829  ABC_SWAP( Jf_Cut_t *, pSto[i], pSto[best_i] );
830  }
831 }
832 
833 /**Function*************************************************************
834 
835  Synopsis [Reference counting.]
836 
837  Description []
838 
839  SideEffects []
840 
841  SeeAlso []
842 
843 ***********************************************************************/
844 int Jf_CutRef_rec( Jf_Man_t * p, int * pCut )
845 {
846  int i, Var, Count = Jf_CutCost(pCut);
847  Jf_CutForEachVar( pCut, Var, i )
848  if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
849  Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var) );
850  return Count;
851 }
852 int Jf_CutDeref_rec( Jf_Man_t * p, int * pCut )
853 {
854  int i, Var, Count = Jf_CutCost(pCut);
855  Jf_CutForEachVar( pCut, Var, i )
856  if ( !Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
857  Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var) );
858  return Count;
859 }
860 static inline int Jf_CutAreaOld( Jf_Man_t * p, int * pCut )
861 {
862  int Ela1, Ela2;
863  Ela1 = Jf_CutRef_rec( p, pCut );
864  Ela2 = Jf_CutDeref_rec( p, pCut );
865  assert( Ela1 == Ela2 );
866  return Ela1;
867 }
868 
869 int Jf_CutAreaRef_rec( Jf_Man_t * p, int * pCut )
870 {
871  int i, Var, Count = Jf_CutCost(pCut);
872  Jf_CutForEachVar( pCut, Var, i )
873  {
874  if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
875  Count += Jf_CutAreaRef_rec( p, Jf_ObjCutBest(p, Var) );
876  Vec_IntPush( p->vTemp, Var );
877  }
878  return Count;
879 }
880 int Jf_CutAreaRefEdge_rec( Jf_Man_t * p, int * pCut )
881 {
882  int i, Var, Count = (Jf_CutCost(pCut) << 4) | Jf_CutSize(pCut);
883  Jf_CutForEachVar( pCut, Var, i )
884  {
885  if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
886  Count += Jf_CutAreaRefEdge_rec( p, Jf_ObjCutBest(p, Var) );
887  Vec_IntPush( p->vTemp, Var );
888  }
889  return Count;
890 }
891 static inline int Jf_CutArea( Jf_Man_t * p, int * pCut, int fEdge )
892 {
893  int Ela, Entry, i;
894  Vec_IntClear( p->vTemp );
895  if ( fEdge )
896  Ela = Jf_CutAreaRefEdge_rec( p, pCut );
897  else
898  Ela = Jf_CutAreaRef_rec( p, pCut );
899  Vec_IntForEachEntry( p->vTemp, Entry, i )
900  Gia_ObjRefDecId( p->pGia, Entry );
901  return Ela;
902 }
903 // returns 1 if MFFC size is less than limit
904 int Jf_CutCheckMffc_rec( Jf_Man_t * p, int * pCut, int Limit )
905 {
906  int i, Var;
907  Jf_CutForEachVar( pCut, Var, i )
908  {
909  int fRecur = (!Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var));
910  Vec_IntPush( p->vTemp, Var );
911  if ( Vec_IntSize(p->vTemp) >= Limit )
912  return 0;
913  if ( fRecur && !Jf_CutCheckMffc_rec( p, Jf_ObjCutBest(p, Var), Limit ) )
914  return 0;
915  }
916  return 1;
917 }
918 static inline int Jf_CutCheckMffc( Jf_Man_t * p, int * pCut, int Limit )
919 {
920  int RetValue, Entry, i;
921  Vec_IntClear( p->vTemp );
922  RetValue = Jf_CutCheckMffc_rec( p, pCut, Limit );
923  Vec_IntForEachEntry( p->vTemp, Entry, i )
924  Gia_ObjRefIncId( p->pGia, Entry );
925  return RetValue;
926 }
927 
928 /**Function*************************************************************
929 
930  Synopsis [Comparison procedures.]
931 
932  Description [Return positive value if the new cut is better than the old cut.]
933 
934  SideEffects []
935 
936  SeeAlso []
937 
938 ***********************************************************************/
939 float Jf_CutCompareDelay( Jf_Cut_t * pOld, Jf_Cut_t * pNew )
940 {
941  if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time;
942  if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0];
943  if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow;
944  return 0;
945 }
946 float Jf_CutCompareArea( Jf_Cut_t * pOld, Jf_Cut_t * pNew )
947 {
948 // float Epsilon = (float)0.001;
949 // if ( pOld->Flow > pNew->Flow + Epsilon ) return 1;
950 // if ( pOld->Flow < pNew->Flow - Epsilon ) return -1;
951  if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow;
952  if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0];
953  if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time;
954  return 0;
955 }
956 static inline int Jf_ObjAddCutToStore( Jf_Man_t * p, Jf_Cut_t ** pSto, int c, int cMax )
957 {
958  Jf_Cut_t * pTemp;
959  int k, last, iPivot;
960  // if the store is empty, add anything
961  if ( c == 0 )
962  return 1;
963  // special case when the cut store is full and last cut is better than new cut
964  if ( c == cMax && p->pCutCmp(pSto[c-1], pSto[c]) <= 0 )
965  return c;
966  // find place of the given cut in the store
967  assert( c <= cMax );
968  for ( iPivot = c-1; iPivot >= 0; iPivot-- )
969  if ( p->pCutCmp(pSto[iPivot], pSto[c]) < 0 ) // iPivot-th cut is better than new cut
970  break;
971  // filter this cut using other cuts
972  if ( p->pPars->fCutMin )
973  {
974  for ( k = 0; k <= iPivot; k++ )
975  if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
976  (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
977  Jf_CutIsContained1(pSto[c]->pCut, pSto[k]->pCut) )
978  return c;
979  }
980  else
981  {
982  for ( k = 0; k <= iPivot; k++ )
983  if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
984  (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
985  Jf_CutIsContainedOrder(pSto[c]->pCut, pSto[k]->pCut) )
986  return c;
987  }
988  // insert this cut after iPivot
989  pTemp = pSto[c];
990  for ( ++iPivot, k = c++; k > iPivot; k-- )
991  pSto[k] = pSto[k-1];
992  pSto[iPivot] = pTemp;
993  // filter other cuts using this cut
994  if ( p->pPars->fCutMin )
995  {
996  for ( k = last = iPivot+1; k < c; k++ )
997  if ( !(pSto[iPivot]->pCut[0] <= pSto[k]->pCut[0] &&
998  (pSto[iPivot]->Sign & pSto[k]->Sign) == pSto[iPivot]->Sign &&
999  Jf_CutIsContained1(pSto[k]->pCut, pSto[iPivot]->pCut)) )
1000  {
1001  if ( last++ == k )
1002  continue;
1003  ABC_SWAP( Jf_Cut_t *, pSto[last-1], pSto[k] );
1004  }
1005  }
1006  else
1007  {
1008  for ( k = last = iPivot+1; k < c; k++ )
1009  if ( !(pSto[iPivot]->pCut[0] <= pSto[k]->pCut[0] &&
1010  (pSto[iPivot]->Sign & pSto[k]->Sign) == pSto[iPivot]->Sign &&
1011  Jf_CutIsContainedOrder(pSto[k]->pCut, pSto[iPivot]->pCut)) )
1012  {
1013  if ( last++ == k )
1014  continue;
1015  ABC_SWAP( Jf_Cut_t *, pSto[last-1], pSto[k] );
1016  }
1017  }
1018  c = last;
1019  // remove the last cut if too many
1020  if ( c == cMax + 1 )
1021  return c - 1;
1022  return c;
1023 }
1024 static inline void Jf_ObjPrintStore( Jf_Man_t * p, Jf_Cut_t ** pSto, int c )
1025 {
1026  int i;
1027  for ( i = 0; i < c; i++ )
1028  {
1029  printf( "Flow =%9.5f ", pSto[i]->Flow );
1030  printf( "Time = %5d ", pSto[i]->Time );
1031  printf( "Func = %5d ", pSto[i]->iFunc );
1032  printf( " " );
1033  Jf_CutPrint( pSto[i]->pCut );
1034  }
1035  printf( "\n" );
1036 }
1037 static inline void Jf_ObjCheckPtrs( Jf_Cut_t ** pSto, int c )
1038 {
1039  int i, k;
1040  for ( i = 1; i < c; i++ )
1041  for ( k = 0; k < i; k++ )
1042  assert( pSto[k] != pSto[i] );
1043 }
1044 static inline void Jf_ObjCheckStore( Jf_Man_t * p, Jf_Cut_t ** pSto, int c, int iObj )
1045 {
1046  int i, k;
1047  for ( i = 1; i < c; i++ )
1048  assert( p->pCutCmp(pSto[i-1], pSto[i]) <= 0 );
1049  for ( i = 1; i < c; i++ )
1050  for ( k = 0; k < i; k++ )
1051  {
1052  assert( !Jf_CutIsContained1(pSto[k]->pCut, pSto[i]->pCut) );
1053  assert( !Jf_CutIsContained1(pSto[i]->pCut, pSto[k]->pCut) );
1054  }
1055 }
1056 
1057 /**Function*************************************************************
1058 
1059  Synopsis [Cut minimization.]
1060 
1061  Description []
1062 
1063  SideEffects []
1064 
1065  SeeAlso []
1066 
1067 ***********************************************************************/
1068 int Jf_TtComputeForCut( Jf_Man_t * p, int iFuncLit0, int iFuncLit1, int * pCut0, int * pCut1, int * pCutOut )
1069 {
1070  word uTruth[JF_WORD_MAX], uTruth0[JF_WORD_MAX], uTruth1[JF_WORD_MAX];
1071  int fCompl, truthId;
1072  int LutSize = p->pPars->nLutSize;
1074  word * pTruth0 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit0));
1075  word * pTruth1 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit1));
1076  Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(iFuncLit0) );
1077  Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(iFuncLit1) );
1078  Abc_TtExpand( uTruth0, LutSize, pCut0 + 1, Jf_CutSize(pCut0), pCutOut + 1, Jf_CutSize(pCutOut) );
1079  Abc_TtExpand( uTruth1, LutSize, pCut1 + 1, Jf_CutSize(pCut1), pCutOut + 1, Jf_CutSize(pCutOut) );
1080  fCompl = (int)(uTruth0[0] & uTruth1[0] & 1);
1081  Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, fCompl );
1082  pCutOut[0] = Abc_TtMinBase( uTruth, pCutOut + 1, pCutOut[0], LutSize );
1083  assert( (uTruth[0] & 1) == 0 );
1084  truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
1085  return Abc_Var2Lit( truthId, fCompl );
1086 }
1087 
1088 /**Function*************************************************************
1089 
1090  Synopsis [Cut enumeration.]
1091 
1092  Description []
1093 
1094  SideEffects []
1095 
1096  SeeAlso []
1097 
1098 ***********************************************************************/
1099 static inline void Jf_ObjAssignCut( Jf_Man_t * p, Gia_Obj_t * pObj )
1100 {
1101  int iObj = Gia_ObjId(p->pGia, pObj);
1102  int pClause[3] = { 1, Jf_CutSetAll(2, 0, 1), Jf_ObjLit(iObj, 0) }; // set function
1103  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) );
1104  Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend( &p->pMem, pClause, 3 ) );
1105 }
1106 static inline void Jf_ObjPropagateBuf( Jf_Man_t * p, Gia_Obj_t * pObj, int fReverse )
1107 {
1108  int iObj = Gia_ObjId( p->pGia, pObj );
1109  int iFanin = Gia_ObjFaninId0( pObj, iObj );
1110  assert( 0 );
1111  assert( Gia_ObjIsBuf(pObj) );
1112  if ( fReverse )
1113  ABC_SWAP( int, iObj, iFanin );
1114  Vec_IntWriteEntry( &p->vArr, iObj, Jf_ObjArr(p, iFanin) );
1115  Vec_FltWriteEntry( &p->vFlow, iObj, Jf_ObjFlow(p, iFanin) );
1116 }
1117 static inline int Jf_ObjHasCutWithSize( Jf_Cut_t ** pSto, int c, int nSize )
1118 {
1119  int i;
1120  for ( i = 0; i < c; i++ )
1121  if ( pSto[i]->pCut[0] <= nSize )
1122  return 1;
1123  return 0;
1124 }
1125 void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
1126 {
1127  int LutSize = p->pPars->nLutSize;
1128  int CutNum = p->pPars->nCutNum;
1129  int iObj = Gia_ObjId(p->pGia, pObj);
1130  word Sign0[JF_CUT_MAX+2]; // signatures of the first cut
1131  word Sign1[JF_CUT_MAX+2]; // signatures of the second cut
1132  Jf_Cut_t Sto[JF_CUT_MAX+2]; // cut storage
1133  Jf_Cut_t * pSto[JF_CUT_MAX+2]; // pointers to cut storage
1134  int * pCut0, * pCut1, * pCuts0, * pCuts1;
1135  int nOldSupp, Config, i, k, c = 0;
1136  // prepare cuts
1137  for ( i = 0; i <= CutNum+1; i++ )
1138  pSto[i] = Sto + i, pSto[i]->Cost = 0, pSto[i]->iFunc = ~0;
1139  // compute signatures
1140  pCuts0 = Jf_ObjCuts( p, Gia_ObjFaninId0(pObj, iObj) );
1141  Jf_ObjForEachCut( pCuts0, pCut0, i )
1142  Sign0[i] = Jf_CutGetSign( pCut0 );
1143  // compute signatures
1144  pCuts1 = Jf_ObjCuts( p, Gia_ObjFaninId1(pObj, iObj) );
1145  Jf_ObjForEachCut( pCuts1, pCut1, i )
1146  Sign1[i] = Jf_CutGetSign( pCut1 );
1147  // merge cuts
1148  p->CutCount[0] += pCuts0[0] * pCuts1[0];
1149  Jf_ObjForEachCut( pCuts0, pCut0, i )
1150  Jf_ObjForEachCut( pCuts1, pCut1, k )
1151  {
1152  if ( Jf_CountBits(Sign0[i] | Sign1[k]) > LutSize )
1153  continue;
1154  p->CutCount[1]++;
1155  if ( !p->pPars->fCutMin )
1156  {
1157  if ( !Jf_CutMergeOrder(pCut0, pCut1, pSto[c]->pCut, LutSize) )
1158  continue;
1159  pSto[c]->Sign = Sign0[i] | Sign1[k];
1160  }
1161  else if ( p->pPars->fFuncDsd )
1162  {
1163  if ( !(Config = Jf_CutMerge2(pCut0, pCut1, pSto[c]->pCut, LutSize)) )
1164  continue;
1165  pSto[c]->Sign = Sign0[i] | Sign1[k];
1166  nOldSupp = pSto[c]->pCut[0];
1167  pSto[c]->iFunc = Sdm_ManComputeFunc( p->pDsd, Jf_ObjFunc0(pObj, pCut0), Jf_ObjFunc1(pObj, pCut1), pSto[c]->pCut, Config, 0 );
1168  if ( pSto[c]->iFunc == -1 )
1169  continue;
1170  if ( p->pPars->fGenCnf && Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[c]->iFunc)) >= 12 ) // no more than 15
1171  continue;
1172  assert( pSto[c]->pCut[0] <= nOldSupp );
1173  if ( pSto[c]->pCut[0] < nOldSupp )
1174  pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut );
1175  }
1176  else
1177  {
1178  if ( !Jf_CutMergeOrder(pCut0, pCut1, pSto[c]->pCut, LutSize) )
1179  continue;
1180  pSto[c]->Sign = Sign0[i] | Sign1[k];
1181  nOldSupp = pSto[c]->pCut[0];
1182  pSto[c]->iFunc = Jf_TtComputeForCut( p, Jf_ObjFunc0(pObj, pCut0), Jf_ObjFunc1(pObj, pCut1), pCut0, pCut1, pSto[c]->pCut );
1183  assert( pSto[c]->pCut[0] <= nOldSupp );
1184  if ( pSto[c]->pCut[0] < nOldSupp )
1185  pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut );
1186  if ( pSto[c]->iFunc >= (1 << 24) )
1187  printf( "Hard limit on the number of different Boolean functions (2^23) is reached. Quitting...\n" ), exit(1);
1188  }
1189  p->CutCount[2]++;
1190  pSto[c]->Time = p->pPars->fAreaOnly ? 0 : Jf_CutArr(p, pSto[c]->pCut);
1191  pSto[c]->Flow = Jf_CutFlow(p, pSto[c]->pCut);
1192  c = Jf_ObjAddCutToStore( p, pSto, c, CutNum );
1193  assert( c <= CutNum );
1194  }
1195 // Jf_ObjPrintStore( p, pSto, c );
1196 // Jf_ObjCheckStore( p, pSto, c, iObj );
1197  // add two variable cut
1198  if ( !Jf_ObjIsUnit(pObj) && !Jf_ObjHasCutWithSize(pSto, c, 2) )
1199  {
1201  if ( p->pPars->fCutMin ) pSto[c]->iFunc = 4; // set function (DSD only!)
1202  pSto[c]->pCut[0] = 2;
1203  pSto[c]->pCut[1] = Jf_ObjLit(Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj));
1204  pSto[c]->pCut[2] = Jf_ObjLit(Gia_ObjFaninId1(pObj, iObj), Gia_ObjFaninC1(pObj));
1205  c++;
1206  }
1207  // add elementary cut
1208  if ( Jf_ObjIsUnit(pObj) && !(p->pPars->fCutMin && Jf_ObjHasCutWithSize(pSto, c, 1)) )
1209  {
1210  if ( p->pPars->fCutMin ) pSto[c]->iFunc = 2; // set function
1211  pSto[c]->pCut[0] = 1;
1212  pSto[c]->pCut[1] = Jf_ObjLit(iObj, 0);
1213  c++;
1214  }
1215  // reorder cuts
1216 // Jf_ObjSortCuts( pSto + 1, c - 1 );
1217 // Jf_ObjCheckPtrs( pSto, CutNum );
1218  // find cost of the best cut
1219  pSto[0]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[0]->iFunc)) : 1;
1220  assert( pSto[0]->Cost >= 0 );
1221  // save best info
1222  assert( pSto[0]->Flow >= 0 );
1223  Vec_IntWriteEntry( &p->vArr, iObj, pSto[0]->Time );
1224  Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : pSto[0]->Cost)) / Jf_ObjRefs(p, iObj) );
1225  // add cuts to storage cuts
1226  Vec_IntClear( p->vTemp );
1227  Vec_IntPush( p->vTemp, c );
1228  for ( i = 0; i < c; i++ )
1229  {
1230  pSto[i]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[i]->iFunc)) : 1;
1231  Vec_IntPush( p->vTemp, Jf_CutSetAll(pSto[i]->iFunc, pSto[i]->Cost, pSto[i]->pCut[0]) );
1232  for ( k = 1; k <= pSto[i]->pCut[0]; k++ )
1233  Vec_IntPush( p->vTemp, pSto[i]->pCut[k] );
1234  }
1236  p->CutCount[3] += c;
1237 }
1238 void Jf_ManComputeCuts( Jf_Man_t * p, int fEdge )
1239 {
1240  Gia_Obj_t * pObj; int i;
1241  if ( p->pPars->fVerbose )
1242  {
1243  printf( "Aig: CI = %d CO = %d AND = %d ", Gia_ManCiNum(p->pGia), Gia_ManCoNum(p->pGia), Gia_ManAndNum(p->pGia) );
1244  printf( "LutSize = %d CutMax = %d Rounds = %d\n", p->pPars->nLutSize, p->pPars->nCutNum, p->pPars->nRounds );
1245  printf( "Computing cuts...\r" );
1246  fflush( stdout );
1247  }
1248  Gia_ManForEachObj( p->pGia, pObj, i )
1249  {
1250  if ( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) )
1251  Jf_ObjAssignCut( p, pObj );
1252  if ( Gia_ObjIsBuf(pObj) )
1253  Jf_ObjPropagateBuf( p, pObj, 0 );
1254  else if ( Gia_ObjIsAnd(pObj) )
1255  Jf_ObjComputeCuts( p, pObj, fEdge );
1256  }
1257  if ( p->pPars->fVerbose )
1258  {
1259  printf( "CutPair = %lu ", p->CutCount[0] );
1260  printf( "Merge = %lu ", p->CutCount[1] );
1261  printf( "Eval = %lu ", p->CutCount[2] );
1262  printf( "Cut = %lu ", p->CutCount[3] );
1263  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1264  printf( "Memory: " );
1265  printf( "Gia = %.2f MB ", Gia_ManMemory(p->pGia) / (1<<20) );
1266  printf( "Man = %.2f MB ", 6.0 * sizeof(int) * Gia_ManObjNum(p->pGia) / (1<<20) );
1267  printf( "Cuts = %.2f MB", Vec_ReportMemory(&p->pMem) / (1<<20) );
1268  if ( p->nCoarse )
1269  printf( " Coarse = %d (%.1f %%)", p->nCoarse, 100.0 * p->nCoarse / Gia_ManObjNum(p->pGia) );
1270  printf( "\n" );
1271  fflush( stdout );
1272  }
1273 }
1274 
1275 
1276 /**Function*************************************************************
1277 
1278  Synopsis [Computing delay/area.]
1279 
1280  Description []
1281 
1282  SideEffects []
1283 
1284  SeeAlso []
1285 
1286 ***********************************************************************/
1287 int Jf_ManComputeDelay( Jf_Man_t * p, int fEval )
1288 {
1289  Gia_Obj_t * pObj;
1290  int i, Delay = 0;
1291  if ( fEval )
1292  {
1293  Gia_ManForEachObj( p->pGia, pObj, i )
1294  if ( Gia_ObjIsBuf(pObj) )
1295  Jf_ObjPropagateBuf( p, pObj, 0 );
1296  else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1297  Vec_IntWriteEntry( &p->vArr, i, Jf_CutArr(p, Jf_ObjCutBest(p, i)) );
1298  }
1299  Gia_ManForEachCoDriver( p->pGia, pObj, i )
1300  {
1301  assert( Gia_ObjRefNum(p->pGia, pObj) > 0 );
1302  Delay = Abc_MaxInt( Delay, Jf_ObjArr(p, Gia_ObjId(p->pGia, pObj)) );
1303  }
1304  return Delay;
1305 }
1307 {
1308  Gia_Obj_t * pObj;
1309  float nRefsNew; int i, * pCut;
1310  float * pRefs = Vec_FltArray(&p->vRefs);
1311  float * pFlow = Vec_FltArray(&p->vFlow);
1312  assert( p->pGia->pRefs != NULL );
1313  memset( p->pGia->pRefs, 0, sizeof(int) * Gia_ManObjNum(p->pGia) );
1314  p->pPars->Area = p->pPars->Edge = 0;
1315  Gia_ManForEachObjReverse( p->pGia, pObj, i )
1316  {
1317  if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBuf(pObj) )
1318  Gia_ObjRefInc( p->pGia, Gia_ObjFanin0(pObj) );
1319  else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1320  {
1321  assert( Jf_ObjIsUnit(pObj) );
1322  pCut = Jf_ObjCutBest(p, i);
1323  Jf_CutRef( p, pCut );
1324  if ( p->pPars->fGenCnf )
1325  p->pPars->Clause += Jf_CutCnfSize(p, pCut);
1326  p->pPars->Edge += Jf_CutSize(pCut);
1327  p->pPars->Area++;
1328  }
1329  }
1330  // blend references and normalize flow
1331  for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
1332  {
1333  if ( p->pPars->fOptEdge )
1334  nRefsNew = Abc_MaxFloat( 1, 0.8 * pRefs[i] + 0.2 * p->pGia->pRefs[i] );
1335  else
1336  nRefsNew = Abc_MaxFloat( 1, 0.2 * pRefs[i] + 0.8 * p->pGia->pRefs[i] );
1337  pFlow[i] = pFlow[i] * pRefs[i] / nRefsNew;
1338  pRefs[i] = nRefsNew;
1339  assert( pFlow[i] >= 0 );
1340  }
1341  // compute delay
1342  p->pPars->Delay = Jf_ManComputeDelay( p, 1 );
1343  return p->pPars->Area;
1344 }
1345 
1346 /**Function*************************************************************
1347 
1348  Synopsis [Mapping rounds.]
1349 
1350  Description []
1351 
1352  SideEffects []
1353 
1354  SeeAlso []
1355 
1356 ***********************************************************************/
1357 void Jf_ObjComputeBestCut( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge, int fEla )
1358 {
1359  int i, iObj = Gia_ObjId( p->pGia, pObj );
1360  int * pCuts = Jf_ObjCuts( p, iObj );
1361  int * pCut, * pCutBest = NULL;
1362  int Time = ABC_INFINITY, TimeBest = ABC_INFINITY;
1363  float Area, AreaBest = ABC_INFINITY;
1364  Jf_ObjForEachCut( pCuts, pCut, i )
1365  {
1366  if ( Jf_CutIsTriv(pCut, iObj) ) continue;
1367  if ( fEdge && !fEla )
1368  Jf_CutSetCost(pCut, Jf_CutSize(pCut));
1369  Area = fEla ? Jf_CutArea(p, pCut, fEdge) : Jf_CutFlow(p, pCut) + Jf_CutCost(pCut);
1370  if ( pCutBest == NULL || AreaBest > Area || (AreaBest == Area && TimeBest > (Time = Jf_CutArr(p, pCut))) )
1371  pCutBest = pCut, AreaBest = Area, TimeBest = Time;
1372  }
1373  Vec_IntWriteEntry( &p->vArr, iObj, Jf_CutArr(p, pCutBest) );
1374  if ( !fEla )
1375  Vec_FltWriteEntry( &p->vFlow, iObj, AreaBest / Jf_ObjRefs(p, iObj) );
1376  Jf_ObjSetBestCut( pCuts, pCutBest, p->vTemp );
1377 // Jf_CutPrint( Jf_ObjCutBest(p, iObj) ); printf( "\n" );
1378 }
1379 void Jf_ManPropagateFlow( Jf_Man_t * p, int fEdge )
1380 {
1381  Gia_Obj_t * pObj;
1382  int i;
1383  Gia_ManForEachObj( p->pGia, pObj, i )
1384  if ( Gia_ObjIsBuf(pObj) )
1385  Jf_ObjPropagateBuf( p, pObj, 0 );
1386  else if ( Gia_ObjIsAnd(pObj) && Jf_ObjIsUnit(pObj) )
1387  Jf_ObjComputeBestCut( p, pObj, fEdge, 0 );
1388  Jf_ManComputeRefs( p );
1389 }
1390 void Jf_ManPropagateEla( Jf_Man_t * p, int fEdge )
1391 {
1392  Gia_Obj_t * pObj;
1393  int i, CostBef, CostAft;
1394  p->pPars->Area = p->pPars->Edge = p->pPars->Clause = 0;
1395  Gia_ManForEachObjReverse( p->pGia, pObj, i )
1396  if ( Gia_ObjIsBuf(pObj) )
1397  Jf_ObjPropagateBuf( p, pObj, 1 );
1398  else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1399  {
1400  assert( Jf_ObjIsUnit(pObj) );
1401  if ( Jf_CutCheckMffc(p, Jf_ObjCutBest(p, i), 50) )
1402  {
1403  CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i) );
1404  Jf_ObjComputeBestCut( p, pObj, fEdge, 1 );
1405  CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i) );
1406  // if ( CostBef != CostAft ) printf( "%d -> %d ", CostBef, CostAft );
1407  assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM
1408  }
1409  if ( p->pPars->fGenCnf )
1410  p->pPars->Clause += Jf_CutCnfSize(p, Jf_ObjCutBest(p, i));
1411  p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i));
1412  p->pPars->Area++;
1413  }
1414  p->pPars->Delay = Jf_ManComputeDelay( p, 1 );
1415 // printf( "\n" );
1416 }
1417 
1418 /**Function*************************************************************
1419 
1420  Synopsis [Derives the result of mapping.]
1421 
1422  Description []
1423 
1424  SideEffects []
1425 
1426  SeeAlso []
1427 
1428 ***********************************************************************/
1430 {
1431  Gia_Man_t * pNew;
1432  Gia_Obj_t * pObj;
1433  Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
1434  Vec_Int_t * vMapping = Vec_IntStart( 2 * Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + 2 * (int)p->pPars->Area );
1435  Vec_Int_t * vMapping2 = Vec_IntStart( (int)p->pPars->Edge + 2 * (int)p->pPars->Area + 1000 );
1436  Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
1437  Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
1438  Vec_Int_t * vLits = NULL, * vClas = NULL;
1439  int i, k, iLit, Class, * pCut;
1440  word uTruth = 0, * pTruth = &uTruth;
1441  assert( p->pPars->fCutMin );
1442  if ( p->pPars->fGenCnf )
1443  {
1444  vLits = Vec_IntAlloc( 1000 );
1445  vClas = Vec_IntAlloc( 1000 );
1446  Vec_IntPush( vClas, Vec_IntSize(vLits) );
1447  Vec_IntPush( vLits, 1 );
1448  }
1449  // create new manager
1450  pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
1451  pNew->pName = Abc_UtilStrsav( p->pGia->pName );
1452  pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
1453  // map primary inputs
1454  Vec_IntWriteEntry( vCopies, 0, 0 );
1455  Gia_ManForEachCi( p->pGia, pObj, i )
1456  Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
1457  // iterate through nodes used in the mapping
1458  Gia_ManForEachAnd( p->pGia, pObj, i )
1459  {
1460  if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1461  continue;
1462  pCut = Jf_ObjCutBest( p, i );
1463 // printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut);
1464  Class = Jf_CutFuncClass( pCut );
1465  if ( Jf_CutSize(pCut) == 0 )
1466  {
1467  assert( Class == 0 );
1468  Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
1469  continue;
1470  }
1471  if ( Jf_CutSize(pCut) == 1 )
1472  {
1473  assert( Class == 1 );
1474  iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
1475  iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
1476  Vec_IntWriteEntry( vCopies, i, iLit );
1477  continue;
1478  }
1479  if ( p->pPars->fFuncDsd )
1480  uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class);
1481  else
1482  pTruth = Vec_MemReadEntry(p->vTtMem, Class);
1483  assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
1484  // collect leaves
1485  Vec_IntClear( vLeaves );
1486  Jf_CutForEachLit( pCut, iLit, k )
1487  Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
1488  // create GIA
1489  iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
1490  if ( p->pPars->fGenCnf )
1491  Jf_ManGenCnf( uTruth, iLit, vLeaves, vLits, vClas, vCover );
1492  iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
1493  Vec_IntWriteEntry( vCopies, i, iLit );
1494  // create mapping
1495  Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) );
1496  Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
1497  Vec_IntForEachEntry( vLeaves, iLit, k )
1498  Vec_IntPush( vMapping2, Abc_Lit2Var(iLit) );
1499  Vec_IntPush( vMapping2, Abc_Lit2Var(Vec_IntEntry(vCopies, i)) );
1500  }
1501  Gia_ManForEachCo( p->pGia, pObj, i )
1502  {
1503  if ( p->pPars->fGenCnf )
1504  Vec_IntClear( vLeaves );
1505  iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
1506  if ( p->pPars->fGenCnf )
1507  Vec_IntPush( vLeaves, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1508  iLit = Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1509  if ( p->pPars->fGenCnf )
1510  Jf_ManGenCnf( ABC_CONST(0xAAAAAAAAAAAAAAAA), iLit, vLeaves, vLits, vClas, vCover );
1511  }
1512  Vec_IntFree( vCopies );
1513  Vec_IntFree( vCover );
1514  Vec_IntFree( vLeaves );
1515  // finish mapping
1516  if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) )
1517  Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) );
1518  else
1519  Vec_IntFillExtra( vMapping, Gia_ManObjNum(pNew), 0 );
1520  assert( Vec_IntSize(vMapping) == Gia_ManObjNum(pNew) );
1521  Vec_IntForEachEntry( vMapping, iLit, i )
1522  if ( iLit > 0 )
1523  Vec_IntAddToEntry( vMapping, i, Gia_ManObjNum(pNew) );
1524  Vec_IntAppend( vMapping, vMapping2 );
1525  Vec_IntFree( vMapping2 );
1526  // attach mapping and packing
1527  assert( pNew->vMapping == NULL );
1528  pNew->vMapping = vMapping;
1529  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
1530  // derive CNF
1531  if ( p->pPars->fGenCnf )
1532  {
1533  if ( p->pPars->fCnfObjIds )
1534  pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
1535  else
1536  pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas, p->pPars->fAddOrCla );
1537  }
1538  Vec_IntFreeP( &vLits );
1539  Vec_IntFreeP( &vClas );
1540  return pNew;
1541 }
1543 {
1544  Vec_Int_t * vMapping;
1545  Gia_Obj_t * pObj;
1546  int i, k, * pCut;
1547  assert( !p->pPars->fCutMin );
1548  vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + (int)p->pPars->Area * 2 );
1549  Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
1550  Gia_ManForEachAnd( p->pGia, pObj, i )
1551  {
1552  if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1553  continue;
1554  pCut = Jf_ObjCutBest( p, i );
1555  Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
1556  assert( !p->pPars->fCutMin || Jf_CutSize(pCut) <= 6 );
1557  Vec_IntPush( vMapping, Jf_CutSize(pCut) );
1558  for ( k = 1; k <= Jf_CutSize(pCut); k++ )
1559  Vec_IntPush( vMapping, Jf_CutVar(pCut, k) );
1560  Vec_IntPush( vMapping, i );
1561  }
1562  assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
1563  p->pGia->vMapping = vMapping;
1564 // Gia_ManMappingVerify( p->pGia );
1565 }
1566 
1567 /**Function*************************************************************
1568 
1569  Synopsis [Derive GIA without mapping.]
1570 
1571  Description []
1572 
1573  SideEffects []
1574 
1575  SeeAlso []
1576 
1577 ***********************************************************************/
1579 {
1580  Gia_Man_t * pNew, * pTemp;
1581  Gia_Obj_t * pObj;
1582  Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
1583  Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
1584  Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
1585  int i, k, iLit, Class, * pCut;
1587  word uTruth = 0, * pTruth = &uTruth, Truth[JF_WORD_MAX];
1588  // create new manager
1589  pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
1590  pNew->pName = Abc_UtilStrsav( p->pGia->pName );
1591  pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
1592  // map primary inputs
1593  Vec_IntWriteEntry( vCopies, 0, 0 );
1594  Gia_ManForEachCi( p->pGia, pObj, i )
1595  Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
1596  // iterate through nodes used in the mapping
1597  if ( !p->pPars->fCutMin )
1599  Gia_ManHashStart( pNew );
1600  Gia_ManForEachAnd( p->pGia, pObj, i )
1601  {
1602  if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1603  continue;
1604  pCut = Jf_ObjCutBest( p, i );
1605 // printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut);
1606  // get the truth table
1607  if ( p->pPars->fCutMin )
1608  {
1609  Class = Jf_CutFuncClass( pCut );
1610  if ( Jf_CutSize(pCut) == 0 )
1611  {
1612  assert( Class == 0 );
1613  Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
1614  continue;
1615  }
1616  if ( Jf_CutSize(pCut) == 1 )
1617  {
1618  assert( Class == 1 );
1619  iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
1620  iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
1621  Vec_IntWriteEntry( vCopies, i, iLit );
1622  continue;
1623  }
1624  if ( p->pPars->fFuncDsd )
1625  uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class);
1626  else
1627  Abc_TtCopy( (pTruth = Truth), Vec_MemReadEntry(p->vTtMem, Class), nWords, 0 );
1628  assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
1629  }
1630  else
1631  {
1632  Vec_IntClear( vLeaves );
1633  Jf_CutForEachLit( pCut, iLit, k )
1634  Vec_IntPush( vLeaves, Abc_Lit2Var(iLit) );
1635  pTruth = Gia_ObjComputeTruthTableCut( p->pGia, pObj, vLeaves );
1636  }
1637  // collect incoming literals
1638  Vec_IntClear( vLeaves );
1639  Jf_CutForEachLit( pCut, iLit, k )
1640  Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
1641  // create GIA
1642  iLit = Dsm_ManTruthToGia( pNew, pTruth, vLeaves, vCover );
1643  iLit = Abc_LitNotCond( iLit, (p->pPars->fCutMin && Jf_CutFuncCompl(pCut)) );
1644  Vec_IntWriteEntry( vCopies, i, iLit );
1645  }
1646  Gia_ManForEachCo( p->pGia, pObj, i )
1647  {
1648  iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
1649  Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1650  }
1651  if ( !p->pPars->fCutMin )
1653  Vec_IntFree( vCopies );
1654  Vec_IntFree( vLeaves );
1655  Vec_IntFree( vCover );
1656  Gia_ManHashStop( pNew );
1657  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
1658 // Dsm_ManReportStats();
1659  // perform cleanup
1660  if ( !p->pPars->fCutMin )
1661  {
1662  pNew = Gia_ManCleanup( pTemp = pNew );
1663  Gia_ManStop( pTemp );
1664  }
1665  return pNew;
1666 }
1667 
1668 /**Function*************************************************************
1669 
1670  Synopsis []
1671 
1672  Description []
1673 
1674  SideEffects []
1675 
1676  SeeAlso []
1677 
1678 ***********************************************************************/
1680 {
1681  memset( pPars, 0, sizeof(Jf_Par_t) );
1682  pPars->nLutSize = 6;
1683  pPars->nCutNum = 8;
1684  pPars->nRounds = 1;
1685  pPars->nVerbLimit = 5;
1686  pPars->DelayTarget = -1;
1687  pPars->fAreaOnly = 1;
1688  pPars->fOptEdge = 1;
1689  pPars->fCoarsen = 0;
1690  pPars->fCutMin = 0;
1691  pPars->fFuncDsd = 0;
1692  pPars->fGenCnf = 0;
1693  pPars->fPureAig = 0;
1694  pPars->fVerbose = 0;
1695  pPars->fVeryVerbose = 0;
1696  pPars->nLutSizeMax = JF_LEAF_MAX;
1697  pPars->nCutNumMax = JF_CUT_MAX;
1698 }
1699 void Jf_ManPrintStats( Jf_Man_t * p, char * pTitle )
1700 {
1701  if ( !p->pPars->fVerbose )
1702  return;
1703  printf( "%s : ", pTitle );
1704  printf( "Level =%6lu ", p->pPars->Delay );
1705  printf( "Area =%9lu ", p->pPars->Area );
1706  printf( "Edge =%9lu ", p->pPars->Edge );
1707  if ( p->pPars->fGenCnf )
1708  printf( "Cnf =%9lu ", p->pPars->Clause );
1709  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1710  fflush( stdout );
1711 }
1713 {
1714  Gia_Man_t * pNew = pGia;
1715  Jf_Man_t * p; int i;
1716  assert( !Gia_ManBufNum(pGia) );
1717  assert( !pPars->fCutMin || !pPars->fFuncDsd || pPars->nLutSize <= 6 );
1718  if ( pPars->fGenCnf )
1719  pPars->fCutMin = 1, pPars->fFuncDsd = 1, pPars->fOptEdge = 0;
1720  if ( pPars->fCutMin && !pPars->fFuncDsd )
1721  pPars->fCoarsen = 0;
1722  p = Jf_ManAlloc( pGia, pPars );
1724  Jf_ManComputeCuts( p, 0 );
1725  Jf_ManComputeRefs( p ); Jf_ManPrintStats( p, "Start" );
1726  for ( i = 0; i < pPars->nRounds; i++ )
1727  {
1728  if ( !p->pPars->fGenCnf )
1729  {
1730  Jf_ManPropagateFlow( p, pPars->fOptEdge ); Jf_ManPrintStats( p, "Flow " );
1731  }
1732  Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " );
1733  Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " );
1734  }
1735  if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
1737  if ( p->pPars->fPureAig )
1738  pNew = Jf_ManDeriveGia(p);
1739  else if ( p->pPars->fCutMin )
1740  pNew = Jf_ManDeriveMappingGia(p);
1741  else
1743  Jf_ManFree( p );
1744  return pNew;
1745 }
1746 Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds )
1747 {
1748  Jf_Par_t Pars, * pPars = &Pars;
1749  Jf_ManSetDefaultPars( pPars );
1750  pPars->fGenCnf = 1;
1751  pPars->fCnfObjIds = fCnfObjIds;
1752  return Jf_ManPerformMapping( p, pPars );
1753 }
1755 {
1756  Jf_Par_t Pars, * pPars = &Pars;
1757  Jf_ManSetDefaultPars( pPars );
1758  pPars->fGenCnf = 1;
1759  pPars->fCnfObjIds = 0;
1760  pPars->fAddOrCla = 1;
1761  pPars->fVerbose = fVerbose;
1762  return Jf_ManPerformMapping( p, pPars );
1763 }
1764 void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose )
1765 {
1766  abctime clk = Abc_Clock();
1767  Gia_Man_t * pNew;
1768  Cnf_Dat_t * pCnf;
1769  pNew = Jf_ManDeriveCnfMiter( p, fVerbose );
1770  pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
1771  Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
1772  Gia_ManStop( pNew );
1773 // if ( fVerbose )
1774  {
1775  printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
1776  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1777  }
1778  Cnf_DataFree(pCnf);
1779 }
1780 
1782 {
1783  Gia_Man_t * pNew;
1784  Cnf_Dat_t * pCnf;
1785  int i;
1786 // Cnf_Dat_t * pCnf = Cnf_DeriveGia( p );
1787  pNew = Jf_ManDeriveCnf( p, 1 );
1788  pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
1789  Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
1790  for ( i = 0; i < pCnf->nVars; i++ )
1791  printf( "%d : %d %d\n", i, pCnf->pObj2Count[i], pCnf->pObj2Clause[i] );
1792  Gia_ManStop( pNew );
1793  Cnf_DataFree(pCnf);
1794 }
1795 
1796 ////////////////////////////////////////////////////////////////////////
1797 /// END OF FILE ///
1798 ////////////////////////////////////////////////////////////////////////
1799 
1800 
1802 
char * memset()
static void Jf_ObjBestCutConePrint(Jf_Man_t *p, Gia_Obj_t *pObj)
Definition: giaJf.c:451
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static void Gia_ObjRefFanin0Inc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:524
int Jf_ManComputeDelay(Jf_Man_t *p, int fEval)
Definition: giaJf.c:1287
VOID_HACK exit()
Vec_Int_t * vTemp
Definition: giaJf.c:65
#define JF_WORD_MAX
Definition: giaJf.c:37
static void Jf_ObjAssignCut(Jf_Man_t *p, Gia_Obj_t *pObj)
Definition: giaJf.c:1099
static int Jf_ObjHasCutWithSize(Jf_Cut_t **pSto, int c, int nSize)
Definition: giaJf.c:1117
static word Jf_CutGetSign(int *pCut)
Definition: giaJf.c:493
#define Jf_ObjForEachCut(pList, pCut, i)
Definition: giaJf.c:107
Cnf_Dat_t * Jf_ManCreateCnfRemap(Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas, int fAddOrCla)
Definition: giaJf.c:162
Vec_Int_t vDep
Definition: giaJf.c:61
Vec_Int_t * vCnfs
Definition: giaJf.c:57
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
Gia_Man_t * Jf_ManDeriveCnfMiter(Gia_Man_t *p, int fVerbose)
Definition: giaJf.c:1754
static int Jf_CutArea(Jf_Man_t *p, int *pCut, int fEdge)
Definition: giaJf.c:891
static int Jf_CutFuncClass(int *pCut)
Definition: giaJf.c:94
int nCutNum
Definition: gia.h:268
int nLutSize
Definition: gia.h:267
void Sdm_ManPrintDsdStats(Sdm_Man_t *p, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: extraUtilDsd.c:676
int Cost
Definition: giaJf.c:47
static int Abc_TtMinBase(word *pTruth, int *pVars, int nVars, int nVarsAll)
Definition: utilTruth.h:1395
int pCut[JF_LEAF_MAX+2]
Definition: giaJf.c:48
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
word Sign
Definition: giaJf.c:43
static void Vec_FltWriteEntry(Vec_Flt_t *p, int i, float Entry)
Definition: vecFlt.h:364
void Jf_ManGenCnf(word uTruth, int iLitOut, Vec_Int_t *vLeaves, Vec_Int_t *vLits, Vec_Int_t *vClas, Vec_Int_t *vCover)
FUNCTION DEFINITIONS ///.
Definition: giaJf.c:128
static int Jf_CutMerge1(int *pCut0, int *pCut1, int *pCut, int LutSize)
Definition: giaJf.c:708
void Jf_ManProfileClasses(Jf_Man_t *p)
Definition: giaJf.c:307
word Edge
Definition: gia.h:299
static void Jf_CutPrint(int *pCut)
Definition: giaJf.c:436
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
void Gia_ObjComputeTruthTableStart(Gia_Man_t *p, int nVarsMax)
Definition: giaTruth.c:282
static void Jf_CutCheck(int *pCut)
Definition: giaJf.c:458
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
Sdm_Man_t * Sdm_ManRead()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Jf_CutIsTriv(int *pCut, int i)
Definition: giaJf.c:100
Gia_Man_t * Jf_ManDeriveMappingGia(Jf_Man_t *p)
Definition: giaJf.c:1429
static void Jf_ObjCleanUnit(Gia_Obj_t *p)
Definition: giaJf.c:73
static int Jf_CutMerge2(int *pCut0, int *pCut1, int *pCut, int LutSize)
Definition: giaJf.c:723
#define JF_CUT_MAX
Definition: giaJf.c:38
static void Vec_IntFillExtra(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:376
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static void Gia_ObjRefFanin1Inc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:525
static int Jf_CutCost(int *pCut)
Definition: giaJf.c:87
word * Gia_ObjComputeTruthTableCut(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves)
Definition: giaTruth.c:351
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:318
int Jf_CutAreaRefEdge_rec(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:880
static int Jf_CutLit(int *pCut, int i)
Definition: giaJf.c:97
static int Abc_Lit2LitL(int *pMap, int Lit)
Definition: abc_global.h:270
Jf_Par_t * pPars
Definition: giaJf.c:55
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
int nClauses
Definition: cnf.h:61
static void Jf_CutSetSize(int *pCut, int s)
Definition: giaJf.c:90
int Jf_TtComputeForCut(Jf_Man_t *p, int iFuncLit0, int iFuncLit1, int *pCut0, int *pCut1, int *pCutOut)
Definition: giaJf.c:1068
static int Jf_CountBits32(unsigned i)
Definition: giaJf.c:472
static int Abc_Truth6WordNum(int nVars)
Definition: abc_global.h:257
static void Vec_SetAlloc_(Vec_Set_t *p, int nPageSize)
FUNCTION DEFINITIONS ///.
Definition: vecSet.h:115
char * Sdm_ManReadDsdStr(Sdm_Man_t *p, int iDsd)
static float Jf_ObjRefs(Jf_Man_t *p, int i)
Definition: giaJf.c:82
int Time
Definition: giaJf.c:45
static void Jf_ObjPropagateBuf(Jf_Man_t *p, Gia_Obj_t *pObj, int fReverse)
Definition: giaJf.c:1106
void Jf_ManTestCnf(Gia_Man_t *p)
Definition: giaJf.c:1781
static int Jf_CutFindLeaf1(int *pCut, int iLit)
Definition: giaJf.c:692
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
int nVars
Definition: cnf.h:59
static void Jf_ObjCheckPtrs(Jf_Cut_t **pSto, int c)
Definition: giaJf.c:1037
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
int nCutNumMax
Definition: gia.h:294
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static int Gia_ObjRefNumId(Gia_Man_t *p, int Id)
Definition: gia.h:518
void Gia_ObjComputeTruthTableStop(Gia_Man_t *p)
Definition: giaTruth.c:293
int Jf_ManComputeRefs(Jf_Man_t *p)
Definition: giaJf.c:1306
static int Gia_ObjRefDecId(Gia_Man_t *p, int Id)
Definition: gia.h:520
int * pVarNums
Definition: cnf.h:63
static void Jf_ObjSetUnit(Gia_Obj_t *p)
Definition: giaJf.c:74
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition: utilMem.c:35
int Jf_CutDeref_rec(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:852
char * memcpy()
static int Jf_ObjFunc0(Gia_Obj_t *p, int *c)
Definition: giaJf.c:104
static int Gia_ObjRefNum(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:521
static int Vec_MemEntryNum(Vec_Mem_t *p)
Definition: vecMem.h:151
static void Vec_IntSetEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:418
word Clause
Definition: gia.h:300
static int Jf_CountBitsSimple(unsigned n)
Definition: giaJf.c:465
void Jf_ManPrintStats(Jf_Man_t *p, char *pTitle)
Definition: giaJf.c:1699
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int Jf_ObjAddCutToStore(Jf_Man_t *p, Jf_Cut_t **pSto, int c, int cMax)
Definition: giaJf.c:956
static float Jf_ObjFlow(Jf_Man_t *p, int i)
Definition: giaJf.c:81
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
static unsigned Jf_CutGetSign32(int *pCut)
Definition: giaJf.c:486
static float * Vec_FltArray(Vec_Flt_t *p)
Definition: vecFlt.h:274
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
abctime clkStart
Definition: giaJf.c:67
static int Jf_CutMergeOrder(int *pCut0, int *pCut1, int *pCut, int LutSize)
Definition: giaJf.c:578
void Jf_ManComputeCuts(Jf_Man_t *p, int fEdge)
Definition: giaJf.c:1238
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition: giaJf.c:1746
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition: gia.h:994
int fAreaOnly
Definition: gia.h:277
int nVerbLimit
Definition: gia.h:275
int Dsm_ManTruthToGia(void *p, word *pTruth, Vec_Int_t *vLeaves, Vec_Int_t *vCover)
Definition: dauGia.c:415
static int * Jf_ObjCuts(Jf_Man_t *p, int i)
Definition: giaJf.c:77
int fCnfObjIds
Definition: gia.h:285
static int Jf_CutArr(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:500
static abctime Abc_Clock()
Definition: abc_global.h:279
static word * Vec_SetEntry(Vec_Set_t *p, int h)
Definition: vecSet.h:70
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Sdm_Man_t * pDsd
Definition: giaJf.c:56
#define Gia_ManForEachCoDriver(p, pObj, i)
Definition: gia.h:1030
static int Jf_ObjCutH(Jf_Man_t *p, int i)
Definition: giaJf.c:76
Aig_Man_t * pMan
Definition: cnf.h:58
static int Vec_SetAppend(Vec_Set_t *p, int *pArray, int nSize)
Definition: vecSet.h:213
Definition: cnf.h:56
static void Vec_FltFill(Vec_Flt_t *p, int nSize, float Entry)
Definition: vecFlt.h:450
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
int nWords
Definition: abcNpn.c:127
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static float Abc_MaxFloat(float a, float b)
Definition: abc_global.h:243
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
word Sdm_ManReadDsdTruth(Sdm_Man_t *p, int iDsd)
static int Jf_ObjIsUnit(Gia_Obj_t *p)
Definition: giaJf.c:72
int * pRefs
Definition: gia.h:114
Definition: gia.h:75
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
static void Jf_ObjSetBestCut(int *pCuts, int *pCut, Vec_Int_t *vTemp)
Definition: giaJf.c:508
int Jf_ObjCutFilter(Jf_Man_t *p, Jf_Cut_t **pSto, int c)
Definition: giaJf.c:787
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
#define Jf_CutForEachLit(pCut, Lit, i)
Definition: giaJf.c:108
static int Jf_CutVar(int *pCut, int i)
Definition: giaJf.c:99
int fVeryVerbose
Definition: gia.h:292
static int Jf_ObjArr(Jf_Man_t *p, int i)
Definition: giaJf.c:79
void Jf_ManSetDefaultPars(Jf_Par_t *pPars)
Definition: giaJf.c:1679
static int Jf_CutSetAll(int f, int c, int s)
Definition: giaJf.c:89
int Jf_ObjCutFilterBoth(Jf_Man_t *p, Jf_Cut_t **pSto, int c)
Definition: giaJf.c:760
Jf_Man_t * Jf_ManAlloc(Gia_Man_t *pGia, Jf_Par_t *pPars)
Definition: giaJf.c:364
static int Jf_CutCnfSize(Jf_Man_t *p, int *c)
Definition: giaJf.c:102
float Flow
Definition: giaJf.c:44
char * memmove()
int * pObj2Clause
Definition: cnf.h:64
word Delay
Definition: gia.h:297
word Area
Definition: gia.h:298
static void Jf_ObjPrintStore(Jf_Man_t *p, Jf_Cut_t **pSto, int c)
Definition: giaJf.c:1024
static void Jf_CutSetFunc(int *pCut, int f)
Definition: giaJf.c:92
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
#define Jf_CutForEachVar(pCut, Var, i)
Definition: giaJf.c:109
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
int fOptEdge
Definition: gia.h:278
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
void Jf_ObjComputeCuts(Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge)
Definition: giaJf.c:1125
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_Man_t * pGia
Definition: giaJf.c:54
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
void Gia_ManPrintCone(Gia_Man_t *p, Gia_Obj_t *pObj, int *pLeaves, int nLeaves, Vec_Int_t *vNodes)
Definition: giaUtil.c:1368
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static void Jf_CutRef(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:521
float Jf_CutCompareArea(Jf_Cut_t *pOld, Jf_Cut_t *pNew)
Definition: giaJf.c:946
int ** pClauses
Definition: cnf.h:62
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Jf_ObjCutPrint(int *pCuts)
Definition: giaJf.c:444
Definition: gia.h:265
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
static Vec_Mem_t * Vec_MemAllocForTT(int nVars, int fCompl)
Definition: vecMem.h:378
void Jf_ManPropagateFlow(Jf_Man_t *p, int fEdge)
Definition: giaJf.c:1379
int iFunc
Definition: giaJf.c:46
static int Jf_CutMerge0(int *pCut0, int *pCut1, int *pCut, int LutSize)
Definition: giaJf.c:665
int Jf_CutCheckMffc_rec(Jf_Man_t *p, int *pCut, int Limit)
Definition: giaJf.c:904
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
void * pData
Definition: gia.h:169
static int Gia_ObjRefInc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:522
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
static void Vec_SetFree_(Vec_Set_t *p)
Definition: vecSet.h:168
void Jf_ManDumpCnf(Gia_Man_t *p, char *pFileName, int fVerbose)
Definition: giaJf.c:1764
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
char * pSpec
Definition: gia.h:98
static double Vec_MemMemory(Vec_Mem_t *p)
Definition: vecMem.h:175
void Jf_ManPropagateEla(Jf_Man_t *p, int fEdge)
Definition: giaJf.c:1390
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static int Jf_CutFindLeaf0(int *pCut, int iObj)
Definition: giaJf.c:649
void Jf_ManDeriveMapping(Jf_Man_t *p)
Definition: giaJf.c:1542
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_Man_t * Jf_ManPerformMapping(Gia_Man_t *pGia, Jf_Par_t *pPars)
Definition: giaJf.c:1712
static int Jf_CutCnfSizeF(Jf_Man_t *p, int f)
Definition: giaJf.c:101
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Jf_CutIsContained1(int *pBase, int *pCut)
Definition: giaJf.c:700
static void Jf_CutSetCost(int *pCut, int c)
Definition: giaJf.c:91
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
static void Vec_MemDumpTruthTables(Vec_Mem_t *p, char *pName, int nLutSize)
Definition: vecMem.h:402
Vec_Set_t pMem
Definition: giaJf.c:64
float * Jf_ManInitRefs(Jf_Man_t *pMan)
Definition: giaJf.c:244
int nCoarse
Definition: giaJf.c:69
static void Vec_MemFree(Vec_Mem_t *p)
Definition: utilMem.c:93
Vec_Int_t vArr
Definition: giaJf.c:60
int Jf_CutRef_rec(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:844
void Sdm_ManReadCnfCosts(Sdm_Man_t *p, int *pCosts, int nCosts)
void Jf_ManFree(Jf_Man_t *p)
Definition: giaJf.c:395
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void Jf_ObjCheckStore(Jf_Man_t *p, Jf_Cut_t **pSto, int c, int iObj)
Definition: giaJf.c:1044
static int Gia_ObjRefDec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:523
int Jf_CutAreaRef_rec(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:869
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
static int Jf_CutSize(int *pCut)
Definition: giaJf.c:86
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
int nRounds
Definition: gia.h:270
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_Flt_t vFlow
Definition: giaJf.c:62
float(* pCutCmp)(Jf_Cut_t *, Jf_Cut_t *)
Definition: giaJf.c:66
typedefABC_NAMESPACE_HEADER_START struct Vec_Set_t_ Vec_Set_t
INCLUDES ///.
Definition: vecSet.h:49
static void Abc_TtExpand(word *pTruth0, int nVars, int *pCut0, int nCutSize0, int *pCut, int nCutSize)
Definition: utilTruth.h:1360
#define JF_LEAF_MAX
DECLARATIONS ///.
Definition: giaJf.c:36
void Jf_ObjComputeBestCut(Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge, int fEla)
Definition: giaJf.c:1357
static int Jf_ObjFunc1(Gia_Obj_t *p, int *c)
Definition: giaJf.c:105
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
unsigned fMark0
Definition: gia.h:79
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Definition: gia.h:95
static int Jf_ObjLit(int i, int c)
Definition: giaJf.c:84
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
int fPureAig
Definition: gia.h:287
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static void Jf_ObjSortCuts(Jf_Cut_t **pSto, int nSize)
Definition: giaJf.c:820
int fCutMin
Definition: gia.h:282
static float Jf_CutFlow(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:533
Gia_Man_t * Jf_ManDeriveGia(Jf_Man_t *p)
Definition: giaJf.c:1578
static int Jf_CutCheckMffc(Jf_Man_t *p, int *pCut, int Limit)
Definition: giaJf.c:918
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
int Var
Definition: SolverTypes.h:42
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
typedefABC_NAMESPACE_HEADER_START struct Vec_Flt_t_ Vec_Flt_t
INCLUDES ///.
Definition: vecFlt.h:42
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
int fFuncDsd
Definition: gia.h:283
Cnf_Dat_t * Jf_ManCreateCnf(Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas)
Definition: giaJf.c:198
Vec_Int_t vCuts
Definition: giaJf.c:59
static int Vec_MemHashInsert(Vec_Mem_t *p, word *pEntry)
Definition: vecMem.h:351
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
static void Vec_MemHashFree(Vec_Mem_t *p)
Definition: vecMem.h:311
int fGenCnf
Definition: gia.h:284
word CutCount[4]
Definition: giaJf.c:68
#define assert(ex)
Definition: util_old.h:213
double Gia_ManMemory(Gia_Man_t *p)
Definition: giaMan.c:156
static float Vec_FltEntry(Vec_Flt_t *p, int i)
Definition: vecFlt.h:342
int Sdm_ManComputeFunc(Sdm_Man_t *p, int iDsdLit0, int iDsdLit1, int *pCut, int uMask, int fXor)
Definition: extraUtilDsd.c:920
int nLutSizeMax
Definition: gia.h:293
static void Jf_CutDeref(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:527
static word * Vec_MemReadEntry(Vec_Mem_t *p, int i)
Definition: vecMem.h:191
Vec_Int_t * vMapping
Definition: gia.h:131
static int Jf_CutFunc(int *pCut)
Definition: giaJf.c:88
static int Jf_CutIsContained0(int *pBase, int *pCut)
Definition: giaJf.c:657
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int * Jf_ObjCutBest(Jf_Man_t *p, int i)
Definition: giaJf.c:78
float Jf_CutCompareDelay(Jf_Cut_t *pOld, Jf_Cut_t *pNew)
Definition: giaJf.c:939
static int Jf_CutFuncCompl(int *pCut)
Definition: giaJf.c:95
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
static int Jf_CountBits(word i)
Definition: giaJf.c:479
int nLiterals
Definition: cnf.h:60
static double Vec_ReportMemory(Vec_Set_t *p)
Definition: vecSet.h:194
int DelayTarget
Definition: gia.h:276
static int Jf_ObjDep(Jf_Man_t *p, int i)
Definition: giaJf.c:80
Vec_Flt_t vRefs
Definition: giaJf.c:63
static int * Vec_IntReleaseArray(Vec_Int_t *p)
Definition: extraZddTrunc.c:89
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
int fAddOrCla
Definition: gia.h:286
static int Jf_CutIsContainedOrder(int *pBase, int *pCut)
Definition: giaJf.c:553
static int Jf_CutAreaOld(Jf_Man_t *p, int *pCut)
Definition: giaJf.c:860
int fVerbose
Definition: gia.h:291
Vec_Mem_t * vTtMem
Definition: giaJf.c:58
static int Gia_ObjRefIncId(Gia_Man_t *p, int Id)
Definition: gia.h:519
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
static int * Jf_CutLits(int *pCut)
Definition: giaJf.c:96
int Sdm_ManReadDsdVarNum(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:997
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
int fCoarsen
Definition: gia.h:281
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
int * pObj2Count
Definition: cnf.h:65
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387