ifDec10.c File Reference

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

Include dependency graph for ifDec10.c:

Go to the source code of this file.

Functions
void	If_Dec10PrintConfig (unsigned *pZ)
void	If_Dec10Verify (word *pF, int nVars, unsigned *pZ)
void	If_Dec10Cofactors (word *pF, int nVars, int iVar, word *pCof0, word *pCof1)
int	If_Dec10Perform (word *pF, int nVars, int fDerive)
int	If_CutPerformCheck10 (If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)

Function Documentation

If_CutPerformCheck10()

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

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

Synopsis [Performs additional check.]

Description []

SideEffects []

SeeAlso []

Definition at line 474 of file ifDec10.c.

{
    int nSupp, fDerive = 0;
    word pF[16];
    if ( nLeaves <= 6 )
        return 1;
    If_Dec10Copy( pF, (word *)pTruth, nVars );
    nSupp = If_Dec10Support( pF, nLeaves );
    if ( !nSupp || !If_DecSuppIsMinBase(nSupp) )
        return 0;
    if ( If_Dec10Perform( pF, nLeaves, fDerive ) )
    {
//        printf( "1" );
        return 1;
//        If_Dec10Verify( t, nLeaves, NULL );
    }
//    printf( "0" );
    return 0;
}

Here is the call graph for this function:

If_Dec10Cofactors()

void If_Dec10Cofactors	(	word *	pF,
		int	nVars,
		int	iVar,
		word *	pCof0,
		word *	pCof1 )

Definition at line 334 of file ifDec10.c.

{
    int nWords = If_Dec10WordNum( nVars );
    assert( iVar < nVars );
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
        {
            pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
            pCof1[i] = (pF[i] &  Truth6[iVar]) | ((pF[i] &  Truth6[iVar]) >> Shift);
        }
        return;
    }
    else
    {
        int i, k, Step = (1 << (iVar - 6));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pCof0[i] = pCof0[Step+i] = pF[i];
                pCof1[i] = pCof1[Step+i] = pF[Step+i];
            }
            pF    += 2*Step;
            pCof0 += 2*Step;
            pCof1 += 2*Step;
        }
        return;
    }
}

Here is the caller graph for this function:

If_Dec10Perform()

int If_Dec10Perform	(	word *	pF,
		int	nVars,
		int	fDerive )

Definition at line 376 of file ifDec10.c.

{ 
//    static int Cnt = 0;
    word pCof0[16], pCof1[16];
    int Pla2Var[10], Var2Pla[10], Count[210], Masks[210];
    int i, i0,i1,i2,i3, v, x;
    assert( nVars >= 6 && nVars <= 10 );
    // start arrays
    for ( i = 0; i < nVars; i++ )
    {
        assert( If_Dec10HasVar( pF, nVars, i ) );
        Pla2Var[i] = Var2Pla[i] = i;
    }
/*
    Cnt++;
//if ( Cnt == 108 )
{
printf( "%d\n", Cnt );
//Extra_PrintHex( stdout, (unsigned *)pF, nVars );
//printf( "\n" ); 
Kit_DsdPrintFromTruth( (unsigned *)pF, nVars );
printf( "\n" );
printf( "\n" );
}
*/
    // generate permutations
    v = 0;
    for ( i0 = 0;    i0 < nVars; i0++ )
    for ( i1 = i0+1; i1 < nVars; i1++ )
    for ( i2 = i1+1; i2 < nVars; i2++ )
    for ( i3 = i2+1; i3 < nVars; i3++, v++ )
    {
        If_Dec10MoveTo( pF, nVars, i0, nVars-1, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i1, nVars-2, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i2, nVars-3, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i3, nVars-4, Pla2Var, Var2Pla );
        If_DecVerifyPerm( Pla2Var, Var2Pla, nVars );
        Count[v] = If_Dec10CofCount( pF, nVars );
        Masks[v] = (1 << i0) | (1 << i1) | (1 << i2) | (1 << i3);
        assert( Count[v] > 1 );
//printf( "%d ", Count[v] );
        if ( Count[v] == 2 || Count[v] > 5 )
            continue;
        for ( x = 0; x < 4; x++ )
        {
            If_Dec10Cofactors( pF, nVars, nVars-1-x, pCof0, pCof1 );
            if ( If_Dec10CofCount2(pCof0, nVars) <= 2 && If_Dec10CofCount2(pCof1, nVars) <= 2 )
            {
                Count[v] = -Count[v];
                break;
            }
        }
    }
//printf( "\n" );
    assert( v <= 210 );
    // check if there are compatible bound sets
    for ( i0 = 0; i0 < v; i0++ )
    for ( i1 = i0+1; i1 < v; i1++ )
    {
        if ( If_Dec10Count16(Masks[i0] & Masks[i1]) > 10 - nVars )
            continue;
        if ( nVars == 10 )
        {
            if ( Count[i0] == 2 && Count[i1] == 2 )
                return 1;
        }
        else if ( nVars == 9 )
        {
            if ( (Count[i0] == 2 && Count[i1] == 2) || 
                 (Count[i0] == 2 && Count[i1] <  0) || 
                 (Count[i0] <  0 && Count[i1] == 2) )
                return 1;
        }
        else
        {
            if ( (Count[i0] == 2 && Count[i1] == 2) || 
                 (Count[i0] == 2 && Count[i1] <  0) || 
                 (Count[i0] <  0 && Count[i1] == 2) || 
                 (Count[i0] <  0 && Count[i1] <  0) )
                return 1;
        }
    }
//    printf( "not found\n" );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

If_Dec10PrintConfig()

void If_Dec10PrintConfig

(

unsigned *

pZ

)

Definition at line 89 of file ifDec10.c.

{
    while ( *pZ )
        If_Dec10PrintConfigOne( *pZ++ );
}

Here is the caller graph for this function:

If_Dec10Verify()

void If_Dec10Verify	(	word *	pF,
		int	nVars,
		unsigned *	pZ )

Definition at line 115 of file ifDec10.c.

{
    word pN[16][16], * pG[4];
    int i, w, v, k, nWords;
    unsigned z;
    nWords = If_Dec10WordNum( nVars );
    for ( k = 0; k < nVars; k++ )
        for ( w = 0; w < nWords; w++ )
            pN[k][w] = Truth10[k][w];
    for ( i = 0; (z = pZ[i]); i++, k++ )
    {
        for ( v = 0; v < 4; v++ )
            pG[v] = pN[ (z >> (16+(v<<2))) & 7 ];
        If_Dec10ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars );
    }
    k--;
    for ( w = 0; w < nWords; w++ )
        if ( pN[k][w] != pF[w] )
        {
            If_Dec10PrintConfig( pZ );
            Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
            Kit_DsdPrintFromTruth( (unsigned*)pN[k], nVars ); printf( "\n" );
            printf( "Verification failed!\n" );
            break;
        }
}

Here is the call graph for this function: