dau.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "misc/vec/vec.h"

Include dependency graph for dau.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros
#define	DAU_MAX_VAR   12
	INCLUDES ///.
#define	DAU_MAX_STR   2000
#define	DAU_MAX_WORD   (1<<(DAU_MAX_VAR-6))

Typedefs
typedef struct Dss_Man_t_	Dss_Man_t
typedef struct Abc_TtHieMan_t_	Abc_TtHieMan_t
typedef unsigned(*	TtCanonicizeFunc) (Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)

Enumerations
enum	Dau_DsdType_t {   DAU_DSD_NONE = 0 , DAU_DSD_CONST0 , DAU_DSD_VAR , DAU_DSD_AND ,   DAU_DSD_XOR , DAU_DSD_MUX , DAU_DSD_PRIME }
	BASIC TYPES ///. More...

Functions
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)
int	Abc_TtCountOnesInCofsSimple (word *pTruth, int nVars, int *pStore)
unsigned	Abc_TtCanonicizeHie (Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int fExact)
Abc_TtHieMan_t *	Abc_TtHieManStart (int nVars, int nLevels)
void	Abc_TtHieManStop (Abc_TtHieMan_t *p)
unsigned	Abc_TtCanonicizeWrap (TtCanonicizeFunc func, Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)
unsigned	Abc_TtCanonicizeAda (Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int iThres)
int	Abc_TtCountOnesInCofsQuick (word *pTruth, int nVars, int *pStore)
int *	Dau_DsdComputeMatches (char *p)
int	Dau_DsdDecompose (word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
int	Dau_DsdDecomposeLevel (word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes, int *pVarLevels)
void	Dau_DsdPrintFromTruthFile (FILE *pFile, word *pTruth, int nVarsInit)
void	Dau_DsdPrintFromTruth (word *pTruth, int nVarsInit)
word *	Dau_DsdToTruth (char *p, int nVars)
word	Dau_Dsd6ToTruth (char *p)
void	Dau_DsdNormalize (char *p)
int	Dau_DsdCountAnds (char *pDsd)
void	Dau_DsdTruthCompose_rec (word *pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word *pRes, int nVars, int nWordsR)
int	Dau_DsdCheck1Step (void *p, word *pTruth, int nVarsInit, int *pVarLevels)
int	Dsm_ManTruthToGia (void *p, word *pTruth, Vec_Int_t *vLeaves, Vec_Int_t *vCover)
void *	Dsm_ManDeriveGia (void *p, int fUseMuxes)
void	Dau_DsdRemoveBraces (char *pDsd, int *pMatches)
char *	Dau_DsdMerge (char *pDsd0i, int *pPerm0, char *pDsd1i, int *pPerm1, int fCompl0, int fCompl1, int nVars)
	DECLARATIONS ///.
Vec_Int_t *	Dau_DecFindSets_int (word *pInit, int nVars, int *pSched[16])
Vec_Int_t *	Dau_DecFindSets (word *pInit, int nVars)
void	Dau_DecSortSet (unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
void	Dau_DecPrintSets (Vec_Int_t *vSets, int nVars)
void	Dau_DecPrintSet (unsigned set, int nVars, int fNewLine)
Dss_Man_t *	Dss_ManAlloc (int nVars, int nNonDecLimit)
void	Dss_ManFree (Dss_Man_t *p)
int	Dss_ManMerge (Dss_Man_t *p, int *iDsd, int *nFans, int **pFans, unsigned uSharedMask, int nKLutSize, unsigned char *pPerm, word *pTruth)
void	Dss_ManPrint (char *pFileName, Dss_Man_t *p)

Macro Definition Documentation

DAU_MAX_STR

#define DAU_MAX_STR   2000

Definition at line 43 of file dau.h.

DAU_MAX_VAR

#define DAU_MAX_VAR   12

INCLUDES ///.

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

FileName [dau.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

dau.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS ///

Definition at line 42 of file dau.h.

DAU_MAX_WORD

#define DAU_MAX_WORD   (1<<(DAU_MAX_VAR-6))

Definition at line 44 of file dau.h.

Typedef Documentation

Abc_TtHieMan_t

typedef struct Abc_TtHieMan_t_ Abc_TtHieMan_t

Definition at line 62 of file dau.h.

Dss_Man_t

typedef struct Dss_Man_t_ Dss_Man_t

Definition at line 61 of file dau.h.

TtCanonicizeFunc

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

Definition at line 63 of file dau.h.

Enumeration Type Documentation

Dau_DsdType_t

enum Dau_DsdType_t

BASIC TYPES ///.

Enumerator
DAU_DSD_NONE
DAU_DSD_CONST0
DAU_DSD_VAR
DAU_DSD_AND
DAU_DSD_XOR
DAU_DSD_MUX
DAU_DSD_PRIME

Definition at line 51 of file dau.h.

             { 
    DAU_DSD_NONE = 0,      // 0:  unknown
    DAU_DSD_CONST0,        // 1:  constant
    DAU_DSD_VAR,           // 2:  variable
    DAU_DSD_AND,           // 3:  AND
    DAU_DSD_XOR,           // 4:  XOR
    DAU_DSD_MUX,           // 5:  MUX
    DAU_DSD_PRIME          // 6:  PRIME
} Dau_DsdType_t;

Function Documentation

Abc_TtCanonicize()

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

extern

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 )

extern

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_TtCanonicizeHie()

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

extern

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 )

extern

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 )

extern

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 )

extern

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_TtCountOnesInCofsQuick()

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

extern

Definition at line 376 of file dauCount.c.

{
    if ( nVars == 0 )
        return (int)(pTruth[0] & 1);
    memset( pStore, 0, sizeof(int)*nVars );
    return Abc_TtCountOnesInCofsQuick_rec( pTruth, nVars, pStore );
}

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 )

extern

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 )

extern

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 )

extern

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:

Dau_DecFindSets()

Vec_Int_t * Dau_DecFindSets ( word * pInit, int nVars )

extern

Definition at line 516 of file dauNonDsd.c.

{
    Vec_Int_t * vSets;
    int v, * pSched[16] = {NULL};
    for ( v = 2; v < nVars; v++ )
        pSched[v] = Extra_GreyCodeSchedule( v );
    vSets = Dau_DecFindSets_int( pInit, nVars, pSched );
    for ( v = 2; v < nVars; v++ )
        ABC_FREE( pSched[v] );
    return vSets;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecFindSets_int()

Vec_Int_t * Dau_DecFindSets_int ( word * pInit, int nVars, int * pSched[16] )

extern

Definition at line 462 of file dauNonDsd.c.

{
    Vec_Int_t * vSets = Vec_IntAlloc( 32 );
    int V2P[16], P2V[16], pVarsB[16];
    int Limit = (1 << nVars);
    int c, v, sizeB, sizeS, maskB, maskS;
    unsigned setMixed;
    word p[1<<10]; 
    memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
    for ( v = 0; v < nVars; v++ )
        assert( Abc_TtHasVar( p, nVars, v ) );
    // initialize permutation
    for ( v = 0; v < nVars; v++ )
        V2P[v] = P2V[v] = v;
    // iterate through bound sets of each size in increasing order
    for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size
    for ( maskB = 0; maskB < Limit; maskB++ ) // bound set
    if ( Abc_TtBitCount16(maskB) == sizeB )
    {
        // permute variables to have bound set on top
        Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB );
        // collect bound set vars on levels nVars-sizeB to nVars-1
        for ( c = 0; c < sizeB; c++ )
            pVarsB[c] = P2V[nVars-sizeB+c];
        // check disjoint
//        if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) )
        if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, pSched[sizeB], NULL, NULL) )
        {
            Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) );
            continue;
        }
        if ( sizeB == 2 )
            continue;
        // iterate through shared sets of each size in the increasing order
        for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ )   // shared set size
        if ( sizeS <= 3 )
//        sizeS = 1; 
        for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set
        if ( Abc_TtBitCount16(maskS) == sizeS )
        {
            setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS );
//            printf( "Considering %10d ", setMixed );
//            Dau_DecPrintSet( setMixed, nVars );
            // check if it exists
            if ( Dau_DecSetIsContained(vSets, setMixed) )
                continue;
            // check if it can be added
//            if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) )
            if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, pSched[sizeB], NULL, NULL) )
                Vec_IntPush( vSets, setMixed );
        }
    }
    return vSets;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecPrintSet()

void Dau_DecPrintSet ( unsigned set, int nVars, int fNewLine )

extern

Definition at line 390 of file dauNonDsd.c.

{
    int v, Counter = 0;
    int nUnique = 0, nShared = 0, nFree = 0;
    Dau_DecSortSet( set, nVars, &nUnique, &nShared, &nFree );
    printf( "S =%2d  D =%2d  C =%2d   ", nShared, nUnique+nShared, nShared+nFree+1 );
 
    printf( "x=" );
    for ( v = 0; v < nVars; v++ )
    {
        int Value = ((set >> (v << 1)) & 3);
        if ( Value == 1 )
            printf( "%c", 'a' + v ), Counter++;
        else if ( Value == 3 )
            printf( "%c", 'A' + v ), Counter++;
        else assert( Value == 0 );
    }
    printf( " y=x" );
    for ( v = 0; v < nVars; v++ )
    {
        int Value = ((set >> (v << 1)) & 3);
        if ( Value == 0 )
            printf( "%c", 'a' + v ), Counter++;
        else if ( Value == 3 )
            printf( "%c", 'A' + v ), Counter++;
    }
    for ( ; Counter < 15; Counter++ )
        printf( " " );
    if ( fNewLine )
        printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecPrintSets()

void Dau_DecPrintSets ( Vec_Int_t * vSets, int nVars )

extern

Definition at line 434 of file dauNonDsd.c.

{
    int i, Entry;
    printf( "The %d-variable set family contains %d sets:\n", nVars, Vec_IntSize(vSets) );
    Vec_IntForEachEntry( vSets, Entry, i )
        Dau_DecPrintSet( (unsigned)Entry, nVars, 1 );
    printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecSortSet()

void Dau_DecSortSet ( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree )

extern

Definition at line 371 of file dauNonDsd.c.

{
    int v;
    int nUnique = 0, nShared = 0, nFree = 0;
    for ( v = 0; v < nVars; v++ )
    {
        int Value = ((set >> (v << 1)) & 3);
        if ( Value == 1 )
            nUnique++;
        else if ( Value == 3 )
            nShared++;
        else if ( Value == 0 )
            nFree++;
        else assert( 0 );
    }
    *pnUnique = nUnique;
    *pnShared = nShared;
    *pnFree   = nFree;
}

Here is the caller graph for this function:

Dau_Dsd6ToTruth()

word Dau_Dsd6ToTruth ( char * p )

extern

Definition at line 445 of file dauDsd.c.

{
    word Res;
    if ( *p == '0' && *(p+1) == 0 )
        Res = 0;
    else if ( *p == '1' && *(p+1) == 0 )
        Res = ~(word)0;
    else
        Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p), s_Truths6 );
    assert( *++p == 0 );
    return Res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdCheck1Step()

int Dau_DsdCheck1Step ( void * p, word * pTruth, int nVarsInit, int * pVarLevels )

extern

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

Synopsis [Find the best cofactoring variable.]

Description [Return -2 if non-DSD; -1 if full DSD; otherwise, returns cofactoring variables i (i >= 0).]

SideEffects []

SeeAlso []

Definition at line 893 of file dauDsd.c.

{
    word pCofTemp[DAU_MAX_WORD];
    int pVarPrios[DAU_MAX_VAR];
    int nWords = Abc_TtWordNum(nVarsInit);
    int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
    int i, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
    nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL );
    if ( nSizeNonDec == 0 )
        return -1;
    assert( nSizeNonDec > 0 );
    // find variable priority
    for ( i = 0; i < nVarsInit; i++ )
        pVarPrios[i] = i;
    if ( pVarLevels )
    {
        extern int Dau_DsdLevelVar( void * pMan, int iVar );
        int pVarLevels[DAU_MAX_VAR];
        for ( i = 0; i < nVarsInit; i++ )
            pVarLevels[i] = -Dau_DsdLevelVar( p, i );
//        for ( i = 0; i < nVarsInit; i++ )
//            printf( "%d ", -pVarLevels[i] );
//        printf( "\n" );
        Vec_IntSelectSortCost2( pVarPrios, nVarsInit, pVarLevels );
//        for ( i = 0; i < nVarsInit; i++ )
//            printf( "%d ", pVarPrios[i] );
//        printf( "\n\n" );
    }
    for ( i = 0; i < nVarsInit; i++ )
    {
        assert( pVarPrios[i] >= 0 && pVarPrios[i] < nVarsInit );
        // try first cofactor
        Abc_TtCofactor0p( pCofTemp, pTruth, nWords, pVarPrios[i] );
        nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
        nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
        // try second cofactor
        Abc_TtCofactor1p( pCofTemp, pTruth, nWords, pVarPrios[i] );
        nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
        nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
        // compare cofactors
        if ( nSizeNonDec0 || nSizeNonDec1 )
            continue;
        if ( nSumCofsBest > nSumCofs )
        {
            vBest = pVarPrios[i];
            nSumCofsBest = nSumCofs;
        }
    }
    return vBest;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdComputeMatches()

int * Dau_DsdComputeMatches ( char * p )

extern

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

Synopsis [DSD formula manipulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file dauDsd.c.

{
    static int pMatches[DAU_MAX_STR];
    int pNested[DAU_MAX_VAR];
    int v, nNested = 0;
    for ( v = 0; p[v]; v++ )
    {
        pMatches[v] = 0;
        if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
            pNested[nNested++] = v;
        else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
            pMatches[pNested[--nNested]] = v;
        assert( nNested < DAU_MAX_VAR );
    }
    assert( nNested == 0 );
    return pMatches;
}

Here is the caller graph for this function:

Dau_DsdCountAnds()

int Dau_DsdCountAnds ( char * pDsd )

extern

Definition at line 316 of file dauDsd.c.

{
    if ( pDsd[1] == 0 )
        return 0;
    return Dau_DsdCountAnds_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdDecompose()

int Dau_DsdDecompose ( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes )

extern

Definition at line 1912 of file dauDsd.c.

{
    Dau_Dsd_t P, * p = &P;
    p->fSplitPrime = fSplitPrime;
    p->fWriteTruth = fWriteTruth;
    p->pVarLevels  = NULL;
    p->nSizeNonDec = 0;
    if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
        { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
    else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
        { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
    else 
    {
        int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
        Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
        if ( pRes )
            strcpy( pRes, p->pOutput );
        assert( fSplitPrime || Status != 1 );
        if ( fSplitPrime && Status == 2 )
            return -1;
    }
//    assert( p->nSizeNonDec == 0 );
    return p->nSizeNonDec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdDecomposeLevel()

int Dau_DsdDecomposeLevel ( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes, int * pVarLevels )

extern

Definition at line 1936 of file dauDsd.c.

{
    Dau_Dsd_t P, * p = &P;
    p->fSplitPrime = fSplitPrime;
    p->fWriteTruth = fWriteTruth;
    p->pVarLevels  = pVarLevels;
    p->nSizeNonDec = 0;
    if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
        { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
    else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
        { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
    else 
    {
        int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
        Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
        if ( pRes )
            strcpy( pRes, p->pOutput );
        assert( fSplitPrime || Status != 1 );
        if ( fSplitPrime && Status == 2 )
            return -1;
    }
//    assert( p->nSizeNonDec == 0 );
    return p->nSizeNonDec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdMerge()

char * Dau_DsdMerge ( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars )

extern

DECLARATIONS ///.

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

Synopsis [Performs merging of two DSD formulas.]

Description []

SideEffects []

SeeAlso []

Definition at line 587 of file dauMerge.c.

{
    int fVerbose = 0;
    int fCheck = 0;
    static int Counter = 0;
    static char pRes[2*DAU_MAX_STR+10];
    char pDsd0[DAU_MAX_STR];
    char pDsd1[DAU_MAX_STR];
    int pMatches0[DAU_MAX_STR];
    int pMatches1[DAU_MAX_STR];
    int pVarPres[DAU_MAX_VAR];
    int pOld2New[DAU_MAX_VAR];
    int pNew2Old[DAU_MAX_VAR];
    int pStatus0[DAU_MAX_STR];
    int pStatus1[DAU_MAX_STR];
    int pMatches[DAU_MAX_STR];
    int nVarsShared, nVarsTotal;
    Dau_Sto_t S, * pS = &S;
    word * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
    word pParts[3][DAU_MAX_WORD];
    int Status;
    abctime clk = Abc_Clock();
    Counter++;
    // create local copies
    Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
    Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 );
if ( fVerbose )
printf( "\nAfter copying:\n" );
if ( fVerbose )
printf( "%s\n", pDsd0 );
if ( fVerbose )
printf( "%s\n", pDsd1 );
    // handle constants
    if ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) )
    {
        if ( Dau_DsdIsConst0(pDsd0) )
            strcpy( pRes, pDsd0 );
        else if ( Dau_DsdIsConst1(pDsd0) )
            strcpy( pRes, pDsd1 );
        else if ( Dau_DsdIsConst0(pDsd1) )
            strcpy( pRes, pDsd1 );
        else if ( Dau_DsdIsConst1(pDsd1) )
            strcpy( pRes, pDsd0 );
        else assert( 0 );
        return pRes;
    }
 
    // compute matches
    Dau_DsdMergeMatches( pDsd0, pMatches0 );
    Dau_DsdMergeMatches( pDsd1, pMatches1 );
    // implement permutation
    Dau_DsdMergeReplace( pDsd0, pMatches0, pPerm0 );
    Dau_DsdMergeReplace( pDsd1, pMatches1, pPerm1 );
if ( fVerbose )
printf( "After replacement:\n" );
if ( fVerbose )
printf( "%s\n", pDsd0 );
if ( fVerbose )
printf( "%s\n", pDsd1 );
 
 
    if ( fCheck )
    {
        pt0 = Dau_DsdToTruth( pDsd0, nVars );
        Abc_TtCopy( pParts[0], pt0, Abc_TtWordNum(nVars), 0 );
    }
    if ( fCheck )
    {
        pt1 = Dau_DsdToTruth( pDsd1, nVars );
        Abc_TtCopy( pParts[1], pt1, Abc_TtWordNum(nVars), 0 );
        Abc_TtAnd( pParts[2], pParts[0], pParts[1], Abc_TtWordNum(nVars), 0 );
    }
 
    // find shared varaiables
    nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
    if ( nVarsShared == 0 )
    {
        sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
if ( fVerbose )
printf( "Disjoint:\n" );
if ( fVerbose )
printf( "%s\n", pRes );
 
        Dau_DsdMergeMatches( pRes, pMatches );
        Dau_DsdRemoveBraces( pRes, pMatches );
        Dau_DsdNormalize( pRes );
if ( fVerbose )
printf( "Normalized:\n" );
if ( fVerbose )
printf( "%s\n", pRes );
 
        s_TimeComp[0] += Abc_Clock() - clk;
        return pRes;
    }
s_TimeComp[3] += Abc_Clock() - clk;
    // create variable mapping
    nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
    // perform variable replacement
    Dau_DsdMergeReplace( pDsd0, pMatches0, pOld2New );
    Dau_DsdMergeReplace( pDsd1, pMatches1, pOld2New );
    // find uniqueness status
    Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 );
    Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 );
if ( fVerbose )
printf( "Individual status:\n" );
if ( fVerbose )
Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
if ( fVerbose )
Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
    // prepare storage
    Dau_DsdMergeStoreClean( pS, nVarsShared );
    // perform substitutions
    Dau_DsdMergeStoreCleanOutput( pS );
    Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 );
    strcpy( pDsd0, pS->pOutput );
if ( fVerbose )
printf( "Substitutions:\n" );
if ( fVerbose )
printf( "%s\n", pDsd0 );
 
    // perform substitutions
    Dau_DsdMergeStoreCleanOutput( pS );
    Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 );
    strcpy( pDsd1, pS->pOutput );
if ( fVerbose )
printf( "%s\n", pDsd1 );
if ( fVerbose )
Dau_DsdMergeStorePrintDefs( pS );
 
    // create new function
//    assert( nVarsTotal <= 6 );
    sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
    pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
    Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput );
//printf( "%d ", Status );
    if ( Status == -1 ) // did not find 1-step DSD
        return NULL;
//    if ( Status > 6 ) // non-DSD part is too large
//        return NULL;
    if ( Dau_DsdIsConst(pS->pOutput) )
    {
        strcpy( pRes, pS->pOutput );
        return pRes;
    }
if ( fVerbose )
printf( "Decomposition:\n" );
if ( fVerbose )
printf( "%s\n", pS->pOutput );
    // substitute definitions
    Dau_DsdMergeMatches( pS->pOutput, pMatches );
    Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS, pRes, nVarsShared );
if ( fVerbose )
printf( "Inlining:\n" );
if ( fVerbose )
printf( "%s\n", pRes );
    // perform variable replacement
    Dau_DsdMergeMatches( pRes, pMatches );
    Dau_DsdMergeReplace( pRes, pMatches, pNew2Old );
    Dau_DsdRemoveBraces( pRes, pMatches );
if ( fVerbose )
printf( "Replaced:\n" );
if ( fVerbose )
printf( "%s\n", pRes );
    Dau_DsdNormalize( pRes );
if ( fVerbose )
printf( "Normalized:\n" );
if ( fVerbose )
printf( "%s\n", pRes );
 
    if ( fCheck )
    {
        pt = Dau_DsdToTruth( pRes, nVars );
        if ( !Abc_TtEqual( pParts[2], pt, Abc_TtWordNum(nVars) ) )
            printf( "Dau_DsdMerge(): Verification failed!\n" );
    }
 
    if ( Status == 0 )
        s_TimeComp[1] += Abc_Clock() - clk;
    else
        s_TimeComp[2] += Abc_Clock() - clk;
    return pRes;
}

Here is the caller graph for this function:

Dau_DsdNormalize()

void Dau_DsdNormalize ( char * p )

extern

Definition at line 260 of file dauDsd.c.

{
    if ( pDsd[1] != 0 )
        Dau_DsdNormalize_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdPrintFromTruth()

void Dau_DsdPrintFromTruth ( word * pTruth, int nVarsInit )

extern

Definition at line 1968 of file dauDsd.c.

{
    char pRes[DAU_MAX_STR];
    word pTemp[DAU_MAX_WORD];
    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
    fprintf( stdout, "%s\n", pRes );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdPrintFromTruthFile()

void Dau_DsdPrintFromTruthFile ( FILE * pFile, word * pTruth, int nVarsInit )

extern

Definition at line 1960 of file dauDsd.c.

{
    char pRes[DAU_MAX_STR];
    word pTemp[DAU_MAX_WORD];
    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
    fprintf( pFile, "%s\n", pRes );
}

Here is the call graph for this function:

Dau_DsdRemoveBraces()

void Dau_DsdRemoveBraces ( char * pDsd, int * pMatches )

extern

Definition at line 554 of file dauMerge.c.

{
    char * q, * p = pDsd;
    if ( pDsd[1] == 0 )
        return;
    Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches );
    for ( q = p; *p; p++ )
        if ( *p != ' ' )
        {
            if ( *p == '!' && p != q && *(q-1) == '!' )
            {
                q--;
                continue;
            }
            *q++ = *p;
        }
    *q = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdToTruth()

word * Dau_DsdToTruth ( char * p, int nVars )

extern

Definition at line 609 of file dauDsd.c.

{
    int nWords = Abc_TtWordNum( nVars );
    word ** pTtElems = Dau_DsdTtElems();
    word * pRes = pTtElems[DAU_MAX_VAR];
    assert( nVars <= DAU_MAX_VAR );
    if ( Dau_DsdIsConst0(p) )
        Abc_TtConst0( pRes, nWords );
    else if ( Dau_DsdIsConst1(p) )
        Abc_TtConst1( pRes, nWords );
    else
        Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p), pTtElems, pRes, nVars );
    assert( *++p == 0 );
    return pRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DsdTruthCompose_rec()

void Dau_DsdTruthCompose_rec ( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )

extern

Definition at line 501 of file dauDsd.c.

{
    int nWordsF;
    if ( nVars <= 6 )
    {
        Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars, nWordsR );
        return;
    }
    nWordsF = Abc_TtWordNum( nVars );
    assert( nWordsF > 1 );
    if ( Abc_TtIsConst0(pFunc, nWordsF) )
    {
        Abc_TtConst0( pRes, nWordsR );
        return;
    }
    if ( Abc_TtIsConst1(pFunc, nWordsF) )
    {
        Abc_TtConst1( pRes, nWordsR );
        return;
    }
    if ( !Abc_TtHasVar( pFunc, nVars, nVars-1 ) )
    {
        Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1, nWordsR );
        return;
    }
    {
        word pTtTemp[2][DAU_MAX_WORD];
        nVars--;
        Dau_DsdTruthCompose_rec( pFunc,             pFanins, pTtTemp[0], nVars, nWordsR );
        Dau_DsdTruthCompose_rec( pFunc + nWordsF/2, pFanins, pTtTemp[1], nVars, nWordsR );
        Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
        return;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dsm_ManDeriveGia()

void * Dsm_ManDeriveGia ( void * pGia, int fUseMuxes )

extern

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

Synopsis [Performs structural hashing on the LUT functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file dauGia.c.

{
    Gia_Man_t * p = (Gia_Man_t *)pGia;
    Gia_Man_t * pNew, * pTemp;
    Vec_Int_t * vCover, * vLeaves;
    Gia_Obj_t * pObj; 
    int k, i, iLut, iVar;
    word * pTruth;
    assert( Gia_ManHasMapping(p) );   
    // create new manager
    pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->vLevels = Vec_IntStart( 6*Gia_ManObjNum(p)/5 + 100 );
    if ( fUseMuxes )
        pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
    // map primary inputs
    Gia_ManFillValue(p);
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // iterate through nodes used in the mapping
    vLeaves = Vec_IntAlloc( 16 );
    vCover  = Vec_IntAlloc( 1 << 16 );
    Gia_ManHashStart( pNew );
    Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
    Gia_ManForEachAnd( p, pObj, iLut )
    {
        if ( Gia_ObjIsBuf(pObj) )
        {
            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
            continue;
        }
        if ( !Gia_ObjIsLut(p, iLut) )
            continue;
        // collect leaves
        Vec_IntClear( vLeaves );
        Gia_LutForEachFanin( p, iLut, iVar, k )
            Vec_IntPush( vLeaves, iVar );
        pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
        // collect incoming literals
        Vec_IntClear( vLeaves );
        Gia_LutForEachFanin( p, iLut, iVar, k )
            Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
        Gia_ManObj(p, iLut)->Value = Dsm_ManTruthToGia( pNew, pTruth, vLeaves, vCover );
    }
    Gia_ObjComputeTruthTableStop( p );
    Gia_ManForEachCo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    Vec_IntFree( vLeaves );
    Vec_IntFree( vCover );
/*
    Gia_ManForEachAnd( pNew, pObj, i )
    {
        int iLev  = Gia_ObjLevelId(pNew, i);
        int iLev0 = Gia_ObjLevelId(pNew, Gia_ObjFaninId0(pObj, i));
        int iLev1 = Gia_ObjLevelId(pNew, Gia_ObjFaninId1(pObj, i));
        assert( iLev == 1 + Abc_MaxInt(iLev0, iLev1) );
    }
*/
    // perform cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dsm_ManTruthToGia()

int Dsm_ManTruthToGia ( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )

extern

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

Synopsis [Convert TT to GIA via DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 441 of file dauGia.c.

{
    int fUseMuxes = 0;
    int fDelayBalance = 1;
    Gia_Man_t * pGia = (Gia_Man_t *)p;
    int nSizeNonDec;
    char pDsd[DAU_MAX_STR];
    word pTruthCopy[DAU_MAX_WORD];
    Abc_TtCopy( pTruthCopy, pTruth, Abc_TtWordNum(Vec_IntSize(vLeaves)), 0 );
    m_Calls++;
    assert( Vec_IntSize(vLeaves) <= DAU_DSD_MAX_VAR );
    if ( Vec_IntSize(vLeaves) == 0 )
        return (int)(pTruth[0] & 1);
    if ( Vec_IntSize(vLeaves) == 1 )
        return Abc_LitNotCond( Vec_IntEntry(vLeaves, 0), (int)(pTruth[0] & 1) );
    // collect delay information
    if ( fDelayBalance && fUseMuxes )
    {
        int i, iLit, pVarLevels[DAU_DSD_MAX_VAR];
        Vec_IntForEachEntry( vLeaves, iLit, i )
            pVarLevels[i] = Gia_ObjLevelId( pGia, Abc_Lit2Var(iLit) );
        nSizeNonDec = Dau_DsdDecomposeLevel( pTruthCopy, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd, pVarLevels );
    }
    else
        nSizeNonDec = Dau_DsdDecompose( pTruthCopy, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd );
    if ( nSizeNonDec )
        m_NonDsd++;
//    printf( "%s\n", pDsd );
    if ( fDelayBalance && pGia->vLevels )
        return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
    else
        return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dss_ManAlloc()

Dss_Man_t * Dss_ManAlloc ( int nVars, int nNonDecLimit )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 967 of file dauTree.c.

{
    Dss_Man_t * p;
    p = ABC_CALLOC( Dss_Man_t, 1 );
    p->nVars  = nVars;
    p->nNonDecLimit = nNonDecLimit;
    p->nBins  = Abc_PrimeCudd( 1000000 );
    p->pBins  = ABC_CALLOC( unsigned, p->nBins );
    p->pMem   = Mem_FlexStart();
    p->vObjs  = Vec_PtrAlloc( 10000 );
    p->vNexts = Vec_IntAlloc( 10000 );
    Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 );
    Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 )->nSupp = 1;
    p->vLeaves = Vec_IntAlloc( 32 );
    p->vCopies = Vec_IntAlloc( 32 );
    p->pTtElems = Dss_ManTtElems();
    p->pMemEnts = Mem_FlexStart();
//    Dss_ManCacheAlloc( p );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dss_ManFree()

void Dss_ManFree ( Dss_Man_t * p )

extern

Definition at line 987 of file dauTree.c.

{
    Abc_PrintTime( 1, "Time begin ", p->timeBeg );
    Abc_PrintTime( 1, "Time decomp", p->timeDec );
    Abc_PrintTime( 1, "Time lookup", p->timeLook );
    Abc_PrintTime( 1, "Time end   ", p->timeEnd );
 
//    Dss_ManCacheProfile( p );
    Dss_ManCacheFree( p );
    Mem_FlexStop( p->pMemEnts, 0 );
    Vec_IntFreeP( &p->vCopies );
    Vec_IntFreeP( &p->vLeaves );
    Vec_IntFreeP( &p->vNexts );
    Vec_PtrFreeP( &p->vObjs );
    Mem_FlexStop( p->pMem, 0 );
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dss_ManMerge()

int Dss_ManMerge ( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm, word * pTruth )

extern

Definition at line 1539 of file dauTree.c.

{
    int fVerbose = 0;
    int fCheck = 0;
    static int Counter = 0;
//    word pTtTemp[DAU_MAX_WORD];
    word * pTruthOne;
    int pPermResInt[DAU_MAX_VAR];
    Dss_Ent_t * pEnt, ** ppSpot;
    Dss_Fun_t * pFun;
    int i;
    abctime clk;
    Counter++;
    if ( DAU_MAX_VAR < nKLutSize )
    {
        printf( "Parameter DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
        return -1;
    }
    assert( iDsd[0] <= iDsd[1] );
 
if ( fVerbose )
{
Dss_ManPrintOne( stdout, p, iDsd[0], pFans[0] );
Dss_ManPrintOne( stdout, p, iDsd[1], pFans[1] );
} 
 
    // constant argument
    if ( iDsd[0] == 0 ) return 0;
    if ( iDsd[0] == 1 ) return iDsd[1];
    if ( iDsd[1] == 0 ) return 0;
    if ( iDsd[1] == 1 ) return iDsd[0];
 
    // no overlap
clk = Abc_Clock();
    assert( nFans[0] == Dss_VecLitSuppSize(p->vObjs, iDsd[0]) );
    assert( nFans[1] == Dss_VecLitSuppSize(p->vObjs, iDsd[1]) );
    assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
    // create map of shared variables
    pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
p->timeBeg += Abc_Clock() - clk;
    // check cache
    if ( p->pCache == NULL )
    {
clk = Abc_Clock();
        if ( uSharedMask == 0 )
            pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
        else
            pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
        if ( pFun == NULL )
            return -1;
        assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
        assert( (int)pFun->nFans <= nKLutSize );
p->timeDec += Abc_Clock() - clk;
    }
    else
    {
clk = Abc_Clock();
        ppSpot = Dss_ManCacheLookup( p, pEnt );
p->timeLook += Abc_Clock() - clk;
clk = Abc_Clock();
        if ( *ppSpot == NULL )
        {
            if ( uSharedMask == 0 )
                pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
            else
                pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
            if ( pFun == NULL )
                return -1;
            assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
            assert( (int)pFun->nFans <= nKLutSize );
            // create cache entry
            *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
        }
        pFun = (*ppSpot)->pFunc;
p->timeDec += Abc_Clock() - clk;
    }
 
clk = Abc_Clock();
    for ( i = 0; i < (int)pFun->nFans; i++ )
        if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
            pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
        else
            pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] );
    // perform support minimization
    if ( uSharedMask && pFun->nFans > 1 )
    {
        int pVarPres[DAU_MAX_VAR];
        int nSupp = 0;
        for ( i = 0; i < p->nVars; i++ )
            pVarPres[i] = -1;
        for ( i = 0; i < (int)pFun->nFans; i++ )
            pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i;
        for ( i = 0; i < p->nVars; i++ )
            if ( pVarPres[i] >= 0 )
                pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) );
        assert( nSupp == (int)pFun->nFans );
    }
 
    for ( i = 0; i < (int)pFun->nFans; i++ )
        pPermResInt[i] = pPermRes[i];
p->timeEnd += Abc_Clock() - clk;
 
if ( fVerbose )
{
Dss_ManPrintOne( stdout, p, pFun->iDsd, pPermResInt );
printf( "\n" );
}
 
if ( Counter == 43418 )
{
//    int s = 0;
//    Dss_ManPrint( NULL, p );
}
 
 
    if ( fCheck )
    {
        pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
        if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
        {
            int s;
    //        Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
    //        Kit_DsdPrintFromTruth( pTruth, p->nVars );     printf( "\n" );
            printf( "Verification failed.\n" );
            s = 0;
        }
    }
    return pFun->iDsd;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dss_ManPrint()

void Dss_ManPrint ( char * pFileName, Dss_Man_t * p )

extern

Definition at line 1086 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    int CountNonDsd = 0, CountNonDsdStr = 0;
    int i, clk = Abc_Clock();
    FILE * pFile;
    pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
    if ( pFileName && pFile == NULL )
    {
        printf( "cannot open output file\n" );
        return;
    }
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        CountNonDsd += (pObj->Type == DAU_DSD_PRIME);
        CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj );
    }
    fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
    fprintf( pFile, "Non-DSD objects (max =%2d)  = %8d\n", p->nNonDecLimit, CountNonDsd );
    fprintf( pFile, "Non-DSD structures         = %8d\n", CountNonDsdStr );
    fprintf( pFile, "Memory used for objects    = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
    fprintf( pFile, "Memory used for array      = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
    fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
    fprintf( pFile, "Memory used for cache      = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMemEnts)/(1<<20) );
    fprintf( pFile, "Cache hits    = %8d %8d\n", p->nCacheHits[0],    p->nCacheHits[1] );
    fprintf( pFile, "Cache misses  = %8d %8d\n", p->nCacheMisses[0],  p->nCacheMisses[1] );
    fprintf( pFile, "Cache entries = %8d %8d\n", p->nCacheEntries[0], p->nCacheEntries[1] );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//    Dss_ManHashProfile( p );
//    Dss_ManDump( p );
//    return;
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        if ( i == 50 )
            break;
        Dss_ManPrintOne( pFile, p, Dss_Obj2Lit(pObj), NULL );
    }
    fprintf( pFile, "\n" );
    if ( pFileName )
        fclose( pFile );
}

Here is the call graph for this function:

Here is the caller graph for this function: