absOldCex.c File Reference

#include "abs.h"
#include "sat/bmc/bmc.h"

Go to the source code of this file.

Data Structures
struct	Saig_ManCba_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Saig_ManCba_t_	Saig_ManCba_t
	DECLARATIONS ///. More...

Functions
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...
Aig_Man_t *	Saig_ManDupWithCubes (Aig_Man_t *pAig, Vec_Vec_t *vReg2Value)
Vec_Int_t *	Saig_ManCbaReason2Inputs (Saig_ManCba_t *p, Vec_Int_t *vReasons)
Abc_Cex_t *	Saig_ManCbaReason2Cex (Saig_ManCba_t *p, Vec_Int_t *vReasons)
void	Saig_ManCbaFindReason_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPrios, Vec_Int_t *vReasons)
Vec_Int_t *	Saig_ManCbaFindReason (Saig_ManCba_t *p)
void	Saig_ManCbaUnrollCollect_rec (Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vObjs, Vec_Int_t *vRoots)
Aig_Man_t *	Saig_ManCbaUnrollWithCex (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, Vec_Int_t **pvMapPiF2A, Vec_Vec_t **pvReg2Frame)
Saig_ManCba_t *	Saig_ManCbaStart (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
void	Saig_ManCbaStop (Saig_ManCba_t *p)
void	Saig_ManCbaShrink (Saig_ManCba_t *p)
static void	Saig_ObjCexMinSet0 (Aig_Obj_t *pObj)
static void	Saig_ObjCexMinSet1 (Aig_Obj_t *pObj)
static void	Saig_ObjCexMinSetX (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet0 (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet1 (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGetX (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet0Fanin0 (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet1Fanin0 (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet0Fanin1 (Aig_Obj_t *pObj)
static int	Saig_ObjCexMinGet1Fanin1 (Aig_Obj_t *pObj)
static void	Saig_ObjCexMinSim (Aig_Obj_t *pObj)
static void	Saig_ObjCexMinPrint (Aig_Obj_t *pObj)
int	Saig_ManCexVerifyUsingTernary (Aig_Man_t *pAig, Abc_Cex_t *pCex, Abc_Cex_t *pCare)
Abc_Cex_t *	Saig_ManCbaFindCexCareBits (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Vec_Int_t *	Saig_ManCbaFilterInputs (Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Vec_Int_t *	Saig_ManCbaPerform (Aig_Man_t *pAbs, int nInputs, Saig_ParBmc_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Saig_ManCba_t_ Saig_ManCba_t

DECLARATIONS ///.

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

FileName [saigAbsCba.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [CEX-based abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 31 of file absOldCex.c.

Function Documentation

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

Vec_Int_t* Saig_ManCbaFilterInputs	(	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 785 of file absOldCex.c.

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

clk = Abc_Clock();
    p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
    p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
    vReasons = Saig_ManCbaFindReason( p );
    vRes = Saig_ManCbaReason2Inputs( 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", Abc_Clock() - clk );
    }

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

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_ManCbaFindReason

(

Saig_ManCba_t *

p

)

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

Synopsis [Returns reasons for the property to fail.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file absOldCex.c.

{
    Aig_Obj_t * pObj;
    Vec_Int_t * vPrios, * vReasons;
    int i;

    // set PI values according to CEX
    vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
    Aig_ManConst1(p->pFrames)->fPhase = 1;
    Aig_ManForEachCi( p->pFrames, pObj, i )
    {
        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
        pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
    }

    // traverse and set the priority
    Aig_ManForEachNode( p->pFrames, pObj, i )
    {
        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
        int iPrio0  = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
        int iPrio1  = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
        pObj->fPhase = fPhase0 && fPhase1;
        if ( fPhase0 && fPhase1 ) // both are one
            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
        else if ( !fPhase0 && fPhase1 ) 
            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
        else if ( fPhase0 && !fPhase1 )
            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
        else // both are zero
            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
    }
    // check the property output
    pObj = Aig_ManCo( p->pFrames, 0 );
    pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
    assert( !pObj->fPhase );

    // select the reason
    vReasons = Vec_IntAlloc( 100 );
    Aig_ManIncrementTravId( p->pFrames );
    Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
    Vec_IntFree( vPrios );
//    assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
    return vReasons;
}

void Saig_ManCbaFindReason_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Int_t *	vPrios,
		Vec_Int_t *	vReasons
	)

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

Synopsis [Returns reasons for the property to fail.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file absOldCex.c.

{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    if ( pObj->fPhase )
    {
        Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
        Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
    }
    else
    {
        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
        assert( !fPhase0 || !fPhase1 );
        if ( !fPhase0 && fPhase1 )
            Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
        else if ( fPhase0 && !fPhase1 )
            Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
        else 
        {
            int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
            int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
            if ( iPrio0 <= iPrio1 )
                Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
            else
                Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
        }
    }
}

Vec_Int_t* Saig_ManCbaPerform	(	Aig_Man_t *	pAbs,
		int	nInputs,
		Saig_ParBmc_t *	pPars
	)

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

Synopsis [Checks the abstracted model for a counter-example.]

Description [Returns the array of abstracted flops that should be added to the abstraction.]

SideEffects []

SeeAlso []

Definition at line 830 of file absOldCex.c.

{
    Vec_Int_t * vAbsFfsToAdd;
    int RetValue;
    abctime clk = Abc_Clock();
//    assert( pAbs->nRegs > 0 );
    // perform BMC
    RetValue = Saig_ManBmcScalable( pAbs, pPars );
    if ( RetValue == -1 ) // time out - nothing to add
    {
        printf( "Resource limit is reached during BMC.\n" );
        assert( pAbs->pSeqModel == NULL );
        return Vec_IntAlloc( 0 );
    }
    if ( pAbs->pSeqModel == NULL )
    {
        printf( "BMC did not detect a CEX with the given depth.\n" );
        return Vec_IntAlloc( 0 );
    }
    if ( pPars->fVerbose )
        Abc_CexPrintStats( pAbs->pSeqModel );
    // CEX is detected - refine the flops
    vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose );
    if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
    {
        Vec_IntFree( vAbsFfsToAdd );
        return NULL;
    }
    if ( pPars->fVerbose )
    {
        printf( "Adding %d registers to the abstraction (total = %d).  ", 
            Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    return vAbsFfsToAdd;
}

Abc_Cex_t* Saig_ManCbaReason2Cex	(	Saig_ManCba_t *	p,
		Vec_Int_t *	vReasons
	)

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

Synopsis [Creates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 224 of file absOldCex.c.

{
    Abc_Cex_t * pCare;
    int i, Entry, iInput, iFrame;
    pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
    memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
    Vec_IntForEachEntry( vReasons, Entry, i )
    {
        assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
        iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
        Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
    }
/*
    for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ )
    {
        int Count = 0;
        for ( i = 0; i < pCare->nPis; i++ )
            Count +=  Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i);
        printf( "%d ", Count );
    }
printf( "\n" );
*/
    return pCare;
}

Vec_Int_t* Saig_ManCbaReason2Inputs	(	Saig_ManCba_t *	p,
		Vec_Int_t *	vReasons
	)

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

Synopsis [Maps array of frame PI IDs into array of additional PI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file absOldCex.c.

{
    Vec_Int_t * vOriginal, * vVisited;
    int i, Entry;
    vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); 
    vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
    Vec_IntForEachEntry( vReasons, Entry, i )
    {
        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
        assert( iInput >= p->nInputs && iInput < Aig_ManCiNum(p->pAig) );
        if ( Vec_IntEntry(vVisited, iInput) == 0 )
            Vec_IntPush( vOriginal, iInput - p->nInputs );
        Vec_IntAddToEntry( vVisited, iInput, 1 );
    }
    Vec_IntFree( vVisited );
    return vOriginal;
}

void Saig_ManCbaShrink

(

Saig_ManCba_t *

p

)

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

Synopsis [Destroys refinement manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 555 of file absOldCex.c.

{
    Aig_Man_t * pManNew;
    Aig_Obj_t * pObjLi, * pObjFrame;
    Vec_Int_t * vLevel, * vLevel2;
    int f, k, ObjId, Lit;
    // assuming that important objects are labeled in Saig_ManCbaFindReason()
    Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f )
    {
        Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k )
        {
            pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) );
            if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) )
                continue;
            pObjLi = Aig_ManObj( p->pAig, ObjId );
            assert( Saig_ObjIsLi(p->pAig, pObjLi) );
            Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
        }
    }
    // print statistics
    Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k )
    {
        vLevel2 = Vec_VecEntryInt( p->vReg2Value, k );
        printf( "Level = %4d   StateBits = %4d (%6.2f %%)  CareBits = %4d (%6.2f %%)\n", k, 
            Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig),
            Vec_IntSize(vLevel2),  100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) );
    }
    // try reducing the frames
    pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
//    Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
    Aig_ManStop( pManNew );
}

Saig_ManCba_t* Saig_ManCbaStart	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex,
		int	nInputs,
		int	fVerbose
	)

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

Synopsis [Creates refinement manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file absOldCex.c.

{
    Saig_ManCba_t * p;
    p = ABC_CALLOC( Saig_ManCba_t, 1 );
    p->pAig = pAig;
    p->pCex = pCex;
    p->nInputs = nInputs;
    p->fVerbose = fVerbose;
    return p;
}

void Saig_ManCbaStop

(

Saig_ManCba_t *

p

)

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

Synopsis [Destroys refinement manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 535 of file absOldCex.c.

{
    Vec_VecFreeP( &p->vReg2Frame );
    Vec_VecFreeP( &p->vReg2Value );
    Aig_ManStopP( &p->pFrames );
    Vec_IntFreeP( &p->vMapPiF2A );
    ABC_FREE( p );
}

void Saig_ManCbaUnrollCollect_rec	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObj,
		Vec_Int_t *	vObjs,
		Vec_Int_t *	vRoots
	)

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

Synopsis [Collect nodes in the unrolled timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file absOldCex.c.

{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsCo(pObj) )
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
    else if ( Aig_ObjIsNode(pObj) )
    {
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
    }
    if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
        Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
    Vec_IntPush( vObjs, Aig_ObjId(pObj) );
}

Aig_Man_t* Saig_ManCbaUnrollWithCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex,
		int	nInputs,
		Vec_Int_t **	pvMapPiF2A,
		Vec_Vec_t **	pvReg2Frame
	)

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

Synopsis [Derive unrolled timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file absOldCex.c.

{
    Aig_Man_t * pFrames;     // unrolled timeframes
    Vec_Vec_t * vFrameCos;   // the list of COs per frame
    Vec_Vec_t * vFrameObjs;  // the list of objects per frame
    Vec_Int_t * vRoots, * vObjs;
    Aig_Obj_t * pObj;
    int i, f;
    // sanity checks
    assert( Saig_ManPiNum(pAig) == pCex->nPis );
//    assert( Saig_ManRegNum(pAig) == pCex->nRegs );
    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );

    // map PIs of the unrolled frames into PIs of the original design
    *pvMapPiF2A = Vec_IntAlloc( 1000 );

    // collect COs and Objs visited in each frame
    vFrameCos  = Vec_VecStart( pCex->iFrame+1 );
    vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
    // initialized the topmost frame
    pObj = Aig_ManCo( pAig, pCex->iPo );
    Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
    for ( f = pCex->iFrame; f >= 0; f-- )
    {
        // collect nodes starting from the roots
        Aig_ManIncrementTravId( pAig );
        vRoots = Vec_VecEntryInt( vFrameCos, f );
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
            Saig_ManCbaUnrollCollect_rec( pAig, pObj, 
                Vec_VecEntryInt(vFrameObjs, f),
                (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
    }

    // derive unrolled timeframes
    pFrames = Aig_ManStart( 10000 );
    pFrames->pName = Abc_UtilStrsav( pAig->pName );
    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
    // initialize the flops 
    if ( Saig_ManRegNum(pAig) == pCex->nRegs )
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
    }
    else // this is the case when synthesis was applied, assume all-0 init state
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), 1 );
    }
    // iterate through the frames
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        // construct
        vObjs = Vec_VecEntryInt( vFrameObjs, f );
        Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
        {
            if ( Aig_ObjIsNode(pObj) )
                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
            else if ( Aig_ObjIsCo(pObj) )
                pObj->pData = Aig_ObjChild0Copy(pObj);
            else if ( Aig_ObjIsConst1(pObj) )
                pObj->pData = Aig_ManConst1(pFrames);
            else if ( Saig_ObjIsPi(pAig, pObj) )
            {
                if ( Aig_ObjCioId(pObj) < nInputs )
                {
                    int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
                    pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
                }
                else
                {
                    pObj->pData = Aig_ObjCreateCi( pFrames );
                    Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
                    Vec_IntPush( *pvMapPiF2A, f );
                }
            }
        }
        if ( f == pCex->iFrame )
            break;
        // transfer
        vRoots = Vec_VecEntryInt( vFrameCos, f );
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
        {
            Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
            if ( *pvReg2Frame )
            {
                Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) );             // record LO
                Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjToLit((Aig_Obj_t *)pObj->pData) ); // record its literal
            }
        }
    }
    // create output
    pObj = Aig_ManCo( pAig, pCex->iPo );
    Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
    Aig_ManSetRegNum( pFrames, 0 );
    // cleanup
    Vec_VecFree( vFrameCos );
    Vec_VecFree( vFrameObjs );
    // finallize
    Aig_ManCleanup( pFrames );
    // return
    return pFrames;
}

int Saig_ManCexVerifyUsingTernary	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex,
		Abc_Cex_t *	pCare
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 647 of file absOldCex.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int i, f, iBit = 0;
    assert( pCex->iFrame == pCare->iFrame );
    assert( pCex->nBits  == pCare->nBits );
    assert( pCex->iPo < Saig_ManPoNum(pAig) );
    Saig_ObjCexMinSet1( Aig_ManConst1(pAig) );
    // set flops to the init state
    Saig_ManForEachLo( pAig, pObj, i )
    {
        assert( !Abc_InfoHasBit(pCex->pData, iBit) );
        assert( !Abc_InfoHasBit(pCare->pData, iBit) );
//        if ( Abc_InfoHasBit(pCare->pData, iBit++) )
            Saig_ObjCexMinSet0( pObj );
//        else
//            Saig_ObjCexMinSetX( pObj );
    }
    iBit = pCex->nRegs;
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        // init inputs
        Saig_ManForEachPi( pAig, pObj, i )
        {
            if ( Abc_InfoHasBit(pCare->pData, iBit++) )
            {
                if ( Abc_InfoHasBit(pCex->pData, iBit-1) )
                    Saig_ObjCexMinSet1( pObj );
                else
                    Saig_ObjCexMinSet0( pObj );
            }
            else
                Saig_ObjCexMinSetX( pObj );
        }
        // simulate internal nodes
        Aig_ManForEachNode( pAig, pObj, i )
            Saig_ObjCexMinSim( pObj );
        // simulate COs
        Aig_ManForEachCo( pAig, pObj, i )
            Saig_ObjCexMinSim( pObj );
/*
        Aig_ManForEachObj( pAig, pObj, i )
        {
            Aig_ObjPrint(pAig, pObj);
            printf( "  Value = " );
            Saig_ObjCexMinPrint( pObj );
            printf( "\n" );
        }
*/
        // transfer
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
            pObjRo->fMarkA = pObjRi->fMarkA,
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == pCex->nBits );
    return Saig_ObjCexMinGet1( Aig_ManCo( pAig, pCex->iPo ) );
}

Aig_Man_t* Saig_ManDupWithCubes	(	Aig_Man_t *	pAig,
		Vec_Vec_t *	vReg2Value
	)

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

Synopsis [Duplicate with literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file absOldCex.c.

{
    Vec_Int_t * vLevel;
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pMiter;
    int i, k, Lit;
    assert( pAig->nConstrs == 0 );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs for cubes
    Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
    {
        pMiter = Aig_ManConst1( pAigNew );
        Vec_IntForEachEntry( vLevel, Lit, k )
        {
            pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
            pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
        }
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

static int Saig_ObjCexMinGet0 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 592 of file absOldCex.c.

{ return  pObj->fMarkA && !pObj->fMarkB; }

static int Saig_ObjCexMinGet0Fanin0 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 596 of file absOldCex.c.

{ return (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }

static int Saig_ObjCexMinGet0Fanin1 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 599 of file absOldCex.c.

{ return (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }

static int Saig_ObjCexMinGet1 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 593 of file absOldCex.c.

{ return !pObj->fMarkA &&  pObj->fMarkB; }

static int Saig_ObjCexMinGet1Fanin0 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 597 of file absOldCex.c.

{ return (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }

static int Saig_ObjCexMinGet1Fanin1 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 600 of file absOldCex.c.

{ return (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }

static int Saig_ObjCexMinGetX ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 594 of file absOldCex.c.

{ return  pObj->fMarkA &&  pObj->fMarkB; }

static void Saig_ObjCexMinPrint ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 625 of file absOldCex.c.

{
    if ( Saig_ObjCexMinGet0(pObj) )
        printf( "0" );
    else if ( Saig_ObjCexMinGet1(pObj) )
        printf( "1" );
    else if ( Saig_ObjCexMinGetX(pObj) )
        printf( "X" );
}

static void Saig_ObjCexMinSet0 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 588 of file absOldCex.c.

{ pObj->fMarkA = 1; pObj->fMarkB = 0;    }

static void Saig_ObjCexMinSet1 ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 589 of file absOldCex.c.

{ pObj->fMarkA = 0; pObj->fMarkB = 1;    }

static void Saig_ObjCexMinSetX ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 590 of file absOldCex.c.

{ pObj->fMarkA = 1; pObj->fMarkB = 1;    }

static void Saig_ObjCexMinSim ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 602 of file absOldCex.c.

{
    if ( Aig_ObjIsAnd(pObj) )
    {
        if ( Saig_ObjCexMinGet0Fanin0(pObj) || Saig_ObjCexMinGet0Fanin1(pObj) )
            Saig_ObjCexMinSet0( pObj );
        else if ( Saig_ObjCexMinGet1Fanin0(pObj) && Saig_ObjCexMinGet1Fanin1(pObj) )
            Saig_ObjCexMinSet1( pObj );
        else 
            Saig_ObjCexMinSetX( pObj );
    }
    else if ( Aig_ObjIsCo(pObj) )
    {
        if ( Saig_ObjCexMinGet0Fanin0(pObj) )
            Saig_ObjCexMinSet0( pObj );
        else if ( Saig_ObjCexMinGet1Fanin0(pObj) )
            Saig_ObjCexMinSet1( pObj );
        else 
            Saig_ObjCexMinSetX( pObj );
    }
    else assert( 0 );
}