4 files changed, 79 insertions, 3 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f356b1da..7653dc62 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -902,6 +902,7 @@ extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex,
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
 extern Gia_Man_t *         Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm );
+extern Gia_Man_t *         Gia_ManDupPermFlopGap( Gia_Man_t * p, Vec_Int_t * vFfPerm );
 extern void                Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo );
 extern void                Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo );
 extern Gia_Man_t *         Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 74227531..85af8748 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -615,6 +615,51 @@ Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupSpreadFlop( Gia_Man_t * p, Vec_Int_t * vFfMask )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, k, Entry;
+    assert( Vec_IntSize(vFfMask) >= Gia_ManRegNum(p) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    k = 0;
+    Vec_IntForEachEntry( vFfMask, Entry, i )
+        if ( Entry == -1 )
+            Gia_ManAppendCi(pNew);
+        else
+            Gia_ManRo(p, k++)->Value = Gia_ManAppendCi(pNew);
+    assert( k == Gia_ManRegNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    k = 0;
+    Vec_IntForEachEntry( vFfMask, Entry, i )
+        if ( Entry == -1 )
+            Gia_ManAppendCo( pNew, 0 );
+        else
+        {
+            pObj = Gia_ManRi( p, k++ );
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        }
+    assert( k == Gia_ManRegNum(p) );
+    Gia_ManSetRegNum( pNew, Vec_IntSize(vFfMask) );
+    return pNew;
+}
+Gia_Man_t * Gia_ManDupPermFlopGap( Gia_Man_t * p, Vec_Int_t * vFfMask )
+{
+    Vec_Int_t * vPerm = Vec_IntCondense( vFfMask, -1 );
+    Gia_Man_t * pPerm = Gia_ManDupPermFlop( p, vPerm );
+    Gia_Man_t * pSpread = Gia_ManDupSpreadFlop( pPerm, vFfMask );
+    Vec_IntFree( vPerm );
+    Gia_ManStop( pPerm );
+    return pSpread;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index c821d121..2cba9f14 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1054,6 +1054,27 @@ static inline Vec_Int_t * Vec_IntInvert( Vec_Int_t * p, int Fill )
   SeeAlso     []
 
 ***********************************************************************/
+static inline Vec_Int_t * Vec_IntCondense( Vec_Int_t * p, int Fill ) 
+{
+    int Entry, i;
+    Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(p) );
+    Vec_IntForEachEntry( p, Entry, i )
+        if ( Entry != Fill )
+            Vec_IntPush( vRes, Entry );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_IntSum( Vec_Int_t * p ) 
 {
     int i, Counter = 0;
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 214a3e3c..e5640f6a 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1133,7 +1133,7 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops )
+Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops, int nUnused )
 {
     Vec_Int_t * vPerm;
     int i, k, * pArray;
@@ -1146,6 +1146,15 @@ Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops )
         k = rand() % nFlops;
         ABC_SWAP( int, pArray[i], pArray[k] );
     }
+    printf( "Randomly adding %d unused flops.\n", nUnused );
+    for ( i = 0; i < nUnused; i++ )
+    {
+        k = rand() % Vec_IntSize(vPerm);
+        Vec_IntPush( vPerm, -1 );
+        pArray = Vec_IntArray( vPerm );
+        ABC_SWAP( int, pArray[Vec_IntSize(vPerm)-1], pArray[k] );
+    }
+//    Vec_IntPrint(vPerm);
     return vPerm;
 }
 
@@ -1166,8 +1175,8 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
     int RetValue;
     if ( pPars->fUseFfGrouping )
     {
-        Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p) );
-        Gia_Man_t * pTemp = Gia_ManDupPermFlop( p, vPerm );
+        Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p), 10 );
+        Gia_Man_t * pTemp = Gia_ManDupPermFlopGap( p, vPerm );
         Vec_IntFree( vPerm );
         pAig = Gia_ManToAigSimple( pTemp );
         Gia_ManStop( pTemp );