Multi-output property solver.

11 files changed, 126 insertions, 45 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 4d2239c7..ca334c98 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1447,6 +1447,10 @@ SOURCE=.\src\sat\bmc\bmcLoad.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcMulti.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcUnroll.c
 # End Source File
 # End Group
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 122e5025..8d953273 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -133,6 +133,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vLutConfigs;   // LUT configurations
     Abc_Cex_t *    pCexComb;      // combinational counter-example
     Abc_Cex_t *    pCexSeq;       // sequential counter-example
+    Vec_Ptr_t *    vSeqModelVec;  // sequential counter-examples
     int *          pCopies;       // intermediate copies
     Vec_Int_t *    vTruths;       // used for truth table computation
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 2eaf8eee..eb728cd0 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -72,6 +72,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
 ***********************************************************************/
 void Gia_ManStop( Gia_Man_t * p )
 {
+    if ( p->vSeqModelVec )
+        Vec_PtrFreeFree( p->vSeqModelVec );
     Gia_ManStaticFanoutStop( p );
     Tim_ManStopP( (Tim_Man_t **)&p->pManTime );
     assert( p->pManTime == NULL );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 08136e7d..f3edca36 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1716,7 +1716,7 @@ int Gia_ManHasChoices_very_old( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
+Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
 {
     Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
     Gia_Man_t * p = Gia_ManDup( pInit );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 21ace6d8..5c66958f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -398,6 +398,7 @@ static int Abc_CommandAbc9Cycle              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Cone               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Slice              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -961,6 +962,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&cone",         Abc_CommandAbc9Cone,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&slice",        Abc_CommandAbc9Slice,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
@@ -32259,9 +32261,9 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
+    extern Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
     Vec_Int_t * vStatus;
     char * pCommLine = NULL;
     int c, nGroupSize = 1, fVerbose = 0;
@@ -32300,15 +32302,15 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" );
         return 1;
     }
-    vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
+    vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
     Vec_IntFree( vStatus );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" );
+    Abc_Print( -2, "usage: &gprove [-GS num] [-vh]\n" );
     Abc_Print( -2, "\t         proves multi-output testcase by splitting outputs into groups\n" );
     Abc_Print( -2, "\t         (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" );
     Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize );
@@ -32329,6 +32331,56 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose );
+    Vec_Int_t * vStatuses;
+    char * pCommLine = NULL;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
+        return 1;
+    }
+    pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose );
+    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, "\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-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4fbf7c70..d662f376 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-    if ( RetValue == 1 )
-    {
-        Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
-    }
-    else if ( RetValue == -1 )
+    if ( !pPars->fSilent )
     {
-        if ( pPars->nFailOuts == 0 )
+        if ( RetValue == 1 )
         {
-            Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
-            if ( nTimeOut && Abc_Clock() > nTimeOut )
-                Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
-            else
-                Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
         }
-        else
+        else if ( RetValue == -1 )
         {
-            Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
-            if ( Abc_Clock() > nTimeOut )
-                Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+            if ( pPars->nFailOuts == 0 )
+            {
+                Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
+                if ( nTimeOut && Abc_Clock() > nTimeOut )
+                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+                else
+                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            }
             else
-                Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
-        }
-    }
-    else // if ( RetValue == 0 )
-    {
-        if ( !pPars->fSolveAll )
-        {
-            Abc_Cex_t * pCex = pNtk->pSeqModel;
-            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+            {
+                Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
+                if ( Abc_Clock() > nTimeOut )
+                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+                else
+                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            }
         }
-        else
+        else // if ( RetValue == 0 )
         {
-            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 );
-            else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
-                Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
+            if ( !pPars->fSolveAll )
+            {
+                Abc_Cex_t * pCex = pNtk->pSeqModel;
+                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+            }
             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, ".   " );
+                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 );
+                else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
+                    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, ".   " );
+                }
             }
-            if ( pNtk->vSeqModelVec )
-                Vec_PtrFreeFree( pNtk->vSeqModelVec );
-            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
+        ABC_PRT( "Time", Abc_Clock() - clk );
+    }
+    if ( RetValue == 0 && pPars->fSolveAll )
+    {
+        if ( pNtk->vSeqModelVec )
+            Vec_PtrFreeFree( pNtk->vSeqModelVec );
+        pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
     }
-    ABC_PRT( "Time", Abc_Clock() - clk );
     if ( pNtk->pSeqModel ) 
     {
         status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index 57bd91bf..cd65fc67 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -101,6 +101,7 @@ struct Ssw_RarPars_t_
     int              fSetLastState;
     int              fVerbose;
     int              fNotVerbose;
+    int              fSilent;
     int              fDropSatOuts;
     int              fMiter;
     int              fUseCex;
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index e5640f6a..cd93d28b 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1051,16 +1051,22 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
             // check timeout
             if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
             {
+                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, "Reached timeout (%d sec).\n",  pPars->TimeOut );
+                }
                 goto finish;
             }
             if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
             {
+                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, "Reached gap timeout (%d sec).\n",  pPars->TimeOutGap );
+                }
                 goto finish;
             }
             // check if all outputs are solved by now
@@ -1106,15 +1112,21 @@ 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 )
     {
+        if ( !pPars->fSilent )
+        {
         if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
         Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        }
     }
     // cleanup
     Ssw_RarManStop( p );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 65c24e93..ff1e005b 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
     int         nLearnedPerce;  // ratio of learned clause limit
     int         fVerbose;       // verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
+    int         fSilent;        // completely silent
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
     int         nDropOuts;      // the number of dropped outputs
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ed8f089a..ea08c1e4 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1397,7 +1397,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             }
             if ( nTimeToStop && Abc_Clock() > nTimeToStop )
             {
-                Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
+                if ( !pPars->fSilent )
+                    Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 goto finish;
             }
             // skip solved outputs
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index e567e92b..82d18fde 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -8,4 +8,5 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcCexMin2.c \
     src/sat/bmc/bmcCexTools.c \
     src/sat/bmc/bmcLoad.c \
+    src/sat/bmc/bmcMulti.c \
     src/sat/bmc/bmcUnroll.c