This graph shows which files directly or indirectly include this file:

Classes
struct	Pdr_Par_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_	Pdr_Par_t
	INCLUDES ///.

Functions
void	Pdr_ManSetDefaultParams (Pdr_Par_t *pPars)
	MACRO DEFINITIONS ///.

int	Pdr_ManSolve (Aig_Man_t p, Pdr_Par_t pPars)

Typedef Documentation

◆ Pdr_Par_t

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

◆ Pdr_ManSetDefaultParams()

void Pdr_ManSetDefaultParams ( Pdr_Par_t * pPars )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 50 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->nConfGenLimit  =       0;  // limit on SAT solver conflicts during generalization
    pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
    pPars->nRandomSeed   = 91648253;  // value to seed the SAT solver with
    pPars->fTwoRounds     =       0;  // use two rounds for generalization
    pPars->fMonoCnf       =       0;  // monolythic CNF
    pPars->fNewXSim       =       0;  // updated X-valued simulation
    pPars->fFlopPrio      =       0;  // use structural flop priorities
    pPars->fFlopOrder     =       0;  // order flops for 'analyze_final' during generalization
    pPars->fDumpInv       =       0;  // dump inductive invariant
    pPars->fUseSupp       =       1;  // using support variables in the invariant
    pPars->fShortest      =       0;  // forces bug traces to be shortest
    pPars->fUsePropOut    =       1;  // use property output
    pPars->fSkipDown      =       1;  // apply down in generalization
    pPars->fCtgs          =       0;  // handle CTGs in down
    pPars->fUseAbs        =       0;  // use abstraction 
    pPars->fUseSimpleRef  =       0;  // simplified CEX refinement
    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
    pPars->pInvFileName   =    NULL;  // invariant file name
    pPars->fBlocking      =       0;  // clause pushing with blocking
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Pdr_ManSolve()

int Pdr_ManSolve	(	Aig_Man_t *	pAig,
		Pdr_Par_t *	pPars )