Updates for the new BMC engine.

10 files changed, 187 insertions, 26 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 59622d93..35429ccd 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1419,6 +1419,10 @@ SOURCE=.\src\sat\bmc\bmcBmc3.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcBmcAnd.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcCexCut.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 7653dc62..2d3cf518 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1018,6 +1018,7 @@ extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP
 extern Gia_Man_t *         Gia_ManStart( int nObjsMax ); 
 extern void                Gia_ManStop( Gia_Man_t * p );  
 extern void                Gia_ManStopP( Gia_Man_t ** p );  
+extern float               Gia_ManMemory( Gia_Man_t * p );
 extern void                Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut ); 
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2e911ba8..e8e186cf 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -907,7 +907,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i, nRos = 0, nRis = 0;
     int CountMarked = 0;
-    Gia_ManForEachObj1( p, pObj, i )
+    Gia_ManForEachObj( p, pObj, i )
         CountMarked += pObj->fMark0;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) - CountMarked );
@@ -945,6 +945,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
             nRis += Gia_ObjIsRi(p, pObj);
         }
     }
+    assert( pNew->nObjsAlloc == pNew->nObjs );
     assert( nRos == nRis );
     Gia_ManSetRegNum( pNew, nRos );
     if ( p->pReprs && p->pNexts )
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index a573e9e7..58057136 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -129,6 +129,27 @@ void Gia_ManStop( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns memory used in megabytes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_ManMemory( Gia_Man_t * p )
+{
+    word Memory = sizeof(Gia_Man_t);
+    Memory += sizeof(Gia_Obj_t) * Gia_ManObjNum(p);
+    Memory += sizeof(int) * Gia_ManCiNum(p);
+    Memory += sizeof(int) * Gia_ManCoNum(p);
+    Memory += sizeof(int) * p->nHTable * (p->pHTable != NULL);
+    return (float)(int)(Memory / (1 << 20)) + (float)(1e-6 * (int)(Memory % (1 << 20)));
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4c986d9c..da3726f3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31611,21 +31611,22 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars );
+//    extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars );
     int c;
-    Bmc_LadPar_t Pars, * pPars = &Pars;
-    memset( pPars, 0, sizeof(Bmc_LadPar_t) );
+    Bmc_AndPar_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Bmc_AndPar_t) );
     pPars->nStart        =    0;  // starting timeframe
     pPars->nFramesMax    =    0;  // maximum number of timeframes 
     pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
     pPars->fLoadCnf      =    0;  // dynamic CNF loading
     pPars->fVerbose      =    0;  // verbose 
+    pPars->fVeryVerbose  =    0;  // very verbose 
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
     pPars->iFrame        =    0;  // explored up to this frame
     pPars->nFailOuts     =    0;  // the number of failed outputs
     pPars->nDropOuts     =    0;  // the number of dropped outputs
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31657,6 +31658,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             pPars->fVerbose ^= 1;
             break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -31668,16 +31672,18 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" );
         return 0;
     }
-    Bmc_PerformBmc( pAbc->pGia, pPars );
+//    Bmc_PerformBmc( pAbc->pGia, pPars );
+    Gia_ManBmcPerform( pAbc->pGia, pPars );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SF num] [-cvh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SF num] [-cvwh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking\n" );
     Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n",              pPars->nStart );
     Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n",    pPars->nFramesMax );
     Abc_Print( -2, "\t-c     : toggle dynamic CNF loading [default = %s]\n",          pPars->fLoadCnf? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index f1407936..51295a53 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -38,7 +38,10 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
+// unrolling manager 
+typedef struct Unr_Man_t_ Unr_Man_t;
+
 typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
 struct Saig_ParBmc_t_
 {
@@ -69,14 +72,15 @@ struct Saig_ParBmc_t_
 };
 
  
-typedef struct Bmc_LadPar_t_ Bmc_LadPar_t;
-struct Bmc_LadPar_t_
+typedef struct Bmc_AndPar_t_ Bmc_AndPar_t;
+struct Bmc_AndPar_t_
 {
     int         nStart;         // starting timeframe
     int         nFramesMax;     // maximum number of timeframes 
     int         nConfLimit;     // maximum number of conflicts at a node
     int         fLoadCnf;       // dynamic CNF loading
     int         fVerbose;       // verbose 
+    int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
@@ -98,11 +102,17 @@ extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
 /*=== bmcBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
+/*=== bmcBmcAnd.c ==========================================================*/
+extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
+/*=== 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 );
+extern void              Unr_ManFree( Unr_Man_t * p );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
new file mode 100644
index 00000000..d3544f6d
--- /dev/null
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBmcAnd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Memory-efficient BMC engine]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcBmcAnd.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     []
+
+***********************************************************************/
+int Gia_ManCountUnmarked_rec( Gia_Obj_t * pObj )
+{
+    if ( !Gia_ObjIsAnd(pObj) || pObj->fMark0 )
+        return 0;
+    pObj->fMark0 = 1;
+    return 1 + Gia_ManCountUnmarked_rec( Gia_ObjFanin0(pObj) ) + 
+        Gia_ManCountUnmarked_rec( Gia_ObjFanin1(pObj) );
+}
+int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
+{
+    int i, Counter = 0;
+    for ( i = iStart; i < Gia_ManPoNum(p); i++ )
+        Counter += Gia_ManCountUnmarked_rec( Gia_ObjFanin0(Gia_ManPo(p, i)) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+{
+    Unr_Man_t * p;
+    Gia_Man_t * pFrames;
+    abctime clk = Abc_Clock();
+    int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
+    int i, f, iStart, status = -1, Counter = 0;
+    p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        pFrames = Unr_ManUnrollFrame( p, f );
+        assert( Gia_ManPoNum(pFrames) == (f + 1) * Gia_ManPoNum(pGia) );
+        iStart = f * Gia_ManPoNum(pGia);
+        for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
+            if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
+                break;
+        if ( i == Gia_ManPoNum(pFrames) )
+        {
+            if ( pPars->fVerbose )
+            {
+                printf( "Frame %4d :  Trivally UNSAT.   Memory = %5.1f Mb   ", f, Gia_ManMemory(pFrames) );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
+            continue;
+        }
+        if ( pPars->fVerbose )
+        {
+            printf( "Frame %4d :  AIG =%9d.   Memory = %5.1f Mb   ", f, Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
+        if ( ++Counter == 10 )
+            break;
+    }
+    Unr_ManFree( p );
+    return status;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmcLoad.c b/src/sat/bmc/bmcLoad.c
index b3d56005..a653861c 100644
--- a/src/sat/bmc/bmcLoad.c
+++ b/src/sat/bmc/bmcLoad.c
@@ -31,7 +31,7 @@ ABC_NAMESPACE_IMPL_START
 typedef struct Bmc_Lad_t_ Bmc_Lad_t;  
 struct Bmc_Lad_t_
 {
-    Bmc_LadPar_t *   pPars;     // parameters
+    Bmc_AndPar_t *   pPars;     // parameters
     Gia_Man_t *      pGia;      // unrolled AIG
     sat_solver *     pSat;      // SAT solvers
     Vec_Int_t *      vSat2Id;   // maps SAT var into its node
@@ -123,7 +123,7 @@ int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_LadPar_t * pPars )
+Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
     Bmc_Lad_t * p;
     int Lit;
@@ -164,7 +164,7 @@ void Bmc_LadStop( Bmc_Lad_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars )
+void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
     int nConfLimit = 0;
     Bmc_Lad_t * p;
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index c05eb66b..9cabcd8b 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -45,7 +45,6 @@ struct Unr_Obj_t_
     unsigned              Res[1];       // RankMax entries
 };
 
-typedef struct Unr_Man_t_ Unr_Man_t;
 struct Unr_Man_t_
 {
     // input data
@@ -366,14 +365,18 @@ void Unr_ManFree( Unr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Unr_ManUnrollStart( Unr_Man_t * p )
+Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose )
 {
     int i, iHandle;
+    Unr_Man_t * p;
+    p = Unr_ManAlloc( pGia );
+    Unr_ManSetup( p, fVerbose );
     for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ )
         if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 )
             Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 );
+    return p;
 }
-void Unr_ManUnrollFrame( Unr_Man_t * p, int f )
+Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f )
 {
     int i, iLit, iLit0, iLit1, hStart;
     for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
@@ -405,14 +408,19 @@ void Unr_ManUnrollFrame( Unr_Man_t * p, int f )
         hStart += Unr_ObjSize( pUnrObj );
     }
     assert( p->pObjs + hStart == p->pEnd );
+    return p->pFrames;
 }
-Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames )
+Gia_Man_t * Unr_ManUnroll( Gia_Man_t * pGia, int nFrames )
 {
+    Unr_Man_t * p;
+    Gia_Man_t * pFrames;
     int f;
-    Unr_ManUnrollStart( p );
+    p = Unr_ManUnrollStart( pGia, 1 );
     for ( f = 0; f < nFrames; f++ )
         Unr_ManUnrollFrame( p, f );
-    return Gia_ManCleanup( p->pFrames );
+    pFrames = Gia_ManCleanup( p->pFrames );
+    Unr_ManFree( p );
+    return pFrames;
 }
 
 /**Function*************************************************************
@@ -472,14 +480,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
 {
     Gia_Man_t * pFrames0, * pFrames1;
     abctime clk = Abc_Clock();
-    Unr_Man_t * p;
-    p = Unr_ManAlloc( pGia );
-    Unr_ManSetup( p, 1 );
-    pFrames0 = Unr_ManUnroll( p, nFrames );
+    pFrames0 = Unr_ManUnroll( pGia, nFrames );
     Abc_PrintTime( 1, "Unroll ", Abc_Clock() - clk );
-
-    Unr_ManFree( p );
-
     clk = Abc_Clock();
     pFrames1 = Unr_ManUnrollSimple( pGia, nFrames );
     Abc_PrintTime( 1, "UnrollS", Abc_Clock() - clk );
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index cde439b4..e567e92b 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc2.c \
     src/sat/bmc/bmcBmc3.c \
+    src/sat/bmc/bmcBmcAnd.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \