From 1ad363c1566bd878bd71f9032f446506efcbcc9a Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 20 Aug 2013 08:46:31 -0700
Subject: Added switch &sim -g to enable flop grouping.

---
 src/proof/ssw/ssw.h       |  1 +
 src/proof/ssw/sswRarity.c | 38 +++++++++++++++++++++++++++++++++++++-
 2 files changed, 38 insertions(+), 1 deletion(-)

(limited to 'src/proof/ssw')

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
@@ -1122,6 +1122,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.]
@@ -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 );
-- 
cgit v1.2.3