#include "base/abc/abc.h"
#include "misc/vec/vecWec.h"
#include "misc/vec/vecQue.h"
#include "misc/vec/vecHsh.h"
#include "opt/fxch/Fxch.h"

Include dependency graph for abcFx.c:

Go to the source code of this file.

Classes
struct	Fx_Man_t_

Macros
#define	Fx_ManForEachCubeVec(vVec, vCubes, vCube, i)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Fx_Man_t_	Fx_Man_t
	DECLARATIONS ///.

Functions
Vec_Wec_t *	Abc_NtkFxRetrieve (Abc_Ntk_t *pNtk)
	FUNCTION DEFINITIONS ///.

void	Abc_NtkFxInsert (Abc_Ntk_t pNtk, Vec_Wec_t vCubes)

int	Abc_NtkFxCheck (Abc_Ntk_t *pNtk)

int	Abc_NtkFxPerform (Abc_Ntk_t *pNtk, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose)

Fx_Man_t *	Fx_ManStart (Vec_Wec_t *vCubes)

void	Fx_ManStop (Fx_Man_t *p)

void	Fx_ManComputeLevel (Fx_Man_t *p)

int	Fx_ManDivFindCubeFree (Vec_Int_t vArr1, Vec_Int_t vArr2, Vec_Int_t vCubeFree, int fWarning)

void	Fx_ManCreateLiterals (Fx_Man_t *p, int nVars)

int	Fx_ManCubeSingleCubeDivisors (Fx_Man_t p, Vec_Int_t vPivot, int fRemove, int fUpdate)

void	Fx_ManCubeDoubleCubeDivisors (Fx_Man_t p, int iFirst, Vec_Int_t vPivot, int fRemove, int fUpdate, int *fWarning)

void	Fx_ManCreateDivisors (Fx_Man_t *p)

void	Fx_ManFindCommonPairs (Vec_Wec_t vCubes, Vec_Int_t vPart0, Vec_Int_t vPart1, Vec_Int_t vPairs, Vec_Int_t vCompls, Vec_Int_t vDiv, Vec_Int_t vCubeFree, int fWarning)

void	Fx_ManUpdate (Fx_Man_t p, int iDiv, int fWarning)

int	Fx_FastExtract (Vec_Wec_t *vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose)

Macro Definition Documentation

◆ Fx_ManForEachCubeVec

#define Fx_ManForEachCubeVec	(	vVec,
		vCubes,
		vCube,
		i )

Value:

for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )

Definition at line 122 of file abcFx.c.

122#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \

123 for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )

Typedef Documentation

◆ Fx_Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Fx_Man_t_ Fx_Man_t

DECLARATIONS ///.

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

FileName [abcFx.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Implementation of traditional "fast_extract" algorithm.]

Author [Alan Mishchenko, Bruno Schmitt]

Affiliation [UC Berkeley, UFRGS]

Date [Ver. 1.0. Started - April 26, 2013.]

Revision [

Id: abcFx.c,v 1.00 2013/04/26 00:00:00 alanmi Exp

]

Definition at line 86 of file abcFx.c.

Function Documentation

◆ Abc_NtkFxCheck()

int Abc_NtkFxCheck ( Abc_Ntk_t * pNtk )

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

Synopsis [Makes sure the nodes do not have complemented and duplicated fanins.]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file abcFx.c.

{
    Abc_Obj_t * pNode;
    int i;
//    Abc_NtkForEachObj( pNtk, pNode, i )
//        Abc_ObjPrint( stdout, pNode );
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) ) {
            printf( "Fanins of node %d: ", i );
            Vec_IntPrint( &pNode->vFanins );
            return 0;
        }
    return 1;
}

Here is the caller graph for this function:

◆ Abc_NtkFxInsert()

void Abc_NtkFxInsert	(	Abc_Ntk_t *	pNtk,
		Vec_Wec_t *	vCubes )

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

Synopsis [Inserts SOP information after fast_extract.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file abcFx.c.

{
    Vec_Int_t * vCube, * vPres, * vFirst, * vCount;
    Abc_Obj_t * pNode, * pFanin;
    char * pCube, * pSop;
    int i, k, v, Lit, iFanin, iNodeMax = 0;
    assert( Abc_NtkIsSopLogic(pNtk) );
    // check that cubes have no gaps and are ordered by first node
    Lit = -1;
    Vec_WecForEachLevel( vCubes, vCube, i )
    {
        assert( Vec_IntSize(vCube) > 0 );
        assert( Lit <= Vec_IntEntry(vCube, 0) );
        Lit = Vec_IntEntry(vCube, 0);
    }
    // find the largest index
    Vec_WecForEachLevel( vCubes, vCube, i )
        iNodeMax = Abc_MaxInt( iNodeMax, Vec_IntEntry(vCube, 0) );
    // quit if nothing changes
    if ( iNodeMax < Abc_NtkObjNumMax(pNtk) )
    {
        //printf( "The network is unchanged by fast extract.\n" );
        return;
    }
    // create new nodes
    for ( i = Abc_NtkObjNumMax(pNtk); i <= iNodeMax; i++ )
    {
        pNode = Abc_NtkCreateNode( pNtk );
        assert( i == (int)Abc_ObjId(pNode) );
    }
    // create node fanins
    vFirst = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
    vCount = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
    Vec_WecForEachLevel( vCubes, vCube, i )
    {
        iFanin = Vec_IntEntry( vCube, 0 );
        if ( Vec_IntEntry(vCount, iFanin) == 0 )
            Vec_IntWriteEntry( vFirst, iFanin, i );
        Vec_IntAddToEntry( vCount, iFanin, 1 );
    }
    // create node SOPs
    vPres = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
//        if ( Vec_IntEntry(vCount, i) == 0 ) continue;
        Abc_ObjRemoveFanins( pNode );
        // create fanins
        assert( Vec_IntEntry(vCount, i) > 0 );
        for ( k = 0; k < Vec_IntEntry(vCount, i); k++ )
        {
            vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k );
            assert( Vec_IntEntry( vCube, 0 ) == i );
            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
            {
                pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit));
                if ( Vec_IntEntry(vPres, Abc_ObjId(pFanin)) >= 0 )
                    continue;
                Vec_IntWriteEntry(vPres, Abc_ObjId(pFanin), Abc_ObjFaninNum(pNode));
                Abc_ObjAddFanin( pNode, pFanin );
            }
        }
        // create SOP
        pSop = pCube = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntEntry(vCount, i), Abc_ObjFaninNum(pNode) );
        for ( k = 0; k < Vec_IntEntry(vCount, i); k++ )
        {
            vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k );
            assert( Vec_IntEntry( vCube, 0 ) == i );
            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
            {
                pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit));
                iFanin = Vec_IntEntry(vPres, Abc_ObjId(pFanin));
                assert( iFanin >= 0 && iFanin < Abc_ObjFaninNum(pNode) );
                pCube[iFanin] = Abc_LitIsCompl(Lit) ? '0' : '1';
            }
            pCube += Abc_ObjFaninNum(pNode) + 3;
        }
        // complement SOP if the original one was complemented
        if ( pNode->pData && Abc_SopIsComplement((char *)pNode->pData) )
            Abc_SopComplement( pSop );
        pNode->pData = pSop;
        // clean fanins
        Abc_ObjForEachFanin( pNode, pFanin, v )
            Vec_IntWriteEntry( vPres, Abc_ObjId(pFanin), -1 );
    }
    Vec_IntFree( vFirst );
    Vec_IntFree( vCount );
    Vec_IntFree( vPres );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkFxPerform()

int Abc_NtkFxPerform	(	Abc_Ntk_t *	pNtk,
		int	nNewNodesMax,
		int	LitCountMax,
		int	fCanonDivs,
		int	fVerbose,
		int	fVeryVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 309 of file abcFx.c.

{
    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
    Vec_Wec_t * vCubes;
    assert( Abc_NtkIsSopLogic(pNtk) );
    // check unique fanins
    if ( !Abc_NtkFxCheck(pNtk) )
    {
        printf( "Abc_NtkFastExtract: Nodes have duplicated fanins. FX is not performed.\n" );
        return 0;
    }
    // collect information about the covers
    vCubes = Abc_NtkFxRetrieve( pNtk );
    // call the fast extract procedure
    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fCanonDivs, fVerbose, fVeryVerbose ) > 0 )
    {
        // update the network
        Abc_NtkFxInsert( pNtk, vCubes );
        Vec_WecFree( vCubes );
        if ( !Abc_NtkCheck( pNtk ) )
            printf( "Abc_NtkFxPerform: The network check has failed.\n" );
        return 1;
    }
    else
        printf( "Warning: The network has not been changed by \"fx\".\n" );
    Vec_WecFree( vCubes );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkFxRetrieve()

Vec_Wec_t * Abc_NtkFxRetrieve ( Abc_Ntk_t * pNtk )

FUNCTION DEFINITIONS ///.

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

Synopsis [Retrieves SOP information for fast_extract.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file abcFx.c.

{
    Vec_Wec_t * vCubes;
    Vec_Int_t * vCube;
    Abc_Obj_t * pNode;
    char * pCube, * pSop;
    int nVars, i, v, Lit;
    assert( Abc_NtkIsSopLogic(pNtk) );
    vCubes = Vec_WecAlloc( 1000 );
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        pSop = (char *)pNode->pData;
        nVars = Abc_SopGetVarNum(pSop);
        assert( nVars == Abc_ObjFaninNum(pNode) );
//        if ( nVars < 2 ) continue;
        Abc_SopForEachCube( pSop, nVars, pCube )
        {
            vCube = Vec_WecPushLevel( vCubes );
            Vec_IntPush( vCube, Abc_ObjId(pNode) );
            Abc_CubeForEachVar( pCube, Lit, v )
            {
                if ( Lit == '0' )
                    Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 1) );
                else if ( Lit == '1' )
                    Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 0) );
            }
            Vec_IntSelectSort( Vec_IntArray(vCube) + 1, Vec_IntSize(vCube) - 1 );
        }
    }
    return vCubes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_FastExtract()

int Fx_FastExtract	(	Vec_Wec_t *	vCubes,
		int	ObjIdMax,
		int	nNewNodesMax,
		int	LitCountMax,
		int	fCanonDivs,
		int	fVerbose,
		int	fVeryVerbose )

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

Synopsis [Implements the traditional fast_extract algorithm.]

Description [J. Rajski and J. Vasudevamurthi, "The testability- preserving concurrent decomposition and factorization of Boolean expressions", IEEE TCAD, Vol. 11, No. 6, June 1992, pp. 778-793.]

SideEffects []

SeeAlso []

Definition at line 1166 of file abcFx.c.

{
    int fVeryVeryVerbose = 0;
    int i, iDiv, fWarning = 0;
    Fx_Man_t * p;
    abctime clk = Abc_Clock();
    // initialize the data-structure
    p = Fx_ManStart( vCubes );
    p->LitCountMax = LitCountMax;
    p->fCanonDivs = fCanonDivs;
    Fx_ManCreateLiterals( p, ObjIdMax );
    Fx_ManComputeLevel( p );
    Fx_ManCreateDivisors( p );
    if ( fVeryVerbose )
        Fx_PrintDivisors( p );
    if ( fVerbose )
        Fx_PrintStats( p, Abc_Clock() - clk );
    // perform extraction
    p->timeStart = Abc_Clock();
    for ( i = 0; i < nNewNodesMax && Vec_QueTopPriority(p->vPrio) > 0.0; i++ )
    {
        iDiv = Vec_QuePop(p->vPrio);
        if ( fVeryVerbose )
            Fx_PrintDiv( p, iDiv );
        Fx_ManUpdate( p, iDiv, &fWarning );
        if ( fVeryVeryVerbose )
            Fx_PrintDivisors( p );
    }
    if ( fVerbose )
        Fx_PrintStats( p, Abc_Clock() - clk );
    Fx_ManStop( p );
    // return the result
    Vec_WecRemoveEmpty( vCubes );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_ManComputeLevel()

void Fx_ManComputeLevel ( Fx_Man_t * p )

Definition at line 410 of file abcFx.c.

{
    Vec_Int_t * vCube;
    int i, iVar, iFirst = 0;
    iVar = Vec_IntEntry( Vec_WecEntry(p->vCubes,0), 0 );
    p->vLevels = Vec_IntStart( p->nVars );
    Vec_WecForEachLevel( p->vCubes, vCube, i )
    {
        if ( iVar != Vec_IntEntry(vCube, 0) )
        {
            // add the number of cubes
            Vec_IntAddToEntry( p->vLevels, iVar, i - iFirst );
            iVar = Vec_IntEntry(vCube, 0);
            iFirst = i;
        }
        Vec_IntUpdateEntry( p->vLevels, iVar, Fx_ManComputeLevelCube(p, vCube) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_ManCreateDivisors()

void Fx_ManCreateDivisors ( Fx_Man_t * p )

Definition at line 855 of file abcFx.c.

{
    Vec_Int_t * vCube;
    float Weight;
    int i, fWarning = 0;
    // alloc hash table
    assert( p->pHash == NULL );
    p->pHash = Hsh_VecManStart( 1000 );
    p->vWeights = Vec_FltAlloc( 1000 );
    // create single-cube two-literal divisors
    Vec_WecForEachLevel( p->vCubes, vCube, i )
        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 0 ); // add - no update
    assert( p->nDivsS == Vec_FltSize(p->vWeights) );
    // create two-cube divisors
    Vec_WecForEachLevel( p->vCubes, vCube, i )
        Fx_ManCubeDoubleCubeDivisors( p, i+1, vCube, 0, 0, &fWarning ); // add - no update
    // create queue with all divisors
    p->vPrio = Vec_QueAlloc( Vec_FltSize(p->vWeights) );
    Vec_QueSetPriority( p->vPrio, Vec_FltArrayP(p->vWeights) );
    Vec_FltForEachEntry( p->vWeights, Weight, i )
        if ( Weight > 0.0 )
            Vec_QuePush( p->vPrio, i );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_ManCreateLiterals()

void Fx_ManCreateLiterals	(	Fx_Man_t *	p,
		int	nVars )

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

Synopsis [Setting up the data-structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 715 of file abcFx.c.

{
    Vec_Int_t * vCube;
    int i, k, Lit, Count;
    // find the number of variables
    p->nVars = p->nLits = 0;
    Vec_WecForEachLevel( p->vCubes, vCube, i )
    {
        assert( Vec_IntSize(vCube) > 0 );
        p->nVars = Abc_MaxInt( p->nVars, Vec_IntEntry(vCube, 0) );
        p->nLits += Vec_IntSize(vCube) - 1;
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            p->nVars = Abc_MaxInt( p->nVars, Abc_Lit2Var(Lit) );
    }
//    p->nVars++;
    assert( p->nVars < nVars );
    p->nVars = nVars;
    // count literals
    p->vCounts = Vec_IntStart( 2*p->nVars );
    Vec_WecForEachLevel( p->vCubes, vCube, i )
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            Vec_IntAddToEntry( p->vCounts, Lit, 1 );
    // start literals
    p->vLits = Vec_WecStart( 2*p->nVars );
    Vec_IntForEachEntry( p->vCounts, Count, Lit )
        Vec_IntGrow( Vec_WecEntry(p->vLits, Lit), Count );
    // fill out literals
    Vec_WecForEachLevel( p->vCubes, vCube, i )
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            Vec_WecPush( p->vLits, Lit, i );
    // create mapping of variable into the first cube
    p->vVarCube = Vec_IntStartFull( p->nVars );
    Vec_WecForEachLevel( p->vCubes, vCube, i )
        if ( Vec_IntEntry(p->vVarCube, Vec_IntEntry(vCube, 0)) == -1 )
            Vec_IntWriteEntry( p->vVarCube, Vec_IntEntry(vCube, 0), i );
}

Here is the caller graph for this function:

◆ Fx_ManCubeDoubleCubeDivisors()

void Fx_ManCubeDoubleCubeDivisors	(	Fx_Man_t *	p,
		int	iFirst,
		Vec_Int_t *	vPivot,
		int	fRemove,
		int	fUpdate,
		int *	fWarning )

Definition at line 791 of file abcFx.c.

{
    Vec_Int_t * vCube;
    int i, iDiv, Base;
    Vec_WecForEachLevelStart( p->vCubes, vCube, i, iFirst )
    {
        if ( Vec_IntSize(vCube) == 0 || vCube == vPivot )
            continue;
        if ( Vec_WecIntHasMark(vCube) && Vec_WecIntHasMark(vPivot) && vCube > vPivot )
            continue;
        if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) )
            break;
        Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vCubeFree, fWarning );
        if ( Base == -1 ) 
        {
            if ( fRemove == 0 )
            {
                if ( Vec_IntSize( vCube ) > Vec_IntSize( vPivot ) )
                    Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vCube ) );
                else
                    Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vPivot ) );
            }
            continue;
        }
        if ( Vec_IntSize(p->vCubeFree) == 4 )
        { 
            int Value = Fx_ManDivNormalize( p->vCubeFree );
            if ( Value == 0 )
                p->nDivMux[0]++;
            else if ( Value == 1 )
                p->nDivMux[1]++;
            else
                p->nDivMux[2]++;
            if ( p->fCanonDivs && Value < 0 )
                continue;
        }
        if ( p->LitCountMax && p->LitCountMax < Vec_IntSize(p->vCubeFree) )
            continue;
        if ( p->fCanonDivs && Vec_IntSize(p->vCubeFree) == 3 )
            continue;
        iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
        if ( !fRemove )
        {
            if ( iDiv == Vec_FltSize(p->vWeights) )
                Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree) + 0.9 - 0.0009 * Fx_ManComputeLevelDiv(p, p->vCubeFree));
            assert( iDiv < Vec_FltSize(p->vWeights) );
            Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vCubeFree) - 1 );
            p->nPairsD++;
        }
        else
        {
            assert( iDiv < Vec_FltSize(p->vWeights) );
            Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vCubeFree) - 1) );
            p->nPairsD--;
        }
        if ( fUpdate )
        {
            if ( Vec_QueIsMember(p->vPrio, iDiv) )
                Vec_QueUpdate( p->vPrio, iDiv );
            else if ( !fRemove )
                Vec_QuePush( p->vPrio, iDiv );
        }
    } 
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_ManCubeSingleCubeDivisors()

int Fx_ManCubeSingleCubeDivisors	(	Fx_Man_t *	p,
		Vec_Int_t *	vPivot,
		int	fRemove,
		int	fUpdate )

Definition at line 751 of file abcFx.c.

{
    int k, n, Lit, Lit2, iDiv;
    if ( Vec_IntSize(vPivot) < 2 )
        return 0;
    Vec_IntForEachEntryStart( vPivot, Lit, k, 1 )
    Vec_IntForEachEntryStart( vPivot, Lit2, n, k+1 )
    {
        assert( Lit < Lit2 );
        Vec_IntClear( p->vCubeFree );
        Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) );
        Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) );
        iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
        if ( !fRemove )
        {
            if ( Vec_FltSize(p->vWeights) == iDiv )
            {
                Vec_FltPush(p->vWeights, -2 + 0.9 - 0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree));
                p->nDivsS++;
            }
            assert( iDiv < Vec_FltSize(p->vWeights) );
            Vec_FltAddToEntry( p->vWeights, iDiv, 1 );
            p->nPairsS++;
        }
        else
        {
            assert( iDiv < Vec_FltSize(p->vWeights) );
            Vec_FltAddToEntry( p->vWeights, iDiv, -1 );
            p->nPairsS--;
        }
        if ( fUpdate )
        {
            if ( Vec_QueIsMember(p->vPrio, iDiv) )
                Vec_QueUpdate( p->vPrio, iDiv );
            else if ( !fRemove )
                Vec_QuePush( p->vPrio, iDiv );
        }
    }
    return Vec_IntSize(vPivot) * (Vec_IntSize(vPivot) - 1) / 2;
}

Here is the caller graph for this function:

◆ Fx_ManDivFindCubeFree()

int Fx_ManDivFindCubeFree	(	Vec_Int_t *	vArr1,
		Vec_Int_t *	vArr2,
		Vec_Int_t *	vCubeFree,
		int *	fWarning )

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

Synopsis [Find a cube-free divisor of the two cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 574 of file abcFx.c.

{
    int * pBeg1 = Vec_IntArray( vArr1 ) + 1;  // skip variable ID
    int * pBeg2 = Vec_IntArray( vArr2 ) + 1;  // skip variable ID
    int * pEnd1 = Vec_IntLimit( vArr1 );
    int * pEnd2 = Vec_IntLimit( vArr2 );
    int Counter = 0, fAttr0 = 0, fAttr1 = 1;
    Vec_IntClear( vCubeFree );
    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
    {
        if ( *pBeg1 == *pBeg2 )
            pBeg1++, pBeg2++, Counter++;
        else if ( *pBeg1 < *pBeg2 )
            Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
        else  
        {
            if ( Vec_IntSize(vCubeFree) == 0 )
                fAttr0 = 1, fAttr1 = 0;
            Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
        }
    }
    while ( pBeg1 < pEnd1 )
        Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
    while ( pBeg2 < pEnd2 )
        Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
    if ( Vec_IntSize(vCubeFree) == 0 )
        printf( "The SOP has duplicated cubes.\n" );
    else if ( Vec_IntSize(vCubeFree) == 1 )
        return -1;
    else if ( Vec_IntSize( vCubeFree ) == 3 )
    {
        int * pArray = Vec_IntArray( vCubeFree ); 
 
        if ( Abc_Lit2Var( pArray[0] ) == Abc_LitNot( Abc_Lit2Var( pArray[1] ) ) )
        {
            if ( Abc_LitIsCompl( pArray[0] ) == Abc_LitIsCompl( pArray[2] ) )
                Vec_IntDrop( vCubeFree, 0 );
            else
                Vec_IntDrop( vCubeFree, 1 );
        }
        else if ( Abc_Lit2Var( pArray[1] ) == Abc_LitNot( Abc_Lit2Var( pArray[2] ) ) )
        {
            if ( Abc_LitIsCompl( pArray[1] ) == Abc_LitIsCompl( pArray[0] ) )
                Vec_IntDrop( vCubeFree, 1 );
            else
                Vec_IntDrop( vCubeFree, 2 );
        }
 
        if ( Vec_IntSize( vCubeFree ) == 2 )
        {
            int Lit0 = Abc_Lit2Var( pArray[0] ),
                Lit1 = Abc_Lit2Var( pArray[1] );
 
            if ( Lit0 > Lit1 )
                ABC_SWAP( int, Lit0, Lit1 );
 
            Vec_IntWriteEntry( vCubeFree, 0, Abc_Var2Lit( Lit0, 0 ) );
            Vec_IntWriteEntry( vCubeFree, 1, Abc_Var2Lit( Lit1, 1 ) );
        }
    }
    assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
    return Counter;
}

Here is the caller graph for this function:

◆ Fx_ManFindCommonPairs()

void Fx_ManFindCommonPairs	(	Vec_Wec_t *	vCubes,
		Vec_Int_t *	vPart0,
		Vec_Int_t *	vPart1,
		Vec_Int_t *	vPairs,
		Vec_Int_t *	vCompls,
		Vec_Int_t *	vDiv,
		Vec_Int_t *	vCubeFree,
		int *	fWarning )

Definition at line 913 of file abcFx.c.

{
    int * pBeg1 = vPart0->pArray;
    int * pBeg2 = vPart1->pArray;
    int * pEnd1 = vPart0->pArray + vPart0->nSize;
    int * pEnd2 = vPart1->pArray + vPart1->nSize;
    int i, k, i_, k_, fCompl, CubeId1, CubeId2;
    Vec_IntClear( vPairs );
    Vec_IntClear( vCompls );
    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
    {
        CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1);
        CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2);
        if ( CubeId1 == CubeId2 )
        {
            for ( i = 1; pBeg1+i < pEnd1; i++ )
                if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg1[i]) )
                    break;
            for ( k = 1; pBeg2+k < pEnd2; k++ )
                if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg2[k]) )
                    break;
            for ( i_ = 0; i_ < i; i_++ )
            for ( k_ = 0; k_ < k; k_++ )
            {
                if ( pBeg1[i_] == pBeg2[k_] )
                    continue;
                Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vCubeFree, fWarning );
                fCompl = (Vec_IntSize(vCubeFree) == 4 && Fx_ManDivNormalize(vCubeFree) == 1);
                if ( !Vec_IntEqual( vDiv, vCubeFree ) )
                    continue;
                Vec_IntPush( vPairs, pBeg1[i_] );
                Vec_IntPush( vPairs, pBeg2[k_] );
                Vec_IntPush( vCompls, fCompl );
            }
            pBeg1 += i;
            pBeg2 += k;
        }
        else if ( CubeId1 < CubeId2 )
            pBeg1++;
        else 
            pBeg2++;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fx_ManStart()

Fx_Man_t * Fx_ManStart ( Vec_Wec_t * vCubes )

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

Synopsis [Starting the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file abcFx.c.

{
    Fx_Man_t * p;
    p = ABC_CALLOC( Fx_Man_t, 1 );
    p->vCubes   = vCubes;
    // temporary data
    p->vCubesS   = Vec_IntAlloc( 100 );
    p->vCubesD   = Vec_IntAlloc( 100 );
    p->vCompls   = Vec_IntAlloc( 100 );
    p->vCubeFree = Vec_IntAlloc( 100 );
    p->vDiv      = Vec_IntAlloc( 100 );
    p->vSCC      = Vec_IntAlloc( 100 );
    return p;
}

Here is the caller graph for this function:

◆ Fx_ManStop()

void Fx_ManStop ( Fx_Man_t * p )

Definition at line 365 of file abcFx.c.

{
//    Vec_WecFree( p->vCubes );
    Vec_WecFree( p->vLits );
    Vec_IntFree( p->vCounts );
    Hsh_VecManStop( p->pHash );
    Vec_FltFree( p->vWeights );
    Vec_QueFree( p->vPrio );
    Vec_IntFree( p->vVarCube );
    Vec_IntFree( p->vLevels );
    // temporary data
    Vec_IntFree( p->vCubesS );
    Vec_IntFree( p->vCubesD );
    Vec_IntFree( p->vCompls );
    Vec_IntFree( p->vCubeFree );
    Vec_IntFree( p->vDiv );
    Vec_IntFree( p->vSCC );
    ABC_FREE( p );
}

Here is the caller graph for this function:

◆ Fx_ManUpdate()

void Fx_ManUpdate	(	Fx_Man_t *	p,
		int	iDiv,
		int *	fWarning )

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

Synopsis [Updates the data-structure when one divisor is selected.]

Description []

SideEffects []

SeeAlso []

Definition at line 968 of file abcFx.c.

{
    Vec_Int_t * vCube, * vCube2, * vLitP = NULL, * vLitN = NULL;
    Vec_Int_t * vDiv = p->vDiv;
    int i, k, Lit0, Lit1, iVarNew = 0, RetValue, Level;
    float Diff = Vec_FltEntry(p->vWeights, iDiv) - (float)((int)Vec_FltEntry(p->vWeights, iDiv));
    assert( Diff > 0.0 && Diff < 1.0 );
 
    // get the divisor and select pivot variables
    p->nDivs++;
    Vec_IntClear( vDiv );
    Vec_IntAppend( vDiv, Hsh_VecReadEntry(p->pHash, iDiv) );
    Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
    assert( Lit0 >= 0 && Lit1 >= 0 );
 
 
    // collect single-cube-divisor cubes
    Vec_IntClear( p->vCubesS );
    if ( Vec_IntSize(vDiv) == 2 )
    {
        Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)) );
        Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)) );
        Vec_IntTwoRemoveCommon( Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)), Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)), p->vCubesS );
    }
 
    // collect double-cube-divisor cube pairs
    Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit0) );
    Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit1) );
    Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, p->vCompls, vDiv, p->vCubeFree, fWarning );
 
    // subtract cost of single-cube divisors
    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
        Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 );  // remove - update
    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
        Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 );  // remove - update
 
    // mark the cubes to be removed
    Vec_WecMarkLevels( p->vCubes, p->vCubesS );
    Vec_WecMarkLevels( p->vCubes, p->vCubesD );
 
    // subtract cost of double-cube divisors
    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1, fWarning );  // remove - update
    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1, fWarning );  // remove - update
 
    // unmark the cubes to be removed
    Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
    Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
 
    if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) == 2 )
        goto ExtractFromPairs;
 
    // create new divisor
    iVarNew = Vec_WecSize( p->vLits ) / 2;
    assert( Vec_IntSize(p->vVarCube) == iVarNew );
    Vec_IntPush( p->vVarCube, Vec_WecSize(p->vCubes) );
    vCube = Vec_WecPushLevel( p->vCubes );
    Vec_IntPush( vCube, iVarNew );
    if ( Vec_IntSize(vDiv) == 2 )
    {
        Vec_IntPush( vCube, Abc_LitNot(Lit0) );
        Vec_IntPush( vCube, Abc_LitNot(Lit1) );
        Level = 1 + Fx_ManComputeLevelCube( p, vCube );
    }
    else
    {
        vCube2 = Vec_WecPushLevel( p->vCubes );
        vCube = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 );
        Vec_IntPush( vCube2, iVarNew );
        Fx_ManDivAddLits( vCube, vCube2, vDiv );
        Level = 2 + Abc_MaxInt( Fx_ManComputeLevelCube(p, vCube), Fx_ManComputeLevelCube(p, vCube2) );
    }
    assert( Vec_IntSize(p->vLevels) == iVarNew );
    Vec_IntPush( p->vLevels, Level );
    // do not add new cubes to the matrix 
    p->nLits += Vec_IntSize( vDiv );
    // create new literals
    vLitP = Vec_WecPushLevel( p->vLits );
    vLitN = Vec_WecPushLevel( p->vLits );
    vLitP = Vec_WecEntry( p->vLits, Vec_WecSize(p->vLits) - 2 );
    // create updated single-cube divisor cubes
    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
    {
        RetValue  = Vec_IntRemove1( vCube, Abc_LitNot(Lit0) );
        RetValue += Vec_IntRemove1( vCube, Abc_LitNot(Lit1) );
        assert( RetValue == 2 );
        Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
        Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) );
        p->nLits--;
    }
    // create updated double-cube divisor cube pairs
ExtractFromPairs:
    k = 0;
    p->nCompls = 0;
    assert( Vec_IntSize(p->vCubesD) % 2 == 0 );
    assert( Vec_IntSize(p->vCubesD) == 2 * Vec_IntSize(p->vCompls) );
    for ( i = 0; i < Vec_IntSize(p->vCubesD); i += 2 )
    {
        int fCompl = Vec_IntEntry(p->vCompls, i/2);
        p->nCompls += fCompl;
        vCube  = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i) );
        vCube2 = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i+1) );
        RetValue  = Fx_ManDivRemoveLits( vCube, vDiv, fCompl );  // cube 2*i
        RetValue += Fx_ManDivRemoveLits( vCube2, vDiv, fCompl ); // cube 2*i+1
        assert( RetValue == Vec_IntSize(vDiv) || RetValue == Vec_IntSize( vDiv ) + 1);
        if ( iVarNew > 0 )
        {
            if ( Vec_IntSize(vDiv) == 2 || fCompl )
            {
                Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) );
                Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
            }
            else 
            {
                Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
                Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
            }
        }
        p->nLits -= Vec_IntSize(vDiv) + Vec_IntSize(vCube2) - 2;
 
        // remove second cube
        Vec_IntWriteEntry( p->vCubesD, k++, Vec_WecLevelId(p->vCubes, vCube) );
        Vec_IntClear( vCube2 ); 
    }
    assert( k == Vec_IntSize(p->vCubesD) / 2 );
    Vec_IntShrink( p->vCubesD, k );
    Vec_IntSort( p->vCubesD, 0 );
    //Vec_IntSort( vLitN, 0 );
    //Vec_IntSort( vLitP, 0 );
 
    // add cost of single-cube divisors
    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 );  // add - update
    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 );  // add - update
 
    // mark the cubes to be removed
    Vec_WecMarkLevels( p->vCubes, p->vCubesS );
    Vec_WecMarkLevels( p->vCubes, p->vCubesD );
 
    // add cost of double-cube divisors
    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1, fWarning );  // add - update
    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1, fWarning );  // add - update
 
    // unmark the cubes to be removed
    Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
    Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
 
    // Deal with SCC
    if ( Vec_IntSize( p->vSCC ) )
    {
        Vec_IntUniqify( p->vSCC );
        Fx_ManForEachCubeVec( p->vSCC, p->vCubes, vCube, i )
        {
            Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1, fWarning );  // remove - update
            Vec_IntClear( vCube );
        }
        Vec_IntClear( p->vSCC );
    }
    // add cost of the new divisor
    if ( Vec_IntSize(vDiv) > 2 )
    {
        vCube  = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 );
        vCube2 = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 1 );
        Fx_ManCubeSingleCubeDivisors( p, vCube,  0, 1 );  // add - update
        Fx_ManCubeSingleCubeDivisors( p, vCube2, 0, 1 );  // add - update
        Vec_IntForEachEntryStart( vCube, Lit0, i, 1 )
            Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube) );
        Vec_IntForEachEntryStart( vCube2, Lit0, i, 1 )
            Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube2) );
    }
 
    // remove these cubes from the lit array of the divisor
    Vec_IntForEachEntry( vDiv, Lit0, i )
    {
        Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD );
        if ( (p->nCompls && i > 1) || Vec_IntSize( vDiv ) == 2 ) // the last two lits are possibly complemented
            Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD );
    }
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ Fx_ManForEachCubeVec

Typedef Documentation

◆ Fx_Man_t

Function Documentation

◆ Abc_NtkFxCheck()

◆ Abc_NtkFxInsert()

◆ Abc_NtkFxPerform()

◆ Abc_NtkFxRetrieve()

◆ Fx_FastExtract()

◆ Fx_ManComputeLevel()

◆ Fx_ManCreateDivisors()

◆ Fx_ManCreateLiterals()

◆ Fx_ManCubeDoubleCubeDivisors()

◆ Fx_ManCubeSingleCubeDivisors()

◆ Fx_ManDivFindCubeFree()

◆ Fx_ManFindCommonPairs()

◆ Fx_ManStart()

◆ Fx_ManStop()

◆ Fx_ManUpdate()