diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-14 14:33:27 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-14 14:33:27 -0800 |
| commit | d8e04032967a524f4891927d73b1f61e60d8953b (patch) | |
| tree | dc09b9ff312d5811c18151a712a7e49a6311e7a7 /src/sat/bmc | |
| parent | ddab80aea4cea4bbdcd4aa17dd1be893e50961b1 (diff) | |
| download | abc-d8e04032967a524f4891927d73b1f61e60d8953b.tar.gz abc-d8e04032967a524f4891927d73b1f61e60d8953b.tar.bz2 abc-d8e04032967a524f4891927d73b1f61e60d8953b.zip | |
Added command 'cexsave' and 'cexload'.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmc.h | 10 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc.c | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc2.c | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcCexCut.c | 6 | ||||
| -rw-r--r-- | src/sat/bmc/bmcCexMin1.c | 1 |
6 files changed, 12 insertions, 8 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 633dc205..e1841bbc 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -27,6 +27,7 @@ //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" +#include "aig/gia/gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -66,13 +67,16 @@ struct Saig_ParBmc_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== saigBmc.c ==========================================================*/ +/*=== 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 ==========================================================*/ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); -/*=== saigBmc3.c ==========================================================*/ +/*=== bmcBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); -/*=== saigCexMin.c ==========================================================*/ +/*=== bmcCexCut.c ==========================================================*/ +extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +/*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c index 56bb7ca6..7a7c8940 100644 --- a/src/sat/bmc/bmcBmc.c +++ b/src/sat/bmc/bmcBmc.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "proof/fra/fra.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c index 778fe8e0..0f55f7ce 100644 --- a/src/sat/bmc/bmcBmc2.c +++ b/src/sat/bmc/bmcBmc2.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "proof/ssw/ssw.h" diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index a29be146..7ca5c7ba 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "proof/fra/fra.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index 3cc81d97..79944097 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [] + Synopsis [Generate GIA for target bad states.] Description [] @@ -42,6 +42,10 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd ) +{ + return NULL; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/bmc/bmcCexMin1.c b/src/sat/bmc/bmcCexMin1.c index 3b0a0274..23133ac0 100644 --- a/src/sat/bmc/bmcCexMin1.c +++ b/src/sat/bmc/bmcCexMin1.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "aig/ioa/ioa.h" #include "bmc.h" |