Added switch &sim -g to enable flop grouping.

2 files changed, 38 insertions, 1 deletions

diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index a05409ee..57bd91bf 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -105,6 +105,7 @@ struct Ssw_RarPars_t_
     int              fMiter;
     int              fUseCex;
     int              fLatchOnly;
+    int              fUseFfGrouping;
     int              nSolved;
     Abc_Cex_t *      pCex;
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 10e19b5a..214a3e3c 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1124,6 +1124,33 @@ finish:
 
 /**Function*************************************************************
 
+  Synopsis    [Derive random flop permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops )
+{
+    Vec_Int_t * vPerm;
+    int i, k, * pArray;
+    srand( 1 );
+    printf( "Generating random permutation of %d flops.\n", nFlops );
+    vPerm = Vec_IntStartNatural( nFlops );
+    pArray = Vec_IntArray( vPerm );
+    for ( i = 0; i < nFlops; i++ )
+    {
+        k = rand() % nFlops;
+        ABC_SWAP( int, pArray[i], pArray[k] );
+    }
+    return vPerm;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Perform sequential simulation.]
 
   Description []
@@ -1137,7 +1164,16 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
 {
     Aig_Man_t * pAig;
     int RetValue;
-    pAig = Gia_ManToAigSimple( p );
+    if ( pPars->fUseFfGrouping )
+    {
+        Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p) );
+        Gia_Man_t * pTemp = Gia_ManDupPermFlop( p, vPerm );
+        Vec_IntFree( vPerm );
+        pAig = Gia_ManToAigSimple( pTemp );
+        Gia_ManStop( pTemp );
+    }
+    else
+        pAig = Gia_ManToAigSimple( p );
     RetValue = Ssw_RarSimulate( pAig, pPars );
     // save counter-example
     Abc_CexFree( p->pCexSeq );