summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaIso2.c193
-rw-r--r--src/base/abci/abc.c12
3 files changed, 141 insertions, 66 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4a41ee9f..fb93e0c2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1093,7 +1093,7 @@ extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pP
/*=== giaIso.c ===========================================================*/
extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
-extern Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fBetterQual, int fDualOut, int fVerbose, int fVeryVerbose );
/*=== giaLogic.c ===========================================================*/
extern void Gia_ManTestDistance( Gia_Man_t * p );
extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
diff --git a/src/aig/gia/giaIso2.c b/src/aig/gia/giaIso2.c
index ef5dbf42..e9d9d883 100644
--- a/src/aig/gia/giaIso2.c
+++ b/src/aig/gia/giaIso2.c
@@ -486,68 +486,87 @@ void Gia_Iso2ManCollectOrder( Gia_Man_t * pGia, int * pPos, int nPos, Vec_Int_t
SeeAlso []
***********************************************************************/
-int Gia_Iso2ManCheckIsoClass( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
+int Gia_Iso2ManCheckIsoPair( Gia_Man_t * p, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
{
Gia_Obj_t * pObj0, * pObj1;
- int i, k, iObj0, iObj1, iPo;
- assert( Vec_IntSize(vClass) > 1 );
- iPo = Vec_IntEntry( vClass, 0 );
- Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
- Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+ int k, iObj0, iObj1;
+ Vec_IntForEachEntryTwo( vVec0, vVec1, iObj0, iObj1, k )
{
- Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
- if ( Vec_IntSize(vVec0) != Vec_IntSize(vVec1) )
+ if ( iObj0 == iObj1 )
+ continue;
+ pObj0 = Gia_ManObj(p, iObj0);
+ pObj1 = Gia_ManObj(p, iObj1);
+ if ( pObj0->Value != pObj1->Value )
+ return 0;
+ assert( pObj0->Value == pObj1->Value );
+ if ( !Gia_ObjIsAnd(pObj0) )
continue;
- Vec_IntForEachEntryTwo( vVec0, vVec1, iObj0, iObj1, k )
+ if ( Gia_ObjFanin0(pObj0)->Value <= Gia_ObjFanin1(pObj0)->Value )
+ {
+ if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
+ {
+ if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1) || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
+ return 0;
+ }
+ else
+ {
+ if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1) || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
+ return 0;
+ }
+ }
+ else
{
- if ( iObj0 == iObj1 )
- continue;
- pObj0 = Gia_ManObj(p, iObj0);
- pObj1 = Gia_ManObj(p, iObj1);
- if ( pObj0->Value != pObj1->Value )
- return 0;
- assert( pObj0->Value == pObj1->Value );
- if ( !Gia_ObjIsAnd(pObj0) )
- continue;
- if ( Gia_ObjFanin0(pObj0)->Value <= Gia_ObjFanin1(pObj0)->Value )
+ if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
{
- if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
- {
- if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1) || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
- return 0;
- }
- else
- {
- if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1) || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
- return 0;
- }
+ if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1) || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
+ return 0;
}
else
{
- if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
- {
- if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1) || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
- return 0;
- }
- else
- {
- if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1) || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) ||
- Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
- return 0;
- }
+ if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1) || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) ||
+ Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
+ return 0;
}
}
}
return 1;
}
-Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_Iso2ManCheckIsoClassOneSkip( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
+{
+ int i, iPo;
+ assert( Vec_IntSize(vClass) > 1 );
+ iPo = Vec_IntEntry( vClass, 0 );
+ Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
+ Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+ {
+ Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
+ if ( Vec_IntSize(vVec0) != Vec_IntSize(vVec1) )
+ return 0;
+ if ( !Gia_Iso2ManCheckIsoPair( p, vVec0, vVec1, vMap0, vMap1 ) )
+ return 0;
+ }
+ return 1;
+}
+Vec_Wec_t * Gia_Iso2ManCheckIsoClassesSkip( Gia_Man_t * p, Vec_Wec_t * vEquivs )
{
Vec_Wec_t * vEquivs2;
Vec_Int_t * vRoots = Vec_IntAlloc( 10000 );
@@ -562,16 +581,7 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
{
if ( i % 100 == 0 )
printf( "%8d finished...\r", i );
-/*
- if ( i == 17 )
- {
- Gia_Man_t * pCone;
- pCone = Gia_ManDupCones( p, Vec_IntArray(vClass), 2, 1 );
- Gia_AigerWrite( pCone, "dump.aig", 0, 0 );
- Gia_ManStop( pCone );
- }
-*/
- if ( Vec_IntSize(vClass) < 2 || Gia_Iso2ManCheckIsoClass(p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1) )
+ if ( Vec_IntSize(vClass) < 2 || Gia_Iso2ManCheckIsoClassOneSkip(p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1) )
{
vClass2 = Vec_WecPushLevel( vEquivs2 );
*vClass2 = *vClass;
@@ -580,7 +590,6 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
}
else
{
-// printf( "Class %d failed.\n", i );
Vec_IntForEachEntry( vClass, Entry, k )
{
vClass2 = Vec_WecPushLevel( vEquivs2 );
@@ -596,6 +605,65 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
return vEquivs2;
}
+void Gia_Iso2ManCheckIsoClassOne( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Int_t * vNewClass )
+{
+ int i, k = 1, iPo;
+ Vec_IntClear( vNewClass );
+ if ( Vec_IntSize(vClass) <= 1 )
+ return;
+ assert( Vec_IntSize(vClass) > 1 );
+ iPo = Vec_IntEntry( vClass, 0 );
+ Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
+ Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+ {
+ Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
+ if ( Vec_IntSize(vVec0) == Vec_IntSize(vVec1) && Gia_Iso2ManCheckIsoPair(p, vVec0, vVec1, vMap0, vMap1) )
+ Vec_IntWriteEntry( vClass, k++, iPo );
+ else
+ Vec_IntPush( vNewClass, iPo );
+ }
+ Vec_IntShrink( vClass, k );
+}
+Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
+{
+ Vec_Wec_t * vEquivs2;
+ Vec_Int_t * vRoots = Vec_IntAlloc( 10000 );
+ Vec_Int_t * vVec0 = Vec_IntAlloc( 10000 );
+ Vec_Int_t * vVec1 = Vec_IntAlloc( 10000 );
+ Vec_Int_t * vMap0 = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vMap1 = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vClass, * vClass2, * vNewClass;
+ int i;
+ vNewClass = Vec_IntAlloc( 100 );
+ vEquivs2 = Vec_WecAlloc( 2 * Vec_WecSize(vEquivs) );
+ Vec_WecForEachLevel( vEquivs, vClass, i )
+ {
+ if ( i % 100 == 0 )
+ printf( "%8d finished...\r", i );
+ // split this class
+ Gia_Iso2ManCheckIsoClassOne( p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1, vNewClass );
+ assert( Vec_IntSize(vClass) > 0 );
+ // add remaining class
+ vClass2 = Vec_WecPushLevel( vEquivs2 );
+ *vClass2 = *vClass;
+ vClass->pArray = NULL;
+ vClass->nSize = vClass->nCap = 0;
+ // add new class
+ if ( Vec_IntSize(vNewClass) == 0 )
+ continue;
+ vClass = Vec_WecPushLevel( vEquivs );
+ Vec_IntAppend( vClass, vNewClass );
+ }
+ Vec_IntFree( vNewClass );
+ Vec_IntFree( vRoots );
+ Vec_IntFree( vVec0 );
+ Vec_IntFree( vVec1 );
+ Vec_IntFree( vMap0 );
+ Vec_IntFree( vMap1 );
+ return vEquivs2;
+}
+
+
/**Function*************************************************************
@@ -646,7 +714,7 @@ Vec_Wec_t * Gia_Iso2ManPerform( Gia_Man_t * pGia, int fVerbose )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fBetterQual, int fDualOut, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pPart;
Vec_Wec_t * vEquivs, * vEquivs2;
@@ -665,7 +733,10 @@ Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_P
return Gia_ManDup(pGia);
}
// verify classes
- vEquivs2 = Gia_Iso2ManCheckIsoClasses( pGia, vEquivs );
+ if ( fBetterQual )
+ vEquivs2 = Gia_Iso2ManCheckIsoClasses( pGia, vEquivs );
+ else
+ vEquivs2 = Gia_Iso2ManCheckIsoClassesSkip( pGia, vEquivs );
Vec_WecFree( vEquivs );
vEquivs = vEquivs2;
// sort equiv classes by the first integer
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 50c29b88..c9633158 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31542,9 +31542,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pAig;
Vec_Ptr_t * vPosEquivs;
// Vec_Ptr_t * vPiPerms;
- int c, fNewAlgo = 1, fEstimate = 0, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
+ int c, fNewAlgo = 1, fEstimate = 0, fBetterQual = 0, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "nedvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "neqdvwh" ) ) != EOF )
{
switch ( c )
{
@@ -31554,6 +31554,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e':
fEstimate ^= 1;
break;
+ case 'q':
+ fBetterQual ^= 1;
+ break;
case 'd':
fDualOut ^= 1;
break;
@@ -31580,7 +31583,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( fNewAlgo )
- pAig = Gia_ManIsoReduce2( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fDualOut, fVerbose, fVeryVerbose );
+ pAig = Gia_ManIsoReduce2( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fBetterQual, fDualOut, fVerbose, fVeryVerbose );
else
pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fDualOut, fVerbose, fVeryVerbose );
// pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, 0, fDualOut, fVerbose, fVeryVerbose );
@@ -31597,10 +31600,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &iso [-nedvwh]\n" );
+ Abc_Print( -2, "usage: &iso [-neqdvwh]\n" );
Abc_Print( -2, "\t removes POs with isomorphic sequential COI\n" );
Abc_Print( -2, "\t-n : toggle using new fast algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-e : toggle computing lower bound on equivalence classes [default = %s]\n", fEstimate? "yes": "no" );
+ Abc_Print( -2, "\t-q : toggle improving quality at the expense of runtime [default = %s]\n", fBetterQual? "yes": "no" );
Abc_Print( -2, "\t-d : toggle treating the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-09 10:06:18 +0000