bmcCexDepth.c File Reference

#include "bmc.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Abc_Cex_t *	Bmc_CexInnerStates (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
	DECLARATIONS ///. More...
Abc_Cex_t *	Bmc_CexCareBits (Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
int	Bmc_CexVerify (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Gia_Man_t *	Bmc_CexTargetEnlarge (Gia_Man_t *p, int nFrames)
	FUNCTION DEFINITIONS ///. More...
Gia_Man_t *	Bmc_CexTarget (Gia_Man_t *p, int nFrames)
Gia_Man_t *	Bmc_CexBuildNetwork2 (Gia_Man_t *p, Abc_Cex_t *pCex, int fStart)
Gia_Man_t *	Bmc_CexBuildNetwork2_ (Gia_Man_t *p, Abc_Cex_t *pCex, int fStart)
Gia_Man_t *	Bmc_CexBuildNetwork2Test (Gia_Man_t *p, Abc_Cex_t *pCex, int nFramesMax)
Gia_Man_t *	Bmc_CexDepthTest (Gia_Man_t *p, Abc_Cex_t *pCex, int nFrames, int fVerbose)

Function Documentation

Gia_Man_t* Bmc_CexBuildNetwork2	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	fStart
	)

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

Synopsis [Computes CE-induced network.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
    int fCompl0, fCompl1;
    int i, k, iBit;
    assert( pCex->nRegs == 0 );
    assert( pCex->nPis == Gia_ManCiNum(p) );
    assert( fStart <= pCex->iFrame );
    // start the manager
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( "unate" );
    // set const0
    Gia_ManConst0(p)->fMark0 = 0; // value
    Gia_ManConst0(p)->fMark1 = 1; // care
    Gia_ManConst0(p)->Value  = ~0;
    // set init state
    Gia_ManForEachRi( p, pObj, k )
    {
        pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
        pObj->fMark1 = 0;
        pObj->Value  = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
    }
    Gia_ManHashAlloc( pNew );
    iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
    for ( i = fStart; i <= pCex->iFrame; i++ )
    {
        //  primary inputs
        Gia_ManForEachPi( p, pObj, k )
        {
            pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
            pObj->fMark1 = 1;
            pObj->Value  = ~0;
        }
        iBit += Gia_ManRegNum(p);
        // transfer 
        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
        {
            pObjRo->fMark0 = pObjRi->fMark0;
            pObjRo->fMark1 = pObjRi->fMark1;
            pObjRo->Value  = pObjRi->Value;
        }
        // internal nodes
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 && !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            else if ( !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
            else assert( 0 );
            pObj->Value = ~0;
            if ( pObj->fMark1 )
                continue;
            if ( pObj->fMark0 )
                pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
            else if ( !fCompl0 && !fCompl1 )
                pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
            else if ( !fCompl0 )
                pObj->Value = Gia_ObjFanin0(pObj)->Value;
            else if ( !fCompl1 )
                pObj->Value = Gia_ObjFanin1(pObj)->Value;
            else assert( 0 );
            assert( pObj->Value > 0 );
        }
        // combinational outputs
        Gia_ManForEachCo( p, pObj, k )
        {
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            pObj->Value  = Gia_ObjFanin0(pObj)->Value;
        }
    }
    Gia_ManHashStop( pNew );
    assert( iBit == pCex->nBits );
    // create primary output
    pObj = Gia_ManPo(p, pCex->iPo);
    assert( pObj->fMark0 == 1 );
    assert( pObj->fMark1 == 0 );
    assert( pObj->Value > 0 );
    Gia_ManAppendCo( pNew, pObj->Value );
    // cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Gia_Man_t* Bmc_CexBuildNetwork2_	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	fStart
	)

Definition at line 220 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
    int fCompl0, fCompl1;
    int i, k, iBit;
    assert( pCex->nRegs == 0 );
    assert( pCex->nPis == Gia_ManCiNum(p) );
    assert( fStart <= pCex->iFrame );
    // start the manager
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( "unate" );
    // set const0
    Gia_ManConst0(p)->fMark0 = 0; // value
    Gia_ManConst0(p)->Value  = 1;
    // set init state
    Gia_ManForEachRi( p, pObj, k )
    {
        pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
        pObj->Value  = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
    }
    Gia_ManHashAlloc( pNew );
    iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
    for ( i = fStart; i <= pCex->iFrame; i++ )
    {
        //  primary inputs
        Gia_ManForEachPi( p, pObj, k )
        {
            pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
            pObj->Value  = 1;
        }
        iBit += Gia_ManRegNum(p);
        // transfer 
        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
        {
            pObjRo->fMark0 = pObjRi->fMark0;
            pObjRo->Value  = pObjRi->Value;
        }
        // internal nodes
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
            else if ( !fCompl0 && !fCompl1 )
                pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
            else if ( !fCompl0 )
                pObj->Value = Gia_ObjFanin0(pObj)->Value;
            else if ( !fCompl1 )
                pObj->Value = Gia_ObjFanin1(pObj)->Value;
            else assert( 0 );
        }
        // combinational outputs
        Gia_ManForEachCo( p, pObj, k )
        {
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            pObj->Value  = Gia_ObjFanin0(pObj)->Value;
        }
    }
    Gia_ManHashStop( pNew );
    assert( iBit == pCex->nBits );
    // create primary output
    pObj = Gia_ManPo(p, pCex->iPo);
    assert( pObj->fMark0 == 1 );
    assert( pObj->Value > 0 );
    Gia_ManAppendCo( pNew, pObj->Value );
    // cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Gia_Man_t* Bmc_CexBuildNetwork2Test	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	nFramesMax
	)

Definition at line 294 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew, * pTemp;
    Vec_Ptr_t * vCones;
    abctime clk = Abc_Clock();
    int i;
    nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame );
    printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax );
    vCones = Vec_PtrAlloc( nFramesMax );
    for ( i = pCex->iFrame; i > pCex->iFrame - nFramesMax; i-- )
    {
        printf( "Frame %5d : ", i );
        pNew = Bmc_CexBuildNetwork2_( p, pCex, i );
        Gia_ManPrintStats( pNew, NULL );
        Vec_PtrPush( vCones, pNew );
    }
    pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
    Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
    Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
        Gia_ManStop( pTemp );
    Vec_PtrFree( vCones );
    printf( "GIA with additional properties is written into \"miter2.aig\".\n" );
//    printf( "CE-induced network is written into file \"unate.aig\".\n" );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//    Gia_ManStop( pNew );
    return pNew;
}

Abc_Cex_t* Bmc_CexCareBits	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCexState,
		Abc_Cex_t *	pCexImpl,
		Abc_Cex_t *	pCexEss,
		int	fFindAll,
		int	fVerbose
	)

Definition at line 550 of file bmcCexTools.c.

{
    Abc_Cex_t * pNew;
    Gia_Obj_t * pObj;
    int fCompl0, fCompl1;
    int i, k, iBit;
    assert( pCexState->nRegs == 0 );
    // start the counter-example
    pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
    pNew->iFrame = pCexState->iFrame;
    pNew->iPo    = pCexState->iPo;
    // set initial state
    Gia_ManCleanMark01(p);
    // set const0
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManConst0(p)->fMark1 = 1;
    for ( i = pCexState->iFrame; i >= 0; i-- )
    {
        // set correct values
        iBit = pCexState->nPis * i;
        Gia_ManForEachCi( p, pObj, k )
        {
            pObj->fMark0 = Abc_InfoHasBit(pCexState->pData, iBit+k);
            pObj->fMark1 = 0;
            if ( pCexImpl )
                pObj->fMark1 |= Abc_InfoHasBit(pCexImpl->pData, iBit+k);
            if ( pCexEss )
                pObj->fMark1 |= Abc_InfoHasBit(pCexEss->pData, iBit+k);
        }
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 && !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            else if ( !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
            else assert( 0 );
        }
        Gia_ManForEachCo( p, pObj, k )
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
        // move values from COs to CIs
        if ( i == pCexState->iFrame )
        {
            assert( Gia_ManPo(p, pCexState->iPo)->fMark0 == 1 );
            if ( fFindAll )
                Bmc_CexCareBits_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
            else
                Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
        }
        else
        {
            Gia_ManForEachRi( p, pObj, k )
                if ( Abc_InfoHasBit(pNew->pData, pNew->nPis * (i+1) + Gia_ManPiNum(p) + k) )
                {
                     if ( fFindAll )
                         Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
                     else
                         Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
                }
        }
        // save the results
        Gia_ManForEachCi( p, pObj, k )
            if ( pObj->fMark1 )
            {
                pObj->fMark1 = 0;
                if ( pCexImpl == NULL || !Abc_InfoHasBit(pCexImpl->pData, pNew->nPis * i + k) )
                    Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
            }
    }
    if ( pCexEss )
        printf( "Minimized:    " );
    else
        printf( "Care bits:    " );
    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
    return pNew;
}

Gia_Man_t* Bmc_CexDepthTest	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	nFrames,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew;
    abctime clk = Abc_Clock();
    Abc_Cex_t * pCexImpl   = NULL;
    Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
    Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
//    Abc_Cex_t * pCexEss, * pCexMin;

    if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
        printf( "Counter-example care-set verification has failed.\n" );

//    pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
//    pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );

//    if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
//        printf( "Counter-example min-set verification has failed.\n" );

//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );

    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames );
//    Bmc_CexPerformUnrollingTest( p, pCex );

    Abc_CexFreeP( &pCexStates );
    Abc_CexFreeP( &pCexImpl );
    Abc_CexFreeP( &pCexCare );
//    Abc_CexFreeP( &pCexEss );
//    Abc_CexFreeP( &pCexMin );
    return pNew;
}

ABC_NAMESPACE_IMPL_START Abc_Cex_t* Bmc_CexInnerStates	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		Abc_Cex_t **	ppCexImpl,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [bmcCexDepth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [CEX depth minimization.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Computes internal states of the CEX.]

Description []

SideEffects []

SeeAlso []

Definition at line 388 of file bmcCexTools.c.

{
    Abc_Cex_t * pNew, * pNew2;
    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
    int fCompl0, fCompl1;
    int i, k, iBit = 0;
    assert( pCex->nRegs > 0 );
    // start the counter-example
    pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
    pNew->iFrame = pCex->iFrame;
    pNew->iPo    = pCex->iPo;
    // start the counter-example
    pNew2 = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
    pNew2->iFrame = pCex->iFrame;
    pNew2->iPo    = pCex->iPo;
    // set initial state
    Gia_ManCleanMark01(p);
    // set const0
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManConst0(p)->fMark1 = 1;
    // set init state
    Gia_ManForEachRi( p, pObjRi, k )
    {
        pObjRi->fMark0 = 0;
        pObjRi->fMark1 = 1;
    }
    iBit = pCex->nRegs;
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
            pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
        {
            pObjRo->fMark0 = pObjRi->fMark0;
            pObjRo->fMark1 = pObjRi->fMark1;
        }
        Gia_ManForEachCi( p, pObj, k )
        {
            if ( pObj->fMark0 )
                Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k );
            if ( pObj->fMark1 )
                Abc_InfoSetBit( pNew2->pData, pNew2->nPis * i + k );
        }
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 && !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            else if ( !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
            else assert( 0 );
        }
        Gia_ManForEachCo( p, pObj, k )
        {
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
        }

/*
        // print input/state/output
        printf( "%3d : ", i );
        Gia_ManForEachPi( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( " " );
        Gia_ManForEachRo( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( " " );
        Gia_ManForEachPo( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( "\n" );
*/
    }
    assert( iBit == pCex->nBits );
    assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );

    printf( "Inner states: " );
    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
    printf( "Implications: " );
    Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
    if ( ppCexImpl )
        *ppCexImpl = pNew2;
    else
        Abc_CexFree( pNew2 );
    return pNew;
}

Gia_Man_t* Bmc_CexTarget	(	Gia_Man_t *	p,
		int	nFrames
	)

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

Synopsis [Create target with quantified inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew, * pTemp;
    int i, Limit = nFrames * Gia_ManPiNum(p);
    pNew = Bmc_CexTargetEnlarge( p, nFrames );
    for ( i = 0; i < Limit; i++ )
    {
        printf( "%3d : ", i );
        if ( i % Gia_ManPiNum(p) == 0 )
            Gia_ManPrintStats( pNew, NULL );
        pNew = Gia_ManDupExist( pTemp = pNew, i );
        Gia_ManStop( pTemp );
    }
    Gia_ManPrintStats( pNew, NULL );
    pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) );
    Gia_ManStop( pTemp );  
    Gia_ManPrintStats( pNew, NULL );
    pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
    Gia_ManStop( pNew );
    Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
    return pTemp;
}

Gia_Man_t* Bmc_CexTargetEnlarge	(	Gia_Man_t *	p,
		int	nFrames
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs targe enlargement of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file bmcCexDepth.c.

{
    Gia_Man_t * pNew, * pOne;
    Gia_Obj_t * pObj, * pObjRo;
    int i, k;
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p)->Value = 0;
    for ( k = 0; k < nFrames; k++ )
        Gia_ManForEachPi( p, pObj, i )
            Gia_ManAppendCi( pNew );
    Gia_ManForEachRo( p, pObj, i )
        pObj->Value = Gia_ManAppendCi( pNew );
    for ( k = 0; k < nFrames; k++ )
    {
        Gia_ManForEachPi( p, pObj, i )
            pObj->Value = Gia_ManCiLit( pNew, (nFrames - 1 - k) * Gia_ManPiNum(p) + i );
        Gia_ManForEachAnd( p, pObj, i )
            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        Gia_ManForEachRi( p, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        Gia_ManForEachRiRo( p, pObj, pObjRo, i )
            pObjRo->Value  = pObj->Value;
    }
    pObj = Gia_ManPo( p, 0 );
    pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManHashStop( pNew );
    pNew = Gia_ManCleanup( pOne = pNew );
    Gia_ManStop( pOne );
    return pNew;
}

int Bmc_CexVerify	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		Abc_Cex_t *	pCexCare
	)

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

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file bmcCexTools.c.

{
    Gia_Obj_t * pObj;
    int i, k;
    assert( pCex->nRegs > 0 );
//    assert( pCexCare->nRegs == 0 );
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachRi( p, pObj, k )
        Gia_ObjTerSimSet0( pObj );
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
        {
            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                Gia_ObjTerSimSetX( pObj );
            else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                Gia_ObjTerSimSet1( pObj );
            else
                Gia_ObjTerSimSet0( pObj );
        }
        Gia_ManForEachRo( p, pObj, k )
            Gia_ObjTerSimRo( p, pObj );
        Gia_ManForEachAnd( p, pObj, k )
            Gia_ObjTerSimAnd( pObj );
        Gia_ManForEachCo( p, pObj, k )
            Gia_ObjTerSimCo( pObj );
    }
    pObj = Gia_ManPo( p, pCex->iPo );
    return Gia_ObjTerSimGet1(pObj);
}