#include "base/abc/abc.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecQue.h"
#include "misc/vec/vecVec.h"
#include "misc/vec/vecWec.h"

Include dependency graph for Fxch.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Fxch_SubCube_t_
	STRUCTURES DEFINITIONS ///. More...

struct	Fxch_SCHashTable_Entry_t_

struct	Fxch_SCHashTable_t_

struct	Fxch_Man_t_

Typedefs
typedef unsigned int	uint32_t

typedef struct Fxch_SubCube_t_	Fxch_SubCube_t

typedef struct Fxch_SCHashTable_t_	Fxch_SCHashTable_t

typedef struct Fxch_SCHashTable_Entry_t_	Fxch_SCHashTable_Entry_t

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_NtkFxchPerform (Abc_Ntk_t *pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose)

int	Fxch_FastExtract (Vec_Wec_t *vCubes, int ObjIdMax, int nMaxDivExt, int fVerbose, int fVeryVerbose)

int	Fxch_DivCreate (Fxch_Man_t pFxchMan, Fxch_SubCube_t pSubCube0, Fxch_SubCube_t *pSubCube1)

int	Fxch_DivAdd (Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)

int	Fxch_DivRemove (Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)

void	Fxch_DivSepareteCubes (Vec_Int_t vDiv, Vec_Int_t vCube0, Vec_Int_t *vCube1)

int	Fxch_DivRemoveLits (Vec_Int_t vCube0, Vec_Int_t vCube1, Vec_Int_t vDiv, int fCompl)

void	Fxch_DivPrint (Fxch_Man_t *pFxchMan, int iDiv)

int	Fxch_DivIsNotConstant1 (Vec_Int_t *vDiv)

Fxch_Man_t *	Fxch_ManAlloc (Vec_Wec_t *vCubes)
	PUBLIC INTERFACE ///.

void	Fxch_ManFree (Fxch_Man_t *pFxchMan)

void	Fxch_ManMapLiteralsIntoCubes (Fxch_Man_t *pFxchMan, int nVars)

void	Fxch_ManGenerateLitHashKeys (Fxch_Man_t *pFxchMan)

void	Fxch_ManSCHashTablesInit (Fxch_Man_t *pFxchMan)

void	Fxch_ManSCHashTablesFree (Fxch_Man_t *pFxchMan)

void	Fxch_ManDivCreate (Fxch_Man_t *pFxchMan)

int	Fxch_ManComputeLevelDiv (Fxch_Man_t pFxchMan, Vec_Int_t vCubeFree)

int	Fxch_ManComputeLevelCube (Fxch_Man_t pFxchMan, Vec_Int_t vCube)

void	Fxch_ManComputeLevel (Fxch_Man_t *pFxchMan)

void	Fxch_ManUpdate (Fxch_Man_t *pFxchMan, int iDiv)

void	Fxch_ManPrintDivs (Fxch_Man_t *pFxchMan)

void	Fxch_ManPrintStats (Fxch_Man_t *pFxchMan)

Fxch_SCHashTable_t *	Fxch_SCHashTableCreate (Fxch_Man_t *pFxchMan, int nEntries)

void	Fxch_SCHashTableDelete (Fxch_SCHashTable_t *)

int	Fxch_SCHashTableInsert (Fxch_SCHashTable_t pSCHashTable, Vec_Wec_t vCubes, uint32_t SubCubeID, uint32_t iCube, uint32_t iLit0, uint32_t iLit1, char fUpdate)

int	Fxch_SCHashTableRemove (Fxch_SCHashTable_t pSCHashTable, Vec_Wec_t vCubes, uint32_t SubCubeID, uint32_t iCube, uint32_t iLit0, uint32_t iLit1, char fUpdate)

unsigned int	Fxch_SCHashTableMemory (Fxch_SCHashTable_t *)

void	Fxch_SCHashTablePrint (Fxch_SCHashTable_t *)

Variables
ABC_NAMESPACE_HEADER_START typedef unsigned char	uint8_t

Typedef Documentation

◆ Fxch_SCHashTable_Entry_t

typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t

Definition at line 40 of file Fxch.h.

◆ Fxch_SCHashTable_t

typedef struct Fxch_SCHashTable_t_ Fxch_SCHashTable_t

Definition at line 39 of file Fxch.h.

◆ Fxch_SubCube_t

typedef struct Fxch_SubCube_t_ Fxch_SubCube_t

Definition at line 38 of file Fxch.h.

◆ uint32_t

typedef unsigned int uint32_t

Definition at line 32 of file Fxch.h.

Function Documentation

◆ Abc_NtkFxCheck()

int Abc_NtkFxCheck ( Abc_Ntk_t * pNtk )

extern

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_NtkFxchPerform()

int Abc_NtkFxchPerform	(	Abc_Ntk_t *	pNtk,
		int	nMaxDivExt,
		int	fVerbose,
		int	fVeryVerbose )

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

Synopsis [ Retrives the necessary information for the fast extract with cube hashing. ]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file Fxch.c.

{
    Vec_Wec_t* vCubes;
 
    assert( Abc_NtkIsSopLogic( pNtk ) );
 
    if ( !Abc_NtkFxCheck( pNtk ) )
    {
        printf( "Abc_NtkFxchPerform(): Nodes have duplicated fanins. FXCH is not performed.\n" );
        return 0;
    }
 
    vCubes = Abc_NtkFxRetrieve( pNtk );
    if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, fVerbose, fVeryVerbose ) > 0 )
    {
        Abc_NtkFxInsert( pNtk, vCubes );
        Vec_WecFree( vCubes );
 
        if ( !Abc_NtkCheck( pNtk ) )
            printf( "Abc_NtkFxchPerform(): The network check has failed.\n" );
 
        return 1;
    }
    else
        printf( "Warning: The network has not been changed by \"fxch\".\n" );
 
    Vec_WecFree( vCubes );
 
    return 0;
}

Here is the call graph for this function:

◆ Abc_NtkFxInsert()

void Abc_NtkFxInsert	(	Abc_Ntk_t *	pNtk,
		Vec_Wec_t *	vCubes )

extern

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_NtkFxRetrieve()

Vec_Wec_t * Abc_NtkFxRetrieve ( Abc_Ntk_t * pNtk )

extern

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:

◆ Fxch_DivAdd()

int Fxch_DivAdd	(	Fxch_Man_t *	pFxchMan,
		int	fUpdate,
		int	fSingleCube,
		int	fBase )

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

Synopsis [ Add a divisor to the divisors hash table. ]

Description [ This functions will try to add the divisor store in vCubeFree to the divisor hash table. If the divisor is already present in the hash table it will just increment its weight, otherwise it will add the divisor and asign an initial weight. ]

SideEffects [ If the fUpdate option is set, the function will also update the divisor priority queue. ]

SeeAlso []

Definition at line 228 of file FxchDiv.c.

{
    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
 
    /* Verify if the divisor already exist */ 
    if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
    {
        Vec_WecPushLevel( pFxchMan->vDivCubePairs );
 
        /* Assign initial weight */
        if ( fSingleCube )
        {
            Vec_FltPush( pFxchMan->vDivWeights,
                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
                         -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
        }
        else
        {
            Vec_FltPush( pFxchMan->vDivWeights,
                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
                         -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
        }
 
    }
 
    /* Increment weight */
    if ( fSingleCube )
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
    else
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
 
    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
 
    if ( fUpdate )
        if ( pFxchMan->vDivPrio )
        {
            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
            else
                Vec_QuePush( pFxchMan->vDivPrio, iDiv );
        }
 
    return iDiv;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_DivCreate()

int Fxch_DivCreate	(	Fxch_Man_t *	pFxchMan,
		Fxch_SubCube_t *	pSubCube0,
		Fxch_SubCube_t *	pSubCube1 )

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

Synopsis [ Creates a Divisor. ]

Description [ This functions receive as input two sub-cubes and creates a divisor using their information. The divisor is stored in vCubeFree vector of the pFxchMan structure.

It returns the base value, which is the number of elements that the cubes pair used to generate the devisor have in common. ]

SideEffects []

SeeAlso []

Definition at line 112 of file FxchDiv.c.

{
    int Base = 0;
 
    int SC0_Lit0,
        SC0_Lit1,
        SC1_Lit0,
        SC1_Lit1;
 
    int Cube0Size,
        Cube1Size;
 
    Vec_IntClear( pFxchMan->vCubeFree );
 
    SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
    SC0_Lit1 = 0;
    SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
    SC1_Lit1 = 0;
 
    if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
    {
        Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
        Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
    }
    else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
    {
        int RetValue;
 
        SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
        SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
 
        if ( SC0_Lit0 < SC1_Lit0 )
        {
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
        }
        else
        {
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
        }
 
        RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
        if ( RetValue == -1 )
            return -1;
    } 
    else
    {
        if ( pSubCube0->iLit1 > 0 )
        {
            SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
 
            Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
            if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
            else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
        }
        else 
        {
            SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
 
            Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
            if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
            else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
        }
    }
 
    if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
        return -1;
 
    if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
    {
        Vec_IntSort( pFxchMan->vCubeFree, 0 );
 
        Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
        Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
    }
 
    Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
    Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
    if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
    {
        Base = Abc_MinInt( Cube0Size, Cube1Size )
               -( Vec_IntSize( pFxchMan->vCubeFree ) / 2)  - 1; /* 1 or 2 Lits, 1 SOP NodeID */
    }
    else
        return -1;
 
    return Base;
}

Here is the caller graph for this function:

◆ Fxch_DivIsNotConstant1()

int Fxch_DivIsNotConstant1 ( Vec_Int_t * vDiv )

Definition at line 470 of file FxchDiv.c.

{
    int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
        Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) );
 
    if ( ( Vec_IntSize( vDiv ) == 2 )  && ( Lit0 == Abc_LitNot( Lit1 ) ) )
            return 0;
 
    return 1;
}

Here is the caller graph for this function:

◆ Fxch_DivPrint()

void Fxch_DivPrint	(	Fxch_Man_t *	pFxchMan,
		int	iDiv )

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

Synopsis [ Print the divisor identified by iDiv. ]

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file FxchDiv.c.

{
    Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
    int i,
        Lit;
 
    printf( "Div %7d : ", iDiv );
    printf( "Weight %12.5f  ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
 
    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( !Abc_LitIsCompl( Lit ) )
            printf( "%d(1)", Abc_Lit2Var( Lit ) );
 
    printf( " + " );
 
    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl( Lit ) )
            printf( "%d(2)", Abc_Lit2Var( Lit ) );
 
    printf( " Lits =%7d  ", pFxchMan->nLits );
    printf( "Divs =%8d  \n", Hsh_VecSize( pFxchMan->pDivHash ) );
}

Here is the caller graph for this function:

◆ Fxch_DivRemove()

int Fxch_DivRemove	(	Fxch_Man_t *	pFxchMan,
		int	fUpdate,
		int	fSingleCube,
		int	fBase )

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

Synopsis [ Removes a divisor to the divisors hash table. ]

Description [ This function don't effectively removes a divisor from the hash table (the hash table implementation don't support such operation). It only assures its existence and decrement its weight. ]

SideEffects [ If the fUpdate option is set, the function will also update the divisor priority queue. ]

SeeAlso []

Definition at line 291 of file FxchDiv.c.

{
    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
 
    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
 
    /* Decrement weight */
    if ( fSingleCube )
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
    else
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
 
    if ( fUpdate )
        if ( pFxchMan->vDivPrio )
        {
            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
        }
 
    return iDiv;
}

Here is the caller graph for this function:

◆ Fxch_DivRemoveLits()

int Fxch_DivRemoveLits	(	Vec_Int_t *	vCube0,
		Vec_Int_t *	vCube1,
		Vec_Int_t *	vDiv,
		int *	fCompl )

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

Synopsis [ Removes the literals present in the divisor from their original cubes. ]

Description [ This function returns the numeber of removed literals which should be equal to the size of the divisor. ]

SideEffects []

SeeAlso []

Definition at line 380 of file FxchDiv.c.

{
    int i,
        Lit,
        CountP = 0,
        CountN = 0,
        Count = 0,
        ret = 0;
 
    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
            CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
        else
            CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
 
    Vec_IntForEachEntry( vDiv, Lit, i )
        Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
 
   if ( Vec_IntSize( vDiv ) == 2 )
       Vec_IntForEachEntry( vDiv, Lit, i )
       {
           Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
           Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
       }
 
    ret = Count + CountP + CountN;
 
    if ( Vec_IntSize( vDiv ) == 4 )
    {
        int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
            Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
            Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
            Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
 
        if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
            *fCompl = 1;
 
        if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
        {
            *fCompl = 1;
 
            Vec_IntForEachEntry( vDiv, Lit, i )
                ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
 
            Vec_IntForEachEntry( vDiv, Lit, i )
                ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
        }
    }
 
    return ret;
}

◆ Fxch_DivSepareteCubes()

void Fxch_DivSepareteCubes	(	Vec_Int_t *	vDiv,
		Vec_Int_t *	vCube0,
		Vec_Int_t *	vCube1 )

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

Synopsis [ Separete the cubes in present in a divisor ]

Description [ In this implementation all stored divsors are composed of two cubes.

In order to save space and to be able to use the Vec_Int_t hash table both cubes are stored in the same vector - using a little hack to differentiate which literal belongs to each cube.

This function separetes the two cubes in their own vectors so that they can be added to the cover.

Note* that this also applies to single cube divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]

SideEffects []

SeeAlso []

Definition at line 339 of file FxchDiv.c.

{
    int* pArray;
    int i,
        Lit;
 
    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl(Lit) )
            Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
        else
            Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
 
    if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
    {
        assert( Vec_IntSize( vCube1 ) == 3 );
 
        pArray = Vec_IntArray( vCube0 );
        if ( pArray[1] > pArray[2] )
            ABC_SWAP( int, pArray[1], pArray[2] );
 
        pArray = Vec_IntArray( vCube1 );
        if ( pArray[1] > pArray[2] )
            ABC_SWAP( int, pArray[1], pArray[2] );
    }
}

◆ Fxch_FastExtract()

int Fxch_FastExtract	(	Vec_Wec_t *	vCubes,
		int	ObjIdMax,
		int	nMaxDivExt,
		int	fVerbose,
		int	fVeryVerbose )

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

Synopsis [ Performs fast extract with cube hashing on a set of covers. ]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file Fxch.c.

{
    abctime TempTime;
    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes );
    int i;
 
    TempTime = Abc_Clock();
    Fxch_CubesGruping( pFxchMan );
    Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax );
    Fxch_ManGenerateLitHashKeys( pFxchMan );
    Fxch_ManComputeLevel( pFxchMan );
    Fxch_ManSCHashTablesInit( pFxchMan );
    Fxch_ManDivCreate( pFxchMan );
    pFxchMan->timeInit = Abc_Clock() - TempTime;
 
    if ( fVeryVerbose )
        Fxch_ManPrintDivs( pFxchMan );
 
    if ( fVerbose )
        Fxch_ManPrintStats( pFxchMan );
 
    TempTime = Abc_Clock();
    
    for ( i = 0; (!nMaxDivExt || i < nMaxDivExt) && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
    {
        int iDiv = Vec_QuePop( pFxchMan->vDivPrio );
 
        if ( fVeryVerbose )
            Fxch_DivPrint( pFxchMan, iDiv );
 
        Fxch_ManUpdate( pFxchMan, iDiv );
    }
   
    pFxchMan->timeExt = Abc_Clock() - TempTime;
 
    if ( fVerbose )
    {
        Fxch_ManPrintStats( pFxchMan );
        Abc_PrintTime( 1, "\n[FXCH] Elapsed Time", pFxchMan->timeInit + pFxchMan->timeExt );
        Abc_PrintTime( 1, "[FXCH]    +-> Init", pFxchMan->timeInit );
        Abc_PrintTime( 1, "[FXCH]    +-> Extr", pFxchMan->timeExt );
    }
 
    Fxch_CubesUnGruping( pFxchMan );
    Fxch_ManSCHashTablesFree( pFxchMan );
    Fxch_ManFree( pFxchMan );
 
    Vec_WecRemoveEmpty( vCubes );
    Vec_WecSortByFirstInt( vCubes, 0 );
 
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManAlloc()

Fxch_Man_t * Fxch_ManAlloc ( Vec_Wec_t * vCubes )

PUBLIC INTERFACE ///.

Definition at line 169 of file FxchMan.c.

{
    Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 );
 
    pFxchMan->vCubes = vCubes;
    pFxchMan->nCubesInit = Vec_WecSize( vCubes );
 
    pFxchMan->pDivHash = Hsh_VecManStart( 1024 );
    pFxchMan->vDivWeights = Vec_FltAlloc( 1024 );
    pFxchMan->vDivCubePairs = Vec_WecAlloc( 1024 );
 
    pFxchMan->vCubeFree = Vec_IntAlloc( 4 );
    pFxchMan->vDiv = Vec_IntAlloc( 4 );
 
    pFxchMan->vCubesS = Vec_IntAlloc( 128 );
    pFxchMan->vPairs = Vec_IntAlloc( 128 );
    pFxchMan->vCubesToUpdate = Vec_IntAlloc( 64 );
    pFxchMan->vCubesToRemove = Vec_IntAlloc( 64 );
    pFxchMan->vSCC = Vec_IntAlloc( 64 );
 
    return pFxchMan;
}

Here is the caller graph for this function:

◆ Fxch_ManComputeLevel()

void Fxch_ManComputeLevel ( Fxch_Man_t * pFxchMan )

Definition at line 338 of file FxchMan.c.

{
    Vec_Int_t* vCube;
    int i,
        iVar,
        iFirst = 0;
 
    iVar = Vec_IntEntry( Vec_WecEntry( pFxchMan->vCubes, 0 ), 0 );
    pFxchMan->vLevels = Vec_IntStart( pFxchMan->nVars );
 
    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
    {
        if ( iVar != Vec_IntEntry( vCube, 0 ) )
        {
            Vec_IntAddToEntry( pFxchMan->vLevels, iVar, i - iFirst );
            iVar = Vec_IntEntry( vCube, 0 );
            iFirst = i;
        }
        Vec_IntUpdateEntry( pFxchMan->vLevels, iVar, Fxch_ManComputeLevelCube( pFxchMan, vCube ) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManComputeLevelCube()

int Fxch_ManComputeLevelCube	(	Fxch_Man_t *	pFxchMan,
		Vec_Int_t *	vCube )

Definition at line 325 of file FxchMan.c.

{
    int k,
        Lit,
        Level = 0;
 
    Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
        Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Lit ) ) );
 
    return Level;
}

Here is the caller graph for this function:

◆ Fxch_ManComputeLevelDiv()

int Fxch_ManComputeLevelDiv	(	Fxch_Man_t *	pFxchMan,
		Vec_Int_t *	vCubeFree )

Definition at line 312 of file FxchMan.c.

{
    int i,
        Lit,
        Level = 0;
 
    Vec_IntForEachEntry( vCubeFree, Lit, i )
        Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Abc_Lit2Var( Lit ) ) ) );
 
    return Abc_MinInt( Level, 800 );
}

Here is the caller graph for this function:

◆ Fxch_ManDivCreate()

void Fxch_ManDivCreate ( Fxch_Man_t * pFxchMan )

Definition at line 288 of file FxchMan.c.

{
    Vec_Int_t* vCube;
    float Weight;
    int fAdd = 1,
        fUpdate = 0,
        iCube;
 
    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
    {
        Fxch_ManDivSingleCube( pFxchMan, iCube, fAdd, fUpdate );
        Fxch_ManDivDoubleCube( pFxchMan, iCube, fAdd, fUpdate );
    }
 
    pFxchMan->vDivPrio = Vec_QueAlloc( Vec_FltSize( pFxchMan->vDivWeights ) );
    Vec_QueSetPriority( pFxchMan->vDivPrio, Vec_FltArrayP( pFxchMan->vDivWeights ) );
    Vec_FltForEachEntry( pFxchMan->vDivWeights, Weight, iCube )
    {
        if ( Weight > 0.0 )
            Vec_QuePush( pFxchMan->vDivPrio, iCube );
    }
}

Here is the caller graph for this function:

◆ Fxch_ManFree()

void Fxch_ManFree ( Fxch_Man_t * pFxchMan )

Definition at line 192 of file FxchMan.c.

{
    Vec_WecFree( pFxchMan->vLits );
    Vec_IntFree( pFxchMan->vLitCount );
    Vec_IntFree( pFxchMan->vLitHashKeys );
    Hsh_VecManStop( pFxchMan->pDivHash );
    Vec_FltFree( pFxchMan->vDivWeights );
    Vec_QueFree( pFxchMan->vDivPrio );
    Vec_WecFree( pFxchMan->vDivCubePairs );
    Vec_IntFree( pFxchMan->vLevels );
 
    Vec_IntFree( pFxchMan->vCubeFree );
    Vec_IntFree( pFxchMan->vDiv );
 
    Vec_IntFree( pFxchMan->vCubesS );
    Vec_IntFree( pFxchMan->vPairs );
    Vec_IntFree( pFxchMan->vCubesToUpdate );
    Vec_IntFree( pFxchMan->vCubesToRemove );
    Vec_IntFree( pFxchMan->vSCC );
 
    ABC_FREE( pFxchMan );
}

Here is the caller graph for this function:

◆ Fxch_ManGenerateLitHashKeys()

void Fxch_ManGenerateLitHashKeys ( Fxch_Man_t * pFxchMan )

Definition at line 255 of file FxchMan.c.

{
    int i;
    /* Generates the random number which will be used for hashing cubes */
    Gia_ManRandom( 1 );
    pFxchMan->vLitHashKeys = Vec_IntAlloc( ( 2 * pFxchMan->nVars ) );
    for ( i = 0; i < (2 * pFxchMan->nVars); i++ )
        Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManMapLiteralsIntoCubes()

void Fxch_ManMapLiteralsIntoCubes	(	Fxch_Man_t *	pFxchMan,
		int	nVars )

Definition at line 215 of file FxchMan.c.

{
 
    Vec_Int_t* vCube;
    int i, k,
        Lit,
        Count;
 
    pFxchMan->nVars = 0;
    pFxchMan->nLits = 0;
    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
    {
        assert( Vec_IntSize(vCube) > 0 );
        pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Vec_IntEntry( vCube, 0 ) );
        pFxchMan->nLits += Vec_IntSize(vCube) - 1;
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Abc_Lit2Var( Lit ) );
    }
 
    assert( pFxchMan->nVars < nVars );
    pFxchMan->nVars = nVars;
 
    /* Count the number of time each literal appears on the SOP */
    pFxchMan->vLitCount = Vec_IntStart( 2 * pFxchMan->nVars );
    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            Vec_IntAddToEntry( pFxchMan->vLitCount, Lit, 1 );
 
    /* Allocate space to the array of arrays wich maps Literals into cubes which uses them */
    pFxchMan->vLits = Vec_WecStart( 2 * pFxchMan->nVars );
    Vec_IntForEachEntry( pFxchMan->vLitCount, Count, Lit )
        Vec_IntGrow( Vec_WecEntry( pFxchMan->vLits, Lit ), Count );
 
    /* Maps Literals into cubes which uses them */
    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
            Vec_WecPush( pFxchMan->vLits, Lit, i );
}

Here is the caller graph for this function:

◆ Fxch_ManPrintDivs()

void Fxch_ManPrintDivs ( Fxch_Man_t * pFxchMan )

Definition at line 764 of file FxchMan.c.

{
    int iDiv;
 
    for ( iDiv = 0; iDiv < Vec_FltSize( pFxchMan->vDivWeights ); iDiv++ )
        Fxch_DivPrint( pFxchMan, iDiv );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManPrintStats()

void Fxch_ManPrintStats ( Fxch_Man_t * pFxchMan )

Definition at line 772 of file FxchMan.c.

{
    printf( "Cubes =%8d  ", Vec_WecSizeUsed( pFxchMan->vCubes ) );
    printf( "Lits  =%8d  ", Vec_WecSizeUsed( pFxchMan->vLits ) );
    printf( "Divs  =%8d  ", Hsh_VecSize( pFxchMan->pDivHash ) );
    printf( "Divs+ =%8d  ", Vec_QueSize( pFxchMan->vDivPrio ) );
    printf( "Extr  =%7d  \n", pFxchMan->nExtDivs );
}

Here is the caller graph for this function:

◆ Fxch_ManSCHashTablesFree()

void Fxch_ManSCHashTablesFree ( Fxch_Man_t * pFxchMan )

Definition at line 283 of file FxchMan.c.

{
    Fxch_SCHashTableDelete( pFxchMan->pSCHashTable );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManSCHashTablesInit()

void Fxch_ManSCHashTablesInit ( Fxch_Man_t * pFxchMan )

Definition at line 265 of file FxchMan.c.

{
    Vec_Wec_t* vCubes = pFxchMan->vCubes;
    Vec_Int_t* vCube;
    int iCube,
        nTotalHashed = 0;
 
    Vec_WecForEachLevel( vCubes, vCube, iCube )
    {
        int nLits = Vec_IntSize( vCube ) - 1,
            nSubCubes = nLits <= 2? nLits + 1: ( nLits * nLits + nLits ) / 2;
 
        nTotalHashed += nSubCubes + 1;
    }
 
    pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, nTotalHashed );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_ManUpdate()

void Fxch_ManUpdate	(	Fxch_Man_t *	p,
		int	iDiv )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 617 of file plaFxch.c.

{
    Vec_Int_t * vCube1, * vCube2, * vLitP, * vLitN;
    //int nLitsNew = p->nLits - (int)Vec_FltEntry(&p->vWeights, iDiv);
    int i, Lit0, Lit1, hCube1, hCube2, iVarNew;
    //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
    Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); 
    Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF );
    Lit0 = Hash_IntObjData0( p->vHash, iDiv );
    Lit1 = Hash_IntObjData1( p->vHash, iDiv );
    assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 );
    Vec_WrdPush( &p->vDivs, ((word)Lit1 << 32) | (word)Lit0 );
 
    // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
    // although it is not strictly correct, it seems to be fine to just skip such divisors
//    if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->vHash, iDiv)) == 2 )
//        return;
 
    // collect single-cube-divisor cubes
    vLitP = Vec_WecEntry(&p->vLits, Lit0);
    vLitN = Vec_WecEntry(&p->vLits, Lit1);
    Fxch_CompressCubes( p, vLitP );
    Fxch_CompressCubes( p, vLitN );
//    Fxch_CollectSingles( vLitP, vLitN, &p->vCubesS );
//    assert( Vec_IntSize(&p->vCubesS) % 2 == 0 );
    Vec_IntTwoRemoveCommon( vLitP, vLitN, &p->vCubesS );
    Fxch_FilterCubes( p, &p->vCubesS, Lit0, Lit1 );
 
    // collect double-cube-divisor cube pairs
    Fxch_CollectDoubles( p, Vec_WecEntry(&p->vPairs, iDiv), &p->vCubesD, Abc_LitNot(Lit0), Abc_LitNot(Lit1) );
    assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
    Vec_IntUniqifyPairs( &p->vCubesD );
    assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
 
    // subtract cost of single-cube divisors
//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 );  // remove - update
    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ),  // remove - update
        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube2), 0 );  // remove - update
 
    // subtract cost of double-cube divisors
//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
    {
        //printf( "%d ", Pla_CubeNum(hCube1) );
        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 );  // remove - update
    }
    //printf( "\n" );
 
    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
    {
        //printf( "%d ", Pla_CubeNum(hCube1) );
        //printf( "%d  ", Pla_CubeNum(hCube2) );
        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ),  // remove - update
        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube2), 0 );  // remove - update
    }
    //printf( "\n" );
 
    // create new literals
    p->nLits += 2;
    iVarNew = Vec_WecSize( &p->vLits ) / 2;
    vLitP = Vec_WecPushLevel( &p->vLits );
    vLitN = Vec_WecPushLevel( &p->vLits );
    vLitP = Vec_WecEntry( &p->vLits, Vec_WecSize(&p->vLits) - 2 );
    // update single-cube divisor cubes
//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
    {
//        int Lit0s, Lit1s;
        vCube1 = Fxch_ManCube( p, hCube1 );
//        Lit0s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube1));
//        Lit1s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube2));
//        assert( Pla_CubeNum(hCube1) == Pla_CubeNum(hCube2) );
//        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Lit0 );
//        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube2)) == Lit1 );
        Fxch_CompressLiterals( vCube1, Lit0, Lit1 );
//        Vec_IntPush( vLitP, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
        Vec_IntPush( vLitP, Pla_CubeNum(hCube1) );
        Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 0) );
 
        //if ( Pla_CubeNum(hCube1) == 3 )
        //    printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
 
        p->nLits--;
    }
    // update double-cube divisor cube pairs
    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
    {
        vCube1 = Fxch_ManCube( p, hCube1 );
        vCube2 = Fxch_ManCube( p, hCube2 );
        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Abc_LitNot(Lit0) );
        assert( Vec_IntEntry(vCube2, Pla_CubeLit(hCube2)) == Abc_LitNot(Lit1) );
        Fxch_CompressLiterals2( vCube1, Pla_CubeLit(hCube1), -1 );
//        Vec_IntPush( vLitN, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
        Vec_IntPush( vLitN, Pla_CubeNum(hCube1) );
        Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 1) );
        p->nLits -= Vec_IntSize(vCube2);
 
        //if ( Pla_CubeNum(hCube1) == 3 )
        //    printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
 
        // remove second cube
        Vec_IntClear( vCube2 ); 
    }
    Vec_IntSort( vLitN, 0 );
    Vec_IntSort( vLitP, 0 );
 
    // add cost of single-cube divisors
//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
 
    // add cost of double-cube divisors
//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
    
    // check predicted improvement: (new SOP lits == old SOP lits - divisor weight)
    //assert( p->nLits == nLitsNew );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fxch_SCHashTableCreate()

Fxch_SCHashTable_t * Fxch_SCHashTableCreate	(	Fxch_Man_t *	pFxchMan,
		int	nEntries )

Definition at line 93 of file FxchSCHashTable.c.

{
    Fxch_SCHashTable_t* pSCHashTable = ABC_CALLOC( Fxch_SCHashTable_t, 1 );
    int nBits = Abc_Base2Log( nEntries + 1 );
 
 
    pSCHashTable->pFxchMan = pFxchMan;
    pSCHashTable->SizeMask = (1 << nBits) - 1;
    pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 );
 
    return pSCHashTable;
}

Here is the caller graph for this function:

◆ Fxch_SCHashTableDelete()

void Fxch_SCHashTableDelete ( Fxch_SCHashTable_t * pSCHashTable )

Definition at line 107 of file FxchSCHashTable.c.

{
    unsigned i;
    for ( i = 0; i <= pSCHashTable->SizeMask; i++ )
        ABC_FREE( pSCHashTable->pBins[i].vSCData );
    Vec_IntErase( &pSCHashTable->vSubCube0 );
    Vec_IntErase( &pSCHashTable->vSubCube1 );
    ABC_FREE( pSCHashTable->pBins );
    ABC_FREE( pSCHashTable );
}

Here is the caller graph for this function:

◆ Fxch_SCHashTableInsert()

int Fxch_SCHashTableInsert	(	Fxch_SCHashTable_t *	pSCHashTable,
		Vec_Wec_t *	vCubes,
		uint32_t	SubCubeID,
		uint32_t	iCube,
		uint32_t	iLit0,
		uint32_t	iLit1,
		char	fUpdate )

Definition at line 179 of file FxchSCHashTable.c.

{
    int iNewEntry;
    int Pairs = 0;
    uint32_t BinID;
    Fxch_SCHashTable_Entry_t* pBin;
    Fxch_SubCube_t* pNewEntry;
    int iEntry;
 
    MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
    pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
 
    if ( pBin->vSCData == NULL )
    {
        pBin->vSCData = ABC_CALLOC( Fxch_SubCube_t, 16 );
        pBin->Size = 0;
        pBin->Cap = 16;
    }
    else if ( pBin->Size == pBin->Cap )
    {
        assert(pBin->Cap <= 0xAAAA);
        pBin->Cap = ( pBin->Cap >> 1 ) * 3;
        pBin->vSCData = ABC_REALLOC( Fxch_SubCube_t, pBin->vSCData, pBin->Cap );
    }
 
    iNewEntry = pBin->Size++;
    pBin->vSCData[iNewEntry].Id = SubCubeID;
    pBin->vSCData[iNewEntry].iCube = iCube;
    pBin->vSCData[iNewEntry].iLit0 = iLit0;
    pBin->vSCData[iNewEntry].iLit1 = iLit1;
    pSCHashTable->nEntries++;
 
    if ( pBin->Size == 1 )
        return 0;
 
    pNewEntry = &( pBin->vSCData[iNewEntry] );
    for ( iEntry = 0; iEntry < (int)pBin->Size - 1; iEntry++ )
    {
        Fxch_SubCube_t* pEntry = &( pBin->vSCData[iEntry] );
        int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
        int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNewEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
        int Result = 0;
        int Base;
        int iNewDiv = -1, i, z;
 
        if ( (pEntry->iLit1 != 0 && pNewEntry->iLit1 == 0) || (pEntry->iLit1 == 0 && pNewEntry->iLit1 != 0)  )
            continue;
 
        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNewEntry ) )
            continue;
 
        if ( ( pEntry->iLit0 == 0 ) || ( pNewEntry->iLit0 == 0 ) )
        {
            Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->iCube ),
                     * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pNewEntry->iCube );
 
            if ( Vec_IntSize( vCube0 ) > Vec_IntSize( vCube1 ) )
            {
                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
            }
            else
            {
                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
            }
 
            continue;
        }
 
        Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pEntry, pNewEntry );
 
        if ( Base < 0 )
            continue;
 
        for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
            Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
 
        for ( z = 0; z < Result; z++ )
            iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->iCube );
        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->iCube );
 
        Pairs++;
    }
 
    return Pairs;
}

Here is the call graph for this function:

◆ Fxch_SCHashTableMemory()

unsigned int Fxch_SCHashTableMemory ( Fxch_SCHashTable_t * pHashTable )

Definition at line 362 of file FxchSCHashTable.c.

{
    unsigned int Memory = sizeof ( Fxch_SCHashTable_t );
 
    Memory += sizeof( Fxch_SubCube_t ) * ( pHashTable->SizeMask + 1 );
 
    return Memory;
}

Here is the caller graph for this function:

◆ Fxch_SCHashTablePrint()

void Fxch_SCHashTablePrint ( Fxch_SCHashTable_t * pHashTable )

Definition at line 371 of file FxchSCHashTable.c.

{
    int Memory;
    printf( "SubCube Hash Table at %p\n", ( void* )pHashTable );
    printf("%20s %20s\n", "nEntries",
                          "Memory Usage (MB)" );
 
    Memory = Fxch_SCHashTableMemory( pHashTable );
    printf("%20d %18.2f\n", pHashTable->nEntries,
                            ( ( double ) Memory / 1048576 ) );
}

Here is the call graph for this function:

◆ Fxch_SCHashTableRemove()

int Fxch_SCHashTableRemove	(	Fxch_SCHashTable_t *	pSCHashTable,
		Vec_Wec_t *	vCubes,
		uint32_t	SubCubeID,
		uint32_t	iCube,
		uint32_t	iLit0,
		uint32_t	iLit1,
		char	fUpdate )

Definition at line 275 of file FxchSCHashTable.c.

{
    int iEntry;
    int Pairs = 0;
    uint32_t BinID;
    Fxch_SCHashTable_Entry_t* pBin;
    Fxch_SubCube_t* pEntry;
    int idx;
 
    MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
 
    pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
 
    if ( pBin->Size == 1 )
    {
        pBin->Size = 0;
        return 0;
    }
 
    for ( iEntry = 0; iEntry < (int)pBin->Size; iEntry++ )
        if ( pBin->vSCData[iEntry].iCube == iCube )
            break;
 
    assert( ( iEntry != (int)pBin->Size ) && ( pBin->Size != 0 ) );
 
    pEntry = &( pBin->vSCData[iEntry] );
    for ( idx = 0; idx < (int)pBin->Size; idx++ )
    if ( idx != iEntry )
    {
        int Base,
            iDiv = -1;
 
        int i, z,
            iCube0,
            iCube1;
 
        Fxch_SubCube_t* pNextEntry = &( pBin->vSCData[idx] );
        Vec_Int_t* vDivCubePairs;
        int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
        int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNextEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
        int Result = 0;
 
        if ( (pEntry->iLit1 != 0 && pNextEntry->iLit1 == 0) || (pEntry->iLit1 == 0 && pNextEntry->iLit1 != 0)  )
            continue;
 
        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNextEntry )
             || pEntry->iLit0 == 0
             || pNextEntry->iLit0 == 0 )
            continue;
 
        Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pNextEntry, pEntry );
 
        if ( Base < 0 )
            continue;
 
        for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
            Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
 
        for ( z = 0; z < Result; z++ )
            iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
        vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv );
        Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i )
            if ( ( iCube0 == (int)pNextEntry->iCube && iCube1 == (int)pEntry->iCube )  ||
                 ( iCube0 == (int)pEntry->iCube && iCube1 == (int)pNextEntry->iCube ) )
            {
                Vec_IntDrop( vDivCubePairs, i+1 );
                Vec_IntDrop( vDivCubePairs, i );
            }
        if ( Vec_IntSize( vDivCubePairs ) == 0 )
            Vec_IntErase( vDivCubePairs );
 
        Pairs++;
    }
 
    memmove(pBin->vSCData + iEntry, pBin->vSCData + iEntry + 1, (pBin->Size - iEntry - 1) * sizeof(*pBin->vSCData));
    pBin->Size -= 1;
 
    return Pairs;
}

Here is the call graph for this function:

Variable Documentation

◆ uint8_t

ABC_NAMESPACE_HEADER_START typedef unsigned char uint8_t

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

FileName [ Fxch.h ]

PackageName [ Fast eXtract with Cube Hashing (FXCH) ]

Synopsis [ External declarations of fast extract with cube hashing. ]

Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]

Affiliation [ UFRGS ]

Date [ Ver. 1.0. Started - March 6, 2016. ]

Revision []

Definition at line 31 of file Fxch.h.

Classes

Typedefs

Functions

Variables

Typedef Documentation

◆ Fxch_SCHashTable_Entry_t

◆ Fxch_SCHashTable_t

◆ Fxch_SubCube_t

◆ uint32_t

Function Documentation

◆ Abc_NtkFxCheck()

◆ Abc_NtkFxchPerform()

◆ Abc_NtkFxInsert()

◆ Abc_NtkFxRetrieve()

◆ Fxch_DivAdd()

◆ Fxch_DivCreate()

◆ Fxch_DivIsNotConstant1()

◆ Fxch_DivPrint()

◆ Fxch_DivRemove()

◆ Fxch_DivRemoveLits()

◆ Fxch_DivSepareteCubes()

◆ Fxch_FastExtract()

◆ Fxch_ManAlloc()

◆ Fxch_ManComputeLevel()

◆ Fxch_ManComputeLevelCube()

◆ Fxch_ManComputeLevelDiv()

◆ Fxch_ManDivCreate()

◆ Fxch_ManFree()

◆ Fxch_ManGenerateLitHashKeys()

◆ Fxch_ManMapLiteralsIntoCubes()

◆ Fxch_ManPrintDivs()

◆ Fxch_ManPrintStats()

◆ Fxch_ManSCHashTablesFree()

◆ Fxch_ManSCHashTablesInit()

◆ Fxch_ManUpdate()

◆ Fxch_SCHashTableCreate()

◆ Fxch_SCHashTableDelete()

◆ Fxch_SCHashTableInsert()

◆ Fxch_SCHashTableMemory()

◆ Fxch_SCHashTablePrint()

◆ Fxch_SCHashTableRemove()

Variable Documentation

◆ uint8_t