ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraUtilSupp.c
Go to the documentation of this file.
1
20
21#include <stdio.h>
22#include <stdlib.h>
23#include <string.h>
24#include <assert.h>
25#include "misc/vec/vec.h"
26#include "misc/vec/vecWec.h"
27#include "extra.h"
28
30
34
35extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
36
37
41
53static inline int Abc_SuppCountOnes( unsigned i )
54{
55 i = i - ((i >> 1) & 0x55555555);
56 i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
57 i = ((i + (i >> 4)) & 0x0F0F0F0F);
58 return (i*(0x01010101))>>24;
59}
60Vec_Wrd_t * Abc_SuppGen( int m, int n )
61{
62 Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
63 int i, Size = (1 << n);
64 for ( i = 0; i < Size; i++ )
65 if ( Abc_SuppCountOnes(i) == m )
66 Vec_WrdPush( vRes, i );
67 return vRes;
68}
69
81void Abc_SuppVerify( Vec_Wrd_t * p, word * pMatrix, int nVars, int nVarsMin )
82{
83 Vec_Wrd_t * pNew;
84 word * pLimit, * pEntry1, * pEntry2;
85 word Entry, EntryNew;
86 int i, k, v, Value, Counter = 0;
87 pNew = Vec_WrdAlloc( Vec_WrdSize(p) );
88 Vec_WrdForEachEntry( p, Entry, i )
89 {
90 EntryNew = 0;
91 for ( v = 0; v < nVarsMin; v++ )
92 {
93 Value = 0;
94 for ( k = 0; k < nVars; k++ )
95 if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) )
96 Value ^= 1;
97 if ( Value )
98 EntryNew |= (((word)1) << v);
99 }
100 Vec_WrdPush( pNew, EntryNew );
101 }
102 // check that they are disjoint
103 pLimit = Vec_WrdLimit(pNew);
104 pEntry1 = Vec_WrdArray(pNew);
105 for ( ; pEntry1 < pLimit; pEntry1++ )
106 for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
107 if ( *pEntry1 == *pEntry2 )
108 Counter++;
109 if ( Counter )
110 printf( "The total of %d pairs fail verification.\n", Counter );
111 else
112 printf( "Verification successful.\n" );
113 Vec_WrdFree( pNew );
114}
115
128{
129 Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
130 unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) );
131 word * pLimit = Vec_WrdLimit(p);
132 word * pEntry1 = Vec_WrdArray(p);
133 word * pEntry2, Value;
134 for ( ; pEntry1 < pLimit; pEntry1++ )
135 for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
136 {
137 Value = *pEntry1 ^ *pEntry2;
138 if ( Abc_InfoHasBit(pMap, (int)Value) )
139 continue;
140 Abc_InfoXorBit( pMap, (int)Value );
141 Vec_WrdPush( vRes, Value );
142 }
143 ABC_FREE( pMap );
144 return vRes;
145}
146Vec_Wrd_t * Abc_SuppGenPairs2( int nOnes, int nBits )
147{
148 Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
149 int i, k, Size = (1 << nBits), Value;
150 for ( i = 0; i < Size; i++ )
151 {
152 Value = Abc_SuppCountOnes(i);
153 for ( k = 1; k <= nOnes; k++ )
154 if ( Value == 2*k )
155 break;
156 if ( k <= nOnes )
157 Vec_WrdPush( vRes, i );
158 }
159 return vRes;
160}
161
173void Abc_SuppPrintMask( word uMask, int nBits )
174{
175 int i;
176 for ( i = 0; i < nBits; i++ )
177 printf( "%d", (int)((uMask >> i) & 1) );
178 printf( "\n" );
179}
180void Abc_SuppGenProfile( Vec_Wrd_t * p, int nBits, int * pCounts )
181{
182 word Ent;
183 int i, k, b;
184 Vec_WrdForEachEntry( p, Ent, i )
185 for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ )
186 pCounts[k] += ((Ent >> k) & 1) ^ b;
187}
188void Abc_SuppPrintProfile( Vec_Wrd_t * p, int nBits )
189{
190 int k, Counts[64] = {0};
191 Abc_SuppGenProfile( p, nBits, Counts );
192 for ( k = 0; k < nBits; k++ )
193 printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_WrdSize(p) );
194}
195int Abc_SuppGenFindBest( Vec_Wrd_t * p, int nBits, int * pMerit )
196{
197 int k, kBest = 0, Counts[64] = {0};
198 Abc_SuppGenProfile( p, nBits, Counts );
199 for ( k = 1; k < nBits; k++ )
200 if ( Counts[kBest] < Counts[k] )
201 kBest = k;
202 *pMerit = Counts[kBest];
203 return kBest;
204}
205void Abc_SuppGenSelectVar( Vec_Wrd_t * p, int nBits, int iVar )
206{
207 word * pEntry = Vec_WrdArray(p);
208 word * pLimit = Vec_WrdLimit(p);
209 for ( ; pEntry < pLimit; pEntry++ )
210 if ( (*pEntry >> iVar) & 1 )
211 *pEntry ^= (((word)1) << nBits);
212}
213void Abc_SuppGenFilter( Vec_Wrd_t * p, int nBits )
214{
215 word Ent;
216 int i, k = 0;
217 Vec_WrdForEachEntry( p, Ent, i )
218 if ( ((Ent >> nBits) & 1) == 0 )
219 Vec_WrdWriteEntry( p, k++, Ent );
220 Vec_WrdShrink( p, k );
221}
223{
224 word uMask = 0;
225 int Prev = -1, This, Var;
226 while ( 1 )
227 {
228 Var = Abc_SuppGenFindBest( p, nBits, &This );
229 if ( Prev >= This )
230 break;
231 Prev = This;
232 Abc_SuppGenSelectVar( p, nBits, Var );
233 uMask |= (((word)1) << Var);
234 }
235 return uMask;
236}
237int Abc_SuppMinimize( word * pMatrix, Vec_Wrd_t * p, int nBits, int fVerbose )
238{
239 int i;
240 for ( i = 0; Vec_WrdSize(p) > 0; i++ )
241 {
242// Abc_SuppPrintProfile( p, nBits );
243 pMatrix[i] = Abc_SuppFindOne( p, nBits );
244 Abc_SuppGenFilter( p, nBits );
245 if ( !fVerbose )
246 continue;
247 // print stats
248 printf( "%2d : ", i );
249 printf( "%6d ", Vec_WrdSize(p) );
250 Abc_SuppPrintMask( pMatrix[i], nBits );
251// printf( "\n" );
252 }
253 return i;
254}
255
267void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose )
268{
269 int nVarsMin;
270 word Matrix[64];
271 abctime clk = Abc_Clock();
272 // create the problem
273 Vec_Wrd_t * vRes = Abc_SuppGen( nOnes, nVars );
274 Vec_Wrd_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars );
275 assert( nVars < 100 );
276 printf( "M = %2d N = %2d : ", nOnes, nVars );
277 printf( "K = %6d ", Vec_WrdSize(vRes) );
278 printf( "Total = %12.0f ", 0.5 * Vec_WrdSize(vRes) * (Vec_WrdSize(vRes) - 1) );
279 printf( "Distinct = %8d ", Vec_WrdSize(vPairs) );
280 Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
281 // solve the problem
282 clk = Abc_Clock();
283 nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose );
284 printf( "Solution with %d variables found. ", nVarsMin );
285 Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
286 if ( fCheck )
287 Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin );
288 Vec_WrdFree( vPairs );
289 Vec_WrdFree( vRes );
290}
291
292
304Vec_Wrd_t * Abc_SuppReadMin( char * pFileName, int * pnVars )
305{
306 Vec_Wrd_t * vRes; word uCube;
307 int nCubes = 0, nVars = -1, iVar;
308 char * pCur, * pToken, * pStart = "INPUT F-COVER";
309 char * pStr = Extra_FileReadContents( pFileName );
310 if ( pStr == NULL )
311 { printf( "Cannot open input file (%s).\n", pFileName ); return NULL; }
312 pCur = strstr( pStr, pStart );
313 if ( pCur == NULL )
314 { printf( "Cannot find beginning of cube cover (%s).\n", pStart ); return NULL; }
315 pToken = strtok( pCur + strlen(pStart), " \t\r\n," );
316 nCubes = atoi( pToken );
317 if ( nCubes < 1 || nCubes > 1000000 )
318 { printf( "The number of cubes in not in the range [1; 1000000].\n" ); return NULL; }
319 vRes = Vec_WrdAlloc( 1000 );
320 uCube = 0; iVar = 0;
321 while ( (pToken = strtok(NULL, " \t\r\n,")) != NULL )
322 {
323 if ( strlen(pToken) > 2 )
324 {
325 if ( !strncmp(pToken, "INPUT", strlen("INPUT")) )
326 break;
327 if ( iVar > 64 )
328 { printf( "The number of inputs (%d) is too high.\n", iVar ); Vec_WrdFree(vRes); return NULL; }
329 if ( nVars == -1 )
330 nVars = iVar;
331 else if ( nVars != iVar )
332 { printf( "The number of inputs (%d) does not match declaration (%d).\n", nVars, iVar ); Vec_WrdFree(vRes); return NULL; }
333 Vec_WrdPush( vRes, uCube );
334 uCube = 0; iVar = 0;
335 continue;
336 }
337 if ( pToken[1] == '0' && pToken[0] == '1' ) // value 1
338 uCube |= (((word)1) << iVar);
339 else if ( pToken[1] != '1' || pToken[0] != '0' ) // value 0
340 { printf( "Strange literal representation (%s) of cube %d.\n", pToken, nCubes ); Vec_WrdFree(vRes); return NULL; }
341 iVar++;
342 }
343 ABC_FREE( pStr );
344 if ( Vec_WrdSize(vRes) != nCubes )
345 { printf( "The number of cubes (%d) does not match declaration (%d).\n", Vec_WrdSize(vRes), nCubes ); Vec_WrdFree(vRes); return NULL; }
346 else
347 printf( "Successfully parsed function with %d inputs and %d cubes.\n", nVars, nCubes );
348 *pnVars = nVars;
349 return vRes;
350}
351
364{
365 abctime clk = Abc_Clock();
366 word * pEnt2, * pEnt = Vec_WrdArray( vCubes );
367 word * pLimit = Vec_WrdLimit( vCubes );
368 Vec_Wrd_t * vRes, * vPairs = Vec_WrdAlloc( Vec_WrdSize(vCubes) * (Vec_WrdSize(vCubes) - 1) / 2 );
369 word * pStore = Vec_WrdArray( vPairs );
370 for ( ; pEnt < pLimit; pEnt++ )
371 for ( pEnt2 = pEnt+1; pEnt2 < pLimit; pEnt2++ )
372 *pStore++ = *pEnt ^ *pEnt2;
373 vPairs->nSize = Vec_WrdCap(vPairs);
374 assert( pStore == Vec_WrdLimit(vPairs) );
375// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
376// vRes = Vec_WrdUniqifyHash( vPairs, 1 );
377 vRes = Vec_WrdDup( vPairs );
378 printf( "Successfully generated diff matrix with %10d rows (%6.2f %%). ",
379 Vec_WrdSize(vRes), 100.0 * Vec_WrdSize(vRes) / Vec_WrdSize(vPairs) );
380 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
381 Vec_WrdFree( vPairs );
382 return vRes;
383}
384
396static inline int Abc_SuppCountOnes64( word i )
397{
398 i = i - ((i >> 1) & 0x5555555555555555);
399 i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
400 i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
401 return (i*(0x0101010101010101))>>56;
402}
403int Abc_SuppFindVar( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
404{
405 int v, vBest = -1, dBest = -1;
406 for ( v = 0; v < nVars; v++ )
407 {
408 if ( Vec_WecLevelSize(pS, v) )
409 continue;
410 if ( vBest == -1 || dBest > Vec_WecLevelSize(pD, v) )
411 vBest = v, dBest = Vec_WecLevelSize(pD, v);
412 }
413 return vBest;
414}
415void Abc_SuppRemove( Vec_Wrd_t * p, int * pCounts, Vec_Wec_t * pS, Vec_Wec_t * pD, int iVar, int nVars )
416{
417 word Entry; int i, v;
418 assert( Vec_WecLevelSize(pS, iVar) == 0 );
419 Vec_IntClear( Vec_WecEntry(pD, iVar) );
420 Vec_WrdForEachEntry( p, Entry, i )
421 {
422 if ( ((Entry >> iVar) & 1) == 0 )
423 continue;
424 pCounts[i]--;
425 if ( pCounts[i] == 1 )
426 {
427 for ( v = 0; v < nVars; v++ )
428 if ( (Entry >> v) & 1 )
429 {
430 Vec_IntRemove( Vec_WecEntry(pD, v), i );
431 Vec_WecPush( pS, v, i );
432 }
433 }
434 else if ( pCounts[i] == 2 )
435 {
436 for ( v = 0; v < nVars; v++ )
437 if ( (Entry >> v) & 1 )
438 Vec_WecPush( pD, v, i );
439 }
440 }
441}
442void Abc_SuppProfile( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
443{
444 int v;
445 for ( v = 0; v < nVars; v++ )
446 printf( "%2d : S = %3d D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) );
447}
448int Abc_SuppSolve( Vec_Wrd_t * p, int nVars )
449{
450 abctime clk = Abc_Clock();
451 Vec_Wrd_t * pNew = Vec_WrdDup( p );
452 Vec_Wec_t * vSingles = Vec_WecStart( 64 );
453 Vec_Wec_t * vDoubles = Vec_WecStart( 64 );
454 word Entry; int i, v, iVar, nVarsNew = nVars;
455 int * pCounts = ABC_ALLOC( int, Vec_WrdSize(p) );
456 Vec_WrdForEachEntry( p, Entry, i )
457 {
458 pCounts[i] = Abc_SuppCountOnes64( Entry );
459 if ( pCounts[i] == 1 )
460 {
461 for ( v = 0; v < nVars; v++ )
462 if ( (Entry >> v) & 1 )
463 Vec_WecPush( vSingles, v, i );
464 }
465 else if ( pCounts[i] == 2 )
466 {
467 for ( v = 0; v < nVars; v++ )
468 if ( (Entry >> v) & 1 )
469 Vec_WecPush( vDoubles, v, i );
470 }
471 }
472 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
473// Abc_SuppProfile( vSingles, vDoubles, nVars );
474 // find variable in 0 singles and the smallest doubles
475 while ( 1 )
476 {
477 iVar = Abc_SuppFindVar( vSingles, vDoubles, nVars );
478 if ( iVar == -1 )
479 break;
480// printf( "Selected variable %d.\n", iVar );
481 Abc_SuppRemove( pNew, pCounts, vSingles, vDoubles, iVar, nVars );
482// Abc_SuppProfile( vSingles, vDoubles, nVars );
483 nVarsNew--;
484 }
485// printf( "Result = %d (out of %d)\n", nVarsNew, nVars );
486 Vec_WecFree( vSingles );
487 Vec_WecFree( vDoubles );
488 Vec_WrdFree( pNew );
489 ABC_FREE( pCounts );
490 return nVarsNew;
491}
492
504void Abc_SuppReadMinTest( char * pFileName )
505{
506// int fVerbose = 0;
507 abctime clk = Abc_Clock();
508// word Matrix[64];
509 int nVars, nVarsMin;
510 Vec_Wrd_t * vPairs, * vCubes;
511 vCubes = Abc_SuppReadMin( pFileName, &nVars );
512 if ( vCubes == NULL )
513 return;
514 vPairs = Abc_SuppDiffMatrix( vCubes );
515 Vec_WrdFreeP( &vCubes );
516 // solve the problem
517 clk = Abc_Clock();
518// nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose );
519 nVarsMin = Abc_SuppSolve( vPairs, nVars );
520 printf( "Solution with %d variables found. ", nVarsMin );
521 Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
522
523 Vec_WrdFreeP( &vPairs );
524}
525
529
530
532
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
int Var
Definition exorList.c:228
void Abc_SuppTest(int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose)
Vec_Wrd_t * Abc_SuppGen(int m, int n)
Vec_Wrd_t * Abc_SuppReadMin(char *pFileName, int *pnVars)
Vec_Wrd_t * Abc_SuppGenPairs2(int nOnes, int nBits)
int Abc_SuppFindVar(Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
int Abc_SuppSolve(Vec_Wrd_t *p, int nVars)
void Abc_SuppGenFilter(Vec_Wrd_t *p, int nBits)
int Abc_SuppGenFindBest(Vec_Wrd_t *p, int nBits, int *pMerit)
Vec_Wrd_t * Abc_SuppDiffMatrix(Vec_Wrd_t *vCubes)
void Abc_SuppPrintProfile(Vec_Wrd_t *p, int nBits)
void Abc_SuppPrintMask(word uMask, int nBits)
Vec_Wrd_t * Abc_SuppGenPairs(Vec_Wrd_t *p, int nBits)
void Abc_SuppGenProfile(Vec_Wrd_t *p, int nBits, int *pCounts)
void Abc_SuppProfile(Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
void Abc_SuppGenSelectVar(Vec_Wrd_t *p, int nBits, int iVar)
word Abc_SuppFindOne(Vec_Wrd_t *p, int nBits)
void Abc_SuppVerify(Vec_Wrd_t *p, word *pMatrix, int nVars, int nVarsMin)
void Abc_SuppRemove(Vec_Wrd_t *p, int *pCounts, Vec_Wec_t *pS, Vec_Wec_t *pD, int iVar, int nVars)
void Abc_SuppReadMinTest(char *pFileName)
int Abc_SuppMinimize(word *pMatrix, Vec_Wrd_t *p, int nBits, int fVerbose)
ABC_NAMESPACE_IMPL_START void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
DECLARATIONS ///.
char * Extra_FileReadContents(char *pFileName)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
#define assert(ex)
Definition util_old.h:213
int strncmp()
int strlen()
char * strtok()
char * strstr()
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42