wlcAbs.c File Reference

#include "wlc.h"
#include "proof/pdr/pdr.h"
#include "proof/pdr/pdrInt.h"
#include "proof/ssw/ssw.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"

Include dependency graph for wlcAbs.c:

Go to the source code of this file.

Classes
struct	Int_Pair_t_

Typedefs
typedef struct Int_Pair_t_	Int_Pair_t

Functions
ABC_NAMESPACE_IMPL_START Vec_Vec_t *	IPdr_ManSaveClauses (Pdr_Man_t *p, int fDropLast)
	DECLARATIONS ///.
int	IPdr_ManRestoreClauses (Pdr_Man_t *p, Vec_Vec_t *vClauses, Vec_Int_t *vMap)
int	IPdr_ManRebuildClauses (Pdr_Man_t *p, Vec_Vec_t *vClauses)
int	IPdr_ManSolveInt (Pdr_Man_t *p, int fCheckClauses, int fPushClauses)
int	IPdr_ManCheckCombUnsat (Pdr_Man_t *p)
int	IPdr_ManReduceClauses (Pdr_Man_t *p, Vec_Vec_t *vClauses)
void	IPdr_ManPrintClauses (Vec_Vec_t *vClauses, int kStart, int nRegs)
void	Wla_ManJoinThread (Wla_Man_t *pWla, int RunId)
void	Wla_ManConcurrentBmc3 (Wla_Man_t *pWla, Aig_Man_t *pAig, Abc_Cex_t **ppCex)
int	Wla_CallBackToStop (int RunId)
int	Wla_GetGlobalRunId ()
int	IntPairPtrCompare (Int_Pair_t **a, Int_Pair_t **b)
void	Wlc_NtkPrintNtk (Wlc_Ntk_t *p)
	FUNCTION DEFINITIONS ///.
void	Wlc_NtkAbsGetSupp_rec (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, Vec_Bit_t *vCiMarks, Vec_Int_t *vSuppRefs, Vec_Int_t *vSuppList)
void	Wlc_NtkAbsGetSupp (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, Vec_Bit_t *vCiMarks, Vec_Int_t *vSuppRefs, Vec_Int_t *vSuppList)
int	Wlc_NtkNumPiBits (Wlc_Ntk_t *pNtk)
void	Wlc_NtkAbsAnalyzeRefine (Wlc_Ntk_t *p, Vec_Int_t *vBlacks, Vec_Bit_t *vUnmark, int *nDisj, int *nNDisj)
Wlc_Ntk_t *	Wlc_NtkIntroduceChoices (Wlc_Ntk_t *pNtk, Vec_Int_t *vBlacks, Vec_Int_t *vPPIs)
Vec_Int_t *	Wlc_NtkFlopsRemap (Wlc_Ntk_t *p, Vec_Int_t *vFfOld, Vec_Int_t *vFfNew)
Vec_Int_t *	Wla_ManCollectNodes (Wla_Man_t *pWla, int fBlack)
int	Wla_ManShrinkAbs (Wla_Man_t *pWla, int nFrames, int RunId)
Wlc_Ntk_t *	Wla_ManCreateAbs (Wla_Man_t *pWla)
Aig_Man_t *	Wla_ManBitBlast (Wla_Man_t *pWla, Wlc_Ntk_t *pAbs)
int	Wla_ManCheckCombUnsat (Wla_Man_t *pWla, Aig_Man_t *pAig)
int	Wla_ManSolveInt (Wla_Man_t *pWla, Aig_Man_t *pAig)
void	Wla_ManRefine (Wla_Man_t *pWla)
Wla_Man_t *	Wla_ManStart (Wlc_Ntk_t *pNtk, Wlc_Par_t *pPars)
void	Wla_ManStop (Wla_Man_t *p)
int	Wla_ManSolve (Wla_Man_t *pWla, Wlc_Par_t *pPars)
int	Wlc_NtkPdrAbs (Wlc_Ntk_t *p, Wlc_Par_t *pPars)
int	Wlc_NtkAbsCore (Wlc_Ntk_t *p, Wlc_Par_t *pPars)
	FUNCTION DECLARATIONS ///.

Typedef Documentation

Int_Pair_t

typedef struct Int_Pair_t_ Int_Pair_t

Definition at line 46 of file wlcAbs.c.

Function Documentation

IntPairPtrCompare()

int IntPairPtrCompare	(	Int_Pair_t **	a,
		Int_Pair_t **	b )

Definition at line 53 of file wlcAbs.c.

{
    return (*a)->second < (*b)->second; 
}

IPdr_ManCheckCombUnsat()

int IPdr_ManCheckCombUnsat ( Pdr_Man_t * p )

extern

Definition at line 871 of file pdrIncr.c.

{
    int iFrame, RetValue = -1;
 
    Pdr_ManCreateSolver( p, (iFrame = 0) );
    Pdr_ManCreateSolver( p, (iFrame = 1) );
 
    p->nFrames = iFrame;
    p->iUseFrame = Abc_MaxInt(iFrame, 1);
 
    RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

IPdr_ManPrintClauses()

void IPdr_ManPrintClauses ( Vec_Vec_t * vClauses, int kStart, int nRegs )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file pdrIncr.c.

{
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pCube;
    int i, k, Counter = 0;
    Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
    {
        Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
        {
            Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
            // Pdr_SetPrint( stdout, pCube, nRegs, NULL );  
            ZPdr_SetPrint( pCube );  
            Abc_Print( 1, "\n" ); 
        }
    }
}

Here is the call graph for this function:

IPdr_ManRebuildClauses()

int IPdr_ManRebuildClauses ( Pdr_Man_t * p, Vec_Vec_t * vClauses )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 256 of file pdrIncr.c.

{
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pCube;
    int i, j;
    int RetValue = -1;
    int nCubes = 0;
 
    if ( vClauses == NULL )
        return RetValue;
 
    assert( Vec_VecSize(vClauses) >= 2 );
    assert( Vec_VecSize(p->vClauses) == 0 ); 
    Vec_VecExpand( p->vClauses, 1 );
 
    IPdr_ManSetSolver( p, 0, 1 );
 
    // push clauses from R0 to R1
    Vec_VecForEachLevelStart( vClauses, vArrayK, i, 1 )
    {
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
        {
            ++nCubes;
 
            RetValue = Pdr_ManCheckCube( p, 0, pCube, NULL, 0, 0, 1 );
            Vec_IntWriteEntry( p->vActVars, 0, 0 );
 
            assert( RetValue != -1 );
 
            if ( RetValue == 0 )
            {
                Abc_Print( 1, "Cube[%d][%d] cannot be pushed from R0 to R1.\n", i, j );
                Pdr_SetDeref( pCube );
                continue;
            }
 
            Vec_VecPush( p->vClauses, 1, pCube );
        }
    }
    Abc_Print( 1, "RebuildClauses: %d out of %d cubes reused in R1.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, 1)), nCubes );
    IPdr_ManSetSolver( p, 1, 0 );
    Vec_VecFree( vClauses );
 
    /*
    for ( i = 1; i < Vec_VecSize( vClauses ) - 1; ++i )
    {
        vArrayK = IPdr_ManPushClausesK( p, i );
        if ( Vec_PtrSize(vArrayK) == 0 )
        {
            Abc_Print( 1, "RebuildClauses: stopped at frame %d.\n", i );
            break;
        }
 
        Vec_PtrGrow( (Vec_Ptr_t *)(p->vClauses), i + 2 );
        p->vClauses->nSize = i + 2;
        p->vClauses->pArray[i+1] = vArrayK;
        IPdr_ManSetSolver( p, i + 1, 0 );
    }
 
    Abc_Print( 1, "After rebuild:" );
    Vec_VecForEachLevel( p->vClauses, vArrayK, i )
        Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) );
    Abc_Print( 1, "\n" );
    */
 
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

IPdr_ManReduceClauses()

int IPdr_ManReduceClauses ( Pdr_Man_t * p, Vec_Vec_t * vClauses )

extern

Definition at line 971 of file pdrIncr.c.

{
    int iFrame, RetValue = -1;
    Vec_Ptr_t * vLast = NULL;
 
    Pdr_ManCreateSolver( p, (iFrame = 0) );
    Pdr_ManCreateSolver( p, (iFrame = 1) );
 
    p->nFrames = iFrame;
    p->iUseFrame = Abc_MaxInt(iFrame, 1);
 
    vLast = Vec_VecEntry( vClauses, Vec_VecSize( vClauses ) - 1 );
    RetValue = IPdr_ManCheckCubeReduce( p, vLast, NULL, p->pPars->nConfLimit );
    return RetValue;
}

Here is the call graph for this function:

IPdr_ManRestoreClauses()

int IPdr_ManRestoreClauses ( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap )

extern

Definition at line 338 of file pdrIncr.c.

{
    int i;
 
    assert(vClauses);
 
    Vec_VecFree(p->vClauses);
    p->vClauses = vClauses;
 
    // remap clause literals using mapping (old flop -> new flop) found in array vMap
    if ( vMap )
    {
        Pdr_Set_t * pSet; int j, k;   
        Vec_VecForEachEntry( Pdr_Set_t *, vClauses, pSet, i, j )
            for ( k = 0; k < pSet->nLits; k++ )
                pSet->Lits[k] = Abc_Lit2LitV( Vec_IntArray(vMap), pSet->Lits[k] );
    }
 
    for ( i = 0; i < Vec_VecSize(p->vClauses); ++i )
        IPdr_ManSetSolver( p, i, i < Vec_VecSize( p->vClauses ) - 1 );
 
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

IPdr_ManSaveClauses()

ABC_NAMESPACE_IMPL_START Vec_Vec_t * IPdr_ManSaveClauses ( Pdr_Man_t * p, int fDropLast )

extern

DECLARATIONS ///.

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

FileName [wlcAbs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [Abstraction for word-level networks.]

Author [Yen-Sheng Ho, Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - August 22, 2014.]

Revision [

Id

wlcAbs.c,v 1.00 2014/09/12 00:00:00 alanmi Exp

]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file pdrIncr.c.

{
    int i, k;
    Vec_Vec_t * vClausesSaved;
    Pdr_Set_t * pCla;
 
    if ( Vec_VecSize( p->vClauses ) == 1 )
        return NULL;
    if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast )
        return NULL;
 
    if ( fDropLast )
        vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
    else 
        vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) );
 
    Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) )
        Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla));
 
    return vClausesSaved;
}

Here is the call graph for this function:

Here is the caller graph for this function:

IPdr_ManSolveInt()

int IPdr_ManSolveInt ( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file pdrIncr.c.

{
    int fPrintClauses = 0;
    Pdr_Set_t * pCube = NULL;
    Aig_Obj_t * pObj;
    Abc_Cex_t * pCexNew;
    int iFrame, RetValue = -1;
    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
    abctime clkStart = Abc_Clock(), clkOne = 0;
    p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    // assert( Vec_PtrSize(p->vSolvers) == 0 );
    // in the multi-output mode, mark trivial POs (those fed by const0) as solved 
    if ( p->pPars->fSolveAll )
        Saig_ManForEachPo( p->pAig, pObj, iFrame )
            if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
            {
                Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
                p->pPars->nProveOuts++;
                if ( p->pPars->fUseBridge )
                    Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
            }
    // create the first timeframe
    p->pPars->timeLastSolved = Abc_Clock();
 
    if ( Vec_VecSize(p->vClauses) == 0 )
        Pdr_ManCreateSolver( p, (iFrame = 0) );
    else {
        iFrame = Vec_VecSize(p->vClauses) - 1;
 
        if ( fCheckClauses )
        {
            if ( p->pPars->fVerbose )
               Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
            IPdr_ManCheckClauses( p );
            if ( p->pPars->fVerbose )
               Abc_Print( 1, " Passed!\n" ) ;
        }
 
        if ( fPushClauses )
        {
            p->iUseFrame = Abc_MaxInt(iFrame, 1);
 
            if ( p->pPars->fVerbose ) 
            {
                Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            }
 
            RetValue = Pdr_ManPushClauses( p );
 
            if ( p->pPars->fVerbose ) 
            {
                Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            }
 
            if ( RetValue ) 
            {
                Pdr_ManReportInvariant( p );
                Pdr_ManVerifyInvariant( p );
                return 1;
            }
        }
 
        if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 )
        {
            assert( p->vAbsFlops == NULL );
            p->vAbsFlops  = Vec_IntStart( Saig_ManRegNum(p->pAig) );
            p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
            p->vMapPpi2Ff = Vec_IntAlloc( 100 );
            
            IPdr_ManRestoreAbsFlops( p );
        }
 
    }
    while ( 1 )
    {
        int fRefined = 0;
        if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
        {
//            int i, Prio;
            assert( p->vAbsFlops == NULL );
            p->vAbsFlops  = Vec_IntStart( Saig_ManRegNum(p->pAig) );
            p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
            p->vMapPpi2Ff = Vec_IntAlloc( 100 );
//            Vec_IntForEachEntry( p->vPrio, Prio, i )
//                if ( Prio >> p->nPrioShift  )
//                    Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
        }
        //if ( p->pPars->fUseAbs && p->vAbsFlops )
        //    printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
        p->nFrames = iFrame;
        assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
        p->iUseFrame = Abc_MaxInt(iFrame, 1);
        Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
        {
            // skip disproved outputs
            if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
                continue;
            // skip output whose time has run out
            if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
                continue;
            // check if the output is trivially solved
            if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
                continue;
            // check if the output is trivially solved
            if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
            {
                if ( !p->pPars->fSolveAll )
                {
                    pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
                    p->pAig->pSeqModel = pCexNew;
                    return 0; // SAT
                }
                pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                p->pPars->nFailOuts++;
                if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                if ( !p->pPars->fNotVerbose )
                Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
                    nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
                if ( p->pPars->fUseBridge )
                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
                if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                {
                    if ( p->pPars->fVerbose )
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
                    p->pPars->iFrame = iFrame;
                    return -1;
                }
                if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
                    return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
                p->pPars->timeLastSolved = Abc_Clock();
                continue;
            }
            // try to solve this output
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[p->iOutCur] > 0 );
                clkOne = Abc_Clock();
                p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
            }
            while ( 1 )
            {
                if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                {
                    if ( p->pPars->fVerbose )
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
                    p->pPars->iFrame = iFrame;
                    return -1;
                }
                RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
                if ( RetValue == 1 )
                    break;
                if ( RetValue == -1 )
                {
                    if ( p->pPars->fVerbose )
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                    if ( p->timeToStop && Abc_Clock() > p->timeToStop )
                        Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                    else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                        Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
                    else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
                    {
                        Pdr_QueueClean( p );
                        pCube = NULL;
                        break; // keep solving
                    }
                    else if ( p->pPars->nConfLimit )
                        Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
                    else if ( p->pPars->fVerbose )
                        Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
                    p->pPars->iFrame = iFrame;
                    return -1;
                }
                if ( RetValue == 0 )
                {
                    RetValue = Pdr_ManBlockCube( p, pCube );
                    if ( RetValue == -1 )
                    {
                        if ( p->pPars->fVerbose )
                            Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
                            Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                        else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                            Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
                        else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
                        {
                            Pdr_QueueClean( p );
                            pCube = NULL;
                            break; // keep solving
                        }
                        else if ( p->pPars->nConfLimit )
                            Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
                        else if ( p->pPars->fVerbose )
                            Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
                        p->pPars->iFrame = iFrame;
                        return -1;
                    }
                    if ( RetValue == 0 )
                    {
                        if ( fPrintClauses )
                        {
                            Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                            Pdr_ManPrintClauses( p, 0 );
                        }
                        if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
                            Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
                        p->pPars->iFrame = iFrame;
                        if ( !p->pPars->fSolveAll )
                        {
                            abctime clk = Abc_Clock();
                            Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
                            p->tAbs += Abc_Clock() - clk;
                            if ( pCex == NULL )
                            {
                                assert( p->pPars->fUseAbs );
                                Pdr_QueueClean( p );
                                pCube = NULL;
                                fRefined = 1;
                                break; // keep solving
                            }
                            p->pAig->pSeqModel = pCex;
 
                            if ( p->pPars->fVerbose && p->pPars->fUseAbs )
                                Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
                            return 0; // SAT
                        }
                        p->pPars->nFailOuts++;
                        pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                        if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                        assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
                        if ( p->pPars->fUseBridge )
                            Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
                        if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                        {
                            if ( p->pPars->fVerbose )
                                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                            if ( !p->pPars->fSilent )
                                Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
                            p->pPars->iFrame = iFrame;
                            return -1;
                        }
                        if ( !p->pPars->fNotVerbose )
                            Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
                                nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                        if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                            return 0; // all SAT
                        Pdr_QueueClean( p );
                        pCube = NULL;
                        break; // keep solving
                    }
                    if ( p->pPars->fVerbose )
                        Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
                }
            }
            if ( fRefined )
                break;
            if ( p->pTime4Outs )
            {
                abctime timeSince = Abc_Clock() - clkOne;
                assert( p->pTime4Outs[p->iOutCur] > 0 );
                p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
                if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
                {
                    p->pPars->nDropOuts++;
                    if ( p->pPars->vOutMap ) 
                        Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
                    if ( !p->pPars->fNotVerbose ) 
                        Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
                }
                p->timeToStopOne = 0;
            }
        }
        /*
        if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
        {
            int i, Used;
            Vec_IntForEachEntry( p->vAbsFlops, Used, i )
                if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
                    Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
        }
        */
        if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
        {
            Pdr_Set_t * pSet;
            int i, j, k;
            Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 );
            Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
                for ( k = 0; k < pSet->nLits; k++ )
                    Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
        }
 
        if ( p->pPars->fVerbose )
            Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
        if ( fRefined )
            continue;
        //if ( p->pPars->fUseAbs && p->vAbsFlops )
        //    printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
        // open a new timeframe
        p->nQueLim = p->pPars->nRestLimit;
        assert( pCube == NULL );
        Pdr_ManSetPropertyOutput( p, iFrame );
        Pdr_ManCreateSolver( p, ++iFrame );
        if ( fPrintClauses )
        {
            Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
            Pdr_ManPrintClauses( p, 0 );
        }
        // push clauses into this timeframe
        RetValue = Pdr_ManPushClauses( p );
        if ( RetValue == -1 )
        {
            if ( p->pPars->fVerbose )
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            if ( !p->pPars->fSilent )
            {
                if ( p->timeToStop && Abc_Clock() > p->timeToStop )
                    Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                else
                    Abc_Print( 1, "Reached conflict limit (%d) in frame.\n",  p->pPars->nConfLimit, iFrame );
            }
            p->pPars->iFrame = iFrame;
            return -1;
        }
        if ( RetValue )
        {
            if ( p->pPars->fVerbose )
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            if ( !p->pPars->fSilent )
                Pdr_ManReportInvariant( p );
            if ( !p->pPars->fSilent )
                Pdr_ManVerifyInvariant( p );
            p->pPars->iFrame = iFrame;
            // count the number of UNSAT outputs
            p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
            // convert previously 'unknown' into 'unsat'
            if ( p->pPars->vOutMap )
                for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
                    if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
                    {
                        Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
                        if ( p->pPars->fUseBridge )
                            Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
                    }
            if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
                return 1; // UNSAT
            if ( p->pPars->nFailOuts > 0 )
                return 0; // SAT
            return -1;
        }
        if ( p->pPars->fVerbose )
            Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
 
        // check termination
        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
        {
            p->pPars->iFrame = iFrame;
            return -1;
        }
        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
        {
            if ( fPrintClauses )
            {
                Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                Pdr_ManPrintClauses( p, 0 );
            }
            if ( p->pPars->fVerbose )
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            if ( !p->pPars->fSilent )
                Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
            p->pPars->iFrame = iFrame;
            return -1;
        }
        if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
        {
            if ( fPrintClauses )
            {
                Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                Pdr_ManPrintClauses( p, 0 );
            }
            if ( p->pPars->fVerbose )
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            if ( !p->pPars->fSilent )
                Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
            p->pPars->iFrame = iFrame;
            return -1;
        }
        if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
        {
            if ( p->pPars->fVerbose )
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
            if ( !p->pPars->fSilent )
                Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
            p->pPars->iFrame = iFrame;
            return -1;
        }
    }
    assert( 0 );
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_CallBackToStop()

int Wla_CallBackToStop ( int RunId )

extern

Definition at line 46 of file wlcPth.c.

{ assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }

Here is the caller graph for this function:

Wla_GetGlobalRunId()

int Wla_GetGlobalRunId ( )

extern

Definition at line 47 of file wlcPth.c.

{ return g_nRunIds; }

Here is the caller graph for this function:

Wla_ManBitBlast()

Aig_Man_t * Wla_ManBitBlast	(	Wla_Man_t *	pWla,
		Wlc_Ntk_t *	pAbs )

Definition at line 1398 of file wlcAbs.c.

{
    int nDcFlops;
    Gia_Man_t * pTemp;
    Aig_Man_t * pAig;
 
    pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
    // if the abstraction has flops with DC-init state,
    // new PIs were introduced by bit-blasting at the end of the PI list
    // here we move these variables to be *before* PPIs, because
    // PPIs are supposed to be at the end of the PI list for refinement
    nDcFlops = Wlc_NtkDcFlopNum(pAbs);
    if ( nDcFlops > 0 ) // DC-init flops are present
    {
        pWla->pGia = Gia_ManPermuteInputs( pTemp = pWla->pGia, Wlc_NtkCountObjBits(pWla->p, pWla->vBlacks), nDcFlops );
        Gia_ManStop( pTemp );
    }
    // if the word-level outputs have to be XORs, this is a place to do it
    if ( pWla->pPars->fXorOutput )
    {
        pWla->pGia = Gia_ManTransformMiter2( pTemp = pWla->pGia );
        Gia_ManStop( pTemp );
    }
    if ( pWla->pPars->fVerbose )
    {
        printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(pWla->vBlacks) ); 
        Gia_ManPrintStats( pWla->pGia, NULL );
    }
 
    // try to prove abstracted GIA by converting it to AIG and calling PDR
    pAig = Gia_ManToAigSimple( pWla->pGia );
 
    return pAig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManCheckCombUnsat()

int Wla_ManCheckCombUnsat	(	Wla_Man_t *	pWla,
		Aig_Man_t *	pAig )

Definition at line 1434 of file wlcAbs.c.

{
    Pdr_Man_t * pPdr;
    Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars;
    abctime clk;
    int RetValue = -1;
 
    if ( Aig_ManAndNum( pAig ) <= 20000 )
    { 
        Aig_Man_t * pAigScorr;
        Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
        int nAnds;
 
        clk = Abc_Clock();
 
        Ssw_ManSetDefaultParams( pScorrPars );
        pScorrPars->fStopWhenGone = 1;
        pScorrPars->nFramesK = 1;
        pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
        assert ( pAigScorr );
        nAnds = Aig_ManAndNum( pAigScorr); 
        Aig_ManStop( pAigScorr );
 
        if ( nAnds == 0 )
        {
            if ( pWla->pPars->fVerbose )
                Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk );
            return 1;
        }
        else if ( pWla->pPars->fVerbose )
        {
            Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
    }
 
    clk = Abc_Clock();
 
    pPdrPars->fVerbose = 0;
    pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
    RetValue = IPdr_ManCheckCombUnsat( pPdr );
    Pdr_ManStop( pPdr );
    pPdrPars->fVerbose = pWla->pPars->fPdrVerbose;
 
    pWla->tPdr += Abc_Clock() - clk;
 
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManCollectNodes()

Vec_Int_t * Wla_ManCollectNodes	(	Wla_Man_t *	pWla,
		int	fBlack )

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

Synopsis [Performs PDR with word-level abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 1330 of file wlcAbs.c.

{
    Vec_Int_t * vNodes = NULL;
    int i, Entry;
 
    assert( pWla->vSignals );
 
    vNodes = Vec_IntAlloc( 100 );
    Vec_IntForEachEntry( pWla->vSignals, Entry, i )
    {
        if ( !fBlack && Vec_BitEntry(pWla->vUnmark, Entry) )
            Vec_IntPush( vNodes, Entry );
        
        if ( fBlack && !Vec_BitEntry(pWla->vUnmark, Entry) )
            Vec_IntPush( vNodes, Entry );
    }
 
    return vNodes;
}

Here is the caller graph for this function:

Wla_ManConcurrentBmc3()

void Wla_ManConcurrentBmc3 ( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex )

extern

Definition at line 52 of file wlcPth.c.

{}

Here is the caller graph for this function:

Wla_ManCreateAbs()

Wlc_Ntk_t * Wla_ManCreateAbs

(

Wla_Man_t *

pWla

)

Definition at line 1379 of file wlcAbs.c.

{
    Wlc_Ntk_t * pAbs;
 
    // get abstracted GIA and the set of pseudo-PIs (vBlacks)
    if ( pWla->vBlacks == NULL )
    {
        pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
        pWla->vSignals = Vec_IntDup( pWla->vBlacks );
    }
    else
    {
        Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark, pWla->vSignals );
    }
    pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL );
 
    return pAbs;
}

Here is the caller graph for this function:

Wla_ManJoinThread()

void Wla_ManJoinThread ( Wla_Man_t * pWla, int RunId )

extern

Definition at line 51 of file wlcPth.c.

{}

Here is the caller graph for this function:

Wla_ManRefine()

void Wla_ManRefine

(

Wla_Man_t *

pWla

)

Definition at line 1570 of file wlcAbs.c.

{
    abctime clk;
    int nNodes;
    Vec_Int_t * vRefine = NULL;
 
    if ( pWla->fNewAbs )
    {
        if ( pWla->pCex )
            Abc_CexFree( pWla->pCex );
        pWla->pCex = NULL;
        Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
        return;
    }
 
    // perform refinement
    if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine )
    {
        clk = Abc_Clock();
        vRefine = Wlc_NtkAbsRefinement( pWla->p, pWla->pGia, pWla->pCex, pWla->vBlacks );
        pWla->tCbr += Abc_Clock() - clk;
    }
    else // proof-based only
    {
        vRefine = Vec_IntDup( pWla->vBlacks );
    }
    if ( pWla->pPars->fProofRefine ) 
    {
        clk = Abc_Clock();
        Wlc_NtkProofRefine( pWla->p, pWla->pPars, pWla->pCex, pWla->vBlacks, &vRefine );
        pWla->tPbr += Abc_Clock() - clk;
    }
 
    if ( pWla->vClauses && pWla->pPars->fVerbose )
    {
        int i;
        Vec_Ptr_t * vVec; 
        Vec_VecForEachLevel( pWla->vClauses, vVec, i )
            pWla->nTotalCla += Vec_PtrSize( vVec ); 
    }
 
    // update the set of objects to be un-abstracted
    clk = Abc_Clock();
    if ( pWla->pPars->fMFFC )
    {
        nNodes = Wlc_NtkRemoveFromAbstraction( pWla->p, vRefine, pWla->vUnmark );
        if ( pWla->pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pWla->pCex->iFrame, Vec_IntSize(vRefine), nNodes );
    }
    else
    {
        nNodes = Wlc_NtkUnmarkRefinement( pWla->p, vRefine, pWla->vUnmark );
        if ( pWla->pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pWla->pCex->iFrame, Vec_IntSize(vRefine) );
 
    }
    /*
    if ( pWla->pPars->fVerbose ) 
    {
        Wlc_NtkAbsAnalyzeRefine( pWla->p, pWla->vBlacks, pWla->vUnmark, &pWla->nDisj, &pWla->nNDisj );
        Abc_Print( 1, "Refine analysis (total): %d disjoint PPIs and %d non-disjoint PPIs\n", pWla->nDisj, pWla->nNDisj );
    }
    */
    pWla->tCbr += Abc_Clock() - clk;
    
    // Experimental
    /*
    if ( pWla->pCex->iFrame > 0 )
    {
        Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
        Vec_Bit_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
        Vec_IntFree( vWhites );
        Vec_BitFree( vCore );
    }
    */
 
    pWla->iCexFrame = pWla->pCex->iFrame;
 
    Vec_IntFree( vRefine );
    Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
    Abc_CexFree( pWla->pCex ); pWla->pCex = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManShrinkAbs()

int Wla_ManShrinkAbs	(	Wla_Man_t *	pWla,
		int	nFrames,
		int	RunId )

Definition at line 1350 of file wlcAbs.c.

{
    int i, Entry;
    int RetValue = 0;
 
    Vec_Int_t * vWhites = Wla_ManCollectNodes( pWla, 0 );
    Vec_Int_t * vBlacks = Wla_ManCollectNodes( pWla, 1 );
    Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites, vBlacks, RunId );
 
    if ( vCoreMarks == NULL )
    {
        Vec_IntFree( vWhites );
        Vec_IntFree( vBlacks );
        return -1;
    }
 
    RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
 
    Vec_IntForEachEntry( vWhites, Entry, i )
        if ( !Vec_BitEntry( vCoreMarks, i ) )
            Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
 
    Vec_IntFree( vWhites );
    Vec_IntFree( vBlacks );
    Vec_BitFree( vCoreMarks );
 
    return RetValue;
}

Here is the call graph for this function:

Wla_ManSolve()

int Wla_ManSolve	(	Wla_Man_t *	pWla,
		Wlc_Par_t *	pPars )

Definition at line 1698 of file wlcAbs.c.

{
    abctime clk = Abc_Clock();
    abctime tTotal;
    Wlc_Ntk_t * pAbs = NULL;
    Aig_Man_t * pAig = NULL;
 
    int RetValue = -1;
 
    // perform refinement iterations
    for ( pWla->nIters = 1; pWla->nIters < pPars->nIterMax; ++pWla->nIters )
    {
        if ( pPars->fVerbose )
            printf( "\nIteration %d:\n", pWla->nIters );
 
        pAbs = Wla_ManCreateAbs( pWla );
 
        pAig = Wla_ManBitBlast( pWla, pAbs );
        Wlc_NtkFree( pAbs );
 
        RetValue = Wla_ManSolveInt( pWla, pAig );
        Aig_ManStop( pAig );
 
        if ( RetValue != -1 || (pPars->pFuncStop && pPars->pFuncStop( pPars->RunId)) )
            break;
 
        Wla_ManRefine( pWla );
    }
 
    // report the result
    if ( pPars->fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 )
        printf( "resulted in a real CEX" );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", pWla->nIters );
    tTotal = Abc_Clock() - clk;
    Abc_PrintTime( 1, "Time", tTotal );
 
    if ( pPars->fVerbose )
        Abc_Print( 1, "PDRA reused %d clauses.\n", pWla->nTotalCla );
    if ( pPars->fVerbose )
    {
        ABC_PRTP( "PDR          ", pWla->tPdr,                          tTotal );
        ABC_PRTP( "CEX Refine   ", pWla->tCbr,                          tTotal );
        ABC_PRTP( "Proof Refine ", pWla->tPbr,                          tTotal );
        ABC_PRTP( "Misc.        ", tTotal - pWla->tPdr - pWla->tCbr - pWla->tPbr,   tTotal );
        ABC_PRTP( "Total        ", tTotal,                              tTotal );
    }
 
    return RetValue;
} 

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManSolveInt()

int Wla_ManSolveInt	(	Wla_Man_t *	pWla,
		Aig_Man_t *	pAig )

Definition at line 1483 of file wlcAbs.c.

{
    abctime clk;
    Pdr_Man_t * pPdr;
    Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars;
    Abc_Cex_t * pBmcCex = NULL;
    Abc_Cex_t * pCexReal = NULL;
    int RetValue = -1;
    int RunId = Wla_GetGlobalRunId();
 
    if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat )
    {
        clk = Abc_Clock();
 
        RetValue = Wla_ManCheckCombUnsat( pWla, pAig );
        if ( RetValue == 1 )
        {
            if ( pWla->pPars->fVerbose )
                Abc_PrintTime( 1,  "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk );
            return 1;
        }
 
        if ( pWla->pPars->fVerbose )
            Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk );
    }
 
    if ( pWla->pPars->fUseBmc3 )
    {
        pPdrPars->RunId = RunId;
        pPdrPars->pFuncStop = Wla_CallBackToStop;
 
        Wla_ManConcurrentBmc3( pWla, Aig_ManDupSimple(pAig), &pBmcCex );
    }
 
    clk = Abc_Clock();
    pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
    if ( pWla->vClauses ) {
        assert( Vec_VecSize( pWla->vClauses) >= 2 ); 
        
        if ( pWla->fNewAbs )
            IPdr_ManRebuildClauses( pPdr, pWla->pPars->fShrinkScratch ? NULL : pWla->vClauses );
        else
            IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
 
        pWla->fNewAbs = 0;
    }
 
    RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses );
    pPdr->tTotal += Abc_Clock() - clk;
    pWla->tPdr += pPdr->tTotal;
    if ( pWla->pPars->fLoadTrace)
        pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 );
    Pdr_ManStop( pPdr );
 
 
    if ( pWla->pPars->fUseBmc3 )
        Wla_ManJoinThread( pWla, RunId );
 
    if ( pBmcCex )
    {
        pWla->pCex = pBmcCex ;
    }
    else
    {
        pWla->pCex = pAig->pSeqModel;
        pAig->pSeqModel = NULL;
    }
 
    // consider outcomes
    if ( pWla->pCex == NULL ) 
    {
        assert( RetValue ); // proved or undecided
        return RetValue;
    }
 
    // verify CEX
    pCexReal = Wlc_NtkCexIsReal( pWla->p, pWla->pCex );
    if ( pCexReal )
    {
        Abc_CexFree( pWla->pCex );
        pWla->pCex = pCexReal; 
        return 0;
    }
 
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManStart()

Wla_Man_t * Wla_ManStart	(	Wlc_Ntk_t *	pNtk,
		Wlc_Par_t *	pPars )

Definition at line 1653 of file wlcAbs.c.

{
    Wla_Man_t * p = ABC_CALLOC( Wla_Man_t, 1 );
    Pdr_Par_t * pPdrPars;
    p->p = pNtk;
    p->pPars = pPars;
    p->vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(pNtk) );
 
    pPdrPars = ABC_CALLOC( Pdr_Par_t, 1 );
    Pdr_ManSetDefaultParams( pPdrPars );
    pPdrPars->fVerbose   = pPars->fPdrVerbose;
    pPdrPars->fVeryVerbose = 0;
    pPdrPars->pFuncStop  = pPars->pFuncStop;
    pPdrPars->RunId      = pPars->RunId;
    if ( pPars->fPdra )
    {
        pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
        pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
        pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
        pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
    } 
    p->pPdrPars = (void *)pPdrPars;
 
    p->iCexFrame = 0;
    p->fNewAbs   = 0;
 
    p->nIters    = 1;
    p->nTotalCla = 0;
    p->nDisj     = 0;
    p->nNDisj    = 0;
 
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wla_ManStop()

void Wla_ManStop

(

Wla_Man_t *

p

)

Definition at line 1687 of file wlcAbs.c.

{
    if ( p->vBlacks )   Vec_IntFree( p->vBlacks );
    if ( p->vSignals )  Vec_IntFree( p->vSignals );
    if ( p->pGia )      Gia_ManStop( p->pGia );
    if ( p->pCex )      Abc_CexFree( p->pCex );
    Vec_BitFree( p->vUnmark );
    ABC_FREE( p->pPdrPars );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkAbsAnalyzeRefine()

void Wlc_NtkAbsAnalyzeRefine	(	Wlc_Ntk_t *	p,
		Vec_Int_t *	vBlacks,
		Vec_Bit_t *	vUnmark,
		int *	nDisj,
		int *	nNDisj )

Definition at line 129 of file wlcAbs.c.

{
    Vec_Bit_t * vCurCis, * vCandCis;
    Vec_Int_t * vSuppList;
    Vec_Int_t * vDeltaB;
    Vec_Int_t * vSuppRefs;
    int i, Entry;
    Wlc_Obj_t * pObj;
    
    vCurCis    = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
    vCandCis   = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
    vDeltaB    = Vec_IntAlloc( Vec_IntSize(vBlacks) );
    vSuppList  = Vec_IntAlloc( Wlc_NtkCiNum(p) + Vec_IntSize(vBlacks) );
    vSuppRefs  = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) );
 
 
    Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 );
 
    Wlc_NtkForEachCi( p, pObj, i )
    {
        Vec_BitWriteEntry( vCurCis, Wlc_ObjId(p, pObj), 1 ) ;
        Vec_BitWriteEntry( vCandCis, Wlc_ObjId(p, pObj), 1 ) ;
    }
 
    Vec_IntForEachEntry( vBlacks, Entry, i )
    {
        Vec_BitWriteEntry( vCurCis, Entry, 1 );
        if ( !Vec_BitEntry( vUnmark, Entry ) )
            Vec_BitWriteEntry( vCandCis, Entry, 1 );
        else
            Vec_IntPush( vDeltaB, Entry );
    }
    assert( Vec_IntSize( vDeltaB ) );
    
    Wlc_NtkForEachCo( p, pObj, i )
        Wlc_NtkAbsGetSupp( p, pObj, vCurCis, vSuppRefs, NULL );
    
    /*
    Abc_Print( 1, "SuppCurrentAbs =" );
    Wlc_NtkForEachObj( p, pObj, i )
        if ( Vec_IntEntry(vSuppRefs, i) > 0 )
            Abc_Print( 1, " %d", i );
    Abc_Print( 1, "\n" );
    */
 
    Vec_IntForEachEntry( vDeltaB, Entry, i )
        Wlc_NtkAbsGetSupp( p, Wlc_NtkObj(p, Entry), vCandCis, vSuppRefs, NULL );
 
    Vec_IntForEachEntry( vDeltaB, Entry, i )
    {
        int iSupp, ii;
        int fDisjoint = 1;
 
        Vec_IntClear( vSuppList );
        Wlc_NtkAbsGetSupp( p, Wlc_NtkObj(p, Entry), vCandCis, NULL, vSuppList );
 
        //Abc_Print( 1, "SuppCandAbs =" );
        Vec_IntForEachEntry( vSuppList, iSupp, ii )
        {
            //Abc_Print( 1, " %d(%d)", iSupp, Vec_IntEntry( vSuppRefs, iSupp ) );
            if ( Vec_IntEntry( vSuppRefs, iSupp ) >= 2 )
            {
                fDisjoint = 0;
                break;
            }
        }
        //Abc_Print( 1, "\n" );
        
        if ( fDisjoint )
        {
            //Abc_Print( 1, "PPI[%d] is disjoint.\n", Entry );
            ++(*nDisj);
        }
        else 
        {
            //Abc_Print( 1, "PPI[%d] is non-disjoint.\n", Entry );
            ++(*nNDisj);
        }
    }
 
    Vec_BitFree( vCurCis );
    Vec_BitFree( vCandCis );
    Vec_IntFree( vDeltaB );
    Vec_IntFree( vSuppList );
    Vec_IntFree( vSuppRefs );
}

Here is the call graph for this function:

Wlc_NtkAbsCore()

int Wlc_NtkAbsCore	(	Wlc_Ntk_t *	p,
		Wlc_Par_t *	pPars )

FUNCTION DECLARATIONS ///.

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

Synopsis [Performs abstraction.]

Description [Derives initial abstraction based on user-specified parameter values, which tell what is the smallest bit-width of a primitive that is being abstracted away. Currently only add/sub, mul/div, mux, and flop are supported with individual parameters. The second step is to refine the initial abstraction until the point when the property is proved.]

SideEffects []

SeeAlso []

Definition at line 1786 of file wlcAbs.c.

{
    abctime clk = Abc_Clock();
    Vec_Int_t * vBlacks = NULL;
    int nIters, nNodes, nDcFlops, RetValue = -1;
    // start the bitmap to mark objects that cannot be abstracted because of refinement
    // currently, this bitmap is empty because abstraction begins without refinement
    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
    // set up parameters to run PDR
    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
    Pdr_ManSetDefaultParams( pPdrPars );
    //pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
    //pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
    //pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
    //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
    pPdrPars->fVerbose   = pPars->fPdrVerbose;
    pPdrPars->fVeryVerbose = 0;
    // perform refinement iterations
    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
    {
        Aig_Man_t * pAig;
        Abc_Cex_t * pCex;
        Vec_Int_t * vPisNew, * vRefine;  
        Gia_Man_t * pGia, * pTemp;
        Wlc_Ntk_t * pAbs;
 
        if ( pPars->fVerbose )
            printf( "\nIteration %d:\n", nIters );
 
        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
        if ( pPars->fAbs2 )
        {
            if ( vBlacks == NULL )
                vBlacks = Wlc_NtkGetBlacks( p, pPars );
            else
                Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark, NULL );
            pAbs = Wlc_NtkAbs2( p, vBlacks, NULL );
            vPisNew = Vec_IntDup( vBlacks );
        }
        else
        {
            if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
                Wlc_NtkSetUnmark( p, pPars, vUnmark );
 
            pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
        }
        pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
        // if the abstraction has flops with DC-init state,
        // new PIs were introduced by bit-blasting at the end of the PI list
        // here we move these variables to be *before* PPIs, because
        // PPIs are supposed to be at the end of the PI list for refinement
        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
        if ( nDcFlops > 0 ) // DC-init flops are present
        {
            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
            Gia_ManStop( pTemp );
        }
        // if the word-level outputs have to be XORs, this is a place to do it
        if ( pPars->fXorOutput )
        {
            pGia = Gia_ManTransformMiter2( pTemp = pGia );
            Gia_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
        {
            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
            Gia_ManPrintStats( pGia, NULL );
        }
        Wlc_NtkFree( pAbs );
 
        // try to prove abstracted GIA by converting it to AIG and calling PDR
        pAig = Gia_ManToAigSimple( pGia );
        RetValue = Pdr_ManSolve( pAig, pPdrPars );
        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
        Aig_ManStop( pAig );
 
        // consider outcomes
        if ( pCex == NULL ) 
        {
            assert( RetValue ); // proved or undecided
            Gia_ManStop( pGia );
            Vec_IntFree( vPisNew );
            break;
        }
 
        // perform refinement
        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
        Gia_ManStop( pGia );
        Vec_IntFree( vPisNew );
        if ( vRefine == NULL ) // real CEX
        {
            Abc_CexFree( pCex ); // return CEX in the future
            break;
        }
 
        // update the set of objects to be un-abstracted
        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
        if ( pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
        Vec_IntFree( vRefine );
        Abc_CexFree( pCex );
    }
    Vec_IntFreeP( &vBlacks );
    Vec_BitFreeP( &vUnmark );
    // report the result
    if ( pPars->fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 )
        printf( "resulted in a real CEX" );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", nIters );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkAbsGetSupp()

void Wlc_NtkAbsGetSupp	(	Wlc_Ntk_t *	p,
		Wlc_Obj_t *	pObj,
		Vec_Bit_t *	vCiMarks,
		Vec_Int_t *	vSuppRefs,
		Vec_Int_t *	vSuppList )

Definition at line 110 of file wlcAbs.c.

{
    assert( vSuppRefs || vSuppList );
    Wlc_NtkCleanMarks( p );
 
    Wlc_NtkAbsGetSupp_rec( p, pObj, vCiMarks, vSuppRefs, vSuppList );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkAbsGetSupp_rec()

void Wlc_NtkAbsGetSupp_rec	(	Wlc_Ntk_t *	p,
		Wlc_Obj_t *	pObj,
		Vec_Bit_t *	vCiMarks,
		Vec_Int_t *	vSuppRefs,
		Vec_Int_t *	vSuppList )

Definition at line 91 of file wlcAbs.c.

{
    int i, iFanin, iObj;
    if ( pObj->Mark ) // visited
        return;
    pObj->Mark = 1;
    iObj = Wlc_ObjId( p, pObj );
    if ( Vec_BitEntry( vCiMarks, iObj ) )
    {
        if ( vSuppRefs )
            Vec_IntAddToEntry( vSuppRefs, iObj, 1 );
        if ( vSuppList )
            Vec_IntPush( vSuppList, iObj );
        return;
    }
    Wlc_ObjForEachFanin( pObj, iFanin, i )
        Wlc_NtkAbsGetSupp_rec( p, Wlc_NtkObj(p, iFanin), vCiMarks, vSuppRefs, vSuppList );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkFlopsRemap()

Vec_Int_t * Wlc_NtkFlopsRemap	(	Wlc_Ntk_t *	p,
		Vec_Int_t *	vFfOld,
		Vec_Int_t *	vFfNew )

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

Synopsis [Computes the map for remapping flop IDs used in the clauses.]

Description [Takes the original network (Wlc_Ntk_t) and the array of word-level flops used in the old abstraction (vFfOld) and those used in the new abstraction (vFfNew). Returns the integer map, which remaps every binary flop found in the old abstraction into a binary flop found in the new abstraction.]

SideEffects []

SeeAlso []

Definition at line 1284 of file wlcAbs.c.

{
    Vec_Int_t * vMap = Vec_IntAlloc( 1000 );             // the resulting map
    Vec_Int_t * vMapFfNew2Bit1 = Vec_IntAlloc( 1000 );   // first binary bit of each new word-level flop
    int i, b, iFfOld, iFfNew, iBit1New, nBits = 0;
    // map object IDs of old flops into their flop indexes
    Vec_Int_t * vMapFfObj2FfId = Vec_IntStartFull( Wlc_NtkObjNumMax(p) );
    Vec_IntForEachEntry( vFfNew, iFfNew, i )
        Vec_IntWriteEntry( vMapFfObj2FfId, iFfNew, i );
    // map each new flop index into its first bit
    Vec_IntForEachEntry( vFfNew, iFfNew, i )
    {
        Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfNew );
        int nRange = Wlc_ObjRange( pObj );
        Vec_IntPush( vMapFfNew2Bit1, nBits );
        nBits += nRange;
    }
    assert( Vec_IntSize(vMapFfNew2Bit1) == Vec_IntSize(vFfNew) );
    // remap old binary flops into new binary flops
    Vec_IntForEachEntry( vFfOld, iFfOld, i )
    {
        Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfOld );
        int nRange = Wlc_ObjRange( pObj );
        iFfNew = Vec_IntEntry( vMapFfObj2FfId, iFfOld );
        assert( iFfNew >= 0 ); // every old flop should be present in the new abstraction
        // find the first bit of this new flop
        iBit1New = Vec_IntEntry( vMapFfNew2Bit1, iFfNew );
        for ( b = 0; b < nRange; b++ )
            Vec_IntPush( vMap, iBit1New + b );
    }
    Vec_IntFree( vMapFfNew2Bit1 );
    Vec_IntFree( vMapFfObj2FfId );
    return vMap;
}

Wlc_NtkIntroduceChoices()

Wlc_Ntk_t * Wlc_NtkIntroduceChoices	(	Wlc_Ntk_t *	pNtk,
		Vec_Int_t *	vBlacks,
		Vec_Int_t *	vPPIs )

Definition at line 435 of file wlcAbs.c.

{
    //if ( vBlacks== NULL ) return NULL;
    Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj;
    int i, k, iObj, iFanin;
    Vec_Int_t * vFanins = Vec_IntAlloc( 3 );
    Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
    Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
    int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
    Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
    Vec_Bit_t * vPPIMark = NULL;
 
    Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) 
    {
        // TODO : fix FOs here
        Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
    }
 
    if ( vPPIs )
    {
        vPPIMark = Vec_BitStart( Wlc_NtkObjNumMax(pNtk) );
        Wlc_NtkForEachObjVec( vPPIs, pNtk, pObj, i ) 
        {
            Vec_IntWriteEntry(vPPIs, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
            Vec_BitWriteEntry( vPPIMark, Vec_IntEntry(vPPIs, i), 1 );
        }
    }
 
    // Vec_IntPrint(vNodes);
    Wlc_NtkCleanCopy( p );
 
    // mark nodes
    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
    {
        iObj = Wlc_ObjId(p, pObj);
        pObj->Mark = 1;
        // add fresh PI with the same number of bits
        Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
    }
 
    if ( vPPIs )
    {
        Wlc_NtkForEachObjVec( vPPIs, p, pObj, i ) 
        {
            iObj = Wlc_ObjId(p, pObj);
            pObj->Mark = 1;
            // add fresh PI with the same number of bits
            Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
        }
    }
 
    // add sel PI
    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
    {
        iObj = Wlc_ObjId( p, pObj );
        Vec_IntWriteEntry( vMapNode2Sel, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0 ) );
    }
 
    // iterate through the nodes in the DFS order
    Wlc_NtkForEachObj( p, pObj, i )
    {
        int isSigned, range;
        if ( i == nOrigObjNum ) 
        {
            // cout << "break at " << i << endl;
            break;
        }
 
        // update fanins
        Wlc_ObjForEachFanin( pObj, iFanin, k )
            Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
        // node to remain
        iObj = i;
 
        if ( pObj->Mark ) 
        {
            // clean
            pObj->Mark = 0;
 
            if ( vPPIMark && Vec_BitEntry(vPPIMark, i) )
                iObj = Vec_IntEntry( vMapNode2Pi, i );
            else
            {
                isSigned = Wlc_ObjIsSigned(pObj);
                range = Wlc_ObjRange(pObj);
                Vec_IntClear(vFanins);
                Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
                Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
                Vec_IntPush(vFanins, i);
                iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
            }
        }
        
        Wlc_ObjSetCopy( p, i, iObj );
    }
 
    Wlc_NtkForEachCo( p, pObj, i )
    {
        iObj = Wlc_ObjId(p, pObj);
        if (iObj != Wlc_ObjCopy(p, iObj)) 
        {
            if (pObj->fIsFi)
                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
            else
                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
 
            Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
        }
    }
 
    // DumpWlcNtk(p);
    pNew = Wlc_NtkDupDfsSimple( p );
 
    if ( vPPIMark )
        Vec_BitFree( vPPIMark );
    Vec_IntFree( vFanins );
    Vec_IntFree( vMapNode2Pi );
    Vec_IntFree( vMapNode2Sel );
    Vec_IntFree( vNodes );
    Wlc_NtkFree( p );
 
    return pNew;
}

Here is the call graph for this function:

Wlc_NtkNumPiBits()

int Wlc_NtkNumPiBits

(

Wlc_Ntk_t *

pNtk

)

Definition at line 118 of file wlcAbs.c.

{
    int num = 0;
    int i;
    Wlc_Obj_t * pObj;
    Wlc_NtkForEachPi(pNtk, pObj, i) {
        num += Wlc_ObjRange(pObj);
    }
    return num;
}

Wlc_NtkPdrAbs()

int Wlc_NtkPdrAbs	(	Wlc_Ntk_t *	p,
		Wlc_Par_t *	pPars )

Definition at line 1755 of file wlcAbs.c.

{
    Wla_Man_t * pWla = NULL;
    
    int RetValue = -1;
 
    pWla = Wla_ManStart( p, pPars );
 
    RetValue = Wla_ManSolve( pWla, pPars );
 
    Wla_ManStop( pWla );
    
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkPrintNtk()

void Wlc_NtkPrintNtk

(

Wlc_Ntk_t *

p

)

FUNCTION DEFINITIONS ///.

Definition at line 62 of file wlcAbs.c.

{
    int i;
    Wlc_Obj_t * pObj;
 
    Abc_Print( 1, "PIs:");
    Wlc_NtkForEachPi( p, pObj, i )
        Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
    Abc_Print( 1, "\n\n");
 
    Abc_Print( 1, "POs:");
    Wlc_NtkForEachPo( p, pObj, i )
        Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
    Abc_Print( 1, "\n\n");
 
    Abc_Print( 1, "FO(Fi)s:");
    Wlc_NtkForEachCi( p, pObj, i )
        if ( !Wlc_ObjIsPi( pObj ) )
            Abc_Print( 1, " %s(%s)", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
    Abc_Print( 1, "\n\n");
 
    Abc_Print( 1, "Objs:\n");
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( !Wlc_ObjIsCi(pObj) )
           Wlc_NtkPrintNode( p, pObj ) ;
    }
}

Here is the call graph for this function: