abcDress2.c File Reference

#include "base/abc/abc.h"
#include "aig/aig/aig.h"
#include "proof/dch/dch.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Abc_ObjEquivId2ObjId (int EquivId)
int	Abc_ObjEquivId2Polar (int EquivId)
int	Abc_ObjEquivId2NtkId (int EquivId)
Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///. More...
void	Dch_ComputeEquivalences (Aig_Man_t *pAig, Dch_Pars_t *pPars)
Aig_Man_t *	Aig_ManCreateDualOutputMiter (Aig_Man_t *p1, Aig_Man_t *p2)
	FUNCTION DEFINITIONS ///. More...
void	Abc_NtkDressMapSetPolarity (Abc_Ntk_t *pNtk)
Vec_Int_t *	Abc_NtkDressMapClasses (Aig_Man_t *pMiter, Abc_Ntk_t *pNtk)
Vec_Int_t *	Abc_ObjDressClass (Vec_Ptr_t *vRes, Vec_Int_t *vClass2Num, int Class)
int	Abc_ObjDressMakeId (Abc_Ntk_t *pNtk, int ObjId, int iNtk)
Vec_Ptr_t *	Abc_NtkDressMapIds (Aig_Man_t *pMiter, Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2)
Vec_Ptr_t *	Abc_NtkDressComputeEquivs (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nConflictLimit, int fVerbose)
void	Abc_NtkDressPrintEquivs (Vec_Ptr_t *vRes)
void	Abc_NtkDressPrintStats (Vec_Ptr_t *vRes, int nNodes0, int nNodes1, abctime Time)
void	Abc_NtkDress2 (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nConflictLimit, int fVerbose)

Function Documentation

void Abc_NtkDress2	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int	nConflictLimit,
		int	fVerbose
	)

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

Synopsis [Transfers names from pNtk1 to pNtk2.]

Description [Internally calls new procedure for mapping node IDs of both networks into the shared equivalence classes.]

SideEffects []

SeeAlso []

Definition at line 419 of file abcDress2.c.

{
    Vec_Ptr_t * vRes;
    abctime clk = Abc_Clock();
    vRes = Abc_NtkDressComputeEquivs( pNtk1, pNtk2, nConflictLimit, fVerbose );
//    Abc_NtkDressPrintEquivs( vRes );
    Abc_NtkDressPrintStats( vRes, Abc_NtkNodeNum(pNtk1), Abc_NtkNodeNum(pNtk1), Abc_Clock() - clk );
    Vec_VecFree( (Vec_Vec_t *)vRes );
}

Vec_Ptr_t* Abc_NtkDressComputeEquivs	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int	nConflictLimit,
		int	fVerbose
	)

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

Synopsis [Computes equivalence classes of objects in pNtk1 and pNtk2.]

Description [Returns the array (Vec_Ptr_t) of integer arrays (Vec_Int_t). Each of the integer arrays contains entries of one equivalence class. Each entry contains the following information: the network number (0/1), the polarity (0/1) and the object ID in the the network (0 <= num < MaxId) where MaxId is the largest number of an ID of an object in that network.]

SideEffects []

SeeAlso []

Definition at line 290 of file abcDress2.c.

{
    Dch_Pars_t Pars, * pPars = &Pars;
    Abc_Ntk_t * pAig1, * pAig2;
    Aig_Man_t * pMan1, * pMan2, * pMiter;
    Vec_Ptr_t * vRes;
    assert( !Abc_NtkIsStrash(pNtk1) );
    assert( !Abc_NtkIsStrash(pNtk2) );
    // convert network into AIG
    pAig1 = Abc_NtkStrash( pNtk1, 1, 1, 0 );
    pAig2 = Abc_NtkStrash( pNtk2, 1, 1, 0 );
    pMan1 = Abc_NtkToDar( pAig1, 0, 0 );
    pMan2 = Abc_NtkToDar( pAig2, 0, 0 );
    // derive the miter
    pMiter = Aig_ManCreateDualOutputMiter( pMan1, pMan2 );
    // set up parameters for SAT sweeping
    Dch_ManSetDefaultParams( pPars );
    pPars->nBTLimit = nConflictLimit;
    pPars->fVerbose = fVerbose;
    // perform SAT sweeping
    Dch_ComputeEquivalences( pMiter, pPars );
    // now, pMiter is annotated with the equivl class info
    // convert this info into the resulting array
    vRes = Abc_NtkDressMapIds( pMiter, pNtk1, pNtk2 );
    Aig_ManStop( pMiter );
    Aig_ManStop( pMan1 );
    Aig_ManStop( pMan2 );
    Abc_NtkDelete( pAig1 );
    Abc_NtkDelete( pAig2 );
    return vRes;
}

Vec_Int_t* Abc_NtkDressMapClasses	(	Aig_Man_t *	pMiter,
		Abc_Ntk_t *	pNtk
	)

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

Synopsis [Create mapping of node IDs of pNtk into equiv classes of pMiter.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file abcDress2.c.

{
    Vec_Int_t * vId2Lit;
    Abc_Obj_t * pObj, * pAnd;
    Aig_Obj_t * pObjMan, * pObjMiter, * pObjRepr;
    int i;
    vId2Lit = Vec_IntAlloc( 0 );
    Vec_IntFill( vId2Lit, Abc_NtkObjNumMax(pNtk), -1 );
    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        // get the pointer to the miter node corresponding to pObj
        if ( (pAnd = Abc_ObjRegular(pObj->pCopy)) && Abc_ObjType(pAnd) != ABC_OBJ_NONE &&          // strashed node is present and legal
             (pObjMan = Aig_Regular((Aig_Obj_t *)pAnd->pCopy)) && Aig_ObjType(pObjMan) != AIG_OBJ_NONE &&       // AIG node is present and legal
             (pObjMiter = Aig_Regular((Aig_Obj_t *)pObjMan->pData)) && Aig_ObjType(pObjMiter) != AIG_OBJ_NONE ) // miter node is present and legal
        {
            // get the representative of the miter node
            pObjRepr = Aig_ObjRepr( pMiter, pObjMiter );
            pObjRepr = pObjRepr? pObjRepr : pObjMiter;
            // map pObj (whose ID is i) into the repr node ID (i.e. equiv class)
            Vec_IntWriteEntry( vId2Lit, i, Aig_ObjId(pObjRepr) );
        }
    }
    return vId2Lit;
}

Vec_Ptr_t* Abc_NtkDressMapIds	(	Aig_Man_t *	pMiter,
		Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2
	)

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

Synopsis [Computes equivalence classes of objects in pNtk1 and pNtk2.]

Description [Internal procedure.]

SideEffects []

SeeAlso []

Definition at line 225 of file abcDress2.c.

{
    Vec_Ptr_t * vRes;
    Vec_Int_t * vId2Lit1, * vId2Lit2, * vCounts0, * vCounts1, * vClassC, * vClass2Num;
    int i, Class;
    // start the classes
    vRes = Vec_PtrAlloc( 1000 );
    // set polarity of the nodes
    Abc_NtkDressMapSetPolarity( pNtk1 );
    Abc_NtkDressMapSetPolarity( pNtk2 );
    // create mapping of node IDs of pNtk1/pNtk2 into the IDs of equiv classes of pMiter
    vId2Lit1 = Abc_NtkDressMapClasses( pMiter, pNtk1 );
    vId2Lit2 = Abc_NtkDressMapClasses( pMiter, pNtk2 );
    // count the number of nodes in each equivalence class
    vCounts0 = Vec_IntStart( Aig_ManObjNumMax(pMiter) );
    Vec_IntForEachEntry( vId2Lit1, Class, i )
        if ( Class >= 0 )
            Vec_IntAddToEntry( vCounts0, Class, 1 );
    vCounts1 = Vec_IntStart( Aig_ManObjNumMax(pMiter) );
    Vec_IntForEachEntry( vId2Lit2, Class, i )
        if ( Class >= 0 )
            Vec_IntAddToEntry( vCounts1, Class, 1 );
    // get the costant class
    vClassC = Vec_IntAlloc( 100 );
    Vec_IntForEachEntry( vId2Lit1, Class, i )
        if ( Class == 0 )
            Vec_IntPush( vClassC, Abc_ObjDressMakeId(pNtk1, i, 0) );
    Vec_IntForEachEntry( vId2Lit2, Class, i )
        if ( Class == 0 )
            Vec_IntPush( vClassC, Abc_ObjDressMakeId(pNtk2, i, 1) );
    Vec_PtrPush( vRes, vClassC );
    // map repr node IDs into class numbers
    vClass2Num = Vec_IntAlloc( 0 );
    Vec_IntFill( vClass2Num, Aig_ManObjNumMax(pMiter), -1 );
    // keep classes having at least one element from pNtk1 and one from pNtk2
    Vec_IntForEachEntry( vId2Lit1, Class, i )
        if ( Class > 0 && Vec_IntEntry(vCounts0, Class) && Vec_IntEntry(vCounts1, Class) )
            Vec_IntPush( Abc_ObjDressClass(vRes, vClass2Num, Class), Abc_ObjDressMakeId(pNtk1, i, 0) );
    Vec_IntForEachEntry( vId2Lit2, Class, i )
        if ( Class > 0 && Vec_IntEntry(vCounts0, Class) && Vec_IntEntry(vCounts1, Class) )
            Vec_IntPush( Abc_ObjDressClass(vRes, vClass2Num, Class), Abc_ObjDressMakeId(pNtk2, i, 1) );
    // package them accordingly
    Vec_IntFree( vClass2Num );
    Vec_IntFree( vCounts0 );
    Vec_IntFree( vCounts1 );
    Vec_IntFree( vId2Lit1 );
    Vec_IntFree( vId2Lit2 );
    return vRes;
}

void Abc_NtkDressMapSetPolarity

(

Abc_Ntk_t *

pNtk

)

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

Synopsis [Sets polarity attribute of each object in the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 123 of file abcDress2.c.

{
    Abc_Obj_t * pObj, * pAnd;
    int i;
    // each node refers to the the strash copy whose polarity is set
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        if ( (pAnd = Abc_ObjRegular(pObj->pCopy)) && Abc_ObjType(pAnd) != ABC_OBJ_NONE ) // strashed object is present and legal
            pObj->fPhase = pAnd->fPhase ^ Abc_ObjIsComplement(pObj->pCopy);
    }
}

void Abc_NtkDressPrintEquivs

(

Vec_Ptr_t *

vRes

)

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

Synopsis [Prints information about node equivalences.]

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file abcDress2.c.

{
    Vec_Int_t * vClass;
    int i, k, Entry;
    Vec_PtrForEachEntry( Vec_Int_t *, vRes, vClass, i )
    {
        printf( "Class %5d : ", i );
        printf( "Num =%5d    ", Vec_IntSize(vClass) );
        Vec_IntForEachEntry( vClass, Entry, k )
            printf( "%5d%c%d ", 
                Abc_ObjEquivId2ObjId(Entry), 
                Abc_ObjEquivId2Polar(Entry)? '-':'+', 
                Abc_ObjEquivId2NtkId(Entry) );
        printf( "\n" );
    }
}

void Abc_NtkDressPrintStats	(	Vec_Ptr_t *	vRes,
		int	nNodes0,
		int	nNodes1,
		abctime	Time
	)

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

Synopsis [Prints information about node equivalences.]

Description []

SideEffects []

SeeAlso []

Definition at line 361 of file abcDress2.c.

{
    Vec_Int_t * vClass;
    int i, k, Entry;
    int NegAll[2] = {0}, PosAll[2] = {0}, PairsAll = 0, PairsOne = 0;
    int Pos[2], Neg[2];
    // count the number of equivalences in each class
    Vec_PtrForEachEntry( Vec_Int_t *, vRes, vClass, i )
    {
        Pos[0] = Pos[1] = 0;
        Neg[0] = Neg[1] = 0;
        Vec_IntForEachEntry( vClass, Entry, k )
        {
            if ( Abc_ObjEquivId2NtkId(Entry) )
            {
                if ( Abc_ObjEquivId2Polar(Entry) )
                    Neg[1]++; // negative polarity in network 1
                else
                    Pos[1]++; // positive polarity in network 1
            }
            else
            {
                if ( Abc_ObjEquivId2Polar(Entry) )
                    Neg[0]++; // negative polarity in network 0
                else
                    Pos[0]++; // positive polarity in network 0
            }
        }
        PosAll[0] += Pos[0]; // total positive polarity in network 0
        PosAll[1] += Pos[1]; // total positive polarity in network 1
        NegAll[0] += Neg[0]; // total negative polarity in network 0
        NegAll[1] += Neg[1]; // total negative polarity in network 1

        // assuming that the name can be transferred to only one node
        PairsAll += Abc_MinInt(Neg[0] + Pos[0], Neg[1] + Pos[1]);
        PairsOne += Abc_MinInt(Neg[0], Neg[1]) + Abc_MinInt(Pos[0], Pos[1]);
    }
    printf( "Total number of equiv classes                = %7d.\n", Vec_PtrSize(vRes) );
    printf( "Participating nodes from both networks       = %7d.\n", NegAll[0]+PosAll[0]+NegAll[1]+PosAll[1] );
    printf( "Participating nodes from the first network   = %7d. (%7.2f %% of nodes)\n", NegAll[0]+PosAll[0], 100.0*(NegAll[0]+PosAll[0])/(nNodes0+1) );
    printf( "Participating nodes from the second network  = %7d. (%7.2f %% of nodes)\n", NegAll[1]+PosAll[1], 100.0*(NegAll[1]+PosAll[1])/(nNodes1+1) );
    printf( "Node pairs (any polarity)                    = %7d. (%7.2f %% of names can be moved)\n", PairsAll, 100.0*PairsAll/(nNodes0+1) );
    printf( "Node pairs (same polarity)                   = %7d. (%7.2f %% of names can be moved)\n", PairsOne, 100.0*PairsOne/(nNodes0+1) );
    ABC_PRT( "Total runtime", Time );
}

Aig_Man_t* Abc_NtkToDar	(	Abc_Ntk_t *	pNtk,
		int	fExors,
		int	fRegisters
	)

DECLARATIONS ///.

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [Assumes that registers are ordered after PIs/POs.]

SideEffects []

SeeAlso []

Definition at line 233 of file abcDar.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Man_t * pMan;
    Aig_Obj_t * pObjNew;
    Abc_Obj_t * pObj;
    int i, nNodes, nDontCares;
    // make sure the latches follow PIs/POs
    if ( fRegisters ) 
    { 
        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
        Abc_NtkForEachCi( pNtk, pObj, i )
            if ( i < Abc_NtkPiNum(pNtk) )
            {
                assert( Abc_ObjIsPi(pObj) );
                if ( !Abc_ObjIsPi(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBo(pObj) );
        Abc_NtkForEachCo( pNtk, pObj, i )
            if ( i < Abc_NtkPoNum(pNtk) )
            {
                assert( Abc_ObjIsPo(pObj) );
                if ( !Abc_ObjIsPo(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBi(pObj) );
        // print warning about initial values
        nDontCares = 0;
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInitDc(pObj) )
            {
                Abc_LatchSetInit0(pObj);
                nDontCares++;
            }
        if ( nDontCares )
        {
            Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
            Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
            Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
            Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
        }
    }
    // create the manager
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
    pMan->fCatchExor = fExors;
    pMan->nConstrs = pNtk->nConstrs;
    pMan->nBarBufs = pNtk->nBarBufs;
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
        // initialize logic level of the CIs
        ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
    }
    // complement the 1-values registers
    if ( fRegisters ) {
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInit1(pObj) )
                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
    }
    // perform the conversion of the internal nodes (assumes DFS ordering)
//    pMan->fAddStrash = 1;
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
//    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
    }
    Vec_PtrFree( vNodes );
    pMan->fAddStrash = 0;
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
    // complement the 1-valued registers
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
    if ( fRegisters )
        Aig_ManForEachLiSeq( pMan, pObjNew, i )
            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
    // remove dangling nodes
    nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
    if ( !fExors && nNodes )
        Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
    // save the number of registers
    if ( fRegisters )
    {
        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
//        pMan->vFlopNums = NULL;
//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
        if ( pNtk->vOnehots )
            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
    }
    if ( !Aig_ManCheck( pMan ) )
    {
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}

Vec_Int_t* Abc_ObjDressClass	(	Vec_Ptr_t *	vRes,
		Vec_Int_t *	vClass2Num,
		int	Class
	)

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

Synopsis [Returns the vector of given equivalence class of objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file abcDress2.c.

{
    int ClassNumber;
    assert( Class > 0 );
    ClassNumber = Vec_IntEntry( vClass2Num, Class );
    assert( ClassNumber != 0 );
    if ( ClassNumber > 0 )
        return (Vec_Int_t *)Vec_PtrEntry( vRes, ClassNumber ); // previous class
    // create new class
    Vec_IntWriteEntry( vClass2Num, Class, Vec_PtrSize(vRes) );
    Vec_PtrPush( vRes, Vec_IntAlloc(4) );
    return (Vec_Int_t *)Vec_PtrEntryLast( vRes ); 
}

int Abc_ObjDressMakeId	(	Abc_Ntk_t *	pNtk,
		int	ObjId,
		int	iNtk
	)

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

Synopsis [Returns the ID of a node in an equivalence class.]

Description [The ID is composed of three parts: object ID, followed by one bit telling the phase of this node, followed by one bit telling the network to which this node belongs.]

SideEffects []

SeeAlso []

Definition at line 209 of file abcDress2.c.

{
    return (ObjId << 2) | (Abc_NtkObj(pNtk,ObjId)->fPhase << 1) | iNtk;
}

int Abc_ObjEquivId2NtkId

(

int

EquivId

)

Definition at line 58 of file abcDress2.c.

{ return  EquivId       & 1; }

int Abc_ObjEquivId2ObjId

(

int

EquivId

)

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

FileName [abcDressw.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Transfers names from one netlist to the other.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 56 of file abcDress2.c.

{ return  EquivId >> 2;      }

int Abc_ObjEquivId2Polar

(

int

EquivId

)

Definition at line 57 of file abcDress2.c.

{ return (EquivId >> 1) & 1; }

Aig_Man_t* Aig_ManCreateDualOutputMiter	(	Aig_Man_t *	p1,
		Aig_Man_t *	p2
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates the dual-output miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file abcDress2.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManCiNum(p1) == Aig_ManCiNum(p2) );
    assert( Aig_ManCoNum(p1) == Aig_ManCoNum(p2) );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
    // add first AIG
    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p1, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Aig_ManForEachNode( p1, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // add second AIG
    Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p2, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    Aig_ManForEachNode( p2, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // add the outputs
    for ( i = 0; i < Aig_ManCoNum(p1); i++ )
    {
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(Aig_ManCo(p1, i)) );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(Aig_ManCo(p2, i)) );
    }
    Aig_ManCleanup( pNew );
    return pNew;
}

void Dch_ComputeEquivalences	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 134 of file dchCore.c.

{
    Dch_Man_t * p;
    abctime clk, clkTotal = Abc_Clock();
    // reset random numbers
    Aig_ManRandom(1);
    // start the choicing manager
    p = Dch_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
clk = Abc_Clock(); 
    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = Abc_Clock() - clk;
//    Dch_ClassesPrint( p->ppClasses, 0 );
    p->nLits = Dch_ClassesLitNum( p->ppClasses );
    // perform SAT sweeping
    Dch_ManSweep( p );
    // free memory ahead of time
p->timeTotal = Abc_Clock() - clkTotal;
    Dch_ManStop( p );
}