Implemented additional filtering of equivalences (&srm -sf).

4 files changed, 108 insertions, 32 deletions

diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 269c42c0..5cb3bf98 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         // write equivalence classes
         Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
         // reduce the model
-        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0 );
+        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c4d41459..b3d23ee2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -659,7 +659,7 @@ extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose
 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 );
-extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fVerbose );
+extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut );
 extern Gia_Man_t *         Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 170830ee..cfebd3a6 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 )
+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 )
 {
     Gia_Obj_t * pRepr;
     unsigned iLitNew;
@@ -760,7 +760,14 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
         return;
     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) );
+    }
+    else
+    {
+        if ( vTrace ) Vec_IntPush( vTrace, 0 );
+    }
     if ( fSpeculate )
         pObj->Value = iLitNew;
 }
@@ -799,15 +806,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 )
+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 )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate );
+    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace );
 }
 
 /**Function*************************************************************
@@ -821,36 +828,77 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fVerbose )
+Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
 {
+    Vec_Int_t * vXorLits;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    Vec_Int_t * vXorLits;
     int i, iLitNew;
     if ( !p->pReprs )
     {
         printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
         return NULL;
     }
-    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    Vec_IntClear( vTrace );
+    vXorLits = Vec_IntAlloc( 1000 );
+    Gia_ManSetPhase( p );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    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_ManForEachCo( p, pObj, i )
+        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Vec_IntForEachEntry( vXorLits, iLitNew, i )
+        Gia_ManAppendCo( pNew, iLitNew );
+    if ( Vec_IntSize(vXorLits) == 0 )
     {
-        printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
-        return NULL;
+        printf( "Speculatively reduced model has no primary outputs.\n" );
+        Gia_ManAppendCo( pNew, 0 );
     }
-/*
-    if ( Gia_ManHasNoEquivs(p) )
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Vec_IntFree( vXorLits );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces AIG using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vXorLits;
+    int i, iLitNew;
+    if ( !p->pReprs )
     {
-        printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
+        printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
         return NULL;
     }
-*/
-/*
-    if ( !Gia_ManCheckTopoOrder( p ) )
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
     {
-        printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" );
+        printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
-*/
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
@@ -863,9 +911,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 );
+        Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, NULL );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
+        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, NULL );
     if ( !fSynthesis )
     {
         Gia_ManForEachPo( p, pObj, i )
@@ -885,6 +933,29 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
+
+    // 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 = 0;
+            pObj->iDiff0 = Gia_ObjId( pNew, pObj );
+        }
+        Vec_IntFreeP( &vTrace );
+        pNew = Gia_ManCleanup( pTemp = pNew );
+        Gia_ManStop( pTemp );
+    }
     return pNew;
 }
 
@@ -1591,7 +1662,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
             printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
             break;
         }
-        pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); 
+        pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 ); 
         // bmc2 -F 100 -C 25000
         {
             Abc_Cex_t * pCex;
@@ -1628,7 +1699,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
         // write equivalence classes
         Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
         // reduce the model
-        pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 );
+        pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index eba34d62..1b9d8ab9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25941,22 +25941,26 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     char pFileName[10], pFileName2[10];
     Gia_Man_t * pTemp, * pAux;
     int c, fVerbose = 0;
-    int fSpeculate = 1;
     int fSynthesis = 0;
+    int fSpeculate = 1;
+    int fSkipSome = 0;
     int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dsrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "drsfvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'd':
             fDualOut ^= 1;
             break;
+        case 'r':
+            fSynthesis ^= 1;
+            break;
         case 's':
             fSpeculate ^= 1;
             break;
-        case 'r':
-            fSynthesis ^= 1;
+        case 'f':
+            fSkipSome ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -25974,7 +25978,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     } 
     sprintf( pFileName,  "gsrm%s.aig", fSpeculate? "" : "s" );
     sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" );
-    pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fVerbose );
+    pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fSkipSome, fVerbose );
     if ( pTemp )
     {
         if ( fSpeculate )
@@ -26004,11 +26008,12 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &srm [-dsrvh]\n" );
+    Abc_Print( -2, "usage: &srm [-drsfvh]\n" );
     Abc_Print( -2, "\t         writes speculatively reduced model into file \"%s\"\n", pFileName );
     Abc_Print( -2, "\t-d     : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
+    Abc_Print( -2, "\t-f     : toggle filtering to remove redundant 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");
     return 1;
@@ -26127,7 +26132,7 @@ usage:
     Abc_Print( -2, "\t-h          : print the command usage\n");
     Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n");
     Abc_Print( -2, "\t              \n" );
-    Abc_Print( -2, "\t              The external miter should be generated by &srm -m\n" );
+    Abc_Print( -2, "\t              The external miter should be generated by &srm -s\n" );
     Abc_Print( -2, "\t              and (partially) solved by any verification engine(s).\n" );
     Abc_Print( -2, "\t              The external miter should have as many POs as\n" );
     Abc_Print( -2, "\t              the number of POs in the current AIG plus\n" );