diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 13:32:18 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 13:32:18 -0800 |
commit | 624af674a0e7f1a675917afaaf371db6a5588821 (patch) | |
tree | c08e1438c9033da80c85b61585292ba4e95cb244 /src/sat/pdr/pdr.h | |
parent | ab80b015a4efdf196334aafc19d589d48778f0bb (diff) | |
download | abc-624af674a0e7f1a675917afaaf371db6a5588821.tar.gz abc-624af674a0e7f1a675917afaaf371db6a5588821.tar.bz2 abc-624af674a0e7f1a675917afaaf371db6a5588821.zip |
New code since Dec 2010.
Diffstat (limited to 'src/sat/pdr/pdr.h')
-rw-r--r-- | src/sat/pdr/pdr.h | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h new file mode 100644 index 00000000..1099c621 --- /dev/null +++ b/src/sat/pdr/pdr.h @@ -0,0 +1,77 @@ +/**CFile**************************************************************** + + FileName [pdr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + 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 __PDR_H__ +#define __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 fVerbose; // verbose output + int fVeryVerbose; // very verbose output +}; + +//////////////////////////////////////////////////////////////////////// +/// 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 /// +//////////////////////////////////////////////////////////////////////// + |