int2.h File Reference

Go to the source code of this file.

Data Structures
struct	Int2_ManPars_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Int2_ManPars_t_	Int2_ManPars_t
	INCLUDES ///. More...

Functions
void	Int2_ManSetDefaultParams (Int2_ManPars_t *p)
	MACRO DEFINITIONS ///. More...
int	Int2_ManPerformInterpolation (Gia_Man_t *p, Int2_ManPars_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Int2_ManPars_t_ Int2_ManPars_t

INCLUDES ///.

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

FileName [int2.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 50 of file int2.h.

Function Documentation

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;
}

void Int2_ManSetDefaultParams

(

Int2_ManPars_t *

p

)

MACRO DEFINITIONS ///.

FUNCTION 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;
}