Added switch &sim -g to enable flop grouping.

src/aig/gia/gia.h

@@ -901,6 +901,7 @@ extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
 extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
 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 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 );

src/aig/gia/giaDup.c

@@ -589,6 +589,42 @@ Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm )
+{
+    Vec_Int_t * vLits;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Vec_IntSize(vFfPerm) == 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_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+
+    vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        Vec_IntPush( vLits, Gia_ManRo(p, Vec_IntEntry(vFfPerm, i))->Value );
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Vec_IntEntry(vLits, i);
+
+    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) );
+
+    Vec_IntClear( vLits );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        Vec_IntPush( vLits, Gia_ObjFanin0Copy( Gia_ManRi(p, Vec_IntEntry(vFfPerm, i)) ) );
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vLits, i) );
+    Vec_IntFree( vLits );
+
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
 
 /**Function*************************************************************
 

src/base/abci/abc.c

@@ -26008,7 +26008,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     Ssw_RarSetDefaultParams( pPars );
     // parse command line
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGgvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26100,6 +26100,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->TimeOutGap < 0 )
                 goto usage;
             break;
+        case 'g':
+            pPars->fUseFfGrouping ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26120,7 +26123,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-gvh]\n" );
     Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n",       pPars->nFrames );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",        pPars->nWords );
@@ -26129,6 +26132,7 @@ usage:
     Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n",  pPars->nRestart );
     Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n",  pPars->nRandSeed );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n",   pPars->TimeOut );
+    Abc_Print( -2, "\t-g     : toggle heuristic flop grouping [default = %s]\n",    pPars->fUseFfGrouping? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",    pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

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

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 );