bmcBmc3.c File Reference

#include "proof/fra/fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
#include "sat/glucose/AbcGlucose.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"

Include dependency graph for bmcBmc3.c:

Go to the source code of this file.

Classes
struct	Gia_ManBmc_t_

Macros
#define	SAIG_TER_NON   0
	FUNCTION DEFINITIONS ///.
#define	SAIG_TER_ZER   1
#define	SAIG_TER_ONE   2
#define	SAIG_TER_UND   3

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_	Gia_ManBmc_t
	DECLARATIONS ///.

Functions
int	Gia_ManToBridgeResult (FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
	DECLARATIONS ///.
void	Gia_ManReportProgress (FILE *pFile, int prop_no, int depth)
int	Saig_ManBmcTerSimCount01 (Aig_Man_t *p, unsigned *pInfo)
unsigned *	Saig_ManBmcTerSimOne (Aig_Man_t *p, unsigned *pPrev)
Vec_Ptr_t *	Saig_ManBmcTerSim (Aig_Man_t *p)
void	Saig_ManBmcTerSimTest (Aig_Man_t *p)
int	Saig_ManBmcCountNonternary_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vInfos, unsigned *pInfo, int f, int *pCounter)
void	Saig_ManBmcCountNonternary (Aig_Man_t *p, Vec_Ptr_t *vInfos, int iFrame)
int	Saig_ManBmcTerSimCount01Po (Aig_Man_t *p, unsigned *pInfo)
Vec_Ptr_t *	Saig_ManBmcTerSimPo (Aig_Man_t *p)
void	Saig_ManBmcTerSimTestPo (Aig_Man_t *p)
void	Saig_ManBmcDfs_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Saig_ManBmcDfsNodes (Aig_Man_t *p, Vec_Ptr_t *vRoots)
Vec_Vec_t *	Saig_ManBmcSections (Aig_Man_t *p)
void	Saig_ManBmcSectionsTest (Aig_Man_t *p)
void	Saig_ManBmcSupergate_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Vec_Ptr_t *	Saig_ManBmcSupergate (Aig_Man_t *p, int iPo)
int	Saig_ManBmcCountRefed (Aig_Man_t *p, Vec_Ptr_t *vSuper)
void	Saig_ManBmcSupergateTest (Aig_Man_t *p)
void	Saig_ManBmcWriteBlif (Aig_Man_t *p, Vec_Int_t *vMapping, char *pFileName)
void	Saig_ManBmcMappingTest (Aig_Man_t *p)
Vec_Int_t *	Saig_ManBmcComputeMappingRefs (Aig_Man_t *p, Vec_Int_t *vMap)
Gia_ManBmc_t *	Saig_Bmc3ManStart (Aig_Man_t *pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose)
void	Saig_Bmc3ManStop (Gia_ManBmc_t *p)
int	Saig_ManBmcCreateCnf_rec (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
void	Saig_ManBmcCreateCnf_iter (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
int	Saig_ManBmcRunTerSim_rec (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
int	Saig_ManBmcCreateCnf (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
int	Aig_NodeCompareRefsIncrease (Aig_Obj_t **pp1, Aig_Obj_t **pp2)
void	Saig_ParBmcSetDefaultParams (Saig_ParBmc_t *p)
abctime	Saig_ManBmcTimeToStop (Saig_ParBmc_t *pPars, abctime nTimeToStopNG)
Abc_Cex_t *	Saig_ManGenerateCex (Gia_ManBmc_t *p, int f, int i)
int	Saig_ManCallSolver (Gia_ManBmc_t *p, int Lit)
int	Saig_ManBmcScalable (Aig_Man_t *pAig, Saig_ParBmc_t *pPars)

Macro Definition Documentation

SAIG_TER_NON

#define SAIG_TER_NON   0

FUNCTION DEFINITIONS ///.

Definition at line 87 of file bmcBmc3.c.

SAIG_TER_ONE

#define SAIG_TER_ONE   2

Definition at line 89 of file bmcBmc3.c.

SAIG_TER_UND

#define SAIG_TER_UND   3

Definition at line 90 of file bmcBmc3.c.

SAIG_TER_ZER

#define SAIG_TER_ZER   1

Definition at line 88 of file bmcBmc3.c.

Typedef Documentation

Gia_ManBmc_t

typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t

DECLARATIONS ///.

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

FileName [bmcBmc3.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Simple BMC package.]

Author [Alan Mishchenko in collaboration with Niklas Een.]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 36 of file bmcBmc3.c.

Function Documentation

Aig_NodeCompareRefsIncrease()

int Aig_NodeCompareRefsIncrease	(	Aig_Obj_t **	pp1,
		Aig_Obj_t **	pp2 )

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

Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 1308 of file bmcBmc3.c.

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

Gia_ManReportProgress()

void Gia_ManReportProgress	(	FILE *	pFile,
		int	prop_no,
		int	depth )

Definition at line 75 of file bmcBmc3.c.

{
    extern int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer );
    char buf[100];
    sprintf(buf, "property: safe<%d>\nbug-free-depth: %d\n", prop_no, depth);
    Gia_ManToBridgeProgress(pFile, strlen(buf), (unsigned char *)buf);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManToBridgeResult()

int Gia_ManToBridgeResult ( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved )

extern

DECLARATIONS ///.

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

FileName [pdrCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id

pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]

Definition at line 287 of file utilBridge.c.

{
    if ( Result == 0 ) // sat
        Gia_ManFromBridgeCex( pFile, pCex );
    else if ( Result == 1 ) // unsat
        Gia_ManFromBridgeHolds( pFile, iPoProved );
    else if ( Result == -1 ) // undef
        Gia_ManFromBridgeUnknown( pFile, iPoProved );
    else assert( 0 );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_Bmc3ManStart()

Gia_ManBmc_t * Saig_Bmc3ManStart	(	Aig_Man_t *	pAig,
		int	nTimeOutOne,
		int	nConfLimit,
		int	fUseSatoko,
		int	fUseGlucose )

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

Synopsis [Create manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 721 of file bmcBmc3.c.

{
    Gia_ManBmc_t * p;
    Aig_Obj_t * pObj;
    int i;
//    assert( Aig_ManRegNum(pAig) > 0 );
    p = ABC_CALLOC( Gia_ManBmc_t, 1 );
    p->pAig = pAig;
    // create mapping
    p->vMapping = Cnf_DeriveMappingArray( pAig );
    p->vMapRefs = Saig_ManBmcComputeMappingRefs( pAig, p->vMapping );
    // create sections
//    p->vSects = Saig_ManBmcSections( pAig );
    // map object IDs into their numbers and section numbers
    p->nObjNums = 0;
    p->vId2Num  = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
    Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(Aig_ManConst1(pAig)), p->nObjNums++ );
    Aig_ManForEachCi( pAig, pObj, i )
        Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) > 0 )
            Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
    Aig_ManForEachCo( pAig, pObj, i )
        Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
    p->vId2Var  = Vec_PtrAlloc( 100 );
    p->vTerInfo = Vec_PtrAlloc( 100 );
    p->vVisited = Vec_WecAlloc( 100 );
    // create solver
    p->nSatVars = 1;
    if ( fUseSatoko )
    {
        satoko_opts_t opts;
        satoko_default_opts(&opts);
        opts.conf_limit = nConfLimit;
        p->pSat2 = satoko_create();  
        satoko_configure(p->pSat2, &opts);
        satoko_setnvars(p->pSat2, 1000);
    }
    else if ( fUseGlucose )
    {
        //opts.conf_limit = nConfLimit;
        p->pSat3 = bmcg_sat_solver_start();  
        for ( i = 0; i < 1000; i++ )
            bmcg_sat_solver_addvar( p->pSat3 );
    }
    else
    {
        p->pSat  = sat_solver_new();
        sat_solver_setnvars(p->pSat, 1000);
    }
    Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
    // terminary simulation 
    p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
    // hash table
    p->vData = Vec_IntAlloc( 5 * 10000 );
    p->vHash = Hsh_IntManStart( p->vData, 5, 10000 );
    p->vId2Lit = Vec_IntAlloc( 10000 );
    // time spent on each outputs
    if ( nTimeOutOne )
    {
        p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
            p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
    }
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_Bmc3ManStop()

void Saig_Bmc3ManStop

(

Gia_ManBmc_t *

p

)

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

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 799 of file bmcBmc3.c.

{
    if ( p->pPars->fVerbose )
    {
        int nUsedVars = p->pSat ? sat_solver_count_usedvars(p->pSat) : 0;
        Abc_Print( 1, "LStart(P) = %d  LDelta(Q) = %d  LRatio(R) = %d  ReduceDB = %d  Vars = %d  Used = %d (%.2f %%)\n", 
            p->pSat ? p->pSat->nLearntStart     : 0, 
            p->pSat ? p->pSat->nLearntDelta     : 0, 
            p->pSat ? p->pSat->nLearntRatio     : 0, 
            p->pSat ? p->pSat->nDBreduces       : 0, 
            p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), 
            nUsedVars, 
            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
        Abc_Print( 1, "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  UniProps = %d.\n", 
            p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
    }
//    Aig_ManCleanMarkA( p->pAig );
    if ( p->vCexes )
    {
        assert( p->pAig->vSeqModelVec == NULL );
        p->pAig->vSeqModelVec = p->vCexes;
        p->vCexes = NULL;
    }
//    Vec_PtrFreeFree( p->vCexes );
    Vec_WecFree( p->vVisited );
    Vec_IntFree( p->vMapping );
    Vec_IntFree( p->vMapRefs );
//    Vec_VecFree( p->vSects );
    Vec_IntFree( p->vId2Num );
    Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
    Vec_PtrFreeFree( p->vTerInfo );
    if ( p->pSat )  sat_solver_delete( p->pSat );
    if ( p->pSat2 ) satoko_destroy( p->pSat2 );
    if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 );
    ABC_FREE( p->pTime4Outs );
    Vec_IntFree( p->vData );
    Hsh_IntManStop( p->vHash );
    Vec_IntFree( p->vId2Lit );
    ABC_FREE( p->pSopSizes );
    ABC_FREE( p->pSops[1] );
    ABC_FREE( p->pSops );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcComputeMappingRefs()

Vec_Int_t * Saig_ManBmcComputeMappingRefs	(	Aig_Man_t *	p,
		Vec_Int_t *	vMap )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 690 of file bmcBmc3.c.

{
    Vec_Int_t * vRefs;
    Aig_Obj_t * pObj;
    int i, iFan, * pData;
    vRefs = Vec_IntStart( Aig_ManObjNumMax(p) );
    Aig_ManForEachCo( p, pObj, i )
        Vec_IntAddToEntry( vRefs, Aig_ObjFaninId0(pObj), 1 );
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( Vec_IntEntry(vMap, i) == 0 )
            continue;
        pData = Vec_IntEntryP( vMap, Vec_IntEntry(vMap, i) );
        for ( iFan = 0; iFan < 4; iFan++ )
            if ( pData[iFan+1] >= 0 )
                Vec_IntAddToEntry( vRefs, pData[iFan+1], 1 );
    }
    return vRefs;
}

Here is the caller graph for this function:

Saig_ManBmcCountNonternary()

void Saig_ManBmcCountNonternary	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vInfos,
		int	iFrame )

Definition at line 285 of file bmcBmc3.c.

{
    int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
    unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
    assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
    for ( i = 0; i <= iFrame; i++ )
        Abc_Print( 1, "%d=%d ", i, pCounters[i] );
    Abc_Print( 1, "\n" );
    ABC_FREE( pCounters );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcCountNonternary_rec()

int Saig_ManBmcCountNonternary_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vInfos,
		unsigned *	pInfo,
		int	f,
		int *	pCounter )

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

Synopsis [Count the number of non-ternary per frame.]

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file bmcBmc3.c.

{ 
    int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
    if ( Value == SAIG_TER_NON )
        return 0;
    assert( f >= 0 );
    pCounter[f] += (Value == SAIG_TER_UND);
    if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
        return 0;
    if ( Saig_ObjIsLi(p, pObj) )
        return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
    if ( Saig_ObjIsLo(p, pObj) )
        return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
    assert( Aig_ObjIsNode(pObj) );
    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcCountRefed()

int Saig_ManBmcCountRefed	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vSuper )

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

Synopsis [Returns the number of nodes with ref counter more than 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 536 of file bmcBmc3.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
    {
        assert( !Aig_IsComplement(pObj) );
        Counter += (Aig_ObjRefs(pObj) > 1);
    }
    return Counter;
}

Here is the caller graph for this function:

Saig_ManBmcCreateCnf()

int Saig_ManBmcCreateCnf	(	Gia_ManBmc_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame )

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1254 of file bmcBmc3.c.

{
    Vec_Int_t * vVisit, * vVisit2;
    Aig_Obj_t * pTemp;
    int Lit, f, i;
    // perform ternary simulation
    int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
    if ( Value != SAIG_TER_UND )
        return (int)(Value == SAIG_TER_ONE);
    // construct CNF if value is ternary
//    Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
    Vec_WecClear( p->vVisited );
    vVisit = Vec_WecPushLevel( p->vVisited );
    Vec_IntPush( vVisit, Aig_ObjId(pObj) );
    for ( f = iFrame; f >= 0; f-- )
    {
        Aig_ManIncrementTravId( p->pAig );
        vVisit2 = Vec_WecPushLevel( p->vVisited );
        vVisit = Vec_WecEntry( p->vVisited, Vec_WecSize(p->vVisited)-2 );
        Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
            Saig_ManBmcCreateCnf_iter( p, pTemp, f, vVisit2 );
        if ( Vec_IntSize(vVisit2) == 0 )
            break;
    }
    Vec_WecForEachLevelReverse( p->vVisited, vVisit, f )
        Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
            Saig_ManBmcCreateCnf_rec( p, pTemp, iFrame-f );
    Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
    // extend the SAT solver
    if ( p->pSat2 )
        satoko_setnvars( p->pSat2, p->nSatVars );
    else if ( p->pSat3 )
    {
        for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ )
            bmcg_sat_solver_addvar( p->pSat3 );
    }
    else
        sat_solver_setnvars( p->pSat, p->nSatVars );
    return Lit;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcCreateCnf_iter()

void Saig_ManBmcCreateCnf_iter	(	Gia_ManBmc_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame,
		Vec_Int_t *	vVisit )

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1139 of file bmcBmc3.c.

{
    if ( Saig_ManBmcLiteral( p, pObj, iFrame ) != ~0 )
        return; 
    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            Vec_IntPush( vVisit, Saig_ObjLoToLi(p->pAig, pObj)->Id );
        return;
    }
    if ( Aig_ObjIsCo(pObj) )
    {
        Saig_ManBmcCreateCnf_iter( p, Aig_ObjFanin0(pObj), iFrame, vVisit );
        return;
    }
    else
    {
        int * pMapping, i;
        assert( Aig_ObjIsNode(pObj) );
        pMapping = Saig_ManBmcMapping( p, pObj );
        for ( i = 0; i < 4; i++ )
            if ( pMapping[i+1] != -1 )
                Saig_ManBmcCreateCnf_iter( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame, vVisit );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcCreateCnf_rec()

int Saig_ManBmcCreateCnf_rec	(	Gia_ManBmc_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame )

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1052 of file bmcBmc3.c.

{
    extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
    int * pMapping, i, iLit, Lits[5], uTruth;
    iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
    if ( iLit != ~0 )
        return iLit; 
    assert( iFrame >= 0 );
    if ( Aig_ObjIsCi(pObj) )
    {
        if ( Saig_ObjIsPi(p->pAig, pObj) )
            iLit = toLit( p->nSatVars++ );
        else
            iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
    }
    if ( Aig_ObjIsCo(pObj) )
    {
        iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
        if ( Aig_ObjFaninC0(pObj) )
            iLit = lit_neg(iLit);
        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
    }
    assert( Aig_ObjIsNode(pObj) );
    pMapping = Saig_ManBmcMapping( p, pObj );
    for ( i = 0; i < 4; i++ )
        if ( pMapping[i+1] == -1 )
            Lits[i] = -1;
        else
            Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
    uTruth = 0xffff & (unsigned)pMapping[0];
    // propagate constants
    uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
    if ( uTruth == 0 || uTruth == 0xffff )
    {
        iLit = (uTruth == 0xffff);
        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
    }
    // canonicize inputs
    uTruth = Dar_CutSortVars( uTruth, Lits );
    assert( uTruth != 0 && uTruth != 0xffff );
    if ( uTruth == 0xAAAA || uTruth == 0x5555 )
    {
        iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
        p->nBufNum++;
    }
    else 
    {
        int iEntry, iRes;
        int fCompl = (uTruth & 1);
        Lits[4] = (uTruth & 1) ? 0xffff & ~uTruth : uTruth;
        iEntry = Vec_IntSize(p->vData) / 5;
        assert( iEntry * 5 == Vec_IntSize(p->vData) );
        for ( i = 0; i < 5; i++ )
            Vec_IntPush( p->vData, Lits[i] );
        iRes = Hsh_IntManAdd( p->vHash, iEntry );
        if ( iRes == iEntry )
        {
            iLit = toLit( p->nSatVars++ );
            Saig_ManBmcAddClauses( p, Lits[4], Lits, iLit );
            assert( iEntry == Vec_IntSize(p->vId2Lit) );
            Vec_IntPush( p->vId2Lit, iLit );
            p->nHashMiss++;
        }
        else
        {
            iLit = Vec_IntEntry( p->vId2Lit, iRes );
            Vec_IntShrink( p->vData, Vec_IntSize(p->vData) - 5 );
            p->nHashHit++;
        }
        iLit = Abc_LitNotCond( iLit, fCompl );
    }
    return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcDfs_rec()

void Saig_ManBmcDfs_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes )

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file bmcBmc3.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsNode(pObj) )
    {
        Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
        Saig_ManBmcDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
    }
    Vec_PtrPush( vNodes, pObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcDfsNodes()

Vec_Ptr_t * Saig_ManBmcDfsNodes	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vRoots )

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

Synopsis [Collects internal nodes and PIs in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file bmcBmc3.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    vNodes = Vec_PtrAlloc( 100 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
    return vNodes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcMappingTest()

void Saig_ManBmcMappingTest

(

Aig_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 670 of file bmcBmc3.c.

{
    Vec_Int_t * vMapping;
    vMapping = Cnf_DeriveMappingArray( p );
    Saig_ManBmcWriteBlif( p, vMapping, "test.blif" );
    Vec_IntFree( vMapping );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcRunTerSim_rec()

int Saig_ManBmcRunTerSim_rec	(	Gia_ManBmc_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame )

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

Synopsis [Recursively performs terminary simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1179 of file bmcBmc3.c.

{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
    int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
    if ( Value != SAIG_TER_NON )
    {
/*
        // check the value of this literal in the SAT solver
        if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
        {
            int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
            if ( Lit >= 0  )
            {
                assert( Lit >= 2 );
                if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
                {
                    p->nUniProps++;
                    if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
                        Value = SAIG_TER_ONE;
                    else
                        Value = SAIG_TER_ZER;
 
//                    Value = SAIG_TER_UND;  // disable!
 
                    // use the new value
                    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
                    // transfer to the unrolling
                    if ( Value != SAIG_TER_UND )
                        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
                }
            }
        }
*/
        return Value;
    }
    if ( Aig_ObjIsCo(pObj) )
    {
        Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
        if ( Aig_ObjFaninC0(pObj) )
            Value = Saig_ManBmcSimInfoNot( Value );
    }
    else if ( Saig_ObjIsLo(p->pAig, pObj) )
    {
        assert( iFrame > 0 );
        Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
    }
    else if ( Aig_ObjIsNode(pObj) )
    {
        Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame  );
        Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame  );
        if ( Aig_ObjFaninC0(pObj) )
            Val0 = Saig_ManBmcSimInfoNot( Val0 );
        if ( Aig_ObjFaninC1(pObj) )
            Val1 = Saig_ManBmcSimInfoNot( Val1 );
        Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
    }
    else assert( 0 );
    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
    // transfer to the unrolling
    if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
    return Value;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcScalable()

int Saig_ManBmcScalable	(	Aig_Man_t *	pAig,
		Saig_ParBmc_t *	pPars )

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

Synopsis [Bounded model checking engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 1461 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, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
    p->pPars = pPars;
    if ( p->pSat )
    {
        p->pSat->nLearntStart = p->pPars->nLearnedStart;
        p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
        p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
        p->pSat->nLearntMax   = p->pSat->nLearntStart;
        p->pSat->fNoRestarts  = p->pPars->fNoRestarts;
        p->pSat->RunId        = p->pPars->RunId;
        p->pSat->pFuncStop    = p->pPars->pFuncStop;
    }
    else if ( p->pSat3 )
    {
//        satoko_set_runid(p->pSat3, p->pPars->RunId);
//        satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
    }
    else
    {
        satoko_set_runid(p->pSat2, p->pPars->RunId);
        satoko_set_stop_func(p->pSat2, p->pPars->pFuncStop);
    }
    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 )
    {
        if ( p->pSat2 )
            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
        else if ( p->pSat3 )
            bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
        else
            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;
            }
            if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
            {
                if ( !pPars->fSilent )
                    Abc_Print( 1, "Bmc3 got callbacks.\n" );
                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;
            if ( p->pSat ) sat_solver_compress( p->pSat );
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[i] > 0 );
                clkOne = Abc_Clock();
                if ( p->pSat2 )
                    satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
                else if ( p->pSat3 )
                    bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
                else
                    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 );
                    if ( p->pSat2 )
                        status = satoko_add_clause( p->pSat2, &Lit, 1 );
                    else if ( p->pSat3 )
                        status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
                    else
                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                    assert( status );
                    // add learned units
                    if ( p->pSat )
                    {
                        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 ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2)) );
                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
//                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
//                        Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
//                        ABC_PRT( "Time", Abc_Clock() - clk );
                        Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
                        Abc_Print( 1, "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
                        Abc_Print( 1, "%4.0f MB",      1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(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 )
                {
                    if ( p->pSat2 )
                        satoko_set_runtime_limit( p->pSat2, nTimeToStop );
                    else if ( p->pSat3 )
                        bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
                    else
                        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
                }
 
                // check if other outputs failed under the same counter-example
                Saig_ManForEachPo( pAig, pObj, k )
                {
                    Abc_Cex_t * pCexDup;
                    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 ( p->pSat2 )
                    {
                        if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                            continue;
                    }
                    else if ( p->pSat3 )
                    {
                        if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                            continue;
                    }
                    else
                    {
                        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)) );
                    pCexDup = Abc_CexDup(pCexNew, Saig_ManRegNum(pAig));
                    pCexDup->iPo = k;
                    Vec_PtrWriteEntry( p->vCexes, k, pCexDup );
                }
                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 ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 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 ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2))   );
            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
//            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
//            Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
            Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
            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*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSections()

Vec_Vec_t * Saig_ManBmcSections

(

Aig_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file bmcBmc3.c.

{
    Vec_Ptr_t * vSects, * vRoots, * vCone;
    Aig_Obj_t * pObj, * pObjPo;
    int i;
    Aig_ManIncrementTravId( p );
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    // start the roots
    vRoots = Vec_PtrAlloc( 1000 );
    Saig_ManForEachPo( p, pObjPo, i )
    {
        Aig_ObjSetTravIdCurrent( p, pObjPo );
        Vec_PtrPush( vRoots, pObjPo );
    }
    // compute the cones
    vSects = Vec_PtrAlloc( 20 );
    while ( Vec_PtrSize(vRoots) > 0 )
    {
        vCone = Saig_ManBmcDfsNodes( p, vRoots );
        Vec_PtrPush( vSects, vCone );
        // get the next set of roots
        Vec_PtrClear( vRoots );
        Vec_PtrForEachEntry( Aig_Obj_t *, vCone, pObj, i )
        {
            if ( !Saig_ObjIsLo(p, pObj) )
                continue;
            pObjPo = Saig_ObjLoToLi( p, pObj );
            if ( Aig_ObjIsTravIdCurrent(p, pObjPo) )
                continue;
            Aig_ObjSetTravIdCurrent( p, pObjPo );
            Vec_PtrPush( vRoots, pObjPo );
        }
    }
    Vec_PtrFree( vRoots );
    return (Vec_Vec_t *)vSects;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSectionsTest()

void Saig_ManBmcSectionsTest

(

Aig_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 453 of file bmcBmc3.c.

{
    Vec_Vec_t * vSects;
    Vec_Ptr_t * vOne;
    int i;
    vSects = Saig_ManBmcSections( p );
    Vec_VecForEachLevel( vSects, vOne, i )
        Abc_Print( 1, "%d=%d ", i, Vec_PtrSize(vOne) );
    Abc_Print( 1, "\n" );
    Vec_VecFree( vSects );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSupergate()

Vec_Ptr_t * Saig_ManBmcSupergate	(	Aig_Man_t *	p,
		int	iPo )

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

Synopsis [Collect the topmost supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file bmcBmc3.c.

{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pObj;
    vSuper = Vec_PtrAlloc( 10 );
    pObj = Aig_ManCo( p, iPo );
    pObj = Aig_ObjChild0( pObj );
    if ( !Aig_IsComplement(pObj) )
    {
        Vec_PtrPush( vSuper, pObj );
        return vSuper;
    }
    pObj = Aig_Regular( pObj );
    if ( !Aig_ObjIsNode(pObj) )
    {
        Vec_PtrPush( vSuper, pObj );
        return vSuper;
    }
    Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
    Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
    return vSuper;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSupergate_rec()

void Saig_ManBmcSupergate_rec	(	Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 478 of file bmcBmc3.c.

{
    // if the new node is complemented or a PI, another gate begins
    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) )
    {
        Vec_PtrPushUnique( vSuper, Aig_Regular(pObj) );
        return;
    }
    // go through the branches
    Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
    Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSupergateTest()

void Saig_ManBmcSupergateTest

(

Aig_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 559 of file bmcBmc3.c.

{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pObj;
    int i;
    Abc_Print( 1, "Supergates: " );
    Saig_ManForEachPo( p, pObj, i )
    {
        vSuper = Saig_ManBmcSupergate( p, i );
        Abc_Print( 1, "%d=%d(%d) ", i, Vec_PtrSize(vSuper), Saig_ManBmcCountRefed(p, vSuper) );
        Vec_PtrFree( vSuper );
    }
    Abc_Print( 1, "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcTerSim()

Vec_Ptr_t * Saig_ManBmcTerSim

(

Aig_Man_t *

p

)

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

Synopsis [Collects internal nodes and PIs in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file bmcBmc3.c.

{
    Vec_Ptr_t * vInfos;
    unsigned * pInfo = NULL;
    int i, TerPrev = ABC_INFINITY, TerCur, CountIncrease = 0;
    vInfos = Vec_PtrAlloc( 100 );
    for ( i = 0; i < 1000 && CountIncrease < 5 && TerPrev > 0; i++ )
    {
        TerCur = Saig_ManBmcTerSimCount01( p, pInfo );
        if ( TerCur >= TerPrev )
            CountIncrease++;
        TerPrev = TerCur;
        pInfo = Saig_ManBmcTerSimOne( p, pInfo );
        Vec_PtrPush( vInfos, pInfo );
    }
    return vInfos;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcTerSimCount01()

int Saig_ManBmcTerSimCount01	(	Aig_Man_t *	p,
		unsigned *	pInfo )

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

Synopsis [Returns the number of LIs with binary ternary info.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file bmcBmc3.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    if ( pInfo == NULL )
        return Saig_ManRegNum(p);
    Saig_ManForEachLi( p, pObj, i )
        if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
    return Counter;
}

Here is the caller graph for this function:

Saig_ManBmcTerSimCount01Po()

int Saig_ManBmcTerSimCount01Po	(	Aig_Man_t *	p,
		unsigned *	pInfo )

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

Synopsis [Returns the number of POs with binary ternary info.]

Description []

SideEffects []

SeeAlso []

Definition at line 309 of file bmcBmc3.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Saig_ManForEachPo( p, pObj, i )
        Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
    return Counter;
}

Here is the caller graph for this function:

Saig_ManBmcTerSimOne()

unsigned * Saig_ManBmcTerSimOne	(	Aig_Man_t *	p,
		unsigned *	pPrev )

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

Synopsis [Performs ternary simulation of one frame.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file bmcBmc3.c.

{
    Aig_Obj_t * pObj, * pObjLi;
    unsigned * pInfo;
    int i, Val0, Val1;
    pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) );
    Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE );
    Saig_ManForEachPi( p, pObj, i )
        Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
    if ( pPrev == NULL )
    {
        Saig_ManForEachLo( p, pObj, i )
            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
    }
    else
    {
        Saig_ManForEachLiLo( p, pObjLi, pObj, i )
            Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoGet(pPrev, pObjLi) );
    }
    Aig_ManForEachNode( p, pObj, i )
    {
        Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
        Val1 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin1(pObj) );
        if ( Aig_ObjFaninC0(pObj) )
            Val0 = Saig_ManBmcSimInfoNot( Val0 );
        if ( Aig_ObjFaninC1(pObj) )
            Val1 = Saig_ManBmcSimInfoNot( Val1 );
        Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoAnd(Val0, Val1) );
    }
    Aig_ManForEachCo( p, pObj, i )
    {
        Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
        if ( Aig_ObjFaninC0(pObj) )
            Val0 = Saig_ManBmcSimInfoNot( Val0 );
        Saig_ManBmcSimInfoSet( pInfo, pObj, Val0 );
    }
    return pInfo;    
}

Here is the caller graph for this function:

Saig_ManBmcTerSimPo()

Vec_Ptr_t * Saig_ManBmcTerSimPo

(

Aig_Man_t *

p

)

Definition at line 317 of file bmcBmc3.c.

{
    Vec_Ptr_t * vInfos;
    unsigned * pInfo = NULL;
    int i, nPoBin;
    vInfos = Vec_PtrAlloc( 100 );
    for ( i = 0; ; i++ )
    {
        if ( i % 100 == 0 )
            Abc_Print( 1, "Frame %5d\n", i );
        pInfo = Saig_ManBmcTerSimOne( p, pInfo );
        Vec_PtrPush( vInfos, pInfo );
        nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
        if ( nPoBin < Saig_ManPoNum(p) )
            break;
    }
    Abc_Print( 1, "Detected terminary PO in frame %d.\n", i );
    Saig_ManBmcCountNonternary( p, vInfos, i );
    return vInfos;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcTerSimTest()

void Saig_ManBmcTerSimTest

(

Aig_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file bmcBmc3.c.

{
    Vec_Ptr_t * vInfos;
    unsigned * pInfo;
    int i;
    vInfos = Saig_ManBmcTerSim( p );
    Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i )
        Abc_Print( 1, "%d=%d ", i, Saig_ManBmcTerSimCount01(p, pInfo) );
    Abc_Print( 1, "\n" );
    Vec_PtrFreeFree( vInfos );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcTerSimTestPo()

void Saig_ManBmcTerSimTestPo

(

Aig_Man_t *

p

)

Definition at line 337 of file bmcBmc3.c.

{
    Vec_Ptr_t * vInfos;
    vInfos = Saig_ManBmcTerSimPo( p );
    Vec_PtrFreeFree( vInfos );
}

Here is the call graph for this function:

Saig_ManBmcTimeToStop()

abctime Saig_ManBmcTimeToStop	(	Saig_ParBmc_t *	pPars,
		abctime	nTimeToStopNG )

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

Synopsis [Returns time to stop.]

Description []

SideEffects []

SeeAlso []

Definition at line 1369 of file bmcBmc3.c.

{
    abctime nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + Abc_Clock(): 0;
    abctime nTimeToStop = 0;
    if ( nTimeToStopNG && nTimeToStopGap )
        nTimeToStop = nTimeToStopNG < nTimeToStopGap ? nTimeToStopNG : nTimeToStopGap;
    else if ( nTimeToStopNG )
        nTimeToStop = nTimeToStopNG;
    else if ( nTimeToStopGap )
        nTimeToStop = nTimeToStopGap;
    return nTimeToStop;
}

Here is the caller graph for this function:

Saig_ManBmcWriteBlif()

void Saig_ManBmcWriteBlif	(	Aig_Man_t *	p,
		Vec_Int_t *	vMapping,
		char *	pFileName )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 585 of file bmcBmc3.c.

{
    FILE * pFile;
    char * pSopSizes, ** pSops;
    Aig_Obj_t * pObj;
    char Vals[4];
    int i, k, b, iFan, iTruth, * pData;
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        Abc_Print( 1, "Cannot open file %s\n", pFileName );
        return;
    }
    fprintf( pFile, ".model test\n" );
    fprintf( pFile, ".inputs" );
    Aig_ManForEachCi( p, pObj, i )
        fprintf( pFile, " n%d", Aig_ObjId(pObj) );
    fprintf( pFile, "\n" );
    fprintf( pFile, ".outputs" );
    Aig_ManForEachCo( p, pObj, i )
        fprintf( pFile, " n%d", Aig_ObjId(pObj) );
    fprintf( pFile, "\n" );
    fprintf( pFile, ".names" );
    fprintf( pFile, " n%d\n", Aig_ObjId(Aig_ManConst1(p)) );
    fprintf( pFile, " 1\n" );
 
    Cnf_ReadMsops( &pSopSizes, &pSops );
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( Vec_IntEntry(vMapping, i) == 0 )
            continue;
        pData = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, i) );
        fprintf( pFile, ".names" );
        for ( iFan = 0; iFan < 4; iFan++ )
            if ( pData[iFan+1] >= 0 )
                fprintf( pFile, " n%d", pData[iFan+1] );
            else
                break;
        fprintf( pFile, " n%d\n", i );
        // write SOP
        iTruth = pData[0] & 0xffff;
        for ( k = 0; k < pSopSizes[iTruth]; k++ )
        {
            int Lit = pSops[iTruth][k];
            for ( b = 3; b >= 0; b-- )
            {
                if ( Lit % 3 == 0 )
                    Vals[b] = '0';
                else if ( Lit % 3 == 1 )
                    Vals[b] = '1';
                else
                    Vals[b] = '-';
                Lit = Lit / 3;
            }
            for ( b = 0; b < iFan; b++ )
                fprintf( pFile, "%c", Vals[b] );
            fprintf( pFile, " 1\n" );
        }
    }
    free( pSopSizes );
    free( pSops[1] );
    free( pSops );
 
    Aig_ManForEachCo( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        fprintf( pFile, " n%d", Aig_ObjId(Aig_ObjFanin0(pObj)) );
        fprintf( pFile, " n%d\n", Aig_ObjId(pObj) );
        fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
    }
    fprintf( pFile, ".end\n" );
    fclose( pFile );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManCallSolver()

int Saig_ManCallSolver	(	Gia_ManBmc_t *	p,
		int	Lit )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1433 of file bmcBmc3.c.

{
    if ( Lit == 0 )
        return l_False;
    if ( Lit == 1 )
        return l_True;
    if ( p->pSat2 )
        return satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->pPars->nConfLimit );
    else if ( p->pSat3 )
    {
        bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit );
        return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 );
    }
    else
        return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManGenerateCex()

Abc_Cex_t * Saig_ManGenerateCex	(	Gia_ManBmc_t *	p,
		int	f,
		int	i )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1393 of file bmcBmc3.c.

{
    Aig_Obj_t * pObjPi;
    Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), f*Saig_ManPoNum(p->pAig)+i );
    int j, k, iBit = Saig_ManRegNum(p->pAig);
    for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(p->pAig) )
        Saig_ManForEachPi( p->pAig, pObjPi, k )
        {
            int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
            if ( p->pSat2 )
            {
                if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
                    Abc_InfoSetBit( pCex->pData, iBit + k );
            }
            else if ( p->pSat3 )
            {
                if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) )
                    Abc_InfoSetBit( pCex->pData, iBit + k );
            }
            else
            {
                if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
                    Abc_InfoSetBit( pCex->pData, iBit + k );
            }
        }
    return pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ParBmcSetDefaultParams()

void Saig_ParBmcSetDefaultParams

(

Saig_ParBmc_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 1334 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
}

Here is the call graph for this function:

Here is the caller graph for this function: