summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h21
-rw-r--r--src/aig/gia/giaAiger.c15
-rw-r--r--src/aig/gia/giaAigerExt.c26
-rw-r--r--src/aig/gia/giaChoice.c373
-rw-r--r--src/aig/gia/giaHcd.c2
-rw-r--r--src/aig/gia/giaIf.c151
-rw-r--r--src/aig/gia/giaMan.c6
-rw-r--r--src/aig/gia/giaShrink.c2
-rw-r--r--src/aig/gia/giaShrink6.c2
-rw-r--r--src/aig/gia/giaSpeedup.c2
-rw-r--r--src/aig/gia/giaUtil.c92
-rw-r--r--src/aig/gia/module.make1
12 files changed, 245 insertions, 448 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 559d40a1..5d3a8762 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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 );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index fd5996c9..8f199f43 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -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 );
diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c
index f7781f5d..7b7758ff 100644
--- a/src/aig/gia/giaAigerExt.c
+++ b/src/aig/gia/giaAigerExt.c
@@ -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 )
{
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c
deleted file mode 100644
index ca2acb28..00000000
--- a/src/aig/gia/giaChoice.c
+++ /dev/null
@@ -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
-
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 11f81e0a..5d3e28f5 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -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 );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 2e8805ae..e42cf638 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -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 );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 5738595b..a573e9e7 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -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 );
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index af727726..1060dbe2 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -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" );
diff --git a/src/aig/gia/giaShrink6.c b/src/aig/gia/giaShrink6.c
index 5ca95fd3..5deb033c 100644
--- a/src/aig/gia/giaShrink6.c
+++ b/src/aig/gia/giaShrink6.c
@@ -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;
diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c
index 5be4dae9..b23decae 100644
--- a/src/aig/gia/giaSpeedup.c
+++ b/src/aig/gia/giaSpeedup.c
@@ -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;
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 99557c7a..2faf424e 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -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*************************************************************
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 8cdbe137..aeda2428 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -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 \
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 12:05:45 +0000