New BMC engine.

src/aig/gia/giaJf.c

@@ -159,7 +159,7 @@ void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vL
         }
     }
 }
-Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
+Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
 {
     Cnf_Dat_t * pCnf; 
     Gia_Obj_t * pObj;
@@ -189,6 +189,42 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas
     pCnf->pVarNums = pMap;
     return pCnf;
 }
+Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
+{
+    Cnf_Dat_t * pCnf; 
+    int i, Entry, iOut;
+    // generate CNF
+    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
+    pCnf->pMan = (Aig_Man_t *)p;
+    pCnf->nVars = Gia_ManObjNum(p);
+    pCnf->nLiterals = Vec_IntSize(vLits);
+    pCnf->nClauses = Vec_IntSize(vClas);
+    pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
+    pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
+    Vec_IntForEachEntry( vClas, Entry, i )
+        pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
+    pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
+    // create mapping of objects into their clauses
+    pCnf->pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p) );
+    pCnf->pObj2Count  = ABC_FALLOC( int, Gia_ManObjNum(p) );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        iOut = Abc_Lit2Var(pCnf->pClauses[i][0]);
+        if ( pCnf->pObj2Clause[iOut] == -1 )
+        {
+//            printf( "\n" );
+            pCnf->pObj2Clause[iOut] = i;
+            pCnf->pObj2Count[iOut] = 1;
+        }
+        else
+        {
+            assert( pCnf->pObj2Count[iOut] > 0 );
+            pCnf->pObj2Count[iOut]++;
+        }
+//printf( "%d ", iOut );
+    }
+    return pCnf;
+}
 
 /**Function*************************************************************
 
@@ -1713,7 +1749,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
     Jf_ManFree( p );
     return pNew;
 }
-void Jf_ManTestCnf( Gia_Man_t * p )
+Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p )
 {
     Cnf_Dat_t * pCnf; 
     Gia_Man_t * pNew;
@@ -1722,8 +1758,14 @@ void Jf_ManTestCnf( Gia_Man_t * p )
     pPars->fGenCnf = 1;
     pNew = Jf_ManPerformMapping( p, pPars );
     pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
-    Gia_ManStop( pNew );
+//    Gia_ManStop( pNew );
+    return pCnf;
+}
+void Jf_ManTestCnf( Gia_Man_t * p )
+{
+    Cnf_Dat_t * pCnf = Jf_ManDeriveCnf( p );
     Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
+    Gia_ManStop( (Gia_Man_t *)pCnf->pMan );
     Cnf_DataFree(pCnf);
 }
 

src/sat/bmc/bmcBmcAnd.c

@@ -34,6 +34,7 @@ typedef struct Bmc_Mna_t_ Bmc_Mna_t;
 struct Bmc_Mna_t_
 {
     Gia_Man_t *         pFrames;  // time frames
+    Cnf_Dat_t *         pCnf;     // CNF derived for the timeframes
     Vec_Int_t *         vPiMap;   // maps unrolled GIA PIs into user GIA PIs
     Vec_Int_t *         vId2Var;  // maps GIA IDs into SAT vars
     Vec_Int_t *         vInputs;  // inputs of the cone
@@ -396,10 +397,12 @@ Bmc_Mna_t * Bmc_MnaAlloc()
     p->pSat      = sat_solver_new();
     p->nSatVars  = 1;
     p->clkStart  = Abc_Clock();
+    sat_solver_setnvars( p->pSat, 1000 );
     return p;
 }
 void Bmc_MnaFree( Bmc_Mna_t * p )
 {
+    Cnf_DataFree( p->pCnf );
     Vec_IntFreeP( &p->vPiMap );
     Vec_IntFreeP( &p->vId2Var );
     Vec_IntFreeP( &p->vInputs );
@@ -767,7 +770,7 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
     Bmc_Mna_t * p;
     int nFramesMax, f, i=0, Lit, status, RetValue = -2;
@@ -851,6 +854,199 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p )
+{
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 );
+    Aig_ManStop( pAig );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
+{
+    int iObj = Gia_ObjId( p->pFrames, pObj );
+    if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
+    {
+        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
+        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
+        return;
+    }
+    if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
+        return;
+    Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
+    if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
+    {
+        int i, nClas, iCla;
+        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
+        if ( Gia_ObjIsAnd(pObj) )
+        Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
+        // extend the SAT solver
+        if ( p->nSatVars > sat_solver_nvars(p->pSat) )
+            sat_solver_setnvars( p->pSat, p->nSatVars );
+        // add clauses
+        nClas = p->pCnf->pObj2Count[iObj];
+        iCla  = p->pCnf->pObj2Clause[iObj];
+        for ( i = 0; i < nClas; i++ )
+        {
+            int nLits, pLits[8];
+            int * pClauseThis = p->pCnf->pClauses[iCla+i];
+            int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
+            for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
+            {
+                assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
+                pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
+            }
+            assert( nLits < 8 );
+            if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
+                break;
+        }
+        if ( i < nClas )
+            printf( "SAT solver became UNSAT after adding clauses.\n" );
+    }
+    else assert( Gia_ObjIsCi(pObj) );
+}
+void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    for ( i = iStart; i < iStop; i++ )
+    {
+        pObj = Gia_ManPo(p->pFrames, i);
+        if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p->pFrames) )
+            continue;
+        Gia_ManBmcAddCnfNew_rec( p, pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+{
+    extern Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p );
+    Bmc_Mna_t * p;
+    int nFramesMax, f, i=0, Lit, status, RetValue = -2;
+    abctime clk = Abc_Clock();
+    p = Bmc_MnaAlloc();
+    p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
+    nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
+    if ( pPars->fVerbose )
+    {
+        printf( "Unfolding for %d frames with first non-trivial PO %d.  ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
+    if ( pPars->fUseSynth )
+    {
+        Gia_Man_t * pTemp = p->pFrames;
+        p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
+        Gia_ManStop( pTemp );
+    }
+    else if ( pPars->fVerbose )
+        Gia_ManPrintStats( p->pFrames, NULL );
+    if ( pPars->fDumpFrames )
+    {
+        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+        printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
+    }
+//    p->pCnf = Jf_ManDeriveCnf( p->pFrames );
+//    Gia_ManStop( p->pFrames );
+//    p->pFrames = (Gia_Man_t *)p->pCnf->pMan; p->pCnf->pMan = NULL;
+    p->pCnf = Cnf_DeriveGia( p->pFrames );
+    Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
+        {
+            // create another slice
+//            Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
+            // create CNF in the SAT solver
+//            Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
+            Gia_ManBmcAddCnfNew( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
+            // try solving the outputs
+            for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
+            {
+                Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
+                if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
+                    continue;
+                if ( Gia_ObjChild0(pObj) == Gia_ManConst1(p->pFrames) )
+                {
+                    printf( "Output %d is trivially SAT.\n", i );
+                    continue;
+                }
+                Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
+                status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+                if ( status == l_False ) // unsat
+                    continue;
+                if ( status == l_True )  // sat
+                    RetValue = 0;
+                if ( status == l_Undef ) // undecided
+                    RetValue = -1;
+                break;
+            }
+            // report statistics
+            if ( pPars->fVerbose )
+            {
+                printf( "%4d :  PI =%9d.  AIG =%9d.  Var =%8d.  In =%6d.  And =%9d.  Cla =%9d.  Conf =%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), 
+                    sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+            }
+        }
+        if ( RetValue != -2 )
+        {
+            if ( RetValue == -1 )
+                printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
+            else
+            {
+                ABC_FREE( pGia->pCexSeq );
+                pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
+                printf( "Output %d of miter \"%s\" was asserted in frame %d.  ", 
+                    i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+            }
+            break;
+        }
+        pPars->iFrame = f;
+    }
+    if ( RetValue == -2 )
+        RetValue = -1;
+    // cleanup
+    Gia_ManStop( p->pFrames );
+    Bmc_MnaFree( p );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////