giaHcd.c File Reference

#include "gia.h"
#include "giaAig.h"
#include "aig/aig/aig.h"
#include "opt/dar/dar.h"

Go to the source code of this file.

Data Structures
struct	Hcd_Pars_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Hcd_Pars_t_	Hcd_Pars_t
	DECLARATIONS ///. More...

Functions
void	Gia_ComputeEquivalences (Gia_Man_t *pMiter, int nBTLimit, int fUseMiniSat, int fVerbose)
void	Hcd_ManSetDefaultParams (Hcd_Pars_t *p)
	FUNCTION DEFINITIONS ///. More...
Aig_Man_t *	Hcd_Compress (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Aig_Man_t *	Hcd_Compress2 (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Vec_Ptr_t *	Hcd_ChoiceSynthesis (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
int	Hcd_ManChoiceMiter_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Gia_Man_t *	Hcd_ManChoiceMiter (Vec_Ptr_t *vGias)
int	Hcd_ObjCheckTfi_rec (Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode, Vec_Ptr_t *vVisited)
int	Hcd_ObjCheckTfi (Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
void	Hcd_ManAddNextEntry_rec (Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
void	Hcd_ManEquivToChoices_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
void	Hcd_ManRemoveBadChoices (Gia_Man_t *p)
Gia_Man_t *	Hcd_ManEquivToChoices (Gia_Man_t *p, int nSnapshots)
Aig_Man_t *	Hcd_ComputeChoices (Aig_Man_t *pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose)
void	Hcd_ComputeChoicesTest (Gia_Man_t *pGia, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Hcd_Pars_t_ Hcd_Pars_t

DECLARATIONS ///.

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

FileName [giaHcd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [New choice computation package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 34 of file giaHcd.c.

Function Documentation

void Gia_ComputeEquivalences	(	Gia_Man_t *	pGia,
		int	nBTLimit,
		int	fUseMiniSat,
		int	fVerbose
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 1030 of file giaGiarf.c.

{
    Hcd_Man_t * p;
    Vec_Ptr_t * vRoots;
    Gia_Man_t * pGiaLev;
    int i, Lev, nLevels, nIters;
    clock_t clk;
    Gia_ManRandom( 1 );
    Gia_ManSetPhase( pGia );
    nLevels = Gia_ManLevelNum( pGia );
    Gia_ManIncrementTravId( pGia );
    // start the manager
    p = Gia_ManEquivStart( pGia, nBTLimit, fVerbose );
    // create trivial classes
    Hcd_ManClassesCreate( p );
    // refine
    for ( i = 0; i < 3; i++ )
    {
        clk = clock();       
        Hcd_ManSimulationInit( p );
        Hcd_ManSimulateSimple( p );
        ABC_PRT( "Sim", clock() - clk );
        clk = clock();
        Hcd_ManClassesRefine( p );
        ABC_PRT( "Ref", clock() - clk );
    }
    // process in the levelized order
    for ( Lev = 1; Lev < nLevels; Lev++ )
    {
        clk = clock();
        printf( "LEVEL %3d  (out of %3d)   ", Lev, nLevels );
        pGiaLev = Gia_GenerateReducedLevel( pGia, Lev, &vRoots );
        nIters = Gia_ComputeEquivalencesLevel( p, pGiaLev, vRoots, Lev, fUseMiniSat );
        Gia_ManStop( pGiaLev );
        Vec_PtrFree( vRoots );
        printf( "Iters = %3d   " );
        ABC_PRT( "Time", clock() - clk );
    }
    Gia_GiarfPrintClasses( pGia );
    // clean up
    Gia_ManEquivStop( p );
}

Vec_Ptr_t* Hcd_ChoiceSynthesis	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file giaHcd.c.

{
    Vec_Ptr_t * vGias;
    Gia_Man_t * pGia;

    vGias = Vec_PtrAlloc( 3 );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );

    pAig = Hcd_Compress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );

    pAig = Hcd_Compress2( pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );

    Aig_ManStop( pAig );
    return vGias;
}

Aig_Man_t* Hcd_Compress	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress".]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file giaHcd.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;

    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

//    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    }

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    return pAig;
}

Aig_Man_t* Hcd_Compress2	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fFanout,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file giaHcd.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;
    pParsRwr->fFanout = fFanout;
    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

//    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // balance
//    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    }
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    }
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) Aig_ManPrintStats( pAig );
    }
    return pAig;
}

Aig_Man_t* Hcd_ComputeChoices	(	Aig_Man_t *	pAig,
		int	nBTLimit,
		int	fSynthesis,
		int	fUseMiniSat,
		int	fVerbose
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 610 of file giaHcd.c.

{
    Vec_Ptr_t * vGias;
    Gia_Man_t * pGia, * pMiter;
    Aig_Man_t * pAigNew;
    int i;
    clock_t clk = clock();
    // perform synthesis
    if ( fSynthesis )
    {
        vGias = Hcd_ChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, 0, 0 );
        if ( fVerbose )
            ABC_PRT( "Synthesis time", clock() - clk );
        // create choices
        clk = clock();
        pMiter = Hcd_ManChoiceMiter( vGias );
        Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
            Gia_ManStop( pGia );

        Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
    }
    else 
    {
        vGias = Vec_PtrStart( 3 );
        pMiter = Gia_ManFromAig(pAig);
    }
    // perform choicing
    Gia_ComputeEquivalences( pMiter, nBTLimit, fUseMiniSat, fVerbose );
    // derive AIG with choices
    pGia = Hcd_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
    Gia_ManSetRegNum( pGia, Aig_ManRegNum(pAig) );
    Gia_ManStop( pMiter );
    Vec_PtrFree( vGias );
    if ( fVerbose )
        ABC_PRT( "Choicing time", clock() - clk );
//    Gia_ManHasChoices_very_old( pGia );
    // transform back
    pAigNew = Gia_ManToAig( pGia, 1 );
    Gia_ManStop( pGia );

    if ( fVerbose )
    {
        extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
        extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
        printf( "Choices   : Reprs = %5d. Equivs = %5d. Choices = %5d.\n", 
            Dch_DeriveChoiceCountReprs( pAigNew ), 
            Dch_DeriveChoiceCountEquivs( pAigNew ), 
            Aig_ManChoiceNum( pAigNew ) );
    }

    return pAigNew;
}

void Hcd_ComputeChoicesTest	(	Gia_Man_t *	pGia,
		int	nBTLimit,
		int	fSynthesis,
		int	fUseMiniSat,
		int	fVerbose
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 674 of file giaHcd.c.

{
    Aig_Man_t * pAig, * pAigNew;
    pAig = Gia_ManToAig( pGia, 0 );
    pAigNew = Hcd_ComputeChoices( pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
    Aig_ManStop( pAigNew );
    Aig_ManStop( pAig );
}

void Hcd_ManAddNextEntry_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pOld,
		Gia_Obj_t *	pNode
	)

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

Synopsis [Adds the next entry while making choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file giaHcd.c.

{
    if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
    {
        Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
        return;
    }
    Hcd_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
}

Gia_Man_t* Hcd_ManChoiceMiter

(

Vec_Ptr_t *

vGias

)

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

Synopsis [Derives the miter of several AIGs for choice computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file giaHcd.c.

{
    Gia_Man_t * pNew, * pGia, * pGia0;
    int i, k, iNode, nNodes;
    // make sure they have equal parameters
    assert( Vec_PtrSize(vGias) > 0 );
    pGia0 = (Gia_Man_t *)Vec_PtrEntry( vGias, 0 );
    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
    {
        assert( Gia_ManCiNum(pGia)  == Gia_ManCiNum(pGia0) );
        assert( Gia_ManCoNum(pGia)  == Gia_ManCoNum(pGia0) );
        assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
        Gia_ManFillValue( pGia );
        Gia_ManConst0(pGia)->Value = 0;
    }
    // start the new manager
    pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
    pNew->pName = Abc_UtilStrsav( pGia0->pName );
    pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
    // create new CIs and assign them to the old manager CIs
    for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
    {
        iNode = Gia_ManAppendCi(pNew);
        Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
            Gia_ManCi( pGia, k )->Value = iNode; 
    }
    // create internal nodes
    Gia_ManHashAlloc( pNew );
    for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
    {
        Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
            Hcd_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
    }
    Gia_ManHashStop( pNew );
    // check the presence of dangling nodes
    nNodes = Gia_ManHasDangling( pNew );
    assert( nNodes == 0 );
    return pNew;
}

int Hcd_ManChoiceMiter_rec	(	Gia_Man_t *	pNew,
		Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Duplicates the AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 296 of file giaHcd.c.

{
    if ( ~pObj->Value )
        return pObj->Value;
    Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
    if ( Gia_ObjIsCo(pObj) )
        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
    return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
} 

Gia_Man_t* Hcd_ManEquivToChoices	(	Gia_Man_t *	p,
		int	nSnapshots
	)

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

Synopsis [Reduces AIG using equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 559 of file giaHcd.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    int i;
    assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
    Gia_ManSetPhase( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
    pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
    for ( i = 0; i < Gia_ManObjNum(p); i++ )
        Gia_ObjSetRepr( pNew, i, GIA_VOID );
    Gia_ManFillValue( p );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    Gia_ManForEachRo( p, pObj, i )
        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
        {
            assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
            pObj->Value = pRepr->Value;
        }
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachCo( p, pObj, i )
        Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
    Gia_ManForEachCo( p, pObj, i )
        if ( i % nSnapshots == 0 )
            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    Hcd_ManRemoveBadChoices( pNew );
//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
    return pNew;
} 

void Hcd_ManEquivToChoices_rec	(	Gia_Man_t *	pNew,
		Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Duplicates the AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file giaHcd.c.

{
    Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
    if ( ~pObj->Value )
        return;
    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
    {
        if ( Gia_ObjIsConst0(pRepr) )
        {
            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
            return;
        }
        Hcd_ManEquivToChoices_rec( pNew, p, pRepr );
        assert( Gia_ObjIsAnd(pObj) );
        Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
        Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
        {
            assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
            return;
        }
        if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
            return;
        assert( pRepr->Value < pObj->Value );
        pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
        pObjNew  = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
        if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
        {
            assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
            return;
        }
        if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
        {
            assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
            Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
            Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
        }
        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
    Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}

void Hcd_ManRemoveBadChoices

(

Gia_Man_t *

p

)

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

Synopsis [Removes choices, which contain fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file giaHcd.c.

{
    Gia_Obj_t * pObj;
    int i, iObj, iPrev, Counter = 0;
    // mark nodes with fanout
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
    }
    // go through the classes and remove 
    Gia_ManForEachClass( p, i )
    {
        for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
        {
            if ( !Gia_ManObj(p, iObj)->fMark0 )
            {
                iPrev = iObj; 
                continue;
            }
            Gia_ObjSetRepr( p, iObj, GIA_VOID );
            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
            Gia_ObjSetNext( p, iObj, 0 );
            Counter++;
        } 
    }
    // remove the marks
    Gia_ManCleanMark0( p );
//    printf( "Removed %d bad choices.\n", Counter );
}

void Hcd_ManSetDefaultParams

(

Hcd_Pars_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file giaHcd.c.

{
    memset( p, 0, sizeof(Hcd_Pars_t) );
    p->nWords         =     8;  // the number of simulation words
    p->nBTLimit       =  1000;  // conflict limit at a node
    p->nSatVarMax     =  5000;  // the max number of SAT variables
    p->fSynthesis     =     1;  // derives three snapshots
    p->fPolarFlip     =     1;  // uses polarity adjustment
    p->fSimulateTfo   =     1;  // simulate TFO
    p->fPower         =     0;  // power-aware rewriting
    p->fVerbose       =     0;  // verbose stats
    p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
}

int Hcd_ObjCheckTfi	(	Gia_Man_t *	p,
		Gia_Obj_t *	pOld,
		Gia_Obj_t *	pNode
	)

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

Synopsis [Returns 1 if pOld is in the TFI of pNode.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file giaHcd.c.

{
    Vec_Ptr_t * vVisited;
    Gia_Obj_t * pObj;
    int RetValue, i;
    assert( !Gia_IsComplement(pOld) );
    assert( !Gia_IsComplement(pNode) );
    vVisited = Vec_PtrAlloc( 100 );
    RetValue = Hcd_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
    Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
        pObj->fMark0 = 0;
    Vec_PtrFree( vVisited );
    return RetValue;
}

int Hcd_ObjCheckTfi_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pOld,
		Gia_Obj_t *	pNode,
		Vec_Ptr_t *	vVisited
	)

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

Synopsis [Returns 1 if pOld is in the TFI of pNode.]

Description []

SideEffects []

SeeAlso []

Definition at line 369 of file giaHcd.c.

{
    // check the trivial cases
    if ( pNode == NULL )
        return 0;
    if ( Gia_ObjIsCi(pNode) )
        return 0;
//    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
//        return 0;
    if ( pNode == pOld )
        return 1;
    // skip the visited node
    if ( pNode->fMark0 )
        return 0;
    pNode->fMark0 = 1;
    Vec_PtrPush( vVisited, pNode );
    // check the children
    if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
        return 1;
    if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
        return 1;
    // check equivalent nodes
    return Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
}