bmc.h File Reference

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

Go to the source code of this file.

Data Structures
struct	Saig_ParBmc_t_
struct	Bmc_AndPar_t_
struct	Bmc_BCorePar_t_
struct	Bmc_MulPar_t_
struct	Bmc_ParFf_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Unr_Man_t_	Unr_Man_t
	INCLUDES ///. More...
typedef struct Saig_ParBmc_t_	Saig_ParBmc_t
typedef struct Bmc_AndPar_t_	Bmc_AndPar_t
typedef struct Bmc_BCorePar_t_	Bmc_BCorePar_t
typedef struct Bmc_MulPar_t_	Bmc_MulPar_t
typedef struct Bmc_ParFf_t_	Bmc_ParFf_t

Functions
void	Bmc_ManBCorePerform (Gia_Man_t *pGia, Bmc_BCorePar_t *pPars)
	MACRO DEFINITIONS ///. More...
int	Saig_ManBmcSimple (Aig_Man_t *pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit)
int	Saig_BmcPerform (Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
void	Saig_ParBmcSetDefaultParams (Saig_ParBmc_t *p)
int	Saig_ManBmcScalable (Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
int	Gia_ManBmcPerform (Gia_Man_t *p, Bmc_AndPar_t *pPars)
Abc_Cex_t *	Bmc_CexCareMinimize (Aig_Man_t *p, Abc_Cex_t *pCex, int fCheck, int fVerbose)
void	Bmc_CexCareVerify (Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Gia_Man_t *	Bmc_GiaTargetStates (Gia_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose)
Aig_Man_t *	Bmc_AigTargetStates (Aig_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose)
Abc_Cex_t *	Saig_ManCexMinPerform (Aig_Man_t *pAig, Abc_Cex_t *pCex)
void	Bmc_CexPrint (Abc_Cex_t *pCex, int nInputs, int fVerbose)
int	Bmc_CexVerify (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
void	Bmc_PerformICheck (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose)
Vec_Int_t *	Bmc_PerformISearch (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose)
Unr_Man_t *	Unr_ManUnrollStart (Gia_Man_t *pGia, int fVerbose)
Gia_Man_t *	Unr_ManUnrollFrame (Unr_Man_t *p, int f)
void	Unr_ManFree (Unr_Man_t *p)

Typedef Documentation

typedef struct Bmc_AndPar_t_ Bmc_AndPar_t

Definition at line 78 of file bmc.h.

typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t

Definition at line 98 of file bmc.h.

typedef struct Bmc_MulPar_t_ Bmc_MulPar_t

Definition at line 109 of file bmc.h.

typedef struct Bmc_ParFf_t_ Bmc_ParFf_t

Definition at line 123 of file bmc.h.

typedef struct Saig_ParBmc_t_ Saig_ParBmc_t

Definition at line 45 of file bmc.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Unr_Man_t_ Unr_Man_t

INCLUDES ///.

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

FileName [bmc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 43 of file bmc.h.

Function Documentation

Aig_Man_t* Bmc_AigTargetStates	(	Aig_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	iFrBeg,
		int	iFrEnd,
		int	fCombOnly,
		int	fUseOne,
		int	fAllFrames,
		int	fVerbose
	)

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

Synopsis [Generate AIG for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file bmcCexCut.c.

{
    Aig_Man_t * pAig;
    Gia_Man_t * pGia, * pRes;
    pGia = Gia_ManFromAigSimple( p );
    if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) )
    {
        Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); 
        Gia_ManStop( pGia );
        return NULL;
    }
    pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose );
    Gia_ManStop( pGia );
    pAig = Gia_ManToAigSimple( pRes );
    Gia_ManStop( pRes );
    return pAig;
}

Abc_Cex_t* Bmc_CexCareMinimize	(	Aig_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	fCheck,
		int	fVerbose
	)

Definition at line 255 of file bmcCexCare.c.

{
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, pCex, fCheck, fVerbose );
    Gia_ManStop( pGia );
    return pCexMin;
}

void Bmc_CexCareVerify	(	Aig_Man_t *	p,
		Abc_Cex_t *	pCex,
		Abc_Cex_t *	pCexMin,
		int	fVerbose
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file bmcCexCare.c.

{
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    if ( fVerbose )
    {
        printf( "Original :    " );
        Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
        printf( "Minimized:    " );
        Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
    }
    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
        printf( "Counter-example verification has failed.\n" );
    else 
        printf( "Counter-example verification succeeded.\n" );
    Gia_ManStop( pGia );
}

void Bmc_CexPrint	(	Abc_Cex_t *	pCex,
		int	nInputs,
		int	fVerbose
	)

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

Synopsis [Prints one counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file bmcCexTools.c.

{
    int i, k, Count, iBit = pCex->nRegs;
    Abc_CexPrintStatsInputs( pCex, nInputs );
    if ( !fVerbose )
        return;

    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Count = 0;
        printf( "%3d : ", i );
        for ( k = 0; k < nInputs; k++ )
        {
            Count += Abc_InfoHasBit(pCex->pData, iBit);
            printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
        }
        printf( " %3d ", Count );
        Count = 0;
        for (      ; k < pCex->nPis; k++ )
        {
            Count += Abc_InfoHasBit(pCex->pData, iBit);
            printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
        }
        printf( " %3d\n", Count );
    }
    assert( iBit == pCex->nBits );
}

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

Gia_Man_t* Bmc_GiaTargetStates	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	iFrBeg,
		int	iFrEnd,
		int	fCombOnly,
		int	fUseOne,
		int	fAllFrames,
		int	fVerbose
	)

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

Synopsis [Generate GIA for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 461 of file bmcCexCut.c.

{
    Gia_Man_t * pNew, * pTemp;
    Vec_Bit_t * vInitNew;

    if ( iFrBeg < 0 )
        { printf( "Starting frame is less than 0.\n" ); return NULL; }
    if ( iFrEnd < 0 )
        { printf( "Stopping frame is less than 0.\n" ); return NULL; }
    if ( iFrBeg > pCex->iFrame )
        { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
    if ( iFrEnd > pCex->iFrame )
        { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
    if ( iFrBeg > iFrEnd )
        { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
    assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
    assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
    assert( iFrBeg < iFrEnd );

    if ( fUseOne )
        pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
    else if ( fAllFrames )
        pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd );
    else 
        pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );

    if ( !fCombOnly )
    {
        // create new GIA
        pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); 
        Gia_ManStop( pTemp );

        // create new initial state
        pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
        Gia_ManStop( pTemp );
    }

    Vec_BitFree( vInitNew );
    return pNew;
}

void Bmc_ManBCorePerform	(	Gia_Man_t *	p,
		Bmc_BCorePar_t *	pPars
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file bmcBCore.c.

{
    clock_t clk = clock();
    Intp_Man_t * pManProof;
    Vec_Int_t * vVarMap, * vCore;
    sat_solver * pSat;
    FILE * pFile;
    void * pSatCnf; 
    int RetValue;
    // create SAT solver
    pSat = sat_solver_new();
    sat_solver_store_alloc( pSat ); 
    sat_solver_setnvars( pSat, 1000 );
    sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat );
    sat_solver_store_mark_roots( pSat ); 
    // create pivot variables
    if ( pPars->pFilePivots )
    {
        Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap);
        sat_solver_set_pivot_variables( pSat, Vec_IntArray(vPivots), Vec_IntSize(vPivots) );
        Vec_IntReleaseArray( vPivots );
        Vec_IntFree( vPivots );
    }
    // solve the problem
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_Undef )
    {
        Vec_IntFree( vVarMap );
        sat_solver_delete( pSat );
        printf( "Timeout of conflict limit is reached.\n" );
        return;
    }
    if ( RetValue == l_True )
    {
        Vec_IntFree( vVarMap );
        sat_solver_delete( pSat );
        printf( "The BMC problem is SAT.\n" );
        return;
    }
    if ( pPars->fVerbose )
    {
        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    assert( RetValue == l_False );
    pSatCnf = sat_solver_store_release( pSat ); 
//    Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" );
    // derive the UNSAT core
    clk = clock();
    pManProof = Intp_ManAlloc();
    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 1, pPars->fVerbose );
    Intp_ManFree( pManProof );
    if ( pPars->fVerbose )
    {
        printf( "UNSAT core contains %d (out of %d) learned clauses.   ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    // write the problem
    Vec_IntSort( vCore, 0 );
    pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
    Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
    if ( pFile != stdout )
        fclose( pFile );
    // cleanup
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
    Vec_IntFree( vVarMap );
    Vec_IntFree( vCore );
    sat_solver_delete( pSat );
}

void Bmc_PerformICheck	(	Gia_Man_t *	p,
		int	nFramesMax,
		int	nTimeOut,
		int	fEmpty,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file bmcICheck.c.

{
    int fUseOldCnf = 0;
    Gia_Man_t * pMiter, * pTemp;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Vec_Int_t * vLits, * vUsed;
    int i, status, Lit;
    int nLitsUsed, nLits, * pLits;
    abctime clkStart = Abc_Clock();
    assert( nFramesMax > 0 );
    assert( Gia_ManRegNum(p) > 0 );

    if ( fVerbose )
    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );

    // create miter
    pTemp = Gia_ManDup( p );
    pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
    Gia_ManStop( pTemp );
    assert( Gia_ManPoNum(pMiter)  == 2 * Gia_ManPoNum(p) );
    assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
    // derive CNF
    if ( fUseOldCnf )
        pCnf = Cnf_DeriveGiaRemapped( pMiter );
    else
    {
        pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
        Gia_ManStop( pTemp );
        pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
    }

    // collect positive literals
    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );

    // iteratively compute a minimal M-inductive set of next-state functions
    nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
    vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
    while ( 1 )
    {
        int fChanges = 0;
        // derive SAT solver        
        pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
//        sat_solver_bookmark( pSat );
        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
            printf( "Timeout reached after %d seconds.\n", nTimeOut );
            break;
        }
        if ( status == l_True )
        {
            printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
            break;
        }
        assert( status == l_False );
        // call analize_final
        nLits = sat_solver_final( pSat, &pLits );
        // mark used literals
        Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
        for ( i = 0; i < nLits; i++ )
            Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );

        // check if there are any positive unused
        Vec_IntForEachEntry( vLits, Lit, i )
        {
            assert( i == Abc_Lit2Var(Lit) );
            if ( Abc_LitIsCompl(Lit) )
                continue;
            if ( Vec_IntEntry(vUsed, i) )
                continue;
            // positive literal became unused
            Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
            nLitsUsed--;
            fChanges = 1;
        }
        // report the results
        if ( fVerbose )
        printf( "M =%4d :  AIG =%8d.  SAT vars =%8d.  SAT conf =%8d.  S =%6d. (%6.2f %%)  ",
            nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), 
            Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), 
            sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
        if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
        // count the number of negative literals
        sat_solver_delete( pSat );
        if ( !fChanges || fEmpty )
            break;
//        break;
//        sat_solver_rollback( pSat );
    }
    Cnf_DataFree( pCnf );
    Gia_ManStop( pMiter );
    Vec_IntFree( vLits );
    Vec_IntFree( vUsed );
}

Vec_Int_t* Bmc_PerformISearch	(	Gia_Man_t *	p,
		int	nFramesMax,
		int	nTimeOut,
		int	fReverse,
		int	fDump,
		int	fVerbose
	)

Definition at line 417 of file bmcICheck.c.

{
    Vec_Int_t * vLits, * vFlops;
    int i, f;
    if ( fVerbose )
    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
    fflush( stdout );

    // collect positive literals
    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );

    for ( f = 1; f <= nFramesMax; f++ )
        if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits ) )
        {
            Vec_IntFree( vLits );
            return NULL;
        }

    // dump the numbers of the flops
    if ( fDump )
    {
        int nLitsUsed = 0;
        for ( i = 0; i < Gia_ManRegNum(p); i++ )
            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
                nLitsUsed++;
        printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
        for ( i = 0; i < Gia_ManRegNum(p); i++ )
            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
                printf( "%d ", i );
        printf( "\n" );
    }       
    // save flop indexes
    vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
            Vec_IntPush( vFlops, 1 );
        else
            Vec_IntPush( vFlops, 0 );
    Vec_IntFree( vLits );
    return vFlops;
}

int Gia_ManBmcPerform	(	Gia_Man_t *	pGia,
		Bmc_AndPar_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1066 of file bmcBmcAnd.c.

{
    abctime TimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
    if ( pPars->nFramesAdd == 0 )
        return Gia_ManBmcPerformInt( pGia, pPars );
    // iterate over the engine until we read the global timeout
    assert( pPars->nTimeOut >= 0 );
    while ( 1 )
    {
        if ( TimeToStop && TimeToStop < Abc_Clock() )
            return -1;
        if ( Gia_ManBmcPerformInt( pGia, pPars ) == 0 )
            return 0;
        // set the new runtime limit
        if ( pPars->nTimeOut )
        {
            pPars->nTimeOut = Abc_MinInt( pPars->nTimeOut-1, (int)((TimeToStop - Abc_Clock()) / CLOCKS_PER_SEC) );
            if ( pPars->nTimeOut <= 0 )
                return -1;
        }
        else
            return -1;
        // set the new frames limit
        pPars->nFramesAdd *= 2;
    }
    return -1;
}

int Saig_BmcPerform	(	Aig_Man_t *	pAig,
		int	nStart,
		int	nFramesMax,
		int	nNodesMax,
		int	nTimeOut,
		int	nConfMaxOne,
		int	nConfMaxAll,
		int	fVerbose,
		int	fVerbOverwrite,
		int *	piFrames,
		int	fSilent
	)

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

Synopsis [Performs BMC with the given parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 761 of file bmcBmc2.c.

{
    Saig_Bmc_t * p;
    Aig_Man_t * pNew;
    Cnf_Dat_t * pCnf;
    int nOutsSolved = 0;
    int Iter, RetValue = -1;
    abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
    int Status = -1;
/*
    Vec_Ptr_t * vSimInfo;
    vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
    Abs_ManFreeAray( vSimInfo );
*/
    if ( fVerbose )
    {
        printf( "Running \"bmc2\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
    } 
    nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
    // set runtime limit
    if ( nTimeOut )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
    for ( Iter = 0; ; Iter++ )
    {
        clk2 = Abc_Clock();
        // add new logic interval to frames
        Saig_BmcInterval( p );
//        Saig_BmcAddTargetsAsPos( p );
        if ( Vec_PtrSize(p->vTargets) == 0 )
            break;
        // convert logic slice into new AIG
        pNew = Saig_BmcIntervalToAig( p );
//printf( "StitchVars = %d.\n", p->nStitchVars );
        // derive CNF for the new AIG
        pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
        Cnf_DataLift( pCnf, p->nSatVars );
        p->nSatVars += pCnf->nVars;
        // add this CNF to the solver
        Saig_BmcLoadCnf( p, pCnf );
        Cnf_DataFree( pCnf );
        Aig_ManStop( pNew );
        // solve the targets
        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
        if ( fVerbose )
        {
            printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
            printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
            printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
            printf( "\n" );
            fflush( stdout );
        }
        if ( RetValue != l_False )
            break;
        // check the timeout
        if ( nTimeOut && Abc_Clock() > nTimeToStop )
        {
            if ( !fSilent )
                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
            if ( piFrames )
                *piFrames = p->iFrameLast-1;
            Saig_BmcManStop( p );
            return Status;
        }
    }
    if ( RetValue == l_True )
    {
        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
        if ( !fSilent )
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", 
                p->iOutputFail, p->pAig->pName, p->iFrameFail );
        Status = 0;
        if ( piFrames )
            *piFrames = p->iFrameFail - 1;
    }
    else // if ( RetValue == l_False || RetValue == l_Undef )
    {
        if ( !fSilent )
            Abc_Print( 1, "No output failed in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
        if ( piFrames )
        {
            if ( p->iOutputLast > 0 )
                *piFrames = p->iFramePrev - 2;
            else
                *piFrames = p->iFramePrev - 1;
        }
    }
    if ( !fSilent )
    {
        if ( fVerbOverwrite )
        {
            ABC_PRTr( "Time", Abc_Clock() - clk );
        }
        else
        {
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( RetValue != l_True )
        {
            if ( p->iFrameLast >= p->nFramesMax )
                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
            else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
            else if ( nTimeOut && Abc_Clock() > nTimeToStop )
                printf( "Reached timeout (%d seconds).\n", nTimeOut );
            else
                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
        }
    }
    Saig_BmcManStop( p );
    fflush( stdout );
    return Status;
}

int Saig_ManBmcScalable	(	Aig_Man_t *	pAig,
		Saig_ParBmc_t *	pPars
	)

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

Synopsis [Bounded model checking engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 1390 of file bmcBmc3.c.

{
    Gia_ManBmc_t * p;
    Aig_Obj_t * pObj;
    Abc_Cex_t * pCexNew, * pCexNew0;
    FILE * pLogFile = NULL;
    unsigned * pInfo;
    int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
    int i, f, k, Lit, status;
    abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
    abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
    abctime nTimeToStopNG, nTimeToStop;
    if ( pPars->pLogFileName )
        pLogFile = fopen( pPars->pLogFileName, "wb" );
    if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
        pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
        pPars->nTimeOutOne = 0;
    nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
    // create BMC manager
    p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
    p->pPars = pPars;
    p->pSat->nLearntStart = p->pPars->nLearnedStart;
    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
    p->pSat->nLearntMax   = p->pSat->nLearntStart;
    if ( pPars->fSolveAll && p->vCexes == NULL )
        p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d.\n",// Sect =%3d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums );//, Vec_VecSize(p->vSects) );
        Abc_Print( 1, "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
            pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
    } 
    pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
    // set runtime limit
    if ( nTimeToStop )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
    // perform frames
    Aig_ManRandom( 1 );
    pPars->timeLastSolved = Abc_Clock();
    for ( f = 0; f < pPars->nFramesMax; f++ )
    {
        // stop BMC after exploring all reachable states
        if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
        {
            Abc_Print( 1, "Stopping BMC because all 2^%d reachable states are visited.\n", Aig_ManRegNum(pAig) );
            if ( p->pPars->fUseBridge )
                Saig_ManForEachPo( pAig, pObj, i )
                    if ( !(p->vCexes && Vec_PtrEntry(p->vCexes, i)) && !(p->pTime4Outs && p->pTime4Outs[i] == 0) ) // not SAT and not timed out
                        Gia_ManToBridgeResult( stdout, 1, NULL, i );
            RetValue = pPars->nFailOuts ? 0 : 1;
            goto finish;
        }
        // stop BMC if all targets are solved
        if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) )
        {
            Abc_Print( 1, "Stopping BMC because all targets are disproved or timed out.\n" );
            RetValue = pPars->nFailOuts ? 0 : 1;
            goto finish;
        }
        // consider the next timeframe
        if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
            pPars->iFrame = f-1;
        // map nodes of this section
        Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
        Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
/*
        // cannot remove mapping of frame values for any timeframes
        // because with constant propagation they may be needed arbitrarily far
        if ( f > 2*Vec_VecSize(p->vSects) )
        {
            int iFrameOld = f - 2*Vec_VecSize( p->vSects );
            void * pMemory = Vec_IntReleaseArray( Vec_PtrEntry(p->vId2Var, iFrameOld) );
            ABC_FREE( pMemory );
        } 
*/
        // prepare some nodes
        Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
        Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
        Saig_ManForEachPi( pAig, pObj, i )
            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
        if ( f == 0 )
        {
            Saig_ManForEachLo( p->pAig, pObj, i )
            {
                Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
                Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
            }
        }
        if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
            continue;
        // create CNF upfront
        if ( pPars->fSolveAll )
        {
            Saig_ManForEachPo( pAig, pObj, i )
            {
                if ( i >= Saig_ManPoNum(pAig) )
                    break;
                // check for timeout
                if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
                {
                    Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  pPars->nTimeOutGap );
                    goto finish;
                }
                if ( nTimeToStop && Abc_Clock() > nTimeToStop )
                {
                    if ( !pPars->fSilent )
                        Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                    goto finish;
                }
                // skip solved outputs
                if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                    continue;
                // skip output whose time has run out
                if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
                    continue;
                // add constraints for this output
clk2 = Abc_Clock();
                Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
            }
        }
        // solve SAT
        clk = Abc_Clock(); 
        Saig_ManForEachPo( pAig, pObj, i )
        {
            if ( i >= Saig_ManPoNum(pAig) )
                break;
            // check for timeout
            if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
            {
                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  pPars->nTimeOutGap );
                goto finish;
            }
            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
            {
                if ( !pPars->fSilent )
                    Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                goto finish;
            }
            // skip solved outputs
            if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                continue;
            // skip output whose time has run out
            if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
                continue;
            // add constraints for this output
clk2 = Abc_Clock();
            Lit = Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
            // solve this output
            fUnfinished = 0;
            sat_solver_compress( p->pSat );
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[i] > 0 );
                clkOne = Abc_Clock();
                sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
            }
clk2 = Abc_Clock();
            status = Saig_ManCallSolver( p, Lit );
clkSatRun = Abc_Clock() - clk2;
            if ( pLogFile )
                fprintf( pLogFile, "Frame %5d  Output %5d  Time(ms) %8d %8d\n", f, i, 
                    Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC),
                    Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) );
            if ( p->pTime4Outs )
            {
                abctime timeSince = Abc_Clock() - clkOne;
                assert( p->pTime4Outs[i] > 0 );
                p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
                if ( p->pTime4Outs[i] == 0 && status != l_True )
                    pPars->nDropOuts++;
            }
            if ( status == l_False )
            {
nTimeUnsat += clkSatRun;
                if ( Lit != 0 )
                {
                    // add final unit clause
                    Lit = lit_neg( Lit );
                    status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                    assert( status );
                    // add learned units
                    for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
                    {
                        Lit = veci_begin(&p->pSat->unit_lits)[k];
                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                        assert( status );
                    }
                    veci_resize(&p->pSat->unit_lits, 0);
                    // propagate units
                    sat_solver_compress( p->pSat );
                }
                if ( p->pPars->fUseBridge )
                    Gia_ManReportProgress( stdout, i, f );
            }
            else if ( status == l_True )
            {
nTimeSat += clkSatRun;
                RetValue = 0;
                fFirst = 0;
                if ( !pPars->fSolveAll )
                {
                    if ( pPars->fVerbose )
                    {
                        Abc_Print( 1, "%4d %s : ", f,  fUnfinished ? "-" : "+" );
                        Abc_Print( 1, "Var =%8.0f. ",  (double)p->nSatVars );
                        Abc_Print( 1, "Cla =%9.0f. ",  (double)p->pSat->stats.clauses );
                        Abc_Print( 1, "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
//                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
                        Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
//                        ABC_PRT( "Time", Abc_Clock() - clk );
                        Abc_Print( 1, "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
                        Abc_Print( 1, "%4.0f MB",      1.0*sat_solver_memory(p->pSat)/(1<<20) );
                        Abc_Print( 1, "%9.2f sec  ",   (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
//                        Abc_Print( 1, "\n" );
//                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
//                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
//                        Abc_Print( 1, "S =%6d. ", p->nBufNum );
//                        Abc_Print( 1, "D =%6d. ", p->nDupNum );
                        Abc_Print( 1, "\n" );
                        fflush( stdout );
                    }
                    ABC_FREE( pAig->pSeqModel );
                    pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
                    goto finish;
                }
                pPars->nFailOuts++;
                if ( !pPars->fNotVerbose )
                    Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                        nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                if ( p->vCexes == NULL )
                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                pCexNew0 = NULL;
                if ( p->pPars->fUseBridge )
                {
                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                    //Abc_CexFree( pCexNew );
                    pCexNew0 = pCexNew; 
                    pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
                }
                Vec_PtrWriteEntry( p->vCexes, i, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); 
                if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
                {
                    Abc_CexFreeP( &pCexNew0 );
                    Abc_Print( 1, "Quitting due to callback on fail.\n" );
                    goto finish;
                }
                // reset the timeout
                pPars->timeLastSolved = Abc_Clock();
                nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
                if ( nTimeToStop )
                    sat_solver_set_runtime_limit( p->pSat, nTimeToStop );

                // check if other outputs failed under the same counter-example
                Saig_ManForEachPo( pAig, pObj, k )
                {
                    if ( k >= Saig_ManPoNum(pAig) )
                        break;
                    // skip solved outputs
                    if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
                        continue;
                    // check if this output is solved
                    Lit = Saig_ManBmcCreateCnf( p, pObj, f );
                    if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                        continue;
                    // write entry
                    pPars->nFailOuts++;
                    if ( !pPars->fNotVerbose )
                        Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                            nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                    // report to the bridge
                    if ( p->pPars->fUseBridge )
                    {
                        // set the output number
                        pCexNew0->iPo = k;
                        Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
                    }
                    // remember solved output
                    Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
                }
                Abc_CexFreeP( &pCexNew0 );
                Abc_CexFree( pCexNew );
            }
            else 
            {
nTimeUndec += clkSatRun;
                assert( status == l_Undef );
                if ( pPars->nFramesJump )
                {
                    pPars->nConfLimit = pPars->nConfLimitJump;
                    nJumpFrame = f + pPars->nFramesJump;
                    fUnfinished = 1;
                    break;
                }
                if ( p->pTime4Outs == NULL )
                    goto finish;
            }
        }
        if ( pPars->fVerbose ) 
        {
            if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 )
            {
                fFirst = 0;
//                Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
            }
            Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
            Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
//            Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
            Abc_Print( 1, "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
            Abc_Print( 1, "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
//            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
            Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
            if ( pPars->fSolveAll )
                Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
            if ( pPars->nTimeOutOne )
                Abc_Print( 1, "T/O =%4d. ", pPars->nDropOuts );
//            ABC_PRT( "Time", Abc_Clock() - clk );
//            Abc_Print( 1, "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
            Abc_Print( 1, "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
            Abc_Print( 1, "%4.0f MB",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
//            Abc_Print( 1, " %6d %6d ",   p->nLitUsed, p->nLitUseless );
            Abc_Print( 1, "%9.2f sec ",  1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
//            Abc_Print( 1, "\n" );
//            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
//            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
//            Abc_Print( 1, "Simples = %6d. ", p->nBufNum );
//            Abc_Print( 1, "Dups = %6d. ", p->nDupNum );
            Abc_Print( 1, "\n" );
            fflush( stdout );
        }
    }
    // consider the next timeframe
    if ( nJumpFrame && pPars->nStart == 0 )
        pPars->iFrame = nJumpFrame - pPars->nFramesJump;
    else if ( RetValue == -1 && pPars->nStart == 0 )
        pPars->iFrame = f-1;
//ABC_PRT( "CNF generation runtime", clkOther );
finish:
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Runtime:  " );
        Abc_Print( 1, "CNF = %.1f sec (%.1f %%)  ",   1.0*clkOther/CLOCKS_PER_SEC,   100.0*clkOther/(Abc_Clock() - clkTotal)   );
        Abc_Print( 1, "UNSAT = %.1f sec (%.1f %%)  ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
        Abc_Print( 1, "SAT = %.1f sec (%.1f %%)  ",   1.0*nTimeSat/CLOCKS_PER_SEC,   100.0*nTimeSat/(Abc_Clock() - clkTotal)   );
        Abc_Print( 1, "UNDEC = %.1f sec (%.1f %%)",   1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
        Abc_Print( 1, "\n" );
    }
    Saig_Bmc3ManStop( p );
    fflush( stdout );
    if ( pLogFile )
        fclose( pLogFile );
    return RetValue;
}

int Saig_ManBmcSimple	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nSizeMax,
		int	nConfLimit,
		int	fRewrite,
		int	fVerbose,
		int *	piFrame,
		int	nCofFanLit
	)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file bmcBmc.c.

{
    extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    Aig_Man_t * pFrames, * pAigTemp;
    Aig_Obj_t * pObj;
    int status, Lit, i, RetValue = -1;
    abctime clk;

    // derive the timeframes
    clk = Abc_Clock();
    if ( nCofFanLit )
    {
        pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
        if ( pFrames == NULL )
            return -1;
    }
    else if ( nSizeMax > 0 )
    {
        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
        nFrames = Aig_ManCoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManCoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
    }
    else
        pFrames = Saig_ManFramesBmc( pAig, nFrames );
    if ( piFrame )
        *piFrame = nFrames;
    if ( fVerbose )
    {
        printf( "Running \"bmc\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
            nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames), 
            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
        ABC_PRT( "Time", Abc_Clock() - clk );
        fflush( stdout );
    }
    // rewrite the timeframes
    if ( fRewrite )
    {
        clk = Abc_Clock();
//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
        Aig_ManStop( pAigTemp );
        if ( fVerbose )
        {
            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
            ABC_PRT( "Time", Abc_Clock() - clk );
            fflush( stdout );
        }
    }
    // create the SAT solver
    clk = Abc_Clock();
    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );  
//if ( s_fInterrupt )
//return -1;
    pSat = sat_solver_new();
    sat_solver_setnvars( pSat, pCnf->nVars );
    for ( i = 0; i < pCnf->nClauses; i++ )
    {
        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
            assert( 0 );
    }
    if ( fVerbose )
    {
        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
        ABC_PRT( "Time", Abc_Clock() - clk );
        fflush( stdout );
    }
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        if ( fVerbose )
        {
            printf( "The BMC problem is trivially UNSAT\n" );
            fflush( stdout );
        }
    }
    else
    {
        abctime clkPart = Abc_Clock();
        Aig_ManForEachCo( pFrames, pObj, i )
        {
//if ( s_fInterrupt )
//return -1;
            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
            if ( fVerbose )
            {
                printf( "Solving output %2d of frame %3d ... \r", 
                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
            }
            clk = Abc_Clock();
            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
            {
                printf( "Solved %2d outputs of frame %3d.  ", 
                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
                ABC_PRT( "T", Abc_Clock() - clkPart );
                clkPart = Abc_Clock();
                fflush( stdout );
            }
            if ( status == l_False )
            {
/*
                Lit = lit_neg( Lit );
                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
                assert( RetValue );
                if ( pSat->qtail != pSat->qhead )
                {
                    RetValue = sat_solver_simplify(pSat);
                    assert( RetValue );
                }
*/
            }
            else if ( status == l_True )
            {
                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
                pModel[Aig_ManCiNum(pFrames)] = pObj->Id;
                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
                ABC_FREE( pModel );
                Vec_IntFree( vCiIds );

                if ( piFrame )
                    *piFrame = i / Saig_ManPoNum(pAig);
                RetValue = 0;
                break;
            }
            else
            {
                if ( piFrame )
                    *piFrame = i / Saig_ManPoNum(pAig);
                RetValue = -1;
                break;
            }
        }
    }
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Aig_ManStop( pFrames );
    return RetValue;
}

Abc_Cex_t* Saig_ManCexMinPerform	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 547 of file bmcCexMin1.c.

{
    int fReasonPi = 0;

    Abc_Cex_t * pCexMin = NULL;
    Aig_Man_t * pManNew = NULL;
    Vec_Vec_t * vFrameReas;
    vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
    printf( "Reason size = %d.  Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );

    // try reducing the frames
    if ( !fReasonPi )
    {
        char * pFileName = "aigcube.aig";
        pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
        Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
        Aig_ManStop( pManNew );
        printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
    }

    // find reduced counter-example
    Vec_VecFree( vFrameReas );
    return pCexMin;
}

void Saig_ParBmcSetDefaultParams

(

Saig_ParBmc_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 1284 of file bmcBmc3.c.

{
    memset( p, 0, sizeof(Saig_ParBmc_t) );
    p->nStart         =     0;    // maximum number of timeframes 
    p->nFramesMax     =     0;    // maximum number of timeframes 
    p->nConfLimit     =     0;    // maximum number of conflicts at a node
    p->nConfLimitJump =     0;    // maximum number of conflicts after jumping
    p->nFramesJump    =     0;    // the number of tiemframes to jump
    p->nTimeOut       =     0;    // approximate timeout in seconds
    p->nTimeOutGap    =     0;    // time since the last CEX found
    p->nPisAbstract   =     0;    // the number of PIs to abstract
    p->fSolveAll      =     0;    // stops on the first SAT instance
    p->fDropSatOuts   =     0;    // replace sat outputs by constant 0
    p->nLearnedStart  = 10000;    // starting learned clause limit
    p->nLearnedDelta  =  2000;    // delta of learned clause limit
    p->nLearnedPerce  =    80;    // ratio of learned clause limit
    p->fVerbose       =     0;    // verbose 
    p->fNotVerbose    =     0;    // skip line-by-line print-out 
    p->iFrame         =    -1;    // explored up to this frame
    p->nFailOuts      =     0;    // the number of failed outputs
    p->nDropOuts      =     0;    // the number of timed out outputs
    p->timeLastSolved =     0;    // time when the last one was solved
}

void Unr_ManFree

(

Unr_Man_t *

p

)

Definition at line 340 of file bmcUnroll.c.

{
    Gia_ManStop( p->pFrames );
    // intermediate data
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vOrderLim );
    Vec_IntFreeP( &p->vTents );
    Vec_IntFreeP( &p->vRanks );
    // unrolling data
    Vec_IntFreeP( &p->vObjLim );
    Vec_IntFreeP( &p->vCiMap );
    Vec_IntFreeP( &p->vCoMap );
    Vec_IntFreeP( &p->vPiLits );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

Gia_Man_t* Unr_ManUnrollFrame	(	Unr_Man_t *	p,
		int	f
	)

Definition at line 379 of file bmcUnroll.c.

{
    int i, iLit, iLit0, iLit1, hStart;
    for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
        Vec_IntPush( p->vPiLits, Gia_ManAppendCi(p->pFrames) );
    hStart = Vec_IntEntry( p->vObjLim, Abc_MaxInt(0, Vec_IntSize(p->vObjLim)-1-f) );
    while ( p->pObjs + hStart < p->pEnd )
    {
        Unr_Obj_t * pUnrObj = Unr_ManObj( p, hStart );
        if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) // AND node
        {
            iLit0 = Unr_ManFanin0Value( p, pUnrObj );
            iLit1 = Unr_ManFanin1Value( p, pUnrObj );
            iLit  = Gia_ManHashAnd( p->pFrames, iLit0, iLit1 );
            Unr_ManObjSetValue( pUnrObj, iLit );
        }
        else if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 == UNR_DIFF_NULL ) // PO/RI/RO
        {
            iLit  = Unr_ManFanin0Value( p, pUnrObj );
            Unr_ManObjSetValue( pUnrObj, iLit );
            if ( pUnrObj->fItIsPo )
                Gia_ManAppendCo( p->pFrames, iLit );
        }
        else // PI  (pUnrObj->hFan0 is CioId; pUnrObj->hFan1 is tent)
        {
            assert( pUnrObj->fItIsPi && f >= (int)pUnrObj->hFan1 );
            iLit = Vec_IntEntry( p->vPiLits, Gia_ManPiNum(p->pGia) * (f - pUnrObj->hFan1) + pUnrObj->hFan0 );
            Unr_ManObjSetValue( pUnrObj, iLit );
        }
        hStart += Unr_ObjSize( pUnrObj );
    }
    assert( p->pObjs + hStart == p->pEnd );
    assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(p->pGia) );
    return p->pFrames;
}

Unr_Man_t* Unr_ManUnrollStart	(	Gia_Man_t *	pGia,
		int	fVerbose
	)

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

Synopsis [Perform smart unrolling.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file bmcUnroll.c.

{
    int i, iHandle;
    Unr_Man_t * p;
    p = Unr_ManAlloc( pGia );
    Unr_ManSetup( p, fVerbose );
    for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ )
        if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 )
            Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 );
    return p;
}