diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
| commit | 42927d5ebb7b7a828790394dc555cd129aa2481b (patch) | |
| tree | e608e44763ffb52169a8e7d19021643fb8a27bdc /src/sat/bmc/bmc.h | |
| parent | af6705a8b1c75d069ef1fc504080b7bc6ee1c8f5 (diff) | |
| download | abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.gz abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.bz2 abc-42927d5ebb7b7a828790394dc555cd129aa2481b.zip | |
Adding command to dump UNSAT core of BMC instance.
Diffstat (limited to 'src/sat/bmc/bmc.h')
| -rw-r--r-- | src/sat/bmc/bmc.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3eeeb7b5..558b2d62 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -94,7 +94,18 @@ struct Bmc_AndPar_t_ int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs }; - + +typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t; +struct Bmc_BCorePar_t_ +{ + int iFrame; // timeframe + int iOutput; // property output + int nTimeOut; // timeout in seconds + char * pFilePivots; // file name with AIG IDs of pivot objects + char * pFileProof; // file name to write the resulting proof + int fVerbose; // verbose output +}; + typedef struct Bmc_MulPar_t_ Bmc_MulPar_t; struct Bmc_MulPar_t_ { @@ -117,6 +128,8 @@ struct Bmc_MulPar_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== bmcBCore.c ==========================================================*/ +extern void Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars ); /*=== bmcBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); /*=== bmcBmc2.c ==========================================================*/ |