55 pFile = fopen( pFileName,
"wb" );
56 fprintf( pFile,
"# %d prime numbers up to 2^%d generated by ABC on %s\n", Vec_IntSize(vPrimes), nVars,
Extra_TimeStamp() );
57 fprintf( pFile,
".i %d\n", nVars );
58 fprintf( pFile,
".o %d\n", 1 );
59 fprintf( pFile,
".p %d\n", Vec_IntSize(vPrimes) );
61 for ( k = nVars-1; k >= 0; k-- )
62 fprintf( pFile,
"%d%s", (Prime >> k)&1, k ?
"" :
" 1\n" );
63 fprintf( pFile,
".e\n\n" );
81 int i, k, Prime, Count = 0;
84 for ( k = 0; k < nVars; k++ )
85 if ( !Vec_BitEntry(vMap, Prime ^ (1<<k)) )
91 printf(
"Dist1 pairs = %d. ", Count/2 );
92 Abc_PrintTime( 1,
"Time", Abc_Clock() - clk );
96 int i, n, nBits = ( 1 << nVars );
98 Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 );
99 Vec_BitWriteEntry(vMap, 0, 1);
100 Vec_BitWriteEntry(vMap, 1, 1);
101 for ( n = 2; n < nBits; n++ )
102 if ( !Vec_BitEntry(vMap, n) )
103 for ( i = 2*n; i < nBits; i += n )
104 Vec_BitWriteEntry(vMap, i, 1);
105 for ( n = 2; n < nBits; n++ )
106 if ( !Vec_BitEntry(vMap, n) )
107 Vec_IntPush( vPrimes, n );
108 printf(
"Primes up to 2^%d = %d\n", nVars, Vec_IntSize(vPrimes) );
120 printf(
"Primes up to 2^%d = %d\n", nVars, Vec_IntSize(vPrimes) );
122 Vec_IntFree( vPrimes );
128#define ABC_PRIME_MASK 0xFF
131 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
132 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
133 0x50d66b74,0x2f01ae9e,0xa1a80123,0x3e1ce2dc,0xebedbc57,0x4e68bc34,0x855ee0cf,0x17275120,
134 0x2ae7f2df,0xf71039eb,0x7c283eec,0x70cd1137,0x7cf651f3,0xa87bfa7a,0x14d87f02,0xe82e197d,
135 0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
136 0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10,
137 0x8fa783f7,0x252062ce,0x3dc46b4b,0xf70f6432,0x3f378276,0x44b137a1,0x2bf74b77,0x04892ed6,
138 0xfd318de1,0xd58c235e,0x94c6d25b,0x7aa5f218,0x35c9e921,0x5732fbbb,0x06026481,0xf584a44f,
139 0x946e1b5f,0x8463d5b2,0x4ebca7b2,0x54887b15,0x08d1e804,0x5b22067d,0x794580f6,0xb351ea43,
140 0xbce555b9,0x19ae2194,0xd32f1396,0x6fc1a7f1,0x1fd8a867,0x3a89fdb0,0xea49c61c,0x25f8a879,
141 0xde1e6437,0x7c74afca,0x8ba63e50,0xb1572074,0xe4655092,0xdb6f8b1c,0xc2955f3c,0x327f85ba,
142 0x60a17021,0x95bd261d,0xdea94f28,0x04528b65,0xbe0109cc,0x26dd5688,0x6ab2729d,0xc4f029ce,
143 0xacf7a0be,0x4c912f55,0x34c06e65,0x4fbb938e,0x1533fb5f,0x03da06bd,0x48262889,0xc2523d7d,
144 0x28a71d57,0x89f9713a,0xf574c551,0x7a99deb5,0x52834d91,0x5a6f4484,0xc67ba946,0x13ae698f,
145 0x3e390f34,0x34fc9593,0x894c7932,0x6cf414a3,0xdb7928ab,0x13a3b8a3,0x4b381c1d,0xa10b54cb,
146 0x55359d9d,0x35a3422a,0x58d1b551,0x0fd4de20,0x199eb3f4,0x167e09e2,0x3ee6a956,0x5371a7fa,
147 0xd424efda,0x74f521c5,0xcb899ff6,0x4a42e4f4,0x747917b6,0x4b08df0b,0x090c7a39,0x11e909e4,
148 0x258e2e32,0xd9fad92d,0x48fe5f69,0x0545cde6,0x55937b37,0x9b4ae4e4,0x1332b40e,0xc3792351,
149 0xaff982ef,0x4dba132a,0x38b81ef1,0x28e641bf,0x227208c1,0xec4bbe37,0xc4e1821c,0x512c9d09,
150 0xdaef1257,0xb63e7784,0x043e04d7,0x9c2cea47,0x45a0e59a,0x281315ca,0x849f0aac,0xa4071ed3,
151 0x0ef707b3,0xfe8dac02,0x12173864,0x471f6d46,0x24a53c0a,0x35ab9265,0xbbf77406,0xa2144e79,
152 0xb39a884a,0x0baf5b6d,0xcccee3dd,0x12c77584,0x2907325b,0xfd1adcd2,0xd16ee972,0x345ad6c1,
153 0x315ebe66,0xc7ad2b8d,0x99e82c8d,0xe52da8c8,0xba50f1d3,0x66689cd8,0x2e8e9138,0x43e15e74,
154 0xf1ced14d,0x188ec52a,0xe0ef3cbb,0xa958aedc,0x4107a1bc,0x5a9e7a3e,0x3bde939f,0xb5b28d5a,
155 0x596fe848,0xe85ad00c,0x0b6b3aae,0x44503086,0x25b5695c,0xc0c31dcd,0x5ee617f0,0x74d40c3a,
156 0xd2cb2b9f,0x1e19f5fa,0x81e24faf,0xa01ed68f,0xcee172fc,0x7fdf2e4d,0x002f4774,0x664f82dd,
157 0xc569c39a,0xa2d4dcbe,0xaadea306,0xa4c947bf,0xa413e4e3,0x81fb5486,0x8a404970,0x752c980c,
158 0x98d1d881,0x5c932c1e,0xeee65dfb,0x37592cdd,0x0fd4e65b,0xad1d383f,0x62a1452f,0x8872f68d,
159 0xb58c919b,0x345c8ee3,0xb583a6d6,0x43d72cb3,0x77aaa0aa,0xeb508242,0xf2db64f8,0x86294328,
160 0x82211731,0x1239a9d5,0x673ba5de,0xaf4af007,0x44203b19,0x2399d955,0xa175cd12,0x595928a7,
161 0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0,
162 0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d
167#define TAB_UNUSED 0xFFFF
193static inline int * Tab_ManCube(
Tab_Man_t *
p,
int i ) {
assert(i >= 0 && i < p->nCubes);
return p->pCubes + i * (
p->nVars + 1); }
194static inline Tab_Ent_t * Tab_ManEnt(
Tab_Man_t *
p,
int i ) {
assert(i >= -1 && i < p->nTable);
return i >= 0 ?
p->pTable + i : NULL; }
196static inline int Tab_ManValue(
Tab_Man_t *
p,
int a )
198 assert( a >= 0 && a < 256 );
199 return s_256Primes[a];
201static inline int Tab_ManFinal(
Tab_Man_t *
p,
int a )
207 word Value = 0;
int i;
208 for ( i = 1; i <= pCube[0]; i++ )
209 Value += Tab_ManValue(
p, pCube[i] );
212static inline word Tab_ManHashValueWithoutVar(
Tab_Man_t *
p,
int * pCube,
int iVar )
214 word Value = 0;
int i;
215 for ( i = 1; i <= pCube[0]; i++ )
217 Value += Tab_ManValue(
p, pCube[i] );
220static inline unsigned Tab_ManHashValueCube(
Tab_Man_t *
p,
int c,
int iVar )
222 if ( iVar == 0xFFFF )
223 return (
unsigned)(
p->pValues[c] %
p->nTable);
224 return (
unsigned)((
p->pValues[c] - Tab_ManValue(
p, Tab_ManCube(
p, c)[iVar+1])) %
p->nTable);
226static inline void Tab_ManPrintCube(
Tab_Man_t *
p,
int c,
int Var )
228 int i, * pCube = Tab_ManCube(
p, c );
229 for ( i = 1; i <= pCube[0]; i++ )
233 printf(
"%d", !Abc_LitIsCompl(pCube[i]) );
235static inline void Tab_ManHashAdd(
Tab_Man_t *
p,
int Value,
int Cube,
int VarA,
int VarB )
244 if ( pBin->
Table >= 0 )
251static inline void Tab_ManPrintEntry(
Tab_Man_t *
p,
int e )
253 printf(
"Entry %10d : ", e );
254 printf(
"Cube %6d ",
p->pTable[e].Cube );
255 printf(
"Value %12u ", Tab_ManHashValueCube(
p,
p->pTable[e].Cube,
p->pTable[e].VarA) %
p->nTable );
256 Tab_ManPrintCube(
p,
p->pTable[e].Cube,
p->pTable[e].VarA );
258 if (
p->pTable[e].VarA != 0xFFFF )
259 printf(
"%2d ",
p->pTable[e].VarA );
262 if (
p->pTable[e].VarB != 0xFFFF )
263 printf(
"%2d ",
p->pTable[e].VarB );
271 Vec_IntClear( vBin );
272 for ( pEnt = Tab_ManEnt(
p, pEnt->
Table); pEnt; pEnt = Tab_ManEnt(
p, pEnt->
Next) )
274 Vec_IntPush( vBin, pEnt -
p->pTable );
280#define Tab_ManForEachCube( p, pCube, c ) \
281 for ( c = 0; c < p->nCubes && (pCube = Tab_ManCube(p, c)); c++ ) \
282 if ( pCube[0] == -1 ) {} else
284#define Tab_ManForEachCubeReverse( p, pCube, c ) \
285 for ( c = p->nCubes - 1; c >= 0 && (pCube = Tab_ManCube(p, c)); c-- ) \
286 if ( pCube[0] == -1 ) {} else
305 p->Degree = Abc_Base2Log((
p->nVars + 1) *
p->nCubes + 1) + 3;
306 p->Mask = (1 <<
p->Degree) - 1;
311 printf(
"Allocated %.2f MB for cube structure.\n", 4.0 *
p->nCubes * (
p->nVars + 2) / (1 << 20) );
323 int * pCube,
Cube, c, v;
327 Cube = Vec_IntEntry( vCubes, c );
329 for ( v = 0; v <
p->nVars; v++ )
330 pCube[v+1] = Abc_Var2Lit( v, !((
Cube >> v) & 1) );
331 p->pValues[c] = Tab_ManHashValue(
p, pCube );
332 p->nLits += pCube[0];
350 int * pBeg1 = pCube1 + 1;
351 int * pBeg2 = pCube2 + 1;
352 int * pEnd1 = pBeg1 + pCube1[0];
353 int * pEnd2 = pBeg2 + pCube2[0];
354 int Counter = 0, fAttr0 = 0, fAttr1 = 1;
355 Vec_IntClear( vCubeFree );
356 while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
358 if ( *pBeg1 == *pBeg2 )
359 pBeg1++, pBeg2++, Counter++;
360 else if ( *pBeg1 < *pBeg2 )
361 Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
364 if ( Vec_IntSize(vCubeFree) == 0 )
365 fAttr0 = 1, fAttr1 = 0;
366 Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
369 while ( pBeg1 < pEnd1 )
370 Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
371 while ( pBeg2 < pEnd2 )
372 Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
373 if ( Vec_IntSize(vCubeFree) == 0 )
374 printf(
"The SOP has duplicated cubes.\n" );
375 else if ( Vec_IntSize(vCubeFree) == 1 )
376 printf(
"The SOP has contained cubes.\n" );
379 assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
385 for ( i1 = i2 = 1; ; i1++, i2++ )
387 if ( i1 ==
Var1 ) i1++;
388 if ( i2 == Var2 ) i2++;
389 if ( i1 > pCube1[0] || i2 > pCube2[0] )
391 if ( pCube1[i1] != pCube2[i2] )
393 if ( i1 == pCube1[0] && i2 == pCube2[0] )
399 int Cube1[32], Cube2[32];
400 int i, k, nVars1, nVars2;
401 assert( pCube1[0] <= 32 );
402 assert( pCube2[0] <= 32 );
403 for ( i = 1, k = 0; i <= pCube1[0]; i++ )
405 Cube1[k++] = pCube1[i];
407 for ( i = 1, k = 0; i <= pCube2[0]; i++ )
409 Cube2[k++] = pCube2[i];
411 if ( nVars1 != nVars2 )
413 for ( i = 0; i < nVars1; i++ )
414 if ( Cube1[i] != Cube2[i] )
432 Vec_Int_t * vStarts = Vec_IntAlloc(
p->nCubes );
433 int * pCube, c, Count = 0;
436 Vec_IntPush( vStarts, Count );
437 Count += 1 + pCube[0];
439 Count += pCube[0] * pCube[0] / 2;
441 assert( Vec_IntSize(vStarts) ==
p->nCubes );
450 int nBits = Abc_Base2Log( nItems ) + 6;
451 Vec_Bit_t * vPres = Vec_BitStart( 1 << nBits );
452 Vec_Bit_t * vMarks = Vec_BitStart( nItems );
453 Vec_Int_t * vUseful = Vec_IntAlloc( 1000 );
455 Vec_Int_t * vCubeFree = Vec_IntAlloc( 100 );
456 word Value;
unsigned Mask = (1 << nBits) - 1;
457 int * pCube, c, a, b, nMarks = 0, nUseful, Entry1, Entry2;
462 if ( Vec_BitAddEntry(vPres, (
int)
p->pValues[c] & Mask) )
463 Vec_BitWriteEntry( vMarks, nMarks, 1 );
466 for ( a = 1; a <= pCube[0]; a++, nMarks++ )
467 if ( Vec_BitAddEntry(vPres, (
int)(
p->pValues[c] - Tab_ManValue(
p, pCube[a])) & Mask) )
468 Vec_BitWriteEntry( vMarks, nMarks, 1 );
471 for ( a = 1; a <= pCube[0]; a++ )
473 Value =
p->pValues[c] - Tab_ManValue(
p, pCube[a]);
474 for ( b = a + 1; b <= pCube[0]; b++, nMarks++ )
475 if ( Vec_BitAddEntry(vPres, (
int)(Value - Tab_ManValue(
p, pCube[b])) & Mask) )
476 Vec_BitWriteEntry( vMarks, nMarks, 1 );
479 assert( nMarks == nItems );
480 Vec_BitReset( vPres );
485 Value =
p->pValues[c];
488 for ( a = pCube[0]; a >= 1; a-- )
490 Value =
p->pValues[c] - Tab_ManValue(
p, pCube[a]);
491 for ( b = pCube[0]; b >= a + 1; b--, nMarks-- )
492 if ( Vec_BitAddEntry(vPres, (
int)(Value - Tab_ManValue(
p, pCube[b])) & Mask) )
493 Vec_BitWriteEntry( vMarks, nMarks, 1 );
496 for ( a = pCube[0]; a >= 1; a--, nMarks-- )
497 if ( Vec_BitAddEntry(vPres, (
int)(
p->pValues[c] - Tab_ManValue(
p, pCube[a])) & Mask) )
498 Vec_BitWriteEntry( vMarks, nMarks, 1 );
500 if ( Vec_BitAddEntry(vPres, (
int)
p->pValues[c] & Mask) )
501 Vec_BitWriteEntry( vMarks, nMarks, 1 );
506 Vec_BitFree( vPres );
508 nUseful = Vec_BitCount( vMarks );
509printf(
"Items = %d. Bits = %d. Useful = %d. \n", nItems, nBits, nUseful );
512 p->nTable = Abc_PrimeCudd(nUseful);
514printf(
"Table %d\n",
p->nTable );
518 if ( Vec_BitEntry(vMarks, nMarks++) )
521 for ( a = 1; a <= pCube[0]; a++, nMarks++ )
522 if ( Vec_BitEntry(vMarks, nMarks) )
523 Tab_ManHashAdd(
p, (
int)((
p->pValues[c] - Tab_ManValue(
p, pCube[a])) %
p->nTable), c, a-1,
TAB_UNUSED );
526 for ( a = 1; a <= pCube[0]; a++ )
528 Value =
p->pValues[c] - Tab_ManValue(
p, pCube[a]);
529 for ( b = a + 1; b <= pCube[0]; b++, nMarks++ )
530 if ( Vec_BitEntry(vMarks, nMarks) )
531 Tab_ManHashAdd(
p, (
int)((Value - Tab_ManValue(
p, pCube[b])) %
p->nTable), c, a-1, b-1 );
534 assert( nMarks == nItems );
536 for ( c = 0; c <
p->nTable; c++ )
538 Tab_ManHashCollectBin(
p, c, vBin );
547 int * pCubeA = Tab_ManCube(
p, pEntA->
Cube );
548 int * pCubeB = Tab_ManCube(
p, pEntB->
Cube );
553 Vec_IntPushTwo( vUseful, pEntA->
Cube, pEntB->
Cube );
561 Vec_IntFree( vCubeFree );
563 Vec_BitFree( vMarks );
586 printf(
"Created %d cubes dependent on %d variables.\n",
p->nCubes,
p->nVars );
588 printf(
"Collected %d pairs.\n", Vec_IntSize(vPairs)/2 );
589 Vec_IntFree( vPairs );
591 Vec_IntFree( vPrimes );
592 Abc_PrintTime( 1,
"Time", Abc_Clock() - clk );
#define ABC_FALLOC(type, num)
#define ABC_CALLOC(type, num)
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
unsigned __int64 word
DECLARATIONS ///.
struct Tab_Man_t_ Tab_Man_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)