int2Int.h File Reference

#include "aig/gia/gia.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"
#include "int2.h"

Go to the source code of this file.

Data Structures
struct	Int2_Man_t_
	DECLARATIONS ///. More...

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_	Int2_Man_t
	INCLUDES ///. More...

Functions
static Int2_Man_t *	Int2_ManCreate (Gia_Man_t *pGia, Int2_ManPars_t *pPars)
static void	Int2_ManStop (Int2_Man_t *p)
int	Int2_ManCheckInit (Gia_Man_t *p)
	MACRO DEFINITIONS ///. More...
Gia_Man_t *	Int2_ManDupInit (Gia_Man_t *p, int fVerbose)
	DECLARATIONS ///. More...
sat_solver *	Int2_ManSetupBmcSolver (Gia_Man_t *p, int nFrames)
void	Int2_ManCreateFrames (Int2_Man_t *p, int iFrame, Vec_Int_t *vPrefCos)
int	Int2_ManCheckBmc (Int2_Man_t *p, Vec_Int_t *vCube)
Vec_Int_t *	Int2_ManRefineCube (Gia_Man_t *p, Vec_Int_t *vAssign, Vec_Int_t *vPrio)
Gia_Man_t *	Int2_ManProbToGia (Gia_Man_t *p, Vec_Int_t *vSop)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_ Int2_Man_t

INCLUDES ///.

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

FileName [int2Int.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 1, 2013.]

Revision [

Id:

int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 45 of file int2Int.h.

Function Documentation

int Int2_ManCheckBmc	(	Int2_Man_t *	p,
		Vec_Int_t *	vCube
	)

Definition at line 318 of file int2Bmc.c.

{
    int status;
    if ( vCube == NULL )
    {
        Gia_Obj_t * pObj;
        int i, iLit;
        Gia_ManForEachPo( p->pGia, pObj, i )
        {
            iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
            if ( iLit == 0 )
                continue;
            if ( iLit == 1 )
                return 0;
            status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
            if ( status == l_False )
                continue;
            if ( status == l_True )
                return 0;
            return -1;
        }
        return 1;
    }
    status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
    if ( status == l_False )
        return 1;
    if ( status == l_True )
        return 0;
    return -1;
}

int Int2_ManCheckInit

(

Gia_Man_t *

p

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Returns 1 if AIG has transition into init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file int2Bmc.c.

{
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    Vec_Int_t * vLits;
    int i, Lit, RetValue = 0;
    assert( Gia_ManRegNum(p) > 0 );
    pNew = Jf_ManDeriveCnf( p, 0 );  
    pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat != NULL )
    {
        vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
        Gia_ManForEachRi( pNew, pObj, i )
        {
            Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
            Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
            Vec_IntPush( vLits, Abc_LitNot(Lit) );
        }
        if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
            RetValue = 1;
        Vec_IntFree( vLits );
        sat_solver_delete( pSat );
    }
    Cnf_DataFree( pCnf );
    Gia_ManStop( pNew );
    return RetValue;
}

static Int2_Man_t* Int2_ManCreate ( Gia_Man_t *  pGia, Int2_ManPars_t *  pPars  )

inlinestatic

Definition at line 79 of file int2Int.h.

{
    Int2_Man_t * p;
    p = ABC_CALLOC( Int2_Man_t, 1 );
    p->pPars       = pPars;
    p->pGia        = pGia;
    p->pGiaPref    = Gia_ManStart( 10000 );
    // perform structural hashing
    Gia_ManHashAlloc( pFrames );
    // subset of the manager
    p->vSuffCis    = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    p->vSuffCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
    p->vPrefCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
    p->vStack      = Vec_IntAlloc( 10000 );
    // preimages
    p->vImageOne   = Vec_IntAlloc( 1000 );
    p->vImagesAll  = Vec_IntAlloc( 1000 );
    // variable maps
    p->vMapFrames  = Vec_PtrAlloc( 100 );
    p->vMapPref    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
    p->vMapSuff    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
    // initial minimization
    p->vAssign     = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    p->vPrio       = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    return p;
}

void Int2_ManCreateFrames	(	Int2_Man_t *	p,
		int	iFrame,
		Vec_Int_t *	vPrefCos
	)

Definition at line 219 of file int2Bmc.c.

{
    Gia_Obj_t * pObj;
    int i, Entry, iLit;
    // create storage room for unfolded IDs
    for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
        Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
    assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
    // create constant 0 node
    if ( f == 0 )
    {
        iLit = 1;
        Int2_ManWriteFrames( p, iFrame, iObj, 0 );
        sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
    }
    // start the stack
    Vec_IntClear( p->vStack );
    Vec_IntForEachEntry( vPrefCos, Entry, i )
    {
        pObj = Gia_ManCo( p->pGia, Entry );
        Vec_IntPush( p->vStack, iFrame );
        Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
    }
    // construct unfolded AIG
    while ( Vec_IntSize(p->vStack) > 0 )
    {
        int iObj   = Vec_IntPop(p->vStack);
        int iFrame = Vec_IntPop(p->vStack);
        if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
            continue;
        pObj = Gia_ManObj( p->pGia, iObj );
        if ( Gia_ObjIsPi(p->pGia, pObj) )
            Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
        else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
            Int2_ManWriteFrames( p, iFrame, iObj, 0 );
        else if ( Gia_ObjIsRo(p->pGia, iObj) )
        {
            int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
            int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
            if ( iLit >= 0 )
                Int2_ManWriteFrames( p, iFrame, iObj, iLit );
            else
            {
                Vec_IntPush( p->vStack, iFrame );
                Vec_IntPush( p->vStack, iObj );
                Vec_IntPush( p->vStack, iFrame-1 );
                Vec_IntPush( p->vStack, iObjF );
            }
        }
        else if ( Gia_ObjIsCo(pObj) )
        {
            int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
            int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
            if ( iLit >= 0 )
                Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
            else
            {
                Vec_IntPush( p->vStack, iFrame );
                Vec_IntPush( p->vStack, iObj );
                Vec_IntPush( p->vStack, iFrame );
                Vec_IntPush( p->vStack, iObjF );
            }
        }
        else if ( Gia_ObjIsAnd(pObj) )
        {
            int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
            int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
            int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
            int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
            if ( iLit0 >= 0 && iLit1 >= 0 )
            {
                Entry = Gia_ManObjNum(pFrames);
                iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
                Int2_ManWriteFrames( p, iFrame, iObj, iLit );
                if ( Entry < Gia_ManObjNum(pFrames) )
                {
                    assert( !Abc_LitIsCompl(iLit) );
                    sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 ); 
                }
            }
            else
            {
                Vec_IntPush( p->vStack, iFrame );
                Vec_IntPush( p->vStack, iObj );
                if ( iLit0 < 0 )
                {
                    Vec_IntPush( p->vStack, iFrame );
                    Vec_IntPush( p->vStack, iObjF0 );
                }
                if ( iLit1 < 0 )
                {
                    Vec_IntPush( p->vStack, iFrame );
                    Vec_IntPush( p->vStack, iObjF1 );
                }
            }
        }
        else assert( 0 );
    }
}

Gia_Man_t* Int2_ManDupInit	(	Gia_Man_t *	p,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [int2Bmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [BMC used inside IMC.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 1, 2013.]

Revision [

Id:

int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Trasnforms AIG to transition into the init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file int2Bmc.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
    int i, iCtrl;
    assert( Gia_ManRegNum(p) > 0 );
    pNew = Gia_ManStart( 10000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
    {
        if ( i == Gia_ManPiNum(p) )
            iCtrl = Gia_ManAppendCi( pNew );
        pObj->Value = Gia_ManAppendCi( pNew );
    }
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachAnd( p, pObj, i )
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Gia_ManForEachPo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
        Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    // remove dangling
    pNew = Gia_ManCleanup( pTemp = pNew );
    if ( fVerbose )
        printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", 
            Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
    Gia_ManStop( pTemp );
    return pNew;
}

Gia_Man_t* Int2_ManProbToGia	(	Gia_Man_t *	p,
		Vec_Int_t *	vSop
	)

Definition at line 98 of file int2Util.c.

{
    Vec_Int_t * vCoPres, * vNodes;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;
    int i, k, Entry, Limit;
    int Lit, Cube, Sop;
    assert( Gia_ManPoNum(p) == 1 );
    // collect COs and ANDs
    vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) );
    vNodes = Int2_ManCollectInternal( p, vCoPres );
    // create new manager
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Vec_IntForEachEntry( vCoPres, Entry, i )
    {
        pObj = Gia_ManCo(p, Entry);
        pObj->Value = Gia_ObjFanin0Copy( pObj );
    }
    // create additional cubes
    Sop = 0;
    Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
    {
        Cube = 1;
        for ( k = 0; k < Limit; k++ )
        {
            i++;
            Lit = Vec_IntEntry( vSop, i + k );
            pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) );
            Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) );
        }
        Sop = Gia_ManHashOr( pNew, Sop, Cube );
    }
    Gia_ManAppendCo( pNew, Sop );
    Gia_ManHashStop( pNew );
    // cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Vec_Int_t* Int2_ManRefineCube	(	Gia_Man_t *	p,
		Vec_Int_t *	vAssign,
		Vec_Int_t *	vPrio
	)

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

Synopsis [Computes the reduced set of flop variables.]

Description [Given is a single-output seq AIG manager and an assignment of its CIs. Returned is a subset of flops that justifies the output.]

SideEffects []

SeeAlso []

Definition at line 104 of file int2Refine.c.

{
    Vec_Int_t * vSubset;
    Gia_Obj_t * pObj;
    int i;
    // set values and prios
    assert( Gia_ManRegNum(p) > 0 );
    assert( Vec_IntSize(vAssign) == Vec_IntSize(vPrio) );
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManConst0(p)->fMark1 = 0;
    Gia_ManConst0(p)->Value = ABC_INFINITY;
    Gia_ManForEachCi( p, pObj, i )
    {
        pObj->fMark0 = Vec_IntEntry(vAssign, i);
        pObj->fMark1 = 0;
        pObj->Value  = Vec_IntEntry(vPrio, i);        
    }
    Gia_ManForEachAnd( p, pObj, i )
    {
        pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
        pObj->fMark1 = 0;
        if ( pObj->fMark0 == 1 )
            pObj->Value = Abc_MaxInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
        else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
            pObj->Value = Abc_MinInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); // choice
        else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
            pObj->Value = Gia_ObjFanin0(pObj)->Value;
        else 
            pObj->Value = Gia_ObjFanin1(pObj)->Value;
    }
    pObj = Gia_ManPo( p, 0 );
    pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
    pObj->fMark1 = 0;
    pObj->Value  = Gia_ObjFanin0(pObj)->Value;
    assert( pObj->fMark0 == 1 );
    assert( pObj->Value < ABC_INFINITY );
    // select subset
    vSubset = Vec_IntAlloc( 100 );
    Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSubset );
    return vSubset;
}

sat_solver* Int2_ManSetupBmcSolver	(	Gia_Man_t *	p,
		int	nFrames
	)

Definition at line 170 of file int2Bmc.c.

{
    Gia_Man_t * pFrames, * pTemp;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    // unfold for the given number of timeframes
    pFrames = Int2_ManFrameInit( p, nFrames, 1 );
    assert( Gia_ManRegNum(pFrames) == 0 );
    // derive CNF for the timeframes
    pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 );  Gia_ManStop( pTemp );
    pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
    // create SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat != NULL )
    {
        Gia_Obj_t * pObj;
        int i, nVars = sat_solver_nvars( pSat );
        sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
        // add clauses for the POs
        Gia_ManForEachCo( pFrames, pObj, i )
            sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
    }
    Cnf_DataFree( pCnf );
    Gia_ManStop( pFrames );
    return pSat;
}

static void Int2_ManStop ( Int2_Man_t *  p )

inlinestatic

Definition at line 105 of file int2Int.h.

{
    // GIA managers
    Gia_ManStopP( &p->pGiaPref );
    Gia_ManStopP( &p->pGiaSuff );
    // subset of the manager
    Vec_IntFreeP( &p->vSuffCis );
    Vec_IntFreeP( &p->vSuffCos );
    Vec_IntFreeP( &p->vPrefCos );
    Vec_IntFreeP( &p->vStack );
    // preimages
    Vec_IntFreeP( &p->vImageOne );
    Vec_IntFreeP( &p->vImagesAll );
    // variable maps
    Vec_VecFree( (Vec_Vec_t *)p->vMapFrames );
    Vec_IntFreeP( &p->vMapPref );
    Vec_IntFreeP( &p->vMapSuff );
    // initial minimization
    Vec_IntFreeP( &p->vAssign );
    Vec_IntFreeP( &p->vPrio );
    // SAT solving
    if ( p->pSatPref )
        sat_solver_delete( p->pSatPref );
    if ( p->timeSatSuff )
        sat_solver_delete( p->pSatSuff );
    ABC_FREE( p );
}