diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 15:39:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 15:39:18 -0700 |
| commit | e9d0466494cbf7a707a450a7e058a0ae4c652f8b (patch) | |
| tree | 4433986c02f58247676c0fb032f98c848278eeab /src/sat/bmc/bmc.h | |
| parent | e651e227886452e088fd8c4b87f8cf48d189f7fb (diff) | |
| download | abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.tar.gz abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.tar.bz2 abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.zip | |
Updates for the new BMC engine.
Diffstat (limited to 'src/sat/bmc/bmc.h')
| -rw-r--r-- | src/sat/bmc/bmc.h | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index f1407936..51295a53 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -38,7 +38,10 @@ ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// - + +// unrolling manager +typedef struct Unr_Man_t_ Unr_Man_t; + typedef struct Saig_ParBmc_t_ Saig_ParBmc_t; struct Saig_ParBmc_t_ { @@ -69,14 +72,15 @@ struct Saig_ParBmc_t_ }; -typedef struct Bmc_LadPar_t_ Bmc_LadPar_t; -struct Bmc_LadPar_t_ +typedef struct Bmc_AndPar_t_ Bmc_AndPar_t; +struct Bmc_AndPar_t_ { int nStart; // starting timeframe int nFramesMax; // maximum number of timeframes int nConfLimit; // maximum number of conflicts at a node int fLoadCnf; // dynamic CNF loading int fVerbose; // verbose + int fVeryVerbose; // very verbose int fNotVerbose; // skip line-by-line print-out int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs @@ -98,11 +102,17 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra /*=== bmcBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); +/*=== bmcBmcAnd.c ==========================================================*/ +extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars ); /*=== bmcCexCut.c ==========================================================*/ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); +/*=== bmcUnroll.c ==========================================================*/ +extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose ); +extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f ); +extern void Unr_ManFree( Unr_Man_t * p ); ABC_NAMESPACE_HEADER_END |