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

Macros
#define	DAU_MAX_VAR 12
	INCLUDES ///. More...

#define	DAU_MAX_STR 2000

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

Typedefs
typedef struct Dss_Man_t_	Dss_Man_t

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
static int	Dau_DsdIsConst (char *p)
	MACRO DEFINITIONS ///. More...

static int	Dau_DsdIsConst0 (char *p)

static int	Dau_DsdIsConst1 (char *p)

static int	Dau_DsdIsVar (char *p)

static int	Dau_DsdReadVar (char *p)

unsigned	Abc_TtCanonicize (word pTruth, int nVars, char pCanonPerm)
	FUNCTION DECLARATIONS ///. More...

unsigned	Abc_TtCanonicizePhase (word *pTruth, int nVars)

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 ///. More...

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

#define DAU_MAX_STR 2000

Definition at line 43 of file dau.h.

#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.

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

Definition at line 44 of file dau.h.

Typedef Documentation

typedef struct Dss_Man_t_ Dss_Man_t

Definition at line 61 of file dau.h.

Enumeration Type Documentation

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

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

FUNCTION DECLARATIONS ///.

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

Synopsis [Semi-canonical form computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 895 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 );
     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;
 }

unsigned Abc_TtCanonicizePhase	(	word *	pTruth,
		int	nVars
	)

Definition at line 999 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;
 }

Vec_Int_t* Dau_DecFindSets	(	word *	pInit,
		int	nVars
	)

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

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

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

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

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

void Dau_DecPrintSets	(	Vec_Int_t *	vSets,
		int	nVars
	)

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

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

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

word Dau_Dsd6ToTruth ( char * p )

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

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

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

int* Dau_DsdComputeMatches ( char * p )

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

int Dau_DsdCountAnds ( char * pDsd )

Definition at line 316 of file dauDsd.c.

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

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

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

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

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

static int Dau_DsdIsConst ( char * p )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 67 of file dau.h.

67 { return (p[0] == '0' || p[0] == '1') && p[1] == 0; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

static int Dau_DsdIsConst0 ( char * p )

inlinestatic

Definition at line 68 of file dau.h.

68 { return p[0] == '0' && p[1] == 0; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

static int Dau_DsdIsConst1 ( char * p )

inlinestatic

Definition at line 69 of file dau.h.

69 { return p[0] == '1' && p[1] == 0; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

static int Dau_DsdIsVar ( char * p )

inlinestatic

Definition at line 70 of file dau.h.

70 { if ( *p == '!' ) p++; return *p >= 'a' && *p <= 'z'; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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

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[DAU_MAX_STR];
     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;
 }

void Dau_DsdNormalize ( char * p )

Definition at line 260 of file dauDsd.c.

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

void Dau_DsdPrintFromTruth	(	word *	pTruth,
		int	nVarsInit
	)

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

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

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

static int Dau_DsdReadVar ( char * p )

inlinestatic

Definition at line 71 of file dau.h.

71 { if ( *p == '!' ) p++; return *p - 'a'; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

void Dau_DsdRemoveBraces	(	char *	pDsd,
		int *	pMatches
	)

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 == '!' && *(q-1) == '!' && p != q )
             {
                 q--;
                 continue;
             }
             *q++ = *p;
         }
     *q = 0;
 }

word* Dau_DsdToTruth	(	char *	p,
		int	nVars
	)

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

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

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

void* Dsm_ManDeriveGia	(	void *	pGia,
		int	fUseMuxes
	)

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

Synopsis [Performs structural hashing on the LUT functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 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;
 }

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

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

Synopsis [Convert TT to GIA via DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 415 of file dauGia.c.

 {
     int fUseMuxes = 0;
     int fDelayBalance = 1;
     Gia_Man_t * pGia = (Gia_Man_t *)p;
     int nSizeNonDec;
     char pDsd[1000];
     m_Calls++;
     assert( Vec_IntSize(vLeaves) <= DAU_DSD_MAX_VAR );
     // 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( pTruth, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd, pVarLevels );
     }
     else
         nSizeNonDec = Dau_DsdDecompose( pTruth, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd );
     if ( nSizeNonDec )
         m_NonDsd++;
 //    printf( "%s\n", pDsd );
     if ( fDelayBalance )
         return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
     else
         return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
 }

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

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

int Dss_ManMerge	(	Dss_Man_t *	p,
		int *	iDsd,
		int *	nFans,
		int **	pFans,
		unsigned	uSharedMask,
		int	nKLutSize,
		unsigned char *	pPerm,
		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;
 }

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

Macros

Typedefs

Enumerations

Functions

Macro Definition Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation