abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraUtilSupp.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraUtilSupp.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [extra]
8 
9  Synopsis [Support minimization.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: extraUtilSupp.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
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 
29 ABC_NAMESPACE_IMPL_START
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
36 
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis [Generate m-out-of-n vectors.]
45 
46  Description []
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 static 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 }
60 Vec_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 
70 /**Function*************************************************************
71 
72  Synopsis [Perform verification.]
73 
74  Description []
75 
76  SideEffects []
77 
78  SeeAlso []
79 
80 ***********************************************************************/
81 void 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 
116 /**Function*************************************************************
117 
118  Synopsis [Generate pairs.]
119 
120  Description []
121 
122  SideEffects []
123 
124  SeeAlso []
125 
126 ***********************************************************************/
127 Vec_Wrd_t * Abc_SuppGenPairs( Vec_Wrd_t * p, int nBits )
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 }
146 Vec_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 
162 /**Function*************************************************************
163 
164  Synopsis [Select variable.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 void 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 }
180 void 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 }
188 void 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 }
195 int 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 }
205 void 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 }
213 void 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 }
222 word Abc_SuppFindOne( Vec_Wrd_t * p, int nBits )
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 }
237 int 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 
256 /**Function*************************************************************
257 
258  Synopsis [Create representation.]
259 
260  Description []
261 
262  SideEffects []
263 
264  SeeAlso []
265 
266 ***********************************************************************/
267 void 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 
293 /**Function*************************************************************
294 
295  Synopsis [Reads the input part of the cubes specified in MIN format.]
296 
297  Description []
298 
299  SideEffects []
300 
301  SeeAlso []
302 
303 ***********************************************************************/
304 Vec_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 
352 /**Function*************************************************************
353 
354  Synopsis []
355 
356  Description []
357 
358  SideEffects []
359 
360  SeeAlso []
361 
362 ***********************************************************************/
363 Vec_Wrd_t * Abc_SuppDiffMatrix( Vec_Wrd_t * vCubes )
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 
385 /**Function*************************************************************
386 
387  Synopsis [Solve difference matrix.]
388 
389  Description []
390 
391  SideEffects []
392 
393  SeeAlso []
394 
395 ***********************************************************************/
396 static 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 }
403 int 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 }
415 void 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 }
442 void 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 }
448 int 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 
493 /**Function*************************************************************
494 
495  Synopsis []
496 
497  Description []
498 
499  SideEffects []
500 
501  SeeAlso []
502 
503 ***********************************************************************/
504 void 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 
526 ////////////////////////////////////////////////////////////////////////
527 /// END OF FILE ///
528 ////////////////////////////////////////////////////////////////////////
529 
530 
531 ABC_NAMESPACE_IMPL_END
532 
Abc_SuppCountOnes
static int Abc_SuppCountOnes(unsigned i)
FUNCTION DEFINITIONS ///.
Definition: extraUtilSupp.c:53
Abc_SuppGenFilter
void Abc_SuppGenFilter(Vec_Wrd_t *p, int nBits)
Definition: extraUtilSupp.c:213
Abc_SuppMinimize
int Abc_SuppMinimize(word *pMatrix, Vec_Wrd_t *p, int nBits, int fVerbose)
Definition: extraUtilSupp.c:237
Vec_WecLevelSize
static int Vec_WecLevelSize(Vec_Wec_t *p, int i)
Definition: vecWec.h:197
Abc_SuppFindOne
word Abc_SuppFindOne(Vec_Wrd_t *p, int nBits)
Definition: extraUtilSupp.c:222
Abc_SuppCountOnes64
static int Abc_SuppCountOnes64(word i)
Definition: extraUtilSupp.c:396
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition: vecWec.h:42
Abc_SuppVerify
void Abc_SuppVerify(Vec_Wrd_t *p, word *pMatrix, int nVars, int nVarsMin)
Definition: extraUtilSupp.c:81
Abc_SuppGenFindBest
int Abc_SuppGenFindBest(Vec_Wrd_t *p, int nBits, int *pMerit)
Definition: extraUtilSupp.c:195
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_SuppGenPairs2
Vec_Wrd_t * Abc_SuppGenPairs2(int nOnes, int nBits)
Definition: extraUtilSupp.c:146
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Vec_WrdPush
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Vec_WecFree
static void Vec_WecFree(Vec_Wec_t *p)
Definition: vecWec.h:345
Vec_WecStart
static Vec_Wec_t * Vec_WecStart(int nSize)
Definition: vecWec.h:98
Vec_WrdCap
static int Vec_WrdCap(Vec_Wrd_t *p)
Definition: vecWrd.h:352
Abc_SuppTest
void Abc_SuppTest(int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose)
Definition: extraUtilSupp.c:267
strtok
char * strtok()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_WrdSize
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
Vec_WrdFreeP
static void Vec_WrdFreeP(Vec_Wrd_t **p)
Definition: vecWrd.h:277
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
Abc_SuppRemove
void Abc_SuppRemove(Vec_Wrd_t *p, int *pCounts, Vec_Wec_t *pS, Vec_Wec_t *pD, int iVar, int nVars)
Definition: extraUtilSupp.c:415
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Abc_SuppPrintProfile
void Abc_SuppPrintProfile(Vec_Wrd_t *p, int nBits)
Definition: extraUtilSupp.c:188
Abc_SuppDiffMatrix
Vec_Wrd_t * Abc_SuppDiffMatrix(Vec_Wrd_t *vCubes)
Definition: extraUtilSupp.c:363
strstr
char * strstr()
Extra_PrintBinary
ABC_NAMESPACE_IMPL_START void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
DECLARATIONS ///.
Definition: extraUtilFile.c:497
Vec_WrdShrink
static void Vec_WrdShrink(Vec_Wrd_t *p, int nSizeNew)
Definition: vecWrd.h:585
Abc_SuppFindVar
int Abc_SuppFindVar(Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
Definition: extraUtilSupp.c:403
Vec_WrdWriteEntry
static void Vec_WrdWriteEntry(Vec_Wrd_t *p, int i, word Entry)
Definition: vecWrd.h:418
Abc_SuppGenPairs
Vec_Wrd_t * Abc_SuppGenPairs(Vec_Wrd_t *p, int nBits)
Definition: extraUtilSupp.c:127
Vec_WrdLimit
static word * Vec_WrdLimit(Vec_Wrd_t *p)
Definition: vecWrd.h:320
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
Abc_SuppReadMinTest
void Abc_SuppReadMinTest(char *pFileName)
Definition: extraUtilSupp.c:504
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_SuppPrintMask
void Abc_SuppPrintMask(word uMask, int nBits)
Definition: extraUtilSupp.c:173
Vec_IntRemove
static int Vec_IntRemove(Vec_Int_t *p, int Entry)
Definition: vecInt.h:915
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
Vec_WecEntry
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Minisat::Var
int Var
Definition: SolverTypes.h:42
strncmp
int strncmp()
Abc_SuppProfile
void Abc_SuppProfile(Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
Definition: extraUtilSupp.c:442
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Abc_SuppReadMin
Vec_Wrd_t * Abc_SuppReadMin(char *pFileName, int *pnVars)
Definition: extraUtilSupp.c:304
Abc_SuppGen
Vec_Wrd_t * Abc_SuppGen(int m, int n)
Definition: extraUtilSupp.c:60
Abc_SuppGenSelectVar
void Abc_SuppGenSelectVar(Vec_Wrd_t *p, int nBits, int iVar)
Definition: extraUtilSupp.c:205
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_WrdDup
static Vec_Wrd_t * Vec_WrdDup(Vec_Wrd_t *pVec)
Definition: vecWrd.h:208
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Extra_FileReadContents
char * Extra_FileReadContents(char *pFileName)
Definition: extraUtilFile.c:388
Abc_SuppSolve
int Abc_SuppSolve(Vec_Wrd_t *p, int nVars)
Definition: extraUtilSupp.c:448
Abc_SuppGenProfile
void Abc_SuppGenProfile(Vec_Wrd_t *p, int nBits, int *pCounts)
Definition: extraUtilSupp.c:180
Vec_WecPush
static void Vec_WecPush(Vec_Wec_t *p, int Level, int Entry)
Definition: vecWec.h:275