Version abc80212

3 files changed, 14 insertions, 5 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 64268358..2ee84f39 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
     int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
+    int              nLevelMax;         // the max level to consider seriously
     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
@@ -266,7 +267,7 @@ extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
 extern int                 Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
+extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
 /*=== fraHot.c ========================================================*/
 extern Vec_Int_t *         Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0157421b..0a81105b 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -303,6 +303,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
 //    Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew;
     int i, Pos = 0;
+    int nBTracksOld;
     // fraig latch outputs
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
     {
@@ -315,6 +316,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
     // fraig internal nodes
 //    if ( !p->pPars->fDontShowBar )
 //        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
+    nBTracksOld = p->pPars->nBTLimitNode;
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
 //        if ( pProgress )
@@ -327,7 +329,12 @@ void Fra_FraigSweep( Fra_Man_t * p )
         if ( p->pManFraig->pData )
             continue;
         // perform fraiging
+        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+            p->pPars->nBTLimitNode = 5;
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+            p->pPars->nBTLimitNode = nBTracksOld;
+        // check implications
         if ( p->pPars->fUseImps )
             Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
     }
@@ -382,7 +389,7 @@ clk = clock();
     // finalize the fraiged manager
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
-    {
+    { 
 int clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
@@ -419,7 +426,7 @@ p->timeTotal = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax )
 {
     Fra_Par_t Pars, * pPars = &Pars; 
     Fra_ParamsDefault( pPars );
@@ -430,6 +437,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
     pPars->fProve       = 0;
     pPars->fVerbose     = 0;
     pPars->fDontShowBar = 1;
+    pPars->nLevelMax    = nLevelMax;
     return Fra_FraigPerform( pManAig, pPars );
 }
  
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 3e0fca6a..a43d83b1 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -211,8 +211,8 @@ PRT( "Time", clock() - clk );
         } 
 
         // perform retiming
-//        if ( fRetimeFirst && pNew->nRegs )
-        if ( pNew->nRegs )
+        if ( fRetimeFirst && pNew->nRegs )
+//        if ( pNew->nRegs )
         {
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );