Version abc80511_2

6 files changed, 120 insertions, 12 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7311d414..f7ad40dd 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -104,6 +104,7 @@ struct Fra_Ssw_t_
     int              fUse1Hot;          // use one-hotness constraints
     int              fVerbose;          // enable verbose output 
     int              nIters;            // the number of iterations performed
+    float            TimeLimit;         // the runtime budget for this call
 };
 
 // FRAIG equivalence classes
@@ -312,7 +313,7 @@ extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars
 /*=== fraIndVer.c =====================================================*/
 extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
 /*=== fraLcr.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -328,7 +329,7 @@ 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 );
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit );
 /*=== 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/fraInd.c b/src/aig/fra/fraInd.c
index b29fa946..99b62856 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -336,9 +336,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
-    Aig_Man_t * pManAigNew;
+    Aig_Man_t * pManAigNew = NULL;
     int nNodesBeg, nRegsBeg;
     int nIter, i, clk = clock(), clk2;
+    int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC);
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
@@ -419,6 +420,12 @@ PRT( "Time", clock() - clk );
     if ( pPars->fUseImps )
         p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
 
+    if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+    {
+        printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+        goto finish;
+    }
+
     // perform BMC (for the min number of frames)
     Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
 //Fra_ClassesPrint( p->pCla, 1 );
@@ -442,6 +449,13 @@ PRT( "Time", clock() - clk );
         int nLitsOld = Fra_ClassesCountLits(p->pCla);
         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
+
+        if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+        {
+            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+            goto finish;
+        }
+
         // mark the classes as non-refined
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
@@ -592,6 +606,7 @@ p->timeTotal = clock() - clk;
     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
     // free the manager
+finish:
     Fra_ManStop( p );
     // check the output
 //    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 145bafae..0f5cc207 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -526,7 +526,7 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit )
 {
     int nPartSize    = 200;
     int fReprSelect  = 0;
@@ -536,6 +536,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Aig_Man_t * pAigPart, * pAigNew = NULL;
     Vec_Int_t * vPart;
     int i, nIter, timeSim, clk = clock(), clk2, clk3;
+    int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -609,6 +610,15 @@ p->timePart += clock() - clk2;
         Vec_PtrClear( p->vFraigs );
         Vec_PtrForEachEntry( p->vParts, vPart, i )
         {
+            if ( TimeLimit != 0.0 && clock() > TimeToStop )
+            {
+                Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+                    Aig_ManStop( pAigPart );
+                Aig_ManCleanMarkA( pAig );
+                Aig_ManCleanMarkB( pAig );
+                printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
+                goto finish;
+            }
 clk2 = clock();
             pAigPart = Fra_LcrCreatePart( p, vPart );
 p->timeTrav += clock() - clk2;
@@ -649,7 +659,6 @@ clk2 = clock();
 p->timePart += clock() - clk2;
         }
     }
-    free( pTemp );
     p->nIters = nIter;
 
     // move the classes into representatives and reduce AIG
@@ -667,6 +676,8 @@ p->timeTotal = clock() - clk;
     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
     p->nNodesEnd = Aig_ManNodeNum(pAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pAigNew);
+finish:
+    free( pTemp );
     Lcr_ManFree( p );
     if ( pnIter ) *pnIter = nIter;
     return pAigNew;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 9a500680..5146344c 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,13 +40,14 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit )
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+    float TimeLeft = 0.0;
 
     // try the miter before solving
     pNew = Aig_ManDup( p );
@@ -119,7 +120,24 @@ clk = clock();
     pNew = Aig_ManDupOrdered( pTemp = pNew );
 //    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)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;
+            goto finish;
+        }
+    }
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft );
+    if ( pNew == NULL )
+    {
+        pNew = pTemp;
+        RetValue = -1;
+        goto finish;
+    }
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
     Aig_ManStop( pTemp );
     if ( pNew == NULL )
@@ -138,6 +156,18 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)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;
+            goto finish;
+        }
+    }
+
     // perform fraiging
     if ( fFraiging )
     {
@@ -159,6 +189,18 @@ PRT( "Time", clock() - clk );
     if ( RetValue >= 0 )
         goto finish;
 
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)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;
+            goto finish;
+        }
+    }
+
     // perform min-area retiming
     if ( fRetimeRegs && pNew->nRegs )
     {
@@ -184,9 +226,28 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
+        if ( TimeLimit )
+        {
+            TimeLeft = (float)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;
+                goto finish;
+            }
+        }
+
 clk = clock();
         pPars->nFramesK = nFrames;
+        pPars->TimeLimit = TimeLeft;
         pNew = Fra_FraigInduction( pTemp = pNew, pPars );
+        if ( pNew == NULL )
+        {
+            pNew = pTemp;
+            RetValue = -1;
+            goto finish;
+        }
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
@@ -264,11 +325,33 @@ PRT( "Time", clock() - clkTotal );
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
 
+    // try interplation
+clk = clock();
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
+    {
+        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, 10000, 0, 1, 0, &Depth );
+        if ( fVerbose )
+        {
+        if ( RetValue == 1 )
+            printf( "Property proved using interpolation.  " );
+        else if ( RetValue == 0 )
+            printf( "Property DISPROVED with cex at depth %d using interpolation.  ", Depth );
+        else if ( RetValue == -1 )
+            printf( "Property UNDECIDED after interpolation.  " );
+        else
+            assert( 0 ); 
+PRT( "Time", clock() - clk );
+        }
+    }
+
     // try reachability analysis
-    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 )
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 )
     {
         extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
-        assert( Aig_ManRegNum(pNew) > 0 );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index a723c981..1b135212 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -347,7 +347,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
 
     // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
-    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
 
     // finalize the transformation
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index ffd32206..c3bb0875 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -519,8 +519,6 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTrans
         p->pAigTrans = Saig_ManTransformed( pAig );
     else
         p->pAigTrans = Saig_ManDuplicated( pAig );
-//    p->pAigTrans = Dar_ManRwsat( pAigTemp = p->pAigTrans, 1, 0 );
-//    Aig_ManStop( pAigTemp );
     // derive CNF for the transformed AIG
 clk = clock();
     p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) );