summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigIso.c135
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigDup.c76
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/misc/vec/vecInt.h2
6 files changed, 217 insertions, 12 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index ad8ce927..0a2ea6b6 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -163,6 +163,7 @@ struct Aig_Man_t_
Vec_Vec_t * vClockDoms;
Vec_Int_t * vProbs; // probability of node being 1
Vec_Int_t * vCiNumsOrig; // original CI names
+ int nComplEdges; // complemented edges
// timing statistics
int time1;
int time2;
diff --git a/src/aig/aig/aigIso.c b/src/aig/aig/aigIso.c
index 71687f14..6e5ff6a5 100644
--- a/src/aig/aig/aigIso.c
+++ b/src/aig/aig/aigIso.c
@@ -92,6 +92,8 @@ int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
+ if ( pAig->nComplEdges > 0 )
+ return pAig->nComplEdges;
Aig_ManForEachObj( pAig, pObj, i )
if ( Aig_ObjIsNode(pObj) )
{
@@ -100,7 +102,7 @@ int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
}
else if ( Aig_ObjIsPo(pObj) )
Counter += Aig_ObjFaninC0(pObj);
- return Counter;
+ return (pAig->nComplEdges = Counter);
}
/**Function*************************************************************
@@ -716,7 +718,7 @@ int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2
SeeAlso []
***********************************************************************/
-Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbose )
+Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
{
Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
int i, Entry;
@@ -732,12 +734,16 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbo
return NULL;
if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
return NULL;
- if ( fVerbose )
+ if ( fVerbose )
printf( "AIG1:\n" );
- vPerm1 = Iso_ManFindPerm( pAig1, fVerbose );
+ vPerm1 = vPerm1_ ? vPerm1_ : Iso_ManFindPerm( pAig1, fVerbose );
if ( fVerbose )
printf( "AIG1:\n" );
- vPerm2 = Iso_ManFindPerm( pAig2, fVerbose );
+ vPerm2 = vPerm2_ ? vPerm2_ : Iso_ManFindPerm( pAig2, fVerbose );
+ if ( vPerm1_ )
+ assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) );
+ if ( vPerm2_ )
+ assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) );
// find canonical permutation
// vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
@@ -746,8 +752,10 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbo
assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
}
- Vec_IntFree( vPerm1 );
- Vec_IntFree( vPerm2 );
+ if ( vPerm1_ == NULL )
+ Vec_IntFree( vPerm1 );
+ if ( vPerm2_ == NULL )
+ Vec_IntFree( vPerm2 );
// check if they are indeed equivalent
if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
Vec_IntFreeP( &vInvPerm2 );
@@ -772,9 +780,10 @@ void Iso_ManTestOne( Aig_Man_t * pAig, int fVerbose )
Vec_IntFree( vPerm );
}
-#include "src/base/abc/abc.h"
+#include "src/aig/saig/saig.h"
+
/**Function*************************************************************
Synopsis []
@@ -786,7 +795,91 @@ void Iso_ManTestOne( Aig_Man_t * pAig, int fVerbose )
SeeAlso []
***********************************************************************/
-void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
+Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+{
+ int fVeryVerbose = 0;
+ Vec_Ptr_t * vParts, * vPerms, * vAigs;
+ Vec_Int_t * vPos, * vMap;
+ Aig_Man_t * pPart, * pTemp;
+ int i, k, nPos;
+
+ // derive AIG for each PO
+ nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+ vParts = Vec_PtrAlloc( nPos );
+ vPerms = Vec_PtrAlloc( nPos );
+ for ( i = 0; i < nPos; i++ )
+ {
+ pPart = Saig_ManDupCones( pAig, &i, 1 );
+ vMap = Iso_ManFindPerm( pPart, fVeryVerbose );
+ Vec_PtrPush( vParts, pPart );
+ Vec_PtrPush( vPerms, vMap );
+ }
+
+ // check AIGs for each PO
+ vAigs = Vec_PtrAlloc( 1000 );
+ vPos = Vec_IntAlloc( 1000 );
+ Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+ {
+ if ( fVeryVerbose )
+ {
+ printf( "AIG %4d : ", i );
+ Aig_ManPrintStats( pPart );
+ }
+ Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
+ {
+ if ( fVeryVerbose )
+ printf( "Comparing AIG %4d and AIG %4d. ", Vec_IntEntry(vPos,k), i );
+ vMap = Iso_ManFindMapping( pTemp, pPart,
+ (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)),
+ (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
+ fVeryVerbose );
+ if ( vMap != NULL )
+ {
+ if ( fVeryVerbose )
+ printf( "Found match\n" );
+ if ( fVerbose )
+ printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
+ Vec_IntFree( vMap );
+ break;
+ }
+ if ( fVeryVerbose )
+ printf( "No match.\n" );
+ }
+ if ( k == Vec_PtrSize(vAigs) )
+ {
+ Vec_PtrPush( vAigs, pPart );
+ Vec_IntPush( vPos, i );
+ }
+ }
+ // delete AIGs
+ Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+ Aig_ManStop( pPart );
+ Vec_PtrFree( vParts );
+ Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
+ Vec_IntFree( vMap );
+ Vec_PtrFree( vPerms );
+ // derive the resulting AIG
+ pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
+ Vec_PtrFree( vAigs );
+ Vec_IntFree( vPos );
+ return pPart;
+}
+
+
+#include "src/base/abc/abc.h"
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Iso_ManTestOld( Aig_Man_t * pAig1, int fVerbose )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
@@ -799,7 +892,7 @@ void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
Abc_NtkDelete( pNtk );
- vMap = Iso_ManFindMapping( pAig1, pAig2, fVerbose );
+ vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
Aig_ManStop( pAig2 );
if ( vMap != NULL )
@@ -813,6 +906,28 @@ void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
Vec_IntFreeP( &vMap );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
+{
+ Aig_Man_t * pPart;
+ int clk = clock();
+ pPart = Iso_ManFilterPos( pAig, fVerbose );
+ printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+// Aig_ManStop( pPart );
+ return pPart;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index a20096ec..74566966 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -174,6 +174,7 @@ extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
+extern Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigInd.c ==========================================================*/
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index fa915f52..e0b3bd2a 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -446,6 +446,82 @@ Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit )
return pAigNew;
}
+/**Function*************************************************************
+
+ Synopsis [Copy an AIG structure related to the selected POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManDupCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
+{
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+ Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
+ Vec_PtrPush( vNodes, pObj );
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+ else if ( Saig_ObjIsLo(p, pObj) )
+ Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
+ else if ( Saig_ObjIsPi(p, pObj) )
+ Vec_PtrPush( vLeaves, pObj );
+ else assert( 0 );
+}
+Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos )
+{
+ Aig_Man_t * pAigNew;
+ Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
+ Aig_Obj_t * pObj;
+ int i;
+
+ // collect initial POs
+ vLeaves = Vec_PtrAlloc( 100 );
+ vNodes = Vec_PtrAlloc( 100 );
+ vRoots = Vec_PtrAlloc( 100 );
+ for ( i = 0; i < nPos; i++ )
+ Vec_PtrPush( vRoots, Aig_ManPo(pAig, pPos[i]) );
+
+ // mark internal nodes
+ Aig_ManIncrementTravId( pAig );
+ Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+ Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+ Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
+
+ // start the new manager
+ pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
+ pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // create PIs
+ Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ // create LOs
+ Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
+ Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreatePi( pAigNew );
+ // create internal nodes
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create COs
+ Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ // finalize
+ Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
+ Vec_PtrFree( vLeaves );
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vRoots );
+ return pAigNew;
+
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c71cfc7b..2ed59dbb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8837,16 +8837,26 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Aig_ManSupportsTest( Aig_Man_t * pMan );
extern int Aig_SupportSizeTest( Aig_Man_t * pMan );
extern int Abc_NtkSuppSizeTest( Abc_Ntk_t * p );
- extern void Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
+ extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
if ( pNtk )
{
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+ Aig_Man_t * pRes;
+ Abc_Ntk_t * pNtkRes;
// Aig_ManInterRepar( pAig, 1 );
// Aig_ManInterTest( pAig, 1 );
// Aig_ManSupportsTest( pAig );
// Aig_SupportSizeTest( pAig );
- Iso_ManTest( pAig, fVerbose );
+ pRes = Iso_ManTest( pAig, fVerbose );
Aig_ManStop( pAig );
+
+ pNtkRes = Abc_NtkFromAigPhase( pRes );
+ Aig_ManStop( pRes );
+
+ ABC_FREE( pNtkRes->pName );
+ pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
}
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 5a25d2c9..be54e583 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -926,6 +926,8 @@ static inline Vec_Int_t * Vec_IntInvert( Vec_Int_t * p, int Fill )
{
int Entry, i;
Vec_Int_t * vRes = Vec_IntAlloc( 0 );
+ if ( Vec_IntSize(p) == 0 )
+ return vRes;
Vec_IntFill( vRes, Vec_IntFindMax(p) + 1, Fill );
Vec_IntForEachEntry( p, Entry, i )
if ( Entry != Fill )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 06:03:35 +0000