Adding resource limit switch -C to 'sop'.

20 files changed, 73 insertions, 57 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bf84226b..18e7b9f6 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -654,14 +654,14 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraigRestore();
 extern ABC_DLL void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit );
 extern ABC_DLL void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
 extern ABC_DLL void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
 extern ABC_DLL Gia_Man_t *        Abc_NtkAigToGia( Abc_Ntk_t * p );
 extern ABC_DLL int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
-extern ABC_DLL int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit );
 extern ABC_DLL int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkToAig( Abc_Ntk_t * pNtk );
 /*=== abcHaig.c ==========================================================*/
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index dc8a1c5e..e100f570 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -356,7 +356,7 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
 {
     extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk );
     Abc_Obj_t * pNode;
@@ -366,18 +366,21 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     Vec_Str_t * vCube;
     int i, fMode, nCubes;
 
-    // collect all BDDs into one array
-    Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
-    assert( !Cudd_ReorderingStatus(dd, &nCubes) );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( !Abc_ObjIsBarBuf(pNode) )
-            Vec_PtrPush( vFuncs, pNode->pData );
-    // estimate the number of cubes in the ISOPs
-    nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, ABC_MAX_CUBES );
-    Vec_PtrFree( vFuncs );
-    if ( nCubes == -1 )
-        return 0;
-    //printf( "The total number of cubes = %d.\n", nCubes );
+    if ( nCubeLimit < ABC_INFINITY )
+    {
+        // collect all BDDs into one array
+        Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
+        assert( !Cudd_ReorderingStatus(dd, &nCubes) );
+        Abc_NtkForEachNode( pNtk, pNode, i )
+            if ( !Abc_ObjIsBarBuf(pNode) )
+                Vec_PtrPush( vFuncs, pNode->pData );
+        // estimate the number of cubes in the ISOPs
+        nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, nCubeLimit );
+        Vec_PtrFree( vFuncs );
+        if ( nCubes == -1 )
+            return 0;
+        //printf( "The total number of cubes = %d.\n", nCubes );
+    }
 
     if ( fDirect )
         fMode = 1;
@@ -407,6 +410,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
             Vec_StrFree( vCube );
             return 0;
         }
+        assert( Abc_ObjFaninNum(pNode) == Abc_SopGetVarNum((char *)pNode->pNext) );
     }
     Vec_StrFree( vCube );
 
@@ -1134,7 +1138,7 @@ int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
+int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
 {
     assert( !Abc_NtkIsStrash(pNtk) );
     if ( Abc_NtkHasSop(pNtk) )
@@ -1143,17 +1147,17 @@ int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
             return 1;
         if ( !Abc_NtkSopToBdd(pNtk) )
             return 0;
-        return Abc_NtkBddToSop(pNtk, fDirect);
+        return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
     }
     if ( Abc_NtkHasMapping(pNtk) )
         return Abc_NtkMapToSop(pNtk);
     if ( Abc_NtkHasBdd(pNtk) )
-        return Abc_NtkBddToSop(pNtk, fDirect);
+        return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
     if ( Abc_NtkHasAig(pNtk) )
     {
         if ( !Abc_NtkAigToBdd(pNtk) )
             return 0;
-        return Abc_NtkBddToSop(pNtk, fDirect);
+        return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
     }
     assert( 0 );
     return 0;
@@ -1214,7 +1218,7 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
     }
     if ( Abc_NtkHasBdd(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk,0) )
+        if ( !Abc_NtkBddToSop(pNtk,0, ABC_INFINITY) )
             return 0;
         return Abc_NtkSopToAig(pNtk);
     }
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 57bec593..fb48bb80 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -446,7 +446,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
             iState |= (1 << i);
     }
     // transfer logic to SOPs
-    Abc_NtkToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
     // create new network
     pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc );
     nStates = (1 << nFlops);
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 75bcfa03..70740657 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -740,7 +740,7 @@ int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose )
     Abc_NtkCleanup( pNtk, 0 );
 
     // convert network to SOPs
-    if ( !Abc_NtkToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
     {
         fprintf( stdout, "Converting to SOP has failed.\n" );
         return 0;
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index a1136ef7..c452b70c 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -209,7 +209,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse )
     // convert to logic SOP
     pNtk = Abc_NtkDup( pNtk0 );
     if ( Abc_NtkIsLogic(pNtk) && !Abc_NtkHasMapping(pNtk) )
-        Abc_NtkToSop( pNtk, 0 );
+        Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
 
     // collect all nodes in the network
     vNodes = Vec_PtrAlloc( 100 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7367ac87..1b92b334 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7889,16 +7889,27 @@ usage:
 int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int fDirect;
+    int fDirect, nCubeLimit = 1000000;
     int c;
 
     // set defaults
     fDirect = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cdh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCubeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCubeLimit < 0 )
+                goto usage;
+            break;
         case 'd':
             fDirect ^= 1;
             break;
@@ -7918,7 +7929,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Converting to SOP is possible only for logic networks.\n" );
         return 1;
     }
-    if ( !Abc_NtkToSop(pNtk, fDirect) )
+    if ( !Abc_NtkToSop(pNtk, fDirect, nCubeLimit) )
     {
         Abc_Print( -1, "Converting to SOP has failed.\n" );
         return 1;
@@ -7926,8 +7937,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sop [-dh]\n" );
+    Abc_Print( -2, "usage: sop [-C num] [-dh]\n" );
     Abc_Print( -2, "\t         converts node functions to SOP\n" );
+    Abc_Print( -2, "\t-C num : the limit on the total cube count of all nodes [default = %d]\n", nCubeLimit );
     Abc_Print( -2, "\t-d     : toggles using both phases or only positive [default = %s]\n", fDirect? "direct": "both" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -17226,7 +17238,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the network in the SOP form
-    if ( !Abc_NtkToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
     {
         Abc_Print( -1, "Converting to SOPs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index db795c60..b3618cfc 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -199,7 +199,7 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1
 
     Abc_NtkSweep( pNtk, 0 );
     Abc_NtkCleanupSeq( pNtk, 0, 0, 0 );
-    Abc_NtkToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
     Abc_NtkCycleInitStateSop( pNtk, 50, 0 );
     return pNtk;
 }
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index 2e78ad3f..42ed2806 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -58,7 +58,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
         Abc_NtkMapToSop(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Abc_NtkEspresso(): Converting to SOPs has failed.\n" );
             return;
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 64318ea0..942f8c6d 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -91,7 +91,7 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 //        Abc_NtkBddToSop(pNtk);
     }
     // get the network in the SOP form
-    if ( !Abc_NtkToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
     {
         printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index fd4f7d1c..bc1a6090 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -88,7 +88,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
             return NULL;
@@ -634,7 +634,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             Vec_IntFree( vInit );
             printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index c01c6f2b..46c8dec1 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -561,7 +561,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
     pNtkNew  = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
-    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    if ( !Abc_NtkBddToSop( pNtkNew, 0, ABC_INFINITY ) )
     {
         printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
         return NULL;
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index ad55ce04..1c53a153 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -389,7 +389,7 @@ void Abc_NktMffcPrint( char * pFileName, Abc_Obj_t ** pNodes, int nNodes, Vec_Pt
     Abc_Obj_t * pObj, * pFanin;
     int i, k;
     // convert the network
-    Abc_NtkToSop( pNodes[0]->pNtk, 0 );
+    Abc_NtkToSop( pNodes[0]->pNtk, 0, ABC_INFINITY );
     // write the file
     pFile = fopen( pFileName, "wb" );
     fprintf( pFile, ".model %s_part\n", pNodes[0]->pNtk->pName );
@@ -430,7 +430,7 @@ void Abc_NktMffcPrintInt( char * pFileName, Abc_Ntk_t * pNtk, Vec_Int_t * vRoots
     Abc_Obj_t * pObj, * pFanin;
     int i, k;
     // convert the network
-    Abc_NtkToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
     // write the file
     pFile = fopen( pFileName, "wb" );
     fprintf( pFile, ".model %s_part\n", pNtk->pName );
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index aab18ed0..d2ac549e 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -55,11 +55,7 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->iTemp = i;
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
-    {
         pObj->iTemp = Abc_NtkCiNum(pNtk) + i;
-//printf( "%d->%d ", pObj->Id, pObj->iTemp );
-    }
-//printf( "\n" );
     Abc_NtkForEachCo( pNtk, pObj, i )
         pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + i;
     return vNodes;
@@ -265,7 +261,11 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
         return 0;
     }
     if ( !Abc_NtkHasSop(pNtk) )
-        Abc_NtkToSop( pNtk, 0 );
+        if ( !Abc_NtkToSop( pNtk, 0, ABC_INFINITY ) )
+        {
+            printf( "Conversion to SOP has failed due to low resource limit.\n" );
+            return 0;
+        }
     // collect information
     p = Abc_NtkExtractMfs( pNtk, pPars->nFirstFixed );
     // perform optimization
@@ -442,7 +442,7 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
         return 0;
     }
     if ( !Abc_NtkHasSop(p) )
-        Abc_NtkToSop( p, 0 );
+        Abc_NtkToSop( p, 0, ABC_INFINITY );
     // derive unfolded network
     pNtk = Abc_NtkUnrollAndDrop( p, nFrames, nFramesAdd, vFlops, &iPivot );
     Io_WriteBlifLogic( pNtk, "unroll_dump.blif", 0 );
@@ -466,7 +466,7 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
     // perform final sweep
     Abc_NtkSweep( p, 0 );
     if ( !Abc_NtkHasSop(p) )
-        Abc_NtkToSop( p, 0 );
+        Abc_NtkToSop( p, 0, ABC_INFINITY );
     return 1;
 
 }
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 361f1e99..af598ed8 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1119,7 +1119,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Abc_NtkPrintGates(): Converting to SOPs has failed.\n" );
             return;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 2a203c96..8145c256 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -337,7 +337,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    if ( !Abc_NtkBddToSop( pNtkNew, 0, ABC_INFINITY ) )
     {
         printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
         return NULL;
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 42274433..35e028c1 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1907,7 +1907,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkToSop(pNtk, 0);
+        Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
     pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
@@ -2049,7 +2049,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkToSop(pNtk, 0);
+        Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
     pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
@@ -2263,7 +2263,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkToSop(pNtk, 0);
+        Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
     pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 0f60bb7f..3446aafc 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -286,7 +286,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
             Abc_NtkDelete( pNtk );
             return NULL;
         }
-        if ( !Abc_NtkToSop(pNtk, 0) )
+        if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Io_ReadBenchNetwork(): Converting to SOP has failed.\n" );
             Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 7e7d1701..c0d2897f 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -367,7 +367,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( !Abc_NtkHasSop(pNtk) )
-            Abc_NtkToSop( pNtk, 0 );
+            Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
         Io_WriteBblif( pNtk, pFileName );
         return;
     }
@@ -396,7 +396,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             pNtkTemp = Abc_NtkToNetlist( pNtk );
             Abc_NtkDelete( pNtkCopy );
         }
-        if ( !Abc_NtkToSop( pNtkTemp, 1 ) )
+        if ( !Abc_NtkToSop( pNtkTemp, 1, ABC_INFINITY ) )
             return;
     }
     else if ( FileType == IO_FILE_MOPLA )
@@ -433,7 +433,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     if ( FileType == IO_FILE_BLIF )
     {
         if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
-            Abc_NtkToSop( pNtkTemp, 0 );
+            Abc_NtkToSop( pNtkTemp, 0, ABC_INFINITY );
         Io_WriteBlif( pNtkTemp, pFileName, 1, 0, 0 );
     }
     else if ( FileType == IO_FILE_BLIFMV )
@@ -568,12 +568,12 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
         {
             Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkResult->pDesign->vModules, pNtkTemp, i )
                 if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
-                    Abc_NtkToSop( pNtkTemp, 0 );
+                    Abc_NtkToSop( pNtkTemp, 0, ABC_INFINITY );
         }
         else
         {
             if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
-                Abc_NtkToSop( pNtkResult, 0 );
+                Abc_NtkToSop( pNtkResult, 0, ABC_INFINITY );
         }
         Io_WriteBlif( pNtkResult, pFileName, 1, 0, 0 );
     }
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 88544d9f..9dde2e58 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -1388,7 +1388,7 @@ void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct,
 {
     Abc_Ntk_t * pNtkTemp;
     assert( Abc_NtkIsLogic(pNtk) );
-    Abc_NtkToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
     // derive the netlist
     pNtkTemp = Abc_NtkToNetlist(pNtk);
     if ( pNtkTemp == NULL )
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 24f3da63..339efd8f 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -100,7 +100,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;
@@ -463,7 +463,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;