bmcExpand.c File Reference

#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "base/abc/abc.h"

Include dependency graph for bmcExpand.c:

Go to the source code of this file.

Macros
#define	Bmc_SopForEachCube(pSop, nVars, pCube)
	DECLARATIONS ///.

Functions
int	Abc_ObjExpandCubesTry (Vec_Str_t *vSop, sat_solver *pSat, Vec_Int_t *vVars)
	FUNCTION DEFINITIONS ///.
int	Abc_ObjExpandCubes (Vec_Str_t *vSop, Gia_Man_t *p, int nVars)
void	Abc_NtkExpandCubes (Abc_Ntk_t *pNtk, Gia_Man_t *pGia, int fVerbose)

Macro Definition Documentation

Bmc_SopForEachCube

#define Bmc_SopForEachCube	(		pSop,
			nVars,
			pCube )

Value:

for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )

DECLARATIONS ///.

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

FileName [bmcExpand.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Expanding cubes against the offset.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 34 of file bmcExpand.c.

Function Documentation

Abc_NtkExpandCubes()

void Abc_NtkExpandCubes	(	Abc_Ntk_t *	pNtk,
		Gia_Man_t *	pGia,
		int	fVerbose )

Definition at line 135 of file bmcExpand.c.

{
    Gia_Man_t * pNew;
    Abc_Obj_t * pObj; int i;
    Vec_Str_t * vSop = Vec_StrAlloc( 1000 );
    assert( Abc_NtkIsSopLogic(pNtk) );
    assert( Abc_NtkCiNum(pNtk) == Gia_ManCiNum(pGia) );
    assert( Abc_NtkCoNum(pNtk) == Gia_ManCoNum(pGia) );
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        pObj = Abc_ObjFanin0(pObj);
        if ( !Abc_ObjIsNode(pObj) || Abc_ObjFaninNum(pObj) == 0 )
            continue;
        assert( Abc_ObjFaninNum(pObj) == Gia_ManCiNum(pGia) );
 
        Vec_StrClear( vSop );
        Vec_StrAppend( vSop, (char *)pObj->pData );
        Vec_StrPush( vSop, '\0' );
 
        pNew = Gia_ManDupCones( pGia, &i, 1, 0 );
        assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pGia) );
        if ( Abc_ObjExpandCubes( vSop, pNew, Abc_ObjFaninNum(pObj) ) )
            Vec_IntClear( &pObj->vFanins );
        Gia_ManStop( pNew );
 
        pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, Vec_StrArray(vSop) );
    }
    Vec_StrFree( vSop );
    Abc_NtkSortSops( pNtk );
}

Here is the call graph for this function:

Abc_ObjExpandCubes()

int Abc_ObjExpandCubes	(	Vec_Str_t *	vSop,
		Gia_Man_t *	p,
		int	nVars )

Definition at line 88 of file bmcExpand.c.

{
    extern int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars );
 
    int fReverse = 0;
    Vec_Int_t * vVars = Vec_IntAlloc( nVars );
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
    int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars;
 
    // check that on-set/off-set is sat
    int iOutVar = 1;
    for ( n = 0; n < 2; n++ )
    {
        iLit  = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1   n=1 => F=0
        status = sat_solver_solve( pSat, &iLit, &iLit + 1, 0, 0, 0, 0 );
        if ( status == l_False )
        {
            Vec_StrClear( vSop );
            Vec_StrPrintStr( vSop, n ? " 1\n" : " 0\n" );
            Vec_StrPush( vSop, '\0' );
            return 1;
        }
    }
 
    // add literals to the solver
    iLit  = Abc_Var2Lit( iOutVar, 1 ); 
    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
    assert( status );
 
    // collect variables
    if ( fReverse )
        for ( v = nVars - 1; v >= 0; v-- )
            Vec_IntPush( vVars, iCiVarBeg + v );
    else
        for ( v = 0; v < nVars; v++ )
            Vec_IntPush( vVars, iCiVarBeg + v );
 
    nCubesNew = Abc_ObjExpandCubesTry( vSop, pSat, vVars );
 
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Vec_IntFree( vVars );
    if ( nCubesNew > 1 )
        Bmc_CollapseIrredundantFull( vSop, nCubesNew, nVars );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_ObjExpandCubesTry()

int Abc_ObjExpandCubesTry	(	Vec_Str_t *	vSop,
		sat_solver *	pSat,
		Vec_Int_t *	vVars )

FUNCTION DEFINITIONS ///.

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

Synopsis [Expands cubes against the offset given as an AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file bmcExpand.c.

{
    extern int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit );
 
    char * pCube, * pSop = Vec_StrArray(vSop);
    int nCubes = Abc_SopGetCubeNum(pSop);
    int nVars = Abc_SopGetVarNum(pSop);
 
    Vec_Int_t * vLits = Vec_IntAlloc( nVars );
    Vec_Int_t * vTemp = Vec_IntAlloc( nVars );
 
    assert( nVars == Vec_IntSize(vVars) );
    assert( Vec_StrSize(vSop) == nCubes * (nVars + 3) + 1 );
    Bmc_SopForEachCube( pSop, nVars, pCube )
    {
        int k, Entry;
        // collect literals and clean cube
        Vec_IntFill( vLits, nVars, -1 );
        for ( k = 0; k < nVars; k++ )
        {
            if ( pCube[k] == '-' )
                continue;
            Vec_IntWriteEntry( vLits, k, Abc_Var2Lit(Vec_IntEntry(vVars, k), pCube[k] == '0') );
            pCube[k] = '-';
        }
        // expand cube
        Bmc_CollapseExpandRound( pSat, NULL, vLits, NULL, vTemp, 0, 0, -1 );
        // insert literals
        Vec_IntForEachEntry( vLits, Entry, k )
            if ( Entry != -1 )
                pCube[k] = '1' - Abc_LitIsCompl(Entry);
    }
 
    Vec_IntFree( vLits );
    Vec_IntFree( vTemp );
    return nCubes;
}

Here is the call graph for this function:

Here is the caller graph for this function: