Added supporting dual-output seq miters in &iso.

3 files changed, 48 insertions, 9 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 376488bd..2d465e86 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -752,7 +752,7 @@ extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
 /*=== 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, int fVerbose );
+extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fDualOut, int fVerbose );
 /*=== 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/giaIso.c b/src/aig/gia/giaIso.c
index c9ede676..89b8ac9c 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -775,7 +775,7 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
                 break;
         }
 
-        Gia_IsoReportTopmost( p );
+//        Gia_IsoReportTopmost( p );
 
         while ( Vec_IntSize(p->vClasses) > 0 )
         {
@@ -1063,19 +1063,33 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, int fDualOut, int fVerbose )
 { 
     int fVeryVerbose = 0;
-    Gia_Man_t * pPart;
+    Gia_Man_t * p, * pPart;
     Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
     Vec_Int_t * vRemain, * vLevel, * vLevel2;
     Vec_Str_t * vStr, * vStr2;
     int i, k, s, sStart, Entry, Counter, clk = clock();
 
+    if ( fDualOut )
+    {
+        assert( (Gia_ManPoNum(pInit) & 1) == 0 );
+        p = Gia_ManTransformMiter( pInit );
+        p = Gia_ManSeqStructSweep( pPart = p, 1, 1, 0 );
+        Gia_ManStop( pPart );
+    }
+    else
+        p = pInit;
+
     // create preliminary equivalences
     vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVeryVerbose );
     if ( vEquivs == NULL )
+    {
+        if ( fDualOut )
+            Gia_ManStop( p );
         return NULL;
+    }
 //    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
 //    Abc_PrintTime( 1, "Time", clock() - clk );
 
@@ -1126,11 +1140,32 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerb
     Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
         Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
 
+    if ( fDualOut )
+    {
+        Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vRemain) );
+        int i, Entry;
+        Vec_IntForEachEntry( vRemain, Entry, i )
+        {
+            printf( "%d ", Entry );
+            Vec_IntPush( vTemp, 2*Entry );
+            Vec_IntPush( vTemp, 2*Entry+1 );
+        }
+        printf( "\n" );
+        Vec_IntFree( vRemain );
+        vRemain = vTemp;
+        Gia_ManStop( p );
+        p = pInit;
+    }
+
+
     // derive the resulting AIG
     pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
     Vec_IntFree( vRemain );
     // report the results
-    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Gia_ManPoNum(pPart) );
+    if ( !fDualOut )
+        printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Gia_ManPoNum(pPart) );
+    else
+        printf( "Reduced %d dual outputs to %d dual outputs.  ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 );
     Abc_PrintTime( 1, "Time", clock() - clk );
     if ( fVerbose )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8b9a72bf..5fde1ca0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28338,12 +28338,15 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pAig;
     Vec_Ptr_t * vPosEquivs;
-    int c, fVerbose = 0;
+    int c, fDualOut = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'd':
+            fDualOut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -28363,7 +28366,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
         return 1;
     }
-    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fVerbose );
+    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fDualOut, fVerbose );
     if ( pAig == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Iso(): Transformation has failed.\n" );
@@ -28376,8 +28379,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &iso [-vh]\n" );
+    Abc_Print( -2, "usage: &iso [-dvh]\n" );
     Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
+    Abc_Print( -2, "\t-d     : treat 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-h     : print the command usage\n");
     return 1;