abc/src/proof/abs/absOldRef.c - third_party/vtr-verilog-to-routing - Git at Google

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

   FileName    [saigAbsStart.c]

   SystemName  [ABC: Logic synthesis and verification system.]

   PackageName [Sequential AIG package.]

   Synopsis    [Counter-example-based abstraction.]

   Author      [Alan Mishchenko]

   Affiliation [UC Berkeley]

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

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

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

 #include "abs.h"
 #include "proof/ssw/ssw.h"
 #include "proof/fra/fra.h"
 #include "bdd/bbr/bbr.h"
 #include "proof/pdr/pdr.h"
 #include "sat/bmc/bmc.h"

 ABC_NAMESPACE_IMPL_START


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

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

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

   Synopsis    [This procedure sets default parameters.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p )
 {
     memset( p, 0, sizeof(Gia_ParAbs_t) );
     p->Algo        =        0;    // algorithm: CBA
     p->nFramesMax  =       10;    // timeframes for PBA
     p->nConfMax    =    10000;    // conflicts for PBA
     p->fDynamic    =        1;    // dynamic unfolding for PBA
     p->fConstr     =        0;    // use constraints
     p->nFramesBmc  =      250;    // timeframes for BMC
     p->nConfMaxBmc =     5000;    // conflicts for BMC
     p->nStableMax  =  1000000;    // the number of stable frames to quit
     p->nRatio      =       10;    // ratio of flops to quit
     p->nBobPar     =  1000000;    // the number of frames before trying to quit
     p->fUseBdds    =        0;    // use BDDs to refine abstraction
     p->fUseDprove  =        0;    // use 'dprove' to refine abstraction
     p->fUseStart   =        1;    // use starting frame
     p->fVerbose    =        0;    // verbose output
     p->fVeryVerbose=        0;    // printing additional information
     p->Status      =       -1;    // the problem status
     p->nFramesDone =       -1;    // the number of rames covered
 }


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

   Synopsis    [Derive a new counter-example.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
 {
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     int i, f;
     if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
         printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
 //    else
 //        printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
     // start the counter-example
     pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
     pCex->iFrame = pCexAbs->iFrame;
     pCex->iPo    = pCexAbs->iPo;
     // copy the bit data
     for ( f = 0; f <= pCexAbs->iFrame; f++ )
     {
         Saig_ManForEachPi( pAbs, pObj, i )
         {
             if ( i == Saig_ManPiNum(p) )
                 break;
             if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
                 Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
         }
     }
     // verify the counter example
     if ( !Saig_ManVerifyCex( p, pCex ) )
     {
         printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
         Abc_CexFree( pCex );
         pCex = NULL;
     }
     else
     {
         Abc_Print( 1, "Counter-example verification is successful.\n" );
         Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
     }
     return pCex;
 }

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

   Synopsis    [Find the first PI corresponding to the flop.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
 {
     Aig_Obj_t * pObj;
     int i;
     assert( pAbs->vCiNumsOrig != NULL );
     Aig_ManForEachCi( p, pObj, i )
     {
         if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) )
             return i;
     }
     return -1;
 }

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

   Synopsis    [Refines abstraction using one step.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
 {
     Vec_Int_t * vFlopsNew;
     int i, Entry, RetValue;
     *piRetValue = -1;
     if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
     {
 /*
         Fra_Sec_t SecPar, * pSecPar = &SecPar;
         Fra_SecSetDefaultParams( pSecPar );
         pSecPar->fVerbose       = fVerbose;
         RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
 */
         Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
         Pdr_Par_t Pars, * pPars = &Pars;
         Pdr_ManSetDefaultParams( pPars );
         pPars->nTimeOut = 10;
         pPars->fVerbose = fVerbose;
         if ( pPars->fVerbose )
             printf( "Running property directed reachability...\n" );
         RetValue = Pdr_ManSolve( pAbsOrpos, pPars );
         if ( pAbsOrpos->pSeqModel )
             pAbsOrpos->pSeqModel->iPo = Saig_ManFindFailedPoCex( pAbs, pAbsOrpos->pSeqModel );
         pAbs->pSeqModel = pAbsOrpos->pSeqModel;
         pAbsOrpos->pSeqModel = NULL;
         Aig_ManStop( pAbsOrpos );
         if ( RetValue )
             *piRetValue = 1;

     }
     else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
     {
         Saig_ParBbr_t Pars, * pPars = &Pars;
         Bbr_ManSetDefaultParams( pPars );
         pPars->TimeLimit     = 0;
         pPars->nBddMax       = 1000000;
         pPars->nIterMax      = nFrames;
         pPars->fPartition    = 1;
         pPars->fReorder      = 1;
         pPars->fReorderImage = 1;
         pPars->fVerbose      = fVerbose;
         pPars->fSilent       = 0;
         RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
         if ( RetValue )
             *piRetValue = 1;
     }
     else
     {
         Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0, 0 );
     }
     if ( pAbs->pSeqModel == NULL )
         return NULL;
     if ( pnUseStart )
         *pnUseStart = pAbs->pSeqModel->iFrame;
 //    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
     vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
     if ( vFlopsNew == NULL )
         return NULL;
     if ( Vec_IntSize(vFlopsNew) == 0 )
     {
         printf( "Discovered a true counter-example!\n" );
         p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel );
         Vec_IntFree( vFlopsNew );
         *piRetValue = 0;
         return NULL;
     }
     // vFlopsNew contains PI numbers that should be kept in pAbs
     if ( fVerbose )
         printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) );
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {
         Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
         assert( Entry >= Saig_ManPiNum(p) );
         assert( Entry < Aig_ManCiNum(p) );
         Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
     }
     Vec_IntFree( vFlopsNew );

     Vec_IntSort( vFlops, 0 );
     Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
         assert( Vec_IntEntry(vFlops, i-1) != Entry );

     return Saig_ManDupAbstraction( p, vFlops );
 }

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

   Synopsis    [Refines abstraction using one step.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
 {
     Aig_Man_t * pAbs;
     Vec_Int_t * vFlopsNew;
     int i, Entry;
     abctime clk = Abc_Clock();
     pAbs = Saig_ManDupAbstraction( p, vFlops );
     if ( fSensePath )
         vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     else
 //        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
         vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     if ( vFlopsNew == NULL )
     {
         Aig_ManStop( pAbs );
         return 0;
     }
     if ( Vec_IntSize(vFlopsNew) == 0 )
     {
         printf( "Refinement did not happen. Discovered a true counter-example.\n" );
         printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAbs), Aig_ManCiNum(p) );
         p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex );
         Vec_IntFree( vFlopsNew );
         Aig_ManStop( pAbs );
         return 0;
     }
     if ( fVerbose )
     {
         printf( "Adding %d registers to the abstraction (total = %d).  ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
     // vFlopsNew contains PI numbers that should be kept in pAbs
     // select the most useful flops among those to be added
     if ( nFfToAddMax > 0 && Vec_IntSize(vFlopsNew) > nFfToAddMax )
     {
         Vec_Int_t * vFlopsNewBest;
         // shift the indices
         Vec_IntForEachEntry( vFlopsNew, Entry, i )
             Vec_IntAddToEntry( vFlopsNew, i, -Saig_ManPiNum(p) );
         // create new flops
         vFlopsNewBest = Saig_ManCbaFilterFlops( p, pCex, vFlopClasses, vFlopsNew, nFfToAddMax );
         assert( Vec_IntSize(vFlopsNewBest) == nFfToAddMax );
         printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vFlopsNew), Vec_IntSize(vFlopsNewBest) );
         // update
         Vec_IntFree( vFlopsNew );
         vFlopsNew = vFlopsNewBest;
         // shift the indices
         Vec_IntForEachEntry( vFlopsNew, Entry, i )
             Vec_IntAddToEntry( vFlopsNew, i, Saig_ManPiNum(p) );
     }
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {
         Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
         assert( Entry >= Saig_ManPiNum(p) );
         assert( Entry < Aig_ManCiNum(p) );
         Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
     }
     Vec_IntFree( vFlopsNew );
     Aig_ManStop( pAbs );
     return 1;
 }

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

   Synopsis    [Transform flop map into flop list.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
 {
     Vec_Int_t * vFlops;
     int i, Entry;
     vFlops = Vec_IntAlloc( 100 );
     Vec_IntForEachEntry( vFlopClasses, Entry, i )
         if ( Entry )
             Vec_IntPush( vFlops, i );
     return vFlops;
 }

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

   Synopsis    [Transform flop list into flop map.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops )
 {
     Vec_Int_t * vFlopClasses;
     int i, Entry;
     vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
     Vec_IntForEachEntry( vFlops, Entry, i )
         Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
     return vFlopClasses;
 }

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

   Synopsis    [Refines abstraction using the latch map.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
 {
     Aig_Man_t * pNew;
     Vec_Int_t * vFlops;
     if ( pGia->vFlopClasses == NULL )
     {
         printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" );
         return -1;
     }
     pNew = Gia_ManToAig( pGia, 0 );
     vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
     if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
     {
         pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
         Vec_IntFree( vFlops );
         Aig_ManStop( pNew );
         return 0;
     }
     Vec_IntFree( pGia->vFlopClasses );
     pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
     Vec_IntFree( vFlops );
     Aig_ManStop( pNew );
     return -1;
 }


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

   Synopsis    [Computes the flops to remain after abstraction.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
 {
     int nUseStart = 0;
     Aig_Man_t * pAbs, * pTemp;
     Vec_Int_t * vFlops;
     int Iter;//, clk = Abc_Clock(), clk2 = Abc_Clock();//, iFlop;
     assert( Aig_ManRegNum(p) > 0 );
     if ( pPars->fVerbose )
         printf( "Performing counter-example-based refinement.\n" );
     Aig_ManSetCioIds( p );
     vFlops = Vec_IntStartNatural( 1 );
 /*
     iFlop = Saig_ManFindFirstFlop( p );
     assert( iFlop >= 0 );
     vFlops = Vec_IntAlloc( 1 );
     Vec_IntPush( vFlops, iFlop );
 */
     // create the resulting AIG
     pAbs = Saig_ManDupAbstraction( p, vFlops );
     if ( !pPars->fVerbose )
     {
         printf( "Init : " );
         Aig_ManPrintStats( pAbs );
     }
     printf( "Refining abstraction...\n" );
     for ( Iter = 0; ; Iter++ )
     {
         pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
         if ( pTemp == NULL )
         {
             ABC_FREE( p->pSeqModel );
             p->pSeqModel = pAbs->pSeqModel;
             pAbs->pSeqModel = NULL;
             Aig_ManStop( pAbs );
             break;
         }
         Aig_ManStop( pAbs );
         pAbs = pTemp;
         printf( "ITER %4d : ", Iter );
         if ( !pPars->fVerbose )
             Aig_ManPrintStats( pAbs );
         // output the intermediate result of abstraction
         Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
 //            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
         // check if the ratio is reached
         if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
         {
             printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
             Aig_ManStop( pAbs );
             pAbs = NULL;
             Vec_IntFree( vFlops );
             vFlops = NULL;
             break;
         }
     }
     return vFlops;
 }


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


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

	FileName [saigAbsStart.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Sequential AIG package.]

	Synopsis [Counter-example-based abstraction.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

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

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

	#include "abs.h"
	#include "proof/ssw/ssw.h"
	#include "proof/fra/fra.h"
	#include "bdd/bbr/bbr.h"
	#include "proof/pdr/pdr.h"
	#include "sat/bmc/bmc.h"

	ABC_NAMESPACE_IMPL_START


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

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

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

	Synopsis [This procedure sets default parameters.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p )
	{
	memset( p, 0, sizeof(Gia_ParAbs_t) );
	p->Algo = 0; // algorithm: CBA
	p->nFramesMax = 10; // timeframes for PBA
	p->nConfMax = 10000; // conflicts for PBA
	p->fDynamic = 1; // dynamic unfolding for PBA
	p->fConstr = 0; // use constraints
	p->nFramesBmc = 250; // timeframes for BMC
	p->nConfMaxBmc = 5000; // conflicts for BMC
	p->nStableMax = 1000000; // the number of stable frames to quit
	p->nRatio = 10; // ratio of flops to quit
	p->nBobPar = 1000000; // the number of frames before trying to quit
	p->fUseBdds = 0; // use BDDs to refine abstraction
	p->fUseDprove = 0; // use 'dprove' to refine abstraction
	p->fUseStart = 1; // use starting frame
	p->fVerbose = 0; // verbose output
	p->fVeryVerbose= 0; // printing additional information
	p->Status = -1; // the problem status
	p->nFramesDone = -1; // the number of rames covered
	}


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

	Synopsis [Derive a new counter-example.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
	{
	Abc_Cex_t * pCex;
	Aig_Obj_t * pObj;
	int i, f;
	if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
	printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
	// else
	// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
	// start the counter-example
	pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
	pCex->iFrame = pCexAbs->iFrame;
	pCex->iPo = pCexAbs->iPo;
	// copy the bit data
	for ( f = 0; f <= pCexAbs->iFrame; f++ )
	{
	Saig_ManForEachPi( pAbs, pObj, i )
	{
	if ( i == Saig_ManPiNum(p) )
	break;
	if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
	Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
	}
	}
	// verify the counter example
	if ( !Saig_ManVerifyCex( p, pCex ) )
	{
	printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
	Abc_CexFree( pCex );
	pCex = NULL;
	}
	else
	{
	Abc_Print( 1, "Counter-example verification is successful.\n" );
	Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
	}
	return pCex;
	}

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

	Synopsis [Find the first PI corresponding to the flop.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
	{
	Aig_Obj_t * pObj;
	int i;
	assert( pAbs->vCiNumsOrig != NULL );
	Aig_ManForEachCi( p, pObj, i )
	{
	if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) )
	return i;
	}
	return -1;
	}

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

	Synopsis [Refines abstraction using one step.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
	{
	Vec_Int_t * vFlopsNew;
	int i, Entry, RetValue;
	*piRetValue = -1;
	if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
	{
	/*
	Fra_Sec_t SecPar, * pSecPar = &SecPar;
	Fra_SecSetDefaultParams( pSecPar );
	pSecPar->fVerbose = fVerbose;
	RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
	*/
	Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
	Pdr_Par_t Pars, * pPars = &Pars;
	Pdr_ManSetDefaultParams( pPars );
	pPars->nTimeOut = 10;
	pPars->fVerbose = fVerbose;
	if ( pPars->fVerbose )
	printf( "Running property directed reachability...\n" );
	RetValue = Pdr_ManSolve( pAbsOrpos, pPars );
	if ( pAbsOrpos->pSeqModel )
	pAbsOrpos->pSeqModel->iPo = Saig_ManFindFailedPoCex( pAbs, pAbsOrpos->pSeqModel );
	pAbs->pSeqModel = pAbsOrpos->pSeqModel;
	pAbsOrpos->pSeqModel = NULL;
	Aig_ManStop( pAbsOrpos );
	if ( RetValue )
	*piRetValue = 1;

	}
	else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
	{
	Saig_ParBbr_t Pars, * pPars = &Pars;
	Bbr_ManSetDefaultParams( pPars );
	pPars->TimeLimit = 0;
	pPars->nBddMax = 1000000;
	pPars->nIterMax = nFrames;
	pPars->fPartition = 1;
	pPars->fReorder = 1;
	pPars->fReorderImage = 1;
	pPars->fVerbose = fVerbose;
	pPars->fSilent = 0;
	RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
	if ( RetValue )
	*piRetValue = 1;
	}
	else
	{
	Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0, 0 );
	}
	if ( pAbs->pSeqModel == NULL )
	return NULL;
	if ( pnUseStart )
	*pnUseStart = pAbs->pSeqModel->iFrame;
	// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
	vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
	if ( vFlopsNew == NULL )
	return NULL;
	if ( Vec_IntSize(vFlopsNew) == 0 )
	{
	printf( "Discovered a true counter-example!\n" );
	p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel );
	Vec_IntFree( vFlopsNew );
	*piRetValue = 0;
	return NULL;
	}
	// vFlopsNew contains PI numbers that should be kept in pAbs
	if ( fVerbose )
	printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) );
	// add to the abstraction
	Vec_IntForEachEntry( vFlopsNew, Entry, i )
	{
	Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
	assert( Entry >= Saig_ManPiNum(p) );
	assert( Entry < Aig_ManCiNum(p) );
	Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
	}
	Vec_IntFree( vFlopsNew );

	Vec_IntSort( vFlops, 0 );
	Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
	assert( Vec_IntEntry(vFlops, i-1) != Entry );

	return Saig_ManDupAbstraction( p, vFlops );
	}

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

	Synopsis [Refines abstraction using one step.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
	{
	Aig_Man_t * pAbs;
	Vec_Int_t * vFlopsNew;
	int i, Entry;
	abctime clk = Abc_Clock();
	pAbs = Saig_ManDupAbstraction( p, vFlops );
	if ( fSensePath )
	vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
	else
	// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
	vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
	if ( vFlopsNew == NULL )
	{
	Aig_ManStop( pAbs );
	return 0;
	}
	if ( Vec_IntSize(vFlopsNew) == 0 )
	{
	printf( "Refinement did not happen. Discovered a true counter-example.\n" );
	printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAbs), Aig_ManCiNum(p) );
	p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex );
	Vec_IntFree( vFlopsNew );
	Aig_ManStop( pAbs );
	return 0;
	}
	if ( fVerbose )
	{
	printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) );
	Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
	}
	// vFlopsNew contains PI numbers that should be kept in pAbs
	// select the most useful flops among those to be added
	if ( nFfToAddMax > 0 && Vec_IntSize(vFlopsNew) > nFfToAddMax )
	{
	Vec_Int_t * vFlopsNewBest;
	// shift the indices
	Vec_IntForEachEntry( vFlopsNew, Entry, i )
	Vec_IntAddToEntry( vFlopsNew, i, -Saig_ManPiNum(p) );
	// create new flops
	vFlopsNewBest = Saig_ManCbaFilterFlops( p, pCex, vFlopClasses, vFlopsNew, nFfToAddMax );
	assert( Vec_IntSize(vFlopsNewBest) == nFfToAddMax );
	printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vFlopsNew), Vec_IntSize(vFlopsNewBest) );
	// update
	Vec_IntFree( vFlopsNew );
	vFlopsNew = vFlopsNewBest;
	// shift the indices
	Vec_IntForEachEntry( vFlopsNew, Entry, i )
	Vec_IntAddToEntry( vFlopsNew, i, Saig_ManPiNum(p) );
	}
	// add to the abstraction
	Vec_IntForEachEntry( vFlopsNew, Entry, i )
	{
	Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
	assert( Entry >= Saig_ManPiNum(p) );
	assert( Entry < Aig_ManCiNum(p) );
	Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
	}
	Vec_IntFree( vFlopsNew );
	Aig_ManStop( pAbs );
	return 1;
	}

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

	Synopsis [Transform flop map into flop list.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
	{
	Vec_Int_t * vFlops;
	int i, Entry;
	vFlops = Vec_IntAlloc( 100 );
	Vec_IntForEachEntry( vFlopClasses, Entry, i )
	if ( Entry )
	Vec_IntPush( vFlops, i );
	return vFlops;
	}

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

	Synopsis [Transform flop list into flop map.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops )
	{
	Vec_Int_t * vFlopClasses;
	int i, Entry;
	vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
	Vec_IntForEachEntry( vFlops, Entry, i )
	Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
	return vFlopClasses;
	}

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

	Synopsis [Refines abstraction using the latch map.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
	{
	Aig_Man_t * pNew;
	Vec_Int_t * vFlops;
	if ( pGia->vFlopClasses == NULL )
	{
	printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" );
	return -1;
	}
	pNew = Gia_ManToAig( pGia, 0 );
	vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
	if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
	{
	pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
	Vec_IntFree( vFlops );
	Aig_ManStop( pNew );
	return 0;
	}
	Vec_IntFree( pGia->vFlopClasses );
	pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
	Vec_IntFree( vFlops );
	Aig_ManStop( pNew );
	return -1;
	}


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

	Synopsis [Computes the flops to remain after abstraction.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
	{
	int nUseStart = 0;
	Aig_Man_t * pAbs, * pTemp;
	Vec_Int_t * vFlops;
	int Iter;//, clk = Abc_Clock(), clk2 = Abc_Clock();//, iFlop;
	assert( Aig_ManRegNum(p) > 0 );
	if ( pPars->fVerbose )
	printf( "Performing counter-example-based refinement.\n" );
	Aig_ManSetCioIds( p );
	vFlops = Vec_IntStartNatural( 1 );
	/*
	iFlop = Saig_ManFindFirstFlop( p );
	assert( iFlop >= 0 );
	vFlops = Vec_IntAlloc( 1 );
	Vec_IntPush( vFlops, iFlop );
	*/
	// create the resulting AIG
	pAbs = Saig_ManDupAbstraction( p, vFlops );
	if ( !pPars->fVerbose )
	{
	printf( "Init : " );
	Aig_ManPrintStats( pAbs );
	}
	printf( "Refining abstraction...\n" );
	for ( Iter = 0; ; Iter++ )
	{
	pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
	if ( pTemp == NULL )
	{
	ABC_FREE( p->pSeqModel );
	p->pSeqModel = pAbs->pSeqModel;
	pAbs->pSeqModel = NULL;
	Aig_ManStop( pAbs );
	break;
	}
	Aig_ManStop( pAbs );
	pAbs = pTemp;
	printf( "ITER %4d : ", Iter );
	if ( !pPars->fVerbose )
	Aig_ManPrintStats( pAbs );
	// output the intermediate result of abstraction
	Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
	// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
	// check if the ratio is reached
	if ( 100.0(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0pPars->nRatio )
	{
	printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
	Aig_ManStop( pAbs );
	pAbs = NULL;
	Vec_IntFree( vFlops );
	vFlops = NULL;
	break;
	}
	}
	return vFlops;
	}


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


	ABC_NAMESPACE_IMPL_END