dauMerge.c File Reference

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

Go to the source code of this file.

Data Structures
struct	Dau_Sto_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Dau_Sto_t_	Dau_Sto_t
	DECLARATIONS ///. More...

Functions
static void	Dau_DsdMergeStoreClean (Dau_Sto_t *pS, int nShared)
static void	Dau_DsdMergeStoreCleanOutput (Dau_Sto_t *pS)
static void	Dau_DsdMergeStoreAddToOutput (Dau_Sto_t *pS, char *pBeg, char *pEnd)
static void	Dau_DsdMergeStoreAddToOutputChar (Dau_Sto_t *pS, char c)
static int	Dau_DsdMergeStoreStartDef (Dau_Sto_t *pS, char c)
static void	Dau_DsdMergeStoreAddToDef (Dau_Sto_t *pS, int New, char *pBeg, char *pEnd)
static void	Dau_DsdMergeStoreAddToDefChar (Dau_Sto_t *pS, int New, char c)
static void	Dau_DsdMergeStoreStopDef (Dau_Sto_t *pS, int New, char c)
static char	Dau_DsdMergeStoreCreateDef (Dau_Sto_t *pS, char *pBeg, char *pEnd)
static void	Dau_DsdMergeStorePrintDefs (Dau_Sto_t *pS)
static void	Dau_DsdMergeCopy (char *pDsd, int fCompl, char *pRes)
static void	Dau_DsdMergeReplace (char *pDsd, int *pMatches, int *pMap)
static void	Dau_DsdMergeMatches (char *pDsd, int *pMatches)
static void	Dau_DsdMergeVarPres (char *pDsd, int *pMatches, int *pPres, int Mask)
static int	Dau_DsdMergeCountShared (int *pPres, int Mask)
static int	Dau_DsdMergeFindShared (char *pDsd0, char *pDsd1, int *pMatches0, int *pMatches1, int *pVarPres)
static int	Dau_DsdMergeCreateMaps (int *pVarPres, int nShared, int *pOld2New, int *pNew2Old)
static void	Dau_DsdMergeInlineDefinitions (char *pDsd, int *pMatches, Dau_Sto_t *pS, char *pRes, int nShared)
static void	Dau_DsdMergePrintWithStatus (char *p, int *pStatus)
int	Dau_DsdMergeStatus_rec (char *pStr, char **p, int *pMatches, int nShared, int *pStatus)
static int	Dau_DsdMergeStatus (char *pDsd, int *pMatches, int nShared, int *pStatus)
static int	Dau_DsdMergeGetStatus (char *pBeg, char *pStr, int *pMatches, int *pStatus)
void	Dau_DsdMergeSubstitute_rec (Dau_Sto_t *pS, char *pStr, char **p, int *pMatches, int *pStatus, int fWrite)
static void	Dau_DsdMergeSubstitute (Dau_Sto_t *pS, char *pDsd, int *pMatches, int *pStatus)
void	Dau_DsdRemoveBraces_rec (char *pStr, char **p, int *pMatches)
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...
void	Dau_DsdTest66 ()

Variables
abctime	s_TimeComp [4] = {0}

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Dau_Sto_t_ Dau_Sto_t

DECLARATIONS ///.

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

FileName [dauMerge.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis [Enumeration of decompositions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Substitution storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file dauMerge.c.

Function Documentation

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

static void Dau_DsdMergeCopy ( char *  pDsd, int  fCompl, char *  pRes  )

inlinestatic

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

Synopsis [Creates local copy.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file dauMerge.c.

{
    if ( fCompl && pDsd[0] == '!' )
        fCompl = 0, pDsd++;
    if ( Dau_DsdIsConst(pDsd) ) // constant
        pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0;
    else
        sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd );
}

static int Dau_DsdMergeCountShared ( int *  pPres, int  Mask  )

inlinestatic

Definition at line 197 of file dauMerge.c.

{
    int i, Counter = 0;
    for ( i = 0; i < DAU_MAX_VAR; i++ )
        Counter += (pPres[i] == Mask);
    return Counter;
}

static int Dau_DsdMergeCreateMaps ( int *  pVarPres, int  nShared, int *  pOld2New, int *  pNew2Old  )

inlinestatic

Definition at line 211 of file dauMerge.c.

{
    int i, Counter = 0, Counter2 = nShared;
    for ( i = 0; i < DAU_MAX_VAR; i++ )
    {
        if ( pVarPres[i] == 0 )
            continue;
        if ( pVarPres[i] == 3 )
        {
            pOld2New[i] = Counter;
            pNew2Old[Counter] = i;
            Counter++;
            continue;
        }
        assert( pVarPres[i] == 1 || pVarPres[i] == 2 );
        pOld2New[i] = Counter2;
        pNew2Old[Counter2] = i;
        Counter2++;
    }
    return Counter2;
}

static int Dau_DsdMergeFindShared ( char *  pDsd0, char *  pDsd1, int *  pMatches0, int *  pMatches1, int *  pVarPres  )

inlinestatic

Definition at line 204 of file dauMerge.c.

{
    memset( pVarPres, 0, sizeof(int)*DAU_MAX_VAR );
    Dau_DsdMergeVarPres( pDsd0, pMatches0, pVarPres, 1 );
    Dau_DsdMergeVarPres( pDsd1, pMatches1, pVarPres, 2 );
    return Dau_DsdMergeCountShared( pVarPres, 3 );
}

static int Dau_DsdMergeGetStatus ( char *  pBeg, char *  pStr, int *  pMatches, int *  pStatus  )

inlinestatic

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

Synopsis [Extracts the formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 362 of file dauMerge.c.

{
    if ( *pBeg == '!' )
        pBeg++;
    while ( (*pBeg >= 'A' && *pBeg <= 'F') || (*pBeg >= '0' && *pBeg <= '9') )
        pBeg++;
    if ( *pBeg == '<' )
    {
        char * q = pStr + pMatches[pBeg - pStr];
        if ( *(q+1) == '{' )
            pBeg = q+1;
    }
    return pStatus[pBeg - pStr];
}

static void Dau_DsdMergeInlineDefinitions ( char *  pDsd, int *  pMatches, Dau_Sto_t *  pS, char *  pRes, int  nShared  )

inlinestatic

Definition at line 232 of file dauMerge.c.

{
    int i;
    char * pDef;
    char * pBegin = pRes;
    for ( i = 0; pDsd[i]; i++ )
    {
        // skip non-DSD block
        if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
        {
            assert( pDsd[pMatches[i]] == '>' );
            for ( ; i <= pMatches[i]; i++ )
                *pRes++ = pDsd[i];
        }
        if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
            while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
                *pRes++ = pDsd[i++];
        // detect variables
        if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') || (pDsd[i] - 'a' < nShared) )
        {
            *pRes++ = pDsd[i];
            continue;
        }
        // inline definition
        assert( pDsd[i]-'a' < DAU_MAX_STR );
        for ( pDef = pS->pStore[pDsd[i]-'a']; *pDef; pDef++ )
            *pRes++ = *pDef;
    }
    *pRes++ = 0;
    assert( pRes - pBegin < DAU_MAX_STR );
}

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

inlinestatic

Definition at line 163 of file dauMerge.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 );
}

static void Dau_DsdMergePrintWithStatus ( char *  p, int *  pStatus  )

inlinestatic

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

Synopsis [Computes independence status for each opening paranthesis.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file dauMerge.c.

{
    int i;
    printf( "%s\n", p );
    for ( i = 0; p[i]; i++ )
        if ( !(p[i] == '(' || p[i] == '[' || p[i] == '<' || p[i] == '{' || (p[i] >= 'a' && p[i] <= 'z')) )
            printf( " " );
        else if ( pStatus[i] >= 0 )
            printf( "%d", pStatus[i] );
        else
            printf( "-" );
    printf( "\n" );
}

static void Dau_DsdMergeReplace ( char *  pDsd, int *  pMatches, int *  pMap  )

inlinestatic

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

Synopsis [Replaces variables according to the mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file dauMerge.c.

{
    int i;
    for ( i = 0; pDsd[i]; i++ )
    {
        // skip non-DSD block
        if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
            i = pMatches[i] + 1;
        if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
            while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
                i++;
        // detect variables
        if ( pDsd[i] >= 'a' && pDsd[i] <= 'z' )
            pDsd[i] = 'a' + pMap[ pDsd[i] - 'a' ];
    }
}

static int Dau_DsdMergeStatus ( char *  pDsd, int *  pMatches, int  nShared, int *  pStatus  )

inlinestatic

Definition at line 346 of file dauMerge.c.

{
    return Dau_DsdMergeStatus_rec( pDsd, &pDsd, pMatches, nShared, pStatus );
}

int Dau_DsdMergeStatus_rec	(	char *	pStr,
		char **	p,
		int *	pMatches,
		int	nShared,
		int *	pStatus
	)

Definition at line 289 of file dauMerge.c.

{
    // none pure
    // 1 one pure
    // 2 two or more pure
    // 3 all pure
    if ( **p == '!' )
    {
        pStatus[*p - pStr] = -1;
        (*p)++;
    }
    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
    {
        pStatus[*p - pStr] = -1;
        (*p)++;
    }
    if ( **p == '<' )
    {
        char * q = pStr + pMatches[ *p - pStr ];
        if ( *(q+1) == '{' )
        {
            char * pTemp = *p;
            *p = q+1;
            for ( ; pTemp < q+1; pTemp++ )
                pStatus[pTemp - pStr] = -1;
        }
    }
    if ( **p >= 'a' && **p <= 'z' ) // var
        return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3;
    if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
    {
        int Status, nPure = 0, nTotal = 0;
        char * pOld = *p;
        char * q = pStr + pMatches[ *p - pStr ];
        assert( *q == **p + 1 + (**p != '(') );
        for ( (*p)++; *p < q; (*p)++ )
        {
            Status = Dau_DsdMergeStatus_rec( pStr, p, pMatches, nShared, pStatus );
            nPure += (Status == 3);
            nTotal++;
        }
        assert( *p == q );
        assert( nTotal > 1 );
        if ( nPure == 0 )
            Status = 0;
        else if ( nPure == 1 )
            Status = 1;
        else if ( nPure < nTotal )
            Status = 2;
        else if ( nPure == nTotal ) 
            Status = 3;
        else assert( 0 );
        return (pStatus[pOld - pStr] = Status);
    }
    assert( 0 );
    return 0;
}

static void Dau_DsdMergeStoreAddToDef ( Dau_Sto_t *  pS, int  New, char *  pBeg, char *  pEnd  )

inlinestatic

Definition at line 85 of file dauMerge.c.

{
    while ( pBeg < pEnd )
        *pS->pPosStore[New]++ = *pBeg++;
}

static void Dau_DsdMergeStoreAddToDefChar ( Dau_Sto_t *  pS, int  New, char  c  )

inlinestatic

Definition at line 90 of file dauMerge.c.

{
    *pS->pPosStore[New]++ = c;
}

static void Dau_DsdMergeStoreAddToOutput ( Dau_Sto_t *  pS, char *  pBeg, char *  pEnd  )

inlinestatic

Definition at line 69 of file dauMerge.c.

{
    while ( pBeg < pEnd )
        *pS->pPosOutput++ = *pBeg++;
}

static void Dau_DsdMergeStoreAddToOutputChar ( Dau_Sto_t *  pS, char  c  )

inlinestatic

Definition at line 74 of file dauMerge.c.

{
    *pS->pPosOutput++ = c;
}

static void Dau_DsdMergeStoreClean ( Dau_Sto_t *  pS, int  nShared  )

inlinestatic

Definition at line 57 of file dauMerge.c.

{
    int i;
    pS->iVarUsed  = nShared;
    for ( i = 0; i < DAU_MAX_VAR; i++ )
        pS->pStore[i][0] = 0;
}

static void Dau_DsdMergeStoreCleanOutput ( Dau_Sto_t *  pS )

inlinestatic

Definition at line 65 of file dauMerge.c.

{
    pS->pPosOutput = pS->pOutput;
}

static char Dau_DsdMergeStoreCreateDef ( Dau_Sto_t *  pS, char *  pBeg, char *  pEnd  )

inlinestatic

Definition at line 100 of file dauMerge.c.

{
    int New = Dau_DsdMergeStoreStartDef( pS, 0 );
    Dau_DsdMergeStoreAddToDef( pS, New, pBeg, pEnd );
    Dau_DsdMergeStoreStopDef( pS, New, 0 );
    return New;
}

static void Dau_DsdMergeStorePrintDefs ( Dau_Sto_t *  pS )

inlinestatic

Definition at line 107 of file dauMerge.c.

{
    int i;
    for ( i = 0; i < DAU_MAX_VAR; i++ )
        if ( pS->pStore[i][0] )
            printf( "%c = %s\n", 'a' + i, pS->pStore[i] );
}

static int Dau_DsdMergeStoreStartDef ( Dau_Sto_t *  pS, char  c  )

inlinestatic

Definition at line 79 of file dauMerge.c.

{
    pS->pPosStore[pS->iVarUsed] = pS->pStore[pS->iVarUsed];
    if (c) *pS->pPosStore[pS->iVarUsed]++ = c;
    return pS->iVarUsed++;
}

static void Dau_DsdMergeStoreStopDef ( Dau_Sto_t *  pS, int  New, char  c  )

inlinestatic

Definition at line 94 of file dauMerge.c.

{
    if (c) *pS->pPosStore[New]++ = c;
    *pS->pPosStore[New]++ = 0;
}

static void Dau_DsdMergeSubstitute ( Dau_Sto_t *  pS, char *  pDsd, int *  pMatches, int *  pStatus  )

inlinestatic

Definition at line 494 of file dauMerge.c.

{
/*
    int fCompl = 0;
    if ( pDsd[0] == '!' )
    {
        Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
        pDsd++;
        fCompl = 1;
    }
*/
    Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 );
    Dau_DsdMergeStoreAddToOutputChar( pS, 0 );
}

void Dau_DsdMergeSubstitute_rec	(	Dau_Sto_t *	pS,
		char *	pStr,
		char **	p,
		int *	pMatches,
		int *	pStatus,
		int	fWrite
	)

Definition at line 376 of file dauMerge.c.

{
//    assert( **p != '!' );

    if ( **p == '!' )
    {
        if ( fWrite )
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
        (*p)++;
    }

    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
    {
        if ( fWrite )
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
        (*p)++;
    }
    if ( **p == '<' )
    {
        char * q = pStr + pMatches[ *p - pStr ];
        if ( *(q+1) == '{' )
        {
            char * pTemp = *p;
            *p = q+1;
            if ( fWrite )
                for ( ; pTemp < q+1; pTemp++ )
                    Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp );
        }
    }
    if ( **p >= 'a' && **p <= 'z' ) // var
    {
        if ( fWrite )
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
        return;
    }
    if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
    {
        int New, StatusFan, Status = pStatus[*p - pStr];
        char * pBeg, * q = pStr + pMatches[ *p - pStr ];
        assert( *q == **p + 1 + (**p != '(') );
        if ( !fWrite )
        {
             assert( Status == 3 );
             *p = q;
             return;
        }
        assert( Status != 3 );
        if ( Status == 0 ) // none pure
        {
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            for ( (*p)++; *p < q; (*p)++ )
            {
                if ( **p == '!' )
                {
                    Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
                    (*p)++;
                }
                Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, 1 );
            }
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            assert( *p == q );
            return;
        }
        if ( Status == 1 || **p == '<' || **p == '{' ) // 1 pure
        {
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            for ( (*p)++; *p < q; (*p)++ )
            {
                if ( **p == '!' )
                {
                    Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
                    (*p)++;
                }
                pBeg = *p;
                StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
                Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
                if ( StatusFan == 3 )
                {
                    int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 );
                    Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
                }
            }
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            assert( *p == q );
            return;
        }
        if ( Status == 2 )
        {
            // add more than one defs
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            New = Dau_DsdMergeStoreStartDef( pS, **p );
            for ( (*p)++; *p < q; (*p)++ )
            {
                pBeg = *p;
                StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
                if ( **p == '!' )
                {
                    if ( StatusFan != 3 )
                        Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
                    else
                        Dau_DsdMergeStoreAddToDefChar( pS, New, '!' );
                    (*p)++;
                    pBeg++;
                }
                Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
                if ( StatusFan == 3 )
                    Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 );
            }
            Dau_DsdMergeStoreStopDef( pS, New, *q );
            Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
            Dau_DsdMergeStoreAddToOutputChar( pS, **p );
            return;
        }
        assert( 0 );
        return;
    }
    assert( 0 );
}

static void Dau_DsdMergeVarPres ( char *  pDsd, int *  pMatches, int *  pPres, int  Mask  )

inlinestatic

Definition at line 178 of file dauMerge.c.

{
    int i;
    for ( i = 0; pDsd[i]; i++ )
    {
        // skip non-DSD block
        if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
            i = pMatches[i] + 1;
        if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
            while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
                i++;
        // skip non-variables
        if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') )
            continue;
        // record the mask
        assert( pDsd[i]-'a' < DAU_MAX_VAR );
        pPres[pDsd[i]-'a'] |= Mask;
    }
}

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

void Dau_DsdRemoveBraces_rec	(	char *	pStr,
		char **	p,
		int *	pMatches
	)

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

Synopsis [Removes braces.]

Description []

SideEffects []

SeeAlso []

Definition at line 520 of file dauMerge.c.

{
    if ( **p == '!' )
        (*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;
    if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) 
    {
        char * q = pStr + pMatches[ *p - pStr ];
        assert( *q == **p + 1 + (**p != '(') );
        for ( (*p)++; *p < q; (*p)++ )
        {
            int fCompl = (**p == '!');
            char * pBeg = fCompl ? *p + 1 : *p;
            Dau_DsdRemoveBraces_rec( pStr, p, pMatches );
            if ( (!fCompl && *pBeg == '(' && *q == ')') || (*pBeg == '[' && *q == ']') )
            {
                assert( **p == ')' || **p == ']' );
                *pBeg = **p = ' ';
            }
        }
        assert( *p == q );
        return;
    }
    assert( 0 );
}

void Dau_DsdTest66

(

)

Definition at line 771 of file dauMerge.c.

{
    int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 };
//    int pMatches[DAU_MAX_STR];
//    int pStatus[DAU_MAX_STR];

//    char * pStr = "(!(!a<bcd>)!(!fe))";
//    char * pStr = "([acb]<!edf>)";
//    char * pStr = "!(f!(b!c!(d[ea])))";
    char * pStr = "[!(a[be])!(c!df)]";
//    char * pStr = "<(e<bca>)fd>";
//    char * pStr = "[d8001{abef}c]";
//    char * pStr1 = "(abc)";
//    char * pStr2 = "[adf]";
//    char * pStr1 = "(!abce)";
//    char * pStr2 = "[adf!b]";
//    char * pStr1 = "(!abc)";
//    char * pStr2 = "[ab]";
//    char * pStr1 = "[d81{abe}c]";
//    char * pStr1 = "[d<a(bc)(!b!c)>{abe}c]";
//    char * pStr1 = "[d81{abe}c]";
//    char * pStr1 = "[d(a[be])c]";
//    char * pStr2 = "(df)";
//    char * pStr1 = "(abf)";
//    char * pStr2 = "(a[(bc)(fde)])";
//    char * pStr1 = "8001{abc[ef]}";
//    char * pStr2 = "(abe)";

    char * pStr1 = "(!(ab)de)";
    char * pStr2 = "(!(ac)f)";

    char * pRes;
    word t = Dau_Dsd6ToTruth( pStr );
    return;

//    pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL );
//    Dau_DsdNormalize( pStr2 );

//    Dau_DsdMergeMatches( pStr, pMatches );
//    Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
//    Dau_DsdMergePrintWithStatus( pStr, pStatus );

    pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0, 6 );

    t = 0; 
}

Variable Documentation

abctime s_TimeComp[4] = {0}

Definition at line 574 of file dauMerge.c.