Added new switched to command &frames.

3 files changed, 60 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c184950e..12d255a4 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -205,6 +205,8 @@ struct Gia_ParFra_t_
     int            nFrames;       // the number of frames to unroll
     int            fInit;         // initialize the timeframes
     int            fSaveLastLit;  // adds POs for outputs of each frame
+    int            fDisableSt;    // disables strashing
+    int            fOrPos;        // ORs respective POs in each timeframe
     int            fVerbose;      // enables verbose output
 };
 
@@ -513,6 +515,18 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     }
     return Gia_ObjId( p, pObj ) << 1;
 }
+static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )  
+{ 
+    if ( iLit0 < 2 )
+        return iLit0 ? iLit1 : 0;
+    if ( iLit1 < 2 )
+        return iLit1 ? iLit0 : 0;
+    if ( iLit0 == iLit1 )
+        return iLit1;
+    if ( iLit0 == Abc_LitNot(iLit1) )
+        return 0;
+    return Gia_ManAppendAnd( p, iLit0, iLit1 );
+}
 static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index a62d17ca..b19e223b 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -864,15 +864,19 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
 {
     Gia_Man_t * pFrames, * pTemp;
     Gia_Obj_t * pObj;
+    Vec_Int_t * vPoLits = NULL;
     int i, f;
     assert( Gia_ManRegNum(pAig) > 0 );
     assert( pPars->nFrames > 0 );
     if ( pPars->fInit )
         return Gia_ManFramesInit( pAig, pPars );
+    if ( pPars->fOrPos )
+        vPoLits = Vec_IntStart( Gia_ManPoNum(pAig) );
     pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
     pFrames->pName = Abc_UtilStrsav( pAig->pName );
     pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
-    Gia_ManHashAlloc( pFrames );
+    if ( !pPars->fDisableSt )
+        Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; f < pPars->nFrames; f++ )
     {
@@ -888,12 +892,31 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
         }
         Gia_ManForEachPi( pAig, pObj, i )
             pObj->Value = Gia_ManAppendCi( pFrames );
-        Gia_ManForEachAnd( pAig, pObj, i )
-            pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        Gia_ManForEachPo( pAig, pObj, i )
-            pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
+        if ( !pPars->fDisableSt )
+            Gia_ManForEachAnd( pAig, pObj, i )
+                pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
+            Gia_ManForEachAnd( pAig, pObj, i )
+                pObj->Value = Gia_ManAppendAnd2( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( vPoLits )
+        {
+            if ( !pPars->fDisableSt )
+                Gia_ManForEachPo( pAig, pObj, i )
+                    Vec_IntWriteEntry( vPoLits, i, Gia_ManHashOr(pFrames, Vec_IntEntry(vPoLits, i), Gia_ObjFanin0Copy(pObj)) );
+            else
+                Gia_ManForEachPo( pAig, pObj, i )
+                    Vec_IntWriteEntry( vPoLits, i, Abc_LitNot(Gia_ManAppendAnd2(pFrames, Abc_LitNot(Vec_IntEntry(vPoLits, i)), Abc_LitNot(Gia_ObjFanin0Copy(pObj)))) );
+        }
+        else
+        {
+            Gia_ManForEachPo( pAig, pObj, i )
+                pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
+        }
         if ( f == pPars->nFrames - 1 )
         {
+            if ( vPoLits )
+                Gia_ManForEachPo( pAig, pObj, i )
+                    pObj->Value = Gia_ManAppendCo( pFrames, Vec_IntEntry(vPoLits, i) );
             Gia_ManForEachRi( pAig, pObj, i )
                 pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
         }
@@ -903,7 +926,9 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
                 pObj->Value = Gia_ObjFanin0Copy(pObj);
         }
     }
-    Gia_ManHashStop( pFrames );
+    Vec_IntFreeP( &vPoLits );
+    if ( !pPars->fDisableSt )
+        Gia_ManHashStop( pFrames );
     Gia_ManFraTransformCis( pAig, pFrames->vCis );
     Gia_ManSetRegNum( pFrames, Gia_ManRegNum(pAig) );
     if ( Gia_ManCombMarkUsed(pFrames) < Gia_ManAndNum(pFrames) )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b93dd29b..5c8b4a7f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26219,11 +26219,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ParFra_t Pars, * pPars = &Pars;
     int c;
     int nCofFanLit = 0;
-    int fNewAlgo = 1;
+    int fNewAlgo = 0;
     int fInitSpecial = 0;
     Gia_ManFraSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FLsoibavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26249,15 +26249,21 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCofFanLit < 0 )
                 goto usage;
             break;
+        case 's':
+            pPars->fDisableSt ^= 1;
+            break;
+        case 'o':
+            pPars->fOrPos ^= 1;
+            break;
         case 'i':
             pPars->fInit ^= 1;
             break;
+        case 'b':
+            fInitSpecial ^= 1;
+            break;
         case 'a':
             fNewAlgo ^= 1;
             break;
-        case 's':
-            fInitSpecial ^= 1;
-            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26289,13 +26295,15 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &frames [-FL <num>] [-iasvh]\n" );
+    Abc_Print( -2, "usage: &frames [-FL <num>] [-soibavh]\n" );
     Abc_Print( -2, "\t         unrolls the design for several timeframes\n" );
     Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
     Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
+    Abc_Print( -2, "\t-s     : toggle disabling structural hashing [default = %s]\n", pPars->fDisableSt? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle ORing corresponding POs [default = %s]\n", pPars->fOrPos? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "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;