Experiment with partitioned &scorr.

2 files changed, 200 insertions, 6 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index a485b147..e868e3ae 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -21,6 +21,7 @@
 #include "gia.h"
 #include "misc/tim/tim.h"
 #include "misc/vec/vecWec.h"
+#include "proof/cec/cec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -4581,6 +4582,190 @@ int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 )
     return 1;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts "half" of the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupHalfSeq( Gia_Man_t * p, int fSecond )
+{
+    int i; Gia_Obj_t * pObj;
+    Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) ); 
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue(p);
+    Gia_ManConst0(p)->Value = 0;
+    if ( fSecond )
+    {
+        Gia_ManForEachCi( p, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachPo( p, pObj, i )
+            Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+        Gia_ManForEachRi( p, pObj, i )
+            if ( i >= Gia_ManRegNum(p)/2 )
+                Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+        Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)- Gia_ManRegNum(p)/2 );
+    }
+    else
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachRo( p, pObj, i )
+            if ( i >= Gia_ManRegNum(p)/2 )
+                pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachRo( p, pObj, i )
+            if ( i < Gia_ManRegNum(p)/2 )
+                pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachPo( p, pObj, i )
+            Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+        Gia_ManForEachRi( p, pObj, i )
+            if ( i < Gia_ManRegNum(p)/2 )
+                Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+        Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)/2 );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merge two sets of sequential equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSeqEquivMerge( Gia_Man_t * p, Gia_Man_t * pPart[2] )
+{
+    int i, iObj, * pClasses    = ABC_FALLOC( int, Gia_ManObjNum(p) );
+    int n, Repr, * pClass2Repr = ABC_FALLOC( int, Gia_ManObjNum(p) );
+    // initialize equiv class representation in the big AIG
+    assert( p->pReprs  == NULL && p->pNexts  == NULL );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    // map equivalences of p into classes
+    pClasses[0] = 0;
+    for ( n = 0; n < 2; n++ )
+    {
+        assert( pPart[n]->pReprs != NULL && pPart[n]->pNexts != NULL );
+        for ( i = 0; i < Gia_ManObjNum(pPart[n]); i++ )
+            if ( Gia_ObjRepr(pPart[n], i) == 0 )
+                pClasses[Gia_ManObj(pPart[n], i)->Value] = 0;
+        Gia_ManForEachClass( pPart[n], i )
+        {
+            Repr = Gia_ManObj(pPart[n], i)->Value;
+            if ( n == 1 )
+            {
+                Gia_ClassForEachObj( pPart[n], i, iObj )
+                    if ( pClasses[Gia_ManObj(pPart[n], iObj)->Value] != -1 )
+                        Repr = pClasses[Gia_ManObj(pPart[n], iObj)->Value];
+            }
+            Gia_ClassForEachObj( pPart[n], i, iObj )
+                pClasses[Gia_ManObj(pPart[n], iObj)->Value] = Repr;
+        }
+    }
+    // map representatives of each class
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        if ( pClasses[i] != -1 && pClass2Repr[pClasses[i]] == -1 )
+        {
+            pClass2Repr[pClasses[i]] = i;
+            pClasses[i] = -1;
+        }
+    // remap the remaining classes
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        if ( pClasses[i] != -1 )
+            p->pReprs[i].iRepr = pClass2Repr[pClasses[i]];
+    ABC_FREE(pClasses);
+    ABC_FREE(pClass2Repr);
+    // create next pointers
+    p->pNexts = Gia_ManDeriveNexts( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintEquivs( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i, iObj;
+    printf( "Const0:" );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjRepr(p, i) == 0 )
+            printf( " %d", i );
+    printf( "\n" );
+    Gia_ManForEachClass( p, i )
+    {
+        printf( "%d:", i );
+        Gia_ClassForEachObj1( p, i, iObj )
+            printf( " %d", iObj );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing seq equivs by dividing AIG into two parts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSeqEquivDivide( Gia_Man_t * p, Cec_ParCor_t * pPars )
+{
+    Gia_Man_t * pParts[2];
+    Gia_Obj_t * pObj;
+    int n, i;
+    for ( n = 0; n < 2; n++ )
+    {
+        // derive n-th part of the AIG
+        pParts[n] = Gia_ManDupHalfSeq( p, n );
+        //Gia_ManPrintStats( pParts[n], NULL );
+        // compute equivalences (recorded internally using pReprs and pNexts)
+        Cec_ManLSCorrespondenceClasses( pParts[n], pPars );
+        // make the nodes of the part AIG point to their prototypes in the AIG
+        Gia_ManForEachObj( p, pObj, i )
+            if ( ~pObj->Value )
+                Gia_ManObj( pParts[n], Abc_Lit2Var(pObj->Value) )->Value = i;
+    }
+    Gia_ManSeqEquivMerge( p, pParts );
+    Gia_ManStop( pParts[0] );
+    Gia_ManStop( pParts[1] );
+}
+Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars )
+{
+    extern Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p );
+    Gia_Man_t * pNew, * pTemp;
+    ABC_FREE( p->pReprs ); p->pReprs = NULL;
+    ABC_FREE( p->pNexts ); p->pNexts = NULL;
+    Gia_ManSeqEquivDivide( p, pPars );
+    //Gia_ManPrintEquivs( p );
+    pNew = Gia_ManCorrReduce( p );
+    pNew = Gia_ManSeqCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ddce35ff..742c0802 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13162,7 +13162,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nLeafMax     =  4;
     int nDivMax      =  2;
     int nDecMax      =  3;
-    int nNumOnes     =  4;
+    int nNumOnes     =  0;
     int fNewAlgo     =  0;
     int fNewOrder    =  0;
     int fVerbose     =  0;
@@ -13367,7 +13367,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 //    Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
     //Dau_NetworkEnumTest();
-    //Extra_DigitsDumpGiaTest();
+    //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -34036,12 +34036,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
     Cec_ParCor_t Pars, * pPars = &Pars;
     Gia_Man_t * pTemp;
+    int fPartition = 0;
     int c;
     Cec_ManCorSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPkrecqwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPpkrecqwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -34078,6 +34080,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nPrefix < 0 )
                 goto usage;
             break;
+        case 'p':
+            fPartition ^= 1;
+            break;
         case 'k':
             pPars->fConstCorr ^= 1;
             break;
@@ -34124,16 +34129,20 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 0, "The network is combinational.\n" );
         return 0;
     }
-    pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
+    if ( fPartition )
+        pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
+    else
+        pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &scorr [-FCP num] [-krecqwvh]\n" );
+    Abc_Print( -2, "usage: &scorr [-FCP num] [-pkrecqwvh]\n" );
     Abc_Print( -2, "\t         performs signal correpondence computation\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
     Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
+    Abc_Print( -2, "\t-p     : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
     Abc_Print( -2, "\t-k     : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
@@ -45571,7 +45580,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 //    pTemp = Slv_ManToAig( pAbc->pGia );
 //    Abc_FrameUpdateGia( pAbc, pTemp );
-    Abc_BddGiaTest( pAbc->pGia, fVerbose );
+//    Extra_TestGia2( pAbc->pGia );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );