Version abc71218

7 files changed, 18 insertions, 13 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 8cd677d1..8d7116c7 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -76,6 +76,7 @@ struct Fra_Par_t_
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
     int              nMaxImps;          // the maximum number of implications to consider
+    int              nMaxLevs;          // the maximum number of levels to consider
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
@@ -245,7 +246,7 @@ extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
 extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
+extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
@@ -274,7 +275,7 @@ extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
 /*=== fraLcr.c ========================================================*/
 extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 962e7f7b..2d03e65d 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -270,7 +270,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
+void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
 {
     Aig_Obj_t ** ppTable, ** ppNexts;
     Aig_Obj_t * pObj, * pTemp;
@@ -296,8 +296,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
-//            if ( pObj->Level > 3 )
-//                continue;
+            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+                continue;
         }
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( pObj, nTableSize );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index dbc6401f..1c2140bb 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -282,12 +282,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
     pPars->nMaxImps   = nMaxImps;
+    pPars->nMaxLevs   = nMaxLevs;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
     pPars->fUseImps   = fUseImps;
     pPars->fWriteImps = fWriteImps;
-
+ 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
@@ -313,7 +314,7 @@ if ( fVerbose )
 {
 PRT( "Time", clock() - clk );
 }
-        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
 //        Fra_ClassesPostprocess( p->pCla );
         // allocate new simulation manager for simulating counter-examples
         Fra_SmlStop( p->pSml );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index daa789a8..a6460ed7 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -550,7 +550,7 @@ timeSim = clock() - clk2;
 
     // get preliminary info about equivalence classes
     pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
-    Fra_ClassesPrepare( p->pCla, 1 );
+    Fra_ClassesPrepare( p->pCla, 1, 0 );
     p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
     p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
     Fra_SmlStop( pTemp->pSml );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 17a7335c..4ccb48e3 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
@@ -185,7 +185,7 @@ PRT( "Time", clock() - clk );
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 3e8f2da1..1ad2d4f7 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -685,7 +685,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
     Fra_SmlSimulateOne( p->pSml );
     if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
         return;
-    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
 //    Fra_ClassesPrint( p->pCla, 0 );
 if ( fVerbose )
 printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index e7264fdc..ffaca75c 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,12 +1,15 @@
 SRC +=    src/aig/fra/fraBmc.c \
     src/aig/fra/fraCec.c \
     src/aig/fra/fraClass.c \
+    src/aig/fra/fraClau.c \
+    src/aig/fra/fraClaus.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \
     src/aig/fra/fraImp.c \
     src/aig/fra/fraInd.c \
     src/aig/fra/fraLcr.c \
     src/aig/fra/fraMan.c \
+    src/aig/fra/fraPart.c \
     src/aig/fra/fraSat.c \
     src/aig/fra/fraSec.c \
     src/aig/fra/fraSim.c