ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
kitTruth.c File Reference
#include "kit.h"
Include dependency graph for kitTruth.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Kit_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
 DECLARATIONS ///.
 
void Kit_TruthSwapAdjacentVars2 (unsigned *pIn, unsigned *pOut, int nVars, int Start)
 
void Kit_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
 
void Kit_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
 
void Kit_TruthPermute (unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
 
int Kit_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
 
int Kit_TruthSupportSize (unsigned *pTruth, int nVars)
 
unsigned Kit_TruthSupport (unsigned *pTruth, int nVars)
 
void Kit_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
 
int Kit_TruthCofactor0Count (unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthCofactor0New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
 
void Kit_TruthCofactor1New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
 
int Kit_TruthVarIsVacuous (unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
 
void Kit_TruthExist (unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthExistNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthExistSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
 
void Kit_TruthForall (unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthForallNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
 
void Kit_TruthUniqueNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
 
int Kit_TruthBooleanDiffCount (unsigned *pTruth, int nVars, int iVar)
 
int Kit_TruthXorCount (unsigned *pTruth0, unsigned *pTruth1, int nVars)
 
void Kit_TruthForallSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
 
void Kit_TruthMuxVar (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
 
void Kit_TruthMuxVarPhase (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
 
int Kit_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
 
int Kit_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
 
void Kit_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
 
int Kit_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
 
int Kit_TruthBestCofVar (unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
 
void Kit_TruthCountOnesInCofs (unsigned *pTruth, int nVars, int *pStore)
 
void Kit_TruthCountOnesInCofs0 (unsigned *pTruth, int nVars, int *pStore)
 
void Kit_TruthCountOnesInCofsSlow (unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
 
unsigned Kit_TruthHash (unsigned *pIn, int nWords)
 
unsigned Kit_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
 
int Kit_TruthCountMinterms (unsigned *pTruth, int nVars, int *pRes, int *pBytesInit)
 
void Kit_PrintHexadecimal (FILE *pFile, unsigned Sign[], int nVars)
 
void Kit_TruthCountMintermsPrecomp ()
 
char * Kit_TruthDumpToFile (unsigned *pTruth, int nVars, int nFile)
 
void Kit_TruthPrintProfile_int (unsigned *pTruth, int nVars)
 
void Kit_TruthPrintProfile (unsigned *pTruth, int nVars)
 

Function Documentation

◆ Kit_PrintHexadecimal()

void Kit_PrintHexadecimal ( FILE * pFile,
unsigned Sign[],
int nVars )

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

Synopsis [Prints the hex unsigned into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1939 of file kitTruth.c.

1940{
1941 int nDigits, Digit, k;
1942 // write the number into the file
1943 nDigits = (1 << nVars) / 4;
1944 for ( k = nDigits - 1; k >= 0; k-- )
1945 {
1946 Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
1947 if ( Digit < 10 )
1948 fprintf( pFile, "%d", Digit );
1949 else
1950 fprintf( pFile, "%c", 'a' + Digit-10 );
1951 }
1952// fprintf( pFile, "\n" );
1953}
Here is the caller graph for this function:

◆ Kit_TruthBestCofVar()

int Kit_TruthBestCofVar ( unsigned * pTruth,
int nVars,
unsigned * pCof0,
unsigned * pCof1 )

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1365 of file kitTruth.c.

1366{
1367 int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
1368 if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
1369 return -1;
1370 // iterate through variables
1371 iBestVar = -1;
1372 nSuppSizeMin = KIT_INFINITY;
1373 for ( i = 0; i < nVars; i++ )
1374 {
1375 // cofactor the functiona and get support sizes
1376 Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
1377 Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
1378 nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
1379 nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
1380 nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
1381 // compare this variable with other variables
1382 if ( nSuppSizeMin > nSuppSizeCur )
1383 {
1384 nSuppSizeMin = nSuppSizeCur;
1385 iBestVar = i;
1386 }
1387 }
1388 assert( iBestVar != -1 );
1389 // cofactor w.r.t. this variable
1390 Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
1391 Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
1392 return iBestVar;
1393}
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
KIT_INFINITY
#define KIT_INFINITY
Definition kit.h:176
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthBooleanDiffCount()

int Kit_TruthBooleanDiffCount ( unsigned * pTruth,
int nVars,
int iVar )

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

Synopsis [Returns the number of minterms in the Boolean difference.]

Description []

SideEffects []

SeeAlso []

Definition at line 977 of file kitTruth.c.

978{
979 int nWords = Kit_TruthWordNum( nVars );
980 int i, k, Step, Counter = 0;
981
982 assert( iVar < nVars );
983 switch ( iVar )
984 {
985 case 0:
986 for ( i = 0; i < nWords; i++ )
987 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 1)) & 0x55555555 );
988 return Counter;
989 case 1:
990 for ( i = 0; i < nWords; i++ )
991 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 2)) & 0x33333333 );
992 return Counter;
993 case 2:
994 for ( i = 0; i < nWords; i++ )
995 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 4)) & 0x0F0F0F0F );
996 return Counter;
997 case 3:
998 for ( i = 0; i < nWords; i++ )
999 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 8)) & 0x00FF00FF );
1000 return Counter;
1001 case 4:
1002 for ( i = 0; i < nWords; i++ )
1003 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >>16)) & 0x0000FFFF );
1004 return Counter;
1005 default:
1006 Step = (1 << (iVar - 5));
1007 for ( k = 0; k < nWords; k += 2*Step )
1008 {
1009 for ( i = 0; i < Step; i++ )
1010 Counter += Kit_WordCountOnes( pTruth[i] ^ pTruth[Step+i] );
1011 pTruth += 2*Step;
1012 }
1013 return Counter;
1014 }
1015}
nWords
int nWords
Definition abcNpn.c:127
Here is the caller graph for this function:

◆ Kit_TruthChangePhase()

void Kit_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 1259 of file kitTruth.c.

1260{
1261 int nWords = Kit_TruthWordNum( nVars );
1262 int i, k, Step;
1263 unsigned Temp;
1264
1265 assert( iVar < nVars );
1266 switch ( iVar )
1267 {
1268 case 0:
1269 for ( i = 0; i < nWords; i++ )
1270 pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
1271 return;
1272 case 1:
1273 for ( i = 0; i < nWords; i++ )
1274 pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
1275 return;
1276 case 2:
1277 for ( i = 0; i < nWords; i++ )
1278 pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
1279 return;
1280 case 3:
1281 for ( i = 0; i < nWords; i++ )
1282 pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
1283 return;
1284 case 4:
1285 for ( i = 0; i < nWords; i++ )
1286 pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
1287 return;
1288 default:
1289 Step = (1 << (iVar - 5));
1290 for ( k = 0; k < nWords; k += 2*Step )
1291 {
1292 for ( i = 0; i < Step; i++ )
1293 {
1294 Temp = pTruth[i];
1295 pTruth[i] = pTruth[Step+i];
1296 pTruth[Step+i] = Temp;
1297 }
1298 pTruth += 2*Step;
1299 }
1300 return;
1301 }
1302}
Here is the caller graph for this function:

◆ Kit_TruthCofactor0()

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

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file kitTruth.c.

369{
370 int nWords = Kit_TruthWordNum( nVars );
371 int i, k, Step;
372
373 assert( iVar < nVars );
374 switch ( iVar )
375 {
376 case 0:
377 for ( i = 0; i < nWords; i++ )
378 pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
379 return;
380 case 1:
381 for ( i = 0; i < nWords; i++ )
382 pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
383 return;
384 case 2:
385 for ( i = 0; i < nWords; i++ )
386 pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
387 return;
388 case 3:
389 for ( i = 0; i < nWords; i++ )
390 pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
391 return;
392 case 4:
393 for ( i = 0; i < nWords; i++ )
394 pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
395 return;
396 default:
397 Step = (1 << (iVar - 5));
398 for ( k = 0; k < nWords; k += 2*Step )
399 {
400 for ( i = 0; i < Step; i++ )
401 pTruth[Step+i] = pTruth[i];
402 pTruth += 2*Step;
403 }
404 return;
405 }
406}
Here is the caller graph for this function:

◆ Kit_TruthCofactor0Count()

int Kit_TruthCofactor0Count ( unsigned * pTruth,
int nVars,
int iVar )

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 419 of file kitTruth.c.

420{
421 int nWords = Kit_TruthWordNum( nVars );
422 int i, k, Step, Counter = 0;
423
424 assert( iVar < nVars );
425 switch ( iVar )
426 {
427 case 0:
428 for ( i = 0; i < nWords; i++ )
429 Counter += Kit_WordCountOnes(pTruth[i] & 0x55555555);
430 return Counter;
431 case 1:
432 for ( i = 0; i < nWords; i++ )
433 Counter += Kit_WordCountOnes(pTruth[i] & 0x33333333);
434 return Counter;
435 case 2:
436 for ( i = 0; i < nWords; i++ )
437 Counter += Kit_WordCountOnes(pTruth[i] & 0x0F0F0F0F);
438 return Counter;
439 case 3:
440 for ( i = 0; i < nWords; i++ )
441 Counter += Kit_WordCountOnes(pTruth[i] & 0x00FF00FF);
442 return Counter;
443 case 4:
444 for ( i = 0; i < nWords; i++ )
445 Counter += Kit_WordCountOnes(pTruth[i] & 0x0000FFFF);
446 return Counter;
447 default:
448 Step = (1 << (iVar - 5));
449 for ( k = 0; k < nWords; k += 2*Step )
450 {
451 for ( i = 0; i < Step; i++ )
452 Counter += Kit_WordCountOnes(pTruth[i]);
453 pTruth += 2*Step;
454 }
455 return Counter;
456 }
457}
Here is the caller graph for this function:

◆ Kit_TruthCofactor0New()

void Kit_TruthCofactor0New ( unsigned * pOut,
unsigned * pIn,
int nVars,
int iVar )

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 521 of file kitTruth.c.

522{
523 int nWords = Kit_TruthWordNum( nVars );
524 int i, k, Step;
525
526 assert( iVar < nVars );
527 switch ( iVar )
528 {
529 case 0:
530 for ( i = 0; i < nWords; i++ )
531 pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
532 return;
533 case 1:
534 for ( i = 0; i < nWords; i++ )
535 pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
536 return;
537 case 2:
538 for ( i = 0; i < nWords; i++ )
539 pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
540 return;
541 case 3:
542 for ( i = 0; i < nWords; i++ )
543 pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
544 return;
545 case 4:
546 for ( i = 0; i < nWords; i++ )
547 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
548 return;
549 default:
550 Step = (1 << (iVar - 5));
551 for ( k = 0; k < nWords; k += 2*Step )
552 {
553 for ( i = 0; i < Step; i++ )
554 pOut[i] = pOut[Step+i] = pIn[i];
555 pIn += 2*Step;
556 pOut += 2*Step;
557 }
558 return;
559 }
560}
Here is the caller graph for this function:

◆ Kit_TruthCofactor1()

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

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file kitTruth.c.

471{
472 int nWords = Kit_TruthWordNum( nVars );
473 int i, k, Step;
474
475 assert( iVar < nVars );
476 switch ( iVar )
477 {
478 case 0:
479 for ( i = 0; i < nWords; i++ )
480 pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
481 return;
482 case 1:
483 for ( i = 0; i < nWords; i++ )
484 pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
485 return;
486 case 2:
487 for ( i = 0; i < nWords; i++ )
488 pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
489 return;
490 case 3:
491 for ( i = 0; i < nWords; i++ )
492 pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
493 return;
494 case 4:
495 for ( i = 0; i < nWords; i++ )
496 pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
497 return;
498 default:
499 Step = (1 << (iVar - 5));
500 for ( k = 0; k < nWords; k += 2*Step )
501 {
502 for ( i = 0; i < Step; i++ )
503 pTruth[i] = pTruth[Step+i];
504 pTruth += 2*Step;
505 }
506 return;
507 }
508}
Here is the caller graph for this function:

◆ Kit_TruthCofactor1New()

void Kit_TruthCofactor1New ( unsigned * pOut,
unsigned * pIn,
int nVars,
int iVar )

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 573 of file kitTruth.c.

574{
575 int nWords = Kit_TruthWordNum( nVars );
576 int i, k, Step;
577
578 assert( iVar < nVars );
579 switch ( iVar )
580 {
581 case 0:
582 for ( i = 0; i < nWords; i++ )
583 pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
584 return;
585 case 1:
586 for ( i = 0; i < nWords; i++ )
587 pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
588 return;
589 case 2:
590 for ( i = 0; i < nWords; i++ )
591 pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
592 return;
593 case 3:
594 for ( i = 0; i < nWords; i++ )
595 pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
596 return;
597 case 4:
598 for ( i = 0; i < nWords; i++ )
599 pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
600 return;
601 default:
602 Step = (1 << (iVar - 5));
603 for ( k = 0; k < nWords; k += 2*Step )
604 {
605 for ( i = 0; i < Step; i++ )
606 pOut[i] = pOut[Step+i] = pIn[Step+i];
607 pIn += 2*Step;
608 pOut += 2*Step;
609 }
610 return;
611 }
612}
Here is the caller graph for this function:

◆ Kit_TruthCountMinterms()

int Kit_TruthCountMinterms ( unsigned * pTruth,
int nVars,
int * pRes,
int * pBytesInit )

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

Synopsis [Fast counting minterms in the cofactors of a function.]

Description [Returns the total number of minterms in the function. The resulting array (pRes) contains the number of minterms in 0-cofactor w.r.t. each variables. The additional array (pBytes) is used for internal storage. It should have the size equal to the number of truth table bytes.]

SideEffects []

SeeAlso []

Definition at line 1839 of file kitTruth.c.

1840{
1841 // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
1842 static unsigned Table[256] = {
1843 0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
1844 0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
1845 0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
1846 0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
1847 0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
1848 0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
1849 0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
1850 0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
1851 0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
1852 0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
1853 0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
1854 0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
1855 0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1856 0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1857 0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
1858 0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
1859 0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
1860 0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
1861 0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1862 0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1863 0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
1864 0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
1865 0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
1866 0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
1867 0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
1868 0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
1869 0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
1870 0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
1871 0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
1872 0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
1873 0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
1874 0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
1875 };
1876 unsigned uSum;
1877 unsigned char * pTruthC, * pLimit;
1878 int * pBytes = pBytesInit;
1879 int i, iVar, Step, nWords, nBytes, nTotal;
1880
1881 assert( nVars <= 20 );
1882
1883 // clear storage
1884 memset( pRes, 0, sizeof(int) * nVars );
1885
1886 // count the number of one's in 0-cofactors of the first three variables
1887 nTotal = uSum = 0;
1888 nWords = Kit_TruthWordNum( nVars );
1889 nBytes = nWords * 4;
1890 pTruthC = (unsigned char *)pTruth;
1891 pLimit = pTruthC + nBytes;
1892 for ( ; pTruthC < pLimit; pTruthC++ )
1893 {
1894 uSum += Table[*pTruthC];
1895 *pBytes++ = (Table[*pTruthC] & 0xff);
1896 if ( (uSum & 0xff) > 246 )
1897 {
1898 nTotal += (uSum & 0xff);
1899 pRes[0] += ((uSum >> 8) & 0xff);
1900 pRes[2] += ((uSum >> 16) & 0xff);
1901 pRes[3] += ((uSum >> 24) & 0xff);
1902 uSum = 0;
1903 }
1904 }
1905 if ( uSum )
1906 {
1907 nTotal += (uSum & 0xff);
1908 pRes[0] += ((uSum >> 8) & 0xff);
1909 pRes[1] += ((uSum >> 16) & 0xff);
1910 pRes[2] += ((uSum >> 24) & 0xff);
1911 }
1912
1913 // count all other variables
1914 for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
1915 for ( i = 0; i < nBytes; i += Step + Step )
1916 {
1917 pRes[iVar] += pBytesInit[i];
1918 pBytesInit[i] += pBytesInit[i+Step];
1919 }
1920 assert( pBytesInit[0] == nTotal );
1921 assert( iVar == nVars );
1922
1923 for ( i = 0; i < nVars; i++ )
1924 assert( pRes[i] == Kit_TruthCofactor0Count(pTruth, nVars, i) );
1925 return nTotal;
1926}
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Kit_TruthCofactor0Count
int Kit_TruthCofactor0Count(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:419
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthCountMintermsPrecomp()

void Kit_TruthCountMintermsPrecomp ( )

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

Synopsis [Fast counting minterms for the functions.]

Description [Returns 0 if the function is a constant.]

SideEffects []

SeeAlso []

Definition at line 1966 of file kitTruth.c.

1967{
1968 int bit_count[256] = {
1969 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
1970 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1971 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1972 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1973 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1974 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1975 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1976 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
1977 };
1978 unsigned i, uWord;
1979 for ( i = 0; i < 256; i++ )
1980 {
1981 if ( i % 8 == 0 )
1982 printf( "\n" );
1983 uWord = bit_count[i];
1984 uWord |= (bit_count[i & 0x55] << 8);
1985 uWord |= (bit_count[i & 0x33] << 16);
1986 uWord |= (bit_count[i & 0x0f] << 24);
1987 printf( "0x" );
1988 Kit_PrintHexadecimal( stdout, &uWord, 5 );
1989 printf( ", " );
1990 }
1991}
Kit_PrintHexadecimal
void Kit_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition kitTruth.c:1939
Here is the call graph for this function:

◆ Kit_TruthCountOnesInCofs()

void Kit_TruthCountOnesInCofs ( unsigned * pTruth,
int nVars,
int * pStore )

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

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

Description [The resulting numbers are stored in the array of ints, 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 1410 of file kitTruth.c.

1411{
1412 int nWords = Kit_TruthWordNum( nVars );
1413 int i, k, Counter;
1414 memset( pStore, 0, sizeof(int) * 2 * nVars );
1415 if ( nVars <= 5 )
1416 {
1417 if ( nVars > 0 )
1418 {
1419 pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1420 pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
1421 }
1422 if ( nVars > 1 )
1423 {
1424 pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1425 pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
1426 }
1427 if ( nVars > 2 )
1428 {
1429 pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1430 pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
1431 }
1432 if ( nVars > 3 )
1433 {
1434 pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1435 pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
1436 }
1437 if ( nVars > 4 )
1438 {
1439 pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1440 pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
1441 }
1442 return;
1443 }
1444 // nVars >= 6
1445 // count 1's for all other variables
1446 for ( k = 0; k < nWords; k++ )
1447 {
1448 Counter = Kit_WordCountOnes( pTruth[k] );
1449 for ( i = 5; i < nVars; i++ )
1450 if ( k & (1 << (i-5)) )
1451 pStore[2*i+1] += Counter;
1452 else
1453 pStore[2*i+0] += Counter;
1454 }
1455 // count 1's for the first five variables
1456 for ( k = 0; k < nWords/2; k++ )
1457 {
1458 pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1459 pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
1460 pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1461 pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
1462 pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1463 pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
1464 pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1465 pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
1466 pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1467 pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
1468 pTruth += 2;
1469 }
1470}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthCountOnesInCofs0()

void Kit_TruthCountOnesInCofs0 ( unsigned * pTruth,
int nVars,
int * pStore )

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

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

Description [The resulting numbers are stored in the array of ints, whose length is 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 1486 of file kitTruth.c.

1487{
1488 int nWords = Kit_TruthWordNum( nVars );
1489 int i, k, Counter;
1490 memset( pStore, 0, sizeof(int) * nVars );
1491 if ( nVars <= 5 )
1492 {
1493 if ( nVars > 0 )
1494 pStore[0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1495 if ( nVars > 1 )
1496 pStore[1] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1497 if ( nVars > 2 )
1498 pStore[2] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1499 if ( nVars > 3 )
1500 pStore[3] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1501 if ( nVars > 4 )
1502 pStore[4] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1503 return;
1504 }
1505 // nVars >= 6
1506 // count 1's for all other variables
1507 for ( k = 0; k < nWords; k++ )
1508 {
1509 Counter = Kit_WordCountOnes( pTruth[k] );
1510 for ( i = 5; i < nVars; i++ )
1511 if ( (k & (1 << (i-5))) == 0 )
1512 pStore[i] += Counter;
1513 }
1514 // count 1's for the first five variables
1515 for ( k = 0; k < nWords/2; k++ )
1516 {
1517 pStore[0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1518 pStore[1] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1519 pStore[2] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1520 pStore[3] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1521 pStore[4] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1522 pTruth += 2;
1523 }
1524}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthCountOnesInCofsSlow()

void Kit_TruthCountOnesInCofsSlow ( unsigned * pTruth,
int nVars,
int * pStore,
unsigned * pAux )

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

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

Description [Verifies the above procedure.]

SideEffects []

SeeAlso []

Definition at line 1537 of file kitTruth.c.

1538{
1539 int i;
1540 for ( i = 0; i < nVars; i++ )
1541 {
1542 Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
1543 pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1544 Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
1545 pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1546 }
1547}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthDumpToFile()

char * Kit_TruthDumpToFile ( unsigned * pTruth,
int nVars,
int nFile )

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2004 of file kitTruth.c.

2005{
2006 static char pFileName[100];
2007 FILE * pFile;
2008 sprintf( pFileName, "tt\\s%04d", nFile );
2009 pFile = fopen( pFileName, "w" );
2010 fprintf( pFile, "rt " );
2011 Kit_PrintHexadecimal( pFile, pTruth, nVars );
2012 fprintf( pFile, "; bdd; sop; ps\n" );
2013 fclose( pFile );
2014 return pFileName;
2015}
sprintf
char * sprintf()
Here is the call graph for this function:

◆ Kit_TruthExist()

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

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 684 of file kitTruth.c.

685{
686 int nWords = Kit_TruthWordNum( nVars );
687 int i, k, Step;
688
689 assert( iVar < nVars );
690 switch ( iVar )
691 {
692 case 0:
693 for ( i = 0; i < nWords; i++ )
694 pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
695 return;
696 case 1:
697 for ( i = 0; i < nWords; i++ )
698 pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
699 return;
700 case 2:
701 for ( i = 0; i < nWords; i++ )
702 pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
703 return;
704 case 3:
705 for ( i = 0; i < nWords; i++ )
706 pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
707 return;
708 case 4:
709 for ( i = 0; i < nWords; i++ )
710 pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
711 return;
712 default:
713 Step = (1 << (iVar - 5));
714 for ( k = 0; k < nWords; k += 2*Step )
715 {
716 for ( i = 0; i < Step; i++ )
717 {
718 pTruth[i] |= pTruth[Step+i];
719 pTruth[Step+i] = pTruth[i];
720 }
721 pTruth += 2*Step;
722 }
723 return;
724 }
725}
Here is the caller graph for this function:

◆ Kit_TruthExistNew()

void Kit_TruthExistNew ( unsigned * pRes,
unsigned * pTruth,
int nVars,
int iVar )

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file kitTruth.c.

739{
740 int nWords = Kit_TruthWordNum( nVars );
741 int i, k, Step;
742
743 assert( iVar < nVars );
744 switch ( iVar )
745 {
746 case 0:
747 for ( i = 0; i < nWords; i++ )
748 pRes[i] = pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
749 return;
750 case 1:
751 for ( i = 0; i < nWords; i++ )
752 pRes[i] = pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
753 return;
754 case 2:
755 for ( i = 0; i < nWords; i++ )
756 pRes[i] = pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
757 return;
758 case 3:
759 for ( i = 0; i < nWords; i++ )
760 pRes[i] = pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
761 return;
762 case 4:
763 for ( i = 0; i < nWords; i++ )
764 pRes[i] = pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
765 return;
766 default:
767 Step = (1 << (iVar - 5));
768 for ( k = 0; k < nWords; k += 2*Step )
769 {
770 for ( i = 0; i < Step; i++ )
771 {
772 pRes[i] = pTruth[i] | pTruth[Step+i];
773 pRes[Step+i] = pRes[i];
774 }
775 pRes += 2*Step;
776 pTruth += 2*Step;
777 }
778 return;
779 }
780}
Here is the caller graph for this function:

◆ Kit_TruthExistSet()

void Kit_TruthExistSet ( unsigned * pRes,
unsigned * pTruth,
int nVars,
unsigned uMask )

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

Synopsis [Existantially quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file kitTruth.c.

794{
795 int v;
796 Kit_TruthCopy( pRes, pTruth, nVars );
797 for ( v = 0; v < nVars; v++ )
798 if ( uMask & (1 << v) )
799 Kit_TruthExist( pRes, nVars, v );
800}
Kit_TruthExist
void Kit_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:684
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthForall()

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

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

Synopsis [Unversally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file kitTruth.c.

814{
815 int nWords = Kit_TruthWordNum( nVars );
816 int i, k, Step;
817
818 assert( iVar < nVars );
819 switch ( iVar )
820 {
821 case 0:
822 for ( i = 0; i < nWords; i++ )
823 pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
824 return;
825 case 1:
826 for ( i = 0; i < nWords; i++ )
827 pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
828 return;
829 case 2:
830 for ( i = 0; i < nWords; i++ )
831 pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
832 return;
833 case 3:
834 for ( i = 0; i < nWords; i++ )
835 pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
836 return;
837 case 4:
838 for ( i = 0; i < nWords; i++ )
839 pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
840 return;
841 default:
842 Step = (1 << (iVar - 5));
843 for ( k = 0; k < nWords; k += 2*Step )
844 {
845 for ( i = 0; i < Step; i++ )
846 {
847 pTruth[i] &= pTruth[Step+i];
848 pTruth[Step+i] = pTruth[i];
849 }
850 pTruth += 2*Step;
851 }
852 return;
853 }
854}
Here is the caller graph for this function:

◆ Kit_TruthForallNew()

void Kit_TruthForallNew ( unsigned * pRes,
unsigned * pTruth,
int nVars,
int iVar )

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 867 of file kitTruth.c.

868{
869 int nWords = Kit_TruthWordNum( nVars );
870 int i, k, Step;
871
872 assert( iVar < nVars );
873 switch ( iVar )
874 {
875 case 0:
876 for ( i = 0; i < nWords; i++ )
877 pRes[i] = pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
878 return;
879 case 1:
880 for ( i = 0; i < nWords; i++ )
881 pRes[i] = pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
882 return;
883 case 2:
884 for ( i = 0; i < nWords; i++ )
885 pRes[i] = pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
886 return;
887 case 3:
888 for ( i = 0; i < nWords; i++ )
889 pRes[i] = pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
890 return;
891 case 4:
892 for ( i = 0; i < nWords; i++ )
893 pRes[i] = pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
894 return;
895 default:
896 Step = (1 << (iVar - 5));
897 for ( k = 0; k < nWords; k += 2*Step )
898 {
899 for ( i = 0; i < Step; i++ )
900 {
901 pRes[i] = pTruth[i] & pTruth[Step+i];
902 pRes[Step+i] = pRes[i];
903 }
904 pRes += 2*Step;
905 pTruth += 2*Step;
906 }
907 return;
908 }
909}
Here is the caller graph for this function:

◆ Kit_TruthForallSet()

void Kit_TruthForallSet ( unsigned * pRes,
unsigned * pTruth,
int nVars,
unsigned uMask )

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

Synopsis [Universally quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1048 of file kitTruth.c.

1049{
1050 int v;
1051 Kit_TruthCopy( pRes, pTruth, nVars );
1052 for ( v = 0; v < nVars; v++ )
1053 if ( uMask & (1 << v) )
1054 Kit_TruthForall( pRes, nVars, v );
1055}
Kit_TruthForall
void Kit_TruthForall(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:813
Here is the call graph for this function:

◆ Kit_TruthHash()

unsigned Kit_TruthHash ( unsigned * pIn,
int nWords )

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1560 of file kitTruth.c.

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

◆ Kit_TruthMinCofSuppOverlap()

int Kit_TruthMinCofSuppOverlap ( unsigned * pTruth,
int nVars,
int * pVarMin )

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 1315 of file kitTruth.c.

1316{
1317 static unsigned uCofactor[16];
1318 int i, ValueCur, ValueMin, VarMin;
1319 unsigned uSupp0, uSupp1;
1320 int nVars0, nVars1;
1321 assert( nVars <= 9 );
1322 ValueMin = 32;
1323 VarMin = -1;
1324 for ( i = 0; i < nVars; i++ )
1325 {
1326 // get negative cofactor
1327 Kit_TruthCopy( uCofactor, pTruth, nVars );
1328 Kit_TruthCofactor0( uCofactor, nVars, i );
1329 uSupp0 = Kit_TruthSupport( uCofactor, nVars );
1330 nVars0 = Kit_WordCountOnes( uSupp0 );
1331//Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
1332 // get positive cofactor
1333 Kit_TruthCopy( uCofactor, pTruth, nVars );
1334 Kit_TruthCofactor1( uCofactor, nVars, i );
1335 uSupp1 = Kit_TruthSupport( uCofactor, nVars );
1336 nVars1 = Kit_WordCountOnes( uSupp1 );
1337//Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
1338 // get the number of common vars
1339 ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
1340 if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
1341 {
1342 ValueMin = ValueCur;
1343 VarMin = i;
1344 }
1345 if ( ValueMin == 0 )
1346 break;
1347 }
1348 if ( pVarMin )
1349 *pVarMin = VarMin;
1350 return ValueMin;
1351}
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:368
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:470
Here is the call graph for this function:

◆ Kit_TruthMuxVar()

void Kit_TruthMuxVar ( unsigned * pOut,
unsigned * pCof0,
unsigned * pCof1,
int nVars,
int iVar )

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1069 of file kitTruth.c.

1070{
1071 int nWords = Kit_TruthWordNum( nVars );
1072 int i, k, Step;
1073
1074 assert( iVar < nVars );
1075 switch ( iVar )
1076 {
1077 case 0:
1078 for ( i = 0; i < nWords; i++ )
1079 pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1080 return;
1081 case 1:
1082 for ( i = 0; i < nWords; i++ )
1083 pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1084 return;
1085 case 2:
1086 for ( i = 0; i < nWords; i++ )
1087 pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1088 return;
1089 case 3:
1090 for ( i = 0; i < nWords; i++ )
1091 pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1092 return;
1093 case 4:
1094 for ( i = 0; i < nWords; i++ )
1095 pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1096 return;
1097 default:
1098 Step = (1 << (iVar - 5));
1099 for ( k = 0; k < nWords; k += 2*Step )
1100 {
1101 for ( i = 0; i < Step; i++ )
1102 {
1103 pOut[i] = pCof0[i];
1104 pOut[Step+i] = pCof1[Step+i];
1105 }
1106 pOut += 2*Step;
1107 pCof0 += 2*Step;
1108 pCof1 += 2*Step;
1109 }
1110 return;
1111 }
1112}
Here is the caller graph for this function:

◆ Kit_TruthMuxVarPhase()

void Kit_TruthMuxVarPhase ( unsigned * pOut,
unsigned * pCof0,
unsigned * pCof1,
int nVars,
int iVar,
int fCompl0 )

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1125 of file kitTruth.c.

1126{
1127 int nWords = Kit_TruthWordNum( nVars );
1128 int i, k, Step;
1129
1130 if ( fCompl0 == 0 )
1131 {
1132 Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
1133 return;
1134 }
1135
1136 assert( iVar < nVars );
1137 switch ( iVar )
1138 {
1139 case 0:
1140 for ( i = 0; i < nWords; i++ )
1141 pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1142 return;
1143 case 1:
1144 for ( i = 0; i < nWords; i++ )
1145 pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1146 return;
1147 case 2:
1148 for ( i = 0; i < nWords; i++ )
1149 pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1150 return;
1151 case 3:
1152 for ( i = 0; i < nWords; i++ )
1153 pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1154 return;
1155 case 4:
1156 for ( i = 0; i < nWords; i++ )
1157 pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1158 return;
1159 default:
1160 Step = (1 << (iVar - 5));
1161 for ( k = 0; k < nWords; k += 2*Step )
1162 {
1163 for ( i = 0; i < Step; i++ )
1164 {
1165 pOut[i] = ~pCof0[i];
1166 pOut[Step+i] = pCof1[Step+i];
1167 }
1168 pOut += 2*Step;
1169 pCof0 += 2*Step;
1170 pCof1 += 2*Step;
1171 }
1172 return;
1173 }
1174}
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition kitTruth.c:1069
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthPermute()

void Kit_TruthPermute ( unsigned * pOut,
unsigned * pIn,
int nVars,
char * pPerm,
int fReturnIn )

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

Synopsis [Implement give permutation.]

Description [The input and output truth tables are in pIn/pOut. The number of variables is nVars. Permutation is in pPerm.]

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 233 of file kitTruth.c.

234{
235 unsigned * pTemp;
236 int i, Temp, fChange, Counter = 0;
237 do {
238 fChange = 0;
239 for ( i = 0; i < nVars-1; i++ )
240 {
241 assert( pPerm[i] != pPerm[i+1] );
242 if ( pPerm[i] <= pPerm[i+1] )
243 continue;
244 Counter++;
245 fChange = 1;
246
247 Temp = pPerm[i];
248 pPerm[i] = pPerm[i+1];
249 pPerm[i+1] = Temp;
250
251 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
252 pTemp = pIn; pIn = pOut; pOut = pTemp;
253 }
254 } while ( fChange );
255 if ( fReturnIn ^ !(Counter & 1) )
256 Kit_TruthCopy( pOut, pIn, nVars );
257}
Kit_TruthSwapAdjacentVars
ABC_NAMESPACE_IMPL_START void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
DECLARATIONS ///.
Definition kitTruth.c:46
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthPrintProfile()

void Kit_TruthPrintProfile ( unsigned * pTruth,
int nVars )

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2203 of file kitTruth.c.

2204{
2205 unsigned uTruth[2];
2206 if ( nVars >= 6 )
2207 {
2208 Kit_TruthPrintProfile_int( pTruth, nVars );
2209 return;
2210 }
2211 assert( nVars >= 2 );
2212 uTruth[0] = pTruth[0];
2213 uTruth[1] = pTruth[0];
2214 Kit_TruthPrintProfile( uTruth, 6 );
2215}
Kit_TruthPrintProfile
void Kit_TruthPrintProfile(unsigned *pTruth, int nVars)
Definition kitTruth.c:2203
Kit_TruthPrintProfile_int
void Kit_TruthPrintProfile_int(unsigned *pTruth, int nVars)
Definition kitTruth.c:2029
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthPrintProfile_int()

void Kit_TruthPrintProfile_int ( unsigned * pTruth,
int nVars )

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2029 of file kitTruth.c.

2030{
2031 int Mints[20];
2032 int Mints0[20];
2033 int Mints1[20];
2034 int Unique1[20];
2035 int Total2[20][20];
2036 int Unique2[20][20];
2037 int Common2[20][20];
2038 int nWords = Kit_TruthWordNum( nVars );
2039 int * pBytes = ABC_ALLOC( int, nWords * 4 );
2040 unsigned * pIn = ABC_ALLOC( unsigned, nWords );
2041 unsigned * pOut = ABC_ALLOC( unsigned, nWords );
2042 unsigned * pCof00 = ABC_ALLOC( unsigned, nWords );
2043 unsigned * pCof01 = ABC_ALLOC( unsigned, nWords );
2044 unsigned * pCof10 = ABC_ALLOC( unsigned, nWords );
2045 unsigned * pCof11 = ABC_ALLOC( unsigned, nWords );
2046 unsigned * pTemp;
2047 int nTotalMints, nTotalMints0, nTotalMints1;
2048 int v, u, i, iVar, nMints1;
2049 int Cof00, Cof01, Cof10, Cof11;
2050 int Coz00, Coz01, Coz10, Coz11;
2051 assert( nVars <= 20 );
2052 assert( nVars >= 6 );
2053
2054 nTotalMints = Kit_TruthCountMinterms( pTruth, nVars, Mints, pBytes );
2055 for ( v = 0; v < nVars; v++ )
2056 Unique1[v] = Kit_TruthBooleanDiffCount( pTruth, nVars, v );
2057
2058 for ( v = 0; v < nVars; v++ )
2059 for ( u = 0; u < nVars; u++ )
2060 Total2[v][u] = Unique2[v][u] = Common2[v][u] = -1;
2061
2062 nMints1 = (1<<(nVars-2));
2063 for ( v = 0; v < nVars; v++ )
2064 {
2065 // move this var to be the first
2066 Kit_TruthCopy( pIn, pTruth, nVars );
2067// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2068 for ( i = v; i < nVars - 1; i++ )
2069 {
2070 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
2071 pTemp = pIn; pIn = pOut; pOut = pTemp;
2072 }
2073// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2074// printf( "\n" );
2075
2076
2077 // count minterms in both cofactor
2078 nTotalMints0 = Kit_TruthCountMinterms( pIn, nVars-1, Mints0, pBytes );
2079 nTotalMints1 = Kit_TruthCountMinterms( pIn+nWords/2, nVars-1, Mints1, pBytes );
2080 assert( nTotalMints == nTotalMints0 + nTotalMints1 );
2081/*
2082 for ( u = 0; u < nVars-1; u++ )
2083 printf( "%2d ", Mints0[u] );
2084 printf( "\n" );
2085
2086 for ( u = 0; u < nVars-1; u++ )
2087 printf( "%2d ", Mints1[u] );
2088 printf( "\n" );
2089*/
2090 for ( u = 0; u < nVars-1; u++ )
2091 {
2092 if ( u < v )
2093 iVar = u;
2094 else
2095 iVar = u + 1;
2096 assert( v != iVar );
2097 // get minter counts in the cofactors
2098 Cof00 = Mints0[u]; Coz00 = nMints1 - Cof00;
2099 Cof01 = nTotalMints0-Mints0[u]; Coz01 = nMints1 - Cof01;
2100 Cof10 = Mints1[u]; Coz10 = nMints1 - Cof10;
2101 Cof11 = nTotalMints1-Mints1[u]; Coz11 = nMints1 - Cof11;
2102
2103 assert( Cof00 >= 0 && Cof00 <= nMints1 );
2104 assert( Cof01 >= 0 && Cof01 <= nMints1 );
2105 assert( Cof10 >= 0 && Cof10 <= nMints1 );
2106 assert( Cof11 >= 0 && Cof11 <= nMints1 );
2107
2108 assert( Coz00 >= 0 && Coz00 <= nMints1 );
2109 assert( Coz01 >= 0 && Coz01 <= nMints1 );
2110 assert( Coz10 >= 0 && Coz10 <= nMints1 );
2111 assert( Coz11 >= 0 && Coz11 <= nMints1 );
2112
2113 Common2[v][iVar] = Common2[iVar][v] = Cof00 * Coz11 + Coz00 * Cof11 + Cof01 * Coz10 + Coz01 * Cof10;
2114
2115 Total2[v][iVar] = Total2[iVar][v] =
2116 Cof00 * Coz01 + Coz00 * Cof01 +
2117 Cof00 * Coz10 + Coz00 * Cof10 +
2118 Cof00 * Coz11 + Coz00 * Cof11 +
2119 Cof01 * Coz10 + Coz01 * Cof10 +
2120 Cof01 * Coz11 + Coz01 * Cof11 +
2121 Cof10 * Coz11 + Coz10 * Cof11 ;
2122
2123
2124 Kit_TruthCofactor0New( pCof00, pIn, nVars-1, u );
2125 Kit_TruthCofactor1New( pCof01, pIn, nVars-1, u );
2126 Kit_TruthCofactor0New( pCof10, pIn+nWords/2, nVars-1, u );
2127 Kit_TruthCofactor1New( pCof11, pIn+nWords/2, nVars-1, u );
2128
2129 Unique2[v][iVar] = Unique2[iVar][v] =
2130 Kit_TruthXorCount( pCof00, pCof01, nVars-1 ) +
2131 Kit_TruthXorCount( pCof00, pCof10, nVars-1 ) +
2132 Kit_TruthXorCount( pCof00, pCof11, nVars-1 ) +
2133 Kit_TruthXorCount( pCof01, pCof10, nVars-1 ) +
2134 Kit_TruthXorCount( pCof01, pCof11, nVars-1 ) +
2135 Kit_TruthXorCount( pCof10, pCof11, nVars-1 );
2136 }
2137 }
2138
2139 printf( "\n" );
2140 printf( " V: " );
2141 for ( v = 0; v < nVars; v++ )
2142 printf( "%8c ", v+'a' );
2143 printf( "\n" );
2144
2145 printf( " M: " );
2146 for ( v = 0; v < nVars; v++ )
2147 printf( "%8d ", Mints[v] );
2148 printf( "\n" );
2149
2150 printf( " U: " );
2151 for ( v = 0; v < nVars; v++ )
2152 printf( "%8d ", Unique1[v] );
2153 printf( "\n" );
2154 printf( "\n" );
2155
2156 printf( "Unique:\n" );
2157 for ( i = 0; i < nVars; i++ )
2158 {
2159 printf( " %2d ", i );
2160 for ( v = 0; v < nVars; v++ )
2161 printf( "%8d ", Unique2[i][v] );
2162 printf( "\n" );
2163 }
2164
2165 printf( "Common:\n" );
2166 for ( i = 0; i < nVars; i++ )
2167 {
2168 printf( " %2d ", i );
2169 for ( v = 0; v < nVars; v++ )
2170 printf( "%8d ", Common2[i][v] );
2171 printf( "\n" );
2172 }
2173
2174 printf( "Total:\n" );
2175 for ( i = 0; i < nVars; i++ )
2176 {
2177 printf( " %2d ", i );
2178 for ( v = 0; v < nVars; v++ )
2179 printf( "%8d ", Total2[i][v] );
2180 printf( "\n" );
2181 }
2182
2183 ABC_FREE( pIn );
2184 ABC_FREE( pOut );
2185 ABC_FREE( pCof00 );
2186 ABC_FREE( pCof01 );
2187 ABC_FREE( pCof10 );
2188 ABC_FREE( pCof11 );
2189 ABC_FREE( pBytes );
2190}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Kit_TruthBooleanDiffCount
int Kit_TruthBooleanDiffCount(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:977
Kit_TruthCountMinterms
int Kit_TruthCountMinterms(unsigned *pTruth, int nVars, int *pRes, int *pBytesInit)
Definition kitTruth.c:1839
Kit_TruthXorCount
int Kit_TruthXorCount(unsigned *pTruth0, unsigned *pTruth1, int nVars)
Definition kitTruth.c:1028
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthSemiCanonicize()

unsigned Kit_TruthSemiCanonicize ( unsigned * pInOut,
unsigned * pAux,
int nVars,
char * pCanonPerm )

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 1657 of file kitTruth.c.

1658{
1659 int pStore[32];
1660 unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
1661 int nWords = Kit_TruthWordNum( nVars );
1662 int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
1663 unsigned uCanonPhase;
1664
1665 // canonicize output
1666 uCanonPhase = 0;
1667 for ( i = 0; i < nVars; i++ )
1668 pCanonPerm[i] = i;
1669
1670 nOnes = Kit_TruthCountOnes(pIn, nVars);
1671 //if(pIn[0] & 1)
1672 if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
1673 {
1674 uCanonPhase |= (1 << nVars);
1675 Kit_TruthNot( pIn, pIn, nVars );
1676 }
1677
1678 // collect the minterm counts
1679 Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
1680/*
1681 Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
1682 for ( i = 0; i < 2*nVars; i++ )
1683 {
1684 assert( pStore[i] == pStore2[i] );
1685 }
1686*/
1687 // canonicize phase
1688 for ( i = 0; i < nVars; i++ )
1689 {
1690 if ( pStore[2*i+0] >= pStore[2*i+1] )
1691 continue;
1692 uCanonPhase |= (1 << i);
1693 Temp = pStore[2*i+0];
1694 pStore[2*i+0] = pStore[2*i+1];
1695 pStore[2*i+1] = Temp;
1696 Kit_TruthChangePhase( pIn, nVars, i );
1697 }
1698
1699// Kit_PrintHexadecimal( stdout, pIn, nVars );
1700// printf( "\n" );
1701
1702 // permute
1703 Counter = 0;
1704 do {
1705 fChange = 0;
1706 for ( i = 0; i < nVars-1; i++ )
1707 {
1708 if ( pStore[2*i] >= pStore[2*(i+1)] )
1709 continue;
1710 Counter++;
1711 fChange = 1;
1712
1713 Temp = pCanonPerm[i];
1714 pCanonPerm[i] = pCanonPerm[i+1];
1715 pCanonPerm[i+1] = Temp;
1716
1717 Temp = pStore[2*i];
1718 pStore[2*i] = pStore[2*(i+1)];
1719 pStore[2*(i+1)] = Temp;
1720
1721 Temp = pStore[2*i+1];
1722 pStore[2*i+1] = pStore[2*(i+1)+1];
1723 pStore[2*(i+1)+1] = Temp;
1724
1725 // if the polarity of variables is different, swap them
1726 if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
1727 {
1728 uCanonPhase ^= (1 << i);
1729 uCanonPhase ^= (1 << (i+1));
1730 }
1731
1732 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
1733 pTemp = pIn; pIn = pOut; pOut = pTemp;
1734 }
1735 } while ( fChange );
1736
1737
1738/*
1739 Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
1740 for ( i = 0; i < nVars; i++ )
1741 printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
1742 printf( " C = %d\n", Counter );
1743 Extra_PrintHexadecimal( stdout, pIn, nVars );
1744 printf( "\n" );
1745*/
1746
1747/*
1748 // process symmetric variable groups
1749 uSymms = 0;
1750 for ( i = 0; i < nVars-1; i++ )
1751 {
1752 if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1753 continue;
1754 if ( pStore[2*i] != pStore[2*i+1] )
1755 continue;
1756 if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
1757 continue;
1758 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
1759 Kit_TruthChangePhase( pIn, nVars, i+1 );
1760 }
1761*/
1762
1763/*
1764 // process symmetric variable groups
1765 uSymms = 0;
1766 for ( i = 0; i < nVars-1; i++ )
1767 {
1768 if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1769 continue;
1770 // i and i+1 can be symmetric
1771 // find the end of this group
1772 for ( k = i+1; k < nVars; k++ )
1773 if ( pStore[2*i] != pStore[2*k] )
1774 break;
1775 Limit = k;
1776 assert( i < Limit-1 );
1777 // go through the variables in this group
1778 for ( j = i + 1; j < Limit; j++ )
1779 {
1780 // check symmetry
1781 if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
1782 {
1783 uSymms |= (1 << j);
1784 continue;
1785 }
1786 // they are phase-unknown
1787 if ( pStore[2*i] == pStore[2*i+1] )
1788 {
1789 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
1790 {
1791 Kit_TruthChangePhase( pIn, nVars, j );
1792 uCanonPhase ^= (1 << j);
1793 uSymms |= (1 << j);
1794 continue;
1795 }
1796 }
1797
1798 // they are not symmetric - move j as far as it goes in the group
1799 for ( k = j; k < Limit-1; k++ )
1800 {
1801 Counter++;
1802
1803 Temp = pCanonPerm[k];
1804 pCanonPerm[k] = pCanonPerm[k+1];
1805 pCanonPerm[k+1] = Temp;
1806
1807 assert( pStore[2*k] == pStore[2*(k+1)] );
1808 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
1809 pTemp = pIn; pIn = pOut; pOut = pTemp;
1810 }
1811 Limit--;
1812 j--;
1813 }
1814 i = Limit - 1;
1815 }
1816*/
1817
1818 // swap if it was moved an even number of times
1819 if ( Counter & 1 )
1820 Kit_TruthCopy( pOut, pIn, nVars );
1821 return uCanonPhase;
1822}
Kit_TruthCountOnesInCofs
void Kit_TruthCountOnesInCofs(unsigned *pTruth, int nVars, int *pStore)
Definition kitTruth.c:1410
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:1259
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthShrink()

void Kit_TruthShrink ( unsigned * pOut,
unsigned * pIn,
int nVars,
int nVarsAll,
unsigned Phase,
int fReturnIn )

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) shows what variables should remain.]

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 200 of file kitTruth.c.

201{
202 unsigned * pTemp;
203 int i, k, Var = 0, Counter = 0;
204 for ( i = 0; i < nVarsAll; i++ )
205 if ( Phase & (1 << i) )
206 {
207 for ( k = i-1; k >= Var; k-- )
208 {
209 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
210 pTemp = pIn; pIn = pOut; pOut = pTemp;
211 Counter++;
212 }
213 Var++;
214 }
215 assert( Var == nVars );
216 // swap if it was moved an even number of times
217 if ( fReturnIn ^ !(Counter & 1) )
218 Kit_TruthCopy( pOut, pIn, nVarsAll );
219}
Var
int Var
Definition exorList.c:228
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthStretch()

void Kit_TruthStretch ( unsigned * pOut,
unsigned * pIn,
int nVars,
int nVarsAll,
unsigned Phase,
int fReturnIn )

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 [The input truth table is modified.]

SeeAlso []

Definition at line 166 of file kitTruth.c.

167{
168 unsigned * pTemp;
169 int i, k, Var = nVars - 1, Counter = 0;
170 for ( i = nVarsAll - 1; i >= 0; i-- )
171 if ( Phase & (1 << i) )
172 {
173 for ( k = Var; k < i; k++ )
174 {
175 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
176 pTemp = pIn; pIn = pOut; pOut = pTemp;
177 Counter++;
178 }
179 Var--;
180 }
181 assert( Var == -1 );
182 // swap if it was moved an even number of times
183 if ( fReturnIn ^ !(Counter & 1) )
184 Kit_TruthCopy( pOut, pIn, nVarsAll );
185}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthSupport()

unsigned Kit_TruthSupport ( unsigned * pTruth,
int nVars )

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file kitTruth.c.

347{
348 int i, Support = 0;
349 for ( i = 0; i < nVars; i++ )
350 if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
351 Support |= (1 << i);
352 return Support;
353}
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:270
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthSupportSize()

int Kit_TruthSupportSize ( unsigned * pTruth,
int nVars )

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file kitTruth.c.

328{
329 int i, Counter = 0;
330 for ( i = 0; i < nVars; i++ )
331 Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
332 return Counter;
333}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthSwapAdjacentVars()

ABC_NAMESPACE_IMPL_START void Kit_TruthSwapAdjacentVars ( unsigned * pOut,
unsigned * pIn,
int nVars,
int iVar )

DECLARATIONS ///.

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

FileName [kitTruth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving truth tables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id
kitTruth.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// 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 46 of file kitTruth.c.

47{
48 static unsigned PMasks[4][3] = {
49 { 0x99999999, 0x22222222, 0x44444444 },
50 { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
51 { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
52 { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
53 };
54 int nWords = Kit_TruthWordNum( nVars );
55 int i, k, Step, Shift;
56
57 assert( iVar < nVars - 1 );
58 if ( iVar < 4 )
59 {
60 Shift = (1 << iVar);
61 for ( i = 0; i < nWords; i++ )
62 pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
63 }
64 else if ( iVar > 4 )
65 {
66 Step = (1 << (iVar - 5));
67 for ( k = 0; k < nWords; k += 4*Step )
68 {
69 for ( i = 0; i < Step; i++ )
70 pOut[i] = pIn[i];
71 for ( i = 0; i < Step; i++ )
72 pOut[Step+i] = pIn[2*Step+i];
73 for ( i = 0; i < Step; i++ )
74 pOut[2*Step+i] = pIn[Step+i];
75 for ( i = 0; i < Step; i++ )
76 pOut[3*Step+i] = pIn[3*Step+i];
77 pIn += 4*Step;
78 pOut += 4*Step;
79 }
80 }
81 else // if ( iVar == 4 )
82 {
83 for ( i = 0; i < nWords; i += 2 )
84 {
85 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
86 pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
87 }
88 }
89}
Here is the caller graph for this function:

◆ Kit_TruthSwapAdjacentVars2()

void Kit_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 103 of file kitTruth.c.

104{
105 int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
106 int i, k, Step;
107
108 assert( Start < nVars - 1 );
109 switch ( Start )
110 {
111 case 0:
112 for ( i = 0; i < nWords; i++ )
113 pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
114 return;
115 case 1:
116 for ( i = 0; i < nWords; i++ )
117 pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
118 return;
119 case 2:
120 for ( i = 0; i < nWords; i++ )
121 pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
122 return;
123 case 3:
124 for ( i = 0; i < nWords; i++ )
125 pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
126 return;
127 case 4:
128 for ( i = 0; i < nWords; i += 2 )
129 {
130 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
131 pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
132 }
133 return;
134 default:
135 Step = (1 << (Start - 5));
136 for ( k = 0; k < nWords; k += 4*Step )
137 {
138 for ( i = 0; i < Step; i++ )
139 pOut[i] = pIn[i];
140 for ( i = 0; i < Step; i++ )
141 pOut[Step+i] = pIn[2*Step+i];
142 for ( i = 0; i < Step; i++ )
143 pOut[2*Step+i] = pIn[Step+i];
144 for ( i = 0; i < Step; i++ )
145 pOut[3*Step+i] = pIn[3*Step+i];
146 pIn += 4*Step;
147 pOut += 4*Step;
148 }
149 return;
150 }
151}

◆ Kit_TruthUniqueNew()

void Kit_TruthUniqueNew ( unsigned * pRes,
unsigned * pTruth,
int nVars,
int iVar )

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 922 of file kitTruth.c.

923{
924 int nWords = Kit_TruthWordNum( nVars );
925 int i, k, Step;
926
927 assert( iVar < nVars );
928 switch ( iVar )
929 {
930 case 0:
931 for ( i = 0; i < nWords; i++ )
932 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
933 return;
934 case 1:
935 for ( i = 0; i < nWords; i++ )
936 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
937 return;
938 case 2:
939 for ( i = 0; i < nWords; i++ )
940 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
941 return;
942 case 3:
943 for ( i = 0; i < nWords; i++ )
944 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
945 return;
946 case 4:
947 for ( i = 0; i < nWords; i++ )
948 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
949 return;
950 default:
951 Step = (1 << (iVar - 5));
952 for ( k = 0; k < nWords; k += 2*Step )
953 {
954 for ( i = 0; i < Step; i++ )
955 {
956 pRes[i] = pTruth[i] ^ pTruth[Step+i];
957 pRes[Step+i] = pRes[i];
958 }
959 pRes += 2*Step;
960 pTruth += 2*Step;
961 }
962 return;
963 }
964}
Here is the caller graph for this function:

◆ Kit_TruthVarInSupport()

int Kit_TruthVarInSupport ( unsigned * pTruth,
int nVars,
int iVar )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file kitTruth.c.

271{
272 int nWords = Kit_TruthWordNum( nVars );
273 int i, k, Step;
274
275 assert( iVar < nVars );
276 switch ( iVar )
277 {
278 case 0:
279 for ( i = 0; i < nWords; i++ )
280 if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
281 return 1;
282 return 0;
283 case 1:
284 for ( i = 0; i < nWords; i++ )
285 if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
286 return 1;
287 return 0;
288 case 2:
289 for ( i = 0; i < nWords; i++ )
290 if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
291 return 1;
292 return 0;
293 case 3:
294 for ( i = 0; i < nWords; i++ )
295 if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
296 return 1;
297 return 0;
298 case 4:
299 for ( i = 0; i < nWords; i++ )
300 if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
301 return 1;
302 return 0;
303 default:
304 Step = (1 << (iVar - 5));
305 for ( k = 0; k < nWords; k += 2*Step )
306 {
307 for ( i = 0; i < Step; i++ )
308 if ( pTruth[i] != pTruth[Step+i] )
309 return 1;
310 pTruth += 2*Step;
311 }
312 return 0;
313 }
314}
Here is the caller graph for this function:

◆ Kit_TruthVarIsVacuous()

int Kit_TruthVarIsVacuous ( unsigned * pOnset,
unsigned * pOffset,
int nVars,
int iVar )

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 625 of file kitTruth.c.

626{
627 int nWords = Kit_TruthWordNum( nVars );
628 int i, k, Step;
629
630 assert( iVar < nVars );
631 switch ( iVar )
632 {
633 case 0:
634 for ( i = 0; i < nWords; i++ )
635 if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
636 return 0;
637 return 1;
638 case 1:
639 for ( i = 0; i < nWords; i++ )
640 if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
641 return 0;
642 return 1;
643 case 2:
644 for ( i = 0; i < nWords; i++ )
645 if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
646 return 0;
647 return 1;
648 case 3:
649 for ( i = 0; i < nWords; i++ )
650 if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
651 return 0;
652 return 1;
653 case 4:
654 for ( i = 0; i < nWords; i++ )
655 if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
656 return 0;
657 return 1;
658 default:
659 Step = (1 << (iVar - 5));
660 for ( k = 0; k < nWords; k += 2*Step )
661 {
662 for ( i = 0; i < Step; i++ )
663 if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
664 return 0;
665 pOnset += 2*Step;
666 pOffset += 2*Step;
667 }
668 return 1;
669 }
670}
Here is the caller graph for this function:

◆ Kit_TruthVarsAntiSymm()

int Kit_TruthVarsAntiSymm ( unsigned * pTruth,
int nVars,
int iVar0,
int iVar1,
unsigned * pCof0,
unsigned * pCof1 )

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

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1223 of file kitTruth.c.

1224{
1225 static unsigned uTemp0[32], uTemp1[32];
1226 if ( pCof0 == NULL )
1227 {
1228 assert( nVars <= 10 );
1229 pCof0 = uTemp0;
1230 }
1231 if ( pCof1 == NULL )
1232 {
1233 assert( nVars <= 10 );
1234 pCof1 = uTemp1;
1235 }
1236 // compute Cof00
1237 Kit_TruthCopy( pCof0, pTruth, nVars );
1238 Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1239 Kit_TruthCofactor0( pCof0, nVars, iVar1 );
1240 // compute Cof11
1241 Kit_TruthCopy( pCof1, pTruth, nVars );
1242 Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1243 Kit_TruthCofactor1( pCof1, nVars, iVar1 );
1244 // compare
1245 return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1246}
Here is the call graph for this function:

◆ Kit_TruthVarsSymm()

int Kit_TruthVarsSymm ( unsigned * pTruth,
int nVars,
int iVar0,
int iVar1,
unsigned * pCof0,
unsigned * pCof1 )

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

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1187 of file kitTruth.c.

1188{
1189 static unsigned uTemp0[32], uTemp1[32];
1190 if ( pCof0 == NULL )
1191 {
1192 assert( nVars <= 10 );
1193 pCof0 = uTemp0;
1194 }
1195 if ( pCof1 == NULL )
1196 {
1197 assert( nVars <= 10 );
1198 pCof1 = uTemp1;
1199 }
1200 // compute Cof01
1201 Kit_TruthCopy( pCof0, pTruth, nVars );
1202 Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1203 Kit_TruthCofactor1( pCof0, nVars, iVar1 );
1204 // compute Cof10
1205 Kit_TruthCopy( pCof1, pTruth, nVars );
1206 Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1207 Kit_TruthCofactor0( pCof1, nVars, iVar1 );
1208 // compare
1209 return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1210}
Here is the call graph for this function:

◆ Kit_TruthXorCount()

int Kit_TruthXorCount ( unsigned * pTruth0,
unsigned * pTruth1,
int nVars )

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

Synopsis [Returns the number of minterms in the Boolean difference.]

Description []

SideEffects []

SeeAlso []

Definition at line 1028 of file kitTruth.c.

1029{
1030 int nWords = Kit_TruthWordNum( nVars );
1031 int i, Counter = 0;
1032 for ( i = 0; i < nWords; i++ )
1033 Counter += Kit_WordCountOnes( pTruth0[i] ^ pTruth1[i] );
1034 return Counter;
1035}
Here is the caller graph for this function: