bmcBmcAnd.c File Reference

#include "bmc.h"
#include "aig/gia/giaAig.h"
#include "sat/bsat/satStore.h"
#include "sat/cnf/cnf.h"

Go to the source code of this file.

Data Structures
struct	Bmc_Mna_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Bmc_Mna_t_	Bmc_Mna_t
	DECLARATIONS ///. More...

Functions
static int	Gia_ManTerSimInfoGet (unsigned *pInfo, int i)
static void	Gia_ManTerSimInfoSet (unsigned *pInfo, int i, int Value)
Vec_Ptr_t *	Bmc_MnaTernary (Gia_Man_t *p, int nFrames, int nFramesAdd, int fVerbose, int *iFirst)
	FUNCTION DEFINITIONS ///. More...
void	Bmc_MnaCollect_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes, unsigned *pState)
void	Bmc_MnaCollect (Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, unsigned *pState)
void	Bmc_MnaSelect_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves)
void	Bmc_MnaSelect (Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, Vec_Int_t *vLeaves)
void	Bmc_MnaBuild_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew, Vec_Int_t *vMap, Vec_Int_t *vPiMap)
void	Bmc_MnaBuild (Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, Gia_Man_t *pNew, Vec_Int_t *vMap, Vec_Int_t *vPiMap)
Gia_Man_t *	Gia_ManBmcUnroll (Gia_Man_t *pGia, int nFramesMax, int nFramesAdd, int fVerbose, Vec_Int_t **pvPiMap)
Bmc_Mna_t *	Bmc_MnaAlloc ()
void	Bmc_MnaFree (Bmc_Mna_t *p)
Gia_Man_t *	Gia_ManBmcDupCone (Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vNodes, Vec_Int_t *vOuts)
int	Gia_ManBmcAssignVarIds (Bmc_Mna_t *p, Vec_Int_t *vIns, Vec_Int_t *vUsed, Vec_Int_t *vOuts)
void	Gia_ManBmcAddCnf (Bmc_Mna_t *p, Gia_Man_t *pGia, Vec_Int_t *vIns, Vec_Int_t *vNodes, Vec_Int_t *vOuts)
void	Gia_ManBmcAddCone_rec (Bmc_Mna_t *p, Gia_Obj_t *pObj)
void	Gia_ManBmcAddCone (Bmc_Mna_t *p, int iStart, int iStop)
int	Gia_ManBmcCheckOutputs (Gia_Man_t *pFrames, int iStart, int iStop)
int	Gia_ManBmcFindFirst (Gia_Man_t *pFrames)
int	Gia_ManBmcPerform_Unr (Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
Abc_Cex_t *	Gia_ManBmcCexGen (Bmc_Mna_t *pMan, Gia_Man_t *p, int iOut)
int	Gia_ManBmcPerform_old_cnf (Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
void	Gia_ManBmcAddCnfNew_rec (Bmc_Mna_t *p, Gia_Obj_t *pObj)
void	Gia_ManBmcAddCnfNew (Bmc_Mna_t *p, int iStart, int iStop)
static Cnf_Dat_t *	Cnf_DeriveGia (Gia_Man_t *p)
int	Gia_ManBmcPerformInt (Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
int	Gia_ManBmcPerform (Gia_Man_t *pGia, Bmc_AndPar_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Bmc_Mna_t_ Bmc_Mna_t

DECLARATIONS ///.

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

FileName [bmcBmcAnd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Memory-efficient BMC engine]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 33 of file bmcBmcAnd.c.

Function Documentation

Bmc_Mna_t* Bmc_MnaAlloc

(

)

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

Synopsis [BMC manager manipulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 389 of file bmcBmcAnd.c.

{
    Bmc_Mna_t * p;
    p = ABC_CALLOC( Bmc_Mna_t, 1 );
    p->vId2Var   = Vec_IntAlloc( 0 );
    p->vInputs   = Vec_IntAlloc( 1000 );
    p->vOutputs  = Vec_IntAlloc( 1000 );
    p->vNodes    = Vec_IntAlloc( 10000 );
    p->pSat      = sat_solver_new();
    p->nSatVars  = 1;
    p->clkStart  = Abc_Clock();
    sat_solver_setnvars( p->pSat, 1000 );
    return p;
}

void Bmc_MnaBuild	(	Gia_Man_t *	p,
		Vec_Int_t *	vCos,
		Vec_Int_t *	vNodes,
		Gia_Man_t *	pNew,
		Vec_Int_t *	vMap,
		Vec_Int_t *	vPiMap
	)

Definition at line 256 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i, iLit;
    Gia_ManForEachObjVec( vCos, p, pObj, i )
    {
        assert( Gia_ObjIsCo(pObj) );
        Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
        iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
        Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit );
    }
    Gia_ManConst0(p)->fPhase = 0;
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->fPhase = 0;
}

void Bmc_MnaBuild_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Gia_Man_t *	pNew,
		Vec_Int_t *	vMap,
		Vec_Int_t *	vPiMap
	)

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

Synopsis [Build AIG for the selected cones.]

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file bmcBmcAnd.c.

{
    if ( !pObj->fPhase )
        return;
    pObj->fPhase = 0;
    assert( pObj->Value == GIA_UND );
    if ( Gia_ObjIsAnd(pObj) )
    {
        int iLit0 = 1, iLit1 = 1;
        if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
            Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
        if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
            Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap, vPiMap );
        if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
            iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
        if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
            iLit1 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId1p(p, pObj)), Gia_ObjFaninC1(pObj) );
        Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManHashAnd(pNew, iLit0, iLit1) );
    }
    else if ( Gia_ObjIsRo(p, pObj) )
        assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 );
    else if ( Gia_ObjIsPi(p, pObj) )
    {
        Vec_IntPush( vPiMap, Gia_ObjCioId(pObj) );
        Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
    }
    else assert( 0 );
}

void Bmc_MnaCollect	(	Gia_Man_t *	p,
		Vec_Int_t *	vCos,
		Vec_Int_t *	vNodes,
		unsigned *	pState
	)

Definition at line 160 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i;
    Vec_IntClear( vNodes );
    Gia_ManConst0(p)->fPhase = 1;
    Gia_ManConst0(p)->Value = GIA_ZER;
    Gia_ManForEachObjVec( vCos, p, pObj, i )
    {
        assert( Gia_ObjIsCo(pObj) );
        Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
        pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
        assert( pObj->Value == GIA_UND );
    }
}

void Bmc_MnaCollect_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vNodes,
		unsigned *	pState
	)

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

Synopsis [Collect AIG nodes for the group of POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file bmcBmcAnd.c.

{
    if ( pObj->fPhase )
        return;
    pObj->fPhase = 1;
    if ( Gia_ObjIsAnd(pObj) )
    {
        Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
        Bmc_MnaCollect_rec( p, Gia_ObjFanin1(pObj), vNodes, pState );
        pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
    }
    else if ( Gia_ObjIsRo(p, pObj) )
        pObj->Value = pState ? Gia_ManTerSimInfoGet( pState, Gia_ObjCioId(Gia_ObjRoToRi(p, pObj)) ) : GIA_ZER;
    else if ( Gia_ObjIsPi(p, pObj) )
        pObj->Value = GIA_UND;
    else assert( 0 );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}

void Bmc_MnaFree

(

Bmc_Mna_t *

p

)

Definition at line 403 of file bmcBmcAnd.c.

{
    Cnf_DataFree( p->pCnf );
    Vec_IntFreeP( &p->vPiMap );
    Vec_IntFreeP( &p->vId2Var );
    Vec_IntFreeP( &p->vInputs );
    Vec_IntFreeP( &p->vOutputs );
    Vec_IntFreeP( &p->vNodes );
    sat_solver_delete( p->pSat );
    ABC_FREE( p );
}

void Bmc_MnaSelect	(	Gia_Man_t *	p,
		Vec_Int_t *	vCos,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vLeaves
	)

Definition at line 205 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i;
    Vec_IntClear( vLeaves );
    Gia_ManForEachObjVec( vCos, p, pObj, i )
        Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
    Gia_ManConst0(p)->fPhase = 0;
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->fPhase = 0;
}

void Bmc_MnaSelect_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vLeaves
	)

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

Synopsis [Select related logic cones for the COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file bmcBmcAnd.c.

{
    if ( !pObj->fPhase )
        return;
    pObj->fPhase = 0;
    assert( pObj->Value == GIA_UND );
    if ( Gia_ObjIsAnd(pObj) )
    {
        if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
            Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
        else assert( Gia_ObjFanin0(pObj)->Value + Gia_ObjFaninC0(pObj) == GIA_ONE );
        if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
            Bmc_MnaSelect_rec( p, Gia_ObjFanin1(pObj), vLeaves );
        else assert( Gia_ObjFanin1(pObj)->Value + Gia_ObjFaninC1(pObj) == GIA_ONE );
    }
    else if ( Gia_ObjIsRo(p, pObj) )
        Vec_IntPush( vLeaves, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
}

Vec_Ptr_t* Bmc_MnaTernary	(	Gia_Man_t *	p,
		int	nFrames,
		int	nFramesAdd,
		int	fVerbose,
		int *	iFirst
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs ternary simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file bmcBmcAnd.c.

{
    Vec_Ptr_t * vStates;
    unsigned * pState;
    int nStateWords = Abc_BitWordNum( 2*Gia_ManCoNum(p) );
    Gia_Obj_t * pObj, * pObjRo;
    int f, i, Count[4];
    abctime clk = Abc_Clock();
    Gia_ManConst0(p)->Value = GIA_ZER;
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = GIA_UND;
    Gia_ManForEachRi( p, pObj, i )
        pObj->Value = GIA_ZER;
    *iFirst = -1;
    vStates = Vec_PtrAlloc( 100 );
    for ( f = 0; ; f++ )
    {
        // if frames are given, break at frames
        if ( nFrames && f == nFrames )
            break;
        // if frames are not given, break after nFramesAdd from the first x-valued
        if ( !nFrames && *iFirst >= 0 && f == *iFirst + nFramesAdd )
            break;
        // aassign CI values
        Gia_ManForEachRiRo( p, pObj, pObjRo, i )
            pObjRo->Value = pObj->Value;
        Gia_ManForEachAnd( p, pObj, i )
            pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
        // compute and save CO values
        pState = ABC_ALLOC( unsigned, nStateWords );
        Gia_ManForEachCo( p, pObj, i )
        {
            pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
            Gia_ManTerSimInfoSet( pState, i, pObj->Value );
            if ( *iFirst == -1 && i < Gia_ManPoNum(p) && pObj->Value == GIA_UND )
                *iFirst = f;
        }
        Vec_PtrPush( vStates, pState );
        // print statistics
        if ( !fVerbose )
            continue;
        Count[0] = Count[1] = Count[2] = Count[3] = 0;
        Gia_ManForEachRi( p, pObj, i )
            Count[pObj->Value]++;
        printf( "%5d : 0 =%7d    1 =%7d    x =%7d    all =%7d   out = %s\n", 
            f, Count[GIA_ZER], Count[GIA_ONE], Count[GIA_UND], Gia_ManRegNum(p), 
            Gia_ManPo(p, 0)->Value == GIA_UND ? "x" : "0" );  
    }
//    assert( Vec_PtrSize(vStates) == nFrames );
    if ( fVerbose )
        printf( "Finished %d frames. First x-valued PO is in frame %d.  ", nFrames, *iFirst );
    if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return vStates;
}

static Cnf_Dat_t* Cnf_DeriveGia ( Gia_Man_t *  p )

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 937 of file bmcBmcAnd.c.

{
    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
    Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 );
    Aig_ManStop( pAig );
    return pCnf;
}

void Gia_ManBmcAddCnf	(	Bmc_Mna_t *	p,
		Gia_Man_t *	pGia,
		Vec_Int_t *	vIns,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vOuts
	)

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

Synopsis [Derives CNF for the given cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file bmcBmcAnd.c.

{
    Gia_Man_t * pNew = Gia_ManBmcDupCone( pGia, vIns, vNodes, vOuts );
    Aig_Man_t * pAig = Gia_ManToAigSimple( pNew );
    Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
    Vec_Int_t * vUsed, * vMap;
    Gia_Obj_t * pObj;
    int i, iObj, VarC0;
    // collect used variables
    vUsed = Vec_IntAlloc( pCnf->nVars - Vec_IntSize(vIns) - Vec_IntSize(vOuts) );
    Gia_ManForEachAnd( pNew, pObj, i )
        if ( pCnf->pVarNums[i] >= 0 )
            Vec_IntPush( vUsed, Vec_IntEntry(vNodes, i - Vec_IntSize(vIns) - 1) );
    // assign variable IDs
    VarC0 = Gia_ManBmcAssignVarIds( p, vIns, vUsed, vOuts );
    Vec_IntFree( vUsed );
    // create variable map from CNF vars into SAT vars
    vMap = Vec_IntStartFull( pCnf->nVars );
    assert( pCnf->pVarNums[0] > 0 );
    Vec_IntWriteEntry( vMap, pCnf->pVarNums[0], VarC0 );
    Gia_ManForEachObj1( pNew, pObj, i )
    {
        if ( pCnf->pVarNums[i] < 0 )
            continue;
        assert( pCnf->pVarNums[i] >= 0 && pCnf->pVarNums[i] < pCnf->nVars );
        if ( Gia_ObjIsCi(pObj) )
            iObj = Vec_IntEntry( vIns, i - 1 );
        else if ( Gia_ObjIsAnd(pObj) )
            iObj = Vec_IntEntry( vNodes, i - Vec_IntSize(vIns) - 1 );
        else if ( Gia_ObjIsCo(pObj) )
            iObj = Vec_IntEntry( vOuts, i - Vec_IntSize(vIns) - Vec_IntSize(vNodes) - 1 );
        else assert( 0 );
        assert( Vec_IntEntry(p->vId2Var, iObj) > 0 );
        Vec_IntWriteEntry( vMap, pCnf->pVarNums[i], Vec_IntEntry(p->vId2Var, iObj) );
    }
//Vec_IntPrint( vMap );
    // remap CNF
    for ( i = 0; i < pCnf->nLiterals; i++ )
    {
        assert( pCnf->pClauses[0][i] > 1 && pCnf->pClauses[0][i] < 2 * pCnf->nVars );
        pCnf->pClauses[0][i] = Abc_Lit2LitV( Vec_IntArray(vMap), pCnf->pClauses[0][i] );
    }
    Vec_IntFree( vMap );
    // add clauses
    for ( i = 0; i < pCnf->nClauses; i++ )
    {
/*
        int v;
        for ( v = 0; v < pCnf->pClauses[i+1] - pCnf->pClauses[i]; v++ )
            printf( "%d ", pCnf->pClauses[i][v] );
        printf( "\n" );
*/
        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" );
    Aig_ManStop( pAig );
    Cnf_DataFree( pCnf );
    Gia_ManStop( pNew );
}

void Gia_ManBmcAddCnfNew	(	Bmc_Mna_t *	p,
		int	iStart,
		int	iStop
	)

Definition at line 913 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i;
    for ( i = iStart; i < iStop; i++ )
    {
        pObj = Gia_ManPo(p->pFrames, i);
        if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p->pFrames) )
            continue;
        Gia_ManBmcAddCnfNew_rec( p, pObj );
    }
}

void Gia_ManBmcAddCnfNew_rec	(	Bmc_Mna_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 868 of file bmcBmcAnd.c.

{
    int iObj = Gia_ObjId( p->pFrames, pObj );
    if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
    {
        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
        return;
    }
    if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
        return;
    Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
    if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
    {
        int i, nClas, iCla;
        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
        if ( Gia_ObjIsAnd(pObj) )
        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
        // extend the SAT solver
        if ( p->nSatVars > sat_solver_nvars(p->pSat) )
            sat_solver_setnvars( p->pSat, p->nSatVars );
        // add clauses
        nClas = p->pCnf->pObj2Count[iObj];
        iCla  = p->pCnf->pObj2Clause[iObj];
        for ( i = 0; i < nClas; i++ )
        {
            int nLits, pLits[8];
            int * pClauseThis = p->pCnf->pClauses[iCla+i];
            int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
            for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
            {
                if ( pClauseThis[nLits] < 2 )
                    printf( "\n\n\nError in CNF generation:  Constant literal!\n\n\n" );
                assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
                pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
            }
            assert( nLits < 8 );
            if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
                break;
        }
        if ( i < nClas )
            printf( "SAT solver became UNSAT after adding clauses.\n" );
    }
    else assert( Gia_ObjIsCi(pObj) );
}

void Gia_ManBmcAddCone	(	Bmc_Mna_t *	p,
		int	iStart,
		int	iStop
	)

Definition at line 589 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i;
    Vec_IntClear( p->vNodes );
    Vec_IntClear( p->vInputs );
    Vec_IntClear( p->vOutputs );
    Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
    for ( i = iStart; i < iStop; i++ )
    {
        pObj = Gia_ManPo(p->pFrames, i);
        if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
            continue;
        Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
        Vec_IntPush( p->vOutputs, Gia_ObjId(p->pFrames, pObj) );
    }
    // clean attributes and create new variables
    Gia_ManForEachObjVec( p->vNodes, p->pFrames, pObj, i )
        pObj->fMark0 = 0;
    Gia_ManForEachObjVec( p->vInputs, p->pFrames, pObj, i )
        pObj->fMark0 = 0;
}

void Gia_ManBmcAddCone_rec	(	Bmc_Mna_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Collects new nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 573 of file bmcBmcAnd.c.

{
    int iObj;
    if ( pObj->fMark0 )
        return;
    pObj->fMark0 = 1;
    iObj = Gia_ObjId( p->pFrames, pObj );
    if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(p->vId2Var, iObj) == 0 )
    {
        Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
        Gia_ManBmcAddCone_rec( p, Gia_ObjFanin1(pObj) );
        Vec_IntPush( p->vNodes, iObj );
    }
    else
        Vec_IntPush( p->vInputs, iObj );
}

int Gia_ManBmcAssignVarIds	(	Bmc_Mna_t *	p,
		Vec_Int_t *	vIns,
		Vec_Int_t *	vUsed,
		Vec_Int_t *	vOuts
	)

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

Synopsis [Derives GIA for the given cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 467 of file bmcBmcAnd.c.

{
    int i, iObj, VarC0 = p->nSatVars++;
    Vec_IntForEachEntry( vIns, iObj, i )
        if ( Vec_IntEntry( p->vId2Var, iObj ) == 0 )
            Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
    Vec_IntForEachEntryReverse( vUsed, iObj, i )
    {
        assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
        Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
    }
    Vec_IntForEachEntry( vOuts, iObj, i )
    {
        assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
        Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
    }
    // extend the SAT solver
    if ( p->nSatVars > sat_solver_nvars(p->pSat) )
        sat_solver_setnvars( p->pSat, p->nSatVars );
    return VarC0;
}

Abc_Cex_t* Gia_ManBmcCexGen	(	Bmc_Mna_t *	pMan,
		Gia_Man_t *	p,
		int	iOut
	)

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

Synopsis [Generate counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 735 of file bmcBmcAnd.c.

{
    Abc_Cex_t * pCex;
    int i, iObjId, iSatVar, iOrigPi;
    int iFramePi = 0, iFrame = -1;
    pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), iOut / Gia_ManPoNum(p) + 1 );
    pCex->iFrame = iOut / Gia_ManPoNum(p);
    pCex->iPo = iOut % Gia_ManPoNum(p);
    // fill in the input values
    Vec_IntForEachEntry( pMan->vPiMap, iOrigPi, i )
    {
        if ( iOrigPi < 0 )
        {
            iFrame = -iOrigPi-1;
            continue;
        }
        // iOrigPi in iFrame of pGia has PI index iFramePi in pMan->pFrames,
        iObjId = Gia_ObjId( pMan->pFrames, Gia_ManPi(pMan->pFrames, iFramePi) );
        iSatVar = Vec_IntEntry( pMan->vId2Var, iObjId );
        if ( sat_solver_var_value(pMan->pSat, iSatVar) )
            Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + Gia_ManPiNum(p) * iFrame + iOrigPi );
        iFramePi++;
    }
    assert( iFramePi == Gia_ManPiNum(pMan->pFrames) );
    return pCex;
}

int Gia_ManBmcCheckOutputs	(	Gia_Man_t *	pFrames,
		int	iStart,
		int	iStop
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 623 of file bmcBmcAnd.c.

{
    int i;
    for ( i = iStart; i < iStop; i++ )
        if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
            return 0;
    return 1;
}

Gia_Man_t* Gia_ManBmcDupCone	(	Gia_Man_t *	p,
		Vec_Int_t *	vIns,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vOuts
	)

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

Synopsis [Derives GIA for the given cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 426 of file bmcBmcAnd.c.

{
    Gia_Man_t * pNew;
    Vec_Int_t * vTempIn, * vTempNode;
    Gia_Obj_t * pObj;
    int i;
    // save values
    vTempIn = Vec_IntAlloc( Vec_IntSize(vIns) );
    Gia_ManForEachObjVec( vIns, p, pObj, i )
        Vec_IntPush( vTempIn, pObj->Value );
    // save values
    vTempNode = Vec_IntAlloc( Vec_IntSize(vNodes) );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        Vec_IntPush( vTempNode, pObj->Value );
    // derive new GIA
    pNew = Gia_ManDupFromVecs( p, vIns, vNodes, vOuts, 0 );
    // reset values
    Gia_ManForEachObjVec( vIns, p, pObj, i )
        pObj->Value = Vec_IntEntry( vTempIn, i );
    // reset values
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->Value = Vec_IntEntry( vTempNode, i );
    // reset values
    Gia_ManForEachObjVec( vOuts, p, pObj, i )
        pObj->Value = 0;
    Vec_IntFree( vTempIn );
    Vec_IntFree( vTempNode );
    return pNew;
}

int Gia_ManBmcFindFirst

(

Gia_Man_t *

pFrames

)

Definition at line 631 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachPo( pFrames, pObj, i )
        if ( Gia_ObjChild0(pObj) != Gia_ManConst0(pFrames) )
            return i;
    return -1;
}

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 Gia_ManBmcPerform_old_cnf	(	Gia_Man_t *	pGia,
		Bmc_AndPar_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 773 of file bmcBmcAnd.c.

{
    Bmc_Mna_t * p;
    int nFramesMax, f, i=0, Lit, status, RetValue = -2;
    abctime clk = Abc_Clock();
    p = Bmc_MnaAlloc();
    p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
    nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
    if ( pPars->fVerbose )
    {
        printf( "Unfolding for %d frames with first non-trivial PO %d.  ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    if ( pPars->fUseSynth )
    {
        Gia_Man_t * pTemp = p->pFrames;
        p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, 0, pPars->fVerbose, 0 );
        Gia_ManStop( pTemp );
    }
    else if ( pPars->fVerbose )
        Gia_ManPrintStats( p->pFrames, NULL );
    if ( pPars->fDumpFrames )
    {
        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
        printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
    }
    for ( f = 0; f < nFramesMax; f++ )
    {
        if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
        {
            // create another slice
            Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
            // create CNF in the SAT solver
            Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
            // try solving the outputs
            for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
            {
                Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
                if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
                    continue;
                Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
                status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( status == l_False ) // unsat
                    continue;
                if ( status == l_True ) // sat
                    RetValue = 0;
                if ( status == l_Undef ) // undecided
                    RetValue = -1;
                break;
            }
            // report statistics
            if ( pPars->fVerbose )
            {
                printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  In =%6d.  And =%9d.  Cla =%9d.  Conf =%9d.  Mem =%7.1f MB   ", 
                    f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), 
                    p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), 
                    sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
            }
        }
        if ( RetValue != -2 )
        {
            if ( RetValue == -1 )
                printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
            else
            {
                ABC_FREE( pGia->pCexSeq );
                pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
                printf( "Output %d of miter \"%s\" was asserted in frame %d.  ", 
                    i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
            }
            break;
        }
        pPars->iFrame = f;
    }
    if ( RetValue == -2 )
        RetValue = -1;
    // cleanup
    Gia_ManStop( p->pFrames );
    Bmc_MnaFree( p );
    return RetValue;
}

int Gia_ManBmcPerform_Unr	(	Gia_Man_t *	pGia,
		Bmc_AndPar_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 652 of file bmcBmcAnd.c.

{
    Unr_Man_t * pUnroll;
    Bmc_Mna_t * p;
    int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
    int f, i=0, Lit, status, RetValue = -2;
    p = Bmc_MnaAlloc();
    pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
    for ( f = 0; f < nFramesMax; f++ )
    {
        p->pFrames = Unr_ManUnrollFrame( pUnroll, f );
        if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
        {
            // create another slice
            Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
            // create CNF in the SAT solver
            Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
            // try solving the outputs
            for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
            {
                Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
                if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
                    continue;
                Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
                status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( status == l_False ) // unsat
                    continue;
                if ( status == l_True ) // sat
                    RetValue = 0;
                if ( status == l_Undef ) // undecided
                    RetValue = -1;
                break;
            }
        }
        // report statistics
        if ( pPars->fVerbose )
        {
            printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  In =%6d.  And =%9d.  Cla =%9d.  Conf =%9d.  Mem =%7.1f MB   ", 
                f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), 
                p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), 
                sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
        }
        if ( RetValue != -2 )
        {
            if ( RetValue == -1 )
                printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
            else
            {
                printf( "Output %d of miter \"%s\" was asserted in frame %d.  ", 
                    i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
            }
            break;
        }
    }
    if ( RetValue == -2 )
        RetValue = -1;
    // dump unfolded frames
    if ( pPars->fDumpFrames )
    {
        p->pFrames = Gia_ManCleanup( p->pFrames );
        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
        printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
        Gia_ManStop( p->pFrames );
    }
    // cleanup
    Unr_ManFree( pUnroll );
    Bmc_MnaFree( p );
    return RetValue;
}

int Gia_ManBmcPerformInt	(	Gia_Man_t *	pGia,
		Bmc_AndPar_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 956 of file bmcBmcAnd.c.

{
    Bmc_Mna_t * p;
    Gia_Man_t * pTemp;
    int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
    abctime clk = Abc_Clock();
    p = Bmc_MnaAlloc();
    sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
    nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
    if ( pPars->fVerbose )
    {
        printf( "Unfolding for %d frames with first non-trivial PO %d.  ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    if ( pPars->fUseSynth )
    {
        p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, 0, pPars->fVerbose, 0 );  Gia_ManStop( pTemp );
    }
    else if ( pPars->fVerbose )
        Gia_ManPrintStats( p->pFrames, NULL );
    if ( pPars->fDumpFrames )
    {
        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
        printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
    }
    if ( pPars->fUseOldCnf )
        p->pCnf = Cnf_DeriveGia( p->pFrames );
    else
    {
        p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 );  Gia_ManStop( pTemp );
        p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
//        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//        p->pCnf = Mf_ManGenerateCnf( p->pFrames, 6, 1, 0, 0 );
    }
    Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
    // create clauses for constant node
//    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
    for ( f = 0; f < nFramesMax; f++ )
    {
        if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
        {
            // create another slice
            Gia_ManBmcAddCnfNew( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
            // try solving the outputs
            for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
            {
                Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
                if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
                    continue;
                if ( Gia_ObjChild0(pObj) == Gia_ManConst1(p->pFrames) )
                {
                    printf( "Output %d is trivially SAT.\n", i );
                    continue;
                }
                Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
                status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( status == l_False ) // unsat
                    continue;
                if ( status == l_True )  // sat
                    RetValue = 0;
                if ( status == l_Undef ) // undecided
                    RetValue = -1;
                break;
            }
            // report statistics
            if ( pPars->fVerbose )
            {
                printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  In =%6d.  And =%9d.  Cla =%9d.  Conf =%9d.  Mem =%7.1f MB   ", 
                    f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), 
                    p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), 
                    sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
            }
        }
        if ( RetValue != -2 )
        {
            if ( RetValue == -1 )
                printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
            else
            {
                ABC_FREE( pGia->pCexSeq );
                pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
                printf( "Output %d of miter \"%s\" was asserted in frame %d.  ", 
                    i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
            }
            break;
        }
        pPars->iFrame = f;
    }
    if ( RetValue == -2 )
        RetValue = -1;
    // cleanup
    Gia_ManStop( p->pFrames );
    Bmc_MnaFree( p );
    return RetValue;
}

Gia_Man_t* Gia_ManBmcUnroll	(	Gia_Man_t *	pGia,
		int	nFramesMax,
		int	nFramesAdd,
		int	fVerbose,
		Vec_Int_t **	pvPiMap
	)

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

Synopsis [Compute the first non-trivial timeframe.]

Description []

SideEffects []

SeeAlso []

Definition at line 284 of file bmcBmcAnd.c.

{
    Gia_Obj_t * pObj;
    Gia_Man_t * pNew, * pTemp;
    Vec_Ptr_t * vStates, * vBegins;
    Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap;
    unsigned * pStateF, * pStateP;
    int f, i, iFirst;
    Gia_ManCleanPhase( pGia );
    vCone = Vec_IntAlloc( 1000 );
    vLeaves = Vec_IntAlloc( 1000 );
    // perform ternary simulation
    vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst );
    // go backward
    *pvPiMap = Vec_IntAlloc( 1000 );
    vBegins = Vec_PtrStart( Vec_PtrSize(vStates) );
    for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- )
    {
        // get ternary states
        pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
        pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
        // collect roots of this frame
        vRoots = Vec_IntAlloc( 100 );
        Gia_ManForEachPo( pGia, pObj, i )
            if ( Gia_ManTerSimInfoGet( pStateF, Gia_ObjCioId(pObj) ) == GIA_UND )
                Vec_IntPush( vRoots, Gia_ObjId(pGia, pObj) );
        // add leaves from the previous frame
        Vec_IntAppend( vRoots, vLeaves );
        Vec_PtrWriteEntry( vBegins, f, vRoots );
        // find the cone
        Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
        Bmc_MnaSelect( pGia, vRoots, vCone, vLeaves );  // computes vLeaves 
        if ( fVerbose )
        printf( "Frame %4d :  Roots = %6d  Leaves = %6d  Cone = %6d\n", 
            f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
        if ( Vec_IntSize(vLeaves) == 0 )
            break;
        // it is possible that some of the POs are still ternary... 
    }
    assert( f >= 0 );
    // go forward
    vMap = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    pNew = Gia_ManStart( 10000 );
    pNew->pName = Abc_UtilStrsav( pGia->pName );
    Gia_ManHashStart( pNew );
    for ( f = 0; f < Vec_PtrSize(vStates); f++ )
    {
        vRoots = (Vec_Int_t *)Vec_PtrEntry( vBegins, f );
        if ( vRoots == NULL )
        {
            Gia_ManForEachPo( pGia, pObj, i )
                Gia_ManAppendCo( pNew, 0 );
            continue;
        }
        // get ternary states
        pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
        pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
        // clean POs
        Gia_ManForEachPo( pGia, pObj, i )
            Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 );
        // find the cone
        Vec_IntPush( *pvPiMap, -f-1 );
        Bmc_MnaCollect( pGia, vRoots, vCone, pStateP );   // computes vCone
        Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap, *pvPiMap );  // computes pNew       
        if ( fVerbose )
        printf( "Frame %4d :  Roots = %6d  Leaves = %6d  Cone = %6d\n", 
            f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
        // create POs
        Gia_ManForEachPo( pGia, pObj, i )
            Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
        // set a new map
        Gia_ManForEachObjVec( vRoots, pGia, pObj, i )
            if ( Gia_ObjIsRi(pGia, pObj) )
                Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, Gia_ObjRiToRo(pGia, pObj)), Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
//            else if ( Gia_ObjIsPo(pGia, pObj) )
//                Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
//            else assert( 0 );
    }
    Gia_ManHashStop( pNew );
    Vec_VecFree( (Vec_Vec_t *)vBegins );
    Vec_PtrFreeFree( vStates );
    Vec_IntFree( vLeaves );
    Vec_IntFree( vCone );
    Vec_IntFree( vMap );
    // cleanup
//    Gia_ManPrintStats( pNew, NULL );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
//    Gia_ManPrintStats( pNew, NULL );
    return pNew;
}

static int Gia_ManTerSimInfoGet ( unsigned *  pInfo, int  i  )

inlinestatic

Definition at line 48 of file bmcBmcAnd.c.

{
    return 3 & (pInfo[i >> 4] >> ((i & 15) << 1));
}

static void Gia_ManTerSimInfoSet ( unsigned *  pInfo, int  i, int  Value  )

inlinestatic

Definition at line 52 of file bmcBmcAnd.c.

{
    assert( Value >= GIA_ZER && Value <= GIA_UND );
    Value ^= Gia_ManTerSimInfoGet( pInfo, i );
    pInfo[i >> 4] ^= (Value << ((i & 15) << 1));
}