abcCollapse.c File Reference

#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"

Include dependency graph for abcCollapse.c:

Go to the source code of this file.

Macros
#define	Abc_NtkSopForEachCube(pSop, nVars, pCube)

Functions
ABC_NAMESPACE_IMPL_START Abc_Ntk_t *	Abc_NtkCollapse (Abc_Ntk_t *pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose)
	DECLARATIONS ///.
Vec_Wec_t *	Gia_ManCreateCoSupps (Gia_Man_t *p, int fVerbose)
int	Gia_ManCoLargestSupp (Gia_Man_t *p, Vec_Wec_t *vSupps)
Vec_Wec_t *	Gia_ManIsoStrashReduceInt (Gia_Man_t *p, Vec_Wec_t *vSupps, int fVerbose)
int	Abc_NtkClpGia_rec (Gia_Man_t *pNew, Abc_Obj_t *pNode)
Gia_Man_t *	Abc_NtkClpGia (Abc_Ntk_t *pNtk)
int	Abc_NtkCollapseReduce (Vec_Str_t *vSop, Vec_Int_t *vSupp, Vec_Int_t *vClass, Vec_Wec_t *vSupps)
sat_solver *	Abc_NtkClpDeriveSatSolver (Cnf_Dat_t *pCnf, int iCoObjId, Vec_Int_t *vSupp, Vec_Int_t *vAnds, Vec_Int_t *vMap, sat_solver **ppSat1, sat_solver **ppSat2, sat_solver **ppSat3)
Vec_Str_t *	Abc_NtkClpGiaOne (Gia_Man_t *p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t *vSupp, int fVerbose, Vec_Int_t *vClass, Vec_Wec_t *vSupps)
Vec_Str_t *	Abc_NtkClpGiaOne2 (Cnf_Dat_t *pCnf, Gia_Man_t *p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t *vSupp, Vec_Int_t *vMap, int fVerbose, Vec_Int_t *vClass, Vec_Wec_t *vSupps)
Vec_Ptr_t *	Abc_GiaDeriveSops (Abc_Ntk_t *pNtkNew, Gia_Man_t *p, Vec_Wec_t *vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose)
Abc_Ntk_t *	Abc_NtkFromSopsInt (Abc_Ntk_t *pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose)
Abc_Ntk_t *	Abc_NtkCollapseSat (Abc_Ntk_t *pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose)

Macro Definition Documentation

Abc_NtkSopForEachCube

#define Abc_NtkSopForEachCube	(		pSop,
			nVars,
			pCube )

Value:

for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )

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

Synopsis [Minimize SOP by removing redundant variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 608 of file abcCollapse.c.

Function Documentation

Abc_GiaDeriveSops()

Vec_Ptr_t * Abc_GiaDeriveSops	(	Abc_Ntk_t *	pNtkNew,
		Gia_Man_t *	p,
		Vec_Wec_t *	vSupps,
		int	nCubeLim,
		int	nBTLimit,
		int	nCostMax,
		int	fCanon,
		int	fReverse,
		int	fCnfShared,
		int	fVerbose )

Definition at line 786 of file abcCollapse.c.

{
    ProgressBar * pProgress;
    abctime clk = Abc_Clock();
    Vec_Ptr_t * vSops = NULL, * vSopsRepr;
    Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
    int i, k, Entry, iCo, * pOrder;
    Vec_Wec_t * vClasses;
    Cnf_Dat_t * pCnf = NULL;
    Vec_Int_t * vMap = NULL;
    // derive classes of outputs
    vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
    if ( fVerbose )
    {
        printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) );
        Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
    }
    // derive representatives
    vReprs = Vec_WecCollectFirsts( vClasses );
    vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) );
    Vec_IntForEachEntry( vReprs, Entry, i )
        Vec_IntPush( vReprSuppSizes, Vec_IntSize(Vec_WecEntry(vSupps, Entry)) );
    pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
    Vec_IntFree( vReprSuppSizes );
    // consider SOPs for representatives
    if ( fCnfShared )
    {
        vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
        pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 1, 0, 0, 0 );
    }
    vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
    pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
    Extra_ProgressBarUpdate( pProgress, 0, NULL );
    for ( i = 0; i < Vec_IntSize(vReprs); i++ )
    {
        int iEntry        = pOrder[Vec_IntSize(vReprs) - 1 - i];
        int iCoThis       = Vec_IntEntry( vReprs, iEntry );
        Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis );
        Vec_Str_t * vSop;
        if ( Vec_IntSize(vSupp) < 2 )
        {
            Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 );
            continue;
        }
        if ( fCnfShared && !fCanon )
            vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
        else
            vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
        if ( vSop == NULL )
            goto finish;
        assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        Vec_PtrWriteEntry( vSopsRepr, iEntry, Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ) );
        Vec_StrFree( vSop );
    }
    Extra_ProgressBarStop( pProgress );
    if ( fCnfShared )
    {
        Cnf_DataFree( pCnf );
        Vec_IntFree( vMap );
    }
    // derive SOPs for each output
    vSops = Vec_PtrStart( Gia_ManCoNum(p) );
    Vec_WecForEachLevel ( vClasses, vClass, i )
        Vec_IntForEachEntry( vClass, iCo, k )
            Vec_PtrWriteEntry( vSops, iCo, Vec_PtrEntry(vSopsRepr, i) );
    assert( Vec_PtrCountZero(vSops) == 0 );
/*
    // verify
    for ( i = 0; i < Gia_ManCoNum(p); i++ )
    {
        Vec_Int_t * vSupp = Vec_WecEntry( vSupps, i );
        char * pSop = (char *)Vec_PtrEntry( vSops, i );
        assert( Vec_IntSize(vSupp) == Abc_SopGetVarNum(pSop) );
    }
*/
    // cleanup
finish:
    ABC_FREE( pOrder );
    Vec_IntFree( vReprs );
    Vec_WecFree( vClasses );
    Vec_PtrFree( vSopsRepr );
    return vSops;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkClpDeriveSatSolver()

sat_solver * Abc_NtkClpDeriveSatSolver	(	Cnf_Dat_t *	pCnf,
		int	iCoObjId,
		Vec_Int_t *	vSupp,
		Vec_Int_t *	vAnds,
		Vec_Int_t *	vMap,
		sat_solver **	ppSat1,
		sat_solver **	ppSat2,
		sat_solver **	ppSat3 )

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

Synopsis [Derives SAT solver for one output from the shared CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file abcCollapse.c.

{
    int i, k, iObj, status, nVars = 2;
//    int i, k, iObj, status, nVars = 1;
    Vec_Int_t * vLits = Vec_IntAlloc( 16 );
    sat_solver * pSat = sat_solver_new();
    if ( ppSat1 ) *ppSat1 = sat_solver_new();
    if ( ppSat2 ) *ppSat2 = sat_solver_new();
    if ( ppSat3 ) *ppSat3 = sat_solver_new();
    // assign SAT variable numbers
    Vec_IntWriteEntry( vMap, iCoObjId, nVars++ );
    Vec_IntForEachEntry( vSupp, iObj, k )
        Vec_IntWriteEntry( vMap, iObj, nVars++ );
    Vec_IntForEachEntry( vAnds, iObj, k )
        if ( pCnf->pObj2Clause[iObj] != -1 )
            Vec_IntWriteEntry( vMap, iObj, nVars++ );
//    Vec_IntForEachEntry( vSupp, iObj, k )
//        Vec_IntWriteEntry( vMap, iObj, nVars++ );
    // create clauses for the internal nodes and for the output
    sat_solver_setnvars( pSat, nVars );
    if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars );
    if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars );
    if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars );
    Vec_IntPush( vAnds, iCoObjId );
    Vec_IntForEachEntry( vAnds, iObj, k )
    {
        int iClaBeg, iClaEnd, * pLit;
        if ( pCnf->pObj2Clause[iObj] == -1 )
            continue;
        iClaBeg = pCnf->pObj2Clause[iObj];
        iClaEnd = iClaBeg + pCnf->pObj2Count[iObj];
        assert( iClaBeg < iClaEnd );
        for ( i = iClaBeg; i < iClaEnd; i++ )
        {
            Vec_IntClear( vLits );
            for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
                Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) );
            status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
            assert( status );
            (void) status;
            if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
            if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
            if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
        }
    }
    Vec_IntPop( vAnds );
    Vec_IntFree( vLits );
    assert( nVars == sat_solver_nvars(pSat) );
    return pSat;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkClpGia()

Gia_Man_t * Abc_NtkClpGia

(

Abc_Ntk_t *

pNtk

)

Definition at line 574 of file abcCollapse.c.

{
    int i, iLit;
    Gia_Man_t * pNew;
    Abc_Obj_t * pNode;
    assert( Abc_NtkIsStrash(pNtk) );
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( pNtk->pName );
    pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
    Abc_NtkForEachObj( pNtk, pNode, i )
        pNode->iTemp = -1;
    Abc_AigConst1(pNtk)->iTemp = 1;
    Abc_NtkForEachCi( pNtk, pNode, i )
        pNode->iTemp = Gia_ManAppendCi(pNew);
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        iLit = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
        iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) );
        Gia_ManAppendCo( pNew, iLit );
    }
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkClpGia_rec()

int Abc_NtkClpGia_rec	(	Gia_Man_t *	pNew,
		Abc_Obj_t *	pNode )

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

Synopsis [Derives GIA for the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 562 of file abcCollapse.c.

{
    int iLit0, iLit1;
    if ( pNode->iTemp >= 0 )
        return pNode->iTemp;
    assert( Abc_ObjIsNode( pNode ) );
    iLit0 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
    iLit1 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin1(pNode) );
    iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) );
    iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) );
    return (pNode->iTemp = Gia_ManAppendAnd(pNew, iLit0, iLit1));
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkClpGiaOne()

Vec_Str_t * Abc_NtkClpGiaOne	(	Gia_Man_t *	p,
		int	iCo,
		int	nCubeLim,
		int	nBTLimit,
		int	fCanon,
		int	fReverse,
		Vec_Int_t *	vSupp,
		int	fVerbose,
		Vec_Int_t *	vClass,
		Vec_Wec_t *	vSupps )

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

Synopsis [Computes SOPs for each output.]

Description []

SideEffects []

SeeAlso []

Definition at line 728 of file abcCollapse.c.

{
    Vec_Str_t * vSop;
    abctime clk = Abc_Clock();
    extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
    Gia_Man_t * pGia  = Gia_ManDupCones( p, &iCo, 1, 1 );
    if ( fVerbose )
        printf( "Output %4d:  Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
    vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
    Gia_ManStop( pGia );
    if ( vSop == NULL )
        return NULL;
    Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
    if ( fVerbose )
        printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
    if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return vSop; 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkClpGiaOne2()

Vec_Str_t * Abc_NtkClpGiaOne2	(	Cnf_Dat_t *	pCnf,
		Gia_Man_t *	p,
		int	iCo,
		int	nCubeLim,
		int	nBTLimit,
		int	fCanon,
		int	fReverse,
		Vec_Int_t *	vSupp,
		Vec_Int_t *	vMap,
		int	fVerbose,
		Vec_Int_t *	vClass,
		Vec_Wec_t *	vSupps )

Definition at line 747 of file abcCollapse.c.

{
    Vec_Str_t * vSop;
    sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
    Gia_Obj_t * pObj;
    abctime clk = Abc_Clock();
    extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
    extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
    extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
    int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) );
    Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
    Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 );
    Gia_ManForEachCiVec( vSupp, p, pObj, i )
        Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) );
    Gia_ManIncrementTravId( p );
    Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds, NULL );
    assert( Vec_IntSize(vAnds) > 0 );
//    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 );
    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL );
    Vec_IntFree( vSuppObjs );
    if ( fVerbose )
        printf( "Output %4d:  Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) );
//    vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
//    vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
    vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
    sat_solver_delete( pSat );
    if ( pSat1 ) sat_solver_delete( pSat1 );
    if ( pSat2 ) sat_solver_delete( pSat2 );
    if ( pSat3 ) sat_solver_delete( pSat3 );
    Vec_IntFree( vAnds );
    if ( vSop == NULL )
        return NULL;
    Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
    if ( fVerbose )
        printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
    if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return vSop; 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkCollapse()

ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkCollapse	(	Abc_Ntk_t *	pNtk,
		int	fBddSizeMax,
		int	fDualRail,
		int	fReorder,
		int	fReverse,
		int	fDumpOrder,
		int	fVerbose )

DECLARATIONS ///.

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

FileName [abcCollapse.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Collapsing the network into two-levels.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 250 of file abcCollapse.c.

{
    return NULL;
}

Here is the caller graph for this function:

Abc_NtkCollapseReduce()

int Abc_NtkCollapseReduce	(	Vec_Str_t *	vSop,
		Vec_Int_t *	vSupp,
		Vec_Int_t *	vClass,
		Vec_Wec_t *	vSupps )

Definition at line 610 of file abcCollapse.c.

{
    int j = 0, i, k, iCo, iVar, nVars = Vec_IntSize(vSupp);
    char * pCube, * pSop = Vec_StrArray(vSop);
    Vec_Int_t * vPres;
    if ( Vec_StrSize(vSop) == 4 ) // constant
    {
        Vec_IntForEachEntry( vClass, iCo, i )
            Vec_IntClear( Vec_WecEntry(vSupps, iCo) );
        return 1;
    }
    vPres = Vec_IntStart( nVars );
    Abc_NtkSopForEachCube( pSop, nVars, pCube )
        for ( k = 0; k < nVars; k++ )
            if ( pCube[k] != '-' )
                Vec_IntWriteEntry( vPres, k, 1 );
    if ( Vec_IntCountZero(vPres) == 0 )
    {
        Vec_IntFree( vPres );
        return 0;
    }
    // reduce cubes
    Abc_NtkSopForEachCube( pSop, nVars, pCube )
        for ( k = 0; k < nVars + 3; k++ )
            if ( k >= nVars || Vec_IntEntry(vPres, k) )
                Vec_StrWriteEntry( vSop, j++, pCube[k] );
    Vec_StrWriteEntry( vSop, j++, '\0' );
    Vec_StrShrink( vSop, j );
    // reduce support
    Vec_IntForEachEntry( vClass, iCo, i )
    {
        j = 0;
        vSupp = Vec_WecEntry( vSupps, iCo );
        Vec_IntForEachEntry( vSupp, iVar, k )
            if ( Vec_IntEntry(vPres, k) )
                Vec_IntWriteEntry( vSupp, j++, iVar );
        Vec_IntShrink( vSupp, j );
    }
    Vec_IntFree( vPres );
//    if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) )
//        printf( "Mismatch!!!\n" );
    return 1;
}

Here is the caller graph for this function:

Abc_NtkCollapseSat()

Abc_Ntk_t * Abc_NtkCollapseSat	(	Abc_Ntk_t *	pNtk,
		int	nCubeLim,
		int	nBTLimit,
		int	nCostMax,
		int	fCanon,
		int	fReverse,
		int	fCnfShared,
		int	fVerbose )

Definition at line 943 of file abcCollapse.c.

{
    Abc_Ntk_t * pNtkNew;
    assert( Abc_NtkIsStrash(pNtk) );
    pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
    if ( pNtkNew == NULL )
        return NULL;
    if ( pNtk->pExdc )
        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCollapseSat: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

Here is the call graph for this function:

Abc_NtkFromSopsInt()

Abc_Ntk_t * Abc_NtkFromSopsInt	(	Abc_Ntk_t *	pNtk,
		int	nCubeLim,
		int	nBTLimit,
		int	nCostMax,
		int	fCanon,
		int	fReverse,
		int	fCnfShared,
		int	fVerbose )

Definition at line 870 of file abcCollapse.c.

{
    Abc_Ntk_t * pNtkNew;
    Gia_Man_t * pGia;
    Vec_Wec_t * vSupps;
    Vec_Int_t * vSupp;
    Vec_Ptr_t * vSops;
    Abc_Obj_t * pNode, * pNodeNew, * pDriver;
    int i, k, iCi; 
    pGia    = Abc_NtkClpGia( pNtk );
    vSupps  = Gia_ManCreateCoSupps( pGia, fVerbose );
    // check the largest output
    if ( nCubeLim > 0 && nCostMax > 0 )
    {
        int iCoMax   = Gia_ManCoLargestSupp( pGia, vSupps );
        int iObjMax  = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) );
        int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
        int nNodeMax = Gia_ManConeSize( pGia, &iObjMax, 1 );
        word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
        if ( Cost > (word)nCostMax )
        {
            printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d  >  %d).\n", 
                nNodeMax, nSuppMax, nCubeLim, nCostMax );
            Gia_ManStop( pGia );
            Vec_WecFree( vSupps );
            return NULL;
        }
    }
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
    vSops   = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
    Gia_ManStop( pGia );
    if ( vSops == NULL )
    {
        Vec_WecFree( vSupps );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        pDriver = Abc_ObjFanin0(pNode);
        if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) )
        {
            Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
            continue;
        }
        if ( Abc_ObjIsCi(pDriver) )
        {
            pNodeNew = Abc_NtkCreateNode( pNtkNew );
            Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); 
            pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
            continue;
        }
        if ( pDriver == Abc_AigConst1(pNtk) )
        {
            pNodeNew = Abc_NtkCreateNode( pNtkNew );
            pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" );
            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
            continue;
        }
        pNodeNew = Abc_NtkCreateNode( pNtkNew );
        vSupp = Vec_WecEntry( vSupps, i );
        Vec_IntForEachEntry( vSupp, iCi, k )
            Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
        pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, (const char*)Vec_PtrEntry( vSops, i ) );
        assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 );
        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
    }
    Vec_WecFree( vSupps );
    Vec_PtrFree( vSops );
    Abc_NtkSortSops( pNtkNew );
    return pNtkNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManCoLargestSupp()

int Gia_ManCoLargestSupp ( Gia_Man_t * p, Vec_Wec_t * vSupps )

extern

Definition at line 4452 of file giaDup.c.

{
    Gia_Obj_t * pObj; 
    Vec_Int_t * vSuppOne;
    int i, iCoMax = -1, nSuppMax = -1;
    Gia_ManForEachCo( p, pObj, i )
    {
        vSuppOne = Vec_WecEntry( vSupps, i );
        if ( nSuppMax < Vec_IntSize(vSuppOne) )
        {
            nSuppMax = Vec_IntSize(vSuppOne);
            iCoMax = i;
        }
    }
    return iCoMax;
}

Here is the caller graph for this function:

Gia_ManCreateCoSupps()

Vec_Wec_t * Gia_ManCreateCoSupps ( Gia_Man_t * p, int fVerbose )

extern

Definition at line 4421 of file giaDup.c.

{
    abctime clk = Abc_Clock();
    Gia_Obj_t * pObj; int i, Id;
    Vec_Wec_t * vSuppsCo = Vec_WecStart( Gia_ManCoNum(p) );
    Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
    Gia_ManForEachCiId( p, Id, i )
        Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
    Gia_ManForEachAnd( p, pObj, Id )
        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), 
                          Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), 
                          Vec_WecEntry(vSupps, Id) ); 
    Gia_ManForEachCo( p, pObj, i )
        Vec_IntAppend( Vec_WecEntry(vSuppsCo, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
    Vec_WecFree( vSupps );
    if ( fVerbose )
        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
    return vSuppsCo;
}

Here is the caller graph for this function:

Gia_ManIsoStrashReduceInt()

Vec_Wec_t * Gia_ManIsoStrashReduceInt ( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose )

extern

Definition at line 4601 of file giaDup.c.

{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 );
    Vec_Int_t * vSuppOne, * vMap = Vec_IntAlloc( 10000 );
    int i, iLit, nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
    // count how many times each support size appears
    Vec_Int_t * vSizeCount = Vec_IntStart( nSuppMax + 1 );
    Vec_WecForEachLevel( vSupps, vSuppOne, i )
        Vec_IntAddToEntry( vSizeCount, Vec_IntSize(vSuppOne), 1 );
    // create array of unique outputs
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    Gia_ManConst0(p)->Value = 0;
    for ( i = 0; i < nSuppMax; i++ )
        Gia_ManAppendCi(pNew);
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachCo( p, pObj, i )
    {
        vSuppOne = Vec_WecEntry( vSupps, i );
        if ( Vec_IntEntry(vSizeCount, Vec_IntSize(vSuppOne)) == 1 )
        {
            Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
            continue;
        }
        iLit = Gia_ManIsoStrashReduceOne( pNew, p, pObj, vSuppOne );
        Vec_IntFillExtra( vMap, iLit + 1, -1 );
        if ( Vec_IntEntry(vMap, iLit) == -1 )
        {
            Vec_IntWriteEntry( vMap, iLit, Vec_WecSize(vPosEquivs) );
            Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
            continue;
        }
        Vec_IntPush( Vec_WecEntry(vPosEquivs, Vec_IntEntry(vMap, iLit)), i );
    }
    Gia_ManHashStop( pNew );
    Gia_ManStop( pNew );
    Vec_IntFree( vSizeCount );
    Vec_IntFree( vMap );
    return vPosEquivs;
}

Here is the call graph for this function:

Here is the caller graph for this function: