New BMC engine.

2 files changed, 36 insertions, 33 deletions

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 1a98001a..ef401e70 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -84,6 +84,7 @@ struct Bmc_AndPar_t_
     int         fLoadCnf;       // dynamic CNF loading
     int         fDumpFrames;    // dump unrolled timeframes
     int         fUseSynth;      // use synthesis
+    int         fUseOldCnf;     // use old CNF construction
     int         fVerbose;       // verbose 
     int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 8a7a1932..649453ee 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -865,36 +865,17 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
   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 ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
+        return;
     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) )
     {
@@ -915,6 +896,8 @@ void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
             int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
             for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
             {
+                if ( pClauseThis[nLits] < 2 )
+                    printf( "\n\n\nError in CNF generation:  Constant literal!\n\n\n" );
                 assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
                 pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
             }
@@ -951,11 +934,30 @@ void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop )
   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     []
+
+***********************************************************************/
 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;
+    Gia_Man_t * pTemp;
+    int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
     abctime clk = Abc_Clock();
     p = Bmc_MnaAlloc();
     p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
@@ -967,9 +969,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     }
     if ( pPars->fUseSynth )
     {
-        Gia_Man_t * pTemp = p->pFrames;
-        p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
-        Gia_ManStop( pTemp );
+        p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, pPars->fVerbose, 0 );  Gia_ManStop( pTemp );
     }
     else if ( pPars->fVerbose )
         Gia_ManPrintStats( p->pFrames, NULL );
@@ -978,19 +978,21 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         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 );
+    if ( pPars->fUseOldCnf )
+        p->pCnf = Cnf_DeriveGia( p->pFrames );
+    else
+    {
+        p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames );  Gia_ManStop( pTemp );
+        p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
+    }
     Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
+    // create clauses for constant node
+//    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
     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++ )