diff options
Diffstat (limited to 'src/proof/pdr/pdr.h')
-rw-r--r-- | src/proof/pdr/pdr.h | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h new file mode 100644 index 00000000..4f0f769e --- /dev/null +++ b/src/proof/pdr/pdr.h @@ -0,0 +1,79 @@ +/**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 $] + +***********************************************************************/ + +#ifndef ABC__sat__pdr__pdr_h +#define ABC__sat__pdr__pdr_h + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Pdr_Par_t_ Pdr_Par_t; +struct Pdr_Par_t_ +{ + int iOutput; // zero-based number of primary output to solve + int nRecycle; // limit on vars for recycling + int nFrameMax; // limit on frame count + int nConfLimit; // limit on SAT solver conflicts + int nTimeOut; // timeout in seconds + int fTwoRounds; // use two rounds for generalization + int fMonoCnf; // monolythic CNF + int fDumpInv; // dump inductive invariant + int fShortest; // forces bug traces to be shortest + int fSkipGeneral; // skips expensive generalization step + int fVerbose; // verbose output + int fVeryVerbose; // very verbose output + int iFrame; // explored up to this frame +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== pdrCore.c ==========================================================*/ +extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); +extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); + + +ABC_NAMESPACE_HEADER_END + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |