Multi-output property solver.

1 files changed, 52 insertions, 15 deletions

diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 7a744228..975783d9 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -105,7 +105,30 @@ void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSiz
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fVerbose )
+Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+    Aig_Man_t * pAig;
+    Gia_Man_t * pGia, * pTemp;
+    pGia = Gia_ManFromAig( p );
+    pGia = Gia_ManAigSyn2( pTemp = pGia, 0, 0 );
+    Gia_ManStop( pTemp );
+    pAig = Gia_ManToAig( pGia, 0 );
+    Gia_ManStop( pGia );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
 {
     Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
     Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
@@ -117,22 +140,18 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
     int nTotalPo     = Saig_ManPoNum(p);
     int nTotalSize   = Aig_ManObjNum(p);
     int i, RetValue  = -1;
+    if ( fVerbose )
+        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d.\n", TimeOutGlo, TimeOutLoc, TimeOutInc );
     // create output map
     vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
     vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
     for ( i = 0; i < 1000; i++ )
     {
-        // synthesize
-//        p = Gia_ManMultiProveSyn( pTemp = p );
-//        Aig_ManStop( pTemp );
-//        if ( fVerbose )
-//            Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
-
         // perform SIM3
         Ssw_RarSetDefaultParams( pParsSim );
         pParsSim->fSolveAll = 1;
         pParsSim->fNotVerbose = 1;
-        pParsSim->fSilent = 1;
+        pParsSim->fSilent = !fVeryVerbose;
         pParsSim->TimeOut = TimeOutLoc;
         pParsSim->nRandSeed = (i * 17) % 500;
         RetValue *= Ssw_RarSimulate( p, pParsSim );
@@ -147,14 +166,21 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
             Vec_IntFree( vLeftOver );
             Aig_ManStop( pTemp );
         }
-//        if ( fVerbose )
+        if ( fVerbose )
             Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
 
+        // check timeout
+        if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+        {
+            printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+            break;
+        }
+
         // perform BMC
         Saig_ParBmcSetDefaultParams( pParsBmc );
         pParsBmc->fSolveAll = 1;
         pParsBmc->fNotVerbose = 1;
-        pParsBmc->fSilent = 1;
+        pParsBmc->fSilent = !fVeryVerbose;
         pParsBmc->nTimeOut = TimeOutLoc;
         RetValue *= Saig_ManBmcScalable( p, pParsBmc );
         // sort outputs
@@ -168,28 +194,39 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
             Vec_IntFree( vLeftOver );
             Aig_ManStop( pTemp );
         }
-//        if ( fVerbose )
+        if ( fVerbose )
             Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
 
-        // increase timeout
-        TimeOutLoc *= TimeOutInc;
+        // check timeout
         if ( nTimeToStop && Abc_Clock() > nTimeToStop )
         {
             printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
             break;
         }
+
+        // synthesize
+        if ( fUseSyn )
+        {
+            p = Gia_ManMultiProveSyn( pTemp = p, fVerbose, fVeryVerbose );
+            Aig_ManStop( pTemp );
+            if ( fVerbose )
+                Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
+        }
+
+        // increase timeout
+        TimeOutLoc *= TimeOutInc;
     }
     Vec_IntFree( vOutMap );
     Aig_ManStop( p );
     return vCexes;
 }
-int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose )
+int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pAig;
     if ( p->vSeqModelVec )
         Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
     pAig = Gia_ManToAig( p, 0 );
-    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, 30, 2, 2, fVerbose );
+    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
     assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
 //    Aig_ManStop( pAig );
     return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;