Adding silent mode to &cec -m.

3 files changed, 41 insertions, 15 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 53838c76..67dd0e6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -30862,7 +30862,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
     Cec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -30900,6 +30900,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fDumpMiter ^= 1;
             break;
+        case 's':
+            pPars->fSilent ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -30918,12 +30921,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
                 return 1;
             }
+            if ( !pPars->fSilent )
             Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
             pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars );
         }
         else
         {
             Gia_Man_t * pTemp;
+            if ( !pPars->fSilent )
             Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
             pTemp = Gia_ManTransformToDual( pAbc->pGia );
             pAbc->Status = Cec_ManVerify( pTemp, pPars );
@@ -30982,7 +30987,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cec [-CT num] [-nmdavh]\n" );
+    Abc_Print( -2, "usage: &cec [-CT num] [-nmdasvh]\n" );
     Abc_Print( -2, "\t         new combinational equivalence checker\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
@@ -30990,6 +30995,7 @@ usage:
     Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
     Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
     Abc_Print( -2, "\t-a     : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
+    Abc_Print( -2, "\t-s     : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index d951954b..3fb5d0b0 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -123,6 +123,7 @@ struct Cec_ParCec_t_
     int              fUseSmartCnf;  // use smart CNF computation
     int              fRewriting;    // enables AIG rewriting
     int              fNaive;        // performs naive SAT-based checking
+    int              fSilent;       // print no messages
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the number of failed output
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 72377d8d..d6e8456d 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -68,7 +68,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal )
+int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal, int fSilent )
 {
 //    extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
     extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
@@ -83,13 +83,19 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
     // report the miter
     if ( RetValue == 1 )
     {
-        Abc_Print( 1, "Networks are equivalent.   " );
-        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        if ( !fSilent )
+        {
+            Abc_Print( 1, "Networks are equivalent.   " );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        }
     }
     else if ( RetValue == 0 )
     {
-        Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
-        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        if ( !fSilent )
+        {
+            Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        }
         if ( pMiterCec->pData == NULL )
             Abc_Print( 1, "Counter-example is not available.\n" );
         else
@@ -99,19 +105,20 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
                 Abc_Print( 1, "Counter-example verification has failed.\n" );
             else 
             {
-//                Aig_Obj_t * pObj = Aig_ManCo(pMiterCec, iOut);
-//                Aig_Obj_t * pFan = Aig_ObjFanin0(pObj);
-                Abc_Print( 1, "Primary output %d has failed", iOut );
-                if ( nOuts-1 >= 0 )
-                    Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 );
-                Abc_Print( 1, ".\n" );
+                if ( !fSilent )
+                {
+                    Abc_Print( 1, "Primary output %d has failed", iOut );
+                    if ( nOuts-1 >= 0 )
+                        Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 );
+                    Abc_Print( 1, ".\n" );
+                }
                 if ( piOutFail )
                     *piOutFail = iOut;
             }
             Cec_ManTransformPattern( pMiter, iOut, (int *)pMiterCec->pData );
         }
     }
-    else
+    else if ( !fSilent )
     {
         Abc_Print( 1, "Networks are UNDECIDED.   " );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
@@ -146,8 +153,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         // (for example, when they have the same driver but complemented)
         if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) )
         {
+            if ( !pPars->fSilent )
+            {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different phase).  ", i/2 );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             return 0;
@@ -158,8 +168,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         // drivers are different PIs
         if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 )
         {
+            if ( !pPars->fSilent )
+            {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different PIs).  ", i/2 );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             // if their compl attributes are the same - one should be complemented
@@ -171,8 +184,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) || 
              (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) )
         {
+            if ( !pPars->fSilent )
+            {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (PI vs. constant).  ", i/2 );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             // the compl attributes are the same - the PI should be complemented
@@ -186,8 +202,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
     }
     if ( Gia_ManAndNum(p) == 0 )
     {
+        if ( !pPars->fSilent )
+        {
         Abc_Print( 1, "Networks are equivalent.  " );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
         return 1;
     }
     return -1;
@@ -383,7 +402,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     if ( pPars->fVerbose )
         Abc_Print( 1, "Calling the old CEC engine.\n" );
     fflush( stdout );
-    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal );
+    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal, pPars->fSilent );
     p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
     if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
         Abc_Print( 1, "Counter-example simulation has failed.\n" );