summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c13
-rw-r--r--src/base/abci/abcRefactor.c343
-rw-r--r--src/base/io/ioReadEqn.c7
3 files changed, 188 insertions, 175 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bf419016..b371c911 100644
--- a/src/base/abci/abc.c
+++ b/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;
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index af01dde7..4d0836f1 100644
--- a/src/base/abci/abcRefactor.c
+++ b/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 ///
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
index 999834d6..1e4f5d46 100644
--- a/src/base/io/ioReadEqn.c
+++ b/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 ///