/**CFile****************************************************************
FileName [giaHcd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [New choice computation package.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaHcd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "aig/aig/aig.h"
#include "opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// choicing parameters
typedef struct Hcd_Pars_t_ Hcd_Pars_t;
struct Hcd_Pars_t_
{
int nWords; // the number of simulation words
int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables
int fSynthesis; // set to 1 to perform synthesis
int fPolarFlip; // uses polarity adjustment
int fSimulateTfo; // uses simulation of TFO classes
int fPower; // uses power-aware rewriting
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
int fVerbose; // verbose stats
clock_t timeSynth; // synthesis runtime
int nNodesAhead; // the lookahead in terms of nodes
int nCallsRecycle; // calls to perform before recycling SAT solver
};
extern void Gia_ComputeEquivalences( Gia_Man_t * pMiter, int nBTLimit, int fUseMiniSat, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManSetDefaultParams( Hcd_Pars_t * p )
{
memset( p, 0, sizeof(Hcd_Pars_t) );
p->nWords = 8; // the number of simulation words
p->nBTLimit = 1000; // conflict limit at a node
p->nSatVarMax = 5000; // the max number of SAT variables
p->fSynthesis = 1; // derives three snapshots
p->fPolarFlip = 1; // uses polarity adjustment
p->fSimulateTfo = 1; // simulate TFO
p->fPower = 0; // power-aware rewriting
p->fVerbose = 0; // verbose stats
p->nNodesAhead = 1000; // the lookahead in terms of nodes
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
}
/**Function*************************************************************
Synopsis [Reproduces script "compress".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Hcd_Compress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = fUpdateLevel;
pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fPower = fPower;
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
// pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
pParsRwr->fUseZeros = 1;
pParsRef->fUseZeros = 1;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
return pAig;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Hcd_Compress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = fUpdateLevel;
pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fFanout = fFanout;
pParsRwr->fPower = fPower;
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
// pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
// if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
pParsRwr->fUseZeros = 1;
pParsRef->fUseZeros = 1;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
return pAig;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Hcd_ChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
//alias resyn "b; rw; rwz; b; rwz; b"
//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
{
Vec_Ptr_t * vGias;
Gia_Man_t * pGia;
vGias = Vec_PtrAlloc( 3 );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
pAig = Hcd_Compress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );
pAig = Hcd_Compress2( pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );
Aig_ManStop( pAig );
return vGias;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
if ( Gia_ObjIsCo(pObj) )
return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Derives the miter of several AIGs for choice computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias )
{
Gia_Man_t * pNew, * pGia, * pGia0;
int i, k, iNode, nNodes;
// make sure they have equal parameters
assert( Vec_PtrSize(vGias) > 0 );
pGia0 = (Gia_Man_t *)Vec_PtrEntry( vGias, 0 );
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
{
assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
Gia_ManFillValue( pGia );
Gia_ManConst0(pGia)->Value = 0;
}
// start the new manager
pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
pNew->pName = Abc_UtilStrsav( pGia0->pName );
pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
// create new CIs and assign them to the old manager CIs
for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
{
iNode = Gia_ManAppendCi(pNew);
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
Gia_ManCi( pGia, k )->Value = iNode;
}
// create internal nodes
Gia_ManHashAlloc( pNew );
for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
{
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
Hcd_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
}
Gia_ManHashStop( pNew );
// check the presence of dangling nodes
nNodes = Gia_ManHasDangling( pNew );
assert( nNodes == 0 );
return pNew;
}
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNode.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
{
// check the trivial cases
if ( pNode == NULL )
return 0;
if ( Gia_ObjIsCi(pNode) )
return 0;
// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
// return 0;
if ( pNode == pOld )
return 1;
// skip the visited node
if ( pNode->fMark0 )
return 0;
pNode->fMark0 = 1;
Vec_PtrPush( vVisited, pNode );
// check the children
if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
return 1;
if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
return 1;
// check equivalent nodes
return Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
}
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNode.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
{
Vec_Ptr_t * vVisited;
Gia_Obj_t * pObj;
int RetValue, i;
assert( !Gia_IsComplement(pOld) );
assert( !Gia_IsComplement(pNode) );
vVisited = Vec_PtrAlloc( 100 );
RetValue = Hcd_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
pObj->fMark0 = 0;
Vec_PtrFree( vVisited );
return RetValue;
}
/**Function*************************************************************
Synopsis [Adds the next entry while making choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
{
if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
{
Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
return;
}
Hcd_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
if ( ~pObj->Value )
return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjIsConst0(pRepr) )
{
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
Hcd_ManEquivToChoices_rec( pNew, p, pRepr );
assert( Gia_ObjIsAnd(pObj) );
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
{
assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
return;
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
{
assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
{
assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Removes choices, which contain fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManRemoveBadChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iObj, iPrev, Counter = 0;
// mark nodes with fanout
Gia_ManForEachObj( p, pObj, i )
{
pObj->fMark0 = 0;
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark0 = 1;
}
else if ( Gia_ObjIsCo(pObj) )
Gia_ObjFanin0(pObj)->fMark0 = 1;
}
// go through the classes and remove
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
{
if ( !Gia_ManObj(p, iObj)->fMark0 )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
}
// remove the marks
Gia_ManCleanMark0( p );
// printf( "Removed %d bad choices.\n", Counter );
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
int i;
assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
pObj->Value = pRepr->Value;
}
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
if ( i % nSnapshots == 0 )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Hcd_ManRemoveBadChoices( pNew );
// Gia_ManEquivPrintClasses( pNew, 0, 0 );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
// Gia_ManEquivPrintClasses( pNew, 0, 0 );
return pNew;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose )
{
Vec_Ptr_t * vGias;
Gia_Man_t * pGia, * pMiter;
Aig_Man_t * pAigNew;
int i;
clock_t clk = clock();
// perform synthesis
if ( fSynthesis )
{
vGias = Hcd_ChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, 0, 0 );
if ( fVerbose )
ABC_PRT( "Synthesis time", clock() - clk );
// create choices
clk = clock();
pMiter = Hcd_ManChoiceMiter( vGias );
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
Gia_ManStop( pGia );
Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
}
else
{
vGias = Vec_PtrStart( 3 );
pMiter = Gia_ManFromAig(pAig);
}
// perform choicing
Gia_ComputeEquivalences( pMiter, nBTLimit, fUseMiniSat, fVerbose );
// derive AIG with choices
pGia = Hcd_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
Gia_ManSetRegNum( pGia, Aig_ManRegNum(pAig) );
Gia_ManStop( pMiter );
Vec_PtrFree( vGias );
if ( fVerbose )
ABC_PRT( "Choicing time", clock() - clk );
// Gia_ManHasChoices_very_old( pGia );
// transform back
pAigNew = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
if ( fVerbose )
{
extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
printf( "Choices : Reprs = %5d. Equivs = %5d. Choices = %5d.\n",
Dch_DeriveChoiceCountReprs( pAigNew ),
Dch_DeriveChoiceCountEquivs( pAigNew ),
Aig_ManChoiceNum( pAigNew ) );
}
return pAigNew;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ComputeChoicesTest( Gia_Man_t * pGia, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose )
{
Aig_Man_t * pAig, * pAigNew;
pAig = Gia_ManToAig( pGia, 0 );
pAigNew = Hcd_ComputeChoices( pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
Aig_ManStop( pAigNew );
Aig_ManStop( pAig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END