Version abc80910

4 files changed, 12 insertions, 48 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 6721634e..91689196 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -283,8 +283,8 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 
 /*=== fraCec.c ========================================================*/
 extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
-extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
+extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
+extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
 extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 9046d574..fdf87ccd 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -157,11 +157,11 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
+int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 {
-    int nBTLimitStart =     300;  // starting SAT run
-    int nBTLimitFirst =       2;  // first fraiging iteration
-    int nBTLimitLast  = 1000000;  // the last-gasp SAT run
+    int nBTLimitStart =        300;   // starting SAT run
+    int nBTLimitFirst =          2;   // first fraiging iteration
+    int nBTLimitLast  = nConfLimit;   // the last-gasp SAT run
 
     Fra_Par_t Params, * pParams = &Params;
     Aig_Man_t * pAig = *ppAig, * pTemp;
@@ -270,7 +270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
 {
     Aig_Man_t * pAig;
     Vec_Ptr_t * vParts;
@@ -294,7 +294,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
             continue;
         if ( RetValue == 0 )
             break;
-        RetValue = Fra_FraigCec( &pAig, 0 );
+        RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
         Vec_PtrWriteEntry( vParts, i, pAig );
         if ( RetValue == 1 )
             continue;
@@ -361,9 +361,9 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
 
     if ( nPartSize )
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
     else // no partitioning
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ce9ec69b..f7674f7d 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -233,42 +233,6 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
     free( pLatches );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Divides a large partition into several ones.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigInductionPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
-{
-    Vec_Int_t * vPart;
-    int i, Counter;
-    assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
-    if ( nOverSize >= nPartSize )
-    {
-        printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
-        printf( "Adjusting it to be equal to half of the partition size.\n" );
-        nOverSize = nPartSize/2;
-    }
-    assert( nOverSize < nPartSize );
-    for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
-    {
-        vPart = Vec_IntAlloc( nPartSize );
-        for ( i = 0; i < nPartSize; i++, Counter++ )
-            if ( Counter < Vec_IntSize(vDomain) )
-                Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
-        if ( Vec_IntSize(vPart) <= nOverSize )
-            Vec_IntFree(vPart);
-        else
-            Vec_PtrPush( vResult, vPart );
-    }
-}
-
 
 /**Function*************************************************************
 
@@ -304,7 +268,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
         Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
         {
             if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
-                Fra_FraigInductionPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
             else
                 Vec_PtrPush( vResult, Vec_IntDup(vPart) );
         }
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 5944cf56..b8f767df 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -230,7 +230,7 @@ PRT( "Time", clock() - clk );
     }
 
     if ( pNew->nRegs == 0 )
-        RetValue = Fra_FraigCec( &pNew, 0 );
+        RetValue = Fra_FraigCec( &pNew, 100000, 0 );
 
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue >= 0 )