diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-02-15 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-02-15 08:01:00 -0800 |
| commit | 0871bffae307e0553e0c5186336189e8b55cf6a6 (patch) | |
| tree | 4571d1563fe33a53a57fea1c35fb668b9d33265f /src/aig/cec/cec.h | |
| parent | f936cc0680c98ffe51b3a1716c996072d5dbf76c (diff) | |
| download | abc-0871bffae307e0553e0c5186336189e8b55cf6a6.tar.gz abc-0871bffae307e0553e0c5186336189e8b55cf6a6.tar.bz2 abc-0871bffae307e0553e0c5186336189e8b55cf6a6.zip | |
Version abc90215
Diffstat (limited to 'src/aig/cec/cec.h')
| -rw-r--r-- | src/aig/cec/cec.h | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index fb0bb830..fa7c5dbc 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -21,10 +21,6 @@ #ifndef __CEC_H__ #define __CEC_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +29,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -44,8 +44,8 @@ struct Cec_ParSat_t_ int nBTLimit; // conflict limit at a node int nSatVarMax; // the max number of SAT variables int nCallsRecycle; // calls to perform before recycling SAT solver + int fPolarFlip; // flops polarity of variables int fFirstStop; // stop on the first sat output - int fPolarFlip; // uses polarity adjustment int fVerbose; // verbose stats }; @@ -55,8 +55,15 @@ struct Cec_ParCsw_t_ { int nWords; // the number of simulation words int nRounds; // the number of simulation rounds - int nBTlimit; // conflict limit at a node + int nItersMax; // the maximum number of iterations of SAT sweeping + int nBTLimit; // conflict limit at a node + int nSatVarMax; // the max number of SAT variables + int nCallsRecycle; // calls to perform before recycling SAT solver + int nLevelMax; // restriction on the level nodes to be swept + int nDepthMax; // the depth in terms of steps of speculative reduction int fRewriting; // enables AIG rewriting + int fFirstStop; // stop on the first sat output + int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; @@ -86,7 +93,8 @@ struct Cec_ParCec_t_ extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ); extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); -extern int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p ); +extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ); +extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); #ifdef __cplusplus } |