Version abc80515

2 files changed, 137 insertions, 44 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index f7ad40dd..7cb846fa 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -51,6 +51,7 @@ extern "C" {
 
 typedef struct Fra_Par_t_   Fra_Par_t;
 typedef struct Fra_Ssw_t_   Fra_Ssw_t;
+typedef struct Fra_Sec_t_   Fra_Sec_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
@@ -87,7 +88,7 @@ struct Fra_Par_t_
     int              fDontShowBar;      // does not show progressbar during fraiging
 };
 
-// seq SAT sweeping parametesr
+// seq SAT sweeping parameters
 struct Fra_Ssw_t_
 {
     int              nPartSize;         // size of the partition
@@ -107,6 +108,27 @@ struct Fra_Ssw_t_
     float            TimeLimit;         // the runtime budget for this call
 };
 
+// SEC parametesr
+struct Fra_Sec_t_
+{
+    int              fTryComb;          // try CEC call as a preprocessing step
+    int              fTryBmc;           // try BMC call as a preprocessing step 
+    int              nFramesMax;        // the max number of frames used for induction
+    int              fPhaseAbstract;    // enables phase abstraction
+    int              fRetimeFirst;      // enables most-forward retiming at the beginning
+    int              fRetimeRegs;       // enables min-register retiming at the beginning
+    int              fFraiging;         // enables fraiging at the beginning
+    int              fInterpolation;    // enables interpolation
+    int              fReachability;     // enables BDD based reachability
+    int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
+    int              fVerbose;          // enables verbose reporting of statistics
+    int              fVeryVerbose;      // enables very verbose reporting  
+    int              TimeLimit;         // enables the timeout
+    // internal parameters
+    int              fRecursive;        // set to 1 when SEC is called recursively
+    int              fReportSolution;   // enables report solution in a special form
+};
+
 // FRAIG equivalence classes
 struct Fra_Cla_t_
 {
@@ -329,7 +351,8 @@ extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig
 extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit );
+extern void                Fra_SecSetDefaultParams( Fra_Sec_t * p );
+extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index db8027d9..b8f93f57 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,12 +40,44 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit )
+void Fra_SecSetDefaultParams( Fra_Sec_t * p )
+{
+    memset( p, 0, sizeof(Fra_Sec_t) );
+    p->fTryComb          =   1;  // try CEC call as a preprocessing step
+    p->fTryBmc           =   1;  // try BMC call as a preprocessing step 
+    p->nFramesMax        =   2;  // the max number of frames used for induction
+    p->fPhaseAbstract    =   1;  // enables phase abstraction
+    p->fRetimeFirst      =   1;  // enables most-forward retiming at the beginning
+    p->fRetimeRegs       =   1;  // enables min-register retiming at the beginning
+    p->fFraiging         =   1;  // enables fraiging at the beginning
+    p->fInterpolation    =   1;  // enables interpolation
+    p->fReachability     =   1;  // enables BDD based reachability
+    p->fStopOnFirstFail  =   1;  // enables stopping after first output of a miter has failed to prove
+    p->fVerbose          =   0;  // enables verbose reporting of statistics
+    p->fVeryVerbose      =   0;  // enables very verbose reporting  
+    p->TimeLimit         =   0;  // enables the timeout
+    // internal parameters
+    p->fReportSolution   =   1;  // enables specialized format for reporting solution
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int TimeOut = 0;
     int fLatchCorr = 0;
     float TimeLeft = 0.0;
 
@@ -58,8 +90,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
     // prepare parameters
     memset( pPars, 0, sizeof(Fra_Ssw_t) );
     pPars->fLatchCorr  = fLatchCorr;
-    pPars->fVerbose = fVeryVerbose;
-    if ( fVerbose )
+    pPars->fVerbose = pParSec->fVeryVerbose;
+    if ( pParSec->fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -72,7 +104,7 @@ clk = clock();
     pNew = Aig_ManReduceLaches( pNew, 0 );
     if ( pNew->nRegs )
     pNew = Aig_ManConstReduce( pNew, 0 );
-    if ( fVerbose )
+    if ( pParSec->fVerbose )
     {
         printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -84,14 +116,14 @@ PRT( "Time", clock() - clk );
 
     // perform phase abstraction
 clk = clock();
-    if ( fPhaseAbstract )
+    if ( pParSec->fPhaseAbstract )
     {
         extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
         pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
         Aig_ManStop( pTemp );
-        if ( fVerbose )
+        if ( pParSec->fVerbose )
         {
             printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -100,12 +132,12 @@ PRT( "Time", clock() - clk );
     }
 
     // perform forward retiming
-    if ( fRetimeFirst && pNew->nRegs )
+    if ( pParSec->fRetimeFirst && pNew->nRegs )
     {
 clk = clock();
     pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
     Aig_ManStop( pTemp );
-    if ( fVerbose )
+    if ( pParSec->fVerbose )
     {
         printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -120,22 +152,24 @@ clk = clock();
     pNew = Aig_ManDupOrdered( pTemp = pNew );
 //    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
-    if ( RetValue == -1 && TimeLimit )
+    if ( RetValue == -1 && pParSec->TimeLimit )
     {
-        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
             printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
+            TimeOut = 1;
             goto finish;
         }
     }
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft );
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
     if ( pNew == NULL )
     {
         pNew = pTemp;
         RetValue = -1;
+        TimeOut = 1;
         goto finish;
     }
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
@@ -148,7 +182,7 @@ PRT( "Time", clock() - clkTotal );
         return RetValue;
     }
 
-    if ( fVerbose )
+    if ( pParSec->fVerbose )
     {
         printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
             nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -156,25 +190,26 @@ PRT( "Time", clock() - clk );
     }
     }
 
-    if ( RetValue == -1 && TimeLimit )
+    if ( RetValue == -1 && pParSec->TimeLimit )
     {
-        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
             printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
+            TimeOut = 1;
             goto finish;
         }
     }
 
     // perform fraiging
-    if ( fFraiging )
+    if ( pParSec->fFraiging )
     {
 clk = clock();
     pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
     Aig_ManStop( pTemp );
-    if ( fVerbose )
+    if ( pParSec->fVerbose )
     {
         printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -189,20 +224,21 @@ PRT( "Time", clock() - clk );
     if ( RetValue >= 0 )
         goto finish;
 
-    if ( RetValue == -1 && TimeLimit )
+    if ( RetValue == -1 && pParSec->TimeLimit )
     {
-        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
             printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
+            TimeOut = 1;
             goto finish;
         }
     }
 
     // perform min-area retiming
-    if ( fRetimeRegs && pNew->nRegs )
+    if ( pParSec->fRetimeRegs && pNew->nRegs )
     {
     extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
@@ -213,7 +249,7 @@ clk = clock();
     Aig_ManStop( pTemp );
     pNew = Aig_ManDupOrdered( pTemp = pNew );
     Aig_ManStop( pTemp );
-    if ( fVerbose )
+    if ( pParSec->fVerbose )
     {
     printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
         Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -224,16 +260,17 @@ PRT( "Time", clock() - clk );
     // perform seq sweeping while increasing the number of frames
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue == -1 )
-    for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
+    for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 )
     {
-        if ( RetValue == -1 && TimeLimit )
+        if ( RetValue == -1 && pParSec->TimeLimit )
         {
-            TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+            TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
             TimeLeft = AIG_MAX( TimeLeft, 0.0 );
             if ( TimeLeft == 0.0 )
             {
                 printf( "Runtime limit exceeded.\n" );
                 RetValue = -1;
+                TimeOut = 1;
                 goto finish;
             }
         }
@@ -246,11 +283,12 @@ clk = clock();
         {
             pNew = pTemp;
             RetValue = -1;
+            TimeOut = 1;
             goto finish;
         }
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
-        if ( fVerbose )
+        if ( pParSec->fVerbose )
         { 
             printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
                 nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -260,7 +298,7 @@ PRT( "Time", clock() - clk );
             break;
 
         // perform retiming
-//        if ( fRetimeFirst && pNew->nRegs )
+//        if ( pParSec->fRetimeFirst && pNew->nRegs )
         if ( pNew->nRegs )
         {
         extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
@@ -272,7 +310,7 @@ clk = clock();
         Aig_ManStop( pTemp );
         pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
-        if ( fVerbose )
+        if ( pParSec->fVerbose )
         {
             printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -290,7 +328,7 @@ clk = clock();
 //        pNew = Dar_ManRewriteDefault( pTemp = pNew );
         pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); 
         Aig_ManStop( pTemp );
-        if ( fVerbose )
+        if ( pParSec->fVerbose )
         {
             printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -302,7 +340,7 @@ PRT( "Time", clock() - clk );
         {
 clk = clock();
         pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 
-        if ( fVerbose )
+        if ( pParSec->fVerbose )
         {
             printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
@@ -327,14 +365,14 @@ PRT( "Time", clock() - clkTotal );
 
     // try interplation
 clk = clock();
-    if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
+    if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
         extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth );
-        if ( fVerbose )
+        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth );
+        if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
             printf( "Property proved using interpolation.  " );
@@ -349,7 +387,7 @@ PRT( "Time", clock() - clk );
     }
 
     // try reachability analysis
-    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 )
+    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
     {
         extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
@@ -371,14 +409,16 @@ PRT( "Time", clock() - clk );
         iCount = 0;
         for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
         {
+            int TimeLimitCopy = 0;
             // get the remaining time for this output
-            if ( TimeLimit )
+            if ( pParSec->TimeLimit )
             {
-                TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+                TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
                 TimeLeft = AIG_MAX( TimeLeft, 0.0 );
                 if ( TimeLeft == 0.0 )
                 {
                     printf( "Runtime limit exceeded.\n" );
+                    TimeOut = 1;
                     goto finish;
                 }
                 TimeLimit2 = 1 + (int)TimeLeft;
@@ -390,12 +430,23 @@ PRT( "Time", clock() - clk );
             iCount++;
             printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
             pNew2 = Aig_ManDupOneOutput( pNew, i );
-            RetValue2 = Fra_FraigSec( pNew2, nFramesMax, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit2 );
+            
+            TimeLimitCopy = pParSec->TimeLimit;
+            pParSec->TimeLimit = TimeLimit2;
+            pParSec->fRecursive = 1;
+            RetValue2 = Fra_FraigSec( pNew2, pParSec );
+            pParSec->fRecursive = 0;
+            pParSec->TimeLimit = TimeLimitCopy;
+
             Aig_ManStop( pNew2 );
             if ( RetValue2 == 0 )
                 goto finish;
             if ( RetValue2 == -1 )
+            {
                 fOneUnsolved = 1;
+                if ( pParSec->fStopOnFirstFail )
+                    break;
+            }
         }
         if ( fOneUnsolved )
             RetValue = -1;
@@ -410,23 +461,42 @@ finish:
     {
         printf( "Networks are equivalent.   " );
 PRT( "Time", clock() - clkTotal );
+        if ( pParSec->fReportSolution && !pParSec->fRecursive )
+        {
+        printf( "SOLUTION: PASS       " );
+PRT( "Time", clock() - clkTotal );
+        }
     }
     else if ( RetValue == 0 )
     {
         printf( "Networks are NOT EQUIVALENT.   " );
 PRT( "Time", clock() - clkTotal );
+        if ( pParSec->fReportSolution && !pParSec->fRecursive )
+        {
+        printf( "SOLUTION: FAIL       " );
+PRT( "Time", clock() - clkTotal );
+        }
     }
-    else
+    else 
     {
-        static int Counter = 1;
-        char pFileName[1000];
         printf( "Networks are UNDECIDED.   " );
 PRT( "Time", clock() - clkTotal );
-        sprintf( pFileName, "sm%03d.aig", Counter++ );
-        Ioa_WriteAiger( pNew, pFileName, 0, 0 );
-        printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+        if ( pParSec->fReportSolution && !pParSec->fRecursive )
+        {
+        printf( "SOLUTION: UNDECIDED  " );
+PRT( "Time", clock() - clkTotal );
+        }
+        if ( !TimeOut )
+        {
+            static int Counter = 1;
+            char pFileName[1000];
+            sprintf( pFileName, "sm%03d.aig", Counter++ );
+            Ioa_WriteAiger( pNew, pFileName, 0, 0 );
+            printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+        }
     }
-    Aig_ManStop( pNew );
+    if ( pNew )
+        Aig_ManStop( pNew );
     return RetValue;
 }