New BMC engine.

6 files changed, 65 insertions, 58 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 8d953273..1d170102 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1097,6 +1097,7 @@ extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars,
 /*=== giaJf.c ===========================================================*/
 extern void                Jf_ManSetDefaultPars( Jf_Par_t * pPars );
 extern Gia_Man_t *         Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
+extern Gia_Man_t *         Jf_ManDeriveCnf( Gia_Man_t * p );
 /*=== giaIso.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 9ab27c7c..46aa5d3f 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -212,7 +212,6 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas
         iOut = Abc_Lit2Var(pCnf->pClauses[i][0]);
         if ( pCnf->pObj2Clause[iOut] == -1 )
         {
-//            printf( "\n" );
             pCnf->pObj2Clause[iOut] = i;
             pCnf->pObj2Count[iOut] = 1;
         }
@@ -221,7 +220,6 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas
             assert( pCnf->pObj2Count[iOut] > 0 );
             pCnf->pObj2Count[iOut]++;
         }
-//printf( "%d ", iOut );
     }
     return pCnf;
 }
@@ -1455,8 +1453,6 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
     {
         vLits = Vec_IntAlloc( 1000 );
         vClas = Vec_IntAlloc( 1000 );
-        Vec_IntPush( vClas, Vec_IntSize(vLits) );
-        Vec_IntPush( vLits, 1 );
     }
     // create new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
@@ -1499,10 +1495,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
             Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
         // create GIA
         iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
-        iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
-        Vec_IntWriteEntry( vCopies, i, iLit );
         if ( p->pPars->fGenCnf )
             Jf_ManGenCnf( uTruth, iLit, vLeaves, vLits, vClas, vCover );
+        iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
+        Vec_IntWriteEntry( vCopies, i, iLit );
         // create mapping
         Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) );
         Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
@@ -1541,7 +1537,11 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
     // derive CNF
     if ( p->pPars->fGenCnf )
+    {
+        Vec_IntPush( vClas, Vec_IntSize(vLits) );
+        Vec_IntPush( vLits, 1 );
         pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
+    }
     Vec_IntFreeP( &vLits );
     Vec_IntFreeP( &vClas );
     return pNew;
@@ -1749,23 +1749,25 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
     Jf_ManFree( p );
     return pNew;
 }
-Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p )
+Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p )
 {
-    Cnf_Dat_t * pCnf; 
-    Gia_Man_t * pNew;
     Jf_Par_t Pars, * pPars = &Pars;
     Jf_ManSetDefaultPars( pPars );
     pPars->fGenCnf = 1;
-    pNew = Jf_ManPerformMapping( p, pPars );
-    pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
-//    Gia_ManStop( pNew );
-    return pCnf;
+    return Jf_ManPerformMapping( p, pPars );
 }
 void Jf_ManTestCnf( Gia_Man_t * p )
 {
-    Cnf_Dat_t * pCnf = Jf_ManDeriveCnf( p );
+    Gia_Man_t * pNew;
+    Cnf_Dat_t * pCnf;
+    int i;
+//    Cnf_Dat_t * pCnf = Cnf_DeriveGia( p );
+    pNew = Jf_ManDeriveCnf( p );
+    pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
     Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
-    Gia_ManStop( (Gia_Man_t *)pCnf->pMan );
+    for ( i = 0; i < pCnf->nVars; i++ )
+        printf( "%d : %d %d\n", i, pCnf->pObj2Count[i], pCnf->pObj2Clause[i] );
+    Gia_ManStop( pNew );
     Cnf_DataFree(pCnf);
 }
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index eb728cd0..71becf0b 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -368,7 +368,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     if ( p->pSibls )
         Gia_ManPrintChoiceStats( p );
     if ( Gia_ManHasMapping(p) )
-        Gia_ManPrintMappingStats( p, pPars->fDumpFile );
+        Gia_ManPrintMappingStats( p, pPars && pPars->fDumpFile );
     if ( pPars && pPars->fNpn && Gia_ManHasMapping(p) && Gia_ManLutSizeMax(p) <= 4 )
         Gia_ManPrintNpnClasses( p );
     if ( p->vPacking )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d4cec6dd..77f7bbe0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32457,6 +32457,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fLoadCnf      =    0;  // dynamic CNF loading
     pPars->fDumpFrames   =    0;  // dump unrolled timeframes
     pPars->fUseSynth     =    0;  // use synthesis
+    pPars->fUseOldCnf    =    0;  // use old CNF construction
     pPars->fVerbose      =    0;  // verbose 
     pPars->fVeryVerbose  =    0;  // very verbose 
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
@@ -32464,7 +32465,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFailOuts     =    0;  // the number of failed outputs
     pPars->nDropOuts     =    0;  // the number of dropped outputs
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdsvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFAdscvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32501,15 +32502,15 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFramesAdd < 0 )
                 goto usage;
             break;
-        case 'c':
-            pPars->fLoadCnf ^= 1;
-            break;
         case 'd':
             pPars->fDumpFrames ^= 1;
             break;
         case 's':
             pPars->fUseSynth ^= 1;
             break;
+        case 'c':
+            pPars->fUseOldCnf ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -32533,15 +32534,15 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SFA num] [-cdsvwh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SFA num] [-dscvwh]\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-A num : the number of additional frames to unroll [default = %d]\n",   pPars->nFramesAdd );
-    Abc_Print( -2, "\t-c     : toggle dynamic CNF loading [default = %s]\n",                  pPars->fLoadCnf? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle dumping unfolded timeframes [default = %s]\n",          pPars->fDumpFrames? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle synthesizing unrolled timeframes [default = %s]\n",     pPars->fUseSynth? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping unfolded timeframes [default = %s]\n",          pPars->fDumpFrames?  "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle synthesizing unrolled timeframes [default = %s]\n",     pPars->fUseSynth?    "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle using old CNF computation [default = %s]\n",            pPars->fUseOldCnf?   "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 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++ )