summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-11-14 13:55:24 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-11-14 13:55:24 -0800
commitbe7a4e4259ca68c9ab3238c6fdd5a69728e98436 (patch)
treee96fdbe2387a0a2a79b32f95f1a533dc4ad3a2e7
parentaba8ff4ba06c35706b37ecb30d6d358d7c941a7d (diff)
downloadabc-be7a4e4259ca68c9ab3238c6fdd5a69728e98436.tar.gz
abc-be7a4e4259ca68c9ab3238c6fdd5a69728e98436.tar.bz2
abc-be7a4e4259ca68c9ab3238c6fdd5a69728e98436.zip
Isolating BMC code into a separate package.
-rw-r--r--Makefile2
-rw-r--r--abclib.dsp56
-rw-r--r--src/aig/gia/giaEquiv.c1
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/aig/saig/module.make6
-rw-r--r--src/aig/saig/saig.h28
-rw-r--r--src/aig/saig/saigTempor.c1
-rw-r--r--src/base/abci/abc.c1
-rw-r--r--src/base/abci/abcDar.c1
-rw-r--r--src/proof/abs/absIter.c1
-rw-r--r--src/proof/abs/absOldCex.c1
-rw-r--r--src/proof/abs/absOldRef.c1
-rw-r--r--src/proof/int/intCore.c1
-rw-r--r--src/proof/ssw/sswRarity.c1
-rw-r--r--src/sat/bmc/bmc.c52
-rw-r--r--src/sat/bmc/bmc.h88
-rw-r--r--src/sat/bmc/bmcBmc.c (renamed from src/aig/saig/saigBmc.c)9
-rw-r--r--src/sat/bmc/bmcBmc2.c (renamed from src/aig/saig/saigBmc2.c)9
-rw-r--r--src/sat/bmc/bmcBmc3.c (renamed from src/aig/saig/saigBmc3.c)9
-rw-r--r--src/sat/bmc/bmcCexCut.c52
-rw-r--r--src/sat/bmc/bmcCexMin1.c (renamed from src/aig/saig/saigCexMin.c)9
-rw-r--r--src/sat/bmc/bmcCexMin2.c (renamed from src/aig/gia/giaCexMin.c)9
-rw-r--r--src/sat/bmc/module.make7
23 files changed, 271 insertions, 75 deletions
diff --git a/Makefile b/Makefile
index e3ebbd8b..ef38f86f 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@ MODULES := \
src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau \
- src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf \
+ src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
diff --git a/abclib.dsp b/abclib.dsp
index 08c2e356..e9638841 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1378,6 +1378,42 @@ SOURCE=.\src\sat\cnf\cnfUtil.c
SOURCE=.\src\sat\cnf\cnfWrite.c
# End Source File
# End Group
+# Begin Group "bmc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcBmc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcBmc2.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcBmc3.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcCexCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcCexMin1.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcCexMin2.c
+# End Source File
+# End Group
# End Group
# Begin Group "opt"
@@ -3315,22 +3351,6 @@ SOURCE=.\src\aig\saig\saig.h
# End Source File
# Begin Source File
-SOURCE=.\src\aig\saig\saigBmc.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\saig\saigBmc2.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\saig\saigBmc3.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\saig\saigCexMin.c
-# End Source File
-# Begin Source File
-
SOURCE=.\src\aig\saig\saigCone.c
# End Source File
# Begin Source File
@@ -3471,10 +3491,6 @@ SOURCE=.\src\aig\gia\giaCex.c
# End Source File
# Begin Source File
-SOURCE=.\src\aig\gia\giaCexMin.c
-# End Source File
-# Begin Source File
-
SOURCE=.\src\aig\gia\giaChoice.c
# End Source File
# Begin Source File
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index fc13f87c..d8545cd5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -20,6 +20,7 @@
#include "gia.h"
#include "proof/cec/cec.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index fcff9a9f..49644fa8 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -4,7 +4,6 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaBidec.c \
src/aig/gia/giaCCof.c \
src/aig/gia/giaCex.c \
- src/aig/gia/giaCexMin.c \
src/aig/gia/giaChoice.c \
src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index a3231929..97b69363 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,4 @@
-SRC += src/aig/saig/saigBmc.c \
- src/aig/saig/saigBmc2.c \
- src/aig/saig/saigBmc3.c \
- src/aig/saig/saigCexMin.c \
- src/aig/saig/saigCone.c \
+SRC += src/aig/saig/saigCone. \
src/aig/saig/saigConstr.c \
src/aig/saig/saigConstr2.c \
src/aig/saig/saigDual.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 8823dcac..836a2051 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -50,26 +50,6 @@ struct Sec_MtrStatus_t_
int iOut; // the satisfied output
};
-typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
-struct Saig_ParBmc_t_
-{
- int nStart; // starting timeframe
- int nFramesMax; // maximum number of timeframes
- int nConfLimit; // maximum number of conflicts at a node
- int nConfLimitJump; // maximum number of conflicts after jumping
- int nFramesJump; // the number of tiemframes to jump
- int nTimeOut; // approximate timeout in seconds
- int nPisAbstract; // the number of PIs to abstract
- int fSolveAll; // does not stop at the first SAT output
- int fDropSatOuts; // replace sat outputs by constant 0
- int nFfToAddMax; // max number of flops to add during CBA
- int fSkipRand; // skip random decisions
- int fVerbose; // verbose
- int iFrame; // explored up to this frame
- int nFailOuts; // the number of failed outputs
-};
-
-
typedef struct Saig_ParBbr_t_ Saig_ParBbr_t;
struct Saig_ParBbr_t_
{
@@ -126,14 +106,6 @@ static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) {
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== saigBmc.c ==========================================================*/
-extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-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 ==========================================================*/
-extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
-extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
-/*=== saigCexMin.c ==========================================================*/
-extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigConstr.c ==========================================================*/
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 040df1f9..4e884140 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "saig.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3fa1a8f7..028dddcc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -50,6 +50,7 @@
#include "map/cov/cov.h"
#include "base/cmd/cmd.h"
#include "proof/abs/abs.h"
+#include "sat/bmc/bmc.h"
#ifndef _WIN32
#include <unistd.h>
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 83da1c60..cc703490 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -34,6 +34,7 @@
#include "proof/cec/cec.h"
#include "opt/csw/csw.h"
#include "proof/pdr/pdr.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/abs/absIter.c b/src/proof/abs/absIter.c
index 88cbe39d..e8e5730b 100644
--- a/src/proof/abs/absIter.c
+++ b/src/proof/abs/absIter.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abs.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/abs/absOldCex.c b/src/proof/abs/absOldCex.c
index fec6d152..e5eaee27 100644
--- a/src/proof/abs/absOldCex.c
+++ b/src/proof/abs/absOldCex.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abs.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c
index dee28cad..eb9b84fa 100644
--- a/src/proof/abs/absOldRef.c
+++ b/src/proof/abs/absOldRef.c
@@ -23,6 +23,7 @@
#include "proof/fra/fra.h"
#include "proof/bbr/bbr.h"
#include "proof/pdr/pdr.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index f563eea2..69ca5044 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "intInt.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 8df54822..2abd9682 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -21,6 +21,7 @@
#include "sswInt.h"
#include "aig/gia/giaAig.h"
#include "base/main/main.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/sat/bmc/bmc.c b/src/sat/bmc/bmc.c
new file mode 100644
index 00000000..2dde80ab
--- /dev/null
+++ b/src/sat/bmc/bmc.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+ FileName [bmc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based bounded model checking.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
new file mode 100644
index 00000000..633dc205
--- /dev/null
+++ b/src/sat/bmc/bmc.h
@@ -0,0 +1,88 @@
+/**CFile****************************************************************
+
+ FileName [bmc.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based bounded model checking.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC___sat_bmc_BMC_h
+#define ABC___sat_bmc_BMC_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/saig/saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
+struct Saig_ParBmc_t_
+{
+ int nStart; // starting timeframe
+ int nFramesMax; // maximum number of timeframes
+ int nConfLimit; // maximum number of conflicts at a node
+ int nConfLimitJump; // maximum number of conflicts after jumping
+ int nFramesJump; // the number of tiemframes to jump
+ int nTimeOut; // approximate timeout in seconds
+ int nPisAbstract; // the number of PIs to abstract
+ int fSolveAll; // does not stop at the first SAT output
+ int fDropSatOuts; // replace sat outputs by constant 0
+ int nFfToAddMax; // max number of flops to add during CBA
+ int fSkipRand; // skip random decisions
+ int fVerbose; // verbose
+ int iFrame; // explored up to this frame
+ int nFailOuts; // the number of failed outputs
+};
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== saigBmc.c ==========================================================*/
+extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
+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 ==========================================================*/
+extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
+extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
+/*=== saigCexMin.c ==========================================================*/
+extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/saig/saigBmc.c b/src/sat/bmc/bmcBmc.c
index f88d3162..56bb7ca6 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/sat/bmc/bmcBmc.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [saigBmc.c]
+ FileName [bmcBmc.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Sequential AIG package.]
+ PackageName [SAT-based bounded model checking.]
Synopsis [Simple BMC package.]
@@ -14,14 +14,15 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: bmcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "saig.h"
+#include "aig/saig/saig.h"
#include "proof/fra/fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
+#include "bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/aig/saig/saigBmc2.c b/src/sat/bmc/bmcBmc2.c
index 7d4bfdd2..778fe8e0 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/sat/bmc/bmcBmc2.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [saigBmc.c]
+ FileName [bmcBmc2.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Sequential AIG package.]
+ PackageName [SAT-based bounded model checking.]
Synopsis [Simple BMC package.]
@@ -14,14 +14,15 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: bmcBmc2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "saig.h"
+#include "aig/saig/saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "proof/ssw/ssw.h"
+#include "bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/aig/saig/saigBmc3.c b/src/sat/bmc/bmcBmc3.c
index c8ed7e5a..a29be146 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [saigBmc3.c]
+ FileName [bmcBmc3.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Sequential AIG package.]
+ PackageName [SAT-based bounded model checking.]
Synopsis [Simple BMC package.]
@@ -14,14 +14,15 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: saigBmc3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: bmcBmc3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "saig.h"
+#include "aig/saig/saig.h"
#include "proof/fra/fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
+#include "bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
new file mode 100644
index 00000000..3cc81d97
--- /dev/null
+++ b/src/sat/bmc/bmcCexCut.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+ FileName [bmcCexCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based bounded model checking.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bmcCexCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigCexMin.c b/src/sat/bmc/bmcCexMin1.c
index f0fca2c4..3b0a0274 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/sat/bmc/bmcCexMin1.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [saigCexMin.c]
+ FileName [bmcCexMin1.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Sequential AIG package.]
+ PackageName [SAT-based bounded model checking.]
Synopsis [CEX minimization.]
@@ -14,12 +14,13 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: saigCexMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: bmcCexMin1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "saig.h"
+#include "aig/saig/saig.h"
#include "aig/ioa/ioa.h"
+#include "bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/aig/gia/giaCexMin.c b/src/sat/bmc/bmcCexMin2.c
index 3249e4cb..076d744c 100644
--- a/src/aig/gia/giaCexMin.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [giaCexMin.c]
+ FileName [bmcCexMin2.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Scalable AIG package.]
+ PackageName [SAT-based bounded model checking.]
Synopsis [CEX minimization.]
@@ -14,11 +14,12 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: giaCexMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: bmcCexMin2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "gia.h"
+#include "aig/gia/gia.h"
+#include "bmc.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
new file mode 100644
index 00000000..071834d8
--- /dev/null
+++ b/src/sat/bmc/module.make
@@ -0,0 +1,7 @@
+SRC += src/sat/bmc/bmc.c \
+ src/sat/bmc/bmcBmc.c \
+ src/sat/bmc/bmcBmc2.c \
+ src/sat/bmc/bmcBmc3.c \
+ src/sat/bmc/bmcCexCut.c \
+ src/sat/bmc/bmcCexMin1.c \
+ src/sat/bmc/bmcCexMin2.c