abc/src/opt/sim/simSymStr.c - third_party/vtr-verilog-to-routing - Git at Google


            
            /**CFile****************************************************************


              FileName    [simSymStr.c]


              SystemName  [ABC: Logic synthesis and verification system.]


              PackageName [Network and node package.]


              Synopsis    [Structural detection of symmetries.]


              Author      [Alan Mishchenko]


              Affiliation [UC Berkeley]


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


              Revision    [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]


            ***********************************************************************/


            #include "base/abc/abc.h"

            
            #include "sim.h"


            ABC_NAMESPACE_IMPL_START


            ////////////////////////////////////////////////////////////////////////

            
            ///                        DECLARATIONS                              ///

            
            ////////////////////////////////////////////////////////////////////////


            #define SIM_READ_SYMMS(pNode)       ((Vec_Int_t *)pNode->pCopy)

            
            #define SIM_SET_SYMMS(pNode,vVect)  (pNode->pCopy = (Abc_Obj_t *)(vVect))


            static void  Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap );

            
            static void  Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );

            
            static void  Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther );

            
            static void  Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap );

            
            static void  Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap );

            
            static int   Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap );

            
            static int   Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );

            
            static void  Sim_SymmsPrint( Vec_Int_t * vSymms );

            
            static void  Sim_SymmsTrans( Vec_Int_t * vSymms );

            
            static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );

            
            static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );


            ////////////////////////////////////////////////////////////////////////

            
            ///                     FUNCTION DEFINITIONS                         ///

            
            ////////////////////////////////////////////////////////////////////////


            /**Function*************************************************************


              Synopsis    [Computes symmetries for a single output function.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )

            
            {

            
                Vec_Ptr_t * vNodes;

            
                Abc_Obj_t * pTemp;

            
                int * pMap, i;


                assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );


                // get the structural support

            
                pNtk->vSupps = Sim_ComputeStrSupp( pNtk );

            
                // set elementary info for the CIs

            
                Abc_NtkForEachCi( pNtk, pTemp, i )

            
                    SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );

            
                // create the map of CI ids into their numbers

            
                pMap = Sim_SymmsCreateMap( pNtk );

            
                // collect the nodes in the TFI cone of this output

            
                vNodes = Abc_NtkDfs( pNtk, 0 );

            
                Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )

            
                {

            
            //        if ( Abc_NodeIsConst(pTemp) )

            
            //            continue;

            
                    Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );

            
                }

            
                // collect the results for the COs;

            
                Abc_NtkForEachCo( pNtk, pTemp, i )

            
                {

            
            //printf( "Output %d:\n", i );

            
                    pTemp = Abc_ObjFanin0(pTemp);

            
                    if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )

            
                        continue;

            
                    Sim_SymmsTransferToMatrix( (Extra_BitMat_t *)Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), (unsigned *)Vec_PtrEntry(vSuppFun, i) );

            
                }

            
                // clean the intermediate results

            
                Sim_UtilInfoFree( pNtk->vSupps );

            
                pNtk->vSupps = NULL;

            
                Abc_NtkForEachCi( pNtk, pTemp, i )

            
                    Vec_IntFree( SIM_READ_SYMMS(pTemp) );

            
                Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )

            
            //        if ( !Abc_NodeIsConst(pTemp) )

            
                        Vec_IntFree( SIM_READ_SYMMS(pTemp) );

            
                Vec_PtrFree( vNodes );

            
                ABC_FREE( pMap );

            
            }


            /**Function*************************************************************


              Synopsis    [Recursively computes symmetries. ]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap )

            
            {

            
                Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther;

            
                Vec_Int_t * vSymms;

            
                Abc_Obj_t * pTemp;

            
                int i;


                // allocate the temporary arrays

            
                vNodes      = Vec_PtrAlloc( 10 );

            
                vNodesPi0   = Vec_PtrAlloc( 10 );

            
                vNodesPi1   = Vec_PtrAlloc( 10 );

            
                vNodesOther = Vec_PtrAlloc( 10 );


                // collect the fanins of the implication supergate

            
                Sim_SymmsBalanceCollect_rec( pNode, vNodes );


                // sort the nodes in the implication supergate

            
                Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther );


                // start the resulting set

            
                vSymms = Vec_IntAlloc( 10 );

            
                // generate symmetries from the groups

            
                Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap );

            
                Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap );

            
                // add symmetries from other inputs

            
                for ( i = 0; i < vNodesOther->nSize; i++ )

            
                {

            
                    pTemp = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);

            
                    Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap );

            
                }

            
                Vec_PtrFree( vNodes );

            
                Vec_PtrFree( vNodesPi0 );

            
                Vec_PtrFree( vNodesPi1 );

            
                Vec_PtrFree( vNodesOther );


                // set the symmetry at the node

            
                SIM_SET_SYMMS( pNode, vSymms );

            
            }


            /**Function*************************************************************


              Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )

            
            {

            
                // if the new node is complemented, another gate begins

            
                if ( Abc_ObjIsComplement(pNode) )

            
                {

            
                    Vec_PtrPushUnique( vNodes, pNode );

            
                    return;

            
                }

            
                // if pNew is the PI node, return

            
                if ( Abc_ObjIsCi(pNode) )

            
                {

            
                    Vec_PtrPushUnique( vNodes, pNode );

            
                    return;

            
                }

            
                // go through the branches

            
                Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes );

            
                Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes );

            
            }


            /**Function*************************************************************


              Synopsis    [Divides PI variables into groups.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0,

            
                Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther )

            
            {

            
                Abc_Obj_t * pNode;

            
                int i;

            
                Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )

            
                {

            
                    if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) )

            
                        Vec_PtrPush( vNodesOther, pNode );

            
                    else if ( Abc_ObjIsComplement(pNode) )

            
                        Vec_PtrPush( vNodesPis0, pNode );

            
                    else

            
                        Vec_PtrPush( vNodesPis1, pNode );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Makes the product of two partitions.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap )

            
            {

            
                Abc_Obj_t * pNode1, * pNode2;

            
                unsigned uSymm;

            
                int i, k;


                if ( vNodesPi->nSize == 0 )

            
                    return;


                // go through the pairs

            
                for ( i = 0; i < vNodesPi->nSize; i++ )

            
                for ( k = i+1; k < vNodesPi->nSize; k++ )

            
                {

            
                    // get the two PI nodes

            
                    pNode1 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);

            
                    pNode2 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[k]);

            
                    assert( pMap[pNode1->Id] != pMap[pNode2->Id] );

            
                    assert( pMap[pNode1->Id] >= 0 );

            
                    assert( pMap[pNode2->Id] >= 0 );

            
                    // generate symmetry

            
                    if ( pMap[pNode1->Id] < pMap[pNode2->Id] )

            
                        uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]);

            
                    else

            
                        uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]);

            
                    // check if symmetry belongs

            
                    if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) )

            
                        Vec_IntPushUnique( vSymms, (int)uSymm );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Add the filters symmetries from the nodes.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther,

            
                Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap )

            
            {

            
                unsigned uSymm;

            
                int i;


                if ( vSymms0->nSize == 0 )

            
                    return;


                // go through the pairs

            
                for ( i = 0; i < vSymms0->nSize; i++ )

            
                {

            
                    uSymm = (unsigned)vSymms0->pArray[i];

            
                    // check if symmetry belongs

            
                    if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) &&

            
                         Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) &&

            
                         Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) )

            
                        Vec_IntPushUnique( vSymms, (int)uSymm );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Returns 1 if symmetry is compatible with the group of nodes.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap )

            
            {

            
                Vec_Int_t * vSymmsNode;

            
                Abc_Obj_t * pNode;

            
                int i, s, Ind1, Ind2, fIsVar1, fIsVar2;


                if ( vNodesOther->nSize == 0 )

            
                    return 1;


                // get the indices of the PI variables

            
                Ind1 = (uSymm & 0xffff);

            
                Ind2 = (uSymm >> 16);


                // go through the nodes

            
                // if they do not belong to a support, it is okay

            
                // if one belongs, the other does not belong, quit

            
                // if they belong, but are not part of symmetry, quit

            
                for ( i = 0; i < vNodesOther->nSize; i++ )

            
                {

            
                    pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);

            
                    fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 );

            
                    fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 );


                    if ( !fIsVar1 && !fIsVar2 )

            
                        continue;

            
                    if ( fIsVar1 ^ fIsVar2 )

            
                        return 0;

            
                    // both belong

            
                    // check if there is a symmetry

            
                    vSymmsNode = SIM_READ_SYMMS( pNode );

            
                    for ( s = 0; s < vSymmsNode->nSize; s++ )

            
                        if ( uSymm == (unsigned)vSymmsNode->pArray[s] )

            
                            break;

            
                    if ( s == vSymmsNode->nSize )

            
                        return 0;

            
                }

            
                return 1;

            
            }


            /**Function*************************************************************


              Synopsis    [Returns 1 if symmetry is compatible with the group of PIs.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap )

            
            {

            
                Abc_Obj_t * pNode;

            
                int i, Ind1, Ind2, fHasVar1, fHasVar2;


                if ( vNodesPi->nSize == 0 )

            
                    return 1;


                // get the indices of the PI variables

            
                Ind1 = (uSymm & 0xffff);

            
                Ind2 = (uSymm >> 16);


                // go through the PI nodes

            
                fHasVar1 = fHasVar2 = 0;

            
                for ( i = 0; i < vNodesPi->nSize; i++ )

            
                {

            
                    pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);

            
                    if ( pMap[pNode->Id] == Ind1 )

            
                        fHasVar1 = 1;

            
                    else if ( pMap[pNode->Id] == Ind2 )

            
                        fHasVar2 = 1;

            
                }

            
                return fHasVar1 == fHasVar2;

            
            }


            /**Function*************************************************************


              Synopsis    [Improvements due to transitivity.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsTrans( Vec_Int_t * vSymms )

            
            {

            
                unsigned uSymm, uSymma, uSymmr;

            
                int i, Ind1, Ind2;

            
                int k, Ind1a, Ind2a;

            
                int j;

            
                int nTrans = 0;


                for ( i = 0; i < vSymms->nSize; i++ )

            
                {

            
                    uSymm = (unsigned)vSymms->pArray[i];

            
                    Ind1 = (uSymm & 0xffff);

            
                    Ind2 = (uSymm >> 16);

            
                    // find other symmetries that have Ind1

            
                    for ( k = i+1; k < vSymms->nSize; k++ )

            
                    {

            
                        uSymma = (unsigned)vSymms->pArray[k];

            
                        if ( uSymma == uSymm )

            
                            continue;

            
                        Ind1a = (uSymma & 0xffff);

            
                        Ind2a = (uSymma >> 16);

            
                        if ( Ind1a == Ind1 )

            
                        {

            
                            // find the symmetry (Ind2,Ind2a)

            
                            if ( Ind2 < Ind2a )

            
                                uSymmr = ((Ind2 << 16) | Ind2a);

            
                            else

            
                                uSymmr = ((Ind2a << 16) | Ind2);

            
                            for ( j = 0; j < vSymms->nSize; j++ )

            
                                if ( uSymmr == (unsigned)vSymms->pArray[j] )

            
                                    break;

            
                            if ( j == vSymms->nSize )

            
                                nTrans++;

            
                        }

            
                    }


                }

            
                printf( "Trans = %d.\n", nTrans );

            
            }


            /**Function*************************************************************


              Synopsis    [Transfers from the vector to the matrix.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )

            
            {

            
                int i, Ind1, Ind2, nInputs;

            
                unsigned uSymm;

            
                // add diagonal elements

            
                nInputs = Extra_BitMatrixReadSize( pMatSymm );

            
                for ( i = 0; i < nInputs; i++ )

            
                    Extra_BitMatrixInsert1( pMatSymm, i, i );

            
                // add non-diagonal elements

            
                for ( i = 0; i < vSymms->nSize; i++ )

            
                {

            
                    uSymm = (unsigned)vSymms->pArray[i];

            
                    Ind1 = (uSymm & 0xffff);

            
                    Ind2 = (uSymm >> 16);

            
            //printf( "%d,%d ", Ind1, Ind2 );

            
                    // skip variables that are not in the true support

            
                    assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );

            
                    if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )

            
                        continue;

            
                    Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );

            
                    Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Mapping of indices into numbers.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )

            
            {

            
                int * pMap;

            
                Abc_Obj_t * pNode;

            
                int i;

            
                pMap = ABC_ALLOC( int, Abc_NtkObjNumMax(pNtk) );

            
                for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )

            
                    pMap[i] = -1;

            
                Abc_NtkForEachCi( pNtk, pNode, i )

            
                    pMap[pNode->Id] = i;

            
                return pMap;

            
            }


            ////////////////////////////////////////////////////////////////////////

            
            ///                       END OF FILE                                ///

            
            ////////////////////////////////////////////////////////////////////////


            ABC_NAMESPACE_IMPL_END
	/CFile**************************************************************

	FileName [simSymStr.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Network and node package.]

	Synopsis [Structural detection of symmetries.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

	Revision [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

	***********************************************************************/

	#include "base/abc/abc.h"
	#include "sim.h"

	ABC_NAMESPACE_IMPL_START


	////////////////////////////////////////////////////////////////////////
	/// DECLARATIONS ///
	////////////////////////////////////////////////////////////////////////

	#define SIM_READ_SYMMS(pNode) ((Vec_Int_t *)pNode->pCopy)
	#define SIM_SET_SYMMS(pNode,vVect) (pNode->pCopy = (Abc_Obj_t *)(vVect))

	static void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap );
	static void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
	static void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther );
	static void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap );
	static void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap );
	static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap );
	static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
	static void Sim_SymmsPrint( Vec_Int_t * vSymms );
	static void Sim_SymmsTrans( Vec_Int_t * vSymms );
	static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
	static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );

	////////////////////////////////////////////////////////////////////////
	/// FUNCTION DEFINITIONS ///
	////////////////////////////////////////////////////////////////////////

	/Function***********************************************************

	Synopsis [Computes symmetries for a single output function.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
	{
	Vec_Ptr_t * vNodes;
	Abc_Obj_t * pTemp;
	int * pMap, i;

	assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );

	// get the structural support
	pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
	// set elementary info for the CIs
	Abc_NtkForEachCi( pNtk, pTemp, i )
	SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
	// create the map of CI ids into their numbers
	pMap = Sim_SymmsCreateMap( pNtk );
	// collect the nodes in the TFI cone of this output
	vNodes = Abc_NtkDfs( pNtk, 0 );
	Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
	{
	// if ( Abc_NodeIsConst(pTemp) )
	// continue;
	Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
	}
	// collect the results for the COs;
	Abc_NtkForEachCo( pNtk, pTemp, i )
	{
	//printf( "Output %d:\n", i );
	pTemp = Abc_ObjFanin0(pTemp);
	if ( Abc_ObjIsCi(pTemp) \|\| Abc_AigNodeIsConst(pTemp) )
	continue;
	Sim_SymmsTransferToMatrix( (Extra_BitMat_t )Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), (unsigned )Vec_PtrEntry(vSuppFun, i) );
	}
	// clean the intermediate results
	Sim_UtilInfoFree( pNtk->vSupps );
	pNtk->vSupps = NULL;
	Abc_NtkForEachCi( pNtk, pTemp, i )
	Vec_IntFree( SIM_READ_SYMMS(pTemp) );
	Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
	// if ( !Abc_NodeIsConst(pTemp) )
	Vec_IntFree( SIM_READ_SYMMS(pTemp) );
	Vec_PtrFree( vNodes );
	ABC_FREE( pMap );
	}

	/Function***********************************************************

	Synopsis [Recursively computes symmetries. ]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap )
	{
	Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther;
	Vec_Int_t * vSymms;
	Abc_Obj_t * pTemp;
	int i;

	// allocate the temporary arrays
	vNodes = Vec_PtrAlloc( 10 );
	vNodesPi0 = Vec_PtrAlloc( 10 );
	vNodesPi1 = Vec_PtrAlloc( 10 );
	vNodesOther = Vec_PtrAlloc( 10 );

	// collect the fanins of the implication supergate
	Sim_SymmsBalanceCollect_rec( pNode, vNodes );

	// sort the nodes in the implication supergate
	Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther );

	// start the resulting set
	vSymms = Vec_IntAlloc( 10 );
	// generate symmetries from the groups
	Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap );
	Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap );
	// add symmetries from other inputs
	for ( i = 0; i < vNodesOther->nSize; i++ )
	{
	pTemp = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);
	Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap );
	}
	Vec_PtrFree( vNodes );
	Vec_PtrFree( vNodesPi0 );
	Vec_PtrFree( vNodesPi1 );
	Vec_PtrFree( vNodesOther );

	// set the symmetry at the node
	SIM_SET_SYMMS( pNode, vSymms );
	}


	/Function***********************************************************

	Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
	{
	// if the new node is complemented, another gate begins
	if ( Abc_ObjIsComplement(pNode) )
	{
	Vec_PtrPushUnique( vNodes, pNode );
	return;
	}
	// if pNew is the PI node, return
	if ( Abc_ObjIsCi(pNode) )
	{
	Vec_PtrPushUnique( vNodes, pNode );
	return;
	}
	// go through the branches
	Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes );
	Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes );
	}

	/Function***********************************************************

	Synopsis [Divides PI variables into groups.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0,
	Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther )
	{
	Abc_Obj_t * pNode;
	int i;
	Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
	{
	if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) )
	Vec_PtrPush( vNodesOther, pNode );
	else if ( Abc_ObjIsComplement(pNode) )
	Vec_PtrPush( vNodesPis0, pNode );
	else
	Vec_PtrPush( vNodesPis1, pNode );
	}
	}

	/Function***********************************************************

	Synopsis [Makes the product of two partitions.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap )
	{
	Abc_Obj_t * pNode1, * pNode2;
	unsigned uSymm;
	int i, k;

	if ( vNodesPi->nSize == 0 )
	return;

	// go through the pairs
	for ( i = 0; i < vNodesPi->nSize; i++ )
	for ( k = i+1; k < vNodesPi->nSize; k++ )
	{
	// get the two PI nodes
	pNode1 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);
	pNode2 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[k]);
	assert( pMap[pNode1->Id] != pMap[pNode2->Id] );
	assert( pMap[pNode1->Id] >= 0 );
	assert( pMap[pNode2->Id] >= 0 );
	// generate symmetry
	if ( pMap[pNode1->Id] < pMap[pNode2->Id] )
	uSymm = ((pMap[pNode1->Id] << 16) \| pMap[pNode2->Id]);
	else
	uSymm = ((pMap[pNode2->Id] << 16) \| pMap[pNode1->Id]);
	// check if symmetry belongs
	if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) )
	Vec_IntPushUnique( vSymms, (int)uSymm );
	}
	}

	/Function***********************************************************

	Synopsis [Add the filters symmetries from the nodes.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther,
	Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap )
	{
	unsigned uSymm;
	int i;

	if ( vSymms0->nSize == 0 )
	return;

	// go through the pairs
	for ( i = 0; i < vSymms0->nSize; i++ )
	{
	uSymm = (unsigned)vSymms0->pArray[i];
	// check if symmetry belongs
	if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) &&
	Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) &&
	Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) )
	Vec_IntPushUnique( vSymms, (int)uSymm );
	}
	}

	/Function***********************************************************

	Synopsis [Returns 1 if symmetry is compatible with the group of nodes.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap )
	{
	Vec_Int_t * vSymmsNode;
	Abc_Obj_t * pNode;
	int i, s, Ind1, Ind2, fIsVar1, fIsVar2;

	if ( vNodesOther->nSize == 0 )
	return 1;

	// get the indices of the PI variables
	Ind1 = (uSymm & 0xffff);
	Ind2 = (uSymm >> 16);

	// go through the nodes
	// if they do not belong to a support, it is okay
	// if one belongs, the other does not belong, quit
	// if they belong, but are not part of symmetry, quit
	for ( i = 0; i < vNodesOther->nSize; i++ )
	{
	pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);
	fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 );
	fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 );

	if ( !fIsVar1 && !fIsVar2 )
	continue;
	if ( fIsVar1 ^ fIsVar2 )
	return 0;
	// both belong
	// check if there is a symmetry
	vSymmsNode = SIM_READ_SYMMS( pNode );
	for ( s = 0; s < vSymmsNode->nSize; s++ )
	if ( uSymm == (unsigned)vSymmsNode->pArray[s] )
	break;
	if ( s == vSymmsNode->nSize )
	return 0;
	}
	return 1;
	}

	/Function***********************************************************

	Synopsis [Returns 1 if symmetry is compatible with the group of PIs.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap )
	{
	Abc_Obj_t * pNode;
	int i, Ind1, Ind2, fHasVar1, fHasVar2;

	if ( vNodesPi->nSize == 0 )
	return 1;

	// get the indices of the PI variables
	Ind1 = (uSymm & 0xffff);
	Ind2 = (uSymm >> 16);

	// go through the PI nodes
	fHasVar1 = fHasVar2 = 0;
	for ( i = 0; i < vNodesPi->nSize; i++ )
	{
	pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);
	if ( pMap[pNode->Id] == Ind1 )
	fHasVar1 = 1;
	else if ( pMap[pNode->Id] == Ind2 )
	fHasVar2 = 1;
	}
	return fHasVar1 == fHasVar2;
	}



	/Function***********************************************************

	Synopsis [Improvements due to transitivity.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsTrans( Vec_Int_t * vSymms )
	{
	unsigned uSymm, uSymma, uSymmr;
	int i, Ind1, Ind2;
	int k, Ind1a, Ind2a;
	int j;
	int nTrans = 0;

	for ( i = 0; i < vSymms->nSize; i++ )
	{
	uSymm = (unsigned)vSymms->pArray[i];
	Ind1 = (uSymm & 0xffff);
	Ind2 = (uSymm >> 16);
	// find other symmetries that have Ind1
	for ( k = i+1; k < vSymms->nSize; k++ )
	{
	uSymma = (unsigned)vSymms->pArray[k];
	if ( uSymma == uSymm )
	continue;
	Ind1a = (uSymma & 0xffff);
	Ind2a = (uSymma >> 16);
	if ( Ind1a == Ind1 )
	{
	// find the symmetry (Ind2,Ind2a)
	if ( Ind2 < Ind2a )
	uSymmr = ((Ind2 << 16) \| Ind2a);
	else
	uSymmr = ((Ind2a << 16) \| Ind2);
	for ( j = 0; j < vSymms->nSize; j++ )
	if ( uSymmr == (unsigned)vSymms->pArray[j] )
	break;
	if ( j == vSymms->nSize )
	nTrans++;
	}
	}

	}
	printf( "Trans = %d.\n", nTrans );
	}


	/Function***********************************************************

	Synopsis [Transfers from the vector to the matrix.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
	{
	int i, Ind1, Ind2, nInputs;
	unsigned uSymm;
	// add diagonal elements
	nInputs = Extra_BitMatrixReadSize( pMatSymm );
	for ( i = 0; i < nInputs; i++ )
	Extra_BitMatrixInsert1( pMatSymm, i, i );
	// add non-diagonal elements
	for ( i = 0; i < vSymms->nSize; i++ )
	{
	uSymm = (unsigned)vSymms->pArray[i];
	Ind1 = (uSymm & 0xffff);
	Ind2 = (uSymm >> 16);
	//printf( "%d,%d ", Ind1, Ind2 );
	// skip variables that are not in the true support
	assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
	if ( !Sim_HasBit(pSupport, Ind1) \|\| !Sim_HasBit(pSupport, Ind2) )
	continue;
	Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
	Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
	}
	}

	/Function***********************************************************

	Synopsis [Mapping of indices into numbers.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )
	{
	int * pMap;
	Abc_Obj_t * pNode;
	int i;
	pMap = ABC_ALLOC( int, Abc_NtkObjNumMax(pNtk) );
	for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
	pMap[i] = -1;
	Abc_NtkForEachCi( pNtk, pNode, i )
	pMap[pNode->Id] = i;
	return pMap;
	}



	////////////////////////////////////////////////////////////////////////
	/// END OF FILE ///
	////////////////////////////////////////////////////////////////////////


	ABC_NAMESPACE_IMPL_END