summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaDup.c3
-rw-r--r--src/aig/gia/giaEquiv.c133
-rw-r--r--src/base/abci/abc.c91
3 files changed, 225 insertions, 2 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 71204548..3672f7c3 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1345,6 +1345,9 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
+
+ pNew = Gia_ManDupNormalized( pTemp = pNew );
+ Gia_ManStop( pTemp );
return pNew;
}
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 383d4e8d..2e5b53ea 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -348,7 +348,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
if ( fVerbose )
{
int Ent;
-/*
+
printf( "Const0 = " );
Gia_ManForEachConst( p, i )
printf( "%d ", i );
@@ -356,7 +356,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 )
@@ -875,6 +875,135 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
return pNew;
}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces AIG using equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2 )
+{
+ Gia_Man_t * pGia1, * pGia2, * pMiter;
+ Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj;
+ int i, iObj, iNext, Counter = 0;
+ if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
+ {
+ printf( "Equivalences are not defined.\n" );
+ return 0;
+ }
+ pGia1 = Gia_ReadAiger( pName1, 0 );
+ if ( pGia1 == NULL )
+ {
+ printf( "Cannot read first file %s.\n", pName1 );
+ return 0;
+ }
+ pGia2 = Gia_ReadAiger( pName2, 0 );
+ if ( pGia2 == NULL )
+ {
+ Gia_ManStop( pGia2 );
+ printf( "Cannot read second file %s.\n", pName2 );
+ return 0;
+ }
+ pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 );
+ if ( pMiter == NULL )
+ {
+ Gia_ManStop( pGia1 );
+ Gia_ManStop( pGia2 );
+ printf( "Cannot create sequential miter.\n" );
+ return 0;
+ }
+ // make sure the miter is isomorphic
+ if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
+ {
+ Gia_ManStop( pGia1 );
+ Gia_ManStop( pGia2 );
+ Gia_ManStop( pMiter );
+ printf( "The number of objects in different.\n" );
+ return 0;
+ }
+ if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
+ {
+ Gia_ManStop( pGia1 );
+ Gia_ManStop( pGia2 );
+ Gia_ManStop( pMiter );
+ printf( "The AIG structure of the miter does not match.\n" );
+ return 0;
+ }
+ // transfer copies
+ Gia_ManCleanMark0( pGia );
+ Gia_ManForEachObj( pGia1, pObj1, i )
+ {
+ if ( pObj1->Value == ~0 )
+ continue;
+ pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) );
+ pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
+ pObj->fMark0 = 1;
+ }
+ Gia_ManCleanMark1( pGia );
+ Gia_ManForEachObj( pGia2, pObj2, i )
+ {
+ if ( pObj2->Value == ~0 )
+ continue;
+ pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) );
+ pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
+ pObj->fMark1 = 1;
+ }
+
+ // filter equivalences
+ Gia_ManForEachConst( pGia, i )
+ {
+ Gia_ObjUnsetRepr( pGia, i );
+ assert( pGia->pNexts[i] == 0 );
+ }
+ Gia_ManForEachClass( pGia, i )
+ {
+ // find the first colorA and colorB
+ int ClassA = -1, ClassB = -1;
+ Gia_ClassForEachObj( pGia, i, iObj )
+ {
+ pObj = Gia_ManObj( pGia, iObj );
+ if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 )
+ ClassA = iObj;
+ if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 )
+ ClassB = iObj;
+ }
+ // undo equivalence classes
+ for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
+ iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
+ {
+ Gia_ObjUnsetRepr( pGia, iObj );
+ Gia_ObjSetNext( pGia, iObj, 0 );
+ }
+ assert( !Gia_ObjIsHead(pGia, i) );
+ if ( ClassA > 0 && ClassB > 0 )
+ {
+ if ( ClassA > ClassB )
+ {
+ ClassA ^= ClassB;
+ ClassB ^= ClassA;
+ ClassA ^= ClassB;
+ }
+ assert( ClassA < ClassB );
+ Gia_ObjSetNext( pGia, ClassA, ClassB );
+ Gia_ObjSetRepr( pGia, ClassB, ClassA );
+ Counter++;
+ assert( Gia_ObjIsHead(pGia, ClassA) );
+ }
+ }
+ printf( "The number of two-node classes after filtering = %d.\n", Counter );
+//Gia_ManEquivPrintClasses( pGia, 1, 0 );
+
+ Gia_ManCleanMark0( pGia );
+ Gia_ManCleanMark1( pGia );
+ return 1;
+}
+
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 41aea7b1..3a900d28 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -356,6 +356,7 @@ static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Srm2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -771,6 +772,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&srm2", Abc_CommandAbc9Srm2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 );
@@ -26262,6 +26264,95 @@ usage:
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2 );
+ char pFileName[10], * pFileName1, * pFileName2;
+ Gia_Man_t * pTemp, * pAux;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Srm2(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( pAbc->pGia->pReprs == NULL || pAbc->pGia->pNexts == NULL )
+ {
+ Abc_Print( -1, "Equivalences are not defined.\n" );
+ return 0;
+ }
+ if ( argc != globalUtilOptind + 2 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Srm2(): Expecting two file names on the command line.\n" );
+ return 1;
+ }
+ // get the input file name
+ pFileName1 = argv[globalUtilOptind];
+ pFileName2 = argv[globalUtilOptind+1];
+ // create file name
+ sprintf( pFileName, "gsrm.aig" );
+ pTemp = Gia_ManDup( pAbc->pGia );
+ // copy equivalences
+ pTemp->pReprs = ABC_ALLOC( Gia_Rpr_t, Gia_ManObjNum(pTemp) );
+ memcpy( pTemp->pReprs, pAbc->pGia->pReprs, sizeof(Gia_Rpr_t) * Gia_ManObjNum(pTemp) );
+ pTemp->pNexts = ABC_ALLOC( int, Gia_ManObjNum(pTemp) );
+ memcpy( pTemp->pNexts, pAbc->pGia->pNexts, sizeof(int) * Gia_ManObjNum(pTemp) );
+//Gia_ManPrintStats( pTemp, 0 );
+ // filter the classes
+ if ( !Gia_ManFilterEquivsForSpeculation( pTemp, pFileName1, pFileName2 ) )
+ {
+ Gia_ManStop( pTemp );
+ Abc_Print( -1, "Filtering equivalences has failed.\n" );
+ return 1;
+ }
+//Gia_ManPrintStats( pTemp, 0 );
+ pTemp = Gia_ManSpecReduce( pAux = pTemp, 0, 0, 1, 0, 0 );
+ Gia_ManStop( pAux );
+ if ( pTemp )
+ {
+ pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
+ Gia_ManStop( pAux );
+
+ Gia_WriteAiger( pTemp, pFileName, 0, 0 );
+ Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
+ Gia_ManPrintStatsShort( pTemp );
+ Gia_ManStop( pTemp );
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &srm2 [-vh]\n" );
+ Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
Synopsis []
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-17 06:41:44 +0000