Isolating BMC code into a separate package.

21 files changed, 234 insertions, 54 deletions

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