summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmc.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-02-11 11:58:25 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2014-02-11 11:58:25 -0800
commit0ff592524818c895517db80a0795b5faea6cf8b5 (patch)
treed399d23387ee38e0940128b9ee67da0d07598e68 /src/sat/bmc/bmc.h
parent367b02aecd32fe66729e3b8b75bba669ed828900 (diff)
downloadabc-0ff592524818c895517db80a0795b5faea6cf8b5.tar.gz
abc-0ff592524818c895517db80a0795b5faea6cf8b5.tar.bz2
abc-0ff592524818c895517db80a0795b5faea6cf8b5.zip
Experiments with inductive don't-cares.
Diffstat (limited to 'src/sat/bmc/bmc.h')
-rw-r--r--src/sat/bmc/bmc.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 2f7af2ba..b3e2d8e8 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -132,7 +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 );
+extern Vec_Int_t * 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 );