summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aigDup.c1
-rw-r--r--src/aig/gia/gia.h8
-rw-r--r--src/aig/gia/giaDup.c26
-rw-r--r--src/aig/gia/giaEquiv.c171
-rw-r--r--src/aig/gia/giaUtil.c70
-rw-r--r--src/base/cmd/cmdHist.c6
-rw-r--r--src/misc/tim/timBox.c6
-rw-r--r--src/misc/tim/timDump.c13
-rw-r--r--src/misc/tim/timInt.h3
-rw-r--r--src/misc/tim/timMan.c107
-rw-r--r--src/proof/dch/dchChoice.c393
11 files changed, 471 insertions, 333 deletions
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index b4c61d15..9d87db92 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -582,6 +582,7 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
if ( pEquivNew )
{
+ assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
if ( pNew->pEquivs )
pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pEquivNew);
if ( pNew->pReprs )
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2980cb4a..c17fae5f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -570,6 +570,7 @@ static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num; }
+static inline void Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ assert( Num == GIA_VOID || Num > Id ); p->pReprs[Id].iRepr = Num; }
static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; }
static inline int Gia_ObjHasRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr != GIA_VOID; }
static inline int Gia_ObjReprSelf( Gia_Man_t * p, int Id ) { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id; }
@@ -590,8 +591,8 @@ static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { r
static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id ) { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );}
-static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; }
-static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
+static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; }
+static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; }
@@ -758,6 +759,7 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
+extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
@@ -914,9 +916,11 @@ extern int Gia_ManHasDangling( Gia_Man_t * p );
extern int Gia_ManMarkDangling( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index a1d9dd97..d598b511 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -926,7 +926,8 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
Tim_Man_t * pTime = p->pManTime;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
- int i, k, curCi, curCo, curNo, nodeId;
+ int i, k, curCi, curCo, curNo, nodeLim;
+//Gia_ManPrint( p );
assert( pTime != NULL );
assert( Gia_ManIsNormalized(p) );
Gia_ManFillValue( p );
@@ -939,24 +940,24 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew);
curCi = Tim_ManPiNum(pTime);
curCo = 0;
- curNo = Gia_ManPiNum(p);
+ curNo = Gia_ManPiNum(p)+1;
for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
{
// find the latest node feeding into inputs of this box
- nodeId = -1;
+ nodeLim = -1;
for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
{
pObj = Gia_ManPo( p, curCo + k );
- nodeId = Abc_MaxInt( nodeId, Gia_ObjFaninId0p(p, pObj) );
+ nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 );
}
// copy nodes up to the given node
- for ( k = curNo; k <= nodeId; k++ )
+ for ( k = curNo; k < nodeLim; k++ )
{
pObj = Gia_ManObj( p, k );
assert( Gia_ObjIsAnd(pObj) );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
- curNo = Abc_MaxInt( curNo, nodeId + 1 );
+ curNo = Abc_MaxInt( curNo, nodeLim );
// copy COs
for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
{
@@ -972,6 +973,16 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
}
curCi += Tim_ManBoxOutputNum(pTime, i);
}
+ // copy remaining nodes
+ nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p);
+ for ( k = curNo; k < nodeLim; k++ )
+ {
+ pObj = Gia_ManObj( p, k );
+ assert( Gia_ObjIsAnd(pObj) );
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ curNo = Abc_MaxInt( curNo, nodeLim );
+ curNo += Gia_ManPoNum(p);
// copy primary outputs
for ( k = 0; k < Tim_ManPoNum(pTime); k++ )
{
@@ -981,9 +992,10 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
curCo += Tim_ManPoNum(pTime);
assert( curCi == Gia_ManPiNum(p) );
assert( curCo == Gia_ManPoNum(p) );
- assert( curNo == Gia_ManAndNum(p) );
+ assert( curNo == Gia_ManObjNum(p) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Gia_ManDupRemapEquiv( pNew, p );
+//Gia_ManPrint( pNew );
// pass the timing manager
pNew->pManTime = pTime; p->pManTime = NULL;
return pNew;
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 62afe26c..9ccb91fe 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -156,52 +156,6 @@ void Gia_ManDeriveReprs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
-{
- int Ent, nLits = 1;
- Gia_ClassForEachObj1( p, i, Ent )
- {
- assert( Gia_ObjRepr(p, Ent) == i );
- nLits++;
- }
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
-{
- int Ent;
- printf( "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
- Gia_ClassForEachObj( p, i, Ent )
- {
- printf(" %d", Ent );
- if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
- printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
- }
- printf( " }\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
{
int i, nLits = 0;
@@ -324,6 +278,28 @@ int Gia_ManEquivCountLits( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
+int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
+{
+ int Ent, nLits = 1;
+ Gia_ClassForEachObj1( p, i, Ent )
+ {
+ assert( Gia_ObjRepr(p, Ent) == i );
+ nLits++;
+ }
+ return nLits;
+}
+void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
+{
+ int Ent;
+ printf( "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
+ Gia_ClassForEachObj( p, i, Ent )
+ {
+ printf(" %d", Ent );
+ if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
+ printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
+ }
+ printf( " }\n" );
+}
void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
{
int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
@@ -342,13 +318,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
-// printf( "cst =%8d cls =%7d lit =%8d\n",
-// Counter0, Counter, nLits );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
- int Ent;
-
+// int Ent;
printf( "Const0 = " );
Gia_ManForEachConst( p, i )
printf( "%d ", i );
@@ -356,7 +329,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
Counter = 0;
Gia_ManForEachClass( p, i )
Gia_ManEquivPrintOne( p, i, ++Counter );
-
+/*
Gia_ManLevelNum( p );
Gia_ManForEachClass( p, i )
if ( i % 100 == 0 )
@@ -368,7 +341,103 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
}
printf( "\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 );
+
+ // check classes
+ if ( !fNowIncreasing )
+ {
+ iPrev = iRepr;
+ Gia_ClassForEachObj1( p, iRepr, iNode )
+ {
+ if ( iPrev < iNode )
+ {
+ printf( "Class %d : ", iRepr );
+ Gia_ClassForEachObj( p, iRepr, iNode )
+ printf( " %d", iNode );
+ printf( "\n" );
+ break;
+ }
+ iPrev = iNode;
+ }
+ }
+ }
+
+ iRepr = 129720;
+ printf( "Class %d : ", iRepr );
+ Gia_ClassForEachObj( p, iRepr, iNode )
+ printf( " %d", iNode );
+ printf( "\n" );
+
+ iRepr = 129737;
+ printf( "Class %d : ", iRepr );
+ Gia_ClassForEachObj( p, iRepr, iNode )
+ printf( " %d", iNode );
+ printf( "\n" );
+
+ // 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 );
+ if ( iRepr == 129720 || iRepr == 129737 )
+ Vec_IntPrint( vClass );
+ // 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*************************************************************
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 43ef3e08..499f9293 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -993,8 +993,22 @@ int Gia_ManHasChoices( Gia_Man_t * p )
void Gia_ManVerifyChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
- int i, fProb = 0;
+ 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) )
@@ -1010,8 +1024,8 @@ void Gia_ManVerifyChoices( Gia_Man_t * p )
printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
}
}
-// if ( !fProb )
-// printf( "GIA with choices is correct.\n" );
+ if ( !fProb )
+ printf( "GIA with choices is correct.\n" );
}
/**Function*************************************************************
@@ -1135,7 +1149,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
pObj = Gia_Not(pObj);
}
assert( !Gia_IsComplement(pObj) );
- printf( "Node %4d : ", Gia_ObjId(p, pObj) );
+ printf( "Obj %4d : ", Gia_ObjId(p, pObj) );
if ( Gia_ObjIsConst0(pObj) )
printf( "constant 0" );
else if ( Gia_ObjIsPi(p, pObj) )
@@ -1180,6 +1194,13 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
}
*/
}
+void Gia_ManPrint( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManForEachObj( p, pObj, i )
+ Gia_ObjPrint( p, pObj );
+}
/**Function*************************************************************
@@ -1419,6 +1440,47 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the manager are structural identical.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
+{
+ Gia_Obj_t * pObj1, * pObj2;
+ int i;
+ if ( Gia_ManObjNum(p1) != Gia_ManObjNum(p2) )
+ {
+ printf( "AIGs have different number of objects.\n" );
+ return 0;
+ }
+ Gia_ManCleanValue( p1 );
+ Gia_ManCleanValue( p2 );
+ Gia_ManForEachObj( p1, pObj1, i )
+ {
+ pObj2 = Gia_ManObj( p2, i );
+ if ( memcmp( pObj1, pObj2, sizeof(Gia_Obj_t) ) )
+ {
+ printf( "Objects %d are different.\n", i );
+ return 0;
+ }
+ if ( p1->pReprs && p2->pReprs )
+ {
+ if ( memcmp( &p1->pReprs[i], &p2->pReprs[i], sizeof(Gia_Rpr_t) ) )
+ {
+ printf( "Representatives of objects %d are different.\n", i );
+ return 0;
+ }
+ }
+ }
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index 27a3e61e..ed1d2efa 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -48,7 +48,7 @@ ABC_NAMESPACE_IMPL_START
void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
{
int nLastLooked = 10; // do not add history if the same entry appears among the last entries
- int nLastSaved = 100; // when saving a file, save no more than this number of last entries
+ int nLastSaved = 500; // when saving a file, save no more than this number of last entries
char Buffer[ABC_MAX_STR];
int Len = strlen(command);
@@ -57,9 +57,11 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
Buffer[Len-1] = 0;
if ( strlen(Buffer) > 3 &&
strncmp(Buffer,"set",3) &&
+ strncmp(Buffer,"time",4) &&
strncmp(Buffer,"quit",4) &&
strncmp(Buffer,"source",6) &&
- strncmp(Buffer,"history",7) && strncmp(Buffer,"hi ", 3) && strcmp(Buffer,"hi") )
+ strncmp(Buffer,"history",7) && strncmp(Buffer,"hi ", 3) && strcmp(Buffer,"hi") &&
+ Buffer[strlen(Buffer)-1] != '?' )
{
char * pStr = NULL;
int i, Start = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory) - nLastLooked );
diff --git a/src/misc/tim/timBox.c b/src/misc/tim/timBox.c
index 65b0ae6e..c1176527 100644
--- a/src/misc/tim/timBox.c
+++ b/src/misc/tim/timBox.c
@@ -189,10 +189,14 @@ int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
***********************************************************************/
float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox )
{
+ float * pTable;
Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
if ( pBox->iDelayTable < 0 )
return NULL;
- return (float *)Vec_PtrEntry( p->vDelayTables, pBox->iDelayTable );
+ pTable = (float *)Vec_PtrEntry( p->vDelayTables, pBox->iDelayTable );
+ assert( (int)pTable[1] == pBox->nInputs );
+ assert( (int)pTable[2] == pBox->nOutputs );
+ return pTable;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/tim/timDump.c b/src/misc/tim/timDump.c
index 031ef5fc..eb9a14a9 100644
--- a/src/misc/tim/timDump.c
+++ b/src/misc/tim/timDump.c
@@ -63,6 +63,7 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
// save number of boxes
Vec_StrPutI_ne( vStr, Tim_ManBoxNum(p) );
// for each box, save num_inputs, num_outputs, and delay table ID
+ if ( Tim_ManBoxNum(p) > 0 )
Tim_ManForEachBox( p, pBox, i )
{
Vec_StrPutI_ne( vStr, Tim_ManBoxInputNum(p, pBox->iBox) );
@@ -72,7 +73,8 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
// save the number of delay tables
Vec_StrPutI_ne( vStr, Tim_ManDelayTableNum(p) );
// save the delay tables
- Vec_PtrForEachEntry( float *, p->vDelayTables, pDelayTable, i )
+ if ( Tim_ManDelayTableNum(p) > 0 )
+ Tim_ManForEachTable( p, pDelayTable, i )
{
assert( (int)pDelayTable[0] == i );
// save table ID and dimensions (inputs x outputs)
@@ -126,7 +128,8 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
// start boxes
nBoxes = Vec_StrGetI_ne( p, &iStr );
assert( pMan->vBoxes == NULL );
- pMan->vBoxes = Vec_PtrAlloc( nBoxes );
+ if ( nBoxes > 0 )
+ pMan->vBoxes = Vec_PtrAlloc( nBoxes );
// create boxes
curPi = nPis;
curPo = 0;
@@ -145,9 +148,9 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
// create delay tables
nTables = Vec_StrGetI_ne( p, &iStr );
assert( pMan->vDelayTables == NULL );
- pMan->vDelayTables = Vec_PtrAlloc( nTables );
+ if ( nTables > 0 )
+ pMan->vDelayTables = Vec_PtrAlloc( nTables );
// read delay tables
- assert( Vec_PtrSize(pMan->vDelayTables) == 0 );
for ( i = 0; i < nTables; i++ )
{
// read table ID and dimensions
@@ -167,7 +170,7 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
assert( Vec_PtrSize(pMan->vDelayTables) == TableId );
Vec_PtrPush( pMan->vDelayTables, pDelayTable );
}
- assert( Vec_PtrSize(pMan->vDelayTables) == nTables );
+ assert( Tim_ManDelayTableNum(pMan) == nTables );
// Tim_ManPrint( pMan );
return pMan;
}
diff --git a/src/misc/tim/timInt.h b/src/misc/tim/timInt.h
index 9d8b7389..6fe5a94c 100644
--- a/src/misc/tim/timInt.h
+++ b/src/misc/tim/timInt.h
@@ -128,6 +128,9 @@ static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int
#define Tim_ManBoxForEachOutput( p, pBox, pObj, i ) \
for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
+#define Tim_ManForEachTable( p, pTable, i ) \
+ Vec_PtrForEachEntry( float *, p->vDelayTables, pTable, i )
+
////////////////////////////////////////////////////////////////////////
/// SEQUENTIAL ITERATORS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 5340ad9e..c177a707 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -112,25 +112,32 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
Tim_ManInitPoRequiredAll( p, (float)TIM_ETERNITY );
}
// duplicate delay tables
- pNew->vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vDelayTables) );
- Vec_PtrForEachEntry( float *, p->vDelayTables, pDelayTable, i )
+ if ( Tim_ManDelayTableNum(p) > 0 )
{
- assert( i == (int)pDelayTable[0] );
- nInputs = (int)pDelayTable[1];
- nOutputs = (int)pDelayTable[2];
- pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
- pDelayTableNew[0] = (int)pDelayTable[0];
- pDelayTableNew[1] = (int)pDelayTable[1];
- pDelayTableNew[2] = (int)pDelayTable[2];
- for ( k = 0; k < nInputs * nOutputs; k++ )
- pDelayTableNew[3+k] = fUnitDelay ? 1.0 : pDelayTable[3+k];
- assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
- Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+ pNew->vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vDelayTables) );
+ Tim_ManForEachTable( p, pDelayTable, i )
+ {
+ assert( i == (int)pDelayTable[0] );
+ nInputs = (int)pDelayTable[1];
+ nOutputs = (int)pDelayTable[2];
+ pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
+ pDelayTableNew[0] = (int)pDelayTable[0];
+ pDelayTableNew[1] = (int)pDelayTable[1];
+ pDelayTableNew[2] = (int)pDelayTable[2];
+ for ( k = 0; k < nInputs * nOutputs; k++ )
+ pDelayTableNew[3+k] = fUnitDelay ? 1.0 : pDelayTable[3+k];
+ assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
+ Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+ }
}
// duplicate boxes
- Tim_ManForEachBox( p, pBox, i )
- Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs,
- pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable );
+ if ( Tim_ManBoxNum(p) > 0 )
+ {
+ pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
+ Tim_ManForEachBox( p, pBox, i )
+ Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs,
+ pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable );
+ }
return pNew;
}
@@ -147,15 +154,8 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
***********************************************************************/
void Tim_ManStop( Tim_Man_t * p )
{
- float * pTable;
- int i;
- if ( p->vDelayTables )
- {
- Vec_PtrForEachEntry( float *, p->vDelayTables, pTable, i )
- ABC_FREE( pTable );
- Vec_PtrFree( p->vDelayTables );
- }
- Vec_PtrFree( p->vBoxes );
+ Vec_PtrFreeFree( p->vDelayTables );
+ Vec_PtrFreeP( &p->vBoxes );
Mem_FlexStop( p->pMemObj, 0 );
ABC_FREE( p->pCis );
ABC_FREE( p->pCos );
@@ -185,7 +185,7 @@ void Tim_ManPrint( Tim_Man_t * p )
Tim_Box_t * pBox;
Tim_Obj_t * pObj, * pPrev;
float * pTable;
- int i, k;
+ int i, j, k, TableX, TableY;
printf( "TIMING INFORMATION:\n" );
// print CI info
@@ -211,40 +211,48 @@ void Tim_ManPrint( Tim_Man_t * p )
printf( "PO%5d : arr = %5.3f req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
// print box info
+ if ( Tim_ManBoxNum(p) > 0 )
Tim_ManForEachBox( p, pBox, i )
{
- printf( "*** Box %3d : Ins = %d. Outs = %d.\n", i, pBox->nInputs, pBox->nOutputs );
- printf( "Delay table:\n" );
- pTable = Tim_ManBoxDelayTable( p, pBox->iBox );
- for ( i = 0; i < pBox->nOutputs; i++, printf( "\n" ) )
- for ( k = 0; k < pBox->nInputs; k++ )
- if ( pTable[3+i*pBox->nInputs+k] == -ABC_INFINITY )
- printf( "%5s", "-" );
- else
- printf( "%5.0f", pTable[3+i*pBox->nInputs+k] );
- printf( "\n" );
+ printf( "*** Box %5d : Ins = %4d. Outs = %4d. DelayTable = %4d\n", i, pBox->nInputs, pBox->nOutputs, pBox->iDelayTable );
// print box inputs
pPrev = Tim_ManBoxInput( p, pBox, 0 );
- Tim_ManBoxForEachInput( p, pBox, pObj, i )
+ Tim_ManBoxForEachInput( p, pBox, pObj, k )
if ( pPrev->timeArr != pObj->timeArr || pPrev->timeReq != pObj->timeReq )
break;
- if ( i == Tim_ManBoxInputNum(p, pBox->iBox) )
+ if ( k == Tim_ManBoxInputNum(p, pBox->iBox) )
printf( "Box inputs : arr = %5.3f req = %5.3f\n", pPrev->timeArr, pPrev->timeReq );
else
- Tim_ManBoxForEachInput( p, pBox, pObj, i )
- printf( "box-inp%3d : arr = %5.3f req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+ Tim_ManBoxForEachInput( p, pBox, pObj, k )
+ printf( "box-in%4d : arr = %5.3f req = %5.3f\n", k, pObj->timeArr, pObj->timeReq );
// print box outputs
pPrev = Tim_ManBoxOutput( p, pBox, 0 );
- Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+ Tim_ManBoxForEachOutput( p, pBox, pObj, k )
if ( pPrev->timeArr != pObj->timeArr || pPrev->timeReq != pObj->timeReq )
break;
- if ( i == Tim_ManBoxOutputNum(p, pBox->iBox) )
+ if ( k == Tim_ManBoxOutputNum(p, pBox->iBox) )
printf( "Box outputs : arr = %5.3f req = %5.3f\n", pPrev->timeArr, pPrev->timeReq );
else
- Tim_ManBoxForEachOutput( p, pBox, pObj, i )
- printf( "box-out%3d : arr = %5.3f req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+ Tim_ManBoxForEachOutput( p, pBox, pObj, k )
+ printf( "box-out%3d : arr = %5.3f req = %5.3f\n", k, pObj->timeArr, pObj->timeReq );
+ }
+
+ // print delay tables
+ if ( Tim_ManDelayTableNum(p) > 0 )
+ Tim_ManForEachTable( p, pTable, i )
+ {
+ printf( "Delay table %d:\n", i );
+ assert( i == (int)pTable[0] );
+ TableX = (int)pTable[1];
+ TableY = (int)pTable[2];
+ for ( j = 0; j < TableY; j++, printf( "\n" ) )
+ for ( k = 0; k < TableX; k++ )
+ if ( pTable[3+j*TableX+k] == -ABC_INFINITY )
+ printf( "%5s", "-" );
+ else
+ printf( "%5.0f", pTable[3+j*TableX+k] );
}
printf( "\n" );
}
@@ -270,20 +278,25 @@ int Tim_ManCoNum( Tim_Man_t * p )
}
int Tim_ManPiNum( Tim_Man_t * p )
{
+ if ( Tim_ManBoxNum(p) == 0 )
+ return Tim_ManCiNum(p);
return Tim_ManBoxOutputFirst(p, 0);
}
int Tim_ManPoNum( Tim_Man_t * p )
{
- int iLastBoxId = Tim_ManBoxNum(p) - 1;
+ int iLastBoxId;
+ if ( Tim_ManBoxNum(p) == 0 )
+ return Tim_ManCoNum(p);
+ iLastBoxId = Tim_ManBoxNum(p) - 1;
return Tim_ManCoNum(p) - (Tim_ManBoxInputFirst(p, iLastBoxId) + Tim_ManBoxInputNum(p, iLastBoxId));
}
int Tim_ManBoxNum( Tim_Man_t * p )
{
- return Vec_PtrSize(p->vBoxes);
+ return p->vBoxes ? Vec_PtrSize(p->vBoxes) : 0;
}
int Tim_ManDelayTableNum( Tim_Man_t * p )
{
- return Vec_PtrSize(p->vDelayTables);
+ return p->vDelayTables ? Vec_PtrSize(p->vDelayTables) : 0;
}
/**Function*************************************************************
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 5da5f0f3..8fc8192f 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -103,68 +103,6 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
/**Function*************************************************************
- Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- // check the trivial cases
- if ( pObj == NULL )
- return 0;
- if ( Aig_ObjIsCi(pObj) )
- return 0;
- if ( pObj->fMarkA )
- return 1;
- // skip the visited node
- if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
- return 0;
- Aig_ObjSetTravIdCurrent( p, pObj );
- // check the children
- if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
- return 1;
- if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
- return 1;
- // check equivalent nodes
- return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pTemp;
- int RetValue;
- assert( !Aig_IsComplement(pObj) );
- assert( !Aig_IsComplement(pRepr) );
- // mark nodes of the choice node
- for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
- pTemp->fMarkA = 1;
- // traverse the new node
- Aig_ManIncrementTravId( p );
- RetValue = Dch_ObjCheckTfi_rec( p, pObj );
- // unmark nodes of the choice node
- for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
- pTemp->fMarkA = 0;
- return RetValue;
-}
-
-/**Function*************************************************************
-
Synopsis [Returns representatives of fanin in approapriate polarity.]
Description []
@@ -190,146 +128,6 @@ static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj
/**Function*************************************************************
- Synopsis [Marks the TFI of the node.]
-
- Description [Returns 1 if there is a CI not marked with previous ID.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- int RetValue;
- if ( pObj == NULL )
- return 0;
- if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
- return 0;
- if ( Aig_ObjIsCi(pObj) )
- {
- RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
- Aig_ObjSetTravIdCurrent( p, pObj );
- return RetValue;
- }
- assert( Aig_ObjIsNode(pObj) );
- Aig_ObjSetTravIdCurrent( p, pObj );
- RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
- RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
-// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
- return (RetValue > 0);
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
-{
- Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
- // get the new node
- pObj->pData = Aig_And( pAigNew,
- Aig_ObjChild0CopyRepr(pAigNew, pObj),
- Aig_ObjChild1CopyRepr(pAigNew, pObj) );
- pRepr = Aig_ObjRepr( pAigOld, pObj );
- if ( pRepr == NULL )
- return;
- // get the corresponding new nodes
- pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData);
- pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
- if ( pObjNew == pReprNew )
- return;
- // skip the earlier nodes
- if ( pReprNew->Id > pObjNew->Id )
- return;
- assert( pReprNew->Id < pObjNew->Id );
- // set the representatives
- Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
- // skip used nodes
- if ( pObjNew->nRefs > 0 )
- return;
- assert( pObjNew->nRefs == 0 );
- // update new nodes of the object
- if ( !Aig_ObjIsNode(pRepr) )
- return;
- // skip choices with combinational loops
- if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
- return;
- // don't add choice if structural support of pObjNew and pReprNew differ
- if ( fSkipRedSupps )
- {
- int fSkipChoice = 0;
- // mark support of the representative node (pReprNew)
- Aig_ManIncrementTravId( pAigNew );
- Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
- // detect if the new node (pObjNew) depends on any additional variables
- Aig_ManIncrementTravId( pAigNew );
- if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
- fSkipChoice = 1;//, printf( "1" );
- // detect if the representative node (pReprNew) depends on any additional variables
- Aig_ManIncrementTravId( pAigNew );
- if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
- fSkipChoice = 1;//, printf( "2" );
- // skip the choice if this is what is happening
- if ( fSkipChoice )
- return;
- }
- // add choice
- pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
- pAigNew->pEquivs[pReprNew->Id] = pObjNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
-{
- Aig_Man_t * pChoices, * pTemp;
- Aig_Obj_t * pObj;
- int i;
- // start recording equivalences
- pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
- pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- pChoices->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- // map constants and PIs
- Aig_ManCleanData( pAig );
- Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
- Aig_ManForEachCi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreateCi( pChoices );
- // construct choices for the internal nodes
- assert( pAig->pReprs != NULL );
- Aig_ManForEachNode( pAig, pObj, i )
- Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, 0 );
- Aig_ManForEachCo( pAig, pObj, i )
- Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
- Dch_DeriveChoiceCountEquivs( pChoices );
- // there is no need for cleanup
- ABC_FREE( pChoices->pReprs );
- pChoices = Aig_ManDupDfs( pTemp = pChoices );
- Aig_ManStop( pTemp );
- return pChoices;
-}
-
-
-
-
-/**Function*************************************************************
-
Synopsis [Checks for combinational loops in the AIG.]
Description [Returns 1 if combinational loop is detected.]
@@ -413,18 +211,6 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
Aig_ObjSetTravIdPrevious( p, pNode );
return 1;
}
-
-/**Function*************************************************************
-
- Synopsis [Checks for combinational loops in the AIG.]
-
- Description [Returns 1 if there is no combinational loops.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
{
Aig_Obj_t * pNode;
@@ -487,6 +273,124 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
/**Function*************************************************************
+ Synopsis [Verify correctness of choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_CheckChoices( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, fProb = 0;
+ Aig_ManCleanMarkA( p );
+ Aig_ManForEachNode( p, pObj, i )
+ if ( p->pEquivs[i] != NULL )
+ {
+ if ( pObj->fMarkA == 1 )
+ printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
+ pObj->fMarkA = 1;
+ // consider the last one
+ pObj = p->pEquivs[i];
+ if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
+ {
+ if ( pObj->fMarkA == 1 )
+ printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
+ pObj->fMarkA = 1;
+ }
+ }
+ Aig_ManCleanMarkA( p );
+ if ( !fProb )
+ printf( "Verification of choice AIG succeeded.\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI of the node.]
+
+ Description [Returns 1 if there is a CI not marked with previous ID.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ int RetValue;
+ if ( pObj == NULL )
+ return 0;
+ if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+ return 0;
+ if ( Aig_ObjIsCi(pObj) )
+ {
+ RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ return RetValue;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
+ RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
+// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+ return (RetValue > 0);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ // check the trivial cases
+ if ( pObj == NULL )
+ return 0;
+ if ( Aig_ObjIsCi(pObj) )
+ return 0;
+ if ( pObj->fMarkA )
+ return 1;
+ // skip the visited node
+ if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+ return 0;
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ // check the children
+ if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
+ return 1;
+ if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
+ return 1;
+ // check equivalent nodes
+ return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+}
+int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+ Aig_Obj_t * pTemp;
+ int RetValue;
+ assert( !Aig_IsComplement(pObj) );
+ assert( !Aig_IsComplement(pRepr) );
+ // mark nodes of the choice node
+ for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+ pTemp->fMarkA = 1;
+ // traverse the new node
+ Aig_ManIncrementTravId( p );
+ RetValue = Dch_ObjCheckTfi_rec( p, pObj );
+ // unmark nodes of the choice node
+ for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+ pTemp->fMarkA = 0;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
Synopsis [Derives the AIG with choices from representatives.]
Description []
@@ -496,11 +400,71 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
+void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
+{
+ Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+ // get the new node
+ assert( pObj->pData == NULL );
+ pObj->pData = Aig_And( pAigNew,
+ Aig_ObjChild0CopyRepr(pAigNew, pObj),
+ Aig_ObjChild1CopyRepr(pAigNew, pObj) );
+ pRepr = Aig_ObjRepr( pAigOld, pObj );
+ if ( pRepr == NULL )
+ return;
+ assert( pRepr->Id < pObj->Id );
+ // get the corresponding new nodes
+ pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData);
+ pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
+ if ( pObjNew == pReprNew )
+ return;
+ // skip the earlier nodes
+ if ( pReprNew->Id > pObjNew->Id )
+ return;
+ assert( pReprNew->Id < pObjNew->Id );
+ // set the representatives
+ Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+ // skip used nodes
+ if ( pObjNew->nRefs > 0 )
+ return;
+ assert( pObjNew->nRefs == 0 );
+ // update new nodes of the object
+ if ( !Aig_ObjIsNode(pRepr) )
+ return;
+ // skip choices with combinational loops
+ if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+ return;
+ // don't add choice if structural support of pObjNew and pReprNew differ
+ if ( fSkipRedSupps )
+ {
+ int fSkipChoice = 0;
+ // mark support of the representative node (pReprNew)
+ Aig_ManIncrementTravId( pAigNew );
+ Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
+ // detect if the new node (pObjNew) depends on any additional variables
+ Aig_ManIncrementTravId( pAigNew );
+ if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
+ fSkipChoice = 1;//, printf( "1" );
+ // detect if the representative node (pReprNew) depends on any additional variables
+ Aig_ManIncrementTravId( pAigNew );
+ if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
+ fSkipChoice = 1;//, printf( "2" );
+ // skip the choice if this is what is happening
+ if ( fSkipChoice )
+ return;
+ }
+ // add choice
+ pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
+ pAigNew->pEquivs[pReprNew->Id] = pObjNew;
+}
Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
{
Aig_Man_t * pChoices;
Aig_Obj_t * pObj;
int i;
+ // make sure reprsentative nodes do not have representatives
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( pAig->pReprs[i] != NULL && pAig->pReprs[pAig->pReprs[i]->Id] != NULL )
+ printf( "Node %d: repr %d has repr %d.\n", i, Aig_ObjId(pAig->pReprs[i]), Aig_ObjId(pAig->pReprs[pAig->pReprs[i]->Id]) );
// start recording equivalences
pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
@@ -518,6 +482,7 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
Dch_DeriveChoiceCountEquivs( pChoices );
Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
+//Dch_CheckChoices( pChoices );
return pChoices;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-28 21:05:54 +0000