pdr.h File Reference

Go to the source code of this file.

Data Structures
struct	Pdr_Par_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_	Pdr_Par_t
	INCLUDES ///. More...

Functions
void	Pdr_ManSetDefaultParams (Pdr_Par_t *pPars)
	MACRO DEFINITIONS ///. More...
int	Pdr_ManSolve (Aig_Man_t *p, Pdr_Par_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_ Pdr_Par_t

INCLUDES ///.

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

FileName [pdr.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:

pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 40 of file pdr.h.

Function Documentation

void Pdr_ManSetDefaultParams

(

Pdr_Par_t *

pPars

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

Synopsis [Returns 1 if the state could be blocked.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file pdrCore.c.

{
    memset( pPars, 0, sizeof(Pdr_Par_t) );
//    pPars->iOutput        =      -1;  // zero-based output number
    pPars->nRecycle       =     300;  // limit on vars for recycling
    pPars->nFrameMax      =   10000;  // limit on number of timeframes
    pPars->nTimeOut       =       0;  // timeout in seconds
    pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
    pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
    pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
    pPars->fTwoRounds     =       0;  // use two rounds for generalization
    pPars->fMonoCnf       =       0;  // monolythic CNF
    pPars->fDumpInv       =       0;  // dump inductive invariant
    pPars->fShortest      =       0;  // forces bug traces to be shortest
    pPars->fVerbose       =       0;  // verbose output
    pPars->fVeryVerbose   =       0;  // very verbose output
    pPars->fNotVerbose    =       0;  // not printing line-by-line progress
    pPars->iFrame         =      -1;  // explored up to this frame
    pPars->nFailOuts      =       0;  // the number of disproved outputs
    pPars->nDropOuts      =       0;  // the number of timed out outputs
    pPars->timeLastSolved =       0;  // last one solved
}

int Pdr_ManSolve	(	Aig_Man_t *	pAig,
		Pdr_Par_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 886 of file pdrCore.c.

{
    Pdr_Man_t * p;
    int k, RetValue;
    abctime clk = Abc_Clock();
    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
        pPars->nTimeOutOne = 0;
    if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
        pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
    if ( pPars->fVerbose )
    {
//    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
            pPars->nRecycle,
            pPars->nFrameMax,
            pPars->nRestLimit,
            pPars->nTimeOut );
        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
            pPars->fMonoCnf ?     "yes" : "no",
            pPars->fSkipGeneral ? "yes" : "no",
            pPars->fSolveAll ?    "yes" : "no" );
    }
    ABC_FREE( pAig->pSeqModel );
    p = Pdr_ManStart( pAig, pPars, NULL );
    RetValue = Pdr_ManSolveInt( p );
    if ( RetValue == 0 )
        assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
    if ( p->vCexes )
    {
        assert( p->pAig->vSeqModelVec == NULL );
        p->pAig->vSeqModelVec = p->vCexes;
        p->vCexes = NULL;
    }
    if ( p->pPars->fDumpInv )
        Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
    p->tTotal += Abc_Clock() - clk;
    Pdr_ManStop( p );
    pPars->iFrame--;
    // convert all -2 (unknown) entries into -1 (undec)
    if ( pPars->vOutMap )
        for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
            if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
                Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
    if ( pPars->fUseBridge )
        Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
    return RetValue;
}