dauTree.c File Reference

#include "dauInt.h"
#include "misc/mem/mem.h"
#include "misc/util/utilTruth.h"

Go to the source code of this file.

Data Structures
struct	Dss_Fun_t_
struct	Dss_Ent_t_
struct	Dss_Obj_t_
struct	Dss_Ntk_t_
struct	Dss_Man_t_

Macros
#define	Dss_VecForEachObj(vVec, pObj, i)   Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )
#define	Dss_VecForEachObjVec(vLits, vVec, pObj, i)   for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
#define	Dss_VecForEachNode(vVec, pObj, i)
#define	Dss_ObjForEachFanin(vVec, pObj, pFanin, i)   for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(vVec, pObj, i)); i++ )
#define	Dss_ObjForEachChild(vVec, pObj, pFanin, i)   for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(vVec, pObj, i)); i++ )

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Dss_Fun_t_	Dss_Fun_t
	DECLARATIONS ///. More...
typedef struct Dss_Ent_t_	Dss_Ent_t
typedef struct Dss_Obj_t_	Dss_Obj_t
typedef struct Dss_Ntk_t_	Dss_Ntk_t

Functions
static Dss_Obj_t *	Dss_Regular (Dss_Obj_t *p)
static Dss_Obj_t *	Dss_Not (Dss_Obj_t *p)
static Dss_Obj_t *	Dss_NotCond (Dss_Obj_t *p, int c)
static int	Dss_IsComplement (Dss_Obj_t *p)
static int	Dss_EntWordNum (Dss_Ent_t *p)
static int	Dss_FunWordNum (Dss_Fun_t *p)
static int	Dss_ObjWordNum (int nFans)
static word *	Dss_ObjTruth (Dss_Obj_t *pObj)
static void	Dss_ObjClean (Dss_Obj_t *pObj)
static int	Dss_ObjId (Dss_Obj_t *pObj)
static int	Dss_ObjType (Dss_Obj_t *pObj)
static int	Dss_ObjSuppSize (Dss_Obj_t *pObj)
static int	Dss_ObjFaninNum (Dss_Obj_t *pObj)
static int	Dss_ObjFaninC (Dss_Obj_t *pObj, int i)
static Dss_Obj_t *	Dss_VecObj (Vec_Ptr_t *p, int Id)
static Dss_Obj_t *	Dss_VecConst0 (Vec_Ptr_t *p)
static Dss_Obj_t *	Dss_VecVar (Vec_Ptr_t *p, int v)
static int	Dss_VecLitSuppSize (Vec_Ptr_t *p, int iLit)
static int	Dss_Obj2Lit (Dss_Obj_t *pObj)
static Dss_Obj_t *	Dss_Lit2Obj (Vec_Ptr_t *p, int iLit)
static Dss_Obj_t *	Dss_ObjFanin (Vec_Ptr_t *p, Dss_Obj_t *pObj, int i)
static Dss_Obj_t *	Dss_ObjChild (Vec_Ptr_t *p, Dss_Obj_t *pObj, int i)
static int	Dss_WordCountOnes (unsigned uWord)
static int	Dss_Lit2Lit (int *pMapLit, int Lit)
static word **	Dss_ManTtElems ()
	FUNCTION DEFINITIONS ///. More...
Dss_Obj_t *	Dss_ObjAllocNtk (Dss_Ntk_t *p, int Type, int nFans, int nTruthVars)
Dss_Obj_t *	Dss_ObjCreateNtk (Dss_Ntk_t *p, int Type, Vec_Int_t *vFaninLits)
Dss_Ntk_t *	Dss_NtkAlloc (int nVars)
void	Dss_NtkFree (Dss_Ntk_t *p)
void	Dss_NtkPrint_rec (Dss_Ntk_t *p, Dss_Obj_t *pObj)
void	Dss_NtkPrint (Dss_Ntk_t *p)
static void	Dau_DsdMergeMatches (char *pDsd, int *pMatches)
int	Dss_NtkCreate_rec (char *pStr, char **p, int *pMatches, Dss_Ntk_t *pNtk, word *pTruth)
Dss_Ntk_t *	Dss_NtkCreate (char *pDsd, int nVars, word *pTruth)
int	Dss_ObjCompare (Vec_Ptr_t *p, Dss_Obj_t *p0i, Dss_Obj_t *p1i)
void	Dss_ObjSort (Vec_Ptr_t *p, Dss_Obj_t **pNodes, int nNodes, int *pPerm)
void	Dss_NtkCheck (Dss_Ntk_t *p)
int	Dss_NtkCollectPerm_rec (Dss_Ntk_t *p, Dss_Obj_t *pObj, int *pPermDsd, int *pnPerms)
void	Dss_NtkTransform (Dss_Ntk_t *p, int *pPermDsd)
Dss_Obj_t *	Dss_ObjAlloc (Dss_Man_t *p, int Type, int nFans, int nTruthVars)
Dss_Obj_t *	Dss_ObjCreate (Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
void	Dss_ManHashProfile (Dss_Man_t *p)
static unsigned	Dss_ObjHashKey (Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
unsigned *	Dss_ObjHashLookup (Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
Dss_Obj_t *	Dss_ObjFindOrAdd (Dss_Man_t *p, int Type, Vec_Int_t *vFaninLits, word *pTruth)
void	Dss_ManCacheAlloc (Dss_Man_t *p)
void	Dss_ManCacheFree (Dss_Man_t *p)
static unsigned	Dss_ManCacheHashKey (Dss_Man_t *p, Dss_Ent_t *pEnt)
void	Dss_ManCacheProfile (Dss_Man_t *p)
Dss_Ent_t **	Dss_ManCacheLookup (Dss_Man_t *p, Dss_Ent_t *pEnt)
Dss_Ent_t *	Dss_ManCacheCreate (Dss_Man_t *p, Dss_Ent_t *pEnt0, Dss_Fun_t *pFun0)
Dss_Man_t *	Dss_ManAlloc (int nVars, int nNonDecLimit)
void	Dss_ManFree (Dss_Man_t *p)
void	Dss_ManPrint_rec (FILE *pFile, Dss_Man_t *p, Dss_Obj_t *pObj, int *pPermLits, int *pnSupp)
void	Dss_ManPrintOne (FILE *pFile, Dss_Man_t *p, int iDsdLit, int *pPermLits)
int	Dss_ManCheckNonDec_rec (Dss_Man_t *p, Dss_Obj_t *pObj)
void	Dss_ManDump (Dss_Man_t *p)
void	Dss_ManPrint (char *pFileName, Dss_Man_t *p)
void	Dss_ManComputeTruth_rec (Dss_Man_t *p, Dss_Obj_t *pObj, int nVars, word *pRes, int *pPermLits, int *pnSupp)
word *	Dss_ManComputeTruth (Dss_Man_t *p, int iDsd, int nVars, int *pPermLits)
int	Dss_NtkRebuild_rec (Dss_Man_t *p, Dss_Ntk_t *pNtk, Dss_Obj_t *pObj)
int	Dss_NtkRebuild (Dss_Man_t *p, Dss_Ntk_t *pNtk)
int	Dss_ManOperation (Dss_Man_t *p, int Type, int *pLits, int nLits, unsigned char *pPerm, word *pTruth)
Dss_Fun_t *	Dss_ManOperationFun (Dss_Man_t *p, int *iDsd, int nFansTot)
void	Dss_EntPrint (Dss_Ent_t *p, Dss_Fun_t *pFun)
Dss_Fun_t *	Dss_ManBooleanAnd (Dss_Man_t *p, Dss_Ent_t *pEnt, int Counter)
Dss_Ent_t *	Dss_ManSharedMap (Dss_Man_t *p, int *iDsd, int *nFans, int **pFans, unsigned uSharedMask)
int	Dss_ManMerge (Dss_Man_t *p, int *iDsd, int *nFans, int **pFans, unsigned uSharedMask, int nKLutSize, unsigned char *pPermRes, word *pTruth)
Dss_Ent_t *	Dss_ManSharedMapDerive (Dss_Man_t *p, int iDsd0, int iDsd1, Vec_Str_t *vShared)
int	Mpm_FuncCompute (Dss_Man_t *p, int iDsd0, int iDsd1, Vec_Str_t *vShared, int *pPerm, int *pnLeaves)
int	Dss_ObjCheckTransparent (Dss_Man_t *p, Dss_Obj_t *pObj)
void	Dau_DsdTest__ ()
void	Dau_DsdTest ()
void	Dau_DsdTest444 ()

Macro Definition Documentation

#define Dss_ObjForEachChild	(		vVec,
			pObj,
			pFanin,
			i
	)		for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(vVec, pObj, i)); i++ )

Definition at line 136 of file dauTree.c.

#define Dss_ObjForEachFanin	(		vVec,
			pObj,
			pFanin,
			i
	)		for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(vVec, pObj, i)); i++ )

Definition at line 134 of file dauTree.c.

#define Dss_VecForEachNode	(		vVec,
			pObj,
			i
	)

Value:

Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )     \
        if ( pObj->Type == DAU_DSD_CONST0 || pObj->Type == DAU_DSD_VAR ) {} else

Definition at line 131 of file dauTree.c.

#define Dss_VecForEachObj	(		vVec,
			pObj,
			i
	)		Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )

Definition at line 127 of file dauTree.c.

#define Dss_VecForEachObjVec	(		vLits,
			vVec,
			pObj,
			i
	)		for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )

Definition at line 129 of file dauTree.c.

Typedef Documentation

typedef struct Dss_Ent_t_ Dss_Ent_t

Definition at line 39 of file dauTree.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Dss_Fun_t_ Dss_Fun_t

DECLARATIONS ///.

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

FileName [dauTree.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis [Canonical DSD package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

dauTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file dauTree.c.

typedef struct Dss_Ntk_t_ Dss_Ntk_t

Definition at line 65 of file dauTree.c.

typedef struct Dss_Obj_t_ Dss_Obj_t

Definition at line 51 of file dauTree.c.

Function Documentation

static void Dau_DsdMergeMatches ( char *  pDsd, int *  pMatches  )

inlinestatic

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

Synopsis [Creating DSD network from SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file dauTree.c.

{
    int pNested[DAU_MAX_VAR];
    int i, nNested = 0;
    for ( i = 0; pDsd[i]; i++ )
    {
        pMatches[i] = 0;
        if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
            pNested[nNested++] = i;
        else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
            pMatches[pNested[--nNested]] = i;
        assert( nNested < DAU_MAX_VAR );
    }
    assert( nNested == 0 );
}

void Dau_DsdTest

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1841 of file dauTree.c.

{
    int nVars = 8;
    Vec_Vec_t * vFuncs;
    Vec_Int_t * vOne, * vTwo, * vRes;//, * vThree;
    Dss_Man_t * p;
    int pEntries[3];
    int iLit, e0, e1;//, e2;
    int i, k, s;//, j;

    return;

    vFuncs = Vec_VecStart( nVars+1 );
    assert( nVars < DAU_MAX_VAR );
    p = Dss_ManAlloc( nVars, 0 );

    // init
    Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_VecVar(p->vObjs,0)) );

    // enumerate
    for ( s = 2; s <= nVars; s++ )
    {
        vRes = Vec_VecEntryInt( vFuncs, s );
        for ( i = 1; i < s; i++ )
        for ( k = i; k < s; k++ )
        if ( i + k == s )
        {
            vOne = Vec_VecEntryInt( vFuncs, i );
            vTwo = Vec_VecEntryInt( vFuncs, k );
            Vec_IntForEachEntry( vOne, pEntries[0], e0 )
            Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
            {
                int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
                int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );

                iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, iLit );

                if ( fAddInv0 )
                {
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv1 )
                {
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv0 && fAddInv1 )
                {
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, Abc_LitRegular(iLit) );
            }
        }
/*
        for ( i = 1; i < s; i++ )
        for ( k = 1; k < s; k++ )
        for ( j = 1; j < s; j++ )
        if ( i + k + j == s )
        {
            vOne   = Vec_VecEntryInt( vFuncs, i );
            vTwo   = Vec_VecEntryInt( vFuncs, k );
            vThree = Vec_VecEntryInt( vFuncs, j );
            Vec_IntForEachEntry( vOne,   pEntries[0], e0 )
            Vec_IntForEachEntry( vTwo,   pEntries[1], e1 )
            Vec_IntForEachEntry( vThree, pEntries[2], e2 )
            {
                int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
                int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
                int fAddInv2 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[2])) );

                if ( !fAddInv0 && k > j )
                    continue;

                iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, iLit );

                if ( fAddInv1 )
                {
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv2 )
                {
                    pEntries[2] = Abc_LitNot( pEntries[2] );
                    iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                    pEntries[2] = Abc_LitNot( pEntries[2] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }
            }
        }
*/
        Vec_IntUniqify( vRes );
    }
    Dss_ManPrint( "_npn/npn/dsdcanon.txt", p );

    Dss_ManFree( p );
    Vec_VecFree( vFuncs );
}

void Dau_DsdTest444

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1978 of file dauTree.c.

{
    Dss_Man_t * p = Dss_ManAlloc( 6, 0 );
    int iLit1[3] = { 2, 4 };
    int iLit2[3] = { 2, 4, 6 };
    int iRes[5];
    int nFans[2] = { 4, 3 };
    int pPermLits1[4] = { 0, 2, 5, 6 };
    int pPermLits2[5] = { 2, 9, 10 };
    int * pPermLits[2] = { pPermLits1, pPermLits2 };
    unsigned char pPermRes[6];
    int pPermResInt[6];
    unsigned uMaskShared = 2;
    int i;

    iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, NULL );
    iRes[1] = iRes[0]; 
    iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL );
    iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL );

    Dss_ManPrintOne( stdout, p, iRes[0], NULL );
    Dss_ManPrintOne( stdout, p, iRes[2], NULL );
    Dss_ManPrintOne( stdout, p, iRes[3], NULL );

    Dss_ManPrintOne( stdout, p, iRes[2], pPermLits1 );
    Dss_ManPrintOne( stdout, p, iRes[3], pPermLits2 );

    iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL );

    for ( i = 0; i < 6; i++ )
        pPermResInt[i] = pPermRes[i];

    Dss_ManPrintOne( stdout, p, iRes[4], NULL );
    Dss_ManPrintOne( stdout, p, iRes[4], pPermResInt );

    Dss_ManFree( p );
}

void Dau_DsdTest__

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1816 of file dauTree.c.

{
    int nVars = 8;
//    char * pDsd = "[(ab)(cd)]";
    char * pDsd = "(!(a!(bh))[cde]!(fg))";
    Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL );
//    Dss_NtkPrint( pNtk );
//    Dss_NtkCheck( pNtk );
//    Dss_NtkTransform( pNtk );
//    Dss_NtkPrint( pNtk );
    Dss_NtkFree( pNtk );
    nVars = 0;
}

void Dss_EntPrint	(	Dss_Ent_t *	p,
		Dss_Fun_t *	pFun
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1411 of file dauTree.c.

{
    int i;
    printf( "%d %d ", p->iDsd0, p->iDsd1 );
    for ( i = 0; i < (int)p->nShared; i++ )
        printf( "%d=%d ", p->pShared[2*i], p->pShared[2*i+1] );
    printf( "-> %d   ", pFun->iDsd );
}

static int Dss_EntWordNum ( Dss_Ent_t *  p )

inlinestatic

Definition at line 105 of file dauTree.c.

{ return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0);            }

static int Dss_FunWordNum ( Dss_Fun_t *  p )

inlinestatic

Definition at line 106 of file dauTree.c.

{ assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0);     }

static int Dss_IsComplement ( Dss_Obj_t *  p )

inlinestatic

Definition at line 103 of file dauTree.c.

{ return (int)((ABC_PTRUINT_T)(p) & 01);                                             }

static int Dss_Lit2Lit ( int *  pMapLit, int  Lit  )

inlinestatic

Definition at line 148 of file dauTree.c.

{ return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) );   }

static Dss_Obj_t* Dss_Lit2Obj ( Vec_Ptr_t *  p, int  iLit  )

inlinestatic

Definition at line 123 of file dauTree.c.

{ return Dss_NotCond(Dss_VecObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit));        }

Dss_Man_t* Dss_ManAlloc	(	int	nVars,
		int	nNonDecLimit
	)

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;
}

Dss_Fun_t* Dss_ManBooleanAnd	(	Dss_Man_t *	p,
		Dss_Ent_t *	pEnt,
		int	Counter
	)

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

Synopsis [Performs AND on two DSD functions with support overlap.]

Description [Returns the perm of the resulting literals. The perm size is equal to the number of support variables. The perm variables are 0-based numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]

SideEffects []

SeeAlso []

Definition at line 1433 of file dauTree.c.

{
    static char Buffer[100];
    Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
    Dss_Ntk_t * pNtk;
    word * pTruthOne, pTruth[DAU_MAX_WORD];
    char pDsd[DAU_MAX_STR];
    int pMapDsd2Truth[DAU_MAX_VAR];
    int pPermLits[DAU_MAX_VAR];
    int pPermDsd[DAU_MAX_VAR];
    int i, nNonDec, nSuppSize = 0;
    int nFans[2];
    nFans[0] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd0 );
    nFans[1] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd1 );
    // create first truth table
    for ( i = 0; i < nFans[0]; i++ )
    {
        pMapDsd2Truth[nSuppSize] = i;
        pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
    }
    pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
    Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
if ( Counter )
{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
}
    // create second truth table
    for ( i = 0; i < nFans[1]; i++ )
        pPermLits[i] = -1;
    for ( i = 0; i < (int)pEnt->nShared; i++ )
        pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1];
    for ( i = 0; i < nFans[1]; i++ )
        if ( pPermLits[i] == -1 )
        {
            pMapDsd2Truth[nSuppSize] = nFans[0] + i;
            pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
        }
    pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
if ( Counter )
{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
}
    Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
    // perform decomposition
    nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd );
    if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit )
        return NULL;
    // derive network and convert it into the manager
    pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL );
//Dss_NtkPrint( pNtk );    
    Dss_NtkCheck( pNtk );
    Dss_NtkTransform( pNtk, pPermDsd );
//Dss_NtkPrint( pNtk );    
    pFun->iDsd = Dss_NtkRebuild( p, pNtk );
    Dss_NtkFree( pNtk );
    // pPermDsd maps vars of iDsdRes into literals of pTruth
    // translate this map into the one that maps vars of iDsdRes into literals of cut
    pFun->nFans = Dss_VecLitSuppSize( p->vObjs, pFun->iDsd );
    for ( i = 0; i < (int)pFun->nFans; i++ )
        pFun->pFans[i] = (unsigned char)Abc_Lit2LitV( pMapDsd2Truth, pPermDsd[i] );

//    Dss_EntPrint( pEnt, pFun );
    return pFun;
}

void Dss_ManCacheAlloc

(

Dss_Man_t *

p

)

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

Synopsis [Cache for decomposition calls.]

Description []

SideEffects []

SeeAlso []

Definition at line 890 of file dauTree.c.

{
    assert( p->nCache == 0 );
    p->nCache = Abc_PrimeCudd( 100000 );
    p->pCache = ABC_CALLOC( Dss_Ent_t *, p->nCache );
}

Dss_Ent_t* Dss_ManCacheCreate	(	Dss_Man_t *	p,
		Dss_Ent_t *	pEnt0,
		Dss_Fun_t *	pFun0
	)

Definition at line 944 of file dauTree.c.

{
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * pEnt0->nWords );
    Dss_Fun_t * pFun = (Dss_Fun_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * Dss_FunWordNum(pFun0) );
    memcpy( pEnt, pEnt0, sizeof(word) * pEnt0->nWords );
    memcpy( pFun, pFun0, sizeof(word) * Dss_FunWordNum(pFun0) );
    pEnt->pFunc = pFun;
    pEnt->pNext = NULL;
    p->nCacheEntries[pEnt->nShared!=0]++;
    return pEnt;
}

void Dss_ManCacheFree

(

Dss_Man_t *

p

)

Definition at line 896 of file dauTree.c.

{
    if ( p->pCache == NULL )
        return;
    assert( p->nCache != 0 );
    p->nCache = 0;
    ABC_FREE( p->pCache );
}

static unsigned Dss_ManCacheHashKey ( Dss_Man_t *  p, Dss_Ent_t *  pEnt  )

inlinestatic

Definition at line 904 of file dauTree.c.

{ 
    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
    int i;
    unsigned uHash = pEnt->nShared * 7103 + pEnt->iDsd0 * 7873 + pEnt->iDsd1 * 8147;
    for ( i = 0; i < 2*(int)pEnt->nShared; i++ )
        uHash += pEnt->pShared[i] * s_Primes[i & 0x7];
    return uHash % p->nCache;
}

Dss_Ent_t** Dss_ManCacheLookup	(	Dss_Man_t *	p,
		Dss_Ent_t *	pEnt
	)

Definition at line 927 of file dauTree.c.

{
    Dss_Ent_t ** pSpot = p->pCache + Dss_ManCacheHashKey( p, pEnt );
    for ( ; *pSpot; pSpot = &(*pSpot)->pNext )
    {
        if ( (*pSpot)->iDsd0   == pEnt->iDsd0 && 
             (*pSpot)->iDsd1   == pEnt->iDsd1 && 
             (*pSpot)->nShared == pEnt->nShared && 
             !memcmp((*pSpot)->pShared, pEnt->pShared, sizeof(char)*2*pEnt->nShared)  ) // equal
        {
            p->nCacheHits[pEnt->nShared!=0]++;
            return pSpot;
        }
    }
    p->nCacheMisses[pEnt->nShared!=0]++;
    return pSpot;
}

void Dss_ManCacheProfile

(

Dss_Man_t *

p

)

Definition at line 913 of file dauTree.c.

{
    Dss_Ent_t ** pSpot;
    int i, Counter;
    for ( i = 0; i < p->nCache; i++ )
    {
        Counter = 0;
        for ( pSpot = p->pCache + i; *pSpot; pSpot = &(*pSpot)->pNext, Counter++ )
            ;
        if ( Counter )
            printf( "%d ", Counter );
    }
    printf( "\n" );
}

int Dss_ManCheckNonDec_rec	(	Dss_Man_t *	p,
		Dss_Obj_t *	pObj
	)

Definition at line 1040 of file dauTree.c.

{
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_CONST0 )
        return 0;
    if ( pObj->Type == DAU_DSD_VAR )
        return 0;
    if ( pObj->Type == DAU_DSD_PRIME )
        return 1;
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
        if ( Dss_ManCheckNonDec_rec( p, pFanin ) )
            return 1;
    return 0;
}

word* Dss_ManComputeTruth	(	Dss_Man_t *	p,
		int	iDsd,
		int	nVars,
		int *	pPermLits
	)

Definition at line 1192 of file dauTree.c.

{
    Dss_Obj_t * pObj = Dss_Lit2Obj(p->vObjs, iDsd);
    word * pRes = p->pTtElems[DAU_MAX_VAR];
    int nWords = Abc_TtWordNum( nVars );
    int nSupp = 0;
    assert( nVars <= DAU_MAX_VAR );
    if ( iDsd == 0 )
        Abc_TtConst0( pRes, nWords );
    else if ( iDsd == 1 )
        Abc_TtConst1( pRes, nWords );
    else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits[nSupp++];
        Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
    }
    else
        Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits, &nSupp );
    assert( nSupp == (int)Dss_Regular(pObj)->nSupp );
    return pRes;
}

void Dss_ManComputeTruth_rec	(	Dss_Man_t *	p,
		Dss_Obj_t *	pObj,
		int	nVars,
		word *	pRes,
		int *	pPermLits,
		int *	pnSupp
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1139 of file dauTree.c.

{
    Dss_Obj_t * pChild;
    int nWords = Abc_TtWordNum(nVars);
    int i, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular(pObj);
    if ( pObj->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits[(*pnSupp)++];
        assert( (*pnSupp) <= nVars );
        Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
        return;
    }
    if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
    {
        word pTtTemp[DAU_MAX_WORD];
        if ( pObj->Type == DAU_DSD_AND )
            Abc_TtConst1( pRes, nWords );
        else
            Abc_TtConst0( pRes, nWords );
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
        {
            Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits, pnSupp );
            if ( pObj->Type == DAU_DSD_AND )
                Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
            else
                Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
        }
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    if ( pObj->Type == DAU_DSD_MUX ) // mux
    {
        word pTtTemp[3][DAU_MAX_WORD];
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
            Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits, pnSupp );
        assert( i == 3 );
        Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    if ( pObj->Type == DAU_DSD_PRIME ) // function
    {
        word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
            Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits, pnSupp );
        Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords );
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    assert( 0 );

}

void Dss_ManDump

(

Dss_Man_t *

p

)

Definition at line 1056 of file dauTree.c.

{
    char * pFileName = "dss_tts.txt";
    FILE * pFile;
    word Temp[DAU_MAX_WORD];
    Dss_Obj_t * pObj;
    int i;
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\".\n", pFileName );
        return;
    }
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        if ( pObj->Type != DAU_DSD_PRIME )
            continue;
        Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 );
        Abc_TtStretch6( Temp, pObj->nFans, p->nVars );
        fprintf( pFile, "0x" );
        Abc_TtPrintHexRev( pFile, Temp, p->nVars );
        fprintf( pFile, "\n" );

//        printf( "%6d : ", i );
//        Abc_TtPrintHexRev( stdout, Temp, p->nVars );
//        printf( "    " );
//        Dau_DsdPrintFromTruth( stdout, Temp, p->nVars );
    }
    fclose( pFile );
}

void Dss_ManFree

(

Dss_Man_t *

p

)

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 );
}

void Dss_ManHashProfile

(

Dss_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 821 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    unsigned * pSpot;
    int i, Counter;
    for ( i = 0; i < p->nBins; i++ )
    {
        Counter = 0;
        for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
             pObj = Dss_VecObj( p->vObjs, *pSpot );
        if ( Counter )
            printf( "%d ", Counter );
    }
    printf( "\n" );
}

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

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( "Paramater 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;
}

int Dss_ManOperation	(	Dss_Man_t *	p,
		int	Type,
		int *	pLits,
		int	nLits,
		unsigned char *	pPerm,
		word *	pTruth
	)

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

Synopsis [Performs DSD operation on the two literals.]

Description [Returns the perm of the resulting literals. The perm size is equal to the number of support variables. The perm variables are 0-based numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]

SideEffects []

SeeAlso []

Definition at line 1287 of file dauTree.c.

{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pObj, * pChild;
    int i, k, nChildren = 0, fCompl = 0, fComplFan;

    assert( Type == DAU_DSD_AND || pPerm == NULL );
    if ( Type == DAU_DSD_AND && pPerm != NULL )
    {
        int pBegEnd[DAU_MAX_VAR];
        int j, nSSize = 0;
        for ( k = 0; k < nLits; k++ )
        {
            pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
            if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
            {
                fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj));
                if ( fComplFan )
                    pObj = Dss_Regular(pObj);
                pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pObj)->nSupp);
                nSSize += Dss_Regular(pObj)->nSupp;
                pChildren[nChildren++] = pObj;
            }
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                {
                    fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild));
                    if ( fComplFan )
                        pChild = Dss_Regular(pChild);
                    pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp);
                    nSSize += Dss_Regular(pChild)->nSupp;
                    pChildren[nChildren++] = pChild;
                }
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
        // create permutation
        for ( j = i = 0; i < nChildren; i++ )
            for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
                pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 );
        assert( j == nSSize );
    }
    else if ( Type == DAU_DSD_AND )
    {
        for ( k = 0; k < nLits; k++ )
        {
            pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
            if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
                pChildren[nChildren++] = pObj;
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                    pChildren[nChildren++] = pChild;
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
    }
    else if ( Type == DAU_DSD_XOR )
    {
        for ( k = 0; k < nLits; k++ )
        {
            fCompl ^= Abc_LitIsCompl(pLits[k]);
            pObj = Dss_Lit2Obj(p->vObjs, Abc_LitRegular(pLits[k]));
            if ( pObj->Type != DAU_DSD_XOR )
                pChildren[nChildren++] = pObj;
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                {
                    assert( !Dss_IsComplement(pChild) );
                    pChildren[nChildren++] = pChild;
                }
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
    }
    else if ( Type == DAU_DSD_MUX )
    {
        if ( Abc_LitIsCompl(pLits[0]) )
        {
            pLits[0] = Abc_LitNot(pLits[0]);
            ABC_SWAP( int, pLits[1], pLits[2] );
        }
        if ( Abc_LitIsCompl(pLits[1]) )
        {
            pLits[1] = Abc_LitNot(pLits[1]);
            pLits[2] = Abc_LitNot(pLits[2]);
            fCompl ^= 1;
        }
        for ( k = 0; k < nLits; k++ )
            pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
    }
    else if ( Type == DAU_DSD_PRIME )
    {
        for ( k = 0; k < nLits; k++ )
            pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
    }
    else assert( 0 );

    // shift subgraphs
    Vec_IntClear( p->vLeaves );
    for ( i = 0; i < nChildren; i++ )
        Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
    // create new graph
    pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth );
    return Abc_Var2Lit( pObj->Id, fCompl );
}

Dss_Fun_t* Dss_ManOperationFun	(	Dss_Man_t *	p,
		int *	iDsd,
		int	nFansTot
	)

Definition at line 1389 of file dauTree.c.

{
    static char Buffer[100];
    Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
    pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL );
//printf( "%d %d -> %d  ", iDsd[0], iDsd[1], pFun->iDsd );
    pFun->nFans = nFansTot;
    assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
    return pFun;
}

void Dss_ManPrint	(	char *	pFileName,
		Dss_Man_t *	p
	)

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 );
}

void Dss_ManPrint_rec	(	FILE *	pFile,
		Dss_Man_t *	p,
		Dss_Obj_t *	pObj,
		int *	pPermLits,
		int *	pnSupp
	)

Definition at line 1005 of file dauTree.c.

{
    char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
    char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_CONST0 )
        { fprintf( pFile, "0" ); return; }
    if ( pObj->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
        fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
        return;
    }
    if ( pObj->Type == DAU_DSD_PRIME )
        Abc_TtPrintHexRev( pFile, Dss_ObjTruth(pObj), pObj->nFans );
    fprintf( pFile, "%c", OpenType[pObj->Type] );
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
    {
        fprintf( pFile, "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
        Dss_ManPrint_rec( pFile, p, pFanin, pPermLits, pnSupp );
    }
    fprintf( pFile, "%c", CloseType[pObj->Type] );
}

void Dss_ManPrintOne	(	FILE *	pFile,
		Dss_Man_t *	p,
		int	iDsdLit,
		int *	pPermLits
	)

Definition at line 1030 of file dauTree.c.

{
    int nSupp = 0;
    fprintf( pFile, "%6d : ", Abc_Lit2Var(iDsdLit) );
    fprintf( pFile, "%2d ",   Dss_VecLitSuppSize(p->vObjs, iDsdLit) );
    fprintf( pFile, "%s",     Abc_LitIsCompl(iDsdLit) ? "!" : ""  );
    Dss_ManPrint_rec( pFile, p, Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit)), pPermLits, &nSupp );
    fprintf( pFile, "\n" );
    assert( nSupp == (int)Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit))->nSupp );
}

Dss_Ent_t* Dss_ManSharedMap	(	Dss_Man_t *	p,
		int *	iDsd,
		int *	nFans,
		int **	pFans,
		unsigned	uSharedMask
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1510 of file dauTree.c.

{
    static char Buffer[100];
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
    pEnt->iDsd0 = iDsd[0];
    pEnt->iDsd1 = iDsd[1];
    pEnt->nShared = 0;
    if ( uSharedMask )
    {
        int i, g, pMapGtoL[DAU_MAX_VAR] = {-1};
        for ( i = 0; i < nFans[0]; i++ )
            pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) );
        for ( i = 0; i < nFans[1]; i++ )
        {
            g = Abc_Lit2Var( pFans[1][i] );
            if ( (uSharedMask >> g) & 1 )
            {
                assert( pMapGtoL[g] >= 0 );
                pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i;
                pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) );
                pEnt->nShared++;
            }
        }
    }
    pEnt->nWords = Dss_EntWordNum( pEnt );
    return pEnt;
}

Dss_Ent_t* Dss_ManSharedMapDerive	(	Dss_Man_t *	p,
		int	iDsd0,
		int	iDsd1,
		Vec_Str_t *	vShared
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1681 of file dauTree.c.

{
    static char Buffer[100];
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
    pEnt->iDsd0 = iDsd0;
    pEnt->iDsd1 = iDsd1;
    pEnt->nShared = Vec_StrSize(vShared)/2;
    memcpy( pEnt->pShared, (unsigned char *)Vec_StrArray(vShared), sizeof(char) * Vec_StrSize(vShared) );
    pEnt->nWords = Dss_EntWordNum( pEnt );
    return pEnt;
}

static word** Dss_ManTtElems ( )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [Elementary truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file dauTree.c.

{
    static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
    if ( pTtElems[0] == NULL )
    {
        int v;
        for ( v = 0; v <= DAU_MAX_VAR; v++ )
            pTtElems[v] = TtElems[v];
        Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
    }
    return pTtElems;
}

static Dss_Obj_t* Dss_Not ( Dss_Obj_t *  p )

inlinestatic

Definition at line 101 of file dauTree.c.

{ return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);                                    }

static Dss_Obj_t* Dss_NotCond ( Dss_Obj_t *  p, int  c  )

inlinestatic

Definition at line 102 of file dauTree.c.

{ return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));                                    }

Dss_Ntk_t* Dss_NtkAlloc

(

int

nVars

)

Definition at line 453 of file dauTree.c.

{
    Dss_Ntk_t * p;
    Dss_Obj_t * pObj;
    int i;
    p = ABC_CALLOC( Dss_Ntk_t, 1 );
    p->nVars     = nVars;
    p->nMemAlloc = DAU_MAX_STR;
    p->pMem      = ABC_ALLOC( word, p->nMemAlloc );
    p->vObjs     = Vec_PtrAlloc( 100 );
    Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 );
    for ( i = 0; i < nVars; i++ )
    {
        pObj = Dss_ObjAllocNtk( p, DAU_DSD_VAR, 0, 0 );
        pObj->iVar = i;
        pObj->nSupp = 1;
    }
    return p;
}

void Dss_NtkCheck

(

Dss_Ntk_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 692 of file dauTree.c.

{
    Dss_Obj_t * pObj, * pFanin;
    int i, k;
    Dss_VecForEachNode( p->vObjs, pObj, i )
    {
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, k )
        {
            if ( pObj->Type == DAU_DSD_AND && pFanin->Type == DAU_DSD_AND )
                assert( Dss_ObjFaninC(pObj, k) );
            else if ( pObj->Type == DAU_DSD_XOR )
                assert( pFanin->Type != DAU_DSD_XOR );
            else if ( pObj->Type == DAU_DSD_MUX )
                assert( !Dss_ObjFaninC(pObj, 0) );
        }
    }
}

int Dss_NtkCollectPerm_rec	(	Dss_Ntk_t *	p,
		Dss_Obj_t *	pObj,
		int *	pPermDsd,
		int *	pnPerms
	)

Definition at line 709 of file dauTree.c.

{
    Dss_Obj_t * pChild;
    int k, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular( pObj );
    if ( pObj->Type == DAU_DSD_VAR )
    {
        pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl);
        pObj->iVar = (*pnPerms)++;
        return fCompl;
    }
    Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
        if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) )
            pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]);
    return 0;
}

Dss_Ntk_t* Dss_NtkCreate	(	char *	pDsd,
		int	nVars,
		word *	pTruth
	)

Definition at line 601 of file dauTree.c.

{
    int fCompl = 0;
    Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars );
    if ( *pDsd == '!' )
         pDsd++, fCompl = 1;
    if ( Dau_DsdIsConst(pDsd) )
        pNtk->pRoot = Dss_VecConst0(pNtk->vObjs);
    else if ( Dau_DsdIsVar(pDsd) )
        pNtk->pRoot = Dss_VecVar(pNtk->vObjs, Dau_DsdReadVar(pDsd));
    else
    {
        int iLit, pMatches[DAU_MAX_STR];
        Dau_DsdMergeMatches( pDsd, pMatches );
        iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk, pTruth );
        pNtk->pRoot = Dss_Lit2Obj( pNtk->vObjs, iLit );
    }
    if ( fCompl )
        pNtk->pRoot = Dss_Not(pNtk->pRoot);
    return pNtk;
}

int Dss_NtkCreate_rec	(	char *	pStr,
		char **	p,
		int *	pMatches,
		Dss_Ntk_t *	pNtk,
		word *	pTruth
	)

Definition at line 538 of file dauTree.c.

{
    int fCompl = 0;
    if ( **p == '!' )
    {
        fCompl = 1;
        (*p)++;
    }
    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
        (*p)++;
/*
    if ( **p == '<' )
    {
        char * q = pStr + pMatches[ *p - pStr ];
        if ( *(q+1) == '{' )
            *p = q+1;
    }
*/
    if ( **p >= 'a' && **p <= 'z' ) // var
        return Abc_Var2Lit( Dss_ObjId(Dss_VecVar(pNtk->vObjs, **p - 'a')), fCompl );
    if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
    {
        Dss_Obj_t * pObj;
        Vec_Int_t * vFaninLits = Vec_IntAlloc( 10 );
        char * q = pStr + pMatches[ *p - pStr ];
        int Type;
        if ( **p == '(' )
            Type = DAU_DSD_AND;
        else if ( **p == '[' )
            Type = DAU_DSD_XOR;
        else if ( **p == '<' )
            Type = DAU_DSD_MUX;
        else if ( **p == '{' )
            Type = DAU_DSD_PRIME;
        else assert( 0 );
        assert( *q == **p + 1 + (**p != '(') );
        for ( (*p)++; *p < q; (*p)++ )
            Vec_IntPush( vFaninLits, Dss_NtkCreate_rec(pStr, p, pMatches, pNtk, pTruth) );
        assert( *p == q );
        if ( Type == DAU_DSD_PRIME )
        {
            Vec_Int_t * vFaninLitsNew;
            word pTemp[DAU_MAX_WORD];
            char pCanonPerm[DAU_MAX_VAR];
            int i, uCanonPhase, nFanins = Vec_IntSize(vFaninLits);
            Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nFanins), 0 );
            uCanonPhase = Abc_TtCanonicize( pTemp, nFanins, pCanonPerm );
            fCompl = (uCanonPhase >> nFanins) & 1;
            vFaninLitsNew = Vec_IntAlloc( nFanins );
            for ( i = 0; i < nFanins; i++ )
                Vec_IntPush( vFaninLitsNew, Abc_LitNotCond(Vec_IntEntry(vFaninLits, pCanonPerm[i]), (uCanonPhase>>i)&1) );
            pObj = Dss_ObjCreateNtk( pNtk, DAU_DSD_PRIME, vFaninLitsNew );
            Abc_TtCopy( Dss_ObjTruth(pObj), pTemp, Abc_TtWordNum(nFanins), 0 );
            Vec_IntFree( vFaninLitsNew );
        }
        else
            pObj = Dss_ObjCreateNtk( pNtk, Type, vFaninLits );
        Vec_IntFree( vFaninLits );
        return Abc_LitNotCond( Dss_Obj2Lit(pObj), fCompl );
    }
    assert( 0 );
    return -1;
}

void Dss_NtkFree

(

Dss_Ntk_t *

p

)

Definition at line 472 of file dauTree.c.

{
    Vec_PtrFree( p->vObjs );
    ABC_FREE( p->pMem );
    ABC_FREE( p );
}

void Dss_NtkPrint

(

Dss_Ntk_t *

p

)

Definition at line 497 of file dauTree.c.

{
    if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
        printf( "%d", Dss_IsComplement(p->pRoot) );
    else
    {
        printf( "%s", Dss_IsComplement(p->pRoot) ? "!":"" );        
        if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_VAR )
            printf( "%c", 'a' + Dss_Regular(p->pRoot)->iVar );
        else
            Dss_NtkPrint_rec( p, Dss_Regular(p->pRoot) );
    }
    printf( "\n" );
}

void Dss_NtkPrint_rec	(	Dss_Ntk_t *	p,
		Dss_Obj_t *	pObj
	)

Definition at line 478 of file dauTree.c.

{
    char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
    char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_VAR )
        { printf( "%c", 'a' + pObj->iVar ); return; }
    if ( pObj->Type == DAU_DSD_PRIME )
        Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
    printf( "%c", OpenType[pObj->Type] );
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
    {
        printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
        Dss_NtkPrint_rec( p, pFanin );
    }
    printf( "%c", CloseType[pObj->Type] );
}

int Dss_NtkRebuild	(	Dss_Man_t *	p,
		Dss_Ntk_t *	pNtk
	)

Definition at line 1264 of file dauTree.c.

{
    assert( p->nVars == pNtk->nVars );
    if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
        return Dss_IsComplement(pNtk->pRoot);
    if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
        return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar + 1, Dss_IsComplement(pNtk->pRoot) );
    return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot );
}

int Dss_NtkRebuild_rec	(	Dss_Man_t *	p,
		Dss_Ntk_t *	pNtk,
		Dss_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1227 of file dauTree.c.

{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pChild, * pObjNew;
    int i, k, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular(pObj);
    if ( pObj->Type == DAU_DSD_VAR )
        return Abc_Var2Lit( 1, fCompl );
    Dss_ObjForEachChild( pNtk->vObjs, pObj, pChild, k )
    {
        pChildren[k] = Dss_Lit2Obj( p->vObjs, Dss_NtkRebuild_rec( p, pNtk, pChild ) );
        if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) )
            pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1;
    }
    // normalize MUX
    if ( pObj->Type == DAU_DSD_MUX )
    {
        if ( Dss_IsComplement(pChildren[0]) )
        {
            pChildren[0] = Dss_Not(pChildren[0]);
            ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] );
        }
        if ( Dss_IsComplement(pChildren[1]) )
        {
            pChildren[1] = Dss_Not(pChildren[1]);
            pChildren[2] = Dss_Not(pChildren[2]);
            fCompl ^= 1;
        }
    }
    // shift subgraphs
    Vec_IntClear( p->vLeaves );
    for ( i = 0; i < k; i++ )
        Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
    // create new graph
    pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
    return Abc_Var2Lit( pObjNew->Id, fCompl );
}

void Dss_NtkTransform	(	Dss_Ntk_t *	p,
		int *	pPermDsd
	)

Definition at line 725 of file dauTree.c.

{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pObj, * pChild;
    int i, k, nPerms;
    if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
        return;
    Dss_VecForEachNode( p->vObjs, pObj, i )
    {
        if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
            continue;
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
            pChildren[k] = pChild;
        Dss_ObjSort( p->vObjs, pChildren, Dss_ObjFaninNum(pObj), NULL );
        for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ )
            pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] );
    }
    nPerms = 0;
    if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) )
        p->pRoot = Dss_Regular(p->pRoot);
    assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp );
}

static int Dss_Obj2Lit ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 122 of file dauTree.c.

{ return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj));                 }

Dss_Obj_t* Dss_ObjAlloc	(	Dss_Man_t *	p,
		int	Type,
		int	nFans,
		int	nTruthVars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 760 of file dauTree.c.

{
    int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
    Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
    Dss_ObjClean( pObj );
    pObj->Type   = Type;
    pObj->nFans  = nFans;
    pObj->nWords = Dss_ObjWordNum(nFans);
    pObj->Id     = Vec_PtrSize( p->vObjs );
    pObj->iVar   = 31;
    Vec_PtrPush( p->vObjs, pObj );
    Vec_IntPush( p->vNexts, 0 );
    return pObj;
}

Dss_Obj_t* Dss_ObjAllocNtk	(	Dss_Ntk_t *	p,
		int	Type,
		int	nFans,
		int	nTruthVars
	)

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

Synopsis [Creating DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    pObj = (Dss_Obj_t *)(p->pMem + p->nMem);
    Dss_ObjClean( pObj );
    pObj->nFans  = nFans;
    pObj->nWords = Dss_ObjWordNum( nFans );
    pObj->Type   = Type;
    pObj->Id     = Vec_PtrSize( p->vObjs );
    pObj->iVar   = 31;
    Vec_PtrPush( p->vObjs, pObj );
    p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
    assert( p->nMem < p->nMemAlloc );
    return pObj;
}

int Dss_ObjCheckTransparent	(	Dss_Man_t *	p,
		Dss_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1776 of file dauTree.c.

{
    Dss_Obj_t * pFanin;
    int i;
    if ( pObj->Type == DAU_DSD_VAR )
        return 1;
    if ( pObj->Type == DAU_DSD_AND )
        return 0;
    if ( pObj->Type == DAU_DSD_XOR )
    {
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
            if ( Dss_ObjCheckTransparent( p, pFanin ) )
                return 1;
        return 0;
    }
    if ( pObj->Type == DAU_DSD_MUX )
    {
        pFanin = Dss_ObjFanin( p->vObjs, pObj, 1 );
        if ( !Dss_ObjCheckTransparent(p, pFanin) )
            return 0;
        pFanin = Dss_ObjFanin( p->vObjs, pObj, 2 );
        if ( !Dss_ObjCheckTransparent(p, pFanin) )
            return 0;
        return 1;
    }
    assert( pObj->Type == DAU_DSD_PRIME );
    return 0;
}

static Dss_Obj_t* Dss_ObjChild ( Vec_Ptr_t *  p, Dss_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 125 of file dauTree.c.

{ assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]);               }

static void Dss_ObjClean ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 110 of file dauTree.c.

{ memset( pObj, 0, sizeof(Dss_Obj_t) );                                              }

int Dss_ObjCompare	(	Vec_Ptr_t *	p,
		Dss_Obj_t *	p0i,
		Dss_Obj_t *	p1i
	)

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

Synopsis [Comparing two DSD nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 634 of file dauTree.c.

{
    Dss_Obj_t * p0 = Dss_Regular(p0i);
    Dss_Obj_t * p1 = Dss_Regular(p1i);
    Dss_Obj_t * pChild0, * pChild1;
    int i, Res;
    if ( Dss_ObjType(p0) < Dss_ObjType(p1) )
        return -1;
    if ( Dss_ObjType(p0) > Dss_ObjType(p1) )
        return 1;
    if ( Dss_ObjType(p0) < DAU_DSD_AND )
        return 0;
    if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) )
        return -1;
    if ( Dss_ObjFaninNum(p0) > Dss_ObjFaninNum(p1) )
        return 1;
    for ( i = 0; i < Dss_ObjFaninNum(p0); i++ )
    {
        pChild0 = Dss_ObjChild( p, p0, i );
        pChild1 = Dss_ObjChild( p, p1, i );
        Res = Dss_ObjCompare( p, pChild0, pChild1 );
        if ( Res != 0 )
            return Res;
    }
    if ( Dss_IsComplement(p0i) < Dss_IsComplement(p1i) )
        return -1;
    if ( Dss_IsComplement(p0i) > Dss_IsComplement(p1i) )
        return 1;
    return 0;
}

Dss_Obj_t* Dss_ObjCreate	(	Dss_Man_t *	p,
		int	Type,
		Vec_Int_t *	vFaninLits,
		word *	pTruth
	)

Definition at line 774 of file dauTree.c.

{
    Dss_Obj_t * pObj, * pFanin, * pPrev = NULL;
    int i, Entry;
    // check structural canonicity
    assert( Type != DAU_DSD_MUX || Vec_IntSize(vFaninLits) == 3 );
    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 0)) );
    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 1)) || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 2)) );
    // check that leaves are in good order
    if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
    Dss_VecForEachObjVec( vFaninLits, p->vObjs, pFanin, i )
    {
        assert( Type != DAU_DSD_AND || Abc_LitIsCompl(Vec_IntEntry(vFaninLits, i)) || Dss_ObjType(pFanin) != DAU_DSD_AND );
        assert( Type != DAU_DSD_XOR || Dss_ObjType(pFanin) != DAU_DSD_XOR );
        assert( pPrev == NULL || Dss_ObjCompare(p->vObjs, pPrev, pFanin) <= 0 );
        pPrev = pFanin;
    }
    // create new node
    pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
    if ( Type == DAU_DSD_PRIME )
        Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 );
    assert( pObj->nSupp == 0 );
    Vec_IntForEachEntry( vFaninLits, Entry, i )
    {
        pObj->pFans[i] = Entry;
        pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
    }
/*
    {
        extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits );
        Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
    }
*/
    return pObj;
}

Dss_Obj_t* Dss_ObjCreateNtk	(	Dss_Ntk_t *	p,
		int	Type,
		Vec_Int_t *	vFaninLits
	)

Definition at line 440 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    int i, Entry;
    pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
    Vec_IntForEachEntry( vFaninLits, Entry, i )
    {
        pObj->pFans[i] = Entry;
        pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
    }
    assert( i == (int)pObj->nFans );
    return pObj;
}

static Dss_Obj_t* Dss_ObjFanin ( Vec_Ptr_t *  p, Dss_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 124 of file dauTree.c.

{ assert(i < (int)pObj->nFans); return Dss_VecObj(p, Abc_Lit2Var(pObj->pFans[i]));   }

static int Dss_ObjFaninC ( Dss_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 115 of file dauTree.c.

{ assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]);               }

static int Dss_ObjFaninNum ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 114 of file dauTree.c.

{ return pObj->nFans;                                                                }

Dss_Obj_t* Dss_ObjFindOrAdd	(	Dss_Man_t *	p,
		int	Type,
		Vec_Int_t *	vFaninLits,
		word *	pTruth
	)

Definition at line 868 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth );
    if ( *pSpot )
        return Dss_VecObj( p->vObjs, *pSpot );
    *pSpot = Vec_PtrSize( p->vObjs );
    pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth );
    return pObj;
}

static unsigned Dss_ObjHashKey ( Dss_Man_t *  p, int  Type, Vec_Int_t *  vFaninLits, word *  pTruth  )

inlinestatic

Definition at line 836 of file dauTree.c.

{
    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
    int i, Entry;
    unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147;
    Vec_IntForEachEntry( vFaninLits, Entry, i )
        uHash += Entry * s_Primes[i & 0x7];
    assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) );
    if ( pTruth )
    {
        unsigned char * pTruthC = (unsigned char *)pTruth;
        int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits));
        for ( i = 0; i < nBytes; i++ )
            uHash += pTruthC[i] * s_Primes[i & 0x7];
    }
    return uHash % p->nBins;
}

unsigned* Dss_ObjHashLookup	(	Dss_Man_t *	p,
		int	Type,
		Vec_Int_t *	vFaninLits,
		word *	pTruth
	)

Definition at line 853 of file dauTree.c.

{
    Dss_Obj_t * pObj;
    unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth);
    for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id) )
    {
        pObj = Dss_VecObj( p->vObjs, *pSpot );
        if ( (int)pObj->Type == Type && 
             (int)pObj->nFans == Vec_IntSize(vFaninLits) && 
             !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) &&
             (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, Abc_TtByteNum(pObj->nFans))) ) // equal
            return pSpot;
    }
    return pSpot;
}

static int Dss_ObjId ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 111 of file dauTree.c.

{ return pObj->Id;                                                                   }

void Dss_ObjSort	(	Vec_Ptr_t *	p,
		Dss_Obj_t **	pNodes,
		int	nNodes,
		int *	pPerm
	)

Definition at line 664 of file dauTree.c.

{
    int i, j, best_i;
    for ( i = 0; i < nNodes-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nNodes; j++ )
            if ( Dss_ObjCompare(p, pNodes[best_i], pNodes[j]) == 1 )
                best_i = j;
        if ( i == best_i )
            continue;
        ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] );
        if ( pPerm )
            ABC_SWAP( int, pPerm[i], pPerm[best_i] );
    }
}

static int Dss_ObjSuppSize ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 113 of file dauTree.c.

{ return pObj->nSupp;                                                                }

static word* Dss_ObjTruth ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 108 of file dauTree.c.

{ return (word *)pObj + pObj->nWords;                                                }

static int Dss_ObjType ( Dss_Obj_t *  pObj )

inlinestatic

Definition at line 112 of file dauTree.c.

{ return pObj->Type;                                                                 }

static int Dss_ObjWordNum ( int  nFans )

inlinestatic

Definition at line 107 of file dauTree.c.

{ return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0);                      }

static Dss_Obj_t* Dss_Regular ( Dss_Obj_t *  p )

inlinestatic

Definition at line 100 of file dauTree.c.

{ return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);                                    }

static Dss_Obj_t* Dss_VecConst0 ( Vec_Ptr_t *  p )

inlinestatic

Definition at line 118 of file dauTree.c.

{ return Dss_VecObj( p, 0 );                                                         }

static int Dss_VecLitSuppSize ( Vec_Ptr_t *  p, int  iLit  )

inlinestatic

Definition at line 120 of file dauTree.c.

{ return Dss_VecObj( p, Abc_Lit2Var(iLit) )->nSupp;                                  }

static Dss_Obj_t* Dss_VecObj ( Vec_Ptr_t *  p, int  Id  )

inlinestatic

Definition at line 117 of file dauTree.c.

{ return (Dss_Obj_t *)Vec_PtrEntry(p, Id);                                           }

static Dss_Obj_t* Dss_VecVar ( Vec_Ptr_t *  p, int  v  )

inlinestatic

Definition at line 119 of file dauTree.c.

{ return Dss_VecObj( p, v+1 );                                                       }

static int Dss_WordCountOnes ( unsigned  uWord )

inlinestatic

Definition at line 139 of file dauTree.c.

{
    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
    return  (uWord & 0x0000FFFF) + (uWord>>16);
}

int Mpm_FuncCompute	(	Dss_Man_t *	p,
		int	iDsd0,
		int	iDsd1,
		Vec_Str_t *	vShared,
		int *	pPerm,
		int *	pnLeaves
	)

Definition at line 1693 of file dauTree.c.

{
    int fVerbose = 0;
//    int fCheck = 0;
    Dss_Ent_t * pEnt, ** ppSpot;
    Dss_Fun_t * pFun;
    int iDsd[2] = { iDsd0, iDsd1 };
    int i;
    abctime clk;

    assert( iDsd0 <= iDsd1 );
    if ( DAU_MAX_VAR < *pnLeaves )
    {
        printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
        return -1;
    }
    if ( fVerbose )
    {
        Dss_ManPrintOne( stdout, p, iDsd0, NULL );
        Dss_ManPrintOne( stdout, p, iDsd1, NULL );
    } 

clk = Abc_Clock();
    pEnt = Dss_ManSharedMapDerive( p, iDsd0, iDsd1, vShared );
    ppSpot = Dss_ManCacheLookup( p, pEnt );
p->timeLook += Abc_Clock() - clk;

clk = Abc_Clock();
    if ( *ppSpot == NULL )
    {
        if ( Vec_StrSize(vShared) == 0 )
            pFun = Dss_ManOperationFun( p, iDsd, *pnLeaves );
        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 <= *pnLeaves );
        // create cache entry
        *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
    }
    pFun = (*ppSpot)->pFunc;
p->timeDec += Abc_Clock() - clk;

    *pnLeaves = (int)pFun->nFans;
    for ( i = 0; i < (int)pFun->nFans; i++ )
        pPerm[i] = (int)pFun->pFans[i];

    if ( fVerbose )
    {
        Dss_ManPrintOne( stdout, p, pFun->iDsd, NULL );
        printf( "\n" );
    }

/*
    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;
}