abs.h File Reference

#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"

Go to the source code of this file.

Data Structures
struct	Abs_Par_t_
struct	Gia_ParAbs_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_	Abs_Par_t
	INCLUDES ///. More...
typedef struct Gia_ParAbs_t_	Gia_ParAbs_t

Functions
static int	Ga2_ObjOffset (Gia_Man_t *p, Gia_Obj_t *pObj)
	MACRO DEFINITIONS ///. More...
static int	Ga2_ObjLeaveNum (Gia_Man_t *p, Gia_Obj_t *pObj)
static int *	Ga2_ObjLeavePtr (Gia_Man_t *p, Gia_Obj_t *pObj)
static unsigned	Ga2_ObjTruth (Gia_Man_t *p, Gia_Obj_t *pObj)
static int	Ga2_ObjRefNum (Gia_Man_t *p, Gia_Obj_t *pObj)
static Vec_Int_t *	Ga2_ObjLeaves (Gia_Man_t *p, Gia_Obj_t *pObj)
Gia_Man_t *	Gia_ManDupAbsFlops (Gia_Man_t *p, Vec_Int_t *vFlopClasses)
	FUNCTION DECLARATIONS ///. More...
Gia_Man_t *	Gia_ManDupAbsGates (Gia_Man_t *p, Vec_Int_t *vGateClasses)
void	Gia_ManGlaCollect (Gia_Man_t *p, Vec_Int_t *vGateClasses, Vec_Int_t **pvPis, Vec_Int_t **pvPPis, Vec_Int_t **pvFlops, Vec_Int_t **pvNodes)
void	Gia_ManPrintFlopClasses (Gia_Man_t *p)
void	Gia_ManPrintObjClasses (Gia_Man_t *p)
void	Gia_ManPrintGateClasses (Gia_Man_t *p)
int	Gia_ManPerformGla (Gia_Man_t *p, Abs_Par_t *pPars)
int	Gia_ManPerformGlaOld (Gia_Man_t *p, Abs_Par_t *pPars, int fStartVta)
Gia_Man_t *	Gia_ManShrinkGla (Gia_Man_t *p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose)
void	Gia_GlaProveAbsracted (Gia_Man_t *p, int fSimpProver, int fVerbose)
	DECLARATIONS ///. More...
void	Gia_GlaProveCancel (int fVerbose)
int	Gia_GlaProveCheck (int fVerbose)
int	Gia_VtaPerform (Gia_Man_t *pAig, Abs_Par_t *pPars)
void	Abs_ParSetDefaults (Abs_Par_t *p)
	DECLARATIONS ///. More...
Vec_Int_t *	Gia_VtaConvertToGla (Gia_Man_t *p, Vec_Int_t *vVta)
Vec_Int_t *	Gia_VtaConvertFromGla (Gia_Man_t *p, Vec_Int_t *vGla, int nFrames)
Vec_Int_t *	Gia_FlaConvertToGla (Gia_Man_t *p, Vec_Int_t *vFla)
Vec_Int_t *	Gia_GlaConvertToFla (Gia_Man_t *p, Vec_Int_t *vGla)
int	Gia_GlaCountFlops (Gia_Man_t *p, Vec_Int_t *vGla)
int	Gia_GlaCountNodes (Gia_Man_t *p, Vec_Int_t *vGla)
Gia_Man_t *	Abs_RpmPerform (Gia_Man_t *p, int nCutMax, int fVerbose, int fVeryVerbose)
Gia_Man_t *	Abs_RpmPerformOld (Gia_Man_t *p, int fVerbose)
void	Gia_ManAbsSetDefaultParams (Gia_ParAbs_t *p)
	DECLARATIONS ///. More...
Vec_Int_t *	Saig_ManCexAbstractionFlops (Aig_Man_t *p, Gia_ParAbs_t *pPars)
Vec_Int_t *	Saig_ManCbaFilterFlops (Aig_Man_t *pAig, Abc_Cex_t *pAbsCex, Vec_Int_t *vFlopClasses, Vec_Int_t *vAbsFfsToAdd, int nFfsToSelect)
	FUNCTION DEFINITIONS ///. More...
Abc_Cex_t *	Saig_ManCbaFindCexCareBits (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
int	Gia_ManCexAbstractionRefine (Gia_Man_t *pGia, Abc_Cex_t *pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose)
Vec_Int_t *	Saig_ManExtendCounterExampleTest3 (Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Vec_Int_t *	Saig_ManExtendCounterExampleTest2 (Aig_Man_t *p, int iFirstPi, Abc_Cex_t *pCex, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t

INCLUDES ///.

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

FileName [abs.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 46 of file abs.h.

typedef struct Gia_ParAbs_t_ Gia_ParAbs_t

Definition at line 84 of file abs.h.

Function Documentation

void Abs_ParSetDefaults

(

Abs_Par_t *

p

)

DECLARATIONS ///.

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

FileName [absUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Interface to pthreads.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file absUtil.c.

{
    memset( p, 0, sizeof(Abs_Par_t) );
    p->nFramesMax         =      0;   // maximum frames
    p->nFramesStart       =      0;   // starting frame 
    p->nFramesPast        =      4;   // overlap frames
    p->nConfLimit         =      0;   // conflict limit
    p->nLearnedMax        =   1000;   // max number of learned clauses
    p->nLearnedStart      =   1000;   // max number of learned clauses
    p->nLearnedDelta      =    200;   // max number of learned clauses
    p->nLearnedPerce      =     70;   // max number of learned clauses
    p->nTimeOut           =      0;   // timeout in seconds
    p->nRatioMin          =      0;   // stop when less than this % of object is abstracted
    p->nRatioMax          =     30;   // restart when more than this % of object is abstracted
    p->fUseTermVars       =      0;   // use terminal variables
    p->fUseRollback       =      0;   // use rollback to the starting number of frames
    p->fPropFanout        =      1;   // propagate fanouts during refinement
    p->fVerbose           =      0;   // verbose flag
    p->iFrame             =     -1;   // the number of frames covered 
    p->iFrameProved       =     -1;   // the number of frames proved
    p->nFramesNoChangeLim =      2;   // the number of frames without change to dump abstraction
}

Gia_Man_t* Abs_RpmPerform	(	Gia_Man_t *	p,
		int	nCutMax,
		int	fVerbose,
		int	fVeryVerbose
	)

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

Synopsis [Performs structural reparametrization.]

Description []

SideEffects []

SeeAlso []

Definition at line 772 of file absRpm.c.

{
    Gia_Man_t * pNew;
//    Gia_ManTestDoms( p );
//    return NULL;
    // perform structural analysis
    Gia_ObjComputeTruthTableStart( p, nCutMax );
    Abs_RpmPerformMark( p, nCutMax, fVerbose, fVeryVerbose );
    Gia_ObjComputeTruthTableStop( p );
    // derive new AIG
    pNew = Gia_ManDupRpm( p );
    Gia_ManCleanMark1( p );
    return pNew;
}

Gia_Man_t* Abs_RpmPerformOld	(	Gia_Man_t *	p,
		int	fVerbose
	)

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

Synopsis [Reparameterized to get rid of useless primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file absRpmOld.c.

{
//    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
    Aig_Man_t * pMan, * pTemp;
    Gia_Man_t * pNew, * pTmp;
    int nFlopsOld = Gia_ManRegNum(p);
    if ( fVerbose )
    {
        printf( "Original AIG:\n" );
        Gia_ManPrintStats( p, NULL );
    }

    // perform input trimming
    pNew = Gia_ManDupTrimmed( p, 1, 0, 0, -1 );
    if ( fVerbose )
    {
        printf( "After PI trimming:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
    // transform GIA
    pNew = Gia_ManDupIn2Ff( pTmp = pNew );
    Gia_ManStop( pTmp );
    if ( fVerbose )
    {
        printf( "After PI-2-FF transformation:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }

    // derive AIG
    pMan = Gia_ManToAigSimple( pNew );
    Gia_ManStop( pNew );
    // perform min-reg retiming
    pMan = Saig_ManRetimeMinArea( pTemp = pMan, 10, 0, 0, 1, 0 );
    Aig_ManStop( pTemp );
    // derive GIA
    pNew = Gia_ManFromAigSimple( pMan );
    Aig_ManStop( pMan );
    if ( fVerbose )
    {
        printf( "After min-area retiming:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }

    // transform back
    pNew = Gia_ManDupFf2In( pTmp = pNew, nFlopsOld );
    Gia_ManStop( pTmp );
    if ( fVerbose )
    {
        printf( "After FF-2-PI tranformation:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
    return pNew;
}

static int Ga2_ObjLeaveNum ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

Definition at line 113 of file abs.h.

{ return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                     }

static int* Ga2_ObjLeavePtr ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

Definition at line 114 of file abs.h.

{ return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                                }

static Vec_Int_t* Ga2_ObjLeaves ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

Definition at line 117 of file abs.h.

{ static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;       }

static int Ga2_ObjOffset ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 112 of file abs.h.

{ return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                         }

static int Ga2_ObjRefNum ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

Definition at line 116 of file abs.h.

{ return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);            }

static unsigned Ga2_ObjTruth ( Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

Definition at line 115 of file abs.h.

{ return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);            }

Vec_Int_t* Gia_FlaConvertToGla	(	Gia_Man_t *	p,
		Vec_Int_t *	vFla
	)

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

Synopsis [Converting FLA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file absUtil.c.

{
    Vec_Int_t * vGla;
    Gia_Obj_t * pObj;
    int i;
    // mark const0 and relevant CI objects
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
    Gia_ManForEachPi( p, pObj, i )
        Gia_ObjSetTravIdCurrent(p, pObj);
    Gia_ManForEachRo( p, pObj, i )
        if ( !Vec_IntEntry(vFla, i) )
            Gia_ObjSetTravIdCurrent(p, pObj);
    // label all objects reachable from the PO and selected flops
    vGla = Vec_IntStart( Gia_ManObjNum(p) );
    Vec_IntWriteEntry( vGla, 0, 1 );
    Gia_ManForEachPo( p, pObj, i )
        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    Gia_ManForEachRi( p, pObj, i )
        if ( Vec_IntEntry(vFla, i) )
            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    return vGla;
}

Vec_Int_t* Gia_GlaConvertToFla	(	Gia_Man_t *	p,
		Vec_Int_t *	vGla
	)

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

Synopsis [Converting GLA vector to FLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file absUtil.c.

{
    Vec_Int_t * vFla;
    Gia_Obj_t * pObj;
    int i;
    vFla = Vec_IntStart( Gia_ManRegNum(p) );
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Vec_IntWriteEntry( vFla, i, 1 );
    return vFla;
}

int Gia_GlaCountFlops	(	Gia_Man_t *	p,
		Vec_Int_t *	vGla
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 231 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}

int Gia_GlaCountNodes	(	Gia_Man_t *	p,
		Vec_Int_t *	vGla
	)

Definition at line 240 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachAnd( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}

void Gia_GlaProveAbsracted	(	Gia_Man_t *	p,
		int	fSimpProver,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [absPth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Interface to pthreads.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 45 of file absPth.c.

{}

void Gia_GlaProveCancel

(

int

fVerbose

)

Definition at line 46 of file absPth.c.

{}

int Gia_GlaProveCheck

(

int

fVerbose

)

Definition at line 47 of file absPth.c.

{ return 0; }

void Gia_ManAbsSetDefaultParams

(

Gia_ParAbs_t *

p

)

DECLARATIONS ///.

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file absOldRef.c.

{
    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
}

int Gia_ManCexAbstractionRefine	(	Gia_Man_t *	pGia,
		Abc_Cex_t *	pCex,
		int	nFfToAddMax,
		int	fTryFour,
		int	fSensePath,
		int	fVerbose
	)

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

Synopsis [Refines abstraction using the latch map.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file absOldRef.c.

{
    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;
}

Gia_Man_t* Gia_ManDupAbsFlops	(	Gia_Man_t *	p,
		Vec_Int_t *	vFlopClasses
	)

FUNCTION DECLARATIONS ///.

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

Synopsis [Extractes a flop-level abstraction given a flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file absDup.c.

{ 
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;
    int i, nFlops = 0;
    Gia_ManFillValue( p );
    // start the new manager
    pNew = Gia_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create PIs
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create additional PIs
    Gia_ManForEachRo( p, pObj, i )
        if ( !Vec_IntEntry(vFlopClasses, i) )
            pObj->Value = Gia_ManAppendCi(pNew);
    // create ROs
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vFlopClasses, i) )
            pObj->Value = Gia_ManAppendCi(pNew);
    // create POs
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachPo( p, pObj, i )
    {
        Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    // create RIs
    Gia_ManForEachRi( p, pObj, i )
        if ( Vec_IntEntry(vFlopClasses, i) )
        {
            Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
            nFlops++;
        }
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, nFlops );
    // clean up
    pNew = Gia_ManSeqCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Gia_Man_t* Gia_ManDupAbsGates	(	Gia_Man_t *	p,
		Vec_Int_t *	vGateClasses
	)

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

Synopsis [Extractes a gate-level abstraction given a gate map.]

Description [The array contains 1 for those objects (const, RO, AND) that are included in the abstraction; 0, otherwise.]

SideEffects []

SeeAlso []

Definition at line 220 of file absDup.c.

{ 
    Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pCopy;
    int i;//, nFlops = 0;
    assert( Gia_ManPoNum(p) == 1 );
    assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );

    // create additional arrays
    Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );

    // start the new manager
    pNew = Gia_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create constant
    Gia_ManFillValue( p );
    Gia_ManConst0(p)->Value = 0;
    // create PIs
    Gia_ManForEachObjVec( vPis, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create additional PIs
    Gia_ManForEachObjVec( vPPis, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create ROs
    Gia_ManForEachObjVec( vFlops, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create internal nodes
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
//        Gia_ManDupAbsGates_rec( pNew, pObj );
    // create PO
    Gia_ManForEachPo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    // create RIs
    Gia_ManForEachObjVec( vFlops, p, pObj, i )
        Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
    Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
    // clean up
    pNew = Gia_ManSeqCleanup( pTemp = pNew );
    // transfer copy values: (p -> pTemp -> pNew) => (p -> pNew)
    if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) )
    {
//        printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
        Gia_ManForEachObj( p, pObj, i )
        {
            if ( !~pObj->Value )
                continue;
            assert( !Abc_LitIsCompl(pObj->Value) );
            pCopy = Gia_ObjCopy( pTemp, pObj );
            if ( !~pCopy->Value )
            {
                Vec_IntWriteEntry( vGateClasses, i, 0 );
                pObj->Value = ~0;
                continue;
            }
            assert( !Abc_LitIsCompl(pCopy->Value) );
            pObj->Value = pCopy->Value;
        }
    }
    Gia_ManStop( pTemp );

    Vec_IntFree( vPis );
    Vec_IntFree( vPPis );
    Vec_IntFree( vFlops );
    Vec_IntFree( vNodes );
    return pNew;
}

void Gia_ManGlaCollect	(	Gia_Man_t *	p,
		Vec_Int_t *	vGateClasses,
		Vec_Int_t **	pvPis,
		Vec_Int_t **	pvPPis,
		Vec_Int_t **	pvFlops,
		Vec_Int_t **	pvNodes
	)

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

Synopsis [Collects PIs and PPIs of the abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file absDup.c.

{ 
    Vec_Int_t * vAssigned;
    Gia_Obj_t * pObj;
    int i;
    assert( Gia_ManPoNum(p) == 1 );
    assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
    // create included objects and their fanins
    vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
    // create additional arrays
    if ( pvPis )   *pvPis   = Vec_IntAlloc( 100 );
    if ( pvPPis )  *pvPPis  = Vec_IntAlloc( 100 );
    if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 );
    if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 );
    Gia_ManForEachObjVec( vAssigned, p, pObj, i )
    {
        if ( Gia_ObjIsPi(p, pObj) )
            { if ( pvPis )   Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) );   }
        else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
            { if ( pvPPis )  Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) );  }
        else if ( Gia_ObjIsRo(p, pObj) )
            { if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); }
        else if ( Gia_ObjIsAnd(pObj) )
            { if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); }
        else assert( Gia_ObjIsConst0(pObj) );
    }
    Vec_IntFree( vAssigned );
}

int Gia_ManPerformGla	(	Gia_Man_t *	pAig,
		Abs_Par_t *	pPars
	)

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

Synopsis [Performs gate-level abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 1500 of file absGla.c.

{
    int fUseSecondCore = 1;
    Ga2_Man_t * p;
    Vec_Int_t * vCore, * vPPis;
    abctime clk2, clk = Abc_Clock();
    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
    int i, c, f, Lit;
    pPars->iFrame = -1;
    // check trivial case 
    assert( Gia_ManPoNum(pAig) == 1 ); 
    ABC_FREE( pAig->pCexSeq );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
        return 0;
    }
    // create gate classes if not given
    if ( pAig->vGateClasses == NULL )
    {
        pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
        Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
        Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
    }
    // start the manager
    p = Ga2_ManStart( pAig, pPars );
    p->timeInit = Abc_Clock() - clk;
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  Limit = %d %%  Limit2 = %d %%  RatioMax = %d %%\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMin2, pPars->nRatioMax );
        Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
        if ( pPars->fDumpVabs || pPars->fDumpMabs )
            Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
                pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
    }
    // iterate unrolling
    for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
    {
        int nAbsOld;
        // remember the timeframe
        p->pPars->iFrame = -1;
        // create new SAT solver
        Ga2_ManRestart( p );
        // remember abstraction size after the last restart
        nAbsOld = Vec_IntSize(p->vAbs);
        // unroll the circuit
        for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
        {
            // remember current limits
            int nConflsBeg = sat_solver2_nconflicts(p->pSat);
            int nAbs       = Vec_IntSize(p->vAbs);
            int nValues    = Vec_IntSize(p->vValues);
            int nVarsOld;
            // remember the timeframe
            p->pPars->iFrame = f;
            // extend and clear storage
            if ( f == Vec_PtrSize(p->vId2Lit) )
                Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
            Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
            // add static clauses to this timeframe
            Ga2_ManAddAbsClauses( p, f );
            // skip checking if skipcheck is enabled (&gla -s)
            if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
                continue;
            // skip checking if we need to skip several starting frames (&gla -S <num>)
            if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
                continue;
            // get the output literal
//            Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
            Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
            assert( Lit >= 0 );
            Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
            if ( Lit == 0 )
                continue;
            assert( Lit > 1 );
            // check for counter-examples
            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
                sat_solver2_setnvars( p->pSat, p->nSatVars );
            nVarsOld = p->nSatVars;
            for ( c = 0; ; c++ )
            {
                // consider the special case when the target literal is implied false
                // by implications which happened as a result of previous refinements
                // note that incremental UNSAT core cannot be computed because there is no learned clauses
                // in this case, we will assume that UNSAT core cannot reduce the problem
                if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
                {
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    break;
                }
                // perform SAT solving
                clk2 = Abc_Clock();
                Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( Status == l_True ) // perform refinement
                {
                    p->nCexes++;
                    p->timeSat += Abc_Clock() - clk2;

                    // cancel old one if it was sent
                    if ( Abc_FrameIsBridgeMode() && fOneIsSent )
                    {
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                        fOneIsSent = 0;
                    }
                    if ( iFrameTryToProve >= 0 )
                    {
                        Gia_GlaProveCancel( pPars->fVerbose );
                        iFrameTryToProve = -1;
                    }

                    // perform refinement
                    clk2 = Abc_Clock();
                    Rnm_ManSetRefId( p->pRnm, c );
                    vPPis = Ga2_ManRefine( p );
                    p->timeCex += Abc_Clock() - clk2;
                    if ( vPPis == NULL )
                    {
                        if ( pPars->fVerbose )
                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
                        goto finish;
                    }

                    if ( c == 0 )
                    {
//                        Ga2_ManRefinePrintPPis( p );
                        // create bookmark to be used for rollback
                        assert( nVarsOld == p->pSat->size );
                        sat_solver2_bookmark( p->pSat );
                        // start incremental proof manager
                        assert( p->pSat->pPrf2 == NULL );
                        p->pSat->pPrf2 = Prf_ManAlloc();
                        if ( p->pSat->pPrf2 )
                        {
                            p->nProofIds = 0;
                            Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                            Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
                        }
                    }
                    else
                    {
                        // resize the proof logger
                        if ( p->pSat->pPrf2 )
                            Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
                    }

                    Ga2_ManAddToAbs( p, vPPis );
                    Vec_IntFree( vPPis );
                    if ( pPars->fVerbose )
                        Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
                    // check if the number of objects is below limit
                    if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
                    {
                        Status = l_Undef;
                        goto finish;
                    }
                    continue;
                }
                p->timeUnsat += Abc_Clock() - clk2;
                if ( Status == l_Undef ) // ran out of resources
                    goto finish;
                if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
                    goto finish;
                if ( c == 0 )
                {
                    if ( f > p->pPars->iFrameProved )
                        p->pPars->nFramesNoChange++;
                    break;
                }
                if ( f > p->pPars->iFrameProved )
                    p->pPars->nFramesNoChange = 0;

                // derive the core
                assert( p->pSat->pPrf2 != NULL );
                vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                Prf_ManStopP( &p->pSat->pPrf2 );
                // update the SAT solver
                sat_solver2_rollback( p->pSat );
                // reduce abstraction
                Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );

                // purify UNSAT core
                if ( fUseSecondCore )
                {
//                    int nOldCore = Vec_IntSize(vCore);
                    // reverse the order of objects in the core
//                    Vec_IntSort( vCore, 0 );
//                    Vec_IntPrint( vCore );
                    // create bookmark to be used for rollback
                    assert( nVarsOld == p->pSat->size );
                    sat_solver2_bookmark( p->pSat );
                    // start incremental proof manager
                    assert( p->pSat->pPrf2 == NULL );
                    p->pSat->pPrf2 = Prf_ManAlloc();
                    if ( p->pSat->pPrf2 )
                    {
                        p->nProofIds = 0;
                        Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                        Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );

                        Ga2_ManAddToAbs( p, vCore );
                        Vec_IntFree( vCore );
                    }
                    // run SAT solver
                    clk2 = Abc_Clock();
                    Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                    if ( Status == l_Undef )
                        goto finish;
                    assert( Status == l_False );
                    p->timeUnsat += Abc_Clock() - clk2;

                    // derive the core
                    assert( p->pSat->pPrf2 != NULL );
                    vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    // update the SAT solver
                    sat_solver2_rollback( p->pSat );
                    // reduce abstraction
                    Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
//                    printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
                }

                Ga2_ManAddToAbs( p, vCore );
//                Ga2_ManRefinePrint( p, vCore );
                Vec_IntFree( vCore );
                break;
            }
            // remember the last proved frame
            if ( p->pPars->iFrameProved < f )
                p->pPars->iFrameProved = f;
            // print statistics
            if ( pPars->fVerbose )
                Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
            // check if abstraction was proved
            if ( Gia_GlaProveCheck( pPars->fVerbose ) )
            {
                RetValue = 1;
                goto finish;
            }
            if ( c > 0 ) 
            {
                if ( p->pPars->fVeryVerbose )
                    Abc_Print( 1, "\n" );
                // recompute the abstraction
                Vec_IntFreeP( &pAig->vGateClasses );
                pAig->vGateClasses = Ga2_ManAbsTranslate( p );
                // check if the number of objects is below limit
                if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
                {
                    Status = l_Undef;
                    goto finish;
                }
            }
            // check the number of stable frames
            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
            {
                // dump the model into file
                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
                {
                    char Command[1000];
                    Abc_FrameSetStatus( -1 );
                    Abc_FrameSetCex( NULL );
                    Abc_FrameSetNFrames( f );
                    sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
                    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                    Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                }
                // call the prover
                if ( p->pPars->fCallProver )
                {
                    // cancel old one if it is proving
                    if ( iFrameTryToProve >= 0 )
                        Gia_GlaProveCancel( pPars->fVerbose );
                    // prove new one
                    Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
                    iFrameTryToProve = f;
                    p->nPdrCalls++;
                }
                // speak to the bridge
                if ( Abc_FrameIsBridgeMode() )
                {
                    // cancel old one if it was sent
                    if ( fOneIsSent )
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                    // send new one 
                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
                    fOneIsSent = 1;
                }
            }
            // if abstraction grew more than a certain percentage, force a restart
            if ( pPars->nRatioMax == 0 )
                continue;
            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
            {
                if ( p->pPars->fVerbose )
                Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
                    nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
                break;
            }
        }
    }
finish:
    Prf_ManStopP( &p->pSat->pPrf2 );
    // cancel old one if it is proving
    if ( iFrameTryToProve >= 0 )
        Gia_GlaProveCancel( pPars->fVerbose );
    // analize the results
    if ( !p->fUseNewLine )
        Abc_Print( 1, "\n" );
    if ( RetValue == 1 )
        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d  ", p->pPars->iFrameProved+1, iFrameTryToProve );
    else if ( pAig->pCexSeq == NULL )
    {
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Ga2_ManAbsTranslate( p );
        if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
            Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
            Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement.  ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
        else if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d.  ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
        else
            Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction.  ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        p->pPars->iFrame = p->pPars->iFrameProved;
    }
    else
    {
        if ( p->pPars->fVerbose )
            Abc_Print( 1, "\n" );
        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
        Abc_Print( 1, "True counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = f - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
        Ga2_ManReportMemory( p );
    }
//    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
    Ga2_ManStop( p );
    fflush( stdout );
    return RetValue;
}

int Gia_ManPerformGlaOld	(	Gia_Man_t *	pAig,
		Abs_Par_t *	pPars,
		int	fStartVta
	)

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

Synopsis [Performs gate-level abstraction]

Description []

SideEffects []

SeeAlso []

Definition at line 1638 of file absGlaOld.c.

{
    extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars );
    extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
    Gla_Man_t * p;
    Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
    Abc_Cex_t * pCex = NULL;
    int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1;
    abctime clk2, clk = Abc_Clock();
    // preconditions
    assert( Gia_ManPoNum(pAig) == 1 );
    assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            printf( "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        ABC_FREE( pAig->pCexSeq );
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        printf( "Sequential miter is trivially SAT.\n" );
        return 0;
    }

    // compute intial abstraction
    if ( pAig->vGateClasses == NULL )
    {
        if ( fStartVta )
        {
            int nFramesMaxOld   = pPars->nFramesMax;
            int nFramesStartOld = pPars->nFramesStart;
            int nTimeOutOld     = pPars->nTimeOut;
            int nDumpOld        = pPars->fDumpVabs;
            pPars->nFramesMax   = pPars->nFramesStart;
            pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
            pPars->nTimeOut     = 20;
            pPars->fDumpVabs    = 0;
            RetValue = Gia_VtaPerformInt( pAig, pPars );
            pPars->nFramesMax   = nFramesMaxOld;
            pPars->nFramesStart = nFramesStartOld;
            pPars->nTimeOut     = nTimeOutOld;
            pPars->fDumpVabs    = nDumpOld;
            // create gate classes
            Vec_IntFreeP( &pAig->vGateClasses );
            if ( pAig->vObjClasses )
                pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
            Vec_IntFreeP( &pAig->vObjClasses );
            // return if VTA solve the problem if could not start
            if ( RetValue == 0 || pAig->vGateClasses == NULL )
                return RetValue;
        }
        else
        {
            pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
            Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
            Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
        }
    }
    // start the manager
    p = Gla_ManStart( pAig, pPars );
    p->timeInit = Abc_Clock() - clk;
    // set runtime limit
    if ( p->pPars->nTimeOut )
        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%.\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
        Abc_Print( 1, "LearnStart = %d  LearnDelta = %d  LearnRatio = %d %%.\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
    }
    for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
    {
        int nConflsBeg = sat_solver2_nconflicts(p->pSat);
        p->pPars->iFrame = f;

        // load timeframe
        Gia_GlaAddTimeFrame( p, f );

        // iterate as long as there are counter-examples
        for ( i = 0; ; i++ )
        { 
            clk2 = Abc_Clock();
            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
//            assert( (vCore != NULL) == (Status == 1) );
            if ( Status == -1 || (p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
            {
                Prf_ManStopP( &p->pSat->pPrf2 );
//                if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction
//                    Vec_IntShrink( p->vAbs, p->nAbsOld );
                goto finish;
            }
            if ( Status == 1 )
            {
                Prf_ManStopP( &p->pSat->pPrf2 );
                p->timeUnsat += Abc_Clock() - clk2;
                break;
            } 
            p->timeSat += Abc_Clock() - clk2;
            assert( Status == 0 );
            p->nCexes++;

            // cancel old one if it was sent
            if ( Abc_FrameIsBridgeMode() && fOneIsSent )
            {
                Gia_GlaSendCancel( p, pPars->fVerbose );
                fOneIsSent = 0;
            }

            // perform the refinement
            clk2 = Abc_Clock();
            if ( pPars->fAddLayer )
            {
                vPPis = Gla_ManCollectPPis( p, NULL );
//                Gla_ManExplorePPis( p, vPPis );
            }
            else
            {
                vPPis = Gla_ManRefinement( p );
                if ( vPPis == NULL )
                {
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
                    break;
                }
            } 
            assert( pCex == NULL );

            // start proof logging
            if ( i == 0 )
            {
                // create bookmark to be used for rollback
                sat_solver2_bookmark( p->pSat );
                Vec_IntClear( p->vAddedNew );
                p->nAbsOld = Vec_IntSize( p->vAbs );
                nVarsOld = p->nSatVars;
//                p->nLrnOld = sat_solver2_nlearnts( p->pSat );
//                p->nAbsNew = 0;
//                p->nLrnNew = 0;

                // start incremental proof manager
                assert( p->pSat->pPrf2 == NULL );
                if ( p->pSat->pPrf1 == NULL )
                    p->pSat->pPrf2 = Prf_ManAlloc();
                if ( p->pSat->pPrf2 )
                {
                    p->nProofIds = 0;
                    Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                    Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
                }
            }
            else
            {
                // resize the proof logger
                if ( p->pSat->pPrf2 )
                    Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
            }

            Gia_GlaAddToAbs( p, vPPis, 1 );
            Gia_GlaAddOneSlice( p, f, vPPis );
            Vec_IntFree( vPPis );

            // print the result (do not count it towards change)
            if ( p->pPars->fVerbose )
            Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
        }
        if ( pCex != NULL )
            break;
        assert( Status == 1 );

        // valid core is obtained
        nCoreSize = 1;
        if ( vCore )
        {
            nCoreSize += Vec_IntSize( vCore );
            Gia_GlaAddToCounters( p, vCore );
        }
        if ( i == 0 )
        {
            p->pPars->nFramesNoChange++;
            Vec_IntFreeP( &vCore );
        }
        else
        {
            p->pPars->nFramesNoChange = 0;
//            p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld;
//            p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld );
            // update the SAT solver
            sat_solver2_rollback( p->pSat );
            // update storage
            Gla_ManRollBack( p );
            p->nSatVars = nVarsOld;
            // load this timeframe
            Gia_GlaAddToAbs( p, vCore, 0 );
            Gia_GlaAddOneSlice( p, f, vCore );
            Vec_IntFree( vCore );
            // run SAT solver
            clk2 = Abc_Clock();
            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
            p->timeUnsat += Abc_Clock() - clk2;
//            assert( (vCore != NULL) == (Status == 1) );
            Vec_IntFreeP( &vCore );
            if ( Status == -1 ) // resource limit is reached
                break;
            if ( Status == 0 )
            {
                assert( 0 );
    //            Vta_ManSatVerify( p );
                // make sure, there was no initial abstraction (otherwise, it was invalid)
                assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
    //            pCex = Vga_ManDeriveCex( p );
                break;
            }
        }
        // print the result
        if ( p->pPars->fVerbose )
        Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );

        if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened
        {
            if ( Abc_FrameIsBridgeMode() )
            {
                // cancel old one if it was sent
                if ( fOneIsSent )
                    Gia_GlaSendCancel( p, pPars->fVerbose );
                // send new one 
                Gia_GlaSendAbsracted( p, pPars->fVerbose );
                fOneIsSent = 1;
            }

            // dump the model into file
            if ( p->pPars->fDumpVabs )
            {
                char Command[1000];
                Abc_FrameSetStatus( -1 );
                Abc_FrameSetCex( NULL );
                Abc_FrameSetNFrames( f+1 );
                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status") );
                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                Gia_GlaDumpAbsracted( p, pPars->fVerbose );
            }
        }

        // check if the number of objects is below limit
        if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
        {
            Status = -1;
            break;
        }
    }
finish:
    // analize the results
    if ( pCex == NULL )
    {
        if ( p->pPars->fVerbose && Status == -1 )
            printf( "\n" );
//        if ( pAig->vGateClasses != NULL )
//            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Gla_ManTranslate( p );
        if ( Status == -1 )
        {
            if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
                Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
            else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
            else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
                Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
            else
                Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
        }
        else
        {
            p->pPars->iFrame++;
            Abc_Print( 1, "GLA completed %d frames with a %d-stable abstraction.  ", f, p->pPars->nFramesNoChange );
        }
    }
    else
    {
        if ( p->pPars->fVerbose )
            printf( "\n" );
        ABC_FREE( pAig->pCexSeq );
        pAig->pCexSeq = pCex;
        if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) )
            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = pCex->iFrame - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
        Gla_ManReportMemory( p );
    }
//    Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 );
    Gla_ManStop( p );
    fflush( stdout );
    return RetValue;
}

void Gia_ManPrintFlopClasses

(

Gia_Man_t *

p

)

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

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file absDup.c.

{
    int Counter0, Counter1;
    if ( p->vFlopClasses == NULL )
        return;
    if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) )
    {
        printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" );
        return;
    }
    Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
    Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
    printf( "Flop-level abstraction:  Excluded FFs = %d  Included FFs = %d  (%.2f %%) ", 
        Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
    if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
        printf( "and there are other FF classes..." );
    printf( "\n" );
}

void Gia_ManPrintGateClasses

(

Gia_Man_t *

p

)

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

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file absDup.c.

{
    Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
    int nTotal;
    if ( p->vGateClasses == NULL )
        return;
    if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
    {
        printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
        return;
    }
    // create additional arrays
    Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
    nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
    printf( "Gate-level abstraction:  PI = %d  PPI = %d  FF = %d (%.2f %%)  AND = %d (%.2f %%)  Obj = %d (%.2f %%)\n", 
        Vec_IntSize(vPis), Vec_IntSize(vPPis), 
        Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), 
        Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), 
        nTotal,              100.0*nTotal             /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
    Vec_IntFree( vPis );
    Vec_IntFree( vPPis );
    Vec_IntFree( vFlops );
    Vec_IntFree( vNodes );
}

void Gia_ManPrintObjClasses

(

Gia_Man_t *

p

)

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

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file absDup.c.

{
    Vec_Int_t * vSeens;  // objects seen so far
    Vec_Int_t * vAbs = p->vObjClasses;
    int i, k, Entry, iStart, iStop = -1, nFrames;
    int nObjBits, nObjMask, iObj, iFrame, nWords;
    unsigned * pInfo;
    int * pCountAll, * pCountUni;
    if ( vAbs == NULL )
        return;
    nFrames = Vec_IntEntry( vAbs, 0 );
    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
    pCountAll = ABC_ALLOC( int, nFrames + 1 );
    pCountUni = ABC_ALLOC( int, nFrames + 1 );
    // start storage for seen objects
    nWords = Abc_BitWordNum( nFrames );
    vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
    // get the bitmasks
    nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
    nObjMask = (1 << nObjBits) - 1;
    assert( Gia_ManObjNum(p) <= nObjMask );
    // print info about frames
    printf( "Frame   Core   F0   F1   F2   F3 ...\n" );
    for ( i = 0; i < nFrames; i++ )
    {
        iStart = Vec_IntEntry( vAbs, i+1 );
        iStop  = Vec_IntEntry( vAbs, i+2 );
        memset( pCountAll, 0, sizeof(int) * (nFrames + 1) );
        memset( pCountUni, 0, sizeof(int) * (nFrames + 1) );
        Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
        {
            iObj   = (Entry &  nObjMask);
            iFrame = (Entry >> nObjBits);
            pInfo  = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
            if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
            {
                Abc_InfoSetBit( pInfo, iFrame );
                pCountUni[iFrame+1]++;
                pCountUni[0]++;
            }
            pCountAll[iFrame+1]++;
            pCountAll[0]++;
        }
        assert( pCountAll[0] == (iStop - iStart) );
//        printf( "%5d%5d  ", pCountAll[0], pCountUni[0] ); 
        printf( "%3d :", i );
        printf( "%7d", pCountAll[0] ); 
        if ( i >= 10 )
        {
            for ( k = 0; k < 4; k++ )
                printf( "%5d", pCountAll[k+1] ); 
            printf( "  ..." );
            for ( k = i-4; k <= i; k++ )
                printf( "%5d", pCountAll[k+1] ); 
        }
        else
        {
            for ( k = 0; k <= i; k++ )
                if ( k <= i )
                    printf( "%5d", pCountAll[k+1] ); 
        }
//        for ( k = 0; k < nFrames; k++ )
//            if ( k <= i )
//                printf( "%5d", pCountAll[k+1] ); 
        printf( "\n" );
    }
    assert( iStop == Vec_IntSize(vAbs) );
    Vec_IntFree( vSeens );
    ABC_FREE( pCountAll );
    ABC_FREE( pCountUni );
}

Gia_Man_t* Gia_ManShrinkGla	(	Gia_Man_t *	p,
		int	nFrameMax,
		int	nTimeOut,
		int	fUsePdr,
		int	fUseSat,
		int	fUseBdd,
		int	fVerbose
	)

Definition at line 67 of file absIter.c.

{
    Gia_Obj_t * pObj;
    int i, iFrame0, iFrame;
    int nTotal = 0, nRemoved = 0;
    Vec_Int_t * vGScopy;
    abctime clk, clkTotal = Abc_Clock();
    assert( Gia_ManPoNum(p) == 1 );
    assert( p->vGateClasses != NULL );
    vGScopy = Vec_IntDup( p->vGateClasses );
    if ( nFrameMax == 0 )
        iFrame0 = Gia_IterTryImprove( p, 0, 0 );
    else
        iFrame0 = nFrameMax - 1;
    while ( 1 )
    {
        int fChanges = 0;
        Gia_ManForEachObj1( p, pObj, i )
        {
            if ( pObj->fMark0 )
                continue;
            if ( !Gia_ObjIsInGla(p, pObj) )
                continue;
            if ( pObj == Gia_ObjFanin0( Gia_ManPo(p, 0) ) )
                continue;
            if ( Gia_ObjIsAnd(pObj) )
            {
                if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsInGla(p, Gia_ObjFanin1(pObj)) )
                    continue;
            }
            if ( Gia_ObjIsRo(p, pObj) )
            {
                if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj))) )
                    continue;
            }        
            clk = Abc_Clock();
            printf( "%5d : ", nTotal );
            printf( "Obj =%7d   ", i );
            Gia_ObjRemFromGla( p, pObj );
            iFrame = Gia_IterTryImprove( p, nTimeOut, iFrame0 );
            if ( nFrameMax )
                assert( iFrame <= nFrameMax );
            else
                assert( iFrame <= iFrame0 );
            printf( "Frame =%6d   ", iFrame );
            if ( iFrame < iFrame0 )
            {
                pObj->fMark0 = 1;
                Gia_ObjAddToGla( p, pObj );
                printf( "           " );
            }
            else
            {
                fChanges = 1;
                nRemoved++;
                printf( "Removing   " );
                Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 );
            }
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            nTotal++;
            // update the classes
            Vec_IntFreeP( &p->vGateClasses );
            p->vGateClasses = Vec_IntDup(vGScopy);
        }
        if ( !fChanges )
            break;
    }
    Gia_ManCleanMark0(p);
    Vec_IntFree( vGScopy );
    printf( "Tried = %d.  ",     nTotal );
    printf( "Removed = %d. (%.2f %%)  ",  nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) );
    Abc_PrintTime( 1, "Time",  Abc_Clock() - clkTotal );
    return NULL;
}

Vec_Int_t* Gia_VtaConvertFromGla	(	Gia_Man_t *	p,
		Vec_Int_t *	vGla,
		int	nFrames
	)

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

Synopsis [Converting GLA vector to VTA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file absUtil.c.

{
    Vec_Int_t * vVta;
    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
    int i, k, j, Entry, Counter, nGlaSize;
    //. get the GLA size
    nGlaSize = Vec_IntSum(vGla);
    // get the bitmask
    nObjBits = Abc_Base2Log(nObjs);
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vVta = Vec_IntAlloc( 1000 );
    Vec_IntPush( vVta, nFrames );
    Counter = nFrames + 2;
    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
        Vec_IntPush( vVta, Counter );
    for ( i = 0; i < nFrames; i++ )
        for ( k = 0; k <= i; k++ )
            Vec_IntForEachEntry( vGla, Entry, j )
                if ( Entry ) 
                    Vec_IntPush( vVta, (k << nObjBits) | j );
    Counter = Vec_IntEntry(vVta, nFrames+1);
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    return vVta;
}

Vec_Int_t* Gia_VtaConvertToGla	(	Gia_Man_t *	p,
		Vec_Int_t *	vVta
	)

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

Synopsis [Converting VTA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    Vec_Int_t * vGla;
    int nObjMask, nObjs = Gia_ManObjNum(p);
    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    // get the bitmask
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vGla = Vec_IntStart( nObjs );
    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
    {
        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
        Vec_IntAddToEntry( vGla, (Entry &  nObjMask), 1 );
    }
    Vec_IntWriteEntry( vGla, 0, nFrames );
    return vGla;
}

int Gia_VtaPerform	(	Gia_Man_t *	pAig,
		Abs_Par_t *	pPars
	)

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

Synopsis [Collect nodes/flops involved in different timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1743 of file absVta.c.

{
    int RetValue = -1;
    if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
    {
        int nFramesMaxOld = pPars->nFramesMax;
        pPars->nFramesMax = pPars->nFramesStart;
        RetValue = Gia_VtaPerformInt( pAig, pPars );
        pPars->nFramesMax = nFramesMaxOld;
    }
    if ( RetValue == 0 )
        return RetValue;
    return Gia_VtaPerformInt( pAig, pPars );
}

Vec_Int_t* Saig_ManCbaFilterFlops	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pAbsCex,
		Vec_Int_t *	vFlopClasses,
		Vec_Int_t *	vAbsFfsToAdd,
		int	nFfsToSelect
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Selects the best flops from the given array.]

Description [Selects the best 'nFfsToSelect' flops among the array 'vAbsFfsToAdd' of flops that should be added to the abstraction. To this end, this procedure simulates the original AIG (pAig) using the given CEX (pAbsCex), which was detected for the abstraction.]

SideEffects []

SeeAlso []

Definition at line 66 of file absOldCex.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
    int i, k, f, Entry, iBit, * pPerm;
    assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
    assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
    // map previously abstracted flops into their original numbers
    vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
    Vec_IntForEachEntry( vFlopClasses, Entry, i )
        if ( Entry == 0 )
            Vec_IntPush( vMapEntries, i );
    // simulate one frame at a time
    assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
    vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
    // initialize the flops
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = 0;
    for ( f = 0; f < pAbsCex->iFrame; f++ )
    {
        // override the flop values according to the cex
        iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k);
        // simulate
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        // transfer
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
        // compare
        iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) )
                Vec_IntAddToEntry( vFlopCosts, k, 1 );
    }
//    Vec_IntForEachEntry( vFlopCosts, Entry, i )
//        printf( "%d ", Entry );
//    printf( "\n" );
    // remap the cost
    vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
    Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
        Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
    // sort the flops
    pPerm = Abc_MergeSortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
    // shrink the array
    vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
    for ( i = 0; i < nFfsToSelect; i++ )
    {
//        printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
        Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
    }
//    printf( "\n" );
    // cleanup
    ABC_FREE( pPerm );
    Vec_IntFree( vMapEntries );
    Vec_IntFree( vFlopCosts );
    Vec_IntFree( vFlopAddCosts );
    Aig_ManCleanMarkB(pAig);
    // return the computed flops
    return vFfsToAddBest;
}

Abc_Cex_t* Saig_ManCbaFindCexCareBits	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex,
		int	nInputs,
		int	fVerbose
	)

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

Synopsis [SAT-based refinement of the counter-example.]

Description [The first parameter (nInputs) indicates how many first primary inputs to skip without considering as care candidates.]

SideEffects []

SeeAlso []

Definition at line 718 of file absOldCex.c.

{
    Saig_ManCba_t * p;
    Vec_Int_t * vReasons;
    Abc_Cex_t * pCare;
    abctime clk = Abc_Clock();

    clk = Abc_Clock();
    p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );

//    p->vReg2Frame = Vec_VecStart( pCex->iFrame );
//    p->vReg2Value = Vec_VecStart( pCex->iFrame );
    p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
    vReasons = Saig_ManCbaFindReason( p );
    if ( p->vReg2Frame )
        Saig_ManCbaShrink( p );


//if ( fVerbose )
//Aig_ManPrintStats( p->pFrames );

    if ( fVerbose )
    {
        Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons );
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
        Vec_IntFree( vRes );
ABC_PRT( "Time", Abc_Clock() - clk );
    }

    pCare = Saig_ManCbaReason2Cex( p, vReasons );
    Vec_IntFree( vReasons );
    Saig_ManCbaStop( p );

if ( fVerbose )
{
printf( "Real " );
Abc_CexPrintStats( pCex );
}
if ( fVerbose )
{
printf( "Care " );
Abc_CexPrintStats( pCare );
}
/*
    // verify the reduced counter-example using ternary simulation
    if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
    else if ( fVerbose )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
*/
    Aig_ManCleanMarkAB( pAig );
    return pCare;
}

Vec_Int_t* Saig_ManCexAbstractionFlops	(	Aig_Man_t *	p,
		Gia_ParAbs_t *	pPars
	)

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

Synopsis [Computes the flops to remain after abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file absOldRef.c.

{
    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;
}

Vec_Int_t* Saig_ManExtendCounterExampleTest2	(	Aig_Man_t *	p,
		int	iFirstFlopPi,
		Abc_Cex_t *	pCex,
		int	fVerbose
	)

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

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file absOldSim.c.

{
    Vec_Int_t * vRes;
    Vec_Ptr_t * vSimInfo;
    abctime clk;
    if ( Saig_ManPiNum(p) != pCex->nPis )
    {
        printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(p), pCex->nPis );
        return NULL;
    }
    Aig_ManFanoutStart( p );
    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
    Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );

clk = Abc_Clock();
    vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
    if ( fVerbose )
    {
        printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Vec_PtrFree( vSimInfo );
    Aig_ManFanoutStop( p );
    return vRes;
}

Vec_Int_t* Saig_ManExtendCounterExampleTest3	(	Aig_Man_t *	pAig,
		int	iFirstFlopPi,
		Abc_Cex_t *	pCex,
		int	fVerbose
	)

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

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 930 of file saigRefSat.c.

{
    Saig_RefMan_t * p;
    Vec_Int_t * vRes, * vReasons;
    clock_t clk;
    if ( Saig_ManPiNum(pAig) != pCex->nPis )
    {
        printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(pAig), pCex->nPis );
        return NULL;
    }

clk = clock();

    p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
    vReasons = Saig_RefManFindReason( p );
    vRes = Saig_RefManReason2Inputs( p, vReasons );

//    if ( fVerbose )
    {
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
    }

/*
    ////////////////////////////////////
    Vec_IntFree( vReasons );
    vReasons = Saig_RefManRefineWithSat( p, vRes );
    ////////////////////////////////////

    // derive new result
    Vec_IntFree( vRes );
    vRes = Saig_RefManReason2Inputs( p, vReasons );
//    if ( fVerbose )
    {
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
    }
*/

    Vec_IntFree( vReasons );
    Saig_RefManStop( p );
    return vRes;
}