luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Unifying representation of mapping in GIA.

This commit is contained in:
Alan Mishchenko 2013-06-25 23:05:51 -07:00
parent 0985491dce
commit a66dc0afb6
18 changed files with 365 additions and 463 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -3503,10 +3503,6 @@ SOURCE=.\src\aig\gia\giaCex.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaChoice.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCof.c
# End Source File
# Begin Source File

21
src/aig/gia/gia.h
View File

@ -127,9 +127,8 @@ struct Gia_Man_t_
int nFansAlloc; // the size of fanout representation
Vec_Int_t * vFanoutNums; // static fanout
Vec_Int_t * vFanout; // static fanout
int * pMapping; // mapping for each node
int nOffset; // mapping offset
Vec_Int_t * vMapping;
Vec_Int_t * vMapping; // mapping for each node
Vec_Int_t * vPacking; // packing information
Vec_Int_t * vLutConfigs; // LUT configurations
Abc_Cex_t * pCexComb; // combinational counter-example
Abc_Cex_t * pCexSeq; // sequential counter-example
@ -144,7 +143,6 @@ struct Gia_Man_t_
Gia_Man_t * pAigExtra; // combinational logic of holes
Vec_Flt_t * vInArrs; // PI arrival times
Vec_Flt_t * vOutReqs; // PO required times
Vec_Int_t * vPacking; // packing information
int * pTravIds; // separate traversal ID representation
int nTravIdsAlloc; // the number of trav IDs allocated
Vec_Ptr_t * vNamesIn; // the input names
@ -310,7 +308,7 @@ static inline int Gia_ManMuxNum( Gia_Man_t * p ) { return p->nMuxe
static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); }
static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; }
static inline void Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1; }
static inline int Gia_ManWithChoices( Gia_Man_t * p ) { return p->pSibls != NULL; }
static inline int Gia_ManHasChoices( Gia_Man_t * p ) { return p->pSibls != NULL; }
static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; }
static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); }
@ -791,9 +789,10 @@ static inline void Gia_ObjSetFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int
#define Gia_ObjForEachFanoutStatic( p, pObj, pFanout, i ) \
for ( i = 0; (i < Gia_ObjFanoutNum(p, pObj)) && (((pFanout) = Gia_ObjFanout(p, pObj, i)), 1); i++ )
static inline int Gia_ObjIsLut( Gia_Man_t * p, int Id ) { return p->pMapping[Id] != 0; }
static inline int Gia_ObjLutSize( Gia_Man_t * p, int Id ) { return p->pMapping[p->pMapping[Id]]; }
static inline int * Gia_ObjLutFanins( Gia_Man_t * p, int Id ) { return p->pMapping + p->pMapping[Id] + 1; }
static inline int Gia_ManHasMapping( Gia_Man_t * p ) { return p->vMapping != NULL; }
static inline int Gia_ObjIsLut( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vMapping, Id) != 0; }
static inline int Gia_ObjLutSize( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vMapping, Vec_IntEntry(p->vMapping, Id)); }
static inline int * Gia_ObjLutFanins( Gia_Man_t * p, int Id ) { return Vec_IntEntryP(p->vMapping, Vec_IntEntry(p->vMapping, Id)) + 1; }
static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { return Gia_ObjLutFanins(p, Id)[i]; }
#define Gia_ManForEachLut( p, i ) \
@ -870,11 +869,6 @@ extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
extern Abc_Cex_t * Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex );
extern Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex );
/*=== giaChoice.c ============================================================*/
extern void Gia_ManVerifyChoices( Gia_Man_t * p );
extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
extern int Gia_ManHasChoices( Gia_Man_t * p );
extern int Gia_ManChoiceLevel( Gia_Man_t * p );
/*=== giaCsatOld.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/
@ -1170,7 +1164,6 @@ extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p );
extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );

15
src/aig/gia/giaAiger.c
View File

@ -612,17 +612,12 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
{
extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
extern int * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs, int * pOffset );
int nSize, nOffset;
extern Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs );
int nSize;
pCur++;
nSize = Gia_AigerReadInt(pCur);
pCurTemp = pCur + nSize + 4; pCur += 4;
// pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) );
// pNew->pMapping = Gia_AigerReadMappingSimple( &pCur, nSize );
// pNew->nOffset = nSize / 4;
// pCur += nSize;
pNew->pMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew), &nOffset );
pNew->nOffset = nOffset;
pNew->vMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew) );
assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
}
@ -786,6 +781,8 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
ABC_FREE( pInit );
}
Vec_IntFreeP( &vInits );
if ( !fSkipStrash && pNew->vMapping )
Abc_Print( 0, "Structural hashing enabled while reading AIGER may have invalidated the mapping. Consider using \"&r -s\".\n" );
return pNew;
}
@ -1218,7 +1215,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
}
// write mapping
if ( p->pMapping )
if ( Gia_ManHasMapping(p) )
{
extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p );

26
src/aig/gia/giaAigerExt.c
View File

@ -171,7 +171,7 @@ unsigned char * Gia_AigerWriteMappingInt( Gia_Man_t * p, int * pMapSize )
{
unsigned char * pBuffer;
int i, k, iPrev, iFan, nItems, iPos = 4;
assert( p->pMapping );
assert( Gia_ManHasMapping(p) );
// count the number of entries to be written
nItems = 0;
Gia_ManForEachLut( p, i )
@ -225,10 +225,10 @@ int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize )
}
Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p )
{
unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*p->nOffset );
memcpy( pBuffer, p->pMapping, 4*p->nOffset );
assert( p->pMapping != NULL && p->nOffset >= Gia_ManObjNum(p) );
return Vec_StrAllocArray( (char *)pBuffer, 4*p->nOffset );
unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*Vec_IntSize(p->vMapping) );
memcpy( pBuffer, Vec_IntArray(p->vMapping), 4*Vec_IntSize(p->vMapping) );
assert( Vec_IntSize(p->vMapping) >= Gia_ManObjNum(p) );
return Vec_StrAllocArray( (char *)pBuffer, 4*Vec_IntSize(p->vMapping) );
}
/**Function*************************************************************
@ -242,27 +242,27 @@ Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs, int * pOffset )
Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs )
{
int * pMapping, nLuts, LutSize, iRoot, nFanins, i, k;
int * pMapping, nLuts, LutSize, iRoot, nFanins, i, k, nOffset;
nLuts = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
LutSize = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
pMapping = ABC_CALLOC( int, nObjs + (LutSize + 2) * nLuts );
*pOffset = nObjs;
nOffset = nObjs;
for ( i = 0; i < nLuts; i++ )
{
iRoot = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
nFanins = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
pMapping[iRoot] = *pOffset;
pMapping[iRoot] = nOffset;
// write one
pMapping[ (*pOffset)++ ] = nFanins;
pMapping[ nOffset++ ] = nFanins;
for ( k = 0; k < nFanins; k++ )
{
pMapping[ (*pOffset)++ ] = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
pMapping[ nOffset++ ] = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
}
pMapping[ (*pOffset)++ ] = iRoot;
pMapping[ nOffset++ ] = iRoot;
}
return pMapping;
return Vec_IntAllocArray( pMapping, nOffset );
}
Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p )
{

373
src/aig/gia/giaChoice.c
View File

@ -1,373 +0,0 @@
/**CFile****************************************************************
FileName [giaChoice.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Normalization of structural choices.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reverse the order of nodes in equiv classes.]
Description [If the flag is 1, assumed current increasing order ]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
{
Vec_Int_t * vCollected;
Vec_Int_t * vClass;
int i, k, iRepr, iNode, iPrev;
// collect classes
vCollected = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, iRepr )
Vec_IntPush( vCollected, iRepr );
// correct each class
vClass = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vCollected, iRepr, i )
{
Vec_IntClear( vClass );
Vec_IntPush( vClass, iRepr );
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( fNowIncreasing )
assert( iRepr < iNode );
else
assert( iRepr > iNode );
Vec_IntPush( vClass, iNode );
}
// if ( !fNowIncreasing )
// Vec_IntSort( vClass, 1 );
// reverse the class
iPrev = 0;
iRepr = Vec_IntEntryLast( vClass );
Vec_IntForEachEntry( vClass, iNode, k )
{
if ( fNowIncreasing )
Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
else
Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
Gia_ObjSetNext( p, iNode, iPrev );
iPrev = iNode;
}
}
Vec_IntFree( vCollected );
Vec_IntFree( vClass );
// verify
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
if ( fNowIncreasing )
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
else
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManVerifyChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iRepr, iNode, fProb = 0;
assert( p->pReprs );
// mark nodes
Gia_ManCleanMark0(p);
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( Gia_ObjIsHead(p, iNode) )
printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
Gia_ManObj( p, iNode )->fMark0 = 1;
}
Gia_ManCleanMark0(p);
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
}
else if ( Gia_ObjIsCo(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
}
}
// if ( !fProb )
// printf( "GIA with choices is correct.\n" );
}
/**Function*************************************************************
Synopsis [Make sure reprsentative nodes do not have representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckReprs( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, fProb = 0;
Gia_ManForEachObj( p, pObj, i )
{
if ( !Gia_ObjHasRepr(p, i) )
continue;
if ( !Gia_ObjIsAnd(pObj) )
printf( "Obj %d is not an AND but it has a repr %d.\n", i, Gia_ObjRepr(p, i) ), fProb = 1;
else if ( Gia_ObjHasRepr( p, Gia_ObjRepr(p, i) ) )
printf( "Obj %d has repr %d with a repr %d.\n", i, Gia_ObjRepr(p, i), Gia_ObjRepr(p, Gia_ObjRepr(p, i)) ), fProb = 1;
}
if ( !fProb )
printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) );
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter1 = 0, Counter2 = 0;
int nFailNoRepr = 0;
int nFailHaveRepr = 0;
int nChoiceNodes = 0;
int nChoices = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
// check if there are any representatives
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter1++;
}
// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
// Counter2++;
}
// printf( "\n" );
Gia_ManForEachObj( p, pObj, i )
{
// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
// Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter2++;
}
}
// printf( "\n" );
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
printf( "%d nodes have reprs.\n", Counter1 );
printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjRefNum(p, pObj) == 0 )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
nFailNoRepr++;
else
nChoices++;
}
else
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
nFailHaveRepr++;
if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
nChoiceNodes++;
}
if ( Gia_ObjReprObj( p, i ) )
assert( Gia_ObjRepr(p, i) < i );
}
if ( nChoices == 0 )
return 0;
if ( nFailNoRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
// return 0;
}
if ( nFailHaveRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
// return 0;
}
// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
return 1;
}
/**Function*************************************************************
Synopsis [Computes levels for AIG with choices and white boxes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
Gia_Obj_t * pNext;
int i, iBox, iTerm1, nTerms, LevelMax = 0;
if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
return;
Gia_ObjSetTravIdCurrent( p, pObj );
if ( Gia_ObjIsCi(pObj) )
{
if ( pManTime )
{
iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
if ( iBox >= 0 ) // this is not a true PI
{
iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
{
pNext = Gia_ManCo( p, iTerm1 + i );
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
LevelMax++;
}
}
// Abc_Print( 1, "%d ", pObj->Level );
}
else if ( Gia_ObjIsCo(pObj) )
{
pNext = Gia_ObjFanin0(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
else if ( Gia_ObjIsAnd(pObj) )
{
// get the maximum level of the two fanins
pNext = Gia_ObjFanin0(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
pNext = Gia_ObjFanin1(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
LevelMax++;
// get the level of the nodes in the choice node
if ( p->pSibls && (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
Gia_ObjSetLevel( p, pObj, LevelMax );
}
int Gia_ManChoiceLevel( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, LevelMax = 0;
// assert( Gia_ManRegNum(p) == 0 );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
{
Gia_ManChoiceLevel_rec( p, pObj );
if ( LevelMax < Gia_ObjLevel(p, pObj) )
LevelMax = Gia_ObjLevel(p, pObj);
}
// account for dangling boxes
Gia_ManForEachCi( p, pObj, i )
{
Gia_ManChoiceLevel_rec( p, pObj );
if ( LevelMax < Gia_ObjLevel(p, pObj) )
LevelMax = Gia_ObjLevel(p, pObj);
// Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
}
// Abc_Print( 1, "\n" );
Gia_ManForEachAnd( p, pObj, i )
assert( Gia_ObjLevel(p, pObj) > 0 );
// printf( "Max level %d\n", LevelMax );
return LevelMax;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

2
src/aig/gia/giaHcd.c
View File

@ -642,7 +642,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
Vec_PtrFree( vGias );
if ( fVerbose )
ABC_PRT( "Choicing time", clock() - clk );
Gia_ManHasChoices( pGia );
// Gia_ManHasChoices_very_old( pGia );
// transform back
pAigNew = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );

151
src/aig/gia/giaIf.c
View File

@ -215,7 +215,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
{
int * pLevels;
int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
if ( !p->pMapping )
if ( !Gia_ManHasMapping(p) )
return;
pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachLut( p, i )
@ -285,6 +285,107 @@ void Gia_ManPrintPackingStats( Gia_Man_t * p )
}
/**Function*************************************************************
Synopsis [Computes levels for AIG with choices and white boxes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
Gia_Obj_t * pNext;
int i, iBox, iTerm1, nTerms, LevelMax = 0;
if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
return;
Gia_ObjSetTravIdCurrent( p, pObj );
if ( Gia_ObjIsCi(pObj) )
{
if ( pManTime )
{
iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
if ( iBox >= 0 ) // this is not a true PI
{
iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
{
pNext = Gia_ManCo( p, iTerm1 + i );
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
LevelMax++;
}
}
// Abc_Print( 1, "%d ", pObj->Level );
}
else if ( Gia_ObjIsCo(pObj) )
{
pNext = Gia_ObjFanin0(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
else if ( Gia_ObjIsAnd(pObj) )
{
// get the maximum level of the two fanins
pNext = Gia_ObjFanin0(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
pNext = Gia_ObjFanin1(pObj);
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
LevelMax++;
// get the level of the nodes in the choice node
if ( (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManChoiceLevel_rec( p, pNext );
if ( LevelMax < Gia_ObjLevel(p, pNext) )
LevelMax = Gia_ObjLevel(p, pNext);
}
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
Gia_ObjSetLevel( p, pObj, LevelMax );
}
int Gia_ManChoiceLevel( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, LevelMax = 0;
// assert( Gia_ManRegNum(p) == 0 );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
{
Gia_ManChoiceLevel_rec( p, pObj );
if ( LevelMax < Gia_ObjLevel(p, pObj) )
LevelMax = Gia_ObjLevel(p, pObj);
}
// account for dangling boxes
Gia_ManForEachCi( p, pObj, i )
{
Gia_ManChoiceLevel_rec( p, pObj );
if ( LevelMax < Gia_ObjLevel(p, pObj) )
LevelMax = Gia_ObjLevel(p, pObj);
// Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
}
// Abc_Print( 1, "\n" );
Gia_ManForEachAnd( p, pObj, i )
assert( Gia_ObjLevel(p, pObj) > 0 );
// printf( "Max level %d\n", LevelMax );
return LevelMax;
}
/**Function*************************************************************
@ -606,9 +707,16 @@ int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec
// derive truth table
if ( Kit_TruthIsConst0((unsigned *)pRes, nLeaves) || Kit_TruthIsConst1((unsigned *)pRes, nLeaves) )
{
assert( 0 );
// fprintf( pFile, ".names %s\n %d\n", Abc_ObjName(Abc_ObjFanout0(pObj)), Kit_TruthIsConst1((unsigned *)pRes, nLeaves) );
return -1;
iObjLit1 = Abc_LitNotCond( 0, Kit_TruthIsConst1((unsigned *)pRes, nLeaves) );
// write mapping
if ( Vec_IntEntry(vMapping, 0) == 0 )
{
Vec_IntSetEntry( vMapping, 0, Vec_IntSize(vMapping2) );
Vec_IntPush( vMapping2, 0 );
Vec_IntPush( vMapping2, 0 );
}
return iObjLit1;
}
// perform decomposition
@ -928,18 +1036,15 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Vec_IntAppend( vMapping, vMapping2 );
Vec_IntFree( vMapping2 );
// attach mapping and packing
pNew->nOffset = Vec_IntSize(vMapping);
pNew->pMapping = Vec_IntReleaseArray(vMapping);
assert( pNew->vMapping == NULL );
assert( pNew->vPacking == NULL );
pNew->vMapping = vMapping;
pNew->vPacking = vPacking;
Vec_IntFree( vMapping );
// verify that COs have mapping
{
Gia_Obj_t * pObj;
Gia_ManForEachCo( pNew, pObj, i )
{
if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
}
assert( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || Gia_ObjIsLut(pNew, Gia_ObjFaninId0p(pNew, pObj)) );
}
return pNew;
}
@ -979,17 +1084,7 @@ void Gia_ManMappingVerify( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pFanin;
int i, Result = 1;
/*
if ( p->pMapping )
{
assert( p->nOffset != 0 );
Vec_IntFreeP( p->vMapping );
Vec_IntAlloc( p->vMapping, p->nOffset );
memmove( Vec_IntArray(p->vMapping), p->pMapping, p->nOffset );
}
assert( p->vMapping );
*/
assert( p->pMapping );
assert( Gia_ManHasMapping(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
{
@ -1024,7 +1119,7 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, k, iFan;
if ( pGia->pMapping == NULL )
if ( !Gia_ManHasMapping(pGia) )
return;
Gia_ManMappingVerify( pGia );
Vec_IntFreeP( &p->vMapping );
@ -1040,12 +1135,6 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) );
Vec_IntPush( p->vMapping, Gia_ObjId(p, pObj) );
}
// create standard mapping
assert( p->pMapping == NULL );
p->pMapping = Vec_IntArray( p->vMapping );
p->vMapping->pArray = NULL;
p->nOffset = Vec_IntSize(p->vMapping);
p->vMapping->nSize = 0;
Gia_ManMappingVerify( p );
}
@ -1112,9 +1201,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
Gia_Man_t * pNew;
If_Man_t * pIfMan;
If_Par_t * pPars = (If_Par_t *)pp;
// disable cut minimization
if ( !(pPars->fDelayOpt || pPars->fUserRecLib) && !pPars->fDeriveLuts )//&& Gia_ManWithChoices(p) )
pPars->fCutMin = 0; // not compatible with deriving result
// disable cut minimization when GIA strucure is needed
if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
pPars->fCutMin = 0;
// reconstruct GIA according to the hierarchy manager
assert( pPars->pTimesArr == NULL );
assert( pPars->pTimesReq == NULL );

6
src/aig/gia/giaMan.c
View File

@ -111,7 +111,7 @@ void Gia_ManStop( Gia_Man_t * p )
ABC_FREE( p->pCexSeq );
ABC_FREE( p->pCexComb );
ABC_FREE( p->pIso );
ABC_FREE( p->pMapping );
// ABC_FREE( p->pMapping );
ABC_FREE( p->pFanData );
ABC_FREE( p->pReprsOld );
ABC_FREE( p->pReprs );
@ -337,7 +337,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut )
Gia_ManEquivPrintClasses( p, 0, 0.0 );
if ( p->pSibls )
Gia_ManPrintChoiceStats( p );
if ( p->pMapping )
if ( Gia_ManHasMapping(p) )
Gia_ManPrintMappingStats( p );
if ( p->vPacking )
Gia_ManPrintPackingStats( p );
@ -498,7 +498,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
int * pLutClass, ClassCounts[222] = {0};
int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
unsigned * pTruth;
assert( p->pMapping != NULL );
assert( Gia_ManHasMapping(p) );
assert( Gia_ManLutSizeMax( p ) <= 4 );
vLeaves = Vec_IntAlloc( 100 );
vVisited = Vec_IntAlloc( 100 );

2
src/aig/gia/giaShrink.c
View File

@ -56,7 +56,7 @@ Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose )
abctime clk = Abc_Clock();
// int ClassCounts[222] = {0};
int * pLutClass, Counter = 0;
assert( p->pMapping != NULL );
assert( Gia_ManHasMapping(p) );
if ( Gia_ManLutSizeMax( p ) > 4 )
{
printf( "Resynthesis is not performed when nodes have more than 4 inputs.\n" );

2
src/aig/gia/giaShrink6.c
View File

@ -404,7 +404,7 @@ Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, in
int RetValue, Counter1 = 0, Counter2 = 0;
abctime clk2, clk = Abc_Clock();
abctime timeFanout = 0;
assert( p->pMapping != NULL );
assert( Gia_ManHasMapping(p) );
pMan = Shr_ManAlloc( p );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;

2
src/aig/gia/giaSpeedup.c
View File

@ -635,7 +635,7 @@ Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerb
int fUseLutLib = (p->pLutLib != NULL);
void * pTempTim = NULL;
unsigned * puTCEdges;
assert( p->pMapping != NULL );
assert( Gia_ManHasMapping(p) );
if ( !fUseLutLib && p->pManTime )
{
pTempTim = p->pManTime;

92
src/aig/gia/giaUtil.c
View File

@ -1443,6 +1443,98 @@ Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p )
return vFans;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasChoices_very_old( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter1 = 0, Counter2 = 0;
int nFailNoRepr = 0;
int nFailHaveRepr = 0;
int nChoiceNodes = 0;
int nChoices = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
// check if there are any representatives
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter1++;
}
// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
// Counter2++;
}
// printf( "\n" );
Gia_ManForEachObj( p, pObj, i )
{
// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
// Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter2++;
}
}
// printf( "\n" );
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
printf( "%d nodes have reprs.\n", Counter1 );
printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjRefNum(p, pObj) == 0 )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
nFailNoRepr++;
else
nChoices++;
}
else
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
nFailHaveRepr++;
if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
nChoiceNodes++;
}
if ( Gia_ObjReprObj( p, i ) )
assert( Gia_ObjRepr(p, i) < i );
}
if ( nChoices == 0 )
return 0;
if ( nFailNoRepr )
{
printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
// return 0;
}
if ( nFailHaveRepr )
{
printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
// return 0;
}
// printf( "Gia_ManHasChoices_very_old(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
return 1;
}
#include "base/main/mainInt.h"
/**Function*************************************************************

1
src/aig/gia/module.make
View File

@ -4,7 +4,6 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaBidec.c \
src/aig/gia/giaCCof.c \
src/aig/gia/giaCex.c \
src/aig/gia/giaChoice.c \
src/aig/gia/giaCof.c \
src/aig/gia/giaCone.c \
src/aig/gia/giaCSatOld.c \

10
src/base/abci/abc.c
View File

@ -24728,7 +24728,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( pAbc->pGia->pMapping )
if ( Gia_ManHasMapping(pAbc->pGia) )
{
extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p );
pNtk = Abc_NtkFromMappedGia( pAbc->pGia );
@ -26861,7 +26861,7 @@ int Abc_CommandAbc9Bidec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Bidec(): There is no AIG.\n" );
return 1;
}
if ( pAbc->pGia->pMapping == NULL )
if ( !Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Bidec(): Mapping of the AIG is not defined.\n" );
return 1;
@ -26930,7 +26930,7 @@ int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Shrink(): There is no AIG.\n" );
return 1;
}
if ( pAbc->pGia->pMapping == NULL )
if ( !Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Shrink(): Mapping of the AIG is not defined.\n" );
return 1;
@ -29256,7 +29256,7 @@ int Abc_CommandAbc9Trace( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Speedup(): There is no AIG to map.\n" );
return 1;
}
if ( pAbc->pGia->pMapping == NULL )
if ( !Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Speedup(): Mapping of the AIG is not defined.\n" );
return 1;
@ -29347,7 +29347,7 @@ int Abc_CommandAbc9Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Speedup(): There is no AIG to map.\n" );
return 1;
}
if ( pAbc->pGia->pMapping == NULL )
if ( !Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Speedup(): Mapping of the AIG is not defined.\n" );
return 1;

2
src/base/abci/abcDar.c
View File

@ -711,7 +711,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
Gia_Obj_t * pObj, * pObjLi, * pObjLo;
Vec_Ptr_t * vReflect;
int i, k, iFan, nDupGates;
assert( p->pMapping != NULL );
assert( Gia_ManHasMapping(p) );
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(p->pName);

115
src/base/abci/abcTim.c
View File

@ -429,6 +429,115 @@ Gia_Man_t * Abc_NtkTestTimPerformSynthesis( Gia_Man_t * p, int fChoices )
return pGia;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManVerifyChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iRepr, iNode, fProb = 0;
assert( p->pReprs );
// mark nodes
Gia_ManCleanMark0(p);
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( Gia_ObjIsHead(p, iNode) )
printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
Gia_ManObj( p, iNode )->fMark0 = 1;
}
Gia_ManCleanMark0(p);
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
}
else if ( Gia_ObjIsCo(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
}
}
// if ( !fProb )
// printf( "GIA with choices is correct.\n" );
}
/**Function*************************************************************
Synopsis [Reverse the order of nodes in equiv classes.]
Description [If the flag is 1, assumed current increasing order ]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
{
Vec_Int_t * vCollected;
Vec_Int_t * vClass;
int i, k, iRepr, iNode, iPrev;
// collect classes
vCollected = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, iRepr )
Vec_IntPush( vCollected, iRepr );
// correct each class
vClass = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vCollected, iRepr, i )
{
Vec_IntClear( vClass );
Vec_IntPush( vClass, iRepr );
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( fNowIncreasing )
assert( iRepr < iNode );
else
assert( iRepr > iNode );
Vec_IntPush( vClass, iNode );
}
// if ( !fNowIncreasing )
// Vec_IntSort( vClass, 1 );
// reverse the class
iPrev = 0;
iRepr = Vec_IntEntryLast( vClass );
Vec_IntForEachEntry( vClass, iNode, k )
{
if ( fNowIncreasing )
Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
else
Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
Gia_ObjSetNext( p, iNode, iPrev );
iPrev = iNode;
}
}
Vec_IntFree( vCollected );
Vec_IntFree( vClass );
// verify
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
if ( fNowIncreasing )
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
else
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
}
/**Function*************************************************************
Synopsis [Tests the hierarchy-timing manager.]
@ -445,7 +554,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
Gia_Man_t * pGia2;
// normalize choices
if ( Gia_ManWithChoices(pGia) )
if ( Gia_ManHasChoices(pGia) )
{
Gia_ManVerifyChoices( pGia );
Gia_ManReverseClasses( pGia, 0 );
@ -453,14 +562,14 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
// write file
Gia_AigerWrite( pGia, pFileName, 0, 0 );
// unnormalize choices
if ( Gia_ManWithChoices(pGia) )
if ( Gia_ManHasChoices(pGia) )
Gia_ManReverseClasses( pGia, 1 );
// read file
pGia2 = Gia_AigerRead( pFileName, 1, 1 );
// normalize choices
if ( Gia_ManWithChoices(pGia2) )
if ( Gia_ManHasChoices(pGia2) )
{
Gia_ManVerifyChoices( pGia2 );
Gia_ManReverseClasses( pGia2, 1 );

2
src/proof/cec/cecChoice.c
View File

@ -320,7 +320,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc
RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
// derive AIG with choices
pNew = Gia_ManEquivToChoices( pGia, nGias );
Gia_ManHasChoices( pNew );
// Gia_ManHasChoices_very_old( pNew );
// Gia_ManStop( pMiter );
// report the results
if ( pPars->fVerbose )

2
src/proof/cec/cecCorr.c
View File

@ -1188,7 +1188,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
if ( pPars->fMakeChoices )
{
pNew = Gia_ManEquivToChoices( pAig, 1 );
Gia_ManHasChoices( pNew );
// Gia_ManHasChoices_very_old( pNew );
}
else
{