#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
#include "proof/ssw/ssw.h"
#include "bmc.h"

Include dependency graph for bmcBmc2.c:

Go to the source code of this file.

Classes
struct	Saig_Bmc_t_

Macros
#define	ABS_ZER 1
	FUNCTION DEFINITIONS ///.

#define	ABS_ONE 2

#define	ABS_UND 3

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Saig_Bmc_t_	Saig_Bmc_t
	DECLARATIONS ///.

Functions
int	Abs_ManExtendOneEval_rec (Vec_Ptr_t vSimInfo, Aig_Man_t p, Aig_Obj_t *pObj, int iFrame)

Vec_Ptr_t *	Abs_ManTernarySimulate (Aig_Man_t *p, int nFramesMax, int fVerbose)

void	Abs_ManFreeAray (Vec_Ptr_t *p)

Saig_Bmc_t *	Saig_BmcManStart (Aig_Man_t *pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fUseSatoko)

void	Saig_BmcManStop (Saig_Bmc_t *p)

Aig_Obj_t *	Saig_BmcIntervalConstruct_rec (Saig_Bmc_t p, Aig_Obj_t pObj, int i, Vec_Int_t *vVisited)

void	Saig_BmcInterval (Saig_Bmc_t *p)

Aig_Obj_t *	Saig_BmcIntervalToAig_rec (Saig_Bmc_t p, Aig_Man_t pNew, Aig_Obj_t *pObj)

Aig_Man_t *	Saig_BmcIntervalToAig (Saig_Bmc_t *p)

void	Saig_BmcLoadCnf (Saig_Bmc_t p, Cnf_Dat_t pCnf)

void	Saig_BmcDeriveFailed (Saig_Bmc_t *p, int iTargetFail)

Abc_Cex_t *	Saig_BmcGenerateCounterExample (Saig_Bmc_t *p)

int	Saig_BmcSolveTargets (Saig_Bmc_t p, int nStart, int pnOutsSolved)

void	Saig_BmcAddTargetsAsPos (Saig_Bmc_t *p)

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, int fUseSatoko)

Macro Definition Documentation

◆ ABS_ONE

#define ABS_ONE 2

Definition at line 108 of file bmcBmc2.c.

◆ ABS_UND

#define ABS_UND 3

Definition at line 109 of file bmcBmc2.c.

◆ ABS_ZER

#define ABS_ZER 1

FUNCTION DEFINITIONS ///.

Definition at line 107 of file bmcBmc2.c.

Typedef Documentation

◆ Saig_Bmc_t

typedef typedefABC_NAMESPACE_IMPL_START struct Saig_Bmc_t_ Saig_Bmc_t

DECLARATIONS ///.

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

FileName [bmcBmc2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Simple BMC package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 35 of file bmcBmc2.c.

Function Documentation

◆ Abs_ManExtendOneEval_rec()

int Abs_ManExtendOneEval_rec	(	Vec_Ptr_t *	vSimInfo,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame )

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

Synopsis [Performs ternary simulation for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file bmcBmc2.c.

{
    int Value0, Value1, Value;
    Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
    if ( Value )
        return Value;
    if ( Aig_ObjIsCi(pObj) )
    {
        assert( Saig_ObjIsLo(p, pObj) );
        Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
        return Value;
    }
    Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Abs_ManSimInfoNot( Value0 );
    if ( Aig_ObjIsCo(pObj) )
    {
        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
        return Value0;
    }
    assert( Aig_ObjIsNode(pObj) );
    if ( Value0 == ABS_ZER )
        Value = ABS_ZER;
    else
    {
        Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
        if ( Aig_ObjFaninC1(pObj) )
            Value1 = Abs_ManSimInfoNot( Value1 );
        Value = Abs_ManSimInfoAnd( Value0, Value1 );
    }
    Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
    assert( Value );
    return Value;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abs_ManFreeAray()

void Abs_ManFreeAray ( Vec_Ptr_t * p )

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

Synopsis [Free the array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file bmcBmc2.c.

{
    void * pTemp;
    int i;
    Vec_PtrForEachEntry( void *, p, pTemp, i )
        ABC_FREE( pTemp );
    Vec_PtrFree( p );
}

◆ Abs_ManTernarySimulate()

Vec_Ptr_t * Abs_ManTernarySimulate	(	Aig_Man_t *	p,
		int	nFramesMax,
		int	fVerbose )

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

Synopsis [Performs ternary simulation for one design.]

Description [The returned array contains the result of ternary simulation for all the frames where the output could be proved 0.]

SideEffects []

SeeAlso []

Definition at line 202 of file bmcBmc2.c.

{
    Vec_Ptr_t * vSimInfo;
    Aig_Obj_t * pObj;
    int i, f, nFramesLimit, nFrameWords;
    abctime clk = Abc_Clock();
    assert( Aig_ManRegNum(p) > 0 );
    // the maximum number of frames will be determined to use at most 200Mb of RAM
    nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
    nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax );
    nFrameWords  = Abc_BitWordNum( 2 * Aig_ManObjNum(p) );
    // allocate simulation info
    vSimInfo = Vec_PtrAlloc( nFramesLimit );
    for ( f = 0; f < nFramesLimit; f++ )
    {
        Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
        if ( f == 0 ) 
        {
            Saig_ManForEachLo( p, pObj, i )
                Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
        }
        Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
        Saig_ManForEachPi( p, pObj, i )
            Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
        Saig_ManForEachPo( p, pObj, i )
            Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
        // check if simulation has derived at least one fail or unknown
        Saig_ManForEachPo( p, pObj, i )
            if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
            {
                if ( fVerbose )
                {
                    printf( "Ternary sim found non-zero output in frame %d.  Used %5.2f MB.  ", 
                        f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
                    ABC_PRT( "Time", Abc_Clock() - clk );
                }
                return vSimInfo;
            }
    }
    if ( fVerbose )
    {
        printf( "Ternary sim proved all outputs in the first %d frames.  Used %5.2f MB.  ", 
            nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    return vSimInfo;
}

Here is the call graph for this function:

◆ Saig_BmcAddTargetsAsPos()

void Saig_BmcAddTargetsAsPos ( Saig_Bmc_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file bmcBmc2.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
        Aig_ObjCreateCo( p->pFrm, pObj );
    Aig_ManPrintStats( p->pFrm );
    Aig_ManCleanup( p->pFrm );
    Aig_ManPrintStats( p->pFrm );
} 

Here is the call graph for this function:

◆ Saig_BmcDeriveFailed()

void Saig_BmcDeriveFailed	(	Saig_Bmc_t *	p,
		int	iTargetFail )

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

Synopsis [Solves targets with the given resource limit.]

Description []

SideEffects []

SeeAlso []

Definition at line 645 of file bmcBmc2.c.

{
    int k;
    p->iOutputFail = p->iOutputLast;
    p->iFrameFail  = p->iFrameLast;
    for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
    {
        if ( p->iOutputFail == 0 )
        {
            p->iOutputFail = Saig_ManPoNum(p->pAig);
            p->iFrameFail--;
        }
        p->iOutputFail--;
    }
}

Here is the caller graph for this function:

◆ Saig_BmcGenerateCounterExample()

Abc_Cex_t * Saig_BmcGenerateCounterExample ( Saig_Bmc_t * p )

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

Synopsis [Solves targets with the given resource limit.]

Description []

SideEffects []

SeeAlso []

Definition at line 672 of file bmcBmc2.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj, * pObjFrm;
    int i, f, iVarNum;
    // start the counter-example
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
    pCex->iFrame = p->iFrameFail;
    pCex->iPo    = p->iOutputFail;
    // copy the bit data
    for ( f = 0; f <= p->iFrameFail; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFrm = Saig_BmcObjFrame( p, pObj, f );
            if ( pObjFrm == NULL )
                continue;
            iVarNum = Saig_BmcSatNum( p, pObjFrm );
            if ( iVarNum == 0 )
                continue;
            if ( p->pSat2 ? satoko_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
                Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
        }
    }
    // verify the counter example
    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
    {
        printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
        Abc_CexFree( pCex );
        pCex = NULL;
    }
    return pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcInterval()

void Saig_BmcInterval ( Saig_Bmc_t * p )

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

Synopsis [Adds new AIG nodes to the frames.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file bmcBmc2.c.

{
    Aig_Obj_t * pTarget;
    int i, iObj, iFrame;
    int nNodes = Aig_ManObjNum( p->pFrm );
    Vec_PtrClear( p->vTargets );
    p->iFramePrev = p->iFrameLast;
    for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
    { 
        if ( p->iOutputLast == 0 )
        {
            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
        }
        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
        {
            if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
                return;
//            Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
            Vec_IntClear( p->vVisited );
            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
            Vec_PtrPush( p->vTargets, pTarget );
            Aig_ObjCreateCo( p->pFrm, pTarget );
            Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!!
            // check if the node is gone
            Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
                Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
            // it is not efficient to remove nodes, which may be used later!!!
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcIntervalConstruct_rec()

Aig_Obj_t * Saig_BmcIntervalConstruct_rec	(	Saig_Bmc_t *	p,
		Aig_Obj_t *	pObj,
		int	i,
		Vec_Int_t *	vVisited )

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

Synopsis [Explores the possibility of constructing the output.]

Description []

SideEffects []

SeeAlso [] Function*************************************************************

Synopsis [Performs the actual construction of the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 426 of file bmcBmc2.c.

{
    Aig_Obj_t * pRes;
    pRes = Saig_BmcObjFrame( p, pObj, i );
    if ( pRes != NULL )
        return pRes;
    if ( Saig_ObjIsPi( p->pAig, pObj ) )
        pRes = Aig_ObjCreateCi(p->pFrm);
    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
    else if ( Aig_ObjIsCo( pObj ) )
    {
        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
        pRes = Saig_BmcObjChild0( p, pObj, i );
    }
    else 
    {
        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
        if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
            pRes = Aig_ManConst0(p->pFrm);
        else
        {
            Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
            pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
        }
    }
    assert( pRes != NULL );
    Saig_BmcObjSetFrame( p, pObj, i, pRes );
    Vec_IntPush( vVisited, Aig_ObjId(pObj) );
    Vec_IntPush( vVisited, i );
    return pRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcIntervalToAig()

Aig_Man_t * Saig_BmcIntervalToAig ( Saig_Bmc_t * p )

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

Synopsis [Creates AIG of the newly added nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file bmcBmc2.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    Aig_ManForEachObj( p->pFrm, pObj, i )
        assert( pObj->pData == NULL );
 
    pNew = Aig_ManStart( p->nNodesMax );
    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
    Vec_IntClear( p->vVisited );
    Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
    {
//        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
        assert( !Aig_IsComplement(pObjNew) );
        Aig_ObjCreateCo( pNew, pObjNew );
    } 
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcIntervalToAig_rec()

Aig_Obj_t * Saig_BmcIntervalToAig_rec	(	Saig_Bmc_t *	p,
		Aig_Man_t *	pNew,
		Aig_Obj_t *	pObj )

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

Synopsis [Performs the actual construction of the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 512 of file bmcBmc2.c.

{
    if ( pObj->pData )
        return (Aig_Obj_t *)pObj->pData;
    Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
    {
        p->nStitchVars += !Aig_ObjIsCi(pObj);
        return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew));
    }
    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
    assert( pObj->pData == NULL );
    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcLoadCnf()

void Saig_BmcLoadCnf	(	Saig_Bmc_t *	p,
		Cnf_Dat_t *	pCnf )

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

Synopsis [Derives CNF for the newly added nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 572 of file bmcBmc2.c.

{
    Aig_Obj_t * pObj, * pObjNew;
    int i, Lits[2], VarNumOld, VarNumNew;
    Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
    {
        // get the new variable of this node
        pObjNew     = (Aig_Obj_t *)pObj->pData;
        pObj->pData = NULL;
        VarNumNew   = pCnf->pVarNums[ pObjNew->Id ];
        if ( VarNumNew == -1 )
            continue;
        // get the old variable of this node
        VarNumOld   = Saig_BmcSatNum( p, pObj );
        if ( VarNumOld == 0 )
        {
            Saig_BmcSetSatNum( p, pObj, VarNumNew );
            continue;
        }
        // add clauses connecting existing variables
        Lits[0] = toLitCond( VarNumOld, 0 );
        Lits[1] = toLitCond( VarNumNew, 1 );
        if ( p->pSat2 )
        {
            if ( !satoko_add_clause( p->pSat2, Lits, 2 ) )
                assert( 0 );
        }
        else
        {
            if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
                assert( 0 );
        }
        Lits[0] = toLitCond( VarNumOld, 1 );
        Lits[1] = toLitCond( VarNumNew, 0 );
        if ( p->pSat2 )
        {
            if ( !satoko_add_clause( p->pSat2, Lits, 2 ) )
                assert( 0 );
        }
        else
        {
            if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
                assert( 0 );
        }
    }
    // add CNF to the SAT solver
    if ( p->pSat2 )
    {
        for ( i = 0; i < pCnf->nClauses; i++ )
            if ( !satoko_add_clause( p->pSat2, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
                break;
    }
    else
    {
        for ( i = 0; i < pCnf->nClauses; i++ )
            if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
                break;
    }
    if ( i < pCnf->nClauses )
        printf( "SAT solver became UNSAT after adding clauses.\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcManStart()

Saig_Bmc_t * Saig_BmcManStart	(	Aig_Man_t *	pAig,
		int	nFramesMax,
		int	nNodesMax,
		int	nConfMaxOne,
		int	nConfMaxAll,
		int	fVerbose,
		int	fUseSatoko )

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

Synopsis [Create manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file bmcBmc2.c.

{
    Saig_Bmc_t * p;
    Aig_Obj_t * pObj;
    int i, Lit;
//    assert( Aig_ManRegNum(pAig) > 0 );
    p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
    memset( p, 0, sizeof(Saig_Bmc_t) );
    // set parameters
    p->nFramesMax   = nFramesMax;
    p->nNodesMax    = nNodesMax;
    p->nConfMaxOne  = nConfMaxOne;
    p->nConfMaxAll  = nConfMaxAll;
    p->fVerbose     = fVerbose;
    p->pAig         = pAig;
    p->nObjs        = Aig_ManObjNumMax(pAig);
    // create node and variable mappings
    p->vAig2Frm     = Vec_PtrAlloc( 100 );
    p->vObj2Var     = Vec_IntAlloc( 0 );
    Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
    // start the AIG manager and map primary inputs
    p->pFrm         = Aig_ManStart( p->nObjs );
    Saig_ManForEachLo( pAig, pObj, i )
        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
    // create SAT solver
    p->nSatVars     = 1;
    Lit = toLit( p->nSatVars );
    if ( fUseSatoko )
    {
        satoko_opts_t opts;
        satoko_default_opts(&opts);
        opts.conf_limit = nConfMaxOne;
        p->pSat2 = satoko_create();  
        satoko_configure(p->pSat2, &opts);
        satoko_setnvars(p->pSat2, 2000);
        satoko_add_clause( p->pSat2, &Lit, 1 );
    }
    else
    {
        p->pSat = sat_solver_new();
        p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart;
        p->pSat->nLearntDelta =  5000;//p->pPars->nLearnedDelta;
        p->pSat->nLearntRatio =    75;//p->pPars->nLearnedPerce;
        p->pSat->nLearntMax   = p->pSat->nLearntStart;
        sat_solver_setnvars( p->pSat, 2000 );
        sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
    }
    Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
    // other data structures
    p->vTargets     = Vec_PtrAlloc( 1000 );
    p->vVisited     = Vec_IntAlloc( 1000 );
    p->iOutputFail  = -1;
    p->iFrameFail   = -1;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcManStop()

void Saig_BmcManStop ( Saig_Bmc_t * p )

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

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 349 of file bmcBmc2.c.

{
    Aig_ManStop( p->pFrm  );
    Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
    Vec_IntFree( p->vObj2Var );
    if ( p->pSat )  sat_solver_delete( p->pSat );
    if ( p->pSat2 ) satoko_destroy( p->pSat2 );
    Vec_PtrFree( p->vTargets );
    Vec_IntFree( p->vVisited );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcPerform()

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,
		int	fUseSatoko )

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

Synopsis [Performs BMC with the given parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 811 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, fUseSatoko );
    // set runtime limit
    if ( nTimeOut )
    {
        if ( p->pSat2 )
            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
        else
            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, 
                p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) );   
            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 ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_BmcSolveTargets()

int Saig_BmcSolveTargets	(	Saig_Bmc_t *	p,
		int	nStart,
		int *	pnOutsSolved )

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

Synopsis [Solves targets with the given resource limit.]

Description []

SideEffects []

SeeAlso []

Definition at line 717 of file bmcBmc2.c.

{
    Aig_Obj_t * pObj;
    int i, k, VarNum, Lit, status, RetValue;
    assert( Vec_PtrSize(p->vTargets) > 0 );
    if ( p->pSat && p->pSat->qtail != p->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pSat);
        assert( RetValue != 0 );
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
    {
        if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
            continue;
        if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
            return l_Undef;
        VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
        Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
        if ( p->pSat2 )
            RetValue = satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->nConfMaxOne );
        else
            RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( RetValue == l_False ) // unsat
        {
            // add final unit clause
            Lit = lit_neg( Lit );
            if ( p->pSat2 )
                status = satoko_add_clause( p->pSat2, &Lit, 1 );
            else
                status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
            assert( status );
            if ( p->pSat )
            {
                // 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 );
            }
            continue;
        }
        if ( RetValue == l_Undef ) // undecided
            return l_Undef;
        // generate counter-example
        Saig_BmcDeriveFailed( p, i );
        p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
 
        {
//            extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
//            Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
        }
        return l_True;
    }
    return l_False;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ ABS_ONE

◆ ABS_UND

◆ ABS_ZER

Typedef Documentation

◆ Saig_Bmc_t

Function Documentation

◆ Abs_ManExtendOneEval_rec()

◆ Abs_ManFreeAray()

◆ Abs_ManTernarySimulate()

◆ Saig_BmcAddTargetsAsPos()

◆ Saig_BmcDeriveFailed()

◆ Saig_BmcGenerateCounterExample()

◆ Saig_BmcInterval()

◆ Saig_BmcIntervalConstruct_rec()

◆ Saig_BmcIntervalToAig()

◆ Saig_BmcIntervalToAig_rec()

◆ Saig_BmcLoadCnf()

◆ Saig_BmcManStart()

◆ Saig_BmcManStop()

◆ Saig_BmcPerform()

◆ Saig_BmcSolveTargets()