summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaEquiv.c140
-rw-r--r--src/base/abci/abc.c15
2 files changed, 102 insertions, 53 deletions
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 44e8f876..ba34fc6b 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace )
+static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide )
{
Gia_Obj_t * pRepr;
unsigned iLitNew;
@@ -761,12 +761,15 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
{
- if ( vTrace ) Vec_IntPush( vTrace, 1 );
- Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
+ if ( vTrace )
+ Vec_IntPush( vTrace, 1 );
+ if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
}
else
{
- if ( vTrace ) Vec_IntPush( vTrace, 0 );
+ if ( vTrace )
+ Vec_IntPush( vTrace, 0 );
}
if ( fSpeculate )
pObj->Value = iLitNew;
@@ -806,15 +809,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace )
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
- Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace );
+ Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
}
/**Function*************************************************************
@@ -850,9 +853,9 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
- Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace );
+ Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vXorLits, iLitNew, i )
@@ -889,6 +892,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_Obj_t * pObj;
Vec_Int_t * vXorLits;
int i, iLitNew;
+ Vec_Int_t * vTrace = NULL, * vGuide = NULL;
if ( !p->pReprs )
{
printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
@@ -899,6 +903,14 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
+ if ( fSkipSome )
+ {
+ vGuide = Vec_IntAlloc( 100 );
+ pTemp = Gia_ManSpecReduceTrace( p, vGuide );
+ Gia_ManStop( pTemp );
+ assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) );
+ vTrace = Vec_IntAlloc( 100 );
+ }
vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
@@ -911,9 +923,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
- Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, NULL );
+ Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, NULL );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
if ( !fSynthesis )
{
Gia_ManForEachPo( p, pObj, i )
@@ -937,25 +949,15 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
// update using trace
if ( fSkipSome )
{
- Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
- int iLit, nLitNum = Gia_ManEquivCountLitsAll(p);
- pTemp = Gia_ManSpecReduceTrace( p, vTrace );
- Gia_ManStop( pTemp );
- assert( Vec_IntSize(vTrace) == nLitNum );
- assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nLitNum );
- iLit = Gia_ManPoNum(p);
- for ( i = 0; i < nLitNum; i++ )
- {
- if ( Vec_IntEntry( vTrace, i ) == 0 )
- continue;
- pObj = Gia_ManPo( pNew, Gia_ManPoNum(p) + i );
- pObj->fCompl0 = 1;
- pObj->iDiff0 = Gia_ObjId( pNew, pObj );
- }
- Vec_IntFreeP( &vTrace );
- pNew = Gia_ManCleanup( pTemp = pNew );
- Gia_ManStop( pTemp );
+ // count the number of non-zero entries
+ int iLit, nAddPos = 0;
+ Vec_IntForEachEntry( vGuide, iLit, i )
+ if ( iLit )
+ nAddPos++;
+ assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nAddPos );
}
+ Vec_IntFreeP( &vTrace );
+ Vec_IntFreeP( &vGuide );
return pNew;
}
@@ -1208,11 +1210,11 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose )
+void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose )
{
- Gia_Man_t * pMiter;
+ Gia_Man_t * pMiter, * pTemp;
Gia_Obj_t * pObj;
- int i, nLits = 0;
+ int i, iLit, nAddPos, nLits = 0;
int nLitsAll, Counter = 0;
nLitsAll = Gia_ManEquivCountLitsAll( p );
if ( nLitsAll == 0 )
@@ -1227,29 +1229,71 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose )
printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
return;
}
- if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
+ if ( fSkipSome )
{
- printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
- Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
- Gia_ManStop( pMiter );
- return;
+ Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
+ pTemp = Gia_ManSpecReduceTrace( p, vTrace );
+ Gia_ManStop( pTemp );
+ assert( Vec_IntSize(vTrace) == nLitsAll );
+ // count the number of non-zero entries
+ nAddPos = 0;
+ Vec_IntForEachEntry( vTrace, iLit, i )
+ if ( iLit )
+ nAddPos++;
+ // check the number
+ if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos )
+ {
+ printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
+ Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos );
+ Gia_ManStop( pMiter );
+ Vec_IntFreeP( &vTrace );
+ return;
+ }
+ // mark corresponding POs as solved
+ nLits = iLit = Counter = 0;
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjRepr(p, i) == GIA_VOID )
+ continue;
+ if ( Vec_IntEntry( vTrace, nLits++ ) == 0 )
+ continue;
+ pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + iLit++ );
+ if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
+ {
+ Gia_ObjSetProved(p, i);
+ Counter++;
+ }
+ }
+ assert( nLits == nLitsAll );
+ assert( iLit == nAddPos );
+ Vec_IntFreeP( &vTrace );
}
- // mark corresponding POs as solved
- nLits = 0;
- for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ else
{
- if ( Gia_ObjRepr(p, i) == GIA_VOID )
- continue;
- pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
- if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
+ if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
{
- Gia_ObjSetProved(p, i);
- Counter++;
+ printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
+ Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
+ Gia_ManStop( pMiter );
+ return;
+ }
+ // mark corresponding POs as solved
+ nLits = 0;
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjRepr(p, i) == GIA_VOID )
+ continue;
+ pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
+ if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
+ {
+ Gia_ObjSetProved(p, i);
+ Counter++;
+ }
}
+ assert( nLits == nLitsAll );
}
if ( fVerbose )
printf( "Set %d equivalences as proved.\n", Counter );
- assert( nLits == nLitsAll );
Gia_ManStop( pMiter );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1b9d8ab9..9890dbcf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25938,7 +25938,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- char pFileName[10], pFileName2[10];
+ char pFileName[10] = "gsrm.aig", pFileName2[10] = "gsyn.aig";
Gia_Man_t * pTemp, * pAux;
int c, fVerbose = 0;
int fSynthesis = 0;
@@ -26095,14 +26095,18 @@ usage:
***********************************************************************/
int Abc_CommandAbc9EquivMark( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose );
+ extern void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose );
char * pFileName;
int c, fVerbose = 0;
+ int fSkipSome = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
{
switch ( c )
{
+ case 'f':
+ fSkipSome ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -26122,12 +26126,13 @@ int Abc_CommandAbc9EquivMark( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the input file name
pFileName = argv[globalUtilOptind];
// mark equivalences
- Gia_ManEquivMark( pAbc->pGia, pFileName, fVerbose );
+ Gia_ManEquivMark( pAbc->pGia, pFileName, fSkipSome, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &equiv_mark [-vh] <miter.aig>\n" );
+ Abc_Print( -2, "usage: &equiv_mark [-fvh] <miter.aig>\n" );
Abc_Print( -2, "\t marks equivalences using an external miter\n" );
+ Abc_Print( -2, "\t-f : toggle the use of filtered equivalences [default = %s]\n", fSkipSome? "yes": "no" );
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");
Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n");
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-16 14:17:44 +0000