abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions | Variables
extraUtilTruth.c File Reference
#include "extra.h"

Go to the source code of this file.

Functions

unsigned ** Extra_TruthElementary (int nVars)
 
void Extra_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
 
void Extra_TruthSwapAdjacentVars2 (unsigned *pIn, unsigned *pOut, int nVars, int Start)
 
void Extra_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
 
void Extra_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
 
int Extra_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
 
int Extra_TruthSupportSize (unsigned *pTruth, int nVars)
 
int Extra_TruthSupport (unsigned *pTruth, int nVars)
 
void Extra_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
 
void Extra_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
 
void Extra_TruthExist (unsigned *pTruth, int nVars, int iVar)
 
void Extra_TruthForall (unsigned *pTruth, int nVars, int iVar)
 
void Extra_TruthMux (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
 
int Extra_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
 
int Extra_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
 
void Extra_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
 
int Extra_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
 
void Extra_TruthCountOnesInCofs (unsigned *pTruth, int nVars, short *pStore)
 
unsigned Extra_TruthHash (unsigned *pIn, int nWords)
 
unsigned Extra_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)
 

Variables

static
ABC_NAMESPACE_IMPL_START
unsigned 		s_VarMasks [5][2]
 

Function Documentation

void Extra_TruthChangePhase ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Changes phase of the function w.r.t. one variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 719 of file extraUtilTruth.c.

720 {
721  int nWords = Extra_TruthWordNum( nVars );
722  int i, k, Step;
723  unsigned Temp;
724 
725  assert( iVar < nVars );
726  switch ( iVar )
727  {
728  case 0:
729  for ( i = 0; i < nWords; i++ )
730  pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
731  return;
732  case 1:
733  for ( i = 0; i < nWords; i++ )
734  pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
735  return;
736  case 2:
737  for ( i = 0; i < nWords; i++ )
738  pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
739  return;
740  case 3:
741  for ( i = 0; i < nWords; i++ )
742  pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
743  return;
744  case 4:
745  for ( i = 0; i < nWords; i++ )
746  pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
747  return;
748  default:
749  Step = (1 << (iVar - 5));
750  for ( k = 0; k < nWords; k += 2*Step )
751  {
752  for ( i = 0; i < Step; i++ )
753  {
754  Temp = pTruth[i];
755  pTruth[i] = pTruth[Step+i];
756  pTruth[Step+i] = Temp;
757  }
758  pTruth += 2*Step;
759  }
760  return;
761  }
762 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
void Extra_TruthCofactor0 ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file extraUtilTruth.c.

451 {
452  int nWords = Extra_TruthWordNum( nVars );
453  int i, k, Step;
454 
455  assert( iVar < nVars );
456  switch ( iVar )
457  {
458  case 0:
459  for ( i = 0; i < nWords; i++ )
460  pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
461  return;
462  case 1:
463  for ( i = 0; i < nWords; i++ )
464  pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
465  return;
466  case 2:
467  for ( i = 0; i < nWords; i++ )
468  pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
469  return;
470  case 3:
471  for ( i = 0; i < nWords; i++ )
472  pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
473  return;
474  case 4:
475  for ( i = 0; i < nWords; i++ )
476  pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
477  return;
478  default:
479  Step = (1 << (iVar - 5));
480  for ( k = 0; k < nWords; k += 2*Step )
481  {
482  for ( i = 0; i < Step; i++ )
483  pTruth[Step+i] = pTruth[i];
484  pTruth += 2*Step;
485  }
486  return;
487  }
488 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
void Extra_TruthCofactor1 ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file extraUtilTruth.c.

400 {
401  int nWords = Extra_TruthWordNum( nVars );
402  int i, k, Step;
403 
404  assert( iVar < nVars );
405  switch ( iVar )
406  {
407  case 0:
408  for ( i = 0; i < nWords; i++ )
409  pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
410  return;
411  case 1:
412  for ( i = 0; i < nWords; i++ )
413  pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
414  return;
415  case 2:
416  for ( i = 0; i < nWords; i++ )
417  pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
418  return;
419  case 3:
420  for ( i = 0; i < nWords; i++ )
421  pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
422  return;
423  case 4:
424  for ( i = 0; i < nWords; i++ )
425  pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
426  return;
427  default:
428  Step = (1 << (iVar - 5));
429  for ( k = 0; k < nWords; k += 2*Step )
430  {
431  for ( i = 0; i < Step; i++ )
432  pTruth[i] = pTruth[Step+i];
433  pTruth += 2*Step;
434  }
435  return;
436  }
437 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
void Extra_TruthCountOnesInCofs ( unsigned *  pTruth,
int  nVars,
short *  pStore 
)

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

Synopsis [Counts the number of 1's in each cofactor.]

Description [The resulting numbers are stored in the array of shorts, whose length is 2*nVars. The number of 1's is counted in a different space than the original function. For example, if the function depends on k variables, the cofactors are assumed to depend on k-1 variables.]

SideEffects []

SeeAlso []

Definition at line 828 of file extraUtilTruth.c.

829 {
830  int nWords = Extra_TruthWordNum( nVars );
831  int i, k, Counter;
832  memset( pStore, 0, sizeof(short) * 2 * nVars );
833  if ( nVars <= 5 )
834  {
835  if ( nVars > 0 )
836  {
837  pStore[2*0+0] = Extra_WordCountOnes( pTruth[0] & 0x55555555 );
838  pStore[2*0+1] = Extra_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
839  }
840  if ( nVars > 1 )
841  {
842  pStore[2*1+0] = Extra_WordCountOnes( pTruth[0] & 0x33333333 );
843  pStore[2*1+1] = Extra_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
844  }
845  if ( nVars > 2 )
846  {
847  pStore[2*2+0] = Extra_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
848  pStore[2*2+1] = Extra_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
849  }
850  if ( nVars > 3 )
851  {
852  pStore[2*3+0] = Extra_WordCountOnes( pTruth[0] & 0x00FF00FF );
853  pStore[2*3+1] = Extra_WordCountOnes( pTruth[0] & 0xFF00FF00 );
854  }
855  if ( nVars > 4 )
856  {
857  pStore[2*4+0] = Extra_WordCountOnes( pTruth[0] & 0x0000FFFF );
858  pStore[2*4+1] = Extra_WordCountOnes( pTruth[0] & 0xFFFF0000 );
859  }
860  return;
861  }
862  // nVars >= 6
863  // count 1's for all other variables
864  for ( k = 0; k < nWords; k++ )
865  {
866  Counter = Extra_WordCountOnes( pTruth[k] );
867  for ( i = 5; i < nVars; i++ )
868  if ( k & (1 << (i-5)) )
869  pStore[2*i+1] += Counter;
870  else
871  pStore[2*i+0] += Counter;
872  }
873  // count 1's for the first five variables
874  for ( k = 0; k < nWords/2; k++ )
875  {
876  pStore[2*0+0] += Extra_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
877  pStore[2*0+1] += Extra_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
878  pStore[2*1+0] += Extra_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
879  pStore[2*1+1] += Extra_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
880  pStore[2*2+0] += Extra_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
881  pStore[2*2+1] += Extra_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
882  pStore[2*3+0] += Extra_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
883  pStore[2*3+1] += Extra_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
884  pStore[2*4+0] += Extra_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
885  pStore[2*4+1] += Extra_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
886  pTruth += 2;
887  }
888 }
memset
char * memset()
nWords
int nWords
Definition: abcNpn.c:127
Counter
static int Counter
Definition: extraBddMisc.c:1877
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
Extra_WordCountOnes
static int Extra_WordCountOnes(unsigned uWord)
Definition: extra.h:255
unsigned** Extra_TruthElementary ( int  nVars)

AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Derive elementary truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file extraUtilTruth.c.

78 {
79  unsigned ** pRes;
80  int i, k, nWords;
81  nWords = Extra_TruthWordNum(nVars);
82  pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 );
83  for ( i = 0; i < nVars; i++ )
84  {
85  if ( i < 5 )
86  {
87  for ( k = 0; k < nWords; k++ )
88  pRes[i][k] = s_VarMasks[i][1];
89  }
90  else
91  {
92  for ( k = 0; k < nWords; k++ )
93  if ( k & (1 << (i-5)) )
94  pRes[i][k] = ~(unsigned)0;
95  else
96  pRes[i][k] = 0;
97  }
98  }
99  return pRes;
100 }
Extra_ArrayAlloc
void ** Extra_ArrayAlloc(int nCols, int nRows, int Size)
Definition: extraUtilMisc.c:880
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
s_VarMasks
static ABC_NAMESPACE_IMPL_START unsigned s_VarMasks[5][2]
Definition: extraUtilTruth.c:42
void Extra_TruthExist ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file extraUtilTruth.c.

503 {
504  int nWords = Extra_TruthWordNum( nVars );
505  int i, k, Step;
506 
507  assert( iVar < nVars );
508  switch ( iVar )
509  {
510  case 0:
511  for ( i = 0; i < nWords; i++ )
512  pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
513  return;
514  case 1:
515  for ( i = 0; i < nWords; i++ )
516  pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
517  return;
518  case 2:
519  for ( i = 0; i < nWords; i++ )
520  pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
521  return;
522  case 3:
523  for ( i = 0; i < nWords; i++ )
524  pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
525  return;
526  case 4:
527  for ( i = 0; i < nWords; i++ )
528  pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
529  return;
530  default:
531  Step = (1 << (iVar - 5));
532  for ( k = 0; k < nWords; k += 2*Step )
533  {
534  for ( i = 0; i < Step; i++ )
535  {
536  pTruth[i] |= pTruth[Step+i];
537  pTruth[Step+i] = pTruth[i];
538  }
539  pTruth += 2*Step;
540  }
541  return;
542  }
543 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
void Extra_TruthForall ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 556 of file extraUtilTruth.c.

557 {
558  int nWords = Extra_TruthWordNum( nVars );
559  int i, k, Step;
560 
561  assert( iVar < nVars );
562  switch ( iVar )
563  {
564  case 0:
565  for ( i = 0; i < nWords; i++ )
566  pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
567  return;
568  case 1:
569  for ( i = 0; i < nWords; i++ )
570  pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
571  return;
572  case 2:
573  for ( i = 0; i < nWords; i++ )
574  pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
575  return;
576  case 3:
577  for ( i = 0; i < nWords; i++ )
578  pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
579  return;
580  case 4:
581  for ( i = 0; i < nWords; i++ )
582  pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
583  return;
584  default:
585  Step = (1 << (iVar - 5));
586  for ( k = 0; k < nWords; k += 2*Step )
587  {
588  for ( i = 0; i < Step; i++ )
589  {
590  pTruth[i] &= pTruth[Step+i];
591  pTruth[Step+i] = pTruth[i];
592  }
593  pTruth += 2*Step;
594  }
595  return;
596  }
597 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
unsigned Extra_TruthHash ( unsigned *  pIn,
int  nWords 
)

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 902 of file extraUtilTruth.c.

903 {
904  // The 1,024 smallest prime numbers used to compute the hash value
905  // http://www.math.utah.edu/~alfeld/math/primelist.html
906  static int HashPrimes[1024] = { 2, 3, 5,
907  7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97,
908  101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191,
909  193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283,
910  293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401,
911  409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509,
912  521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631,
913  641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751,
914  757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877,
915  881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
916  1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091,
917  1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193,
918  1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291,
919  1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423,
920  1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493,
921  1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
922  1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699,
923  1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811,
924  1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931,
925  1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029,
926  2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137,
927  2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267,
928  2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357,
929  2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459,
930  2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593,
931  2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693,
932  2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791,
933  2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903,
934  2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023,
935  3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167,
936  3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271,
937  3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373,
938  3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511,
939  3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607,
940  3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709,
941  3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833,
942  3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931,
943  3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057,
944  4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177,
945  4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283,
946  4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423,
947  4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547,
948  4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657,
949  4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789,
950  4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931,
951  4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011,
952  5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147,
953  5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279,
954  5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413,
955  5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507,
956  5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647,
957  5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743,
958  5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857,
959  5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007,
960  6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121,
961  6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247,
962  6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343,
963  6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473,
964  6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607,
965  6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733,
966  6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857,
967  6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971,
968  6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103,
969  7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229,
970  7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369,
971  7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517,
972  7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603,
973  7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723,
974  7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873,
975  7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009,
976  8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123,
977  8147, 8161 };
978  int i;
979  unsigned uHashKey;
980  assert( nWords <= 1024 );
981  uHashKey = 0;
982  for ( i = 0; i < nWords; i++ )
983  uHashKey ^= HashPrimes[i] * pIn[i];
984  return uHashKey;
985 }
nWords
int nWords
Definition: abcNpn.c:127
assert
#define assert(ex)
Definition: util_old.h:213
int Extra_TruthMinCofSuppOverlap ( unsigned *  pTruth,
int  nVars,
int *  pVarMin 
)

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 775 of file extraUtilTruth.c.

776 {
777  static unsigned uCofactor[16];
778  int i, ValueCur, ValueMin, VarMin;
779  unsigned uSupp0, uSupp1;
780  int nVars0, nVars1;
781  assert( nVars <= 9 );
782  ValueMin = 32;
783  VarMin = -1;
784  for ( i = 0; i < nVars; i++ )
785  {
786  // get negative cofactor
787  Extra_TruthCopy( uCofactor, pTruth, nVars );
788  Extra_TruthCofactor0( uCofactor, nVars, i );
789  uSupp0 = Extra_TruthSupport( uCofactor, nVars );
790  nVars0 = Extra_WordCountOnes( uSupp0 );
791 //Extra_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
792  // get positive cofactor
793  Extra_TruthCopy( uCofactor, pTruth, nVars );
794  Extra_TruthCofactor1( uCofactor, nVars, i );
795  uSupp1 = Extra_TruthSupport( uCofactor, nVars );
796  nVars1 = Extra_WordCountOnes( uSupp1 );
797 //Extra_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
798  // get the number of common vars
799  ValueCur = Extra_WordCountOnes( uSupp0 & uSupp1 );
800  if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
801  {
802  ValueMin = ValueCur;
803  VarMin = i;
804  }
805  if ( ValueMin == 0 )
806  break;
807  }
808  if ( pVarMin )
809  *pVarMin = VarMin;
810  return ValueMin;
811 }
Extra_TruthCofactor1
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:399
Extra_TruthSupport
int Extra_TruthSupport(unsigned *pTruth, int nVars)
Definition: extraUtilTruth.c:377
Extra_TruthCofactor0
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:450
Extra_WordCountOnes
static int Extra_WordCountOnes(unsigned uWord)
Definition: extra.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
void Extra_TruthMux ( unsigned *  pOut,
unsigned *  pCof0,
unsigned *  pCof1,
int  nVars,
int  iVar 
)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file extraUtilTruth.c.

612 {
613  int nWords = Extra_TruthWordNum( nVars );
614  int i, k, Step;
615 
616  assert( iVar < nVars );
617  switch ( iVar )
618  {
619  case 0:
620  for ( i = 0; i < nWords; i++ )
621  pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
622  return;
623  case 1:
624  for ( i = 0; i < nWords; i++ )
625  pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
626  return;
627  case 2:
628  for ( i = 0; i < nWords; i++ )
629  pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
630  return;
631  case 3:
632  for ( i = 0; i < nWords; i++ )
633  pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
634  return;
635  case 4:
636  for ( i = 0; i < nWords; i++ )
637  pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
638  return;
639  default:
640  Step = (1 << (iVar - 5));
641  for ( k = 0; k < nWords; k += 2*Step )
642  {
643  for ( i = 0; i < Step; i++ )
644  {
645  pOut[i] = pCof0[i];
646  pOut[Step+i] = pCof1[Step+i];
647  }
648  pOut += 2*Step;
649  }
650  return;
651  }
652 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
unsigned Extra_TruthSemiCanonicize ( unsigned *  pInOut,
unsigned *  pAux,
int  nVars,
char *  pCanonPerm,
short *  pStore 
)

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 999 of file extraUtilTruth.c.

1000 {
1001  unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
1002  int nWords = Extra_TruthWordNum( nVars );
1003  int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
1004  unsigned uCanonPhase;
1005 
1006  // canonicize output
1007  uCanonPhase = 0;
1008  nOnes = Extra_TruthCountOnes(pIn, nVars);
1009  if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
1010  {
1011  uCanonPhase |= (1 << nVars);
1012  Extra_TruthNot( pIn, pIn, nVars );
1013  }
1014 
1015  // collect the minterm counts
1016  Extra_TruthCountOnesInCofs( pIn, nVars, pStore );
1017 
1018  // canonicize phase
1019  for ( i = 0; i < nVars; i++ )
1020  {
1021  if ( pStore[2*i+0] <= pStore[2*i+1] )
1022  continue;
1023  uCanonPhase |= (1 << i);
1024  Temp = pStore[2*i+0];
1025  pStore[2*i+0] = pStore[2*i+1];
1026  pStore[2*i+1] = Temp;
1027  Extra_TruthChangePhase( pIn, nVars, i );
1028  }
1029 
1030 // Extra_PrintHexadecimal( stdout, pIn, nVars );
1031 // printf( "\n" );
1032 
1033  // permute
1034  Counter = 0;
1035  do {
1036  fChange = 0;
1037  for ( i = 0; i < nVars-1; i++ )
1038  {
1039  if ( pStore[2*i] <= pStore[2*(i+1)] )
1040  continue;
1041  Counter++;
1042  fChange = 1;
1043 
1044  Temp = pCanonPerm[i];
1045  pCanonPerm[i] = pCanonPerm[i+1];
1046  pCanonPerm[i+1] = Temp;
1047 
1048  Temp = pStore[2*i];
1049  pStore[2*i] = pStore[2*(i+1)];
1050  pStore[2*(i+1)] = Temp;
1051 
1052  Temp = pStore[2*i+1];
1053  pStore[2*i+1] = pStore[2*(i+1)+1];
1054  pStore[2*(i+1)+1] = Temp;
1055 
1056  Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
1057  pTemp = pIn; pIn = pOut; pOut = pTemp;
1058  }
1059  } while ( fChange );
1060 
1061 /*
1062  Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
1063  for ( i = 0; i < nVars; i++ )
1064  printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
1065  printf( " C = %d\n", Counter );
1066  Extra_PrintHexadecimal( stdout, pIn, nVars );
1067  printf( "\n" );
1068 */
1069 
1070 /*
1071  // process symmetric variable groups
1072  uSymms = 0;
1073  for ( i = 0; i < nVars-1; i++ )
1074  {
1075  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1076  continue;
1077  if ( pStore[2*i] != pStore[2*i+1] )
1078  continue;
1079  if ( Extra_TruthVarsSymm( pIn, nVars, i, i+1 ) )
1080  continue;
1081  if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
1082  Extra_TruthChangePhase( pIn, nVars, i+1 );
1083  }
1084 */
1085 
1086 /*
1087  // process symmetric variable groups
1088  uSymms = 0;
1089  for ( i = 0; i < nVars-1; i++ )
1090  {
1091  if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1092  continue;
1093  // i and i+1 can be symmetric
1094  // find the end of this group
1095  for ( k = i+1; k < nVars; k++ )
1096  if ( pStore[2*i] != pStore[2*k] )
1097  break;
1098  Limit = k;
1099  assert( i < Limit-1 );
1100  // go through the variables in this group
1101  for ( j = i + 1; j < Limit; j++ )
1102  {
1103  // check symmetry
1104  if ( Extra_TruthVarsSymm( pIn, nVars, i, j ) )
1105  {
1106  uSymms |= (1 << j);
1107  continue;
1108  }
1109  // they are phase-unknown
1110  if ( pStore[2*i] == pStore[2*i+1] )
1111  {
1112  if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, j ) )
1113  {
1114  Extra_TruthChangePhase( pIn, nVars, j );
1115  uCanonPhase ^= (1 << j);
1116  uSymms |= (1 << j);
1117  continue;
1118  }
1119  }
1120 
1121  // they are not symmetric - move j as far as it goes in the group
1122  for ( k = j; k < Limit-1; k++ )
1123  {
1124  Counter++;
1125 
1126  Temp = pCanonPerm[k];
1127  pCanonPerm[k] = pCanonPerm[k+1];
1128  pCanonPerm[k+1] = Temp;
1129 
1130  assert( pStore[2*k] == pStore[2*(k+1)] );
1131  Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
1132  pTemp = pIn; pIn = pOut; pOut = pTemp;
1133  }
1134  Limit--;
1135  j--;
1136  }
1137  i = Limit - 1;
1138  }
1139 */
1140 
1141  // swap if it was moved an even number of times
1142  if ( Counter & 1 )
1143  Extra_TruthCopy( pOut, pIn, nVars );
1144  return uCanonPhase;
1145 }
Extra_TruthSwapAdjacentVars
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: extraUtilTruth.c:114
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthCountOnes
static int Extra_TruthCountOnes(unsigned *pIn, int nVars)
Definition: extra.h:263
Counter
static int Counter
Definition: extraBddMisc.c:1877
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
Extra_TruthCountOnesInCofs
void Extra_TruthCountOnesInCofs(unsigned *pTruth, int nVars, short *pStore)
Definition: extraUtilTruth.c:828
Extra_TruthNot
static void Extra_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:320
Extra_TruthChangePhase
void Extra_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:719
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
void Extra_TruthShrink ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  nVarsAll,
unsigned  Phase 
)

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

Synopsis [Shrinks the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows what variables should remain.]

SideEffects []

SeeAlso []

Definition at line 268 of file extraUtilTruth.c.

269 {
270  unsigned * pTemp;
271  int i, k, Var = 0, Counter = 0;
272  for ( i = 0; i < nVarsAll; i++ )
273  if ( Phase & (1 << i) )
274  {
275  for ( k = i-1; k >= Var; k-- )
276  {
277  Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
278  pTemp = pIn; pIn = pOut; pOut = pTemp;
279  Counter++;
280  }
281  Var++;
282  }
283  assert( Var == nVars );
284  // swap if it was moved an even number of times
285  if ( !(Counter & 1) )
286  Extra_TruthCopy( pOut, pIn, nVarsAll );
287 }
Extra_TruthSwapAdjacentVars
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: extraUtilTruth.c:114
Counter
static int Counter
Definition: extraBddMisc.c:1877
Minisat::Var
int Var
Definition: SolverTypes.h:42
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
void Extra_TruthStretch ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  nVarsAll,
unsigned  Phase 
)

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

Synopsis [Expands the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows where the variables should go.]

SideEffects []

SeeAlso []

Definition at line 234 of file extraUtilTruth.c.

235 {
236  unsigned * pTemp;
237  int i, k, Var = nVars - 1, Counter = 0;
238  for ( i = nVarsAll - 1; i >= 0; i-- )
239  if ( Phase & (1 << i) )
240  {
241  for ( k = Var; k < i; k++ )
242  {
243  Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
244  pTemp = pIn; pIn = pOut; pOut = pTemp;
245  Counter++;
246  }
247  Var--;
248  }
249  assert( Var == -1 );
250  // swap if it was moved an even number of times
251  if ( !(Counter & 1) )
252  Extra_TruthCopy( pOut, pIn, nVarsAll );
253 }
Extra_TruthSwapAdjacentVars
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: extraUtilTruth.c:114
Counter
static int Counter
Definition: extraBddMisc.c:1877
Minisat::Var
int Var
Definition: SolverTypes.h:42
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
int Extra_TruthSupport ( unsigned *  pTruth,
int  nVars 
)

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 377 of file extraUtilTruth.c.

378 {
379  int i, Support = 0;
380  for ( i = 0; i < nVars; i++ )
381  if ( Extra_TruthVarInSupport( pTruth, nVars, i ) )
382  Support |= (1 << i);
383  return Support;
384 }
Extra_TruthVarInSupport
int Extra_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:301
int Extra_TruthSupportSize ( unsigned *  pTruth,
int  nVars 
)

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file extraUtilTruth.c.

359 {
360  int i, Counter = 0;
361  for ( i = 0; i < nVars; i++ )
362  Counter += Extra_TruthVarInSupport( pTruth, nVars, i );
363  return Counter;
364 }
Counter
static int Counter
Definition: extraBddMisc.c:1877
Extra_TruthVarInSupport
int Extra_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:301
void Extra_TruthSwapAdjacentVars ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  iVar 
)

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

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 114 of file extraUtilTruth.c.

115 {
116  static unsigned PMasks[4][3] = {
117  { 0x99999999, 0x22222222, 0x44444444 },
118  { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
119  { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
120  { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
121  };
122  int nWords = Extra_TruthWordNum( nVars );
123  int i, k, Step, Shift;
124 
125  assert( iVar < nVars - 1 );
126  if ( iVar < 4 )
127  {
128  Shift = (1 << iVar);
129  for ( i = 0; i < nWords; i++ )
130  pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
131  }
132  else if ( iVar > 4 )
133  {
134  Step = (1 << (iVar - 5));
135  for ( k = 0; k < nWords; k += 4*Step )
136  {
137  for ( i = 0; i < Step; i++ )
138  pOut[i] = pIn[i];
139  for ( i = 0; i < Step; i++ )
140  pOut[Step+i] = pIn[2*Step+i];
141  for ( i = 0; i < Step; i++ )
142  pOut[2*Step+i] = pIn[Step+i];
143  for ( i = 0; i < Step; i++ )
144  pOut[3*Step+i] = pIn[3*Step+i];
145  pIn += 4*Step;
146  pOut += 4*Step;
147  }
148  }
149  else // if ( iVar == 4 )
150  {
151  for ( i = 0; i < nWords; i += 2 )
152  {
153  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
154  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
155  }
156  }
157 }
nWords
int nWords
Definition: abcNpn.c:127
PMasks
static word PMasks[5][3]
Definition: ifDec07.c:44
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
void Extra_TruthSwapAdjacentVars2 ( unsigned *  pIn,
unsigned *  pOut,
int  nVars,
int  Start 
)

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

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 171 of file extraUtilTruth.c.

172 {
173  int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
174  int i, k, Step;
175 
176  assert( Start < nVars - 1 );
177  switch ( Start )
178  {
179  case 0:
180  for ( i = 0; i < nWords; i++ )
181  pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
182  return;
183  case 1:
184  for ( i = 0; i < nWords; i++ )
185  pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
186  return;
187  case 2:
188  for ( i = 0; i < nWords; i++ )
189  pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
190  return;
191  case 3:
192  for ( i = 0; i < nWords; i++ )
193  pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
194  return;
195  case 4:
196  for ( i = 0; i < nWords; i += 2 )
197  {
198  pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
199  pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
200  }
201  return;
202  default:
203  Step = (1 << (Start - 5));
204  for ( k = 0; k < nWords; k += 4*Step )
205  {
206  for ( i = 0; i < Step; i++ )
207  pOut[i] = pIn[i];
208  for ( i = 0; i < Step; i++ )
209  pOut[Step+i] = pIn[2*Step+i];
210  for ( i = 0; i < Step; i++ )
211  pOut[2*Step+i] = pIn[Step+i];
212  for ( i = 0; i < Step; i++ )
213  pOut[3*Step+i] = pIn[3*Step+i];
214  pIn += 4*Step;
215  pOut += 4*Step;
216  }
217  return;
218  }
219 }
nWords
int nWords
Definition: abcNpn.c:127
assert
#define assert(ex)
Definition: util_old.h:213
int Extra_TruthVarInSupport ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Returns 1 if TT depends on the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file extraUtilTruth.c.

302 {
303  int nWords = Extra_TruthWordNum( nVars );
304  int i, k, Step;
305 
306  assert( iVar < nVars );
307  switch ( iVar )
308  {
309  case 0:
310  for ( i = 0; i < nWords; i++ )
311  if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
312  return 1;
313  return 0;
314  case 1:
315  for ( i = 0; i < nWords; i++ )
316  if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
317  return 1;
318  return 0;
319  case 2:
320  for ( i = 0; i < nWords; i++ )
321  if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
322  return 1;
323  return 0;
324  case 3:
325  for ( i = 0; i < nWords; i++ )
326  if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
327  return 1;
328  return 0;
329  case 4:
330  for ( i = 0; i < nWords; i++ )
331  if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
332  return 1;
333  return 0;
334  default:
335  Step = (1 << (iVar - 5));
336  for ( k = 0; k < nWords; k += 2*Step )
337  {
338  for ( i = 0; i < Step; i++ )
339  if ( pTruth[i] != pTruth[Step+i] )
340  return 1;
341  pTruth += 2*Step;
342  }
343  return 0;
344  }
345 }
nWords
int nWords
Definition: abcNpn.c:127
Extra_TruthWordNum
static int Extra_TruthWordNum(int nVars)
Definition: extra.h:249
assert
#define assert(ex)
Definition: util_old.h:213
int Extra_TruthVarsAntiSymm ( unsigned *  pTruth,
int  nVars,
int  iVar0,
int  iVar1 
)

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

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 692 of file extraUtilTruth.c.

693 {
694  static unsigned uTemp0[16], uTemp1[16];
695  assert( nVars <= 9 );
696  // compute Cof00
697  Extra_TruthCopy( uTemp0, pTruth, nVars );
698  Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
699  Extra_TruthCofactor0( uTemp0, nVars, iVar1 );
700  // compute Cof11
701  Extra_TruthCopy( uTemp1, pTruth, nVars );
702  Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
703  Extra_TruthCofactor1( uTemp1, nVars, iVar1 );
704  // compare
705  return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
706 }
Extra_TruthCofactor1
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:399
Extra_TruthIsEqual
static int Extra_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: extra.h:270
Extra_TruthCofactor0
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:450
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302
int Extra_TruthVarsSymm ( unsigned *  pTruth,
int  nVars,
int  iVar0,
int  iVar1 
)

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

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file extraUtilTruth.c.

666 {
667  static unsigned uTemp0[16], uTemp1[16];
668  assert( nVars <= 9 );
669  // compute Cof01
670  Extra_TruthCopy( uTemp0, pTruth, nVars );
671  Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
672  Extra_TruthCofactor1( uTemp0, nVars, iVar1 );
673  // compute Cof10
674  Extra_TruthCopy( uTemp1, pTruth, nVars );
675  Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
676  Extra_TruthCofactor0( uTemp1, nVars, iVar1 );
677  // compare
678  return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
679 }
Extra_TruthCofactor1
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:399
Extra_TruthIsEqual
static int Extra_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: extra.h:270
Extra_TruthCofactor0
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: extraUtilTruth.c:450
assert
#define assert(ex)
Definition: util_old.h:213
Extra_TruthCopy
static void Extra_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: extra.h:302

Variable Documentation

ABC_NAMESPACE_IMPL_START unsigned s_VarMasks[5][2]
static
Initial value:
= {
{ 0x33333333, 0xAAAAAAAA },
{ 0x55555555, 0xCCCCCCCC },
{ 0x0F0F0F0F, 0xF0F0F0F0 },
{ 0x00FF00FF, 0xFF00FF00 },
{ 0x0000FFFF, 0xFFFF0000 }
}

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

FileName [extraUtilMisc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [Various procedures for truth table manipulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

]

Definition at line 42 of file extraUtilTruth.c.