Added new command &gla_shrink.

4 files changed, 31 insertions, 25 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index ec33b3eb..e7cdea90 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -147,7 +147,7 @@ extern int               Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlop
 extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
 /*=== saigBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index 51033dee..90efef26 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -72,7 +72,7 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
 ***********************************************************************/
 Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
 { 
-    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
     Vec_Int_t * vFlopsNew;
     int i, Entry, RetValue;
     *piRetValue = -1;
@@ -119,7 +119,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     }
     else 
     {
-        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames );
+        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 );
     }
     if ( pAbs->pSeqModel == NULL )
         return NULL;
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index a1dee6e4..f70a0015 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -754,7 +754,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames )
+int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
 {
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
@@ -817,7 +817,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         // check the timeout
         if ( nTimeOut && clock() > nTimeToStop )
         {
-            printf( "Reached timeout (%d seconds).\n",  nTimeOut );
+            if ( !fSilent )
+                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
             if ( piFrames )
                 *piFrames = p->iFrameLast-1;
             Saig_BmcManStop( p );
@@ -827,15 +828,17 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     if ( RetValue == l_True )
     {
         assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
-            p->iOutputFail, p->iFrameFail );
+        if ( !fSilent )
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
+                p->iOutputFail, p->iFrameFail );
         Status = 0;
         if ( piFrames )
             *piFrames = p->iFrameFail;
     }
     else // if ( RetValue == l_False || RetValue == l_Undef )
     {
-        printf( "No output was asserted in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
+        if ( !fSilent )
+            printf( "No output was asserted in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
         if ( piFrames )
         {
             if ( p->iOutputLast > 0 )
@@ -844,24 +847,27 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
                 *piFrames = p->iFramePrev;
         }
     }
-    if ( fVerbOverwrite )
+    if ( !fSilent )
     {
-        ABC_PRTr( "Time", clock() - clk );
-    }
-    else
-    {
-        ABC_PRT( "Time", clock() - clk );
-    }
-    if ( RetValue != l_True )
-    {
-        if ( p->iFrameLast >= p->nFramesMax )
-            printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-        else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
-            printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else if ( nTimeOut && clock() > nTimeToStop )
-            printf( "Reached timeout (%d seconds).\n", nTimeOut );
+        if ( fVerbOverwrite )
+        {
+            ABC_PRTr( "Time", clock() - clk );
+        }
         else
-            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        {
+            ABC_PRT( "Time", clock() - clk );
+        }
+        if ( RetValue != l_True )
+        {
+            if ( p->iFrameLast >= p->nFramesMax )
+                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+            else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
+                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
+            else if ( nTimeOut && clock() > nTimeToStop )
+                printf( "Reached timeout (%d seconds).\n", nTimeOut );
+            else
+                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        }
     }
     Saig_BmcManStop( p );
     fflush( stdout );
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index c8c33680..040df1f9 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -222,7 +222,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
     // run BMC2
     if ( fUseBmc )
     {
-        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 );
         if ( RetValue == 0 )
         {
             Vec_IntFreeP( &vTransSigs );