summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy/ivyRwrPre.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy/ivyRwrPre.c')
-rw-r--r--src/temp/ivy/ivyRwrPre.c597
1 files changed, 597 insertions, 0 deletions
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
new file mode 100644
index 00000000..243ab261
--- /dev/null
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+ FileName [ivyRwtPre.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Rewriting based on precomputation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+#include "deco.h"
+#include "rwt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums );
+static int Ivy_NodeMffcLabel( Ivy_Obj_t * pObj );
+static int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
+static Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut,
+ Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth );
+
+static int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+static void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs incremental rewriting of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose )
+{
+ Rwt_Man_t * pManRwt;
+ Ivy_Obj_t * pNode;
+ int i, nNodes, nGain;
+ int clk, clkStart = clock();
+ // start the rewriting manager
+ pManRwt = Rwt_ManStart( 0 );
+ if ( pManRwt == NULL )
+ return 0;
+ // compute the reverse levels if level update is requested
+ if ( fUpdateLevel )
+ Ivy_ManRequiredLevels( p );
+ // resynthesize each node once
+ nNodes = Ivy_ManObjIdNext( p );
+ Ivy_ManForEachObj( p, pNode, i )
+ {
+ if ( !Ivy_ObjIsNode(pNode) )
+ continue;
+ // fix the fanin buffer problem
+ Ivy_NodeFixBufferFanins( pNode );
+ if ( Ivy_ObjIsBuf(pNode) )
+ continue;
+ // stop if all nodes have been tried once
+ if ( i >= nNodes )
+ break;
+ // skip the nodes with many fanouts
+// if ( Ivy_ObjRefs(pNode) > 1000 )
+// continue;
+ // for each cut, try to resynthesize it
+ nGain = Rwt_NodeRewrite( pManRwt, pNode, fUpdateLevel, fUseZeroCost );
+ if ( nGain > 0 || nGain == 0 && fUseZeroCost )
+ {
+ Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
+ int fCompl = Rwt_ManReadCompl(pManRwt);
+/*
+ {
+ Ivy_Obj_t * pObj;
+ int i;
+ printf( "USING: (" );
+ Vec_PtrForEachEntry( Rwt_ManReadLeaves(pManRwt), pObj, i )
+ printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) );
+ printf( ") Gain = %d.\n", nGain );
+ }
+ if ( nGain > 0 )
+ { // print stats on the MFFC
+ extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode );
+ printf( "Node %6d : Gain = %4d ", pNode->Id, nGain );
+ Ivy_NodeMffsConeSuppPrint( pNode );
+ }
+*/
+ // complement the FF if needed
+clk = clock();
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+ Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+ }
+ }
+Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+ // print stats
+ if ( fVerbose )
+ Rwt_ManPrintStats( pManRwt );
+ // delete the managers
+ Rwt_ManStop( pManRwt );
+ // fix the levels
+ if ( fUpdateLevel )
+ Vec_IntFree( p->vRequired ), p->vRequired = NULL;
+ // check
+ if ( i = Ivy_ManCleanup(p) )
+ printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+ if ( !Ivy_ManCheck(p) )
+ printf( "Ivy_ManRewritePre(): The check has failed.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs rewriting for one node.]
+
+ Description [This procedure considers all the cuts computed for the node
+ and tries to rewrite each of them using the "forest" of different AIG
+ structures precomputed and stored in the RWR manager.
+ Determines the best rewriting and computes the gain in the number of AIG
+ nodes in the final network. In the end, p->vFanins contains information
+ about the best cut that can be used for rewriting, while p->pGraph gives
+ the decomposition dag (represented using decomposition graph data structure).
+ Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost )
+{
+ int fVeryVerbose = 0;
+ Dec_Graph_t * pGraph;
+ Ivy_Store_t * pStore;
+ Ivy_Cut_t * pCut;
+ Ivy_Obj_t * pFanin;
+ unsigned uPhase, uTruthBest, uTruth;
+ char * pPerm;
+ int Required, nNodesSaved, nNodesSaveCur;
+ int i, c, GainCur, GainBest = -1;
+ int clk, clk2;
+
+ p->nNodesConsidered++;
+ // get the required times
+ Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000;
+ // get the node's cuts
+clk = clock();
+ pStore = Ivy_NodeFindCutsAll( pNode, 5 );
+p->timeCut += clock() - clk;
+
+ // go through the cuts
+clk = clock();
+ for ( c = 1; c < pStore->nCuts; c++ )
+ {
+ pCut = pStore->pCuts + c;
+ // consider only 4-input cuts
+ if ( pCut->nSize != 4 )
+ continue;
+ // skip the cuts with buffers
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, pCut->pArray[i]) ) )
+ break;
+ if ( i != pCut->nSize )
+ continue;
+
+// if ( pNode->Id == 82 )
+// Ivy_NodePrintCut( pCut );
+
+ // get the fanin permutation
+clk2 = clock();
+ uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table
+p->timeTruth += clock() - clk2;
+ pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+ uPhase = p->pPhases[uTruth];
+ // collect fanins with the corresponding permutation/phase
+ Vec_PtrClear( p->vFaninsCur );
+ Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ {
+ pFanin = Ivy_ObjObj( pNode, pCut->pArray[pPerm[i]] );
+ assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) );
+ pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
+ Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
+ }
+clk2 = clock();
+/*
+ printf( "Considering: (" );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pFanin)) );
+ printf( ")\n" );
+*/
+ // mark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
+ // label MFFC with current ID
+ Ivy_ManIncrementTravId( Ivy_ObjMan(pNode) );
+ nNodesSaved = Ivy_NodeMffcLabel( pNode );
+ // unmark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+p->timeMffc += clock() - clk2;
+
+ // evaluate the cut
+clk2 = clock();
+ pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+p->timeEval += clock() - clk2;
+
+ // check if the cut is better than the current best one
+ if ( pGraph != NULL && GainBest < GainCur )
+ {
+ // save this form
+ nNodesSaveCur = nNodesSaved;
+ GainBest = GainCur;
+ p->pGraph = pGraph;
+ p->fCompl = ((uPhase & (1<<4)) > 0);
+ uTruthBest = uTruth;
+ // collect fanins in the
+ Vec_PtrClear( p->vFanins );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Vec_PtrPush( p->vFanins, pFanin );
+ }
+ }
+p->timeRes += clock() - clk;
+
+ if ( GainBest == -1 )
+ return -1;
+
+// printf( "%d", nNodesSaveCur - GainBest );
+/*
+ if ( GainBest > 0 )
+ {
+ if ( Rwt_CutIsintean( pNode, p->vFanins ) )
+ printf( "b" );
+ else
+ {
+ printf( "Node %d : ", pNode->Id );
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ printf( "%d ", Ivy_Regular(pFanin)->Id );
+ printf( "a" );
+ }
+ }
+*/
+/*
+ if ( GainBest > 0 )
+ if ( p->fCompl )
+ printf( "c" );
+ else
+ printf( "." );
+*/
+
+ // copy the leaves
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
+
+ p->nScores[p->pMap[uTruthBest]]++;
+ p->nNodesGained += GainBest;
+ if ( fUseZeroCost || GainBest > 0 )
+ p->nNodesRewritten++;
+
+ // report the progress
+ if ( fVeryVerbose && GainBest > 0 )
+ {
+ printf( "Node %6d : ", Ivy_ObjId(pNode) );
+ printf( "Fanins = %d. ", p->vFanins->nSize );
+ printf( "Save = %d. ", nNodesSaveCur );
+ printf( "Add = %d. ", nNodesSaveCur-GainBest );
+ printf( "GAIN = %d. ", GainBest );
+ printf( "Cone = %d. ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+ printf( "Class = %d. ", p->pMap[uTruthBest] );
+ printf( "\n" );
+ }
+ return GainBest;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [References/references the node and returns MFFC size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
+{
+ Ivy_Obj_t * pNode0, * pNode1;
+ int Counter;
+ // label visited nodes
+ if ( fLabel )
+ Ivy_ObjSetTravIdCurrent( pNode );
+ // skip the CI
+ if ( Ivy_ObjIsCi(pNode) )
+ return 0;
+ assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
+ // process the internal node
+ pNode0 = Ivy_ObjFanin0(pNode);
+ pNode1 = Ivy_ObjFanin1(pNode);
+ Counter = Ivy_ObjIsNode(pNode);
+ if ( fReference )
+ {
+ if ( pNode0->nRefs++ == 0 )
+ Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
+ if ( Ivy_ObjIsNode(pNode) && pNode1->nRefs++ == 0 )
+ Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+ }
+ else
+ {
+ assert( pNode0->nRefs > 0 );
+ assert( pNode1->nRefs > 0 );
+ if ( --pNode0->nRefs == 0 )
+ Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
+ if ( Ivy_ObjIsNode(pNode) && --pNode1->nRefs == 0 )
+ Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the size of MFFC and labels nodes with the current TravId.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeMffcLabel( Ivy_Obj_t * pNode )
+{
+ int nConeSize1, nConeSize2;
+ assert( !Ivy_IsComplement( pNode ) );
+ assert( Ivy_ObjIsNode( pNode ) );
+ nConeSize1 = Ivy_NodeRefDeref( pNode, 0, 1 ); // dereference
+ nConeSize2 = Ivy_NodeRefDeref( pNode, 1, 0 ); // reference
+ assert( nConeSize1 == nConeSize2 );
+ assert( nConeSize1 > 0 );
+ return nConeSize1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth_rec( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+ static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ unsigned uTruth0, uTruth1;
+ int i;
+ for ( i = 0; i < nNums; i++ )
+ if ( pObj->Id == pNums[i] )
+ return uMasks[i];
+ assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+ uTruth0 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin0(pObj), pNums, nNums );
+ if ( Ivy_ObjFaninC0(pObj) )
+ uTruth0 = ~uTruth0;
+ if ( Ivy_ObjIsBuf(pObj) )
+ return uTruth0;
+ uTruth1 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin1(pObj), pNums, nNums );
+ if ( Ivy_ObjFaninC1(pObj) )
+ uTruth1 = ~uTruth1;
+ return uTruth0 & uTruth1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+ assert( nNums < 6 );
+ return Ivy_NodeGetTruth_rec( pObj, pNums, nNums );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
+{
+ Vec_Ptr_t * vSubgraphs;
+ Dec_Graph_t * pGraphBest, * pGraphCur;
+ Rwt_Node_t * pNode, * pFanin;
+ int nNodesAdded, GainBest, i, k;
+ // find the matching class of subgraphs
+ vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+ p->nSubgraphs += vSubgraphs->nSize;
+ // determine the best subgraph
+ GainBest = -1;
+ Vec_PtrForEachEntry( vSubgraphs, pNode, i )
+ {
+ // get the current graph
+ pGraphCur = (Dec_Graph_t *)pNode->pNext;
+ // copy the leaves
+ Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+ Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
+ // detect how many unlabeled nodes will be reused
+ nNodesAdded = Ivy_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax );
+ if ( nNodesAdded == -1 )
+ continue;
+ assert( nNodesSaved >= nNodesAdded );
+ // count the gain at this node
+ if ( GainBest < nNodesSaved - nNodesAdded )
+ {
+ GainBest = nNodesSaved - nNodesAdded;
+ pGraphBest = pGraphCur;
+ }
+ }
+ if ( GainBest == -1 )
+ return NULL;
+ *pGainBest = GainBest;
+ return pGraphBest;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of new nodes added when using this graph.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.
+ Returns -1 if the number of nodes and levels exceeded the given limit or
+ the number of levels exceeded the maximum allowed level.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+ Dec_Node_t * pNode, * pNode0, * pNode1;
+ Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
+ int i, Counter, LevelNew, LevelOld;
+ // check for constant function or a literal
+ if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+ return 0;
+ // set the levels of the leaves
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->Level = Ivy_Regular(pNode->pFunc)->Level;
+ // compute the AIG size after adding the internal nodes
+ Counter = 0;
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+ pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
+ pAnd = Ivy_TableLookup( Ivy_ObjCreateGhost(pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
+ // return -1 if the node is the same as the original root
+ if ( Ivy_Regular(pAnd) == pRoot )
+ return -1;
+ }
+ else
+ pAnd = NULL;
+ // count the number of added nodes
+ if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) )
+ {
+ if ( ++Counter > NodeMax )
+ return -1;
+ }
+ // count the number of new levels
+ LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level );
+ if ( pAnd )
+ {
+ if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) )
+ LevelNew = 0;
+ else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) )
+ LevelNew = (int)Ivy_Regular(pAnd0)->Level;
+ else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd1) )
+ LevelNew = (int)Ivy_Regular(pAnd1)->Level;
+ LevelOld = (int)Ivy_Regular(pAnd)->Level;
+// assert( LevelNew == LevelOld );
+ }
+ if ( LevelNew > LevelMax )
+ return -1;
+ pNode->pFunc = pAnd;
+ pNode->Level = LevelNew;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Ivy_Obj_t * pAnd0, * pAnd1;
+ Dec_Node_t * pNode;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Replaces MFFC of the node by the new factored form.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
+{
+ Ivy_Obj_t * pRootNew;
+ int nNodesNew, nNodesOld;
+ nNodesOld = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+ // create the new structure of nodes
+ pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph );
+ // remove the old nodes
+// Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel );
+ Ivy_ObjReplace( pRoot, pRootNew, 1, 0 );
+ // compare the gains
+ nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+ assert( nGain <= nNodesOld - nNodesNew );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+