Multi-output property solver.

3 files changed, 127 insertions, 29 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5c66958f..b8b5f5c4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2447,13 +2447,16 @@ usage:
 ***********************************************************************/
 int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c;
+    int c, fShort = 1;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 's':
+            fShort ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2492,16 +2495,26 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->vStatuses )
     {
-        int i, Entry;
-        Vec_IntForEachEntry( pAbc->vStatuses, Entry, i )
-            printf( "%d=%d  ", i, Entry );
+        if ( fShort )
+        {
+            printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).", 
+                Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1), 
+                Vec_IntCountEntry(pAbc->vStatuses, -1), Vec_IntSize(pAbc->vStatuses) );
+        }
+        else
+        {
+            int i, Entry;
+            Vec_IntForEachEntry( pAbc->vStatuses, Entry, i )
+                printf( "%d=%d  ", i, Entry );
+        }
         printf( "\n" );
     }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: print_status [-h]\n" );
+    Abc_Print( -2, "usage: print_status [-sh]\n" );
     Abc_Print( -2, "\t        prints verification status\n" );
+    Abc_Print( -2, "\t-s    : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -32333,18 +32346,61 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose );
+    extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose );
     Vec_Int_t * vStatuses;
-    char * pCommLine = NULL;
+    int TimeOutGlo = 30;
+    int TimeOutLoc =  2;
+    int TimeOutInc =  2;
+    int fUseSyn    =  0;
     int c, fVerbose = 0;
+    int fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeOutGlo = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOutGlo < 0 )
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeOutLoc = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOutLoc <= 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeOutInc = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOutInc <= 0 )
+                goto usage;
+            break;
+        case 's':
+            fUseSyn ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -32356,16 +32412,21 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
         return 1;
     }
-    pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose );
+    pAbc->Status = Gia_ManMultiProve( pAbc->pGia, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
     vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
     Abc_FrameReplacePoStatuses( pAbc, &vStatuses );        
     Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mprove [-vh]\n" );
+    Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" );
     Abc_Print( -2, "\t         proves multi-output testcase by applying several engines\n" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n",     TimeOutGlo );
+    Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n",      TimeOutLoc );
+    Abc_Print( -2, "\t-M num : approximate multiple of the local runtime limit [default = %d]\n", TimeOutInc );
+    Abc_Print( -2, "\t-s     : toggle using combinational synthesis [default = %s]\n",            fUseSyn? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",             fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing additional verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index cd93d28b..39f95e14 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1054,7 +1054,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
                 if ( !pPars->fSilent )
                 {
                 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
-                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
+                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
                 Abc_Print( 1, "Reached timeout (%d sec).\n",  pPars->TimeOut );
                 }
                 goto finish;
@@ -1064,7 +1064,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
                 if ( !pPars->fSilent )
                 {
                 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
-                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
+                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
                 Abc_Print( 1, "Reached gap timeout (%d sec).\n",  pPars->TimeOutGap );
                 }
                 goto finish;
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;