Isolating BMC code into a separate package.

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 \

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

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
 

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 \

src/aig/saig/module.make

-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 \

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 ==========================================================*/

src/aig/saig/saigTempor.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "saig.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 

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>

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
 

src/proof/abs/absIter.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abs.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 

src/proof/abs/absOldCex.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abs.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 

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
 

src/proof/int/intCore.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "intInt.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 

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
 

src/sat/bmc/bmc.c

+/**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
+

src/sat/bmc/bmc.h

+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+

src/aig/saig/saigBmc.c → src/sat/bmc/bmcBmc.c

 /**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
 

src/aig/saig/saigBmc2.c → src/sat/bmc/bmcBmc2.c

 /**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
 

src/aig/saig/saigBmc3.c → src/sat/bmc/bmcBmc3.c

 /**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
 

src/sat/bmc/bmcCexCut.c

+/**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
+

src/aig/saig/saigCexMin.c → src/sat/bmc/bmcCexMin1.c

 /**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
 

src/aig/gia/giaCexMin.c → src/sat/bmc/bmcCexMin2.c

 /**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
 

src/sat/bmc/module.make

+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