dauCanon.c File Reference

#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecMem.h"
#include "bool/lucky/lucky.h"
#include <math.h>

Include dependency graph for dauCanon.c:

Go to the source code of this file.

Classes
struct	Abc_TtHieMan_t_
struct	TiedGroup_
struct	Abc_TgMan_t_
struct	Abc_SccCost_t_

Macros
#define	TT_MAX_LEVELS   5
#define	CANON_VERIFY

Typedefs
typedef struct TiedGroup_	TiedGroup
typedef struct Abc_TgMan_t_	Abc_TgMan_t
typedef struct Abc_SccCost_t_	Abc_SccCost_t

Functions
void	Abc_TtNormalizeSmallTruth (word *pTruth, int nVars)
int	Abc_TtCountOnesInCofsSimple (word *pTruth, int nVars, int *pStore)
int	Abc_TtScc (word *pTruth, int nVars)
int	Abc_TtCountOnesInCofsFast6_rec (word Truth, int iVar, int nBytes, int *pStore)
int	Abc_TtCountOnesInCofsFast_rec (word *pTruth, int iVar, int nWords, int *pStore)
int	Abc_TtCountOnesInCofsFast (word *pTruth, int nVars, int *pStore)
void	Abc_TtCofactorTest10 (word *pTruth, int nVars, int N)
int	Abc_Tt6CofactorPermNaive (word *pTruth, int i, int fSwapOnly)
int	Abc_TtCofactorPermNaive (word *pTruth, int i, int nWords, int fSwapOnly)
int	Abc_TtCofactorPermConfig (word *pTruth, int i, int nWords, int fSwapOnly, int fNaive)
int	Abc_TtCofactorPerm (word *pTruth, int i, int nWords, int fSwapOnly, char *pCanonPerm, unsigned *puCanonPhase, int fNaive)
unsigned	Abc_TtCanonicize (word *pTruth, int nVars, char *pCanonPerm)
	FUNCTION DECLARATIONS ///.
unsigned	Abc_TtCanonicizePerm (word *pTruth, int nVars, char *pCanonPerm)
unsigned	Abc_TtCanonicizePhase (word *pTruth, int nVars)
Abc_TtHieMan_t *	Abc_TtHieManStart (int nVars, int nLevels)
void	Abc_TtHieManStop (Abc_TtHieMan_t *p)
int	Abc_TtHieRetrieveOrInsert (Abc_TtHieMan_t *p, int level, word *pTruth, word *pResult)
unsigned	Abc_TtCanonicizeHie (Abc_TtHieMan_t *p, word *pTruthInit, int nVars, char *pCanonPerm, int fExact)
unsigned	Abc_TtCanonicizeWrap (TtCanonicizeFunc func, Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)
int	Abc_TgExpendSymmetry (Abc_TgMan_t *pMan, char *pDest)
unsigned	Abc_TtCanonicizeAda (Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int iThres)
unsigned	Abc_TtCanonicizeCA (Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int fCA)

Variables
word	gpVerCopy [1024]

Macro Definition Documentation

CANON_VERIFY

#define CANON_VERIFY

Definition at line 1495 of file dauCanon.c.

TT_MAX_LEVELS

#define TT_MAX_LEVELS   5

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

Synopsis [Hierarchical semi-canonical form computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1243 of file dauCanon.c.

Typedef Documentation

Abc_SccCost_t

typedef struct Abc_SccCost_t_ Abc_SccCost_t

Abc_TgMan_t

typedef struct Abc_TgMan_t_ Abc_TgMan_t

TiedGroup

typedef struct TiedGroup_ TiedGroup

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

Synopsis [Adaptive exact/semi-canonical form computation.]

Description []

SideEffects []

SeeAlso []

Function Documentation

Abc_TgExpendSymmetry()

int Abc_TgExpendSymmetry ( Abc_TgMan_t * pMan, char * pDest )

extern

Definition at line 1980 of file dauCanon.c.

{
    int i = 0, j, k, s;
    char * pPerm = pMan->pPerm;
    for (j = 0; j < pMan->nGVars; j++)
        for (k = pPerm[j]; k >= 0; k = pMan->symLink[k])
            pDest[i++] = k;
    s = i;
    for (k = pMan->symLink[pMan->nVars]; k >= 0; k = pMan->symLink[k])
        pDest[i++] = k;
    assert(i == pMan->nVars);
    return s;
}

Here is the caller graph for this function:

Abc_Tt6CofactorPermNaive()

int Abc_Tt6CofactorPermNaive	(	word *	pTruth,
		int	i,
		int	fSwapOnly )

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

Synopsis [Naive evaluation.]

Description []

SideEffects []

SeeAlso []

Definition at line 740 of file dauCanon.c.

{
    if ( fSwapOnly )
    {
        word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i );
        if ( pTruth[0] > Copy )
        {
            pTruth[0] = Copy;
            return 4;
        }
        return 0;
    }
    {
        word Copy = pTruth[0];
        word Best = pTruth[0];
        int Config = 0;
        // PXY
        // 001
        Copy = Abc_Tt6Flip( Copy, i );
        if ( Best > Copy )
            Best = Copy, Config = 1;
        // PXY
        // 011
        Copy = Abc_Tt6Flip( Copy, i+1 );
        if ( Best > Copy )
            Best = Copy, Config = 3;
        // PXY
        // 010
        Copy = Abc_Tt6Flip( Copy, i );
        if ( Best > Copy )
            Best = Copy, Config = 2;
        // PXY
        // 110
        Copy = Abc_Tt6SwapAdjacent( Copy, i );
        if ( Best > Copy )
            Best = Copy, Config = 6;
        // PXY
        // 111
        Copy = Abc_Tt6Flip( Copy, i+1 );
        if ( Best > Copy )
            Best = Copy, Config = 7;
        // PXY
        // 101
        Copy = Abc_Tt6Flip( Copy, i );
        if ( Best > Copy )
            Best = Copy, Config = 5;
        // PXY
        // 100
        Copy = Abc_Tt6Flip( Copy, i+1 );
        if ( Best > Copy )
            Best = Copy, Config = 4;
        // PXY
        // 000
        Copy = Abc_Tt6SwapAdjacent( Copy, i );
        assert( Copy == pTruth[0] );
        assert( Best <= pTruth[0] );
        pTruth[0] = Best;
        return Config;
    }
}

Here is the caller graph for this function:

Abc_TtCanonicize()

unsigned Abc_TtCanonicize	(	word *	pTruth,
		int	nVars,
		char *	pCanonPerm )

FUNCTION DECLARATIONS ///.

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

Synopsis [Semi-canonical form computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1036 of file dauCanon.c.

{
    int pStoreIn[17];
    unsigned uCanonPhase;
    int i, k, nWords = Abc_TtWordNum( nVars );
    int fNaive = 1;
 
#ifdef CANON_VERIFY
    char pCanonPermCopy[16];
    static word pCopy1[1024];
    static word pCopy2[1024];
    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
#endif
 
    uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 0 );
    for ( k = 0; k < 5; k++ )
    {
        int fChanges = 0;
        for ( i = nVars - 2; i >= 0; i-- )
            if ( pStoreIn[i] == pStoreIn[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
        fChanges = 0;
        for ( i = 1; i < nVars - 1; i++ )
            if ( pStoreIn[i] == pStoreIn[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
    }
 
#ifdef CANON_VERIFY
    Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
    memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
    Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
    if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
        printf( "Canonical form verification failed!\n" );
#endif
/*
    if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
    {
        Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
        Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
        i = 0;
    }
*/
    return uCanonPhase;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCanonicizeAda()

unsigned Abc_TtCanonicizeAda	(	Abc_TtHieMan_t *	p,
		word *	pTruth,
		int	nVars,
		char *	pCanonPerm,
		int	iThres )

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

Synopsis [Adaptive heuristic/exact canonical form computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 2573 of file dauCanon.c.

{
    int nWords = Abc_TtWordNum(nVars);
    unsigned fExac = 0, fHash = 1 << 29;
    static word pCopy[1024];
    Abc_TgMan_t tgMan, tgManCopy;
    int iCost;
    const int MaxCost = 84;  // maximun posible cost for function with 16 inputs
    const int nAlg = iThres >= 1000 ? 1 : 0;
    const int fHigh = (iThres % 1000) >= 100, nEnumThres = iThres % 100;
 
    // handle constant
    if ( nVars == 0 ) {
        Abc_TtClear( pTruth, nWords );
        return 0;
    }
 
    Abc_TtVerifySmallTruth(pTruth, nVars);
#ifdef CANON_VERIFY
    Abc_TtCopy(gpVerCopy, pTruth, nWords, 0);
#endif
 
    assert(nVars <= 16);
    assert(!(nAlg && p == NULL));
    if (p && Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
    Abc_TgInitMan(&tgMan, pTruth, nVars, nAlg, p ? p->vPhase : NULL);
    Abc_TgCreateGroups(&tgMan);
    if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
    Abc_TgPurgeSymmetry(&tgMan, fHigh);
 
    Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
    Abc_TgImplementPerm(&tgMan, pCanonPerm);
    assert(Abc_TgCannonVerify(&tgMan));
 
    iCost = Abc_TgEnumerationCost(&tgMan);
    if (p == NULL || p->nLastLevel == 0) {
        if (nEnumThres > MaxCost || iCost < nEnumThres) {
            Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
            Abc_TgFullEnumeration(&tgManCopy, &tgMan);
        }
        else
            Abc_TgSimpleEnumeration(&tgMan);
    }
    else {
        if (nEnumThres > MaxCost || iCost < nEnumThres) fExac = 1 << 30;
        if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash + fExac;
        Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
        Abc_TgSimpleEnumeration(&tgMan);
        if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash + fExac;
        if (fExac) {
            Abc_TgManCopy(&tgMan, pTruth, &tgManCopy);
            Abc_TgFullEnumeration(&tgManCopy, &tgMan);
        }
        Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth);
    }
    memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars);
 
#ifdef CANON_VERIFY
    if (!Abc_TgCannonVerify(&tgMan))
        printf("Canonical form verification failed!\n");
#endif
    return tgMan.uPhase;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCanonicizeCA()

unsigned Abc_TtCanonicizeCA	(	Abc_TtHieMan_t *	p,
		word *	pTruth,
		int	nVars,
		char *	pCanonPerm,
		int	fCA )

Definition at line 2637 of file dauCanon.c.

{
    int nWords = Abc_TtWordNum(nVars);
    unsigned fHard = 0, fHash = 1 << 29;
    static word pCopy[1024];
    Abc_TgMan_t tgMan, tgManCopy;
    Abc_SccCost_t sc;
 
    // handle constant
    if (nVars == 0) {
        Abc_TtClear(pTruth, nWords);
        return 0;
    }
 
    Abc_TtVerifySmallTruth(pTruth, nVars);
#ifdef CANON_VERIFY
    Abc_TtCopy(gpVerCopy, pTruth, nWords, 0);
#endif
 
    assert(nVars <= 16);
    assert(p != NULL);
    if (Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
    Abc_TgInitMan(&tgMan, pTruth, nVars, 2, p->vPhase);
 
    Abc_TgCreateGroups(&tgMan);
    if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
    Abc_TgPurgeSymmetry(&tgMan, 1);
 
    Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
    Abc_TgImplementPerm(&tgMan, pCanonPerm);
    assert(Abc_TgCannonVerify(&tgMan));
 
    if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash;
    Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
    Abc_TgSimpleEnumeration(&tgMan);
    if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash;
    Abc_TgManCopy(&tgMan, pTruth, &tgManCopy);
    Abc_TtFill(pTruth, nWords);
 
    assert(Abc_TgCannonVerify(&tgManCopy));
    sc = Abc_TgRecordPhase(&tgManCopy, 0);
    if (fCA && Abc_SccEnumCost(&tgManCopy, sc) > Abc_SccPhaseCost(&tgManCopy))
    {
        Abc_TgResetGroup(&tgManCopy);
        sc = Abc_TgRecordPhase(&tgManCopy, 1);
        fHard = 1 << 28;
    }
    Abc_TgFullEnumeration(&tgManCopy, &tgMan);
    Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth);
    memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars);
 
#ifdef CANON_VERIFY
    if (!Abc_TgCannonVerify(&tgMan))
        printf("Canonical form verification failed!\n");
#endif
    return tgMan.uPhase | fHard;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCanonicizeHie()

unsigned Abc_TtCanonicizeHie	(	Abc_TtHieMan_t *	p,
		word *	pTruthInit,
		int	nVars,
		char *	pCanonPerm,
		int	fExact )

Definition at line 1318 of file dauCanon.c.

{
    int fNaive = 1;
    int pStore[17];
    //static word pTruth[1024];
    word * pTruth = pTruthInit;
    unsigned uCanonPhase = 0;
    int nOnes, nWords = Abc_TtWordNum( nVars );
    int i, k;
    assert( nVars <= 16 );
 
    // handle constant
    if ( nVars == 0 )
    {
        Abc_TtClear( pTruthInit, nWords );
        return 0;
    }
 
    //Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
 
    for ( i = 0; i < nVars; i++ )
        pCanonPerm[i] = i;
 
    // normalize polarity    
    nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
    if ( nOnes > nWords * 32 )
    {
        Abc_TtNot( pTruth, nWords );
        nOnes = nWords*64 - nOnes;
        uCanonPhase |= (1 << nVars);
    }
    // check cache
    if (Abc_TtHieRetrieveOrInsert(p, 0, pTruth, pTruthInit) > 0) return 0;
 
    // normalize phase
    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
    pStore[nVars] = nOnes;
    for ( i = 0; i < nVars; i++ )
    {
        if ( pStore[i] >= nOnes - pStore[i] )
            continue;
        Abc_TtFlip( pTruth, nWords, i );
        uCanonPhase |= (1 << i);
        pStore[i] = nOnes - pStore[i]; 
    }
    // check cache
    if (Abc_TtHieRetrieveOrInsert(p, 1, pTruth, pTruthInit) > 0) return 0;
 
    // normalize permutation
    {
        int k, BestK;
        for ( i = 0; i < nVars - 1; i++ )
        {
            BestK = i + 1;
            for ( k = i + 2; k < nVars; k++ )
                if ( pStore[BestK] > pStore[k] )
                    BestK = k;
            if ( pStore[i] <= pStore[BestK] )
                continue;
            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
            ABC_SWAP( int, pStore[i], pStore[BestK] );
            if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
            {
                uCanonPhase ^= (1 << i);
                uCanonPhase ^= (1 << BestK);
            }
            Abc_TtSwapVars( pTruth, nVars, i, BestK );
        }
    }
    // check cache
    if (Abc_TtHieRetrieveOrInsert(p, 2, pTruth, pTruthInit) > 0) return 0;
 
    // iterate TT permutations for tied variables
    for ( k = 0; k < 5; k++ )
    {
        int fChanges = 0;
        for ( i = nVars - 2; i >= 0; i-- )
            if ( pStore[i] == pStore[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
        fChanges = 0;
        for ( i = 1; i < nVars - 1; i++ )
            if ( pStore[i] == pStore[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
    }
    // check cache
    if (Abc_TtHieRetrieveOrInsert(p, 3, pTruth, pTruthInit) > 0) return 0;
 
    // perform exact NPN using groups
    if ( fExact ) {
        extern void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput);
        word pAuxWord[1024], pAuxWord1[1024];
        int pGroups[16];
        int nGroups = 0;
        permInfo * pis[17];
        // get groups
        pGroups[0] = 0;
        for (i = 0; i < nVars - 1; i++) {
            if (pStore[i] == pStore[i + 1]) {
                pGroups[nGroups]++;
            } else {
                pGroups[nGroups]++;
                nGroups++;
                pGroups[nGroups] = 0;
            }
        }
        pGroups[nGroups]++;
        nGroups++;
 
        // compute permInfo from 0 to nVars  (incl.)
        for (i = 0; i <= nVars; i++) {
            pis[i] = setPermInfoPtr(i);
        }
 
        // do the exact matching
        if (nOnes == nWords * 32) /* balanced output */
            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 1, 1);
        else if (pStore[0] != pStore[1] && pStore[0] == (nOnes - pStore[0])) /* balanced singleton input */
            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 1);
        else
            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 0);
 
        // cleanup
        for (i = 0; i <= nVars; i++) {
            freePermInfoPtr(pis[i]);
        }
    }
    // update cache
    Abc_TtHieRetrieveOrInsert(p, 4, pTruth, pTruthInit);
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCanonicizePerm()

unsigned Abc_TtCanonicizePerm	(	word *	pTruth,
		int	nVars,
		char *	pCanonPerm )

Definition at line 1085 of file dauCanon.c.

{
    int pStoreIn[17];
    unsigned uCanonPhase;
    int i, k, nWords = Abc_TtWordNum( nVars );
    int fNaive = 1;
 
#ifdef CANON_VERIFY
    char pCanonPermCopy[16];
    static word pCopy1[1024];
    static word pCopy2[1024];
    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
#endif
 
    assert( nVars <= 16 );
    for ( i = 0; i < nVars; i++ )
        pCanonPerm[i] = i;
 
    uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 1 );
    for ( k = 0; k < 5; k++ )
    {
        int fChanges = 0;
        for ( i = nVars - 2; i >= 0; i-- )
            if ( pStoreIn[i] == pStoreIn[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
        fChanges = 0;
        for ( i = 1; i < nVars - 1; i++ )
            if ( pStoreIn[i] == pStoreIn[i+1] )
                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
        if ( !fChanges )
            break;
    }
 
#ifdef CANON_VERIFY
    Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
    memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
    Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
    if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
        printf( "Canonical form verification failed!\n" );
#endif
 
    assert( uCanonPhase == 0 );
    return uCanonPhase;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCanonicizePhase()

unsigned Abc_TtCanonicizePhase	(	word *	pTruth,
		int	nVars )

Definition at line 1187 of file dauCanon.c.

{
    unsigned uCanonPhase = 0;
    int v, nWords = Abc_TtWordNum( nVars );
//    static int Counter = 0;
//    Counter++;
 
#ifdef CANON_VERIFY
    static word pCopy1[1024];
    static word pCopy2[1024];
    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
#endif
 
    if ( (pTruth[nWords-1] >> 63) & 1 )
    {
        Abc_TtNot( pTruth, nWords );
        uCanonPhase ^= (1 << nVars);
    }
 
//    while ( 1 )
//    {
//        unsigned uCanonPhase2 = uCanonPhase;
        for ( v = nVars - 1; v >= 6; v-- )
            if ( Abc_TtCanonicizePhaseVar6( pTruth, nVars, v ) == 1 )
                uCanonPhase ^= 1 << v;
        for ( ; v >= 0; v-- )
            if ( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) == 1 )
                uCanonPhase ^= 1 << v;
//        if ( uCanonPhase2 == uCanonPhase )
//            break;
//    }
 
//    for ( v = 5; v >= 0; v-- )
//        assert( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) != 1 );
 
#ifdef CANON_VERIFY
    Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
    Abc_TtImplementNpnConfig( pCopy2, nVars, NULL, uCanonPhase );
    if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
        printf( "Canonical form verification failed!\n" );
#endif
    return uCanonPhase;
}

Here is the caller graph for this function:

Abc_TtCanonicizeWrap()

unsigned Abc_TtCanonicizeWrap	(	TtCanonicizeFunc	func,
		Abc_TtHieMan_t *	p,
		word *	pTruth,
		int	nVars,
		char *	pCanonPerm,
		int	flag )

Definition at line 1530 of file dauCanon.c.

{
    int nWords = Abc_TtWordNum(nVars);
    unsigned uCanonPhase1, uCanonPhase2;
    char pCanonPerm2[16];
    static word pTruth2[1024];
 
    Abc_TtNormalizeSmallTruth(pTruth, nVars);
    if (Abc_TtCountOnesInTruth(pTruth, nVars) != nWords * 32)
        return func(p, pTruth, nVars, pCanonPerm, flag);
    Abc_TtCopy(pTruth2, pTruth, nWords, 1);
    uCanonPhase1 = func(p, pTruth, nVars, pCanonPerm, flag);
    uCanonPhase2 = func(p, pTruth2, nVars, pCanonPerm2, flag);
    if (Abc_TtCompareRev(pTruth, pTruth2, nWords) <= 0)
        return uCanonPhase1;
    Abc_TtCopy(pTruth, pTruth2, nWords, 0);
    memcpy(pCanonPerm, pCanonPerm2, nVars);
    return uCanonPhase2;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCofactorPerm()

int Abc_TtCofactorPerm	(	word *	pTruth,
		int	i,
		int	nWords,
		int	fSwapOnly,
		char *	pCanonPerm,
		unsigned *	puCanonPhase,
		int	fNaive )

Definition at line 978 of file dauCanon.c.

{
    if ( fSwapOnly )
    {
        int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
        if ( Config )
        {
            if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
            {
                *puCanonPhase ^= (1 << i);
                *puCanonPhase ^= (1 << (i+1));
            }
            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
        }
        return Config;
    }
    {
        static word pCopy1[1024];
        int Config;
        Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
        Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive );
        if ( Config == 0 )
            return 0;
        if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
        {
            Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
            return 0;
        }
        // improved
        if ( Config & 1 )
            *puCanonPhase ^= (1 << i);
        if ( Config & 2 )
            *puCanonPhase ^= (1 << (i+1));
        if ( Config & 4 )
        {
            if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
            {
                *puCanonPhase ^= (1 << i);
                *puCanonPhase ^= (1 << (i+1));
            }
            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
        }
        return Config;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCofactorPermConfig()

int Abc_TtCofactorPermConfig	(	word *	pTruth,
		int	i,
		int	nWords,
		int	fSwapOnly,
		int	fNaive )

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

Synopsis [Smart evaluation.]

Description []

SideEffects []

SeeAlso []

Definition at line 880 of file dauCanon.c.

{
    if ( nWords == 1 )
        return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly );
    if ( fNaive )
        return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly );
    if ( fSwapOnly )
    {
        if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2
        {
            Abc_TtSwapAdjacent( pTruth, nWords, i );
            return 4;
        }
        return 0;
    }
    {  
        int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
        fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
        fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
        if ( fComp23 >= 0 ) // Cof2 >= Cof3 
        {
            if ( fComp01 >= 0 ) // Cof0 >= Cof1
            {
                fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
                if ( fComp13 < 0 ) // Cof1 < Cof3 
                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
                else if ( fComp13 == 0 ) // Cof1 == Cof3 
                {
                    fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
                    if ( fComp02 < 0 )
                        Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
                }
                // else   Cof1 > Cof3 -- do nothing
            }
            else // Cof0 < Cof1
            {
                fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
                if ( fComp03 < 0 ) // Cof0 < Cof3
                {
                    Abc_TtFlip( pTruth, nWords, i );
                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
                }
                else //  Cof0 >= Cof3
                {
                    if ( fComp23 == 0 ) // can flip Cof0 and Cof1
                        Abc_TtFlip( pTruth, nWords, i ), Config = 1;
                }
            }
        }
        else // Cof2 < Cof3 
        {
            if ( fComp01 >= 0 ) // Cof0 >= Cof1
            {
                fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
                if ( fComp12 > 0 ) // Cof1 > Cof2 
                    Abc_TtFlip( pTruth, nWords, i ), Config = 1;
                else if ( fComp12 == 0 ) // Cof1 == Cof2 
                {
                    Abc_TtFlip( pTruth, nWords, i );
                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
                }
                else // Cof1 < Cof2
                {
                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
                    if ( fComp01 == 0 )
                        Abc_TtFlip( pTruth, nWords, i ), Config ^= 1;
                }
            }
            else // Cof0 < Cof1
            {
                fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
                if ( fComp02 == -1 ) // Cof0 < Cof2 
                {
                    Abc_TtFlip( pTruth, nWords, i );
                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
                }
                else if ( fComp02 == 0 ) // Cof0 == Cof2
                {
                    fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
                    if ( fComp13 >= 0 ) // Cof1 >= Cof3 
                        Abc_TtFlip( pTruth, nWords, i ), Config = 1;
                    else // Cof1 < Cof3 
                    {
                        Abc_TtFlip( pTruth, nWords, i );
                        Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
                    }
                }
                else // Cof0 > Cof2
                    Abc_TtFlip( pTruth, nWords, i ), Config = 1;
            }
        }
        // perform final swap if needed
        fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
        if ( fComp12 < 0 ) // Cof1 < Cof2
            Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4;
        return Config;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCofactorPermNaive()

int Abc_TtCofactorPermNaive	(	word *	pTruth,
		int	i,
		int	nWords,
		int	fSwapOnly )

Definition at line 800 of file dauCanon.c.

{
    if ( fSwapOnly )
    {
        static word pCopy[1024];
        Abc_TtCopy( pCopy, pTruth, nWords, 0 );
        Abc_TtSwapAdjacent( pCopy, nWords, i );
        if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
        {
            Abc_TtCopy( pTruth, pCopy, nWords, 0 );
            return 4;
        }
        return 0;
    }
    {
        static word pCopy[1024];
        static word pBest[1024];
        int Config = 0;
        // save two copies
        Abc_TtCopy( pCopy, pTruth, nWords, 0 );
        Abc_TtCopy( pBest, pTruth, nWords, 0 );
        // PXY
        // 001
        Abc_TtFlip( pCopy, nWords, i );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1;
        // PXY
        // 011
        Abc_TtFlip( pCopy, nWords, i+1 );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3;
        // PXY
        // 010
        Abc_TtFlip( pCopy, nWords, i );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2;
        // PXY
        // 110
        Abc_TtSwapAdjacent( pCopy, nWords, i );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6;
        // PXY
        // 111
        Abc_TtFlip( pCopy, nWords, i+1 );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7;
        // PXY
        // 101
        Abc_TtFlip( pCopy, nWords, i );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5;
        // PXY
        // 100
        Abc_TtFlip( pCopy, nWords, i+1 );
        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4;
        // PXY
        // 000
        Abc_TtSwapAdjacent( pCopy, nWords, i );
        assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
        if ( Config == 0 )
            return 0;
        assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
        Abc_TtCopy( pTruth, pBest, nWords, 0 );
        return Config;
    }
}

Here is the caller graph for this function:

Abc_TtCofactorTest10()

void Abc_TtCofactorTest10	(	word *	pTruth,
		int	nVars,
		int	N )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 710 of file dauCanon.c.

{
    static word pCopy1[1024];
    static word pCopy2[1024];
    int nWords = Abc_TtWordNum( nVars );
    int i;
    for ( i = 0; i < nVars - 1; i++ )
    {
//        Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
        Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
        Abc_TtSwapAdjacent( pCopy1, nWords, i );
//        Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
        Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
        Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
//        Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
        assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
    }
}

Abc_TtCountOnesInCofsFast()

int Abc_TtCountOnesInCofsFast	(	word *	pTruth,
		int	nVars,
		int *	pStore )

Definition at line 565 of file dauCanon.c.

{
    memset( pStore, 0, sizeof(int) * nVars );
    assert( nVars >= 3 );
    if ( nVars <= 6 )
        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
    else
        return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
}

Here is the call graph for this function:

Abc_TtCountOnesInCofsFast6_rec()

int Abc_TtCountOnesInCofsFast6_rec	(	word	Truth,
		int	iVar,
		int	nBytes,
		int *	pStore )

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

Synopsis [Minterm counting in all cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file dauCanon.c.

{
    static int bit_count[256] = {
      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,
      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,
      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,
      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,
      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,
      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,
      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,
      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
    };
    int nMints0, nMints1;
    if ( Truth == 0 )
        return 0;
    if ( ~Truth == 0 )
    {
        int i;
        for ( i = 0; i <= iVar; i++ )
            pStore[i] += nBytes * 4;
        return nBytes * 8;
    }
    if ( nBytes == 1 )
    {
        assert( iVar == 2 );
        pStore[0] += bit_count[ Truth & 0x55 ];
        pStore[1] += bit_count[ Truth & 0x33 ];
        pStore[2] += bit_count[ Truth & 0x0F ];
        return bit_count[ Truth & 0xFF ];
    }
    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor0(Truth, iVar), iVar - 1, nBytes/2, pStore );
    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor1(Truth, iVar), iVar - 1, nBytes/2, pStore );
    pStore[iVar] += nMints0;
    return nMints0 + nMints1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCountOnesInCofsFast_rec()

int Abc_TtCountOnesInCofsFast_rec	(	word *	pTruth,
		int	iVar,
		int	nWords,
		int *	pStore )

Definition at line 535 of file dauCanon.c.

{
    int nMints0, nMints1;
    if ( nWords == 1 )
    {
        assert( iVar == 5 );
        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
    }
    assert( nWords > 1 );
    assert( iVar > 5 );
    if ( pTruth[0] & 1 )
    {
        if ( Abc_TtIsConst1( pTruth, nWords ) )
        {
            int i;
            for ( i = 0; i <= iVar; i++ )
                pStore[i] += nWords * 32;
            return nWords * 64;
        }
    }
    else 
    {
        if ( Abc_TtIsConst0( pTruth, nWords ) )
            return 0;
    }
    nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth,            iVar - 1, nWords/2, pStore );
    nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
    pStore[iVar] += nMints0;
    return nMints0 + nMints1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_TtCountOnesInCofsSimple()

int Abc_TtCountOnesInCofsSimple	(	word *	pTruth,
		int	nVars,
		int *	pStore )

Definition at line 370 of file dauCanon.c.

{
    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
    return Abc_TtCountOnesInTruth( pTruth, nVars );
}

Here is the caller graph for this function:

Abc_TtHieManStart()

Abc_TtHieMan_t * Abc_TtHieManStart	(	int	nVars,
		int	nLevels )

Definition at line 1255 of file dauCanon.c.

{
    Abc_TtHieMan_t * p = NULL;
    int i;
    if (nLevels > TT_MAX_LEVELS) return p;
    p = ABC_CALLOC(Abc_TtHieMan_t, 1);
    p->nLastLevel = nLevels - 1;
    p->nWords = Abc_TtWordNum(nVars);
    for (i = 0; i < nLevels; i++)
    {
        p->vTtMem[i] = Vec_MemAlloc(p->nWords, 12);
        Vec_MemHashAlloc(p->vTtMem[i], 10000);
        p->vRepres[i] = Vec_IntAlloc(1);
    }
    p->vPhase = Vec_IntAlloc(2500);
    return p;
}

Here is the caller graph for this function:

Abc_TtHieManStop()

void Abc_TtHieManStop

(

Abc_TtHieMan_t *

p

)

Definition at line 1273 of file dauCanon.c.

{
    int i;
    for (i = 0; i <= p->nLastLevel; i++)
    {
        Vec_MemHashFree(p->vTtMem[i]);
        Vec_MemFreeP(&p->vTtMem[i]);
        Vec_IntFree(p->vRepres[i]);
    }
    Vec_IntFree( p->vPhase );
    ABC_FREE(p);
}

Here is the caller graph for this function:

Abc_TtHieRetrieveOrInsert()

int Abc_TtHieRetrieveOrInsert	(	Abc_TtHieMan_t *	p,
		int	level,
		word *	pTruth,
		word *	pResult )

Definition at line 1286 of file dauCanon.c.

{
    int i, iSpot, truthId;
    word * pRepTruth;
    if (!p) return -1;
    if (level < 0) level += p->nLastLevel + 1;
    if (level < 0 || level > p->nLastLevel) return -1;
    iSpot = *Vec_MemHashLookup(p->vTtMem[level], pTruth);
    if (iSpot == -1) {
        p->vTruthId[level] = Vec_MemHashInsert(p->vTtMem[level], pTruth);
        if (level < p->nLastLevel) return 0;
        iSpot = p->vTruthId[level];
    }
    // return the class representative
    if (level < p->nLastLevel)
        truthId = Vec_IntEntry(p->vRepres[level], iSpot);
    else
        truthId = iSpot;
    for (i = 0; i < level; i++)
        Vec_IntSetEntry(p->vRepres[i], p->vTruthId[i], truthId);
 
    pRepTruth = Vec_MemReadEntry(p->vTtMem[p->nLastLevel], truthId);
    if (level < p->nLastLevel) {
        Abc_TtCopy(pResult, pRepTruth, p->nWords, 0);
        return 1;
    }
    assert(Abc_TtEqual(pTruth, pRepTruth, p->nWords));
    if (pTruth != pResult)
        Abc_TtCopy(pResult, pRepTruth, p->nWords, 0);
    return 0;
}

Here is the caller graph for this function:

Abc_TtNormalizeSmallTruth()

void Abc_TtNormalizeSmallTruth	(	word *	pTruth,
		int	nVars )

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

Synopsis [Minterm counting in all cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 300 of file dauCanon.c.

{
    if (nVars < 6) {
        int shift, bits = (1 << nVars);
        word base = *pTruth = *pTruth & ((((word)1) << bits) - 1);
        for (shift = bits; shift < 64; shift += bits)
            *pTruth |= base << shift;
    }
}

Here is the caller graph for this function:

Abc_TtScc()

int Abc_TtScc	(	word *	pTruth,
		int	nVars )

Definition at line 393 of file dauCanon.c.

{
    int k, nWords = Abc_TtWordNum(nVars);
    int sum = 0;
    Abc_TtNormalizeSmallTruth(pTruth, nVars);
    for (k = 0; k < nWords; k++)
        sum += Abc_TtScc6(pTruth[k], Abc_TtBitCount16(k));
    return sum;
}

Here is the call graph for this function:

Variable Documentation

gpVerCopy

word gpVerCopy[1024]

Definition at line 1550 of file dauCanon.c.