abc/src/proof/cec/cecChoice.c - third_party/vtr-verilog-to-routing - Git at Google


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


              FileName    [cecChoice.c]


              SystemName  [ABC: Logic synthesis and verification system.]


              PackageName [Combinational equivalence checking.]


              Synopsis    [Computation of structural choices.]


              Author      [Alan Mishchenko]


              Affiliation [UC Berkeley]


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


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


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


            #include "cecInt.h"

            
            #include "aig/gia/giaAig.h"

            
            #include "proof/dch/dch.h"


            ABC_NAMESPACE_IMPL_START


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

            
            ///                        DECLARATIONS                              ///

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


            static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );


            extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );

            
            extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );


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

            
            ///                     FUNCTION DEFINITIONS                         ///

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


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


              Synopsis    [Computes the real value of the literal w/o spec reduction.]


              Description []


              SideEffects []


              SeeAlso     []


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

            
            static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )

            
            {

            
                assert( Gia_ObjIsAnd(pObj) );

            
                Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );

            
                Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );

            
                return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );

            
            }


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


              Synopsis    [Recursively performs speculative reduction for the object.]


              Description []


              SideEffects []


              SeeAlso     []


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

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

            
            {

            
                Gia_Obj_t * pRepr;

            
                if ( ~pObj->Value )

            
                    return;

            
                if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )

            
                {

            
                    Cec_ManCombSpecReduce_rec( pNew, p, pRepr );

            
                    pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );

            
                    return;

            
                }

            
                pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );

            
            }


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


              Synopsis    [Derives SRM for signal correspondence.]


              Description []


              SideEffects []


              SeeAlso     []


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

            
            Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )

            
            {

            
                Gia_Man_t * pNew, * pTemp;

            
                Gia_Obj_t * pObj, * pRepr;

            
                Vec_Int_t * vXorLits;

            
                int i, iPrev, iObj, iPrevNew, iObjNew;

            
                assert( p->pReprs != NULL );

            
                Gia_ManSetPhase( p );

            
                Gia_ManFillValue( p );

            
                pNew = Gia_ManStart( Gia_ManObjNum(p) );

            
                pNew->pName = Abc_UtilStrsav( p->pName );

            
                pNew->pSpec = Abc_UtilStrsav( p->pSpec );

            
                Gia_ManHashAlloc( pNew );

            
                Gia_ManConst0(p)->Value = 0;

            
                Gia_ManForEachCi( p, pObj, i )

            
                    pObj->Value = Gia_ManAppendCi(pNew);

            
                *pvOutputs = Vec_IntAlloc( 1000 );

            
                vXorLits = Vec_IntAlloc( 1000 );

            
                if ( fRings )

            
                {

            
                    Gia_ManForEachObj1( p, pObj, i )

            
                    {

            
                        if ( Gia_ObjIsConst( p, i ) )

            
                        {

            
                            iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );

            
                            iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );

            
                            if ( iObjNew != 0 )

            
                            {

            
                                Vec_IntPush( *pvOutputs, 0 );

            
                                Vec_IntPush( *pvOutputs, i );

            
                                Vec_IntPush( vXorLits, iObjNew );

            
                            }

            
                        }

            
                        else if ( Gia_ObjIsHead( p, i ) )

            
                        {

            
                            iPrev = i;

            
                            Gia_ClassForEachObj1( p, i, iObj )

            
                            {

            
                                iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );

            
                                iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );

            
                                iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );

            
                                iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );

            
                                if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )

            
                                {

            
                                    Vec_IntPush( *pvOutputs, iPrev );

            
                                    Vec_IntPush( *pvOutputs, iObj );

            
                                    Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );

            
                                }

            
                                iPrev = iObj;

            
                            }

            
                            iObj = i;

            
                            iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );

            
                            iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );

            
                            iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );

            
                            iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );

            
                            if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )

            
                            {

            
                                Vec_IntPush( *pvOutputs, iPrev );

            
                                Vec_IntPush( *pvOutputs, iObj );

            
                                Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );

            
                            }

            
                        }

            
                    }

            
                }

            
                else

            
                {

            
                    Gia_ManForEachObj1( p, pObj, i )

            
                    {

            
                        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );

            
                        if ( pRepr == NULL )

            
                            continue;

            
                        iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );

            
                        iObjNew  = Cec_ManCombSpecReal( pNew, p, pObj );

            
                        iObjNew  = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );

            
                        if ( iPrevNew != iObjNew )

            
                        {

            
                            Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );

            
                            Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );

            
                            Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );

            
                        }

            
                    }

            
                }

            
                Vec_IntForEachEntry( vXorLits, iObjNew, i )

            
                    Gia_ManAppendCo( pNew, iObjNew );

            
                Vec_IntFree( vXorLits );

            
                Gia_ManHashStop( pNew );

            
            //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );

            
                pNew = Gia_ManCleanup( pTemp = pNew );

            
            //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );

            
                Gia_ManStop( pTemp );

            
                return pNew;

            
            }


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )

            
            {

            
                int nItersMax = 1000;

            
                Vec_Str_t * vStatus;

            
                Vec_Int_t * vOutputs;

            
                Vec_Int_t * vCexStore;

            
                Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;

            
                Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;

            
                Cec_ManSim_t * pSim;

            
                Gia_Man_t * pSrm;

            
                int r, RetValue;

            
                abctime clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = Abc_Clock();

            
                abctime clk2, clk = Abc_Clock();

            
                ABC_FREE( pAig->pReprs );

            
                ABC_FREE( pAig->pNexts );

            
                Gia_ManRandom( 1 );

            
                // prepare simulation manager

            
                Cec_ManSimSetDefaultParams( pParsSim );

            
                pParsSim->nWords     = pPars->nWords;

            
                pParsSim->nFrames    = pPars->nRounds;

            
                pParsSim->fVerbose   = pPars->fVerbose;

            
                pParsSim->fLatchCorr   = 0;

            
                pParsSim->fSeqSimulate = 0;

            
                // create equivalence classes of registers

            
                pSim = Cec_ManSimStart( pAig, pParsSim );

            
                Cec_ManSimClassesPrepare( pSim, -1 );

            
                Cec_ManSimClassesRefine( pSim );

            
                // prepare SAT solving

            
                Cec_ManSatSetDefaultParams( pParsSat );

            
                pParsSat->nBTLimit = pPars->nBTLimit;

            
                pParsSat->fVerbose = pPars->fVerbose;

            
                if ( pPars->fVerbose )

            
                {

            
                    Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",

            
                        Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );

            
                    Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );

            
                }

            
                // perform refinement of equivalence classes

            
                for ( r = 0; r < nItersMax; r++ )

            
                {

            
                    clk = Abc_Clock();

            
                    // perform speculative reduction

            
                    clk2 = Abc_Clock();

            
                    pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );

            
                    assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );

            
                    clkSrm += Abc_Clock() - clk2;

            
                    if ( Gia_ManCoNum(pSrm) == 0 )

            
                    {

            
                        if ( pPars->fVerbose )

            
                            Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );

            
                        Vec_IntFree( vOutputs );

            
                        Gia_ManStop( pSrm );

            
                        break;

            
                    }

            
            //Gia_DumpAiger( pSrm, "choicesrm", r, 2 );

            
                    // found counter-examples to speculation

            
                    clk2 = Abc_Clock();

            
                    if ( pPars->fUseCSat )

            
                        vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );

            
                    else

            
                        vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );

            
                    Gia_ManStop( pSrm );

            
                    clkSat += Abc_Clock() - clk2;

            
                    if ( Vec_IntSize(vCexStore) == 0 )

            
                    {

            
                        if ( pPars->fVerbose )

            
                            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );

            
                        Vec_IntFree( vCexStore );

            
                        Vec_StrFree( vStatus );

            
                        Vec_IntFree( vOutputs );

            
                        break;

            
                    }

            
                    // refine classes with these counter-examples

            
                    clk2 = Abc_Clock();

            
                    RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );

            
                    Vec_IntFree( vCexStore );

            
                    clkSim += Abc_Clock() - clk2;

            
                    Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );

            
                    if ( pPars->fVerbose )

            
                        Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );

            
                    Vec_StrFree( vStatus );

            
                    Vec_IntFree( vOutputs );

            
            //Gia_ManEquivPrintClasses( pAig, 1, 0 );

            
                }

            
                // check the overflow

            
                if ( r == nItersMax )

            
                    Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );

            
                Cec_ManSimStop( pSim );

            
                clkTotal = Abc_Clock() - clkTotal;

            
                // report the results

            
                if ( pPars->fVerbose )

            
                {

            
                    Abc_PrintTimeP( 1, "Srm  ", clkSrm,                        clkTotal );

            
                    Abc_PrintTimeP( 1, "Sat  ", clkSat,                        clkTotal );

            
                    Abc_PrintTimeP( 1, "Sim  ", clkSim,                        clkTotal );

            
                    Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );

            
                    Abc_PrintTime( 1, "TOTAL",  clkTotal );

            
                }

            
                return 0;

            
            }


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


              Synopsis    [Computes choices for the vector of AIGs.]


              Description []


              SideEffects []


              SeeAlso     []


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

            
            Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )

            
            {

            
                Gia_Man_t * pNew;

            
                int RetValue;

            
                // compute equivalences of the miter

            
            //    pMiter = Gia_ManChoiceMiter( vGias );

            
            //    Gia_ManSetRegNum( pMiter, 0 );

            
                RetValue = Cec_ManChoiceComputation_int( pGia, pPars );

            
                // derive AIG with choices

            
                pNew = Gia_ManEquivToChoices( pGia, nGias );

            
            //    Gia_ManHasChoices_very_old( pNew );

            
            //    Gia_ManStop( pMiter );

            
                // report the results

            
                if ( pPars->fVerbose )

            
                {

            
            //        Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",

            
            //            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),

            
            //            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),

            
            //            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),

            
            //            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );

            
                }

            
                return pNew;

            
            }


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


              Synopsis    [Computes choices for one AIGs.]


              Description []


              SideEffects []


              SeeAlso     []


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

            
            Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )

            
            {

            
            //    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );

            
                Dch_Pars_t Pars, * pPars = &Pars;

            
                Aig_Man_t * pMan, * pManNew;

            
                Gia_Man_t * pGia;

            
                if ( 0 )

            
                {

            
                    pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );

            
                }

            
                else

            
                {

            
                    pMan = Gia_ManToAig( pAig, 0 );

            
                    Dch_ManSetDefaultParams( pPars );

            
                    pPars->fUseGia  = 1;

            
                    pPars->nBTLimit = pParsChc->nBTLimit;

            
                    pPars->fUseCSat = pParsChc->fUseCSat;

            
                    pPars->fVerbose = pParsChc->fVerbose;

            
                    pManNew = Dar_ManChoiceNew( pMan, pPars );

            
                    pGia = Gia_ManFromAig( pManNew );

            
                    Aig_ManStop( pManNew );

            
            //        Aig_ManStop( pMan );

            
                }

            
                return pGia;

            
            }


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


              Synopsis    [Performs computation of AIGs with choices.]


              Description [Takes several AIGs and performs choicing.]


              SideEffects []


              SeeAlso     []


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

            
            Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )

            
            {

            
                Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;

            
                Aig_Man_t * pAig;

            
                if ( pPars->fVerbose )

            
                    Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );

            
                Cec_ManChcSetDefaultParams( pParsChc );

            
                pParsChc->nBTLimit = pPars->nBTLimit;

            
                pParsChc->fUseCSat = pPars->fUseCSat;

            
                if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )

            
                    pParsChc->nBTLimit = 100;

            
                pParsChc->fVerbose = pPars->fVerbose;

            
                pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );

            
                Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );

            
                pAig = Gia_ManToAig( pGia, 1 );

            
                Gia_ManStop( pGia );

            
                return pAig;

            
            }


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

            
            ///                       END OF FILE                                ///

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


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

	FileName [cecChoice.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Combinational equivalence checking.]

	Synopsis [Computation of structural choices.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

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

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

	#include "cecInt.h"
	#include "aig/gia/giaAig.h"
	#include "proof/dch/dch.h"

	ABC_NAMESPACE_IMPL_START


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

	static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );

	extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
	extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );

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

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

	Synopsis [Computes the real value of the literal w/o spec reduction.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	assert( Gia_ObjIsAnd(pObj) );
	Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
	Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
	return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
	}

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

	Synopsis [Recursively performs speculative reduction for the object.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	Gia_Obj_t * pRepr;
	if ( ~pObj->Value )
	return;
	if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
	{
	Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
	pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
	return;
	}
	pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
	}

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

	Synopsis [Derives SRM for signal correspondence.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
	{
	Gia_Man_t * pNew, * pTemp;
	Gia_Obj_t * pObj, * pRepr;
	Vec_Int_t * vXorLits;
	int i, iPrev, iObj, iPrevNew, iObjNew;
	assert( p->pReprs != NULL );
	Gia_ManSetPhase( p );
	Gia_ManFillValue( p );
	pNew = Gia_ManStart( Gia_ManObjNum(p) );
	pNew->pName = Abc_UtilStrsav( p->pName );
	pNew->pSpec = Abc_UtilStrsav( p->pSpec );
	Gia_ManHashAlloc( pNew );
	Gia_ManConst0(p)->Value = 0;
	Gia_ManForEachCi( p, pObj, i )
	pObj->Value = Gia_ManAppendCi(pNew);
	*pvOutputs = Vec_IntAlloc( 1000 );
	vXorLits = Vec_IntAlloc( 1000 );
	if ( fRings )
	{
	Gia_ManForEachObj1( p, pObj, i )
	{
	if ( Gia_ObjIsConst( p, i ) )
	{
	iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
	iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
	if ( iObjNew != 0 )
	{
	Vec_IntPush( *pvOutputs, 0 );
	Vec_IntPush( *pvOutputs, i );
	Vec_IntPush( vXorLits, iObjNew );
	}
	}
	else if ( Gia_ObjIsHead( p, i ) )
	{
	iPrev = i;
	Gia_ClassForEachObj1( p, i, iObj )
	{
	iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
	iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
	iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
	iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
	if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
	{
	Vec_IntPush( *pvOutputs, iPrev );
	Vec_IntPush( *pvOutputs, iObj );
	Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
	}
	iPrev = iObj;
	}
	iObj = i;
	iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
	iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
	iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
	iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
	if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
	{
	Vec_IntPush( *pvOutputs, iPrev );
	Vec_IntPush( *pvOutputs, iObj );
	Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
	}
	}
	}
	}
	else
	{
	Gia_ManForEachObj1( p, pObj, i )
	{
	pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
	if ( pRepr == NULL )
	continue;
	iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
	iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
	iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
	if ( iPrevNew != iObjNew )
	{
	Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
	Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
	Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
	}
	}
	}
	Vec_IntForEachEntry( vXorLits, iObjNew, i )
	Gia_ManAppendCo( pNew, iObjNew );
	Vec_IntFree( vXorLits );
	Gia_ManHashStop( pNew );
	//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
	pNew = Gia_ManCleanup( pTemp = pNew );
	//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
	Gia_ManStop( pTemp );
	return pNew;
	}


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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
	{
	int nItersMax = 1000;
	Vec_Str_t * vStatus;
	Vec_Int_t * vOutputs;
	Vec_Int_t * vCexStore;
	Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
	Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
	Cec_ManSim_t * pSim;
	Gia_Man_t * pSrm;
	int r, RetValue;
	abctime clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = Abc_Clock();
	abctime clk2, clk = Abc_Clock();
	ABC_FREE( pAig->pReprs );
	ABC_FREE( pAig->pNexts );
	Gia_ManRandom( 1 );
	// prepare simulation manager
	Cec_ManSimSetDefaultParams( pParsSim );
	pParsSim->nWords = pPars->nWords;
	pParsSim->nFrames = pPars->nRounds;
	pParsSim->fVerbose = pPars->fVerbose;
	pParsSim->fLatchCorr = 0;
	pParsSim->fSeqSimulate = 0;
	// create equivalence classes of registers
	pSim = Cec_ManSimStart( pAig, pParsSim );
	Cec_ManSimClassesPrepare( pSim, -1 );
	Cec_ManSimClassesRefine( pSim );
	// prepare SAT solving
	Cec_ManSatSetDefaultParams( pParsSat );
	pParsSat->nBTLimit = pPars->nBTLimit;
	pParsSat->fVerbose = pPars->fVerbose;
	if ( pPars->fVerbose )
	{
	Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
	Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
	Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
	}
	// perform refinement of equivalence classes
	for ( r = 0; r < nItersMax; r++ )
	{
	clk = Abc_Clock();
	// perform speculative reduction
	clk2 = Abc_Clock();
	pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
	assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
	clkSrm += Abc_Clock() - clk2;
	if ( Gia_ManCoNum(pSrm) == 0 )
	{
	if ( pPars->fVerbose )
	Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
	Vec_IntFree( vOutputs );
	Gia_ManStop( pSrm );
	break;
	}
	//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
	// found counter-examples to speculation
	clk2 = Abc_Clock();
	if ( pPars->fUseCSat )
	vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
	else
	vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
	Gia_ManStop( pSrm );
	clkSat += Abc_Clock() - clk2;
	if ( Vec_IntSize(vCexStore) == 0 )
	{
	if ( pPars->fVerbose )
	Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
	Vec_IntFree( vCexStore );
	Vec_StrFree( vStatus );
	Vec_IntFree( vOutputs );
	break;
	}
	// refine classes with these counter-examples
	clk2 = Abc_Clock();
	RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
	Vec_IntFree( vCexStore );
	clkSim += Abc_Clock() - clk2;
	Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
	if ( pPars->fVerbose )
	Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
	Vec_StrFree( vStatus );
	Vec_IntFree( vOutputs );
	//Gia_ManEquivPrintClasses( pAig, 1, 0 );
	}
	// check the overflow
	if ( r == nItersMax )
	Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
	Cec_ManSimStop( pSim );
	clkTotal = Abc_Clock() - clkTotal;
	// report the results
	if ( pPars->fVerbose )
	{
	Abc_PrintTimeP( 1, "Srm ", clkSrm, clkTotal );
	Abc_PrintTimeP( 1, "Sat ", clkSat, clkTotal );
	Abc_PrintTimeP( 1, "Sim ", clkSim, clkTotal );
	Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
	Abc_PrintTime( 1, "TOTAL", clkTotal );
	}
	return 0;
	}

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

	Synopsis [Computes choices for the vector of AIGs.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
	{
	Gia_Man_t * pNew;
	int RetValue;
	// compute equivalences of the miter
	// pMiter = Gia_ManChoiceMiter( vGias );
	// Gia_ManSetRegNum( pMiter, 0 );
	RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
	// derive AIG with choices
	pNew = Gia_ManEquivToChoices( pGia, nGias );
	// Gia_ManHasChoices_very_old( pNew );
	// Gia_ManStop( pMiter );
	// report the results
	if ( pPars->fVerbose )
	{
	// Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
	// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
	// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
	// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
	// 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
	}
	return pNew;
	}

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

	Synopsis [Computes choices for one AIGs.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
	{
	// extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
	Dch_Pars_t Pars, * pPars = &Pars;
	Aig_Man_t * pMan, * pManNew;
	Gia_Man_t * pGia;
	if ( 0 )
	{
	pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
	}
	else
	{
	pMan = Gia_ManToAig( pAig, 0 );
	Dch_ManSetDefaultParams( pPars );
	pPars->fUseGia = 1;
	pPars->nBTLimit = pParsChc->nBTLimit;
	pPars->fUseCSat = pParsChc->fUseCSat;
	pPars->fVerbose = pParsChc->fVerbose;
	pManNew = Dar_ManChoiceNew( pMan, pPars );
	pGia = Gia_ManFromAig( pManNew );
	Aig_ManStop( pManNew );
	// Aig_ManStop( pMan );
	}
	return pGia;
	}

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

	Synopsis [Performs computation of AIGs with choices.]

	Description [Takes several AIGs and performs choicing.]

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
	{
	Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
	Aig_Man_t * pAig;
	if ( pPars->fVerbose )
	Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );
	Cec_ManChcSetDefaultParams( pParsChc );
	pParsChc->nBTLimit = pPars->nBTLimit;
	pParsChc->fUseCSat = pPars->fUseCSat;
	if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
	pParsChc->nBTLimit = 100;
	pParsChc->fVerbose = pPars->fVerbose;
	pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
	Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
	pAig = Gia_ManToAig( pGia, 1 );
	Gia_ManStop( pGia );
	return pAig;
	}

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


	ABC_NAMESPACE_IMPL_END