ifDec07.c File Reference

#include "if.h"
#include "misc/extra/extra.h"
#include "bool/kit/kit.h"

Include dependency graph for ifDec07.c:

Go to the source code of this file.

Functions
void	Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars)
void	Extra_PrintBinary (FILE *pFile, unsigned Sign[], int nBits)
void	If_DecPrintConfig (word z)
	FUNCTION DEFINITIONS ///.
word	If_Dec6Truth (word z)
void	If_Dec6Verify (word t, word z)
void	If_Dec7Verify (word t[2], word z)
word	If_Dec6Perform (word t, int fDerive)
word	If_Dec7Perform (word t0[2], int fDerive)
word	If_Dec6MinimumBase (word uTruth, int *pSupp, int nVarsAll, int *pnVars)
void	If_Dec7MinimumBase (word uTruth[2], int *pSupp, int nVarsAll, int *pnVars)
int	If_Dec6PickBestMux (word t, word Cofs[2])
int	If_Dec7PickBestMux (word t[2], word c0r[2], word c1r[2])
word	If_Dec5Perform (word t, int fDerive)
word	If_Dec5PerformEx ()
void	If_Dec5PerformTest ()
word	If_CutPerformDerive07 (If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
int	If_CutPerformCheck07 (If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
int	If_MatchCheck1 (If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
int	If_MatchCheck2 (If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)

Function Documentation

Extra_PrintBinary()

void Extra_PrintBinary ( FILE * pFile, unsigned Sign[], int nBits )

extern

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

Synopsis [Prints the bit string.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file extraUtilFile.c.

{
    int i;
    for ( i = nBits-1; i >= 0; i-- )
        fprintf( pFile, "%c", '0' + Abc_InfoHasBit(Sign, i) );
//    fprintf( pFile, "\n" );
}

Here is the caller graph for this function:

If_CutPerformCheck07()

int If_CutPerformCheck07	(	If_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		int	nLeaves,
		char *	pStr )

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

Synopsis [Performs additional check.]

Description []

SideEffects []

SeeAlso []

Definition at line 1060 of file ifDec07.c.

{
    int fDerive = 0;
    int v;
    // skip non-support minimal
    for ( v = 0; v < nLeaves; v++ )
        if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) )
            return 0;
    // check
    if ( nLeaves < 5 )
        return 1;
    if ( nLeaves == 5 )
    {
        word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
        z = If_Dec5Perform( t, fDerive );
        if ( fDerive && z )
            If_Dec6Verify( t, z );
        return z != 0;
    }
    if ( nLeaves == 6 )
    {
        word z, t = ((word *)pTruth)[0];
        z = If_Dec6Perform( t, fDerive );
        if ( fDerive && z )
        {
//            If_DecPrintConfig( z );
            If_Dec6Verify( t, z );
        }
//        if ( z == 0 )
//            Extra_PrintHex(stdout, (unsigned *)&t, 6), printf( "  " ), Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
        return z != 0;
    }
    if ( nLeaves == 7 )
    {
        word z, t[2];
        t[0] = ((word *)pTruth)[0];
        t[1] = ((word *)pTruth)[1];
//        if ( If_Dec7CheckMux(t) >= 0 )
//            return 1;
        z = If_Dec7Perform( t, fDerive );
        if ( fDerive && z )
            If_Dec7Verify( t, z );
        return z != 0;
    }
    assert( 0 );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_CutPerformDerive07()

word If_CutPerformDerive07	(	If_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		int	nLeaves,
		char *	pStr )

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

Synopsis [Performs additional check.]

Description []

SideEffects []

SeeAlso []

Definition at line 1018 of file ifDec07.c.

{
    if ( nLeaves < 5 )
        return 1;
    if ( nLeaves == 5 )
    {
        word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
        z = If_Dec5Perform( t, 1 );
        If_Dec6Verify( t, z );
        return z;
    }
    if ( nLeaves == 6 )
    {
        word z, t = ((word *)pTruth)[0];
        z = If_Dec6Perform( t, 1 );
        If_Dec6Verify( t, z );
        return z;
    }
    if ( nLeaves == 7 )
    {
        word z, t[2];
        t[0] = ((word *)pTruth)[0];
        t[1] = ((word *)pTruth)[1];
        z = If_Dec7Perform( t, 1 );
        If_Dec7Verify( t, z );
        return z;
    }
    assert( 0 );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_Dec5Perform()

word If_Dec5Perform	(	word	t,
		int	fDerive )

Definition at line 857 of file ifDec07.c.

{
    int Pla2Var[7], Var2Pla[7];
    int i, j, v;
    word t0 = t;
/*
    word c0, c1, c00, c01, c10, c11;
    for ( i = 0; i < 5; i++ )
    {
        c0 = If_Dec6Cofactor( t, i, 0 );
        c1 = If_Dec6Cofactor( t, i, 1 );
        if ( c0 == 0 )
            return 1;
        if ( ~c0 == 0 )
            return 1;
        if ( c1 == 0 )
            return 1;
        if ( ~c1 == 0 )
            return 1;
       if ( c0 == ~c1 )
            return 1;
    }
    for ( i = 0; i < 4; i++ )
    {
        c0 = If_Dec6Cofactor( t, i, 0 );
        c1 = If_Dec6Cofactor( t, i, 1 );
        for ( j = i + 1; j < 5; j++ )
        {
            c00 = If_Dec6Cofactor( c0, j, 0 );
            c01 = If_Dec6Cofactor( c0, j, 1 );
            c10 = If_Dec6Cofactor( c1, j, 0 );
            c11 = If_Dec6Cofactor( c1, j, 1 );
            if ( c00 == c01 && c00 == c10 )
                return 1;
            if ( c11 == c01 && c11 == c10 )
                return 1;
            if ( c11 == c00 && c11 == c01 )
                return 1;
            if ( c11 == c00 && c11 == c10 )
                return 1;
            if ( c00 == c11 && c01 == c10 )
                return 1;
        }
    }
*/
    // start arrays
    for ( i = 0; i < 7; i++ )
        Pla2Var[i] = Var2Pla[i] = i;
    // generate permutations
    for ( v = 0; v < 5; v++ )
    {
        t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
        If_DecVerifyPerm( Pla2Var, Var2Pla );
        for ( i = 0; i < 4; i++ )
            for ( j = i + 1; j < 4; j++ )
            {
                word z = If_Dec5CofCount2( t, i, j, Pla2Var, t0, fDerive );
                if ( z )
                {
/*
                    if ( v == 0 && i == 1 && j == 2 )
                    {
                          Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
                    }
*/
                    return z;
                }
            }
    }
 
/*
    // start arrays
    for ( i = 0; i < 7; i++ )
        Pla2Var[i] = Var2Pla[i] = i;
 
    t = t0;
    for ( v = 0; v < 5; v++ )
    {
        int x, y;
 
        t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
        If_DecVerifyPerm( Pla2Var, Var2Pla );
 
        for ( i = 0; i < 16; i++ )
            printf( "%d ", ((t >> (i<<1)) & 3) );
        printf( "\n" );
 
        for ( x = 0; x < 4; x++ )
        for ( y = x + 1; y < 4; y++ )
        {
            for ( i = 0; i < 16; i++ )
                if ( !((i >> x) & 1) && !((i >> y) & 1) )
                    printf( "%d ", ((t >> (i<<1)) & 3) );
            printf( "\n" );
 
            for ( i = 0; i < 16; i++ )
                if ( ((i >> x) & 1) && !((i >> y) & 1) )
                    printf( "%d ", ((t >> (i<<1)) & 3) );
            printf( "\n" );
 
            for ( i = 0; i < 16; i++ )
                if ( !((i >> x) & 1) && ((i >> y) & 1) )
                    printf( "%d ", ((t >> (i<<1)) & 3) );
            printf( "\n" );
 
            for ( i = 0; i < 16; i++ )
                if ( ((i >> x) & 1) && ((i >> y) & 1) )
                    printf( "%d ", ((t >> (i<<1)) & 3) );
            printf( "\n" );
            printf( "\n" );
        }
    }
*/
 
//    Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
    return 0;
}

Here is the caller graph for this function:

If_Dec5PerformEx()

word If_Dec5PerformEx

(

)

Definition at line 975 of file ifDec07.c.

{
    word z;
    // find one
    z = (word)(0x17ac & 0xFFFF);
    z |= (((word)3) << (16 + 4*0));
    z |= (((word)4) << (16 + 4*1));
    z |= (((word)1) << (16 + 4*2));
    z |= (((word)2) << (16 + 4*3));
    // second one
    z |= (((word)(0x179a & 0xFFFF)) << 32);
    z |= (((word)0) << (48 + 4*0));
    z |= (((word)7) << (48 + 4*1));
    z |= (((word)1) << (48 + 4*2));
    z |= (((word)2) << (48 + 4*3));
    return z;
}

If_Dec5PerformTest()

void If_Dec5PerformTest

(

)

Definition at line 992 of file ifDec07.c.

{
    word z, t, t1;
//    s = If_Dec5PerformEx();
//    t = If_Dec6Truth( s );
    t = ABC_CONST(0xB0F3B0FFB0F3B0FF);
 
    Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf("\n");
 
    z = If_Dec5Perform( t, 1 );
    t1 = If_Dec6Truth( z );
    assert( t == t1 );
}

Here is the call graph for this function:

If_Dec6MinimumBase()

word If_Dec6MinimumBase	(	word	uTruth,
		int *	pSupp,
		int	nVarsAll,
		int *	pnVars )

Definition at line 501 of file ifDec07.c.

{
    int v, iVar = 0, uSupp = 0;
    assert( nVarsAll <= 6 );
    for ( v = 0; v < nVarsAll; v++ )
        if ( If_Dec6HasVar( uTruth, v ) )
        {
            uSupp |= (1 << v);
            if ( pSupp )
                pSupp[iVar] = pSupp[v];
            iVar++;
        }
    if ( pnVars )
        *pnVars = iVar;
    if ( If_DecSuppIsMinBase( uSupp ) )
        return uTruth;
    return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp );
}

Here is the caller graph for this function:

If_Dec6Perform()

word If_Dec6Perform	(	word	t,
		int	fDerive )

Definition at line 409 of file ifDec07.c.

{ 
    word r = 0;
    int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
    // start arrays
    for ( i = 0; i < 6; i++ )
    {
        assert( If_Dec6HasVar( t, i ) );
        Pla2Var[i] = Var2Pla[i] = i;
    }
    // generate permutations
    i = 0;
    for ( v = 0;   v < 6; v++ )
    for ( u = v+1; u < 6; u++, i++ )
    {
        t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
        t = If_Dec6MoveTo( t, u, 1, Pla2Var, Var2Pla );
//        If_DecVerifyPerm( Pla2Var, Var2Pla );
        Count = If_Dec6CofCount2( t );
        assert( Count > 1 );
        if ( Count == 2 )
            return !fDerive ? 1 : If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla );
        // check non-disjoint decomposition
        if ( !r && (Count == 3 || Count == 4) )
        {
            for ( x = 0; x < 4; x++ )
            {
                word c0 = If_Dec6Cofactor( t, x+2, 0 );
                word c1 = If_Dec6Cofactor( t, x+2, 1 );
                if ( If_Dec6CofCount2( c0 ) <= 2 && If_Dec6CofCount2( c1 ) <= 2 )
                {
                    r = !fDerive ? 1 : If_Dec6DeriveNonDisjoint( t, x+2, Pla2Var, Var2Pla );
                    break;
                }
            }
        }
    }
    assert( i == 15 );
    return r;
}

Here is the caller graph for this function:

If_Dec6PickBestMux()

int If_Dec6PickBestMux	(	word	t,
		word	Cofs[2] )

Definition at line 626 of file ifDec07.c.

{
    int v, vBest = -1, Count0, Count1, CountBest = 1000;
    for ( v = 0; v < 6; v++ )
    {
        Count0 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 0) );
        Count1 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 1) );
        if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
        {
            CountBest = Count0 + Count1;
            vBest = v;
            Cofs[0] = If_Dec6Cofactor(t, v, 0);
            Cofs[1] = If_Dec6Cofactor(t, v, 1);
        }
    }
    return vBest;
}

Here is the caller graph for this function:

If_Dec6Truth()

word If_Dec6Truth

(

word

z

)

Definition at line 107 of file ifDec07.c.

{
    word r, q, f[4];
    int i, v;
    assert( z );
    for ( i = 0; i < 4; i++ )
    {
        v = (z >> (16+(i<<2))) & 7;
        assert( v != 7 );
        if ( v == 6 )
            continue;
        f[i] = Truth6[v];
    }
    q = If_Dec6ComposeLut4( (int)(z & 0xffff), f );
    for ( i = 0; i < 4; i++ )
    {
        v = (z >> (48+(i<<2))) & 7;
        if ( v == 6 )
            continue;
        f[i] = (v == 7) ? q : Truth6[v];
    }
    r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f );
    return r;
}

Here is the caller graph for this function:

If_Dec6Verify()

void If_Dec6Verify	(	word	t,
		word	z )

Definition at line 131 of file ifDec07.c.

{
    word r = If_Dec6Truth( z );
    if ( r != t )
    {
        If_DecPrintConfig( z );
        Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" );
//        Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" );
        Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" );
        printf( "Verification failed!\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_Dec7MinimumBase()

void If_Dec7MinimumBase	(	word	uTruth[2],
		int *	pSupp,
		int	nVarsAll,
		int *	pnVars )

Definition at line 533 of file ifDec07.c.

{
    int v, iVar = 0, uSupp = 0;
    assert( nVarsAll <= 7 );
    for ( v = 0; v < nVarsAll; v++ )
        if ( If_Dec7HasVar( uTruth, v ) )
        {
            uSupp |= (1 << v);
            if ( pSupp )
                pSupp[iVar] = pSupp[v];
            iVar++;
        }
    if ( pnVars )
        *pnVars = iVar;
    if ( If_DecSuppIsMinBase( uSupp ) )
        return;
    If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp );
}

Here is the caller graph for this function:

If_Dec7Perform()

word If_Dec7Perform	(	word	t0[2],
		int	fDerive )

Definition at line 449 of file ifDec07.c.

{
    word t[2] = {t0[0], t0[1]}; 
    int i, v, u, y, Pla2Var[7], Var2Pla[7];
    // start arrays
    for ( i = 0; i < 7; i++ )
    {
/*
        if ( i < 6 )
            assert( If_Dec6HasVar( t[0], i ) || If_Dec6HasVar( t[1], i ) );
        else
            assert( t[0] != t[1] );
*/
        Pla2Var[i] = Var2Pla[i] = i;
    }
    // generate permutations
    for ( v = 0;   v < 7; v++ )
    for ( u = v+1; u < 7; u++ )
    for ( y = u+1; y < 7; y++ )
    {
        If_Dec7MoveTo( t, v, 0, Pla2Var, Var2Pla );
        If_Dec7MoveTo( t, u, 1, Pla2Var, Var2Pla );
        If_Dec7MoveTo( t, y, 2, Pla2Var, Var2Pla );
//        If_DecVerifyPerm( Pla2Var, Var2Pla );
        if ( If_Dec7CofCount3( t ) == 2 )
        {
            return !fDerive ? 1 : If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla );
        }
    }
    return 0;
}

Here is the caller graph for this function:

If_Dec7PickBestMux()

int If_Dec7PickBestMux	(	word	t[2],
		word	c0r[2],
		word	c1r[2] )

Definition at line 643 of file ifDec07.c.

{
    word c0[2], c1[2];
    int v, vBest = -1, Count0, Count1, CountBest = 1000;
    for ( v = 0; v < 7; v++ )
    {
        If_Dec7Cofactor( t, v, 0, c0 );
        If_Dec7Cofactor( t, v, 1, c1 );
        Count0 = If_Dec7SuppSize(c0);
        Count1 = If_Dec7SuppSize(c1);
        if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
        {
            CountBest = Count0 + Count1;
            vBest = v;
            c0r[0] = c0[0]; c0r[1] = c0[1];
            c1r[0] = c1[0]; c1r[1] = c1[1];
        }
    }
    return vBest;
}

Here is the caller graph for this function:

If_Dec7Verify()

void If_Dec7Verify	(	word	t[2],
		word	z )

Definition at line 163 of file ifDec07.c.

{
    word f[4][2], r[2];
    int i, v;
    assert( z );
    for ( i = 0; i < 4; i++ )
    {
        v = (z >> (16+(i<<2))) & 7;
        f[i][0] = Truth7[v][0];
        f[i][1] = Truth7[v][1];
    }
    If_Dec7ComposeLut4( (int)(z & 0xffff), f, r );
    f[3][0] = r[0];
    f[3][1] = r[1];
    for ( i = 0; i < 3; i++ )
    {
        v = (z >> (48+(i<<2))) & 7;
        f[i][0] = Truth7[v][0];
        f[i][1] = Truth7[v][1];
    }
    If_Dec7ComposeLut4( (int)((z >> 32) & 0xffff), f, r );
    if ( r[0] != t[0] || r[1] != t[1] )
    {
        If_DecPrintConfig( z );
        Kit_DsdPrintFromTruth( (unsigned*)t, 7 ); printf( "\n" );
        Kit_DsdPrintFromTruth( (unsigned*)r, 7 ); printf( "\n" );
        printf( "Verification failed!\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_DecPrintConfig()

void If_DecPrintConfig

(

word

z

)

FUNCTION DEFINITIONS ///.

Definition at line 66 of file ifDec07.c.

{
   unsigned S[1];
   S[0] = (z & 0xffff) | ((z & 0xffff) << 16);
   Extra_PrintBinary( stdout, S, 16 ); 
   printf( " " );
   Kit_DsdPrintFromTruth( S, 4 );
   printf( " " );
   printf( " %d", (int)((z >> 16) & 7) );
   printf( " %d", (int)((z >> 20) & 7) );
   printf( " %d", (int)((z >> 24) & 7) );
   printf( " %d", (int)((z >> 28) & 7) );
   printf( "   " );
   S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16);
   Extra_PrintBinary( stdout, S, 16 );
   printf( " " );
   Kit_DsdPrintFromTruth( S, 4 );
   printf( " " );
   printf( " %d", (int)((z >> 48) & 7) );
   printf( " %d", (int)((z >> 52) & 7) );
   printf( " %d", (int)((z >> 56) & 7) );
   printf( " %d", (int)((z >> 60) & 7) );
   printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_MatchCheck1()

int If_MatchCheck1	(	If_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		int	nLeaves,
		char *	pStr )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1119 of file ifDec07.c.

{
    if ( nLeaves < nVars )
        return 1;
    assert( nLeaves == nVars );
    if ( Abc_Tt6Check1( ((word *)pTruth)[0], nLeaves ) )
        return 1;
    return 0;
}

If_MatchCheck2()

int If_MatchCheck2	(	If_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		int	nLeaves,
		char *	pStr )

Definition at line 1128 of file ifDec07.c.

{
    if ( nLeaves < nVars )
        return 1;
    assert( nLeaves == nVars );
    if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
        return 1;
    return 0;
}

Kit_DsdPrintFromTruth()

void Kit_DsdPrintFromTruth ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
//    Kit_DsdPrintExpanded( pTemp );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdPrint( stdout, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

Here is the caller graph for this function: