dauNonDsd.c File Reference

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

Include dependency graph for dauNonDsd.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Dau_DecCheckSetTop5 (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
	DECLARATIONS ///.
int	Dau_DecCheckSetTop6 (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
int	Dau_DecCheckSetTopOld (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word **pCof0, word **pCof1, word **pDec)
void	Dau_DecSortSet (unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
void	Dau_DecPrintSet (unsigned set, int nVars, int fNewLine)
unsigned	Dau_DecReadSet (char *pStr)
void	Dau_DecPrintSets (Vec_Int_t *vSets, int nVars)
void	Dau_DecMoveFreeToLSB (word *p, int nVars, int *V2P, int *P2V, int maskB, int sizeB)
Vec_Int_t *	Dau_DecFindSets_int (word *pInit, int nVars, int *pSched[16])
Vec_Int_t *	Dau_DecFindSets (word *pInit, int nVars)
void	Dau_DecFindSetsTest2 ()
void	Dau_DecVarReplace (char *pStr, int *pPerm, int nVars)
int	Dau_DecDecomposeSet (word *pInit, int nVars, unsigned uSet, word *pComp, word *pDec, int *pPermC, int *pPermD, int *pnVarsC, int *pnVarsD, int *pnVarsS)
int	Dau_DecVerify (word *pInit, int nVars, char *pDsdC, char *pDsdD)
int	Dau_DecPerform6 (word *p, int nVars, unsigned uSet)
int	Dau_DecPerform (word *pInit, int nVars, unsigned uSet)
void	Dau_DecTrySets (word *pInit, int nVars, int fVerbose)
void	Dau_DecFindSetsTest3 ()
void	Dau_DecFindSetsTest ()

Function Documentation

Dau_DecCheckSetTop5()

ABC_NAMESPACE_IMPL_START int Dau_DecCheckSetTop5	(	word *	p,
		int	nVars,
		int	nVarsF,
		int	nVarsB,
		int	nVarsS,
		int	uMaskS,
		int *	pSched,
		word *	pDec,
		word *	pComp )

DECLARATIONS ///.

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

FileName [dauNonDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Checks decomposability with given variable set.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file dauNonDsd.c.

{
    word Cof[2][64], Value;
    word MaskFF = (((word)1) << (1 << nVarsF)) - 1;
    int ShiftF = 6 - nVarsF, MaskF = (1 << ShiftF) - 1;
    int pVarsS[16], pVarsB[16];
    int nMints  = (1 << nVarsB);
    int nMintsB = (1 <<(nVarsB-nVarsS));
    int nMintsS = (1 << nVarsS);
    int s, b, v, m, Mint, MintB, MintS;
    assert( nVars == nVarsB + nVarsF );
    assert( nVars <= 16 );
    assert( nVarsS <= 6 );
    assert( nVarsF >= 1 && nVarsF <= 5 );
    // collect bound/shared variables
    for ( s = b = v = 0; v < nVarsB; v++ )
        if ( (uMaskS >> v) & 1 )
            pVarsB[v] = -1, pVarsS[v] = s++;
        else
            pVarsS[v] = -1, pVarsB[v] = b++;
    assert( s == nVarsS );
    assert( b == nVarsB-nVarsS );
    // clean minterm storage
    for ( s = 0; s < nMintsS; s++ )
        Cof[0][s] = Cof[1][s] = ~(word)0;
    // iterate through bound set minters
    for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
    {
        // find minterm value
        Value = (p[Mint>>ShiftF] >> ((Mint&MaskF)<<nVarsF)) & MaskFF;
        // check if this cof already appeared 
        if ( !~Cof[0][MintS] || Cof[0][MintS] == Value )
            Cof[0][MintS] = Value;
        else if ( !~Cof[1][MintS] || Cof[1][MintS] == Value )
        {
            Cof[1][MintS] = Value;
            if ( pDec ) 
            {
                int iMintB = MintS * nMintsB + MintB;
                pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));     
            }
        }
        else
            return 0;            
        // find next minterm
        v = pSched[m];
        Mint ^= (1 << v);
        if ( (uMaskS >> v) & 1 ) // shared variable
            MintS ^= (1 << pVarsS[v]);
        else
            MintB ^= (1 << pVarsB[v]);
    }
    // create composition function
    if ( pComp )
    {
        for ( s = 0; s < nMintsS; s++ )
        {
            pComp[s>>ShiftF] |= (Cof[0][s] << ((s&MaskF) << nVarsF));
            if ( ~Cof[1][s] ) 
                pComp[(s+nMintsS)>>ShiftF] |= (Cof[1][s] << (((s+nMintsS)&MaskF) << nVarsF));
            else
                pComp[(s+nMintsS)>>ShiftF] |= (Cof[0][s] << (((s+nMintsS)&MaskF) << nVarsF));
        }
        if ( nVarsF + nVarsS + 1 < 6 )
            pComp[0] = Abc_Tt6Stretch( pComp[0], nVarsF + nVarsS + 1 );
    }
    if ( pDec && nVarsB < 6 )
        pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
    return 1;
}

Dau_DecCheckSetTop6()

int Dau_DecCheckSetTop6	(	word *	p,
		int	nVars,
		int	nVarsF,
		int	nVarsB,
		int	nVarsS,
		int	uMaskS,
		int *	pSched,
		word *	pDec,
		word *	pComp )

Definition at line 116 of file dauNonDsd.c.

{
    word * Cof[2][64];
    int nWordsF = Abc_TtWordNum(nVarsF); 
    int pVarsS[16], pVarsB[16];
    int nMints  = (1 << nVarsB);
    int nMintsB = (1 <<(nVarsB-nVarsS));
    int nMintsS = (1 << nVarsS);
    int s, b, v, m, Mint, MintB, MintS;
    assert( nVars == nVarsB + nVarsF );
    assert( nVars <= 16 );
    assert( nVarsS <= 6 );
    assert( nVarsF >= 6 );
    // collect bound/shared variables
    for ( s = b = v = 0; v < nVarsB; v++ )
        if ( (uMaskS >> v) & 1 )
            pVarsB[v] = -1, pVarsS[v] = s++;
        else
            pVarsS[v] = -1, pVarsB[v] = b++;
    assert( s == nVarsS );
    assert( b == nVarsB-nVarsS );
    // clean minterm storage
    for ( s = 0; s < nMintsS; s++ )
        Cof[0][s] = Cof[1][s] = NULL;
    // iterate through bound set minters
    for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
    {
        // check if this cof already appeared 
        if ( !Cof[0][MintS] || !memcmp(Cof[0][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
            Cof[0][MintS] = p + Mint * nWordsF;
        else if ( !Cof[1][MintS] || !memcmp(Cof[1][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
        {
            Cof[1][MintS] = p + Mint * nWordsF;
            if ( pDec ) 
            {
                int iMintB = MintS * nMintsB + MintB;
                pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));     
            }
        }
        else
            return 0;            
        // find next minterm
        v = pSched[m];
        Mint ^= (1 << v);
        if ( (uMaskS >> v) & 1 ) // shared variable
            MintS ^= (1 << pVarsS[v]);
        else
            MintB ^= (1 << pVarsB[v]);
    }
    // create composition function
    if ( pComp )
    {
        for ( s = 0; s < nMintsS; s++ )
        {
            memcpy( pComp + s * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
            if ( Cof[1][s] ) 
                memcpy( pComp + (s+nMintsS) * nWordsF, Cof[1][s], sizeof(word) * nWordsF );
            else
                memcpy( pComp + (s+nMintsS) * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
        }
    }
    if ( pDec && nVarsB < 6 )
        pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
    return 1;
}

Here is the call graph for this function:

Dau_DecCheckSetTopOld()

int Dau_DecCheckSetTopOld	(	word *	p,
		int	nVars,
		int	nVarsF,
		int	nVarsB,
		int	nVarsS,
		int	maskS,
		word **	pCof0,
		word **	pCof1,
		word **	pDec )

Definition at line 297 of file dauNonDsd.c.

{
    int i, pVarsS[16];
    int v, m, mMax = (1 << nVarsS), uMaskValue;
    assert( nVars >= 3 && nVars <= 16 );
    assert( nVars == nVarsF + nVarsB );
    assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
    assert( nVarsB >= 2 && nVarsB <= nVars - 1 );
    assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 );
    if ( nVarsS == 0 )
        return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 );
    // collect shared variables
    assert( maskS > 0 && maskS < (1 << nVarsB) );
    for ( i = 0, v = 0; v < nVarsB; v++ )
        if ( (maskS >> v) & 1 )
            pVarsS[i++] = v;
    assert( i == nVarsS );
    // go through shared set minterms
    for ( m = 0; m < mMax; m++ )
    {
        // generate share set mask
        uMaskValue = 0;
        for ( v = 0; v < nVarsS; v++ )
            if ( (m >> v) & 1 )
                uMaskValue |= (1 << pVarsS[v]);
        assert( (maskS & uMaskValue) == uMaskValue );
        // check decomposition
        if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) )
            return 0;
    }
   return 1;
}

Here is the caller graph for this function:

Dau_DecDecomposeSet()

int Dau_DecDecomposeSet	(	word *	pInit,
		int	nVars,
		unsigned	uSet,
		word *	pComp,
		word *	pDec,
		int *	pPermC,
		int *	pPermD,
		int *	pnVarsC,
		int *	pnVarsD,
		int *	pnVarsS )

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

Synopsis [Decomposes with the given bound-set.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file dauNonDsd.c.

{
    word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64];
    word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD;
    int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16];
    int nVarsU = 0, nVarsS = 0, nVarsF = 0;
    int nWords = Abc_TtWordNum(nVars);
    int v, d, c, Status, nDecs;
    assert( nVars <= 16 );
    for ( v = 0; v < nVars; v++ )
        V2P[v] = P2V[v] = v;
    memcpy( p, pInit, sizeof(word) * nWords );
    // sort variables
    for ( v = 0; v < nVars; v++ )
    {
        int Value = (uSet >> (v<<1)) & 3;
        if ( Value == 0 )
            pVarsF[nVarsF++] = v;
        else if ( Value == 1 )
            pVarsU[nVarsU++] = v;
        else if ( Value == 3 )
            pVarsS[nVarsS++] = v;
        else assert(0);
    }
    assert( nVarsS >= 0 && nVarsS <= 6 );
    assert( nVarsF + nVarsS + 1 <= 6 );
    assert( nVarsU + nVarsS <= 6 );
    // init space for decomposition functions
    nDecs = (1 << nVarsS);
    for ( d = 0; d < nDecs; d++ )
    {
        pCof0[d] = Cof0 + d;
        pCof1[d] = Cof1 + d;
        pDecs[d] = Decs + d;
    }
    // permute variables
    c = 0;
    for ( v = 0; v < nVarsF; v++ )
       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ );
    for ( v = 0; v < nVarsS; v++ )
       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ );
    for ( v = 0; v < nVarsU; v++ )
       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ );
    assert( c == nVars );
    // check decomposition
    Status = Dau_DecCheckSetTopOld( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs );
    if ( !Status )
        return 0;
    // compute cofactors
    assert( nVarsF + nVarsS < 6 );
    for ( d = 0; d < nDecs; d++ )
    {
        Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]);
        pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU );
    }
    // compute the resulting functions
    pComp[0] = 0;
    pDec[0] = 0;
    for ( d = 0; d < nDecs; d++ )
    {
        // compute minterms for composition/decomposition function
        MintC = MintD = ~((word)0);
        for ( v = 0; v < nVarsS; v++ )
        {
            MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
            MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
        }
        // derive functions
        pComp[0] |= MintC & Cof[d];
        pDec[0] |= MintD & pDecs[d][0];
    }
    // derive variable permutations
    if ( pPermC )
    {
        for ( v = 0; v < nVarsF; v++ )
            pPermC[v] = pVarsF[v];
        for ( v = 0; v < nVarsS; v++ )
            pPermC[nVarsF+v] = pVarsS[v];
        pPermC[nVarsF + nVarsS] = nVars;
    }
    if ( pPermD )
    {
        for ( v = 0; v < nVarsU; v++ )
            pPermD[v] = pVarsU[v];
        for ( v = 0; v < nVarsS; v++ )
            pPermD[nVarsU+v] = pVarsS[v];
    }
    if ( pnVarsC )
        *pnVarsC = nVarsF + nVarsS + 1;
    if ( pnVarsD )
        *pnVarsD = nVarsU + nVarsS;
    if ( pnVarsS )
        *pnVarsS = nVarsS;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecFindSets()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecFindSets_int()

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

Definition at line 462 of file dauNonDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecFindSetsTest()

void Dau_DecFindSetsTest

(

)

Definition at line 877 of file dauNonDsd.c.

{
    int nVars = 6;
//    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
//    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
//    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
//    word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
//    word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
//    word t = ABC_CONST(0x00000000901FFFFF); // some funct
    word t = ABC_CONST(0x000030F00D0D3FFF); // some funct
//    word t = ABC_CONST(0x00000000690006FF); // some funct
//    word t = ABC_CONST(0x7000F80007FF0FFF); // some funct
//    word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var
//    word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
//    word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
    Dau_DecTrySets( &t, nVars, 1 );
}

Here is the call graph for this function:

Dau_DecFindSetsTest2()

void Dau_DecFindSetsTest2

(

)

Definition at line 527 of file dauNonDsd.c.

{
    Vec_Int_t * vSets;
    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
//    word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
//    word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
//    word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
//    word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
    int nVars = 5;
 
    vSets   = Dau_DecFindSets( &t, nVars );
    Dau_DecPrintSets( vSets, nVars );
    Vec_IntFree( vSets );
}

Here is the call graph for this function:

Dau_DecFindSetsTest3()

void Dau_DecFindSetsTest3

(

)

Definition at line 863 of file dauNonDsd.c.

{
    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
    int nVars = 6;
    char * pStr = "Bcd";
//    char * pStr = "Abcd";
//    char * pStr = "ab";
    unsigned uSet = Dau_DecReadSet( pStr );
    Dau_DecPerform6( &t, nVars, uSet );
}

Here is the call graph for this function:

Dau_DecMoveFreeToLSB()

void Dau_DecMoveFreeToLSB	(	word *	p,
		int	nVars,
		int *	V2P,
		int *	P2V,
		int	maskB,
		int	sizeB )

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

Synopsis [Find decomposable bound-sets of the given function.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file dauNonDsd.c.

{
    int v, c = 0;
    for ( v = 0; v < nVars; v++ )
        if ( !((maskB >> v) & 1) )
            Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
    assert( c == nVars - sizeB );
}

Here is the caller graph for this function:

Dau_DecPerform()

int Dau_DecPerform	(	word *	pInit,
		int	nVars,
		unsigned	uSet )

Definition at line 771 of file dauNonDsd.c.

{
    word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words
    char pDsdC[5000], pDsdD[5000];  // at most 2^12 hex digits
    int nVarsU, nVarsS, nVarsF, nVarsC = 0, nVarsD = 0;
    int V2P[16], P2V[16], pPermC[16], pPermD[16], * pSched;
    int v, i, status, ResC, ResD;
    int nWords = Abc_TtWordNum(nVars);
    assert( nVars <= 16 );
    // backup the function
    memcpy( p, pInit, sizeof(word) * nWords );
    // get variable numbers
    Dau_DecSortSet( uSet, nVars, &nVarsU, &nVarsS, &nVarsF );
    // permute function and order variables
    for ( v = 0; v < nVars; v++ )
        V2P[v] = P2V[v] = v;
    for ( i = v = 0; v < nVars; v++ )
        if ( ((uSet >> (v<<1)) & 3) == 0 ) // free first
           Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
    for ( v = 0; v < nVars; v++ )
        if ( ((uSet >> (v<<1)) & 3) == 3 ) // share second
           Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
    pPermC[nVarsC++] = nVars;
    for ( v = 0; v < nVars; v++ )
        if ( ((uSet >> (v<<1)) & 3) == 1 ) // unique last
           Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermD[nVarsD++] = v;
    for ( v = 0; v < nVarsS; v++ )
        pPermD[nVarsD++] = pPermC[nVarsF+v];
    assert( nVarsD == nVarsU + nVarsS );
    assert( nVarsC == nVarsF + nVarsS + 1 );
    assert( i == nVars );
    // decompose
    pSched = Extra_GreyCodeSchedule( nVarsU + nVarsS );
    memset( pDec, 0, sizeof(word) * Abc_TtWordNum(nVarsD) );
    memset( pComp, 0, sizeof(word) * Abc_TtWordNum(nVarsC) );
    status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsU + nVarsS, nVarsS, nVarsS ? Abc_InfoMask(nVarsS) : 0, pSched, pDec, pComp );
    ABC_FREE( pSched );
    if ( !status )
    {
        printf( "  Decomposition does not exist\n" );
        return 0;
    }
//    Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" );
//    Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" );
//    Kit_DsdPrintFromTruth( (unsigned *)pComp, 6 ); printf( "\n" );
//    Kit_DsdPrintFromTruth( (unsigned *)pDec, 6 );  printf( "\n" );
    // decompose
    ResC = Dau_DsdDecompose( pComp, nVarsC, 0, 1, pDsdC );
    ResD = Dau_DsdDecompose( pDec, nVarsD, 0, 1, pDsdD );
    // replace variables
    Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
    Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
    // report
    printf( "     " );
    printf( "%3d : ", 0 );
    printf( "%24s  ", pDsdD );
    printf( "%24s  ", pDsdC );
    Dau_DecVerify( pInit, nVars, pDsdC, pDsdD );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecPerform6()

int Dau_DecPerform6	(	word *	p,
		int	nVars,
		unsigned	uSet )

Definition at line 714 of file dauNonDsd.c.

{
    word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD;
    char pDsdC[1000], pDsdD[1000];
    int pPermC[16], pPermD[16];
    int nVarsC, nVarsD, nVarsS, nVarsU, nVarsF, nPairs;
    int i, m, v, status, ResC, ResD, Counter = 0;
    status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec0, pPermC, pPermD, &nVarsC, &nVarsD, &nVarsS );
    if ( !status )
    {
        printf( "  Decomposition does not exist\n" );
        return 0;
    }
    nVarsU = nVarsD - nVarsS;
    nVarsF = nVarsC - nVarsS - 1;
    tComp0 = Abc_Tt6Cofactor0( tComp, nVarsF + nVarsS );
    tComp1 = Abc_Tt6Cofactor1( tComp, nVarsF + nVarsS );
    nPairs = 1 << (1 << nVarsS); 
    for ( i = 0; i < nPairs; i++ )
    {
        if ( i & 1 )
            continue;
        // create miterms with this polarity
        FuncC = FuncD = 0;
        for ( m = 0; m < (1 << nVarsS); m++ )
        {
            word MintC, MintD;
            if ( !((i >> m) & 1) )
                continue;
            MintC = MintD = ~(word)0;
            for ( v = 0; v < nVarsS; v++ )
            {
                MintC &= ((m >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
                MintD &= ((m >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
            }
            FuncC |= MintC;
            FuncD |= MintD;
        }
        // uncomplement given variables
        tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~FuncC) | (tComp1 & FuncC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~FuncC) | (tComp0 & FuncC)));
        tDec = tDec0 ^ FuncD;
        // decompose
        ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC );
        ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD );
        // replace variables
        Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
        Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
        // report
//        printf( "  " );
        printf( "%3d : ", Counter++ );
        printf( "%24s  ", pDsdD );
        printf( "%24s  ", pDsdC );
        Dau_DecVerify( p, nVars, pDsdC, pDsdD );
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecPrintSet()

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

Definition at line 390 of file dauNonDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecPrintSets()

void Dau_DecPrintSets	(	Vec_Int_t *	vSets,
		int	nVars )

Definition at line 434 of file dauNonDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecReadSet()

unsigned Dau_DecReadSet

(

char *

pStr

)

Definition at line 421 of file dauNonDsd.c.

{
    unsigned uSet = 0; int v;
    for ( v = 0; pStr[v]; v++ )
    {
        if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
            uSet |= (1 << ((pStr[v] - 'a') << 1));
        else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' )
            uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1));
        else break;
    }
    return uSet;
}

Here is the caller graph for this function:

Dau_DecSortSet()

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

Here is the caller graph for this function:

Dau_DecTrySets()

void Dau_DecTrySets	(	word *	pInit,
		int	nVars,
		int	fVerbose )

Definition at line 831 of file dauNonDsd.c.

{
    Vec_Int_t * vSets;
    int i, Entry;
    assert( nVars <= 16 );
    vSets = Dau_DecFindSets( pInit, nVars );
    if ( !fVerbose )
    {
        Vec_IntFree( vSets );
        return;
    }
    Dau_DsdPrintFromTruth( pInit, nVars ); 
    printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) );
    Vec_IntForEachEntry( vSets, Entry, i )
    {
        unsigned uSet = (unsigned)Entry;
        printf( "Set %4d : ", i );
        if ( nVars > 6 )
        {
            Dau_DecPrintSet( uSet, nVars, 0 );
            Dau_DecPerform( pInit, nVars, uSet );
        }
        else
        {
            Dau_DecPrintSet( uSet, nVars, 1 );
            Dau_DecPerform6( pInit, nVars, uSet );
        }
    }
    Vec_IntFree( vSets );
//    printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dau_DecVarReplace()

void Dau_DecVarReplace	(	char *	pStr,
		int *	pPerm,
		int	nVars )

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

Synopsis [Replaces variables in the string.]

Description []

SideEffects []

SeeAlso []

Definition at line 557 of file dauNonDsd.c.

{
    int v;
    for ( v = 0; pStr[v]; v++ )
        if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
        {
            assert( pStr[v] - 'a' < nVars );
            pStr[v] = 'a' + pPerm[pStr[v] - 'a'];
        }
}

Here is the caller graph for this function:

Dau_DecVerify()

int Dau_DecVerify	(	word *	pInit,
		int	nVars,
		char *	pDsdC,
		char *	pDsdD )

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

Synopsis [Testing procedures.]

Description []

SideEffects []

SeeAlso []

Definition at line 687 of file dauNonDsd.c.

{
    word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16
    int nWordsC = Abc_TtWordNum(nVars+1);
    int nWordsD = Abc_TtWordNum(nVars);
    assert( nVars < 16 );
    memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC );
    memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD );
    if ( nVars >= 6 )
    {
        assert( nWordsD >= 1 );
        assert( nWordsC > 1 );
        Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD );
    }
    else
    {
        word pC0 = Abc_Tt6Stretch( pC[0], nVars );
        word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars );
        Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD );
    }
    if ( !Abc_TtEqual(pInit, pRes, nWordsD) )
        printf( "      Verification failed" );
//    else
//        printf( "      Verification successful" );
    printf( "\n" );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function: