summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmc.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-11-05 19:37:46 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2013-11-05 19:37:46 -0800
commit66b6593513bee13732999d4b2216d7a411003ce0 (patch)
tree264e477a1c33ed89305f65c893c56bc59d4da47d /src/sat/bmc/bmc.h
parente3560904ec9a9bd225237b113f75f18d7182c2a2 (diff)
downloadabc-66b6593513bee13732999d4b2216d7a411003ce0.tar.gz
abc-66b6593513bee13732999d4b2216d7a411003ce0.tar.bz2
abc-66b6593513bee13732999d4b2216d7a411003ce0.zip
Specialized inductive check.
Diffstat (limited to 'src/sat/bmc/bmc.h')
-rw-r--r--src/sat/bmc/bmc.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0cfc9b37..2f7af2ba 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -132,6 +132,7 @@ extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== bmcICheck.c ==========================================================*/
extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
+extern void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
/*=== 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 );