int2Core.c File Reference

#include "int2Int.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Int2_ManSetDefaultParams (Int2_ManPars_t *p)
	DECLARATIONS ///. More...
Gia_Man_t *	Int2_ManUnroll (Gia_Man_t *p, int nFrames)
sat_solver *	Int2_ManPreparePrefix (Gia_Man_t *p, int f, Vec_Int_t **pvCiMap)
sat_solver *	Int2_ManPrepareSuffix (Gia_Man_t *p, Vec_Int_t *vImageOne, Vec_Int_t *vImagesAll, Vec_Int_t **pvCoMap, Gia_Man_t **ppSuff)
Vec_Int_t *	Int2_ManComputePreimage (Gia_Man_t *pSuff, sat_solver *pSatPref, sat_solver *pSatSuff, Vec_Int_t *vCiMap, Vec_Int_t *vCoMap, Vec_Int_t *vPrio)
int	Int2_ManPerformInterpolation (Gia_Man_t *pInit, Int2_ManPars_t *pPars)

Function Documentation

Vec_Int_t* Int2_ManComputePreimage	(	Gia_Man_t *	pSuff,
		sat_solver *	pSatPref,
		sat_solver *	pSatSuff,
		Vec_Int_t *	vCiMap,
		Vec_Int_t *	vCoMap,
		Vec_Int_t *	vPrio
	)

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

Synopsis [Returns the cube cover and status.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file int2Core.c.

{
    int i, iVar, status;
    Vec_IntClear( p->vImage );
    while ( 1 )
    {
        // run suffix solver
        status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 );
        if ( status == l_Undef )
            return NULL; // timeout
        if ( status == l_False )
            return INT2_COMPUTED;
        assert( status == l_True );
        // collect assignment
        Vec_IntClear( p->vAssign );
        Vec_IntForEachEntry( p->vCiMap, iVar, i )
            Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) );
        // derive initial cube
        vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio );
        // expend the cube using prefix
        status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
        if ( status == l_False )
        {
            int k, nCoreLits, * pCoreLits;
            nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits );
            // create cube
            Vec_IntClear( vCube );
            Vec_IntPush( vImage, nCoreLits );
            for ( k = 0; k < nCoreLits; k++ )
            {
                Vec_IntPush( vCube, pCoreLits[k] );
                Vec_IntPush( vImage, pCoreLits[k] );
            }
            // add cube to the solver
            if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) )
            {
                Vec_IntFree( vCube );
                return INT2_COMPUTED;
            }
        }
        Vec_IntFree( vCube );
        if ( status == l_Undef )
            return INT2_TIME_OUT;
        if ( status == l_True )
            return INT2_FALSE_NEG;
        assert( status == l_False );
        continue;
    }
    return p->vImage;
}

int Int2_ManPerformInterpolation	(	Gia_Man_t *	pInit,
		Int2_ManPars_t *	pPars
	)

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

Synopsis [Interpolates while the number of conflicts is not exceeded.]

Description [Returns 1 if proven. 0 if failed. -1 if undecided.]

SideEffects [Does not check the property in 0-th frame.]

SeeAlso []

Definition at line 259 of file int2Core.c.

{
    Int2_Man_t * p;
    int f, i, RetValue = -1;
    abctime clk, clkTotal = Abc_Clock(), timeTemp = 0;
    abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;

    // sanity checks
    assert( Gia_ManPiNum(pInit) > 0 );
    assert( Gia_ManPoNum(pInit) > 0 );
    assert( Gia_ManRegNum(pInit) > 0 );

    // create manager
    p = Int2_ManCreate( pInit, pPars );

    // create SAT solver
    p->pSatPref = sat_solver_new();
    sat_solver_setnvars( p->pSatPref, 1000 );
    sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop );

    // check outputs in the first frame
    for ( i = 0; i < Gia_ManPoNum(pInit); i++ )
        Vec_IntPush( p->vPrefCos, i );
    Int2_ManCreateFrames( p, 0, p->vPrefCos );
    RetValue = Int2_ManCheckBmc( p, NULL );
    if ( RetValue != 1 )
        return RetValue;

    // create original image
    for ( f = pPars->nFramesS; f < p->nFramesMax; f++ )
    {
        for ( i = 0; i < p->nFramesMax; i++ )
        {
            p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff );
            sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop );
            Vec_IntFreeP( &vImageOne );
            vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap );
            Vec_IntFree( vCoMap );
            Gia_ManStop( pGiaSuff );
            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
                return -1;
            if ( vImageOne == NULL )
            {
                if ( i == 0 )
                {
                    printf( "Satisfiable in frame %d.\n", f );
                    Vec_IntFree( vCiMap );
                    sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
                    return 0;
                }
                f += i;
                break;
            }
            Vec_IntAppend( vImagesAll, vImageOne );
            sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL;
        }
        Vec_IntFree( vCiMap );
        sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
    }
    Abc_PrintTime( "Time", Abc_Clock() - clk );


p->timeSatPref += Abc_Clock() - clk;

    Int2_ManStop( p );
    return RetValue;
}

sat_solver* Int2_ManPreparePrefix	(	Gia_Man_t *	p,
		int	f,
		Vec_Int_t **	pvCiMap
	)

Definition at line 99 of file int2Core.c.

{
    Gia_Man_t * pPref, * pNew;
    sat_solver * pSat;
    // create subset of the timeframe
    pPref = Int2_ManUnroll( p, f );
    // create SAT solver
    pNew = Jf_ManDeriveCnf( pPref, 0 );  
    pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL;
    Gia_ManStop( pPref );
    // derive the SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // collect indexes of CO variables
    *pvCiMap = Vec_IntAlloc( 100 );
    Gia_ManForEachPo( pNew, pObj, i )     
        Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
    // cleanup
    Cnf_DataFree( pCnf );
    Gia_ManStop( pNew );
    return pSat;
}

sat_solver* Int2_ManPrepareSuffix	(	Gia_Man_t *	p,
		Vec_Int_t *	vImageOne,
		Vec_Int_t *	vImagesAll,
		Vec_Int_t **	pvCoMap,
		Gia_Man_t **	ppSuff
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file int2Core.c.

{
    Gia_Man_t * pSuff, * pNew;
    Gia_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Vec_Int_t * vLits;
    int i, Lit, Limit;
    // create subset of the timeframe
    pSuff = Int2_ManProbToGia( p, vImageOne );
    assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) );
    // create SAT solver
    pNew = Jf_ManDeriveCnf( pSuff, 0 );  
    pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL;
    Gia_ManStop( pSuff );
    // derive the SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // create new constraints
    vLits = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 )
    {
        Vec_IntClear( vLits );
        for ( k = 0; k < Limit; k++ )
        {
            i++;
            Lit = Vec_IntEntry( vSop, i + k );
            Vec_IntPush( vLits, Abc_LitNot(Lit) );
        }
        if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) )  )  // UNSAT
        {
            Vec_IntFree( vLits );
            Cnf_DataFree( pCnf );
            Gia_ManStop( pNew );
            *pvCoMap = NULL;
            return NULL;
        }
    }
    Vec_IntFree( vLits );
    // collect indexes of CO variables
    *pvCoMap = Vec_IntAlloc( 100 );
    Gia_ManForEachRo( p, pObj, i )     
    {
        pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) );
        Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
    }
    // cleanup
    Cnf_DataFree( pCnf );
    if ( ppSuff )
        *ppSuff = pNew;
    else
        Gia_ManStop( pNew );
    return pSat;
}

ABC_NAMESPACE_IMPL_START void Int2_ManSetDefaultParams

(

Int2_ManPars_t *

p

)

DECLARATIONS ///.

MACRO DEFINITIONS ///.

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

FileName [int2Core.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file int2Core.c.

{ 
    memset( p, 0, sizeof(Int2_ManPars_t) );
    p->nBTLimit      =  0;     // limit on the number of conflicts
    p->nFramesS      =  1;     // the starting number timeframes
    p->nFramesMax    =  0;     // the max number timeframes to unroll
    p->nSecLimit     =  0;     // time limit in seconds
    p->nFramesK      =  1;     // the number of timeframes to use in induction
    p->fRewrite      =  0;     // use additional rewriting to simplify timeframes
    p->fTransLoop    =  0;     // add transition into the init state under new PI var
    p->fDropInvar    =  0;     // dump inductive invariant into file
    p->fVerbose      =  0;     // print verbose statistics
    p->iFrameMax     = -1;
}

Gia_Man_t* Int2_ManUnroll	(	Gia_Man_t *	p,
		int	nFrames
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file int2Core.c.

{
    Gia_Man_t * pFrames, * pTemp;
    Gia_Obj_t * pObj;
    int i, f;
    assert( Gia_ManRegNum(pAig) > 0 );
    pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
    pFrames->pName = Abc_UtilStrsav( pAig->pName );
    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
    Gia_ManHashAlloc( pFrames );
    Gia_ManConst0(pAig)->Value = 0;
    for ( f = 0; f < nFrames; f++ )
    {
        Gia_ManForEachRo( pAig, pObj, i )
            pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
        Gia_ManForEachPi( pAig, pObj, i )
            pObj->Value = Gia_ManAppendCi( pFrames );
        Gia_ManForEachAnd( pAig, pObj, i )
            pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        Gia_ManForEachRi( pAig, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
    }
    Gia_ManForEachRi( pAig, pObj, i )
        Gia_ManAppendCo( pFrames, pObj->Value );
    Gia_ManHashStop( pFrames );
    pFrames = Gia_ManCleanup( pTemp = pFrames );
    Gia_ManStop( pTemp );
    return pFrames;
}