absVta.c File Reference

#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
#include "abs.h"

Go to the source code of this file.

Data Structures
struct	Vta_Obj_t_
struct	Vta_Man_t_

Macros
#define	VTA_LARGE   0xFFFFFFF
#define	VTA_VAR0   1
#define	VTA_VAR1   2
#define	VTA_VARX   3
#define	Vta_ManForEachObj(p, pObj, i)   for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
#define	Vta_ManForEachObjObj(p, pObjVta, pObjGia, i)   for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define	Vta_ManForEachObjObjReverse(p, pObjVta, pObjGia, i)   for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define	Vta_ManForEachObjVec(vVec, p, pObj, i)   for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define	Vta_ManForEachObjVecReverse(vVec, p, pObj, i)   for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
#define	Vta_ManForEachObjObjVec(vVec, p, pObj, pObjG, i)   for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
#define	Vta_ManForEachObjObjVecReverse(vVec, p, pObj, pObjG, i)   for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )

Typedefs
typedef struct Vta_Obj_t_	Vta_Obj_t
	DECLARATIONS ///. More...
typedef struct Vta_Man_t_	Vta_Man_t

Functions
static int	Vta_ValIs0 (Vta_Obj_t *pThis, int fCompl)
static int	Vta_ValIs1 (Vta_Obj_t *pThis, int fCompl)
static Vta_Obj_t *	Vta_ManObj (Vta_Man_t *p, int i)
static int	Vta_ObjId (Vta_Man_t *p, Vta_Obj_t *pObj)
void	Vga_ManAddClausesOne (Vta_Man_t *p, int iObj, int iFrame)
Vec_Ptr_t *	Gia_VtaAbsToFrames (Vec_Int_t *vAbs)
	FUNCTION DEFINITIONS ///. More...
Vec_Int_t *	Gia_VtaFramesToAbs (Vec_Vec_t *vFrames)
static Vec_Int_t *	Vta_ManDeriveAbsAll (Vec_Int_t *p, int nWords)
int	Vec_IntDoubleWidth (Vec_Int_t *p, int nWords)
static int	Vga_ManHash (int iObj, int iFrame, int nBins)
static int *	Vga_ManLookup (Vta_Man_t *p, int iObj, int iFrame)
static Vta_Obj_t *	Vga_ManFind (Vta_Man_t *p, int iObj, int iFrame)
static Vta_Obj_t *	Vga_ManFindOrAdd (Vta_Man_t *p, int iObj, int iFrame)
static void	Vga_ManDelete (Vta_Man_t *p, int iObj, int iFrame)
Abc_Cex_t *	Vga_ManDeriveCex (Vta_Man_t *p)
void	Vta_ManUnsatCoreRemap (Vta_Man_t *p, Vec_Int_t *vCore)
int	Vta_ManComputeDepthIncrease (Vta_Obj_t **pp1, Vta_Obj_t **pp2)
int	Vta_ManObjIsUsed (Vta_Man_t *p, int iObj)
static void	Vta_ObjPreds (Vta_Man_t *p, Vta_Obj_t *pThis, Gia_Obj_t *pObj, Vta_Obj_t **ppThis0, Vta_Obj_t **ppThis1)
void	Vta_ManCollectNodes_rec (Vta_Man_t *p, Vta_Obj_t *pThis, Vec_Int_t *vOrder)
Vec_Int_t *	Vta_ManCollectNodes (Vta_Man_t *p, int f)
void	Vta_ManSatVerify (Vta_Man_t *p)
void	Vta_ManProfileAddition (Vta_Man_t *p, Vec_Int_t *vTermsToAdd)
Abc_Cex_t *	Vta_ManRefineAbstraction (Vta_Man_t *p, int f)
Vta_Man_t *	Vga_ManStart (Gia_Man_t *pGia, Abs_Par_t *pPars)
void	Vga_ManStop (Vta_Man_t *p)
static int	Vga_ManGetOutLit (Vta_Man_t *p, int f)
Vec_Int_t *	Vta_ManUnsatCore (int iLit, sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue, int *pnConfls)
int	Vta_ManAbsPrintFrame (Vta_Man_t *p, Vec_Int_t *vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose)
void	Vga_ManLoadSlice (Vta_Man_t *p, Vec_Int_t *vOne, int Lift)
void	Vga_ManPrintCore (Vta_Man_t *p, Vec_Int_t *vCore, int Lift)
void	Vga_ManRollBack (Vta_Man_t *p, int nObjOld)
void	Gia_VtaSendAbsracted (Vta_Man_t *p, int fVerbose)
void	Gia_VtaSendCancel (Vta_Man_t *p, int fVerbose)
void	Gia_VtaDumpAbsracted (Vta_Man_t *p, int fVerbose)
void	Gia_VtaPrintMemory (Vta_Man_t *p)
int	Gia_VtaPerformInt (Gia_Man_t *pAig, Abs_Par_t *pPars)
int	Gia_VtaPerform (Gia_Man_t *pAig, Abs_Par_t *pPars)

Macro Definition Documentation

#define VTA_LARGE   0xFFFFFFF

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

FileName [absVta.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Variable time-frame abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 27 of file absVta.c.

#define Vta_ManForEachObj	(		p,
			pObj,
			i
	)		for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )

Definition at line 107 of file absVta.c.

#define Vta_ManForEachObjObj	(		p,
			pObjVta,
			pObjGia,
			i
	)		for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

Definition at line 109 of file absVta.c.

#define Vta_ManForEachObjObjReverse	(		p,
			pObjVta,
			pObjGia,
			i
	)		for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

Definition at line 111 of file absVta.c.

#define Vta_ManForEachObjObjVec	(		vVec,
			p,
			pObj,
			pObjG,
			i
	)		for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )

Definition at line 119 of file absVta.c.

#define Vta_ManForEachObjObjVecReverse	(		vVec,
			p,
			pObj,
			pObjG,
			i
	)		for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )

Definition at line 121 of file absVta.c.

#define Vta_ManForEachObjVec	(		vVec,
			p,
			pObj,
			i
	)		for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )

Definition at line 114 of file absVta.c.

#define Vta_ManForEachObjVecReverse	(		vVec,
			p,
			pObj,
			i
	)		for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )

Definition at line 116 of file absVta.c.

#define VTA_VAR0   1

Definition at line 83 of file absVta.c.

#define VTA_VAR1   2

Definition at line 84 of file absVta.c.

#define VTA_VARX   3

Definition at line 85 of file absVta.c.

Typedef Documentation

typedef struct Vta_Man_t_ Vta_Man_t

Definition at line 45 of file absVta.c.

typedef struct Vta_Obj_t_ Vta_Obj_t

DECLARATIONS ///.

Definition at line 33 of file absVta.c.

Function Documentation

Vec_Ptr_t* Gia_VtaAbsToFrames

(

Vec_Int_t *

vAbs

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Converting from one array to per-frame arrays.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file absVta.c.

{
    Vec_Ptr_t * vFrames;
    Vec_Int_t * vFrame;
    int i, k, Entry, iStart, iStop = -1;
    int nFrames = Vec_IntEntry( vAbs, 0 );
    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
    vFrames = Vec_PtrAlloc( nFrames );
    for ( i = 0; i < nFrames; i++ )
    {
        iStart = Vec_IntEntry( vAbs, i+1 );
        iStop  = Vec_IntEntry( vAbs, i+2 );
        vFrame = Vec_IntAlloc( iStop - iStart );
        Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
            Vec_IntPush( vFrame, Entry );
        Vec_PtrPush( vFrames, vFrame );
    }
    assert( iStop == Vec_IntSize(vAbs) );
    return vFrames;
}

void Gia_VtaDumpAbsracted	(	Vta_Man_t *	p,
		int	fVerbose
	)

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1424 of file absVta.c.

{
    char * pFileNameDef = "vabs.aig";
    char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
    Gia_Man_t * pAbs;
    if ( fVerbose )
        Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
    // create obj classes
    Vec_IntFreeP( &p->pGia->vObjClasses );
    p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
    // create gate classes
    Vec_IntFreeP( &p->pGia->vGateClasses );
    p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
    Vec_IntFreeP( &p->pGia->vObjClasses );
    // create abstrated model
    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
    Vec_IntFreeP( &p->pGia->vGateClasses );
    // send it out
    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
    Gia_ManStop( pAbs );
}

Vec_Int_t* Gia_VtaFramesToAbs

(

Vec_Vec_t *

vFrames

)

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

Synopsis [Converting from per-frame arrays to one integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file absVta.c.

{
    Vec_Int_t * vOne, * vAbs;
    int i, k, Entry, nSize;
    vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) );
    Vec_IntPush( vAbs, Vec_VecSize(vFrames) );
    nSize = Vec_VecSize(vFrames) + 2;
    Vec_VecForEachLevelInt( vFrames, vOne, i )
    {
        Vec_IntPush( vAbs, nSize );
        nSize += Vec_IntSize( vOne );
    }
    Vec_IntPush( vAbs, nSize );
    assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 );
    Vec_VecForEachLevelInt( vFrames, vOne, i )
        Vec_IntForEachEntry( vOne, Entry, k )
            Vec_IntPush( vAbs, Entry );
    assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) );
    return vAbs;
}

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

int Gia_VtaPerformInt	(	Gia_Man_t *	pAig,
		Abs_Par_t *	pPars
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1492 of file absVta.c.

{
    Vta_Man_t * p;
    Vec_Int_t * vCore;
    Abc_Cex_t * pCex = NULL;
    int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
    abctime clk = Abc_Clock(), clk2;
    // 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->vObjClasses == NULL )
    {
        pAig->vObjClasses = Vec_IntAlloc( 5 );
        Vec_IntPush( pAig->vObjClasses, 1 );
        Vec_IntPush( pAig->vObjClasses, 3 );
        Vec_IntPush( pAig->vObjClasses, 4 );
        Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
    }
    // start the manager
    p = Vga_ManStart( pAig, pPars );
    // 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 variable-timeframe abstraction (VTA) with the following parameters:\n" );
        Abc_Print( 1, "FramePast = %d  FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%\n", 
            pPars->nFramesPast, 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   %%   Confl  Cex    SatVar   Core   F0   F1   F2  ...\n" );
        Abc_Print( 1, " Frame   %%   Abs   %%   Confl  Cex   Vars   Clas   Lrns   Core     Time      Mem\n" );
    }
    assert( Vec_PtrSize(p->vFrames) > 0 );
    for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
    {
        int nConflsBeg = sat_solver2_nconflicts(p->pSat);
        p->pPars->iFrame = f;
        // realloc storage for abstraction marks
        if ( f == p->nWords * 32 )
            p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );

        // create bookmark to be used for rollback
        nObjOld = p->nObjs;
        sat_solver2_bookmark( p->pSat );
        Vec_IntClear( p->vAddedNew );

        // load new timeframe
        Vga_ManAddClausesOne( p, 0, f );
        if ( f < Vec_PtrSize(p->vFrames) )
            Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
        else
        {
            for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
                Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
        }

        // iterate as long as there are counter-examples
        for ( i = 0; ; i++ )
        { 
            clk2 = Abc_Clock();
            vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
            assert( (vCore != NULL) == (Status == 1) );
            if ( Status == -1 ) // resource limit is reached
            {
                Vga_ManRollBack( p, nObjOld );
                goto finish;
            }
            // check timeout
            if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit )
            {
                Vga_ManRollBack( p, nObjOld );
                goto finish;
            }
            if ( vCore != NULL )
            {
                p->timeUnsat += Abc_Clock() - clk2;
                break;
            }
            p->timeSat += Abc_Clock() - clk2;
            assert( Status == 0 );
            p->nCexes++;
            // perform the refinement
            clk2 = Abc_Clock();
            pCex = Vta_ManRefineAbstraction( p, f );
            p->timeCex += Abc_Clock() - clk2;
            if ( pCex != NULL )
                goto finish;
            // print the result (do not count it towards change)
            Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose );
        }
        assert( Status == 1 );
        // valid core is obtained
        Vta_ManUnsatCoreRemap( p, vCore );
        Vec_IntSort( vCore, 1 );
        // update the SAT solver
        sat_solver2_rollback( p->pSat );
        // update storage
        Vga_ManRollBack( p, nObjOld );
        // load this timeframe
        Vga_ManLoadSlice( p, vCore, 0 );
        Vec_IntFree( vCore );

        // run SAT solver
        clk2 = Abc_Clock();
        vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
        p->timeUnsat += Abc_Clock() - clk2;
        assert( (vCore != NULL) == (Status == 1) );
        if ( Status == -1 ) // resource limit is reached
            break;
        if ( Status == 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;
        }
        // add the core
        Vta_ManUnsatCoreRemap( p, vCore );
        // add in direct topological order
        Vec_IntSort( vCore, 1 );
        Vec_PtrPush( p->vCores, vCore );
        // print the result
        if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) )
        {
            // reset the counter of frames without change
            nCountNoChange = 1;
            p->pPars->nFramesNoChange = 0;
        }
        else if ( ++nCountNoChange == 2 ) // time to send
        {
            p->pPars->nFramesNoChange++;
            if ( Abc_FrameIsBridgeMode() )
            {
                // cancel old one if it was sent
                if ( fOneIsSent )
                    Gia_VtaSendCancel( p, pPars->fVerbose );
                // send new one 
                Gia_VtaSendAbsracted( p, pPars->fVerbose );
                fOneIsSent = 1;
            }
        }
        // dump the model
        if ( p->pPars->fDumpVabs && (f & 1) )
        {
            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 : "vtabs.aig"), ".status") );
            Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
            Gia_VtaDumpAbsracted( p, pPars->fVerbose );
        }
        // check if the number of objects is below limit
        if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
        {
            Status = -1;
            break;
        }
    }
finish:
    // analize the results
    if ( pCex == NULL )
    {
        if ( p->pPars->fVerbose && Status == -1 )
            printf( "\n" );
        if ( Vec_PtrSize(p->vCores) == 0 )
            Abc_Print( 1, "Abstraction is not produced because first frame is not solved.  " );
        else
        {
            assert( Vec_PtrSize(p->vCores) > 0 );
//            if ( pAig->vObjClasses != NULL )
//                Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
            Vec_IntFreeP( &pAig->vObjClasses );
            pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
            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 ( p->nSeenGla >= Gia_ManCandNum(pAig) * (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, "VTA completed %d frames with a %d-stable abstraction.  ", f, p->pPars->nFramesNoChange );
            }
        }
    }
    else
    {
        if ( p->pPars->fVerbose )
            printf( "\n" );
        ABC_FREE( p->pGia->pCexSeq );
        p->pGia->pCexSeq = pCex;
        if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
            Abc_Print( 1, "    Gia_VtaPerform(): CEX verification has failed!\n" );
        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = pCex->iFrame - 1;
        Vec_IntFreeP( &pAig->vObjClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
        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 );
        Gia_VtaPrintMemory( p );
    }

    Vga_ManStop( p );
    fflush( stdout );
    return RetValue;
}

void Gia_VtaPrintMemory

(

Vta_Man_t *

p

)

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

Synopsis [Print memory report.]

Description []

SideEffects []

SeeAlso []

Definition at line 1458 of file absVta.c.

{
    double memTot = 0;
    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
    double memSat = sat_solver2_memory( p->pSat, 1 );
    double memPro = sat_solver2_memory_proof( p->pSat );
    double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
    double memOth = sizeof(Vta_Man_t);
    memOth += Vec_IntCap(p->vOrder) * sizeof(int);
    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
    memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
    memTot = memAig + memSat + memPro + memMap + memOth;
    ABC_PRMP( "Memory: AIG     ", memAig, memTot );
    ABC_PRMP( "Memory: SAT     ", memSat, memTot );
    ABC_PRMP( "Memory: Proof   ", memPro, memTot );
    ABC_PRMP( "Memory: Map     ", memMap, memTot );
    ABC_PRMP( "Memory: Other   ", memOth, memTot );
    ABC_PRMP( "Memory: TOTAL   ", memTot, memTot );
}

void Gia_VtaSendAbsracted	(	Vta_Man_t *	p,
		int	fVerbose
	)

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1384 of file absVta.c.

{
    Gia_Man_t * pAbs;
    assert( Abc_FrameIsBridgeMode() );
//    if ( fVerbose )
//        Abc_Print( 1, "Sending abstracted model...\n" );
    // create obj classes
    Vec_IntFreeP( &p->pGia->vObjClasses );
    p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
    // create gate classes
    Vec_IntFreeP( &p->pGia->vGateClasses );
    p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
    Vec_IntFreeP( &p->pGia->vObjClasses );
    // create abstrated model
    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
    Vec_IntFreeP( &p->pGia->vGateClasses );
    // send it out
    Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
    Gia_ManStop( pAbs );
}

void Gia_VtaSendCancel	(	Vta_Man_t *	p,
		int	fVerbose
	)

Definition at line 1404 of file absVta.c.

{
    extern int Gia_ManToBridgeBadAbs( FILE * pFile );
    assert( Abc_FrameIsBridgeMode() );
//    if ( fVerbose )
//        Abc_Print( 1, "Cancelling previously sent model...\n" );
    Gia_ManToBridgeBadAbs( stdout );
}

int Vec_IntDoubleWidth	(	Vec_Int_t *	p,
		int	nWords
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file absVta.c.

{
    int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 );
    int i, w, nObjs = Vec_IntSize(p) / nWords;
    assert( Vec_IntSize(p) % nWords == 0 );
    for ( i = 0; i < nObjs; i++ )
        for ( w = 0; w < nWords; w++ )
            pArray[2 * nWords * i + w] = p->pArray[nWords * i + w];
    ABC_FREE( p->pArray );
    p->pArray = pArray;
    p->nSize *= 2;
    p->nCap = p->nSize;
    return 2 * nWords;
}

void Vga_ManAddClausesOne	(	Vta_Man_t *	p,
		int	iObj,
		int	iFrame
	)

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1254 of file absVta.c.

{ 
    Vta_Obj_t * pThis0, * pThis1;
    Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
    Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
    int iThis0, iMainVar = Vta_ObjId(p, pThis);
    assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
    if ( pThis->fAdded )
        return;
    pThis->fAdded = 1;
    Vec_IntPush( p->vAddedNew, iMainVar );
    if ( Gia_ObjIsAnd(pObj) )
    {
        pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
        iThis0 = Vta_ObjId(p, pThis0);
        pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
        sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), 
            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
    }
    else if ( Gia_ObjIsRo(p->pGia, pObj) )
    {
        if ( iFrame == 0 )
        {
            if ( p->pPars->fUseTermVars )
            {
                pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
                sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
            }
            else
            {
                sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
            }
        }
        else
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
            pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
            sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );  
        }
    }
    else if ( Gia_ObjIsConst0(pObj) )
    {
        sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
    }
    else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
        assert( 0 );
}

static void Vga_ManDelete ( Vta_Man_t *  p, int  iObj, int  iFrame  )

inlinestatic

Definition at line 321 of file absVta.c.

{
    int * pPlace = Vga_ManLookup( p, iObj, iFrame );
    Vta_Obj_t * pThis = Vta_ManObj(p, *pPlace);
    assert( pThis != NULL );
    *pPlace = pThis->iNext;
    pThis->iNext = -1;
}

Abc_Cex_t* Vga_ManDeriveCex

(

Vta_Man_t *

p

)

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

Synopsis [Derives counter-example using current assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file absVta.c.

{
    Abc_Cex_t * pCex;
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    int i;
    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
    pCex->iPo = 0;
    pCex->iFrame = p->pPars->iFrame;
    Vta_ManForEachObjObj( p, pThis, pObj, i )
        if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
    return pCex;
}

static Vta_Obj_t* Vga_ManFind ( Vta_Man_t *  p, int  iObj, int  iFrame  )

inlinestatic

Definition at line 284 of file absVta.c.

{
    int * pPlace = Vga_ManLookup( p, iObj, iFrame );
    return Vta_ManObj(p, *pPlace);
}

static Vta_Obj_t* Vga_ManFindOrAdd ( Vta_Man_t *  p, int  iObj, int  iFrame  )

inlinestatic

Definition at line 289 of file absVta.c.

{
    Vta_Obj_t * pThis;
    int i, * pPlace;
    assert( iObj >= 0 && iFrame >= -1 );
    if ( p->nObjs == p->nObjsAlloc )
    {
        // resize objects
        p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
        memset( p->pObjs + p->nObjsAlloc, 0, p->nObjsAlloc * sizeof(Vta_Obj_t) );
        p->nObjsAlloc *= 2;
        // rehash entries in the table
        ABC_FREE( p->pBins );
        p->nBins = Abc_PrimeCudd( 2 * p->nBins );
        p->pBins = ABC_CALLOC( int, p->nBins );
        Vta_ManForEachObj( p, pThis, i )
        {
            pThis->iNext = 0;
            pPlace = Vga_ManLookup( p, pThis->iObj, pThis->iFrame );
            assert( *pPlace == 0 );
            *pPlace = i;
        }
    }
    pPlace = Vga_ManLookup( p, iObj, iFrame );
    if ( *pPlace )
        return Vta_ManObj(p, *pPlace);
    *pPlace = p->nObjs++;
    pThis = Vta_ManObj(p, *pPlace);
    pThis->iObj   = iObj;
    pThis->iFrame = iFrame;
    return pThis;
}

static int Vga_ManGetOutLit ( Vta_Man_t *  p, int  f  )

inlinestatic

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

Synopsis [Returns the output literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 1062 of file absVta.c.

{
    Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
    Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
    assert( pThis != NULL && pThis->fAdded );
    if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
        return -Vta_ObjId(p, pThis);
    return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
} 

static int Vga_ManHash ( int  iObj, int  iFrame, int  nBins  )

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file absVta.c.

{
    return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
}

void Vga_ManLoadSlice	(	Vta_Man_t *	p,
		Vec_Int_t *	vOne,
		int	Lift
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1313 of file absVta.c.

{
    int i, Entry;
    Vec_IntForEachEntry( vOne, Entry, i )
        Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
    sat_solver2_simplify( p->pSat );
}

static int* Vga_ManLookup ( Vta_Man_t *  p, int  iObj, int  iFrame  )

inlinestatic

Definition at line 273 of file absVta.c.

{
    Vta_Obj_t * pThis;
    int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins );
    for ( pThis = Vta_ManObj(p, *pPlace); 
          pThis;  pPlace = &pThis->iNext, 
          pThis = Vta_ManObj(p, *pPlace) )
        if ( pThis->iObj == iObj && pThis->iFrame == iFrame )
            break;
    return pPlace;
}

void Vga_ManPrintCore	(	Vta_Man_t *	p,
		Vec_Int_t *	vCore,
		int	Lift
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1332 of file absVta.c.

{
    int i, Entry, iObj, iFrame;
    Vec_IntForEachEntry( vCore, Entry, i )
    {
        iObj   = (Entry &  p->nObjMask);
        iFrame = (Entry >> p->nObjBits);
        Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
    }
    Abc_Print( 1, "\n" );
}

void Vga_ManRollBack	(	Vta_Man_t *	p,
		int	nObjOld
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1355 of file absVta.c.

{
    Vta_Obj_t * pThis  = p->pObjs + nObjOld;
    Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
    int i, Entry;
    for ( ; pThis < pLimit; pThis++ )
        Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
    memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
    p->nObjs = nObjOld;
    Vec_IntForEachEntry( p->vAddedNew, Entry, i )
        if ( Entry < p->nObjs )
        {
            pThis = Vta_ManObj(p, Entry);
            assert( pThis->fAdded == 1 );
            pThis->fAdded = 0;
        }
}

Vta_Man_t* Vga_ManStart	(	Gia_Man_t *	pGia,
		Abs_Par_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 983 of file absVta.c.

{
    Vta_Man_t * p;
    p = ABC_CALLOC( Vta_Man_t, 1 );
    p->pGia        = pGia;
    p->pPars       = pPars;
    // internal data
    p->nObjsAlloc  = (1 << 18);
    p->pObjs       = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
    p->nObjs       = 1;
    p->nBins       = Abc_PrimeCudd( 2*p->nObjsAlloc );
    p->pBins       = ABC_CALLOC( int, p->nBins );
    p->vOrder      = Vec_IntAlloc( 1013 );
    // abstraction
    p->nObjBits    = Abc_Base2Log( Gia_ManObjNum(pGia) );
    p->nObjMask    = (1 << p->nObjBits) - 1;
    assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
    p->nWords      = 1;
    p->vSeens      = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
    p->vSeenGla    = Vec_BitStart( Gia_ManObjNum(pGia) );
    p->nSeenGla    = 1;
    p->nSeenAll    = 1;
    // other data
    p->vCores      = Vec_PtrAlloc( 100 );
    p->pSat        = sat_solver2_new();
    p->pSat->pPrf1 = Vec_SetAlloc( 20 );
//    p->pSat->fVerbose = p->pPars->fVerbose;
//    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
    p->pSat->nLearntStart = p->pPars->nLearnedStart;
    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
    p->pSat->nLearntMax   = p->pSat->nLearntStart;
    // start the abstraction
    assert( pGia->vObjClasses != NULL );
    p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
    p->vAddedNew   = Vec_IntAlloc( 1000 );
    return p;
}

void Vga_ManStop

(

Vta_Man_t *

p

)

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

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1033 of file absVta.c.

{
    if ( p->pPars->fVerbose )
        Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  Objs+ = %d\n", 
            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), 
            sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
    Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
    Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
    Vec_BitFreeP( &p->vSeenGla );
    Vec_IntFreeP( &p->vSeens );
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vAddedNew );
    sat_solver2_delete( p->pSat );
    ABC_FREE( p->pBins );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

int Vta_ManAbsPrintFrame	(	Vta_Man_t *	p,
		Vec_Int_t *	vCore,
		int	nFrames,
		int	nConfls,
		int	nCexes,
		abctime	Time,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1143 of file absVta.c.

{
    unsigned * pInfo;
    int * pCountAll = NULL, * pCountUni = NULL;
    int i, iFrame, iObj, Entry, fChanges = 0;
    // print info about frames
    if ( vCore )
    {
        pCountAll = ABC_CALLOC( int, nFrames + 1 );
        pCountUni = ABC_CALLOC( int, nFrames + 1 );
        Vec_IntForEachEntry( vCore, Entry, i )
        {
            iObj   = (Entry &  p->nObjMask);
            iFrame = (Entry >> p->nObjBits);
            assert( iFrame < nFrames );
            pInfo  = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
            if ( !Abc_InfoHasBit(pInfo, iFrame) )
            {
                Abc_InfoSetBit( pInfo, iFrame );
                pCountUni[iFrame+1]++;
                pCountUni[0]++;
                p->nSeenAll++;
            }
            pCountAll[iFrame+1]++;
            pCountAll[0]++;
            if ( !Vec_BitEntry(p->vSeenGla, iObj) )
            {
                Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
                p->nSeenGla++;
                fChanges = 1;
            }
        }
    }
    if ( !fVerbose )
    {
        ABC_FREE( pCountAll );
        ABC_FREE( pCountUni );
        return fChanges;
    }

    if ( Abc_FrameIsBatchMode() && !vCore )
        return fChanges;

//    Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] ); 
    Abc_Print( 1, "%4d :", nFrames-1 );
    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) ); 
    Abc_Print( 1, "%6d", p->nSeenGla ); 
    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) ); 
    Abc_Print( 1, "%8d", nConfls );
    if ( nCexes == 0 )
        Abc_Print( 1, "%5c", '-' ); 
    else
        Abc_Print( 1, "%5d", nCexes ); 
//    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
    if ( vCore == NULL )
    {
        Abc_Print( 1, "    ..." ); 
//        for ( k = 0; k < 7; k++ )
//            Abc_Print( 1, "     " );
        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
        Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
        Abc_Print( 1, "\r" );
    }
    else
    {
        Abc_PrintInt( pCountAll[0] );
/*
        if ( nFrames > 7 )
        {
            for ( k = 0; k < 3; k++ )
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
            Abc_Print( 1, "  ..." );
            for ( k = nFrames-3; k < nFrames; k++ )
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
        }
        else
        {
            for ( k = 0; k < nFrames; k++ )
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
            for ( k = nFrames; k < 7; k++ )
                Abc_Print( 1, "     " );
        }
*/
        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
        Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
        Abc_Print( 1, "\n" );
    }
    fflush( stdout );

    if ( vCore )
    {
        ABC_FREE( pCountAll );
        ABC_FREE( pCountUni );
    }
    return fChanges;
}

Vec_Int_t* Vta_ManCollectNodes	(	Vta_Man_t *	p,
		int	f
	)

Definition at line 487 of file absVta.c.

{
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    Vec_IntClear( p->vOrder );
    pObj = Gia_ManPo( p->pGia, 0 );
    pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
    assert( pThis != NULL );
    assert( !pThis->fVisit );
    Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
    assert( pThis->fVisit );
    return p->vOrder;
}

void Vta_ManCollectNodes_rec	(	Vta_Man_t *	p,
		Vta_Obj_t *	pThis,
		Vec_Int_t *	vOrder
	)

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

Synopsis [Collect const/PI/RO/AND in a topological order.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file absVta.c.

{
    Gia_Obj_t * pObj;
    Vta_Obj_t * pThis0, * pThis1;
    if ( pThis->fVisit )
        return;
    pThis->fVisit = 1;
    pObj = Gia_ManObj( p->pGia, pThis->iObj );
    if ( pThis->fAdded )
    {
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
        if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
    }
    Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
}

int Vta_ManComputeDepthIncrease	(	Vta_Obj_t **	pp1,
		Vta_Obj_t **	pp2
	)

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

Synopsis [Compares two objects by their distance.]

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file absVta.c.

{
    int Diff = (*pp1)->Prio - (*pp2)->Prio;
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    Diff = (*pp1) - (*pp2);
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    return 0; 
}

static Vec_Int_t* Vta_ManDeriveAbsAll ( Vec_Int_t *  p, int  nWords  )

inlinestatic

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

Synopsis [Detects how many frames are completed.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file absVta.c.

{
    Vec_Int_t * vRes;
    unsigned * pThis;
    int i, w, nObjs = Vec_IntSize(p) / nWords;
    assert( Vec_IntSize(p) % nWords == 0 );
    vRes = Vec_IntAlloc( nObjs );
    for ( i = 0; i < nObjs; i++ )
    {
        pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
        for ( w = 0; w < nWords; w++ )
            if ( pThis[w] )
                break;
        Vec_IntPush( vRes, (int)(w < nWords) );
    }
    return vRes;
}

static Vta_Obj_t* Vta_ManObj ( Vta_Man_t *  p, int  i  )

inlinestatic

Definition at line 104 of file absVta.c.

{ assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                     }

int Vta_ManObjIsUsed	(	Vta_Man_t *	p,
		int	iObj
	)

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

Synopsis [Returns 1 if the object is already used.]

Description []

SideEffects []

SeeAlso []

Definition at line 417 of file absVta.c.

{
    int i;
    unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
    for ( i = 0; i < p->nWords; i++ )
        if ( pInfo[i] )
            return 1;
    return 0;
}

void Vta_ManProfileAddition	(	Vta_Man_t *	p,
		Vec_Int_t *	vTermsToAdd
	)

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 557 of file absVta.c.

{
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    // profile the added ones
    int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
    Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
        pCounters[pThis->iFrame]++;
    for ( i = 0; i <= p->pPars->iFrame; i++ )
        Abc_Print( 1, "%2d", pCounters[i] );
    Abc_Print( 1, "***\n" );
}

Abc_Cex_t* Vta_ManRefineAbstraction	(	Vta_Man_t *	p,
		int	f
	)

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file absVta.c.

{
    int fVerify = 0;
    Abc_Cex_t * pCex = NULL;
    Vec_Int_t * vOrder, * vTermsToAdd;
    Vec_Ptr_t * vTermsUsed, * vTermsUnused;
    Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
    Gia_Obj_t * pObj;
    int i, Counter;

    if ( fVerify )
    Vta_ManSatVerify( p );

    // collect nodes in a topological order
    vOrder = Vta_ManCollectNodes( p, f );
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
    {
        pThis->Prio = VTA_LARGE;
        pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
        pThis->fVisit = 0;
    }

    // verify
    if ( fVerify )
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
    {
        if ( !pThis->fAdded )
            continue;
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
            if ( pThis->iFrame == 0 )
                assert( pThis->Value == VTA_VAR0 );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
            else if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
            else assert( 0 );
        }
    }

    // compute distance in reverse order
    pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
    pThis->Prio  = 1;
    // collect used and unused terms
    vTermsUsed   = Vec_PtrAlloc( 1015 );
    vTermsUnused = Vec_PtrAlloc( 1016 );
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
    {
        // there is no unreachable states
        assert( pThis->Prio < VTA_LARGE );
        // skip constants and PIs
        if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
        {
            pThis->Prio = 0; // set highest priority
            continue;
        }
        // collect terminals
        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
        if ( !pThis->fAdded )
        {
            assert( pThis->Prio > 0 );
            if ( Vta_ManObjIsUsed(p, pThis->iObj) )
                Vec_PtrPush( vTermsUsed, pThis );
            else
                Vec_PtrPush( vTermsUnused, pThis );
            continue;
        }
        // propagate
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( pThis0 ) 
            pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
        if ( pThis1 ) 
            pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
    }

/*
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
        if ( pThis->Prio > 0 )
            pThis->Prio = 10;
*/
/*
    // update priorities according to reconvergence counters
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
    {
        Vta_Obj_t * pThis0, * pThis1;
        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        pThis->Prio += 10000000;
        if ( pThis0 )
            pThis->Prio -= 1000000 * pThis0->fAdded;
        if ( pThis1 )
            pThis->Prio -= 1000000 * pThis1->fAdded;
    }
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
    {
        Vta_Obj_t * pThis0, * pThis1;
        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        pThis->Prio += 10000000;
        if ( pThis0 )
            pThis->Prio -= 1000000 * pThis0->fAdded;
        if ( pThis1 )
            pThis->Prio -= 1000000 * pThis1->fAdded;
    }
*/


    // update priorities according to reconvergence counters
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        pThis->Prio = pThis->iObj;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
        pThis->Prio = pThis->iObj;


    // objects with equal distance should receive priority based on number
    // those objects whose prototypes have been added in other timeframes
    // should have higher priority than the current object
    Vec_PtrSort( vTermsUsed,   (int (*)(void))Vta_ManComputeDepthIncrease );
    Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
    if ( Vec_PtrSize(vTermsUsed) > 1 )
    {
        pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
        pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
        assert( pThis0->Prio <= pThis1->Prio );
    }
    // assign the priority based on these orders
    Counter = 1;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        pThis->Prio = Counter++;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
        pThis->Prio = Counter++;
//    Abc_Print( 1, "Used %d  Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );


    // propagate in the direct order
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
    {
        assert( pThis->fVisit == 0 );
        assert( pThis->Prio < VTA_LARGE );
        // skip terminal objects
        if ( !pThis->fAdded )
            continue;
        // assumes that values are assigned!!!
        assert( pThis->Value != 0 );
        // propagate
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( pThis->Value == VTA_VAR1 )
            {
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
                pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
            }
            else if ( pThis->Value == VTA_VAR0 )
            {
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                    pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
                else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Prio = pThis0->Prio;
                else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                    pThis->Prio = pThis1->Prio;
                else assert( 0 );
            }
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
                pThis->Prio = pThis0->Prio;
            }
            else
                pThis->Prio = 0;
        }
        else if ( Gia_ObjIsConst0(pObj) )
            pThis->Prio = 0;
        else
            assert( 0 );
    }

    // select important values
    pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
    pTop->fVisit = 1;
    vTermsToAdd = Vec_IntAlloc( 100 );
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
    {
        if ( !pThis->fVisit )
            continue;
        pThis->fVisit = 0;
        assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
        // skip terminal objects
        if ( !pThis->fAdded )
        {
            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
            Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
            continue;
        }
        // assumes that values are assigned!!!
        assert( pThis->Value != 0 );
        // propagate
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( pThis->Value == VTA_VAR1 )
            {
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
                assert( pThis0->Prio <= pThis->Prio );
                assert( pThis1->Prio <= pThis->Prio );
                pThis0->fVisit = 1;
                pThis1->fVisit = 1;
            }
            else if ( pThis->Value == VTA_VAR0 )
            {
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                {
                    if ( pThis0->fVisit )
                    {
                    }
                    else if ( pThis1->fVisit )
                    {
                    }
                    else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
                    {
                        pThis0->fVisit = 1;
                        assert( pThis0->Prio == pThis->Prio );
                    }
                    else
                    {
                        pThis1->fVisit = 1;
                        assert( pThis1->Prio == pThis->Prio );
                    }
                }
                else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                {
                    pThis0->fVisit = 1;
                    assert( pThis0->Prio == pThis->Prio );
                }
                else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                {
                    pThis1->fVisit = 1;
                    assert( pThis1->Prio == pThis->Prio );
                }
                else assert( 0 );
            }
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
                pThis0->fVisit = 1;
                assert( pThis0->Prio == pThis->Prio );
            }
        }
        else if ( !Gia_ObjIsConst0(pObj) )
            assert( 0 );
    }

    if ( p->pPars->fAddLayer )
    {
        // mark those currently included
        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
        {
            assert( pThis->fVisit == 0 );
            pThis->fVisit = 1;
        }
        // add used terms, which have close relationship
        Counter = Vec_IntSize(vTermsToAdd);
        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        {
            if ( pThis->fVisit )
                continue;
    //        Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
    //        if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
                Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
        }
        // remove those currenty included
        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
            pThis->fVisit = 0;
    }
//    printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
//Vec_IntReverseOrder( vTermsToAdd );
//Vec_IntSort( vTermsToAdd, 1 );


    // cleanup
    Vec_PtrFree( vTermsUsed );
    Vec_PtrFree( vTermsUnused );


    if ( fVerify )
    {
    // verify
    Vta_ManForEachObjVec( vOrder, p, pThis, i )
        pThis->Value = VTA_VARX;
    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
    {
        assert( !pThis->fAdded );
        pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
    }
    // simulate 
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
    {
        assert( pThis->fVisit == 0 );
        if ( !pThis->fAdded )
            continue;
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
                pThis->Value = VTA_VAR1;
            else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                pThis->Value = VTA_VAR0;
            else
                pThis->Value = VTA_VARX;
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Value = VTA_VAR0;
                else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Value = VTA_VAR1;
                else
                    pThis->Value = VTA_VARX;
            }
            else
            {
                pThis->Value = VTA_VAR0;
            }
        }
        else if ( Gia_ObjIsConst0(pObj) )
        {
            pThis->Value = VTA_VAR0;
        }
        else assert( 0 );
        // double check the solver
        assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
    }

    // check the output
    if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
        Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
//    else
//        Abc_Print( 1, "Verification OK.\n" );
    }


    // produce true counter-example
    if ( pTop->Prio == 0 )
        pCex = Vga_ManDeriveCex( p );
    else
    {
//       Vta_ManProfileAddition( p, vTermsToAdd );

        Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
            if ( !Gia_ObjIsPi(p->pGia, pObj) )
                Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
        sat_solver2_simplify( p->pSat );
    }
    p->nObjAdded += Vec_IntSize(vTermsToAdd);
    Vec_IntFree( vTermsToAdd );
    return pCex;
}

void Vta_ManSatVerify

(

Vta_Man_t *

p

)

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 512 of file absVta.c.

{
    Vta_Obj_t * pThis, * pThis0, * pThis1;
    Gia_Obj_t * pObj;
    int i;
    Vta_ManForEachObj( p, pThis, i )
        pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
    Vta_ManForEachObjObj( p, pThis, pObj, i )
    {
        if ( !pThis->fAdded )
            continue;
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
            if ( pThis->iFrame == 0 )
                assert( pThis->Value == VTA_VAR0 );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
            else if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
            else assert( 0 );
        }
    }
}

Vec_Int_t* Vta_ManUnsatCore	(	int	iLit,
		sat_solver2 *	pSat,
		int	nConfMax,
		int	fVerbose,
		int *	piRetValue,
		int *	pnConfls
	)

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

Synopsis [Finds the set of clauses involved in the UNSAT core.]

Description []

SideEffects []

SeeAlso []

Definition at line 1083 of file absVta.c.

{
    abctime clk = Abc_Clock();
    Vec_Int_t * vCore;
    int RetValue, nConfPrev = pSat->stats.conflicts;
    if ( piRetValue )
        *piRetValue = 1;
    // consider special case when PO points to the flop
    // this leads to immediate conflict in the first timeframe
    if ( iLit < 0 )
    {
        vCore = Vec_IntAlloc( 1 );
        Vec_IntPush( vCore, -iLit );
        return vCore;
    }
    // solve the problem
    RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( pnConfls )
        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
    if ( RetValue == l_Undef )
    {
        if ( piRetValue )
            *piRetValue = -1;
        return NULL;
    }
    if ( RetValue == l_True )
    {
        if ( piRetValue )
            *piRetValue = 0;
        return NULL;
    }
    if ( fVerbose )
    {
//        Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
//        Abc_Print( 1, "UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    assert( RetValue == l_False );
    // derive the UNSAT core
    clk = Abc_Clock();
    vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
    if ( fVerbose )
    {
//        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    return vCore;
}

void Vta_ManUnsatCoreRemap	(	Vta_Man_t *	p,
		Vec_Int_t *	vCore
	)

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

Synopsis [Remaps core into frame/node pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file absVta.c.

{
    Vta_Obj_t * pThis;
    int i, Entry;
    Vec_IntForEachEntry( vCore, Entry, i )
    {
        pThis = Vta_ManObj( p, Entry );
        Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
        Vec_IntWriteEntry( vCore, i, Entry );
    }
}

static int Vta_ObjId ( Vta_Man_t *  p, Vta_Obj_t *  pObj  )

inlinestatic

Definition at line 105 of file absVta.c.

{ assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;      }

static void Vta_ObjPreds ( Vta_Man_t *  p, Vta_Obj_t *  pThis, Gia_Obj_t *  pObj, Vta_Obj_t **  ppThis0, Vta_Obj_t **  ppThis1  )

inlinestatic

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

Synopsis [Finds predecessors of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 438 of file absVta.c.

{
    *ppThis0 = NULL;
    *ppThis1 = NULL;
//    if ( !pThis->fAdded )
//        return;
    assert( !Gia_ObjIsPi(p->pGia, pObj) );
    if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
        return;
    if ( Gia_ObjIsAnd(pObj) )
    {
        *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
        *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
//        assert( *ppThis0 && *ppThis1 );
        return;
    }
    assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
    pObj = Gia_ObjRoToRi( p->pGia, pObj );
    *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
//    assert( *ppThis0 );
}

static int Vta_ValIs0 ( Vta_Obj_t *  pThis, int  fCompl  )

inlinestatic

Definition at line 87 of file absVta.c.

{
    if ( pThis->Value == VTA_VAR1 && fCompl )
        return 1;
    if ( pThis->Value == VTA_VAR0 && !fCompl )
        return 1;
    return 0;
}

static int Vta_ValIs1 ( Vta_Obj_t *  pThis, int  fCompl  )

inlinestatic

Definition at line 95 of file absVta.c.

{
    if ( pThis->Value == VTA_VAR0 && fCompl )
        return 1;
    if ( pThis->Value == VTA_VAR1 && !fCompl )
        return 1;
    return 0;
}