Integrating synthesis into the new BMC engine.

6 files changed, 78 insertions, 14 deletions

diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index cdf36e7a..5855fc3d 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -36,13 +36,14 @@ struct Dam_Man_t_
 {
     Gia_Man_t *      pGia;      // user's AIG
     Vec_Int_t *      vNod2Set;  // node ID into fanin set
-    Vec_Int_t *      vDiv2Nod;  // div ID into fanin set
-    Vec_Int_t *      vSetStore; // stored multisets
-    Vec_Int_t *      vNodStore; // stored divisors
+    Vec_Int_t *      vDiv2Nod;  // div ID into root node set
+    Vec_Int_t *      vSetStore; // fanin set storage
+    Vec_Int_t *      vNodStore; // root node set storage
     Vec_Flt_t *      vCounts;   // occur counts
     Vec_Int_t *      vNodLevR;  // node reverse level
     Vec_Int_t *      vDivLevR;  // divisor reverse level
-    Vec_Que_t *      vQue;      // pairs by count
+    Vec_Int_t *      vVisit;    // visited MUXes
+    Vec_Que_t *      vQue;      // pairs by their weight
     Hash_IntMan_t *  vHash;     // pair hash table
     abctime          clkStart;  // starting the clock
     int              nLevelMax; // maximum level
@@ -386,11 +387,13 @@ Dam_Man_t * Dam_ManAlloc( Gia_Man_t * pGia )
     Dam_Man_t * p;
     p = ABC_CALLOC( Dam_Man_t, 1 );
     p->clkStart = Abc_Clock();
+    p->vVisit = Vec_IntAlloc( 1000 );
     p->pGia = pGia;
     return p;
 }
 void Dam_ManFree( Dam_Man_t * p )
 {   
+    Vec_IntFreeP( &p->vVisit );
     Vec_IntFreeP( &p->vDivLevR );
     Vec_IntFreeP( &p->vNodLevR );
     Vec_IntFreeP( &p->vNod2Set );
@@ -425,6 +428,10 @@ void Dam_ManCollectSets_rec( Dam_Man_t * p, int Id )
         return;
     if ( Gia_ObjIsMux(p->pGia, pObj) )
     {
+        if ( pObj->fMark0 )
+            return;
+        pObj->fMark0 = 1;
+        Vec_IntPush( p->vVisit, Id );
         Dam_ManCollectSets_rec( p, Gia_ObjFaninId0(pObj, Id) );
         Dam_ManCollectSets_rec( p, Gia_ObjFaninId1(pObj, Id) );
         Dam_ManCollectSets_rec( p, Gia_ObjFaninId2(p->pGia, Id) );
@@ -451,9 +458,12 @@ void Dam_ManCollectSets( Dam_Man_t * p )
     p->vNod2Set  = Vec_IntStart( Gia_ManObjNum(p->pGia) );
     p->vSetStore = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );
     Vec_IntPush( p->vSetStore, -1 );
+    Vec_IntClear( p->vVisit );
     Gia_ManForEachCo( p->pGia, pObj, i )
         Dam_ManCollectSets_rec( p, Gia_ObjFaninId0p(p->pGia, pObj) );
     ABC_FREE( p->pGia->pRefs );
+    Gia_ManForEachObjVec( p->vVisit, p->pGia, pObj, i )
+        pObj->fMark0 = 0;
 }
 
 /**Function*************************************************************
@@ -900,7 +910,7 @@ void Dam_ManUpdate( Dam_Man_t * p, int iDiv )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Dam_ManMultiExtractInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Dam_ManAreaBalanceInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew;
     Dam_Man_t * p;
@@ -935,14 +945,14 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
 {
     Gia_Man_t * pNew0, * pNew, * pNew1, * pNew2;
     // get the starting manager
-    pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p) : p;
+    pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p;
     if ( fVerbose )     Gia_ManPrintStats( pNew0, NULL );
     // derive internal manager
     pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0 );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
     if ( pNew0 != p ) Gia_ManStop( pNew0 );
     // perform the operation
-    pNew1 = Dam_ManMultiExtractInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose );
+    pNew1 = Dam_ManAreaBalanceInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose );
     if ( fVerbose )     Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
     // derive the final result
@@ -952,6 +962,36 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
     return pNew2;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Synthesis script.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Jf_Par_t Pars, * pPars = &Pars;
+    Jf_ManSetDefaultPars( pPars );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    // perform mapping
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+//    Gia_ManStop( pTemp );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c7a1c268..0e1c9b84 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32163,6 +32163,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
     pPars->fLoadCnf      =    0;  // dynamic CNF loading
     pPars->fDumpFrames   =    0;  // dump unrolled timeframes
+    pPars->fUseSynth     =    0;  // use synthesis
     pPars->fVerbose      =    0;  // verbose 
     pPars->fVeryVerbose  =    0;  // very verbose 
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
@@ -32170,7 +32171,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, "SFAcdvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdsvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32213,6 +32214,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDumpFrames ^= 1;
             break;
+        case 's':
+            pPars->fUseSynth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -32236,13 +32240,14 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SFA num] [-cdvwh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SFA num] [-cdsvwh]\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-w     : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index a928fecf..92641b71 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -89,7 +89,7 @@ extern int           Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
 
 /*=== dauGia.c  ==========================================================*/
 extern int           Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
-extern void *        Dsm_ManDeriveGia( void * p );
+extern void *        Dsm_ManDeriveGia( void * p, int fUseMuxes );
 
 /*=== dauMerge.c  ==========================================================*/
 extern void          Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index a714f622..2712effc 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -68,7 +68,10 @@ int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVa
         return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars );
     t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
     t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
-    return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
+    if ( pGia->pMuxes )
+        return Gia_ManHashMuxReal( pGia, pFanins[nVars], t1, t0 );
+    else
+        return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
 }
 
 /**Function*************************************************************
@@ -110,7 +113,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
         for ( (*p)++; *p < q; (*p)++ )
         {
             Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
-            Res = Gia_ManHashXor( pGia, Res, Lit );
+            if ( pGia->pMuxes )
+                Res = Gia_ManHashXorReal( pGia, Res, Lit );
+            else
+                Res = Gia_ManHashXor( pGia, Res, Lit );
         }
         assert( *p == q );
         return Abc_LitNotCond( Res, fCompl );
@@ -156,7 +162,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
             assert( **p == '{' && *q == '}' );
             *p = q;
         }
-        Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
+        if ( pGia->pMuxes )
+            Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
+        else
+            Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
         return Abc_LitNotCond( Res, fCompl );
     }
     if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
@@ -250,7 +259,7 @@ void Dsm_ManReportStats()
   SeeAlso     []
 
 ***********************************************************************/
-void * Dsm_ManDeriveGia( void * pGia )
+void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes )
 {
     Gia_Man_t * p = (Gia_Man_t *)pGia;
     Gia_Man_t * pNew, * pTemp;
@@ -263,6 +272,8 @@ void * Dsm_ManDeriveGia( void * pGia )
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    if ( fUseMuxes )
+        pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
     // map primary inputs
     Gia_ManFillValue(p);
     Gia_ManConst0(p)->Value = 0;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 072040c5..65c24e93 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -82,6 +82,7 @@ struct Bmc_AndPar_t_
     int         nConfLimit;     // maximum number of conflicts at a node
     int         fLoadCnf;       // dynamic CNF loading
     int         fDumpFrames;    // dump unrolled timeframes
+    int         fUseSynth;      // use synthesis
     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 1f203373..964ba54e 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -769,11 +769,18 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
 ***********************************************************************/
 int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
+    extern Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
     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 );
+    if ( pPars->fUseSynth )
+    {
+        Gia_Man_t * pTemp = p->pFrames;
+        p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
+        Gia_ManStop( pTemp );
+    }
     nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
     if ( pPars->fVerbose )
     {