abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bdcSpfd.c File Reference
#include "bdcInt.h"
#include "aig/aig/aig.h"

Go to the source code of this file.

Data Structures

struct  Bdc_Nod_t_
 
struct  Bdc_Ent_t_
 

Macros

#define BDC_TERM   0x1FFFFFFF
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Bdc_Nod_t_ 
Bdc_Nod_t
 DECLARATIONS ///. More...
 
typedef struct Bdc_Ent_t_ Bdc_Ent_t
 

Functions

static int Bdc_CountOnes (word t)
 
static int Bdc_CountSpfd (word t, word f)
 
static word Bdc_Cof6 (word t, int iVar, int fCof1)
 
int Bdc_SpfdAdjCost (word t)
 
void Abc_Show6VarFunc (word F0, word F1)
 
void Bdc_SpfdPrint_rec (Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
 FUNCTION DEFINITIONS ///. More...
 
void Bdc_SpfdPrint (Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
 
void Bdc_SpfdDecompose (word Truth, int nVars, int nCands, int nGatesMax)
 
void Bdc_SpfdDecomposeTest_ ()
 
int Bdc_SpfdMark0 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
int Bdc_SpfdMark1 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
void Bdc_SpfdUnmark0 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
void Bdc_SpfdUnmark1 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
int Bdc_SpfdCheckOverlap (Bdc_Ent_t *p, Bdc_Ent_t *pEnt0, Bdc_Ent_t *pEnt1)
 
int Bdc_SpfdHashValue (word t, int Size)
 
int * Bdc_SpfdHashLookup (Bdc_Ent_t *p, int Size, word t)
 
Vec_Wrd_tBdc_SpfdDecomposeTest__ (Vec_Int_t **pvWeights)
 
Vec_Wrd_tBdc_SpfdReadFiles5 (Vec_Int_t **pvWeights)
 
Vec_Wrd_tBdc_SpfdReadFiles6 (Vec_Int_t **pvWeights)
 
int Bdc_SpfdComputeCost (word f, int i, Vec_Int_t *vWeights)
 
word Bdc_SpfdFindBest (Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
 
int Bdc_SpfdDecomposeTestOne (word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
 
void Bdc_SpfdDecomposeTest44 ()
 
void Bdc_SpfdDecomposeTest3 ()
 
void Bdc_SpfdDecomposeTest8 ()
 
void Bdc_SpfdDecomposeTest ()
 

Variables

static word Truths [6]
 

Macro Definition Documentation

#define BDC_TERM   0x1FFFFFFF

Definition at line 414 of file bdcSpfd.c.

Typedef Documentation

typedef struct Bdc_Ent_t_ Bdc_Ent_t

Definition at line 398 of file bdcSpfd.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t

DECLARATIONS ///.

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

FileName [bdcSpfd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Truth-table-based bi-decomposition engine.]

Synopsis [The gateway to bi-decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 30, 2007.]

Revision [

Id:
bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp

]

Definition at line 31 of file bdcSpfd.c.

Function Documentation

void Abc_Show6VarFunc ( word  F0,
word  F1 
)

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

Synopsis [Prints K-map of 6-var function represented by truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1508 of file abcPrint.c.

1509 {
1510  // order of cells in the Karnaugh map
1511 // int Cells[8] = { 0, 1, 3, 2, 6, 7, 5, 4 };
1512  int Cells[8] = { 0, 4, 6, 2, 3, 7, 5, 1 };
1513  // intermediate variables
1514  int s; // symbol counter
1515  int h; // horizontal coordinate;
1516  int v; // vertical coordinate;
1517  assert( (F0 & F1) == 0 );
1518 
1519  // output minterms above
1520  for ( s = 0; s < 4; s++ )
1521  printf( " " );
1522  printf( " " );
1523  for ( h = 0; h < 8; h++ )
1524  {
1525  for ( s = 0; s < 3; s++ )
1526  printf( "%d", ((Cells[h] >> (2-s)) & 1) );
1527  printf( " " );
1528  }
1529  printf( "\n" );
1530 
1531  // output horizontal line above
1532  for ( s = 0; s < 4; s++ )
1533  printf( " " );
1534  printf( "+" );
1535  for ( h = 0; h < 8; h++ )
1536  {
1537  for ( s = 0; s < 3; s++ )
1538  printf( "-" );
1539  printf( "+" );
1540  }
1541  printf( "\n" );
1542 
1543  // output lines with function values
1544  for ( v = 0; v < 8; v++ )
1545  {
1546  for ( s = 0; s < 3; s++ )
1547  printf( "%d", ((Cells[v] >> (2-s)) & 1) );
1548  printf( " |" );
1549 
1550  for ( h = 0; h < 8; h++ )
1551  {
1552  printf( " " );
1553  if ( ((F0 >> ((Cells[v]*8)+Cells[h])) & 1) )
1554  printf( "0" );
1555  else if ( ((F1 >> ((Cells[v]*8)+Cells[h])) & 1) )
1556  printf( "1" );
1557  else
1558  printf( " " );
1559  printf( " |" );
1560  }
1561  printf( "\n" );
1562 
1563  // output horizontal line above
1564  for ( s = 0; s < 4; s++ )
1565  printf( " " );
1566 // printf( "%c", v == 7 ? '+' : '|' );
1567  printf( "+" );
1568  for ( h = 0; h < 8; h++ )
1569  {
1570  for ( s = 0; s < 3; s++ )
1571  printf( "-" );
1572 // printf( "%c", v == 7 ? '+' : '|' );
1573  printf( "%c", (v == 7 || h == 7) ? '+' : '|' );
1574  }
1575  printf( "\n" );
1576  }
1577 }
#define assert(ex)
Definition: util_old.h:213
static word Bdc_Cof6 ( word  t,
int  iVar,
int  fCof1 
)
inlinestatic

Definition at line 73 of file bdcSpfd.c.

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 }
#define assert(ex)
Definition: util_old.h:213
static word Truths[6]
Definition: bdcSpfd.c:45
static int Bdc_CountOnes ( word  t)
inlinestatic

Definition at line 54 of file bdcSpfd.c.

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 }
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
static int Bdc_CountSpfd ( word  t,
word  f 
)
inlinestatic

Definition at line 64 of file bdcSpfd.c.

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 }
static int Bdc_CountOnes(word t)
Definition: bdcSpfd.c:54
int Bdc_SpfdAdjCost ( word  t)

Definition at line 82 of file bdcSpfd.c.

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 }
static word Bdc_Cof6(word t, int iVar, int fCof1)
Definition: bdcSpfd.c:73
static int Bdc_CountOnes(word t)
Definition: bdcSpfd.c:54
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
int Bdc_SpfdCheckOverlap ( Bdc_Ent_t p,
Bdc_Ent_t pEnt0,
Bdc_Ent_t pEnt1 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 479 of file bdcSpfd.c.

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 }
void Bdc_SpfdUnmark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:458
int Bdc_SpfdMark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:439
void Bdc_SpfdUnmark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:450
int Bdc_SpfdMark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:428
#define assert(ex)
Definition: util_old.h:213
int Bdc_SpfdComputeCost ( word  f,
int  i,
Vec_Int_t vWeights 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 786 of file bdcSpfd.c.

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 }
static int Bdc_CountOnes(word t)
Definition: bdcSpfd.c:54
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
void Bdc_SpfdDecompose ( word  Truth,
int  nVars,
int  nCands,
int  nGatesMax 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file bdcSpfd.c.

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 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static int Bdc_CountSpfd(word t, word f)
Definition: bdcSpfd.c:64
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Bdc_SpfdPrint(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
Definition: bdcSpfd.c:157
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Bdc_CountOnes(word t)
Definition: bdcSpfd.c:54
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition: utilSort.c:238
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int pPerm[13719]
Definition: rwrTemp.c:32
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
static word Truths[6]
Definition: bdcSpfd.c:45
typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
DECLARATIONS ///.
Definition: bdcSpfd.c:31
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Bdc_SpfdDecomposeTest ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1134 of file bdcSpfd.c.

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 }
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
word Aig_ManRandom64(int fReset)
Definition: aigUtil.c:1182
static abctime Abc_Clock()
Definition: abc_global.h:279
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Counter
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
ABC_INT64_T abctime
Definition: abc_global.h:278
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
void Bdc_SpfdDecomposeTest3 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1027 of file bdcSpfd.c.

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 }
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
word Aig_ManRandom64(int fReset)
Definition: aigUtil.c:1182
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Counter
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
ABC_INT64_T abctime
Definition: abc_global.h:278
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
void Bdc_SpfdDecomposeTest44 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 904 of file bdcSpfd.c.

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 }
static word Bdc_Cof6(word t, int iVar, int fCof1)
Definition: bdcSpfd.c:73
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
int Bdc_SpfdDecomposeTestOne(word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
Definition: bdcSpfd.c:871
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Vec_Wrd_t * Bdc_SpfdDecomposeTest__(Vec_Int_t **pvWeights)
Definition: bdcSpfd.c:576
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
static word Truths[6]
Definition: bdcSpfd.c:45
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
void Bdc_SpfdDecomposeTest8 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1079 of file bdcSpfd.c.

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 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Wrd_t * Bdc_SpfdReadFiles5(Vec_Int_t **pvWeights)
Definition: bdcSpfd.c:725
static abctime Abc_Clock()
Definition: abc_global.h:279
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
void Abc_Show6VarFunc(word F0, word F1)
Definition: abcPrint.c:1508
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
int Bdc_SpfdAdjCost(word t)
Definition: bdcSpfd.c:82
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
ABC_INT64_T abctime
Definition: abc_global.h:278
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
void Bdc_SpfdDecomposeTest_ ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file bdcSpfd.c.

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 }
void Bdc_SpfdDecompose(word Truth, int nVars, int nCands, int nGatesMax)
Definition: bdcSpfd.c:177
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Vec_Wrd_t* Bdc_SpfdDecomposeTest__ ( Vec_Int_t **  pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 576 of file bdcSpfd.c.

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 }
char * memset()
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
VOID_HACK free()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
unsigned iFan1
Definition: bdcSpfd.c:405
#define BDC_TERM
Definition: bdcSpfd.c:414
unsigned fCompl
Definition: bdcSpfd.c:403
int * Bdc_SpfdHashLookup(Bdc_Ent_t *p, int Size, word t)
Definition: bdcSpfd.c:549
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
unsigned fCompl0
Definition: bdcSpfd.c:402
word Truth
Definition: bdcSpfd.c:411
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_WrdClear(Vec_Wrd_t *p)
Definition: vecWrd.h:602
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
int iList
Definition: bdcSpfd.c:410
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned iFan0
Definition: bdcSpfd.c:401
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
unsigned fCompl1
Definition: bdcSpfd.c:406
char * calloc()
#define assert(ex)
Definition: util_old.h:213
unsigned fExor
Definition: bdcSpfd.c:407
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
static word Truths[6]
Definition: bdcSpfd.c:45
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
int Bdc_SpfdDecomposeTestOne ( word  t,
Vec_Wrd_t vDivs,
Vec_Int_t vWeights 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 871 of file bdcSpfd.c.

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 }
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
int Bdc_SpfdAdjCost(word t)
Definition: bdcSpfd.c:82
word Bdc_SpfdFindBest(Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
Definition: bdcSpfd.c:806
word Bdc_SpfdFindBest ( Vec_Wrd_t vDivs,
Vec_Int_t vWeights,
word  F0,
word  F1,
int *  pCost 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 806 of file bdcSpfd.c.

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 }
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
int Bdc_SpfdComputeCost(word f, int i, Vec_Int_t *vWeights)
Definition: bdcSpfd.c:786
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
#define assert(ex)
Definition: util_old.h:213
int* Bdc_SpfdHashLookup ( Bdc_Ent_t p,
int  Size,
word  t 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 549 of file bdcSpfd.c.

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 }
int iNext
Definition: bdcSpfd.c:409
int Bdc_SpfdHashValue(word t, int Size)
Definition: bdcSpfd.c:501
word Truth
Definition: bdcSpfd.c:411
int iList
Definition: bdcSpfd.c:410
#define assert(ex)
Definition: util_old.h:213
int Bdc_SpfdHashValue ( word  t,
int  Size 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 501 of file bdcSpfd.c.

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 }
int Bdc_SpfdMark0 ( Bdc_Ent_t p,
Bdc_Ent_t pEnt 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 428 of file bdcSpfd.c.

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 }
unsigned iFan1
Definition: bdcSpfd.c:405
#define BDC_TERM
Definition: bdcSpfd.c:414
int Bdc_SpfdMark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:428
unsigned fMark1
Definition: bdcSpfd.c:408
unsigned iFan0
Definition: bdcSpfd.c:401
unsigned fMark0
Definition: bdcSpfd.c:404
int Bdc_SpfdMark1 ( Bdc_Ent_t p,
Bdc_Ent_t pEnt 
)

Definition at line 439 of file bdcSpfd.c.

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 }
unsigned iFan1
Definition: bdcSpfd.c:405
#define BDC_TERM
Definition: bdcSpfd.c:414
int Bdc_SpfdMark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:439
unsigned fMark1
Definition: bdcSpfd.c:408
unsigned iFan0
Definition: bdcSpfd.c:401
unsigned fMark0
Definition: bdcSpfd.c:404
void Bdc_SpfdPrint ( Bdc_Nod_t pNode,
int  Level,
Vec_Ptr_t vLevels,
word  Truth 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file bdcSpfd.c.

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 }
void Bdc_SpfdPrint_rec(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
FUNCTION DEFINITIONS ///.
Definition: bdcSpfd.c:113
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
void Bdc_SpfdPrint_rec ( Bdc_Nod_t pNode,
int  Level,
Vec_Ptr_t vLevels 
)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file bdcSpfd.c.

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 }
void Bdc_SpfdPrint_rec(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
FUNCTION DEFINITIONS ///.
Definition: bdcSpfd.c:113
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
DECLARATIONS ///.
Definition: bdcSpfd.c:31
Vec_Wrd_t* Bdc_SpfdReadFiles5 ( Vec_Int_t **  pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file bdcSpfd.c.

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 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Vec_Wrd_t* Bdc_SpfdReadFiles6 ( Vec_Int_t **  pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 757 of file bdcSpfd.c.

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 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
void Bdc_SpfdUnmark0 ( Bdc_Ent_t p,
Bdc_Ent_t pEnt 
)

Definition at line 450 of file bdcSpfd.c.

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 }
unsigned iFan1
Definition: bdcSpfd.c:405
#define BDC_TERM
Definition: bdcSpfd.c:414
void Bdc_SpfdUnmark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:450
unsigned iFan0
Definition: bdcSpfd.c:401
unsigned fMark0
Definition: bdcSpfd.c:404
void Bdc_SpfdUnmark1 ( Bdc_Ent_t p,
Bdc_Ent_t pEnt 
)

Definition at line 458 of file bdcSpfd.c.

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 }
void Bdc_SpfdUnmark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition: bdcSpfd.c:458
unsigned iFan1
Definition: bdcSpfd.c:405
#define BDC_TERM
Definition: bdcSpfd.c:414
unsigned fMark1
Definition: bdcSpfd.c:408
unsigned iFan0
Definition: bdcSpfd.c:401

Variable Documentation

word Truths[6]
static
Initial value:
= {
ABC_CONST(0xAAAAAAAAAAAAAAAA),
ABC_CONST(0xCCCCCCCCCCCCCCCC),
ABC_CONST(0xF0F0F0F0F0F0F0F0),
ABC_CONST(0xFF00FF00FF00FF00),
ABC_CONST(0xFFFF0000FFFF0000),
}
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206

Definition at line 45 of file bdcSpfd.c.