Updates for the new BMC engine.

src/sat/bmc/bmcBmcAnd.c

@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "bmc.h"
+#include "sat/bsat/satStore.h"
+#include "sat/cnf/cnf.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,6 +29,19 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Bmc_Mna_t_ Bmc_Mna_t; 
+struct Bmc_Mna_t_
+{
+    Gia_Man_t *         pFrames;  // time frames
+    Vec_Int_t *         vId2Var;  // maps GIA IDs into SAT vars
+    Vec_Int_t *         vInputs;  // inputs of the cone
+    Vec_Int_t *         vOutputs; // outputs of the cone
+    Vec_Int_t *         vNodes;   // internal nodes of the cone
+    sat_solver *        pSat;     // SAT solver
+    int                 nSatVars; // the counter of SAT variables
+    abctime             clkStart; // starting time
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,20 +57,111 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManCountUnmarked_rec( Gia_Obj_t * pObj )
+Bmc_Mna_t * Bmc_MnaAlloc()
+{
+    Bmc_Mna_t * p;
+    p = ABC_CALLOC( Bmc_Mna_t, 1 );
+    p->vId2Var   = Vec_IntAlloc( 0 );
+    p->vInputs   = Vec_IntAlloc( 1000 );
+    p->vOutputs  = Vec_IntAlloc( 1000 );
+    p->vNodes    = Vec_IntAlloc( 10000 );
+    p->pSat      = sat_solver_new();
+    p->nSatVars  = 1;
+    p->clkStart  = Abc_Clock();
+    return p;
+}
+void Bmc_MnaFree( Bmc_Mna_t * p )
+{
+    Vec_IntFreeP( &p->vId2Var );
+    Vec_IntFreeP( &p->vInputs );
+    Vec_IntFreeP( &p->vOutputs );
+    Vec_IntFreeP( &p->vNodes );
+    sat_solver_delete( p->pSat );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if all outputs are trivial.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart )
 {
-    if ( !Gia_ObjIsAnd(pObj) || pObj->fMark0 )
+    int i;
+    for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
+        if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
             return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects new nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManBmcAndCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
+{
+    int iObj;
+    if ( pObj->fMark0 )
+        return;
     pObj->fMark0 = 1;
-    return 1 + Gia_ManCountUnmarked_rec( Gia_ObjFanin0(pObj) ) + 
-        Gia_ManCountUnmarked_rec( Gia_ObjFanin1(pObj) );
+    iObj = Gia_ObjId( p->pFrames, pObj );
+    if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(p->vId2Var, iObj) == 0 )
+    {
+        Gia_ManBmcAndCone_rec( p, Gia_ObjFanin0(pObj) );
+        Gia_ManBmcAndCone_rec( p, Gia_ObjFanin1(pObj) );
+        Vec_IntPush( p->vNodes, iObj );
+    }
+    else
+        Vec_IntPush( p->vInputs, iObj );
 }
-int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
+void Gia_ManBmcAndCone( Bmc_Mna_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;
+    Gia_Obj_t * pObj;
+    int i;
+    Vec_IntClear( p->vNodes );
+    Vec_IntClear( p->vInputs );
+    Vec_IntClear( p->vOutputs );
+    Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
+    for ( i = iStart; i < Gia_ManPoNum(p->pFrames); i++ )
+    {
+        pObj = Gia_ManPo(p->pFrames, i);
+        if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
+            continue;
+        Gia_ManBmcAndCone_rec( p, Gia_ObjFanin0(pObj) );
+        Vec_IntPush( p->vOutputs, Gia_ObjId(p->pFrames, pObj) );
+    }
+    // clean attributes and create new variables
+    Gia_ManForEachObjVec( p->vInputs, p->pFrames, pObj, i )
+    {
+        int iObj = Vec_IntEntry(p->vInputs, i);
+        pObj->fMark0 = 0;
+        if ( Vec_IntEntry( p->vId2Var, iObj ) == 0 )
+            Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
+    }
+    Gia_ManForEachObjVec( p->vNodes, p->pFrames, pObj, i )
+    {
+        int iObj = Vec_IntEntry(p->vNodes, i);
+        pObj->fMark0 = 0;
+        assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
+        Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
+    }
+    // extend the SAT solver
+    if ( p->nSatVars > sat_solver_nvars(p->pSat) )
+        sat_solver_setnvars( p->pSat, p->nSatVars );
+
 }
 
 /**Function*************************************************************
@@ -71,46 +177,44 @@ int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
 ***********************************************************************/
 int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
-    Unr_Man_t * p;
-    Gia_Man_t * pFrames;
-    abctime clk = Abc_Clock();
+    Unr_Man_t * pUnroll;
+    Bmc_Mna_t * p = Bmc_MnaAlloc();
     int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
-    int i, f, iStart, status = -1;//, Counter = 0;
-    p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
+    int f, iStart, status = -1;
+    pUnroll = 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) );
+        p->pFrames = Unr_ManUnrollFrame( pUnroll, f );
         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 ( Gia_ManBmcCheckOutputs(p->pFrames, iStart) )
         {
             if ( pPars->fVerbose )
             {
-                printf( "Frame %4d :  PI =%9d.  AIG =%9d.  Trivally UNSAT.   Mem =%7.1f Mb   ", 
-                    f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) );
-                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+                printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  Trivially UNSAT.               Mem =%7.1f Mb   ", 
+                    f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), 
+                    p->nSatVars-1, Gia_ManMemory(p->pFrames) );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
             }
             continue;
         }
+        // create another slice
+        Gia_ManBmcAndCone(p, iStart);
         if ( pPars->fVerbose )
         {
-            printf( "Frame %4d :  PI =%9d.  AIG =%9d.  And =%9d.   Mem =%7.1f Mb   ", 
-                f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
-            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  In =%6d.  And =%9d.   Mem =%7.1f Mb   ", 
+                f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), 
+                p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), Gia_ManMemory(p->pFrames) );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
         }
-//        if ( ++Counter == 10 )
-//            break;
     }
     // dump unfolded frames
-    pFrames = Gia_ManCleanup( pFrames );
-    Gia_AigerWrite( pFrames, "frames.aig", 0, 0 );
+    p->pFrames = Gia_ManCleanup( p->pFrames );
+    Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
     printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
-    Gia_ManStop( pFrames );
+    Gia_ManStop( p->pFrames );
     // cleanup
-    Unr_ManFree( p );
+    Unr_ManFree( pUnroll );
+    Bmc_MnaFree( p );
     return status;
 }
 

src/sat/bmc/bmcUnroll.c

@@ -408,6 +408,7 @@ Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f )
         hStart += Unr_ObjSize( pUnrObj );
     }
     assert( p->pObjs + hStart == p->pEnd );
+    assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(p->pGia) );
     return p->pFrames;
 }
 Gia_Man_t * Unr_ManUnroll( Gia_Man_t * pGia, int nFrames )