Multi-output property solver.

6 files changed, 79 insertions, 51 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b8b5f5c4..d4cec6dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32346,16 +32346,15 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose );
-    Vec_Int_t * vStatuses;
-    int TimeOutGlo = 30;
-    int TimeOutLoc =  2;
-    int TimeOutInc =  2;
-    int fUseSyn    =  0;
-    int c, fVerbose = 0;
-    int fVeryVerbose = 0;
+    extern int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars );
+    Vec_Int_t * vStatuses; int c;
+    Bmc_MulPar_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Bmc_MulPar_t) );
+    pPars->TimeOutGlo =  30;
+    pPars->TimeOutLoc =   2;
+    pPars->TimeOutInc = 100;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32365,9 +32364,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            TimeOutGlo = atoi(argv[globalUtilOptind]);
+            pPars->TimeOutGlo = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( TimeOutGlo < 0 )
+            if ( pPars->TimeOutGlo < 0 )
                 goto usage;
             break;
         case 'L':
@@ -32376,9 +32375,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
             }
-            TimeOutLoc = atoi(argv[globalUtilOptind]);
+            pPars->TimeOutLoc = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( TimeOutLoc <= 0 )
+            if ( pPars->TimeOutLoc <= 0 )
                 goto usage;
             break;
         case 'M':
@@ -32387,19 +32386,22 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
                 goto usage;
             }
-            TimeOutInc = atoi(argv[globalUtilOptind]);
+            pPars->TimeOutInc = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( TimeOutInc <= 0 )
+            if ( pPars->TimeOutInc <= 0 )
                 goto usage;
             break;
         case 's':
-            fUseSyn ^= 1;
+            pPars->fUseSyn ^= 1;
+            break;
+        case 'd':
+            pPars->fDumpFinal ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'w':
-            fVeryVerbose ^= 1;
+            pPars->fVeryVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -32412,21 +32414,22 @@ 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, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
+    pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars );
     vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
     Abc_FrameReplacePoStatuses( pAbc, &vStatuses );        
     Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" );
+    Abc_Print( -2, "usage: &mprove [-TLM num] [-sdvwh]\n" );
     Abc_Print( -2, "\t         proves multi-output testcase by applying several engines\n" );
-    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-T num : approximate global runtime limit in seconds [default = %d]\n",     pPars->TimeOutGlo );
+    Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n",      pPars->TimeOutLoc );
+    Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n",      pPars->TimeOutInc );
+    Abc_Print( -2, "\t-s     : toggle using combinational synthesis [default = %s]\n",            pPars->fUseSyn?      "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping invariant into a file [default = %s]\n",            pPars->fDumpFinal?   "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 additional verbose information [default = %s]\n",  pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d662f376..4800557a 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2174,16 +2174,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
             {
                 int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
                 if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
-                    Abc_Print( 1, "None of the %d outputs is found to be SAT.   ", nOutputs );
+                    Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
                 else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
-                    Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
+                    Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
                 else
                 {
                     Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
                     if ( pPars->nDropOuts )
                         Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
-                    Abc_Print( 1, ".   " );
                 }
+                Abc_Print( 1, " after %d frames", pPars->iFrame );
+                Abc_Print( 1, ".   " );
             }
         }
         ABC_PRT( "Time", Abc_Clock() - clk );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 39f95e14..2dd51f38 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1112,12 +1112,14 @@ finish:
     }
     if ( pPars->nSolved )
     {
+/*
         if ( !pPars->fSilent )
         {
         if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
         Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
         }
+*/
     }
     else if ( r == pPars->nRounds && f == pPars->nFrames )
     {
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index ff1e005b..1a98001a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -91,6 +91,18 @@ struct Bmc_AndPar_t_
     int         nFailOuts;      // the number of failed outputs
     int         nDropOuts;      // the number of dropped outputs
 };
+ 
+typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
+struct Bmc_MulPar_t_
+{
+    int         TimeOutGlo;
+    int         TimeOutLoc;
+    int         TimeOutInc;
+    int         fUseSyn;
+    int         fDumpFinal;
+    int         fVerbose;
+    int         fVeryVerbose;
+};
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ea08c1e4..4cc2a692 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1353,7 +1353,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             goto finish;
         }
         // consider the next timeframe
-        if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
+        if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
             pPars->iFrame = f-1;
         // map nodes of this section
         Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 975783d9..6b60daf9 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -20,7 +20,9 @@
 
 #include "bmc.h"
 #include "proof/ssw/ssw.h"
+#include "misc/extra/extra.h"
 #include "aig/gia/giaAig.h"
+#include "aig/ioa/ioa.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -128,7 +130,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
+Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
 {
     Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
     Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
@@ -136,12 +138,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
     Vec_Ptr_t * vCexes;
     Aig_Man_t * pTemp;
     abctime clkStart = Abc_Clock();
-    int nTimeToStop  = TimeOutGlo ? TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    int nTimeToStop  = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
     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 );
+    if ( pPars->fVerbose )
+        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->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)
@@ -151,8 +153,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
         Ssw_RarSetDefaultParams( pParsSim );
         pParsSim->fSolveAll = 1;
         pParsSim->fNotVerbose = 1;
-        pParsSim->fSilent = !fVeryVerbose;
-        pParsSim->TimeOut = TimeOutLoc;
+        pParsSim->fSilent = !pPars->fVeryVerbose;
+        pParsSim->TimeOut = pPars->TimeOutLoc;
         pParsSim->nRandSeed = (i * 17) % 500;
         RetValue *= Ssw_RarSimulate( p, pParsSim );
         // sort outputs
@@ -166,13 +168,13 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
             Vec_IntFree( vLeftOver );
             Aig_ManStop( pTemp );
         }
-        if ( fVerbose )
+        if ( pPars->fVerbose )
             Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
 
         // check timeout
-        if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+        if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
         {
-            printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
             break;
         }
 
@@ -180,9 +182,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
         Saig_ParBmcSetDefaultParams( pParsBmc );
         pParsBmc->fSolveAll = 1;
         pParsBmc->fNotVerbose = 1;
-        pParsBmc->fSilent = !fVeryVerbose;
-        pParsBmc->nTimeOut = TimeOutLoc;
+        pParsBmc->fSilent = !pPars->fVeryVerbose;
+        pParsBmc->nTimeOut = pPars->TimeOutLoc;
         RetValue *= Saig_ManBmcScalable( p, pParsBmc );
+        if ( pPars->fVeryVerbose )
+            Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", 
+                Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
         // sort outputs
         if ( p->vSeqModelVec )
         {
@@ -194,41 +199,46 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
             Vec_IntFree( vLeftOver );
             Aig_ManStop( pTemp );
         }
-        if ( fVerbose )
+        if ( pPars->fVerbose )
             Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
 
         // check timeout
-        if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+        if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
         {
-            printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
             break;
         }
 
         // synthesize
-        if ( fUseSyn )
+        if ( pPars->fUseSyn )
         {
-            p = Gia_ManMultiProveSyn( pTemp = p, fVerbose, fVeryVerbose );
+            p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
             Aig_ManStop( pTemp );
-            if ( fVerbose )
+            if ( pPars->fVerbose )
                 Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
         }
 
         // increase timeout
-        TimeOutLoc *= TimeOutInc;
+        pPars->TimeOutLoc += pPars->TimeOutLoc * pPars->TimeOutInc / 100;
     }
     Vec_IntFree( vOutMap );
+    if ( pPars->fDumpFinal )
+    {
+        char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
+        Ioa_WriteAiger( p, pFileName, 0, 0 );
+        printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
+    }
     Aig_ManStop( p );
     return vCexes;
 }
-int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
+int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars )
 {
     Aig_Man_t * pAig;
     if ( p->vSeqModelVec )
         Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
     pAig = Gia_ManToAig( p, 0 );
-    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
+    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
     assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
-//    Aig_ManStop( pAig );
     return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
 }