abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bdcSpfd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bdcSpfd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Truth-table-based bi-decomposition engine.]
8 
9  Synopsis [The gateway to bi-decomposition.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 30, 2007.]
16 
17  Revision [$Id: bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bdcInt.h"
22 #include "aig/aig/aig.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 typedef struct Bdc_Nod_t_ Bdc_Nod_t;
32 struct Bdc_Nod_t_
33 {
34  unsigned iFan0g : 8;
35  unsigned iFan0n : 12;
36  unsigned Type : 12; // 0-3 = AND; 4 = XOR
37 
38  unsigned iFan1g : 8;
39  unsigned iFan1n : 12;
40  unsigned Weight : 12;
41 
42  word Truth;
43 };
44 
45 static word Truths[6] = {
46  ABC_CONST(0xAAAAAAAAAAAAAAAA),
47  ABC_CONST(0xCCCCCCCCCCCCCCCC),
48  ABC_CONST(0xF0F0F0F0F0F0F0F0),
49  ABC_CONST(0xFF00FF00FF00FF00),
50  ABC_CONST(0xFFFF0000FFFF0000),
51  ABC_CONST(0xFFFFFFFF00000000)
52 };
53 
54 static inline int Bdc_CountOnes( word t )
55 {
56  t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
57  t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
58  t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
59  t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
60  t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
61  return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
62 }
63 
64 static inline int Bdc_CountSpfd( word t, word f )
65 {
66  int n00 = Bdc_CountOnes( ~t & ~f );
67  int n01 = Bdc_CountOnes( t & ~f );
68  int n10 = Bdc_CountOnes( ~t & f );
69  int n11 = Bdc_CountOnes( t & f );
70  return n00 * n11 + n10 * n01;
71 }
72 
73 static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
74 {
75  assert( iVar >= 0 && iVar < 6 );
76  if ( fCof1 )
77  return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar));
78  else
79  return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar));
80 }
81 
82 int Bdc_SpfdAdjCost( word t )
83 {
84  word c0, c1;
85  int v, Cost = 0;
86  for ( v = 0; v < 6; v++ )
87  {
88  c0 = Bdc_Cof6( t, v, 0 );
89  c1 = Bdc_Cof6( t, v, 1 );
90  Cost += Bdc_CountOnes( c0 ^ c1 );
91  }
92  return Cost;
93 }
94 
95 
96 extern void Abc_Show6VarFunc( word F0, word F1 );
97 
98 ////////////////////////////////////////////////////////////////////////
99 /// FUNCTION DEFINITIONS ///
100 ////////////////////////////////////////////////////////////////////////
101 
102 /**Function*************************************************************
103 
104  Synopsis []
105 
106  Description []
107 
108  SideEffects []
109 
110  SeeAlso []
111 
112 ***********************************************************************/
113 void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
114 {
115  assert( Level > 0 );
116  printf( "(" );
117 
118  if ( pNode->Type & 1 )
119  printf( "!" );
120  if ( pNode->iFan0g == 0 )
121  printf( "%c", 'a' + pNode->iFan0n );
122  else
123  {
124  Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g);
125  Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels );
126  }
127 
128  if ( pNode->Type & 4 )
129  printf( "+" );
130  else
131  printf( "*" );
132 
133  if ( pNode->Type & 2 )
134  printf( "!" );
135  if ( pNode->iFan1g == 0 )
136  printf( "%c", 'a' + pNode->iFan1n );
137  else
138  {
139  Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g);
140  Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels );
141  }
142 
143  printf( ")" );
144 }
145 
146 /**Function*************************************************************
147 
148  Synopsis []
149 
150  Description []
151 
152  SideEffects []
153 
154  SeeAlso []
155 
156 ***********************************************************************/
157 void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth )
158 {
159  word Diff = Truth ^ pNode->Truth;
160  Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( " " );
161  Extra_PrintHex( stdout, (unsigned *)&Diff, 6 ); printf( " " );
162  Bdc_SpfdPrint_rec( pNode, Level, vLevels );
163  printf( " %d\n", pNode->Weight );
164 }
165 
166 /**Function*************************************************************
167 
168  Synopsis []
169 
170  Description []
171 
172  SideEffects []
173 
174  SeeAlso []
175 
176 ***********************************************************************/
177 void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
178 {
179  int nSize = nCands * nCands * (nGatesMax + 1) * 5;
180  Vec_Ptr_t * vLevels;
181  Vec_Int_t * vBegs, * vWeight;
182  Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
183  int Count0, Count1, * pPerm;
184  int i, j, k, c, n;
185  abctime clk;
186  assert( nGatesMax < (1<<8) );
187  assert( nCands < (1<<12) );
188  assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD
189 
190  printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 );
191 
192  printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) );
193 
194  // consider elementary functions
195  if ( Truth == 0 || Truth == ~0 )
196  {
197  printf( "Function is a constant.\n" );
198  return;
199  }
200  for ( i = 0; i < nVars; i++ )
201  if ( Truth == Truths[i] || Truth == ~Truths[i] )
202  {
203  printf( "Function is an elementary variable.\n" );
204  return;
205  }
206 
207  // allocate
208  vLevels = Vec_PtrAlloc( 100 );
209  vBegs = Vec_IntAlloc( 100 );
210  vWeight = Vec_IntAlloc( 100 );
211 
212  // initialize elementary variables
213  pNode = ABC_CALLOC( Bdc_Nod_t, nVars );
214  for ( i = 0; i < nVars; i++ )
215  pNode[i].Truth = Truths[i];
216  for ( i = 0; i < nVars; i++ )
217  pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
218  Vec_PtrPush( vLevels, pNode );
219  Vec_IntPush( vBegs, nVars );
220 
221  // the next level
222 clk = Abc_Clock();
223  pNode0 = pNode;
224  pNode = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 );
225  for ( c = i = 0; i < nVars; i++ )
226  for ( j = i+1; j < nVars; j++ )
227  {
228  pNode[c].Truth = pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
229  pNode[c].Truth = ~pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
230  pNode[c].Truth = pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
231  pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
232  pNode[c].Truth = pNode0[i].Truth ^ pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
233  }
234  assert( c == 5 * nVars * (nVars - 1) / 2 );
235  Vec_PtrPush( vLevels, pNode );
236  Vec_IntPush( vBegs, c );
237  for ( i = 0; i < c; i++ )
238  {
239  pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
240 //Bdc_SpfdPrint( pNode + i, 1, vLevels );
241  if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
242  {
243  printf( "Function can be implemented using 1 gate.\n" );
244  pNode = NULL;
245  goto cleanup;
246  }
247  }
248 printf( "Selected %6d gates on level %2d. ", c, 1 );
249 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
250 
251 
252  // iterate through levels
253  pNode = ABC_CALLOC( Bdc_Nod_t, nSize );
254  for ( n = 2; n <= nGatesMax; n++ )
255  {
256 clk = Abc_Clock();
257  c = 0;
258  pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 );
259  Count1 = Vec_IntEntry( vBegs, n-1 );
260  // go through previous levels
261  for ( k = 0; k < n-1; k++ )
262  {
263  pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k );
264  Count0 = Vec_IntEntry( vBegs, k );
265  for ( i = 0; i < Count0; i++ )
266  for ( j = 0; j < Count1; j++ )
267  {
268  pNode[c].Truth = pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
269  pNode[c].Truth = ~pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
270  pNode[c].Truth = pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
271  pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
272  pNode[c].Truth = pNode0[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
273  }
274  assert( c < nSize );
275  }
276  // go through current level
277  for ( i = 0; i < Count1; i++ )
278  for ( j = i+1; j < Count1; j++ )
279  {
280  pNode[c].Truth = pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
281  pNode[c].Truth = ~pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
282  pNode[c].Truth = pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
283  pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
284  pNode[c].Truth = pNode1[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
285  }
286  assert( c < nSize );
287  // sort
288  Vec_IntClear( vWeight );
289  for ( i = 0; i < c; i++ )
290  {
291  pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
292 if ( pNode[i].Weight > 300 )
293 Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
294  Vec_IntPush( vWeight, pNode[i].Weight );
295 
296  if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
297  {
298  printf( "Function can be implemented using %d gates.\n", n );
299  Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
300  goto cleanup;
301  }
302  }
303  pPerm = Abc_MergeSortCost( Vec_IntArray(vWeight), c );
304  assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) );
305 
306  printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) );
307 // for ( i = 0; i < c; i++ )
308 //printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) );
309 
310  // choose the best ones
311  pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands );
312  for ( j = 0, i = c-1; i >= 0; i-- )
313  {
314  pNode2[j++] = pNode[pPerm[i]];
315  if ( j == nCands )
316  break;
317  }
318  ABC_FREE( pPerm );
319  Vec_PtrPush( vLevels, pNode2 );
320  Vec_IntPush( vBegs, j );
321 
322 printf( "Selected %6d gates (out of %6d) on level %2d. ", j, c, n );
323 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
324 
325  for ( i = 0; i < 10; i++ )
326  Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
327  }
328 
329 cleanup:
330  ABC_FREE( pNode );
331  Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
332  ABC_FREE( pNode );
333  Vec_PtrFree( vLevels );
334  Vec_IntFree( vBegs );
335  Vec_IntFree( vWeight );
336 }
337 
338 
339 /**Function*************************************************************
340 
341  Synopsis []
342 
343  Description []
344 
345  SideEffects []
346 
347  SeeAlso []
348 
349 ***********************************************************************/
350 void Bdc_SpfdDecomposeTest_()
351 {
352  int fTry = 0;
353 // word T[17];
354 // int i;
355 
356 // word Truth = Truths[0] & ~Truths[3];
357 // word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
358 // word Truth = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
359 // word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
360 // word Truth = 0x9ef7a8d9c7193a0f; // AAFFAAFF0A0F0A0F
361 // word Truth = 0x34080226CD163000;
362  word Truth = ABC_CONST(0x5052585a0002080a);
363  int nVars = 6;
364  int nCands = 200;// 75;
365  int nGatesMax = 20;
366 
367  if ( fTry )
368  Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax );
369 /*
370  for ( i = 0; i < 6; i++ )
371  T[i] = Truths[i];
372  T[7] = 0;
373  T[8] = ~T[1] & T[3];
374  T[9] = ~T[8] & T[0];
375  T[10] = T[1] & T[4];
376  T[11] = T[10] & T[2];
377  T[12] = T[11] & T[9];
378  T[13] = ~T[0] & T[5];
379  T[14] = T[2] & T[13];
380  T[15] = ~T[12] & ~T[14];
381  T[16] = ~T[15];
382 // if ( T[16] != Truth )
383 // printf( "Failed\n" );
384 
385  for ( i = 0; i < 17; i++ )
386  {
387 // printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], Truth) );
388  printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], T[16]) );
389  Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" );
390  }
391 // Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" );
392 */
393 }
394 
395 
396 
397 
398 typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
399 struct Bdc_Ent_t_
400 {
401  unsigned iFan0 : 29;
402  unsigned fCompl0 : 1;
403  unsigned fCompl : 1;
404  unsigned fMark0 : 1;
405  unsigned iFan1 : 29;
406  unsigned fCompl1 : 1;
407  unsigned fExor : 1;
408  unsigned fMark1 : 1;
409  int iNext;
410  int iList;
411  word Truth;
412 };
413 
414 #define BDC_TERM 0x1FFFFFFF
415 
416 
417 /**Function*************************************************************
418 
419  Synopsis []
420 
421  Description []
422 
423  SideEffects []
424 
425  SeeAlso []
426 
427 ***********************************************************************/
428 int Bdc_SpfdMark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
429 {
430  if ( pEnt->iFan0 == BDC_TERM )
431  return 0;
432  if ( pEnt->fMark0 )
433  return 0;
434  pEnt->fMark0 = 1;
435  return pEnt->fMark1 +
436  Bdc_SpfdMark0(p, p + pEnt->iFan0) +
437  Bdc_SpfdMark0(p, p + pEnt->iFan1);
438 }
439 int Bdc_SpfdMark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
440 {
441  if ( pEnt->iFan0 == BDC_TERM )
442  return 0;
443  if ( pEnt->fMark1 )
444  return 0;
445  pEnt->fMark1 = 1;
446  return pEnt->fMark0 +
447  Bdc_SpfdMark1(p, p + pEnt->iFan0) +
448  Bdc_SpfdMark1(p, p + pEnt->iFan1);
449 }
450 void Bdc_SpfdUnmark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
451 {
452  if ( pEnt->iFan0 == BDC_TERM )
453  return;
454  pEnt->fMark0 = 0;
455  Bdc_SpfdUnmark0( p, p + pEnt->iFan0 );
456  Bdc_SpfdUnmark0( p, p + pEnt->iFan1 );
457 }
458 void Bdc_SpfdUnmark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
459 {
460  if ( pEnt->iFan0 == BDC_TERM )
461  return;
462  pEnt->fMark1 = 0;
463  Bdc_SpfdUnmark1( p, p + pEnt->iFan0 );
464  Bdc_SpfdUnmark1( p, p + pEnt->iFan1 );
465 }
466 
467 
468 /**Function*************************************************************
469 
470  Synopsis []
471 
472  Description []
473 
474  SideEffects []
475 
476  SeeAlso []
477 
478 ***********************************************************************/
479 int Bdc_SpfdCheckOverlap( Bdc_Ent_t * p, Bdc_Ent_t * pEnt0, Bdc_Ent_t * pEnt1 )
480 {
481  int RetValue;
482  RetValue = Bdc_SpfdMark0( p, pEnt0 );
483  assert( RetValue == 0 );
484  RetValue = Bdc_SpfdMark1( p, pEnt1 );
485  Bdc_SpfdUnmark0( p, pEnt0 );
486  Bdc_SpfdUnmark1( p, pEnt1 );
487  return RetValue;
488 }
489 
490 /**Function*************************************************************
491 
492  Synopsis []
493 
494  Description []
495 
496  SideEffects []
497 
498  SeeAlso []
499 
500 ***********************************************************************/
501 int Bdc_SpfdHashValue( word t, int Size )
502 {
503  // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
504  // 53,
505  // 97,
506  // 193,
507  // 389,
508  // 769,
509  // 1543,
510  // 3079,
511  // 6151,
512  // 12289,
513  // 24593,
514  // 49157,
515  // 98317,
516  // 196613,
517  // 393241,
518  // 786433,
519  // 1572869,
520  // 3145739,
521  // 6291469,
522  // 12582917,
523  // 25165843,
524  // 50331653,
525  // 100663319,
526  // 201326611,
527  // 402653189,
528  // 805306457,
529  // 1610612741,
530  static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
531  unsigned char * s = (unsigned char *)&t;
532  unsigned i, Value = 0;
533  for ( i = 0; i < 8; i++ )
534  Value ^= BigPrimes[i] * s[i];
535  return Value % Size;
536 }
537 
538 /**Function*************************************************************
539 
540  Synopsis []
541 
542  Description []
543 
544  SideEffects []
545 
546  SeeAlso []
547 
548 ***********************************************************************/
549 int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
550 {
551  Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
552  if ( pBin->iList == 0 )
553  return &pBin->iList;
554  for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
555  {
556  if ( pBin->Truth == t )
557  return NULL;
558  if ( pBin->iNext == 0 )
559  return &pBin->iNext;
560  }
561  assert( 0 );
562  return NULL;
563 }
564 
565 /**Function*************************************************************
566 
567  Synopsis []
568 
569  Description []
570 
571  SideEffects []
572 
573  SeeAlso []
574 
575 ***********************************************************************/
576 Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
577 {
578 // int nFuncs = 8000000; // the number of functions to compute
579 // int nSize = 2777111; // the hash table size to use
580 // int Limit = 6;
581 
582 // int nFuncs = 51000000; // the number of functions to compute
583 // int nSize = 50331653; // the hash table size to use
584 // int Limit = 6;
585 
586  int nFuncs = 250000000; // the number of functions to compute
587  int nSize = 201326611; // the hash table size to use
588  int Limit = 6;
589 
590  int * pPlace, i, n, m, k, s, fCompl;
591  abctime clk = Abc_Clock(), clk2;
592  Vec_Int_t * vStops;
593  Vec_Wrd_t * vTruths;
594  Vec_Int_t * vWeights;
595  Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
596  word t0, t1, t;
597  assert( nSize <= nFuncs );
598 
599  printf( "Allocating %.2f MB of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );
600 
601  p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
602  memset( p, 255, sizeof(Bdc_Ent_t) );
603  p->iList = 0;
604  for ( q = p; q < p+nFuncs; q++ )
605  q->iList = 0;
606  q = p + 1;
607  printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
608 
609  vTruths = Vec_WrdStart( nFuncs );
610  vWeights = Vec_IntStart( nFuncs );
611  Vec_WrdClear( vTruths );
612  Vec_IntClear( vWeights );
613 
614  // create elementary vars
615  vStops = Vec_IntAlloc( 10 );
616  Vec_IntPush( vStops, 1 );
617  for ( i = 0; i < 6; i++ )
618  {
619  q->iFan0 = BDC_TERM;
620  q->iFan1 = i;
621  q->Truth = Truths[i];
622  pPlace = Bdc_SpfdHashLookup( p, nSize, q->Truth );
623  *pPlace = q-p;
624  q++;
625  Vec_WrdPush( vTruths, Truths[i] );
626  Vec_IntPush( vWeights, 0 );
627  }
628  Vec_IntPush( vStops, 7 );
629  printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
630 
631  // create gates
632  for ( n = 0; n < Limit; n++ )
633  {
634  // try previous
635  for ( k = 0; k < Limit; k++ )
636  for ( m = 0; m < Limit; m++ )
637  {
638  if ( k + m != n || k > m )
639  continue;
640  // set the start and stop
641  pBeg0 = p + Vec_IntEntry( vStops, k );
642  pEnd0 = p + Vec_IntEntry( vStops, k+1 );
643  // set the start and stop
644  pBeg1 = p + Vec_IntEntry( vStops, m );
645  pEnd1 = p + Vec_IntEntry( vStops, m+1 );
646 
647  clk2 = Abc_Clock();
648  printf( "Trying %7d x %7d. ", (int)(pEnd0-pBeg0), (int)(pEnd1-pBeg1) );
649  for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
650  for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
651  if ( k < m || pThis1 > pThis0 )
652 // if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) )
653  for ( s = 0; s < 5; s++ )
654  {
655  t0 = (s&1) ? ~pThis0->Truth : pThis0->Truth;
656  t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
657  t = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
658  fCompl = t & 1;
659  if ( fCompl )
660  t = ~t;
661  if ( t == 0 )
662  continue;
663  pPlace = Bdc_SpfdHashLookup( p, nSize, t );
664  if ( pPlace == NULL )
665  continue;
666  q->iFan0 = pThis0-p;
667  q->fCompl0 = s&1;
668  q->iFan1 = pThis1-p;
669  q->fCompl1 = (s>>1)&1;
670  q->fExor = (s>>2)&1;
671  q->Truth = t;
672  q->fCompl = fCompl;
673  *pPlace = q-p;
674  q++;
675  Vec_WrdPush( vTruths, t );
676 // Vec_IntPush( vWeights, n == 5 ? n : n+1 );
677  Vec_IntPush( vWeights, n+1 );
678  if ( q-p == nFuncs )
679  {
680  printf( "Reached limit of %d functions.\n", nFuncs );
681  goto finish;
682  }
683  }
684  printf( "Added %d + %d + 1 = %d. Total = %8d. ", k, m, n+1, (int)(q-p) );
685  Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
686  }
687  Vec_IntPush( vStops, q-p );
688  }
689  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
690 
691 
692  {
693  FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
694  fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
695  fclose( pFile );
696  }
697  {
698  FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
699  fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
700  fclose( pFile );
701  }
702 
703 
704 finish:
705  Vec_IntFree( vStops );
706  free( p );
707 
708  *pvWeights = vWeights;
709 // Vec_WrdFree( vTruths );
710  return vTruths;
711 }
712 
713 
714 /**Function*************************************************************
715 
716  Synopsis []
717 
718  Description []
719 
720  SideEffects []
721 
722  SeeAlso []
723 
724 ***********************************************************************/
725 Vec_Wrd_t * Bdc_SpfdReadFiles5( Vec_Int_t ** pvWeights )
726 {
727  Vec_Int_t * vWeights;
728  Vec_Wrd_t * vDivs;
729  FILE * pFile;
730  int RetValue;
731 
732  vDivs = Vec_WrdStart( 3863759 );
733  pFile = fopen( "func6v5n_bin.txt", "rb" );
734  RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
735  fclose( pFile );
736 
737  vWeights = Vec_IntStart( 3863759 );
738  pFile = fopen( "func6v5nW_bin.txt", "rb" );
739  RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
740  fclose( pFile );
741 
742  *pvWeights = vWeights;
743  return vDivs;
744 }
745 
746 /**Function*************************************************************
747 
748  Synopsis []
749 
750  Description []
751 
752  SideEffects []
753 
754  SeeAlso []
755 
756 ***********************************************************************/
757 Vec_Wrd_t * Bdc_SpfdReadFiles6( Vec_Int_t ** pvWeights )
758 {
759  Vec_Int_t * vWeights;
760  Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
761  FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
762  int RetValue;
763  RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
764  fclose( pFile );
765 
766  vWeights = Vec_IntStart( 12776759 );
767  pFile = fopen( "func6v6nW_bin.txt", "rb" );
768  RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
769  fclose( pFile );
770 
771  *pvWeights = vWeights;
772  return vDivs;
773 }
774 
775 /**Function*************************************************************
776 
777  Synopsis []
778 
779  Description []
780 
781  SideEffects []
782 
783  SeeAlso []
784 
785 ***********************************************************************/
786 int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
787 {
788  int Ones = Bdc_CountOnes(f);
789  if ( Ones == 0 )
790  return -1;
791  return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
792 // return Bdc_CountOnes(f);
793 }
794 
795 /**Function*************************************************************
796 
797  Synopsis []
798 
799  Description []
800 
801  SideEffects []
802 
803  SeeAlso []
804 
805 ***********************************************************************/
806 word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
807 {
808  word Func, FuncBest;
809  int i, Cost, CostBest = -1, NumBest = -1;
810  Vec_WrdForEachEntry( vDivs, Func, i )
811  {
812  if ( (Func & F0) == 0 )
813  {
814  Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
815  if ( CostBest < Cost )
816  {
817  CostBest = Cost;
818  FuncBest = Func;
819  NumBest = i;
820  }
821  }
822  if ( (Func & F1) == 0 )
823  {
824  Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
825  if ( CostBest < Cost )
826  {
827  CostBest = Cost;
828  FuncBest = Func;
829  NumBest = i;
830  }
831  }
832  if ( (~Func & F0) == 0 )
833  {
834  Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
835  if ( CostBest < Cost )
836  {
837  CostBest = Cost;
838  FuncBest = ~Func;
839  NumBest = i;
840  }
841  }
842  if ( (~Func & F1) == 0 )
843  {
844  Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
845  if ( CostBest < Cost )
846  {
847  CostBest = Cost;
848  FuncBest = ~Func;
849  NumBest = i;
850  }
851  }
852  }
853  (*pCost) += Vec_IntEntry(vWeights, NumBest);
854  assert( CostBest > 0 );
855  printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
856  Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
857  return FuncBest;
858 }
859 
860 /**Function*************************************************************
861 
862  Synopsis []
863 
864  Description []
865 
866  SideEffects []
867 
868  SeeAlso []
869 
870 ***********************************************************************/
871 int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
872 {
873  word F1 = t;
874  word F0 = ~F1;
875  word Func;
876  int i, Cost = 0;
877  printf( "Trying: " );
878  Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" );
879 // Abc_Show6VarFunc( F0, F1 );
880  for ( i = 0; F0 && F1; i++ )
881  {
882  printf( "*** ITER %2d ", i );
883  Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
884  F0 &= ~Func;
885  F1 &= ~Func;
886 // Abc_Show6VarFunc( F0, F1 );
887  }
888  Cost += (i-1);
889  printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
890  return Cost;
891 }
892 
893 /**Function*************************************************************
894 
895  Synopsis []
896 
897  Description []
898 
899  SideEffects []
900 
901  SeeAlso []
902 
903 ***********************************************************************/
904 void Bdc_SpfdDecomposeTest44()
905 {
906 // word t = 0x5052585a0002080a;
907 
908  word t = ABC_CONST(0x9ef7a8d9c7193a0f);
909 // word t = 0x6BFDA276C7193A0F;
910 // word t = 0xA3756AFE0B1DF60B;
911 
912 // word t = 0xFEF7AEBFCE80AA0F;
913 // word t = 0x9EF7FDBFC77F6F0F;
914 // word t = 0xDEF7FDFF377F6FFF;
915 
916 // word t = 0x345D02736DB390A5; // xor with var 0
917 
918 // word t = 0x3EFDA2736D139A0F; // best solution after changes
919 
920  Vec_Int_t * vWeights;
921  Vec_Wrd_t * vDivs;
922  word c0, c1, s, tt, tbest;
923  int i, j, Cost, CostBest = 100000;
924  abctime clk = Abc_Clock();
925 
926  return;
927 
928 // printf( "%d\n", RAND_MAX );
929 
930  vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
931 // vDivs = Bdc_SpfdReadFiles5( &vWeights );
932 
933 // Abc_Show6VarFunc( ~t, t );
934 
935  // try function
936  tt = t;
937  Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
938  if ( CostBest > Cost )
939  {
940  CostBest = Cost;
941  tbest = tt;
942  }
943  printf( "\n" );
944 
945  // try complemented output
946  for ( i = 0; i < 6; i++ )
947  {
948  tt = t ^ Truths[i];
949  Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
950  if ( CostBest > Cost )
951  {
952  CostBest = Cost;
953  tbest = tt;
954  }
955  }
956  printf( "\n" );
957 
958  // try complemented input
959  for ( i = 0; i < 6; i++ )
960  for ( j = 0; j < 6; j++ )
961  {
962  if ( i == j )
963  continue;
964  c0 = Bdc_Cof6( t, i, 0 );
965  c1 = Bdc_Cof6( t, i, 1 );
966  s = Truths[i] ^ Truths[j];
967  tt = (~s & c0) | (s & c1);
968 
969  Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
970  if ( CostBest > Cost )
971  {
972  CostBest = Cost;
973  tbest = tt;
974  }
975  }
976 
977 /*
978  for ( i = 0; i < 6; i++ )
979  for ( j = 0; j < 6; j++ )
980  {
981  if ( i == j )
982  continue;
983  c0 = Bdc_Cof6( t, i, 0 );
984  c1 = Bdc_Cof6( t, i, 1 );
985  s = Truths[i] ^ Truths[j];
986  tt = (~s & c0) | (s & c1);
987 
988  for ( k = 0; k < 6; k++ )
989  for ( n = 0; n < 6; n++ )
990  {
991  if ( k == n )
992  continue;
993  c0 = Bdc_Cof6( tt, k, 0 );
994  c1 = Bdc_Cof6( tt, k, 1 );
995  s = Truths[k] ^ Truths[n];
996  ttt= (~s & c0) | (s & c1);
997 
998  Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
999  if ( CostBest > Cost )
1000  {
1001  CostBest = Cost;
1002  tbest = ttt;
1003  }
1004  }
1005  }
1006 */
1007 
1008  printf( "Best solution found with cost %d. ", CostBest );
1009  Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
1010  Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1011 
1012  Vec_WrdFree( vDivs );
1013  Vec_IntFree( vWeights );
1014 }
1015 
1016 /**Function*************************************************************
1017 
1018  Synopsis []
1019 
1020  Description []
1021 
1022  SideEffects []
1023 
1024  SeeAlso []
1025 
1026 ***********************************************************************/
1027 void Bdc_SpfdDecomposeTest3()
1028 {
1029  int nSizeM = (1 << 26);
1030  int nSizeK = (1 << 3);
1031  Vec_Wrd_t * v1M;
1032  Vec_Wrd_t * v1K;
1033  int i, k, Counter;
1034  abctime clk;
1035 // int EntryM, EntryK;
1036  Aig_ManRandom64( 1 );
1037 
1038  v1M = Vec_WrdAlloc( nSizeM );
1039  for ( i = 0; i < nSizeM; i++ )
1040  Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1041 
1042  v1K = Vec_WrdAlloc( nSizeK );
1043  for ( i = 0; i < nSizeK; i++ )
1044  Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1045 
1046  clk = Abc_Clock();
1047  Counter = 0;
1048  for ( i = 0; i < nSizeM; i++ )
1049  for ( k = 0; k < nSizeK; k++ )
1050  Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1051 // Vec_WrdForEachEntry( v1M, EntryM, i )
1052 // Vec_WrdForEachEntry( v1K, EntryK, k )
1053 // Counter += ((EntryM & EntryK) == EntryK);
1054 
1055  printf( "Total = %8d. ", Counter );
1056  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1057 
1058  clk = Abc_Clock();
1059  Counter = 0;
1060  for ( k = 0; k < nSizeK; k++ )
1061  for ( i = 0; i < nSizeM; i++ )
1062  Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1063  printf( "Total = %8d. ", Counter );
1064  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1065 
1066 }
1067 
1068 /**Function*************************************************************
1069 
1070  Synopsis []
1071 
1072  Description []
1073 
1074  SideEffects []
1075 
1076  SeeAlso []
1077 
1078 ***********************************************************************/
1079 void Bdc_SpfdDecomposeTest8()
1080 {
1081 // word t = 0x9ef7a8d9c7193a0f;
1082 // word t = 0x9EF7FDBFC77F6F0F;
1083  word t = ABC_CONST(0x513B57150819050F);
1084 
1085  Vec_Int_t * vWeights;
1086  Vec_Wrd_t * vDivs;
1087  word Func, FuncBest;
1088  int Cost, CostBest = ABC_INFINITY;
1089  int i;
1090  abctime clk = Abc_Clock();
1091 
1092 // return;
1093 
1094  vDivs = Bdc_SpfdReadFiles5( &vWeights );
1095 
1096  printf( "Best init = %4d. ", Bdc_SpfdAdjCost(t) );
1097  Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" );
1098  Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1099 
1100  Vec_WrdForEachEntry( vDivs, Func, i )
1101  {
1102  Cost = Bdc_SpfdAdjCost( t ^ Func );
1103  if ( CostBest > Cost )
1104  {
1105  CostBest = Cost;
1106  FuncBest = Func;
1107  }
1108  }
1109 
1110  printf( "Best cost = %4d. ", CostBest );
1111  Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" );
1112  Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1113 
1114 Abc_Show6VarFunc( 0, t );
1115 Abc_Show6VarFunc( 0, FuncBest );
1116 Abc_Show6VarFunc( 0, (FuncBest ^ t) );
1117 
1118  FuncBest ^= t;
1119  Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
1120 
1121 }
1122 
1123 /**Function*************************************************************
1124 
1125  Synopsis []
1126 
1127  Description []
1128 
1129  SideEffects []
1130 
1131  SeeAlso []
1132 
1133 ***********************************************************************/
1134 void Bdc_SpfdDecomposeTest()
1135 {
1136  int nSizeM = (1 << 26); // big array size
1137  int nSizeK = (1 << 3); // small array size
1138  Vec_Wrd_t * v1M, * v1K;
1139  int EntryM, EntryK;
1140  int i, k, Counter;
1141  abctime clk;
1142 
1143  Aig_ManRandom64( 1 );
1144 
1145  v1M = Vec_WrdAlloc( nSizeM );
1146  for ( i = 0; i < nSizeM; i++ )
1147  Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1148 
1149  v1K = Vec_WrdAlloc( nSizeK );
1150  for ( i = 0; i < nSizeK; i++ )
1151  Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1152 
1153  clk = Abc_Clock();
1154  Counter = 0;
1155 // for ( i = 0; i < nSizeM; i++ )
1156 // for ( k = 0; k < nSizeK; k++ )
1157 // Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1158  Vec_WrdForEachEntry( v1M, EntryM, i )
1159  Vec_WrdForEachEntry( v1K, EntryK, k )
1160  Counter += ((EntryM & EntryK) == EntryK);
1161  printf( "Total = %8d. ", Counter );
1162  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1163 
1164  clk = Abc_Clock();
1165  Counter = 0;
1166 // for ( k = 0; k < nSizeK; k++ )
1167 // for ( i = 0; i < nSizeM; i++ )
1168 // Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1169  Vec_WrdForEachEntry( v1K, EntryK, k )
1170  Vec_WrdForEachEntry( v1M, EntryM, i )
1171  Counter += ((EntryM & EntryK) == EntryK);
1172  printf( "Total = %8d. ", Counter );
1173  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1174 }
1175 
1176 
1177 ////////////////////////////////////////////////////////////////////////
1178 /// END OF FILE ///
1179 ////////////////////////////////////////////////////////////////////////
1180 
1181 
1182 ABC_NAMESPACE_IMPL_END
1183 
memset
char * memset()
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Bdc_Ent_t_
Definition: bdcSpfd.c:399
Bdc_SpfdUnmark1
void Bdc_SpfdUnmark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:458
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Bdc_CountSpfd
static int Bdc_CountSpfd(word t, word f)
Definition: bdcSpfd.c:64
free
VOID_HACK free()
Bdc_Nod_t_::Weight
unsigned Weight
Definition: bdcSpfd.c:40
Bdc_Ent_t_::iNext
int iNext
Definition: bdcSpfd.c:409
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Bdc_Cof6
static word Bdc_Cof6(word t, int iVar, int fCof1)
Definition: bdcSpfd.c:73
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Bdc_SpfdPrint
void Bdc_SpfdPrint(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
Definition: bdcSpfd.c:157
Vec_WrdPush
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
Bdc_SpfdDecomposeTest
void Bdc_SpfdDecomposeTest()
Definition: bdcSpfd.c:1134
Bdc_Ent_t_::iFan1
unsigned iFan1
Definition: bdcSpfd.c:405
Bdc_SpfdHashValue
int Bdc_SpfdHashValue(word t, int Size)
Definition: bdcSpfd.c:501
Bdc_SpfdPrint_rec
void Bdc_SpfdPrint_rec(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
FUNCTION DEFINITIONS ///.
Definition: bdcSpfd.c:113
BDC_TERM
#define BDC_TERM
Definition: bdcSpfd.c:414
Bdc_Ent_t_::fCompl
unsigned fCompl
Definition: bdcSpfd.c:403
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManRandom64
word Aig_ManRandom64(int fReset)
Definition: aigUtil.c:1182
Bdc_SpfdReadFiles5
Vec_Wrd_t * Bdc_SpfdReadFiles5(Vec_Int_t **pvWeights)
Definition: bdcSpfd.c:725
Bdc_SpfdHashLookup
int * Bdc_SpfdHashLookup(Bdc_Ent_t *p, int Size, word t)
Definition: bdcSpfd.c:549
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_WrdSize
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
Bdc_Ent_t_::fCompl0
unsigned fCompl0
Definition: bdcSpfd.c:402
Bdc_SpfdMark1
int Bdc_SpfdMark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:439
Abc_Show6VarFunc
void Abc_Show6VarFunc(word F0, word F1)
Definition: abcPrint.c:1508
Bdc_SpfdDecompose
void Bdc_SpfdDecompose(word Truth, int nVars, int nCands, int nGatesMax)
Definition: bdcSpfd.c:177
Bdc_Ent_t_::Truth
word Truth
Definition: bdcSpfd.c:411
Bdc_SpfdDecomposeTest44
void Bdc_SpfdDecomposeTest44()
Definition: bdcSpfd.c:904
Bdc_SpfdDecomposeTest3
void Bdc_SpfdDecomposeTest3()
Definition: bdcSpfd.c:1027
Bdc_CountOnes
static int Bdc_CountOnes(word t)
Definition: bdcSpfd.c:54
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
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition: extraUtilFile.c:620
Bdc_Nod_t_::iFan0g
unsigned iFan0g
Definition: bdcSpfd.c:34
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Bdc_SpfdComputeCost
int Bdc_SpfdComputeCost(word f, int i, Vec_Int_t *vWeights)
Definition: bdcSpfd.c:786
Vec_WrdClear
static void Vec_WrdClear(Vec_Wrd_t *p)
Definition: vecWrd.h:602
Bdc_Nod_t_::Type
unsigned Type
Definition: bdcSpfd.c:36
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Bdc_SpfdDecomposeTest8
void Bdc_SpfdDecomposeTest8()
Definition: bdcSpfd.c:1079
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_WrdFree
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
Bdc_SpfdDecomposeTestOne
int Bdc_SpfdDecomposeTestOne(word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
Definition: bdcSpfd.c:871
Bdc_SpfdCheckOverlap
int Bdc_SpfdCheckOverlap(Bdc_Ent_t *p, Bdc_Ent_t *pEnt0, Bdc_Ent_t *pEnt1)
Definition: bdcSpfd.c:479
Bdc_SpfdUnmark0
void Bdc_SpfdUnmark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:450
Bdc_Nod_t_::iFan0n
unsigned iFan0n
Definition: bdcSpfd.c:35
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Bdc_SpfdDecomposeTest_
void Bdc_SpfdDecomposeTest_()
Definition: bdcSpfd.c:350
Vec_WrdAlloc
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Bdc_Nod_t_::iFan1n
unsigned iFan1n
Definition: bdcSpfd.c:39
Bdc_SpfdMark0
int Bdc_SpfdMark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:428
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_WrdStart
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
Bdc_SpfdAdjCost
int Bdc_SpfdAdjCost(word t)
Definition: bdcSpfd.c:82
Bdc_Ent_t_::fMark1
unsigned fMark1
Definition: bdcSpfd.c:408
Bdc_Ent_t_::iList
int iList
Definition: bdcSpfd.c:410
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Bdc_Ent_t_::iFan0
unsigned iFan0
Definition: bdcSpfd.c:401
Bdc_Nod_t_::Truth
word Truth
Definition: bdcSpfd.c:42
Bdc_SpfdFindBest
word Bdc_SpfdFindBest(Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
Definition: bdcSpfd.c:806
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
Bdc_Ent_t_::fCompl1
unsigned fCompl1
Definition: bdcSpfd.c:406
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
calloc
char * calloc()
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Bdc_Ent_t_::fMark0
unsigned fMark0
Definition: bdcSpfd.c:404
Bdc_SpfdDecomposeTest__
Vec_Wrd_t * Bdc_SpfdDecomposeTest__(Vec_Int_t **pvWeights)
Definition: bdcSpfd.c:576
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
assert
#define assert(ex)
Definition: util_old.h:213
Bdc_Nod_t_
Definition: bdcSpfd.c:32
Bdc_Nod_t_::iFan1g
unsigned iFan1g
Definition: bdcSpfd.c:38
Bdc_SpfdReadFiles6
Vec_Wrd_t * Bdc_SpfdReadFiles6(Vec_Int_t **pvWeights)
Definition: bdcSpfd.c:757
Bdc_Ent_t_::fExor
unsigned fExor
Definition: bdcSpfd.c:407
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
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Truths
static word Truths[6]
Definition: bdcSpfd.c:45
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Bdc_Nod_t
typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
DECLARATIONS ///.
Definition: bdcSpfd.c:31
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223