Changing 'refactor' to work with truth tables.

src/base/abci/abc.c

@@ -5919,7 +5919,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseDcs      =  0;
     fVerbose     =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NClzdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nlzvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5979,6 +5979,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
         return 1;
     }
+    if ( nNodeSizeMax > 15 )
+    {
+        Abc_Print( -1, "The cone size cannot exceed 15.\n" );
+        return 1;
+    }
 
     if ( fUseDcs && nNodeSizeMax >= nConeSizeMax )
     {
@@ -5995,13 +6000,13 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: refactor [-NC <num>] [-lzdvh]\n" );
+    Abc_Print( -2, "usage: refactor [-N <num>] [-lzvh]\n" );
     Abc_Print( -2, "\t           performs technology-independent refactoring of the AIG\n" );
     Abc_Print( -2, "\t-N <num> : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );
-    Abc_Print( -2, "\t-C <num> : the max support of the containing cone [default = %d]\n", nConeSizeMax );
+//    Abc_Print( -2, "\t-C <num> : the max support of the containing cone [default = %d]\n", nConeSizeMax );
     Abc_Print( -2, "\t-l       : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
-    Abc_Print( -2, "\t-d       : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
+//    Abc_Print( -2, "\t-d       : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;

src/base/abci/abcRefactor.c

@@ -20,10 +20,7 @@
 
 #include "base/abc/abc.h"
 #include "bool/dec/dec.h"
-
-#ifdef ABC_USE_CUDD
-#include "bdd/extrab/extraBdd.h"
-#endif
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,8 +29,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef ABC_USE_CUDD
-
 typedef struct Abc_ManRef_t_   Abc_ManRef_t;
 struct Abc_ManRef_t_
 {
@@ -42,7 +37,9 @@ struct Abc_ManRef_t_
     int              nConeSizeMax;      // the limit on the size of the containing cone
     int              fVerbose;          // the verbosity flag
     // internal data structures
-    DdManager *      dd;                // the BDD manager
+    Vec_Ptr_t *      vVars;             // truth tables
+    Vec_Ptr_t *      vFuncs;            // functions
+    Vec_Int_t *      vMemory;           // memory
     Vec_Str_t *      vCube;             // temporary
     Vec_Int_t *      vForm;             // temporary
     Vec_Ptr_t *      vVisited;          // temporary
@@ -56,7 +53,7 @@ struct Abc_ManRef_t_
     int              nNodesEnd;
     // runtime statistics
     abctime          timeCut;
-    abctime          timeBdd;
+    abctime          timeTru;
     abctime          timeDcs;
     abctime          timeSop;
     abctime          timeFact;
@@ -65,11 +62,6 @@ struct Abc_ManRef_t_
     abctime          timeNtk;
     abctime          timeTotal;
 };
- 
-static void           Abc_NtkManRefPrintStats( Abc_ManRef_t * p );
-static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, int fUseDcs, int fVerbose );
-static void           Abc_NtkManRefStop( Abc_ManRef_t * p );
-static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -77,108 +69,74 @@ static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
 
 /**Function*************************************************************
 
-  Synopsis    [Performs incremental resynthesis of the AIG.]
+  Synopsis    [Returns function of the cone.]
 
-  Description [Starting from each node, computes a reconvergence-driven cut, 
-  derives BDD of the cut function, constructs ISOP, factors the ISOP, 
-  and replaces the current implementation of the MFFC of the node by the 
-  new factored form, if the number of AIG nodes is reduced and the total
-  number of levels of the AIG network is not increated. Returns the
-  number of AIG nodes saved.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
+word * Abc_NodeConeTruth( Vec_Ptr_t * vVars, Vec_Ptr_t * vFuncs, int nWordsMax, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
 {
-    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
-    ProgressBar * pProgress;
-    Abc_ManRef_t * pManRef;
-    Abc_ManCut_t * pManCut;
-    Dec_Graph_t * pFForm;
-    Vec_Ptr_t * vFanins;
     Abc_Obj_t * pNode;
-    abctime clk, clkStart = Abc_Clock();
-    int i, nNodes;
-
-    assert( Abc_NtkIsStrash(pNtk) );
-    // cleanup the AIG
-    Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
-    // start the managers
-    pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
-    pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
-    pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
-    // compute the reverse levels if level update is requested
-    if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk, 0 );
-
-    // resynthesize each node once
-    pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
-    nNodes = Abc_NtkObjNumMax(pNtk);
-    pProgress = Extra_ProgressBarStart( stdout, nNodes );
-    Abc_NtkForEachNode( pNtk, pNode, i )
+    word * pTruth0, * pTruth1, * pTruth = NULL;
+    int i, k, nWords = Abc_Truth6WordNum( Vec_PtrSize(vLeaves) );
+    // get nodes in the cut without fanins in the DFS order
+    Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
+    // set elementary functions
+    Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)Vec_PtrEntry( vVars, i );
+    // prepare functions
+    for ( i = Vec_PtrSize(vFuncs); i < Vec_PtrSize(vVisited); i++ )
+        Vec_PtrPush( vFuncs, ABC_ALLOC(word, nWordsMax) );
+    // compute functions for the collected nodes
+    Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // skip the constant node
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        // skip persistant nodes
-        if ( Abc_NodeIsPersistant(pNode) )
-            continue;
-        // skip the nodes with many fanouts
-        if ( Abc_ObjFanoutNum(pNode) > 1000 )
-            continue;
-        // stop if all nodes have been tried once
-        if ( i >= nNodes )
-            break;
-        // compute a reconvergence-driven cut
-clk = Abc_Clock();
-        vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
-pManRef->timeCut += Abc_Clock() - clk;
-        // evaluate this cut
-clk = Abc_Clock();
-        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
-pManRef->timeRes += Abc_Clock() - clk;
-        if ( pFForm == NULL )
-            continue;
-        // acceptable replacement found, update the graph
-clk = Abc_Clock();
-        Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
-pManRef->timeNtk += Abc_Clock() - clk;
-        Dec_GraphFree( pFForm );
-//    {
-//        extern int s_TotalChanges;
-//        s_TotalChanges++;
-//    }
-    }
-    Extra_ProgressBarStop( pProgress );
-pManRef->timeTotal = Abc_Clock() - clkStart;
-    pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
-
-    // print statistics of the manager
-    if ( fVerbose )
-        Abc_NtkManRefPrintStats( pManRef );
-    // delete the managers
-    Abc_NtkManCutStop( pManCut );
-    Abc_NtkManRefStop( pManRef );
-    // put the nodes into the DFS order and reassign their IDs
-    Abc_NtkReassignIds( pNtk );
-//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
-    // fix the levels
-    if ( fUpdateLevel )
-        Abc_NtkStopReverseLevels( pNtk );
-    else
-        Abc_NtkLevel( pNtk );
-    // check
-    if ( !Abc_NtkCheck( pNtk ) )
-    {
-        printf( "Abc_NtkRefactor: The network check has failed.\n" );
-        return 0;
+        assert( !Abc_ObjIsPi(pNode) );
+        pTruth0 = (word *)Abc_ObjFanin0(pNode)->pCopy;
+        pTruth1 = (word *)Abc_ObjFanin1(pNode)->pCopy;
+        pTruth  = (word *)Vec_PtrEntry( vFuncs, i );
+        if ( Abc_ObjFaninC0(pNode) )
+        {
+            if ( Abc_ObjFaninC1(pNode) )
+                for ( k = 0; k < nWords; k++ )
+                    pTruth[k] = ~pTruth0[k] & ~pTruth1[k];
+            else
+                for ( k = 0; k < nWords; k++ )
+                    pTruth[k] = ~pTruth0[k] &  pTruth1[k];
+        }
+        else
+        {
+            if ( Abc_ObjFaninC1(pNode) )
+                for ( k = 0; k < nWords; k++ )
+                    pTruth[k] =  pTruth0[k] & ~pTruth1[k];
+            else
+                for ( k = 0; k < nWords; k++ )
+                    pTruth[k] =  pTruth0[k] &  pTruth1[k];
+        }
+        pNode->pCopy = (Abc_Obj_t *)pTruth;
     }
+    return pTruth;
+}
+int Abc_NodeConeIsConst0( word * pTruth, int nVars )
+{
+    int k, nWords = Abc_Truth6WordNum( nVars );
+    for ( k = 0; k < nWords; k++ )
+        if ( pTruth[k] )
+            return 0;
     return 1;
 }
+int Abc_NodeConeIsConst1( word * pTruth, int nVars )
+{
+    int k, nWords = Abc_Truth6WordNum( nVars );
+    for ( k = 0; k < nWords; k++ )
+        if ( ~pTruth[k] )
+            return 0;
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -193,72 +151,37 @@ pManRef->timeTotal = Abc_Clock() - clkStart;
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
 {
-    extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
-    extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
-    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
     extern int    Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
     int fVeryVerbose = 0;
-    Abc_Obj_t * pFanin;
+    int nVars = Vec_PtrSize(vFanins);
+    int nWordsMax = Abc_Truth6WordNum(p->nNodeSizeMax);
     Dec_Graph_t * pFForm;
-    DdNode * bNodeFunc;
-    int nNodesSaved, nNodesAdded, i;
+    Abc_Obj_t * pFanin;
+    word * pTruth;
     abctime clk;
-    char * pSop;
-    int Required;
-
-    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
+    int i, nNodesSaved, nNodesAdded, Required;
 
     p->nNodesConsidered++;
 
-    // get the function of the cut
-clk = Abc_Clock();
-    bNodeFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pNode, vFanins, p->vVisited );  Cudd_Ref( bNodeFunc );
-p->timeBdd += Abc_Clock() - clk;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
-    // if don't-care are used, transform the function into ISOP
-    if ( fUseDcs )
-    {
-        DdNode * bNodeDc, * bNodeOn, * bNodeOnDc;
-        int nMints, nMintsDc;
+    // get the function of the cut
 clk = Abc_Clock();
-        // get the don't-cares
-        bNodeDc = Abc_NodeConeDcs( p->dd, p->dd->vars + vFanins->nSize, p->dd->vars, p->vLeaves, vFanins, p->vVisited ); Cudd_Ref( bNodeDc );
-        nMints = (1 << vFanins->nSize);
-        nMintsDc = (int)Cudd_CountMinterm( p->dd, bNodeDc, vFanins->nSize );
-//        printf( "Percentage of minterms = %5.2f.\n", 100.0 * nMintsDc / nMints );
-        // get the ISF
-        bNodeOn   = Cudd_bddAnd( p->dd, bNodeFunc, Cudd_Not(bNodeDc) );   Cudd_Ref( bNodeOn );
-        bNodeOnDc = Cudd_bddOr ( p->dd, bNodeFunc, bNodeDc );             Cudd_Ref( bNodeOnDc );
-        Cudd_RecursiveDeref( p->dd, bNodeFunc );
-        Cudd_RecursiveDeref( p->dd, bNodeDc );
-        // get the ISOP
-        bNodeFunc = Cudd_bddIsop( p->dd, bNodeOn, bNodeOnDc );            Cudd_Ref( bNodeFunc );
-        Cudd_RecursiveDeref( p->dd, bNodeOn );
-        Cudd_RecursiveDeref( p->dd, bNodeOnDc );
-p->timeDcs += Abc_Clock() - clk;
-    }
+    pTruth = Abc_NodeConeTruth( p->vVars, p->vFuncs, nWordsMax, pNode, vFanins, p->vVisited );
+p->timeTru += Abc_Clock() - clk;
 
     // always accept the case of constant node
-    if ( Cudd_IsConstant(bNodeFunc) )
+    if ( Abc_NodeConeIsConst0(pTruth, nVars) || Abc_NodeConeIsConst1(pTruth, nVars) )
     {
         p->nLastGain = Abc_NodeMffcSize( pNode );
         p->nNodesGained += p->nLastGain;
         p->nNodesRefactored++;
-        Cudd_RecursiveDeref( p->dd, bNodeFunc );
-        if ( Cudd_IsComplement(bNodeFunc) )
-            return Dec_GraphCreateConst0();
-        return Dec_GraphCreateConst1();
+        return Abc_NodeConeIsConst0(pTruth, nVars) ? Dec_GraphCreateConst0() : Dec_GraphCreateConst1();
     }
 
-    // get the SOP of the cut
-clk = Abc_Clock();
-    pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, 0, p->vCube, -1 );
-p->timeSop += Abc_Clock() - clk;
-
     // get the factored form
 clk = Abc_Clock();
-    pFForm = Dec_Factor( pSop );
-    ABC_FREE( pSop );
+    pFForm = (Dec_Graph_t *)Kit_TruthToGraph( (unsigned *)pTruth, nVars, p->vMemory );
 p->timeFact += Abc_Clock() - clk;
 
     // mark the fanin boundary 
@@ -282,7 +205,6 @@ p->timeEval += Abc_Clock() - clk;
     // quit if there is no improvement
     if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) )
     {
-        Cudd_RecursiveDeref( p->dd, bNodeFunc );
         Dec_GraphFree( pFForm );
         return NULL;
     }
@@ -297,14 +219,12 @@ p->timeEval += Abc_Clock() - clk;
     {
         printf( "Node %6s : ",  Abc_ObjName(pNode) );
         printf( "Cone = %2d. ", vFanins->nSize );
-        printf( "BDD = %2d. ",  Cudd_DagSize(bNodeFunc) );
         printf( "FF = %2d. ",   1 + Dec_GraphNodeNum(pFForm) );
         printf( "MFFC = %2d. ", nNodesSaved );
         printf( "Add = %2d. ",  nNodesAdded );
         printf( "GAIN = %2d. ", p->nLastGain );
         printf( "\n" );
     }
-    Cudd_RecursiveDeref( p->dd, bNodeFunc );
     return pFForm;
 }
 
@@ -330,12 +250,9 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, int fUseD
     p->nNodeSizeMax = nNodeSizeMax;
     p->nConeSizeMax = nConeSizeMax;
     p->fVerbose     = fVerbose;
-    // start the BDD manager
-    if ( fUseDcs )
-        p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    else
-        p->dd = Cudd_Init( p->nNodeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_zddVarsFromBddVars( p->dd, 2 );
+    p->vVars        = Vec_PtrAllocTruthTables( Abc_MaxInt(nNodeSizeMax, 6) );
+    p->vFuncs       = Vec_PtrAlloc( 100 );
+    p->vMemory      = Vec_IntAlloc( 1 << 16 );
     return p;
 }
 
@@ -352,9 +269,11 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, int fUseD
 ***********************************************************************/
 void Abc_NtkManRefStop( Abc_ManRef_t * p )
 {
-    Extra_StopManager( p->dd );
+    Vec_PtrFreeFree( p->vFuncs );
+    Vec_PtrFree( p->vVars );
+    Vec_IntFree( p->vMemory );
     Vec_PtrFree( p->vVisited );
-    Vec_StrFree( p->vCube    );
+    Vec_StrFree( p->vCube );
     ABC_FREE( p );
 }
 
@@ -377,7 +296,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
     printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
     ABC_PRT( "Cuts       ", p->timeCut );
     ABC_PRT( "Resynthesis", p->timeRes );
-    ABC_PRT( "    BDD    ", p->timeBdd );
+    ABC_PRT( "    BDD    ", p->timeTru );
     ABC_PRT( "    DCs    ", p->timeDcs );
     ABC_PRT( "    SOP    ", p->timeSop );
     ABC_PRT( "    FF     ", p->timeFact );
@@ -386,11 +305,107 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
     ABC_PRT( "TOTAL      ", p->timeTotal );
 }
 
-#else
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental resynthesis of the AIG.]
+
+  Description [Starting from each node, computes a reconvergence-driven cut, 
+  derives BDD of the cut function, constructs ISOP, factors the ISOP, 
+  and replaces the current implementation of the MFFC of the node by the 
+  new factored form, if the number of AIG nodes is reduced and the total
+  number of levels of the AIG network is not increated. Returns the
+  number of AIG nodes saved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
+{
+    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+    ProgressBar * pProgress;
+    Abc_ManRef_t * pManRef;
+    Abc_ManCut_t * pManCut;
+    Dec_Graph_t * pFForm;
+    Vec_Ptr_t * vFanins;
+    Abc_Obj_t * pNode;
+    abctime clk, clkStart = Abc_Clock();
+    int i, nNodes;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // cleanup the AIG
+    Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
+    // start the managers
+    pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
+    pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
+    pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
+    // compute the reverse levels if level update is requested
+    if ( fUpdateLevel )
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
-int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) { return 1; }
+    // resynthesize each node once
+    pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // skip the constant node
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
+        // stop if all nodes have been tried once
+        if ( i >= nNodes )
+            break;
+        // compute a reconvergence-driven cut
+clk = Abc_Clock();
+        vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
+pManRef->timeCut += Abc_Clock() - clk;
+        // evaluate this cut
+clk = Abc_Clock();
+        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
+pManRef->timeRes += Abc_Clock() - clk;
+        if ( pFForm == NULL )
+            continue;
+        // acceptable replacement found, update the graph
+clk = Abc_Clock();
+        Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
+pManRef->timeNtk += Abc_Clock() - clk;
+        Dec_GraphFree( pFForm );
+    }
+    Extra_ProgressBarStop( pProgress );
+pManRef->timeTotal = Abc_Clock() - clkStart;
+    pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
+
+    // print statistics of the manager
+    if ( fVerbose )
+        Abc_NtkManRefPrintStats( pManRef );
+    // delete the managers
+    Abc_NtkManCutStop( pManCut );
+    Abc_NtkManRefStop( pManRef );
+    // put the nodes into the DFS order and reassign their IDs
+    Abc_NtkReassignIds( pNtk );
+//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
+    // fix the levels
+    if ( fUpdateLevel )
+        Abc_NtkStopReverseLevels( pNtk );
+    else
+        Abc_NtkLevel( pNtk );
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkRefactor: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
 
-#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/io/ioReadEqn.c

@@ -27,8 +27,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef ABC_USE_CUDD
-
 static Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p );
 static void        Io_ReadEqnStrCompact( char * pStr );
 static int         Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName );
@@ -235,11 +233,6 @@ void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t *
             Vec_PtrPush( vTokens, pToken );
 }
 
-#else
-
-Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ) { return NULL; }
-
-#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///