Added DSD-based collapsing &dsd.

2 files changed, 381 insertions, 4 deletions

diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c
new file mode 100644
index 00000000..04469773
--- /dev/null
+++ b/src/aig/gia/giaClp.c
@@ -0,0 +1,372 @@
+/**CFile****************************************************************
+
+  FileName    [giaClp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Collapsing AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/extra/extraBdd.h"
+#include "bdd/dsd/dsd.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
+extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern int Abc_NtkDeriveFlatGiaSop( Gia_Man_t * pGia, int * gFanins, char * pSop );
+extern Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames );
+extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManRebuildIsop( DdManager * dd, DdNode * bLocal, Gia_Man_t * pNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
+{
+    char * pSop;
+    DdNode * bCover, * zCover, * zCover0, * zCover1;
+    int nFanins = Vec_IntSize(vFanins);
+    int fPhase, nCubes, nCubes0, nCubes1;
+
+    // get the ZDD of the negative polarity
+    bCover = Cudd_zddIsop( dd, Cudd_Not(bLocal), Cudd_Not(bLocal), &zCover0 );
+    Cudd_Ref( zCover0 );
+    Cudd_Ref( bCover );
+    Cudd_RecursiveDeref( dd, bCover );
+    nCubes0 = Abc_CountZddCubes( dd, zCover0 );
+
+    // get the ZDD of the positive polarity
+    bCover = Cudd_zddIsop( dd, bLocal, bLocal, &zCover1 );
+    Cudd_Ref( zCover1 );
+    Cudd_Ref( bCover );
+    Cudd_RecursiveDeref( dd, bCover );
+    nCubes1 = Abc_CountZddCubes( dd, zCover1 );
+
+    // compare the number of cubes
+    if ( nCubes1 <= nCubes0 )
+    { // use positive polarity
+        nCubes = nCubes1;
+        zCover = zCover1;
+        Cudd_RecursiveDerefZdd( dd, zCover0 );
+        fPhase = 1;
+    }
+    else
+    { // use negative polarity
+        nCubes = nCubes0;
+        zCover = zCover0;
+        Cudd_RecursiveDerefZdd( dd, zCover1 );
+        fPhase = 0;
+    }
+    if ( nCubes > 1000 )
+    {
+        Cudd_RecursiveDerefZdd( dd, zCover );
+        return -1;
+    }
+
+    // allocate memory for the cover
+    Vec_StrGrow( vSop, (nFanins + 3) * nCubes + 1 );
+    pSop = Vec_StrArray( vSop );
+    pSop[(nFanins + 3) * nCubes] = 0;
+    // create the SOP
+    Vec_StrFill( vCube, nFanins, '-' );
+    Vec_StrPush( vCube, '\0' );
+    Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
+    Cudd_RecursiveDerefZdd( dd, zCover );
+
+    // perform factoring
+//    return Abc_NtkDeriveFlatGiaSop( pNew, Vec_IntArray(vFanins), pSop );
+    return Gia_ManFactorNode( pNew, pSop, vFanins );
+}
+int Gia_ManRebuildNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Gia_Man_t * pNew, DdManager * ddNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
+{
+    DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
+    DdNode * bLocal, * bTemp;
+    Dsd_Node_t * pFaninDsd;
+    Dsd_Type_t Type;
+    int i, iLit, nDecs;
+
+    // add the fanins
+    Type  = Dsd_NodeReadType( pNodeDsd );
+    nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
+    assert( nDecs > 1 );
+    Vec_IntClear( vFanins );
+    for ( i = 0; i < nDecs; i++ )
+    {
+        pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
+        iLit      = Dsd_NodeReadMark( Dsd_Regular(pFaninDsd) );
+        iLit      = Abc_LitNotCond( iLit, Dsd_IsComplement(pFaninDsd) );
+        assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
+        Vec_IntPush( vFanins, iLit );
+    }
+
+    // create the local function depending on the type of the node
+    switch ( Type )
+    {
+        case DSD_NODE_CONST1:
+        {
+            iLit = 1;
+            break;
+        }
+        case DSD_NODE_OR:
+        {
+            iLit = 0;
+            for ( i = 0; i < nDecs; i++ )
+                iLit = Gia_ManHashOr( pNew, iLit, Vec_IntEntry(vFanins, i) );
+            break;
+        }
+        case DSD_NODE_EXOR:
+        {
+            iLit = 0;
+            for ( i = 0; i < nDecs; i++ )
+                iLit = Gia_ManHashXor( pNew, iLit, Vec_IntEntry(vFanins, i) );
+            break;
+        }
+        case DSD_NODE_PRIME:
+        {
+            bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
+            bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
+            Cudd_RecursiveDeref( ddDsd, bTemp );
+            // bLocal is now in the new BDD manager
+            iLit = Gia_ManRebuildIsop( ddNew, bLocal, pNew, vFanins, vSop, vCube );
+            Cudd_RecursiveDeref( ddNew, bLocal );
+            break;
+        }
+        default:
+        {
+            assert( 0 );
+            break;
+        }
+    }
+    Dsd_NodeSetMark( pNodeDsd, iLit );
+    return iLit;
+}
+Gia_Man_t * Gia_ManRebuild( Gia_Man_t * p, Dsd_Manager_t * pManDsd, DdManager * ddNew )
+{
+    Gia_Man_t * pNew;
+    Dsd_Node_t ** ppNodesDsd;
+    Dsd_Node_t * pNodeDsd;
+    int i, iLit, nNodesDsd;
+    Vec_Str_t * vSop, * vCube;
+    Vec_Int_t * vFanins;
+
+    vFanins = Vec_IntAlloc( 1000 );
+    vSop    = Vec_StrAlloc( 10000 );
+    vCube   = Vec_StrAlloc( 1000 );
+
+    pNew = Gia_ManStart( 2*Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+
+    // save the CI nodes in the DSD nodes
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), 1 );
+    for ( i = 0; i < Gia_ManCiNum(p); i++ )
+    {
+        pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
+        Dsd_NodeSetMark( pNodeDsd, Gia_ManAppendCi( pNew ) );
+    }
+
+    // collect DSD nodes in DFS order (leaves and const1 are not collected)
+    ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
+    for ( i = 0; i < nNodesDsd; i++ )
+    {
+        iLit = Gia_ManRebuildNode( pManDsd, ppNodesDsd[i], pNew, ddNew, vFanins, vSop, vCube );
+        if ( iLit == -1 )
+            break;
+    }
+    ABC_FREE( ppNodesDsd );
+    Vec_IntFree( vFanins );
+    Vec_StrFree( vSop );
+    Vec_StrFree( vCube );
+    if ( iLit == -1 )
+    {
+        Gia_ManStop( pNew );
+        return Gia_ManDup(p);
+    }
+
+    // set the pointers to the CO drivers
+    for ( i = 0; i < Gia_ManCoNum(p); i++ )
+    {
+        pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
+        iLit = Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pNodeDsd) );
+        Gia_ManAppendCo( pNew, iLit );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
+{
+    DdNode * bFunc; int i;
+    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
+        if ( bFunc )
+            Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vFuncs );
+}
+void Gia_ObjCollapseDeref( Gia_Man_t * p, DdManager * dd, Vec_Ptr_t * vFuncs, int Id )
+{
+    if ( Gia_ObjRefDecId(p, Id) )
+        return;
+    Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vFuncs, Id) );
+    Vec_PtrWriteEntry( vFuncs, Id, NULL );
+}
+Vec_Ptr_t * Gia_ManCollapse( Gia_Man_t * p, DdManager * dd, int nBddLimit, int fVerbose )
+{
+    Vec_Ptr_t * vFuncs;
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    Gia_Obj_t * pObj;
+    int i, Id;
+    Gia_ManCreateRefs( p );
+    // assign constant node
+    vFuncs = Vec_PtrStart( Gia_ManObjNum(p) );
+    if ( Gia_ObjRefNumId(p, 0) > 0 )
+        Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
+    // assign elementary variables
+    Gia_ManForEachCiId( p, Id, i )
+        if ( Gia_ObjRefNumId(p, Id) > 0 )
+            Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,i) ), Cudd_Ref(Cudd_bddIthVar(dd,i));
+    // create BDD for AND nodes
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
+        bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
+        bFunc  = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );  
+        if ( bFunc == NULL )
+        {
+            Gia_ManCollapseDeref( dd, vFuncs );
+            return NULL;
+        }        
+        Cudd_Ref( bFunc );
+        Vec_PtrWriteEntry( vFuncs, i, bFunc );
+        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, i) );
+        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId1(pObj, i) );
+    }
+    // create BDD for outputs
+    Gia_ManForEachCoId( p, Id, i )
+    {
+        pObj = Gia_ManCo( p, i );
+        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) );
+        Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
+        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, Id) );
+    }
+    assert( Vec_PtrSize(vFuncs) == Vec_PtrCountZero(vFuncs) + Gia_ManCoNum(p) );
+    // compact
+    Gia_ManForEachCoId( p, Id, i )
+        Vec_PtrWriteEntry( vFuncs, i, Vec_PtrEntry(vFuncs, Id) );
+    Vec_PtrShrink( vFuncs, Gia_ManCoNum(p) );
+    return vFuncs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    DdManager * dd, * ddNew;
+    Dsd_Manager_t * pManDsd;
+    Vec_Ptr_t * vFuncs;
+    // derive global BDDs
+    dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
+    Cudd_AutodynDisable( dd );
+    if ( vFuncs == NULL ) 
+    {
+        Extra_StopManager( dd );
+        return Gia_ManDup(p);
+    }
+    // start ISOP manager
+    ddNew = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_zddVarsFromBddVars( ddNew, 2 );
+//    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+    printf( "Ins = %d. Outs = %d.  Shared BDD nodes = %d.  Peak live nodes = %d. Peak nodes = %d.\n", 
+        Gia_ManCiNum(p), Gia_ManCoNum(p), 
+        Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ),
+        Cudd_ReadPeakLiveNodeCount(dd), Cudd_ReadNodeCount(dd) );
+    // perform decomposition
+    pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
+    Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
+    if ( fVerbose )
+    {
+        Vec_Ptr_t * vNamesCi = Abc_NodeGetFakeNames( Gia_ManCiNum(p) );
+        Vec_Ptr_t * vNamesCo = Abc_NodeGetFakeNames( Gia_ManCoNum(p) );
+        char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
+        char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
+        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
+        Vec_PtrFreeFree( vNamesCi );
+        Vec_PtrFreeFree( vNamesCo );
+    }
+
+    pNew = Gia_ManRebuild( p, pManDsd, ddNew );
+    Dsd_ManagerStop( pManDsd );
+    // return manager
+    Gia_ManCollapseDeref( dd, vFuncs );
+    Extra_StopManager( dd );
+    Extra_StopManager( ddNew );
+    return pNew;
+}
+void Gia_ManCollapseTestTest( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    pNew = Gia_ManCollapseTest( p, 0 );
+    Gia_ManPrintStats( p, NULL );
+    Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaMffc.c b/src/aig/gia/giaMffc.c
index 3d3cc271..de44ae1d 100644
--- a/src/aig/gia/giaMffc.c
+++ b/src/aig/gia/giaMffc.c
@@ -207,7 +207,7 @@ Gia_Man_t * Gia_ManDomDerive( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vSup
     Gia_Man_t * pNew, * pTemp;
     int nMints = 1 << nVars;
     int i, m, iResLit;
-    assert( nVars > 0 && nVars <= 5 );
+    assert( nVars >= 0 && nVars <= 5 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
@@ -249,6 +249,8 @@ Gia_Man_t * Gia_ManDomDerive( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vSup
 ***********************************************************************/
 void Gia_ManComputeDomsTry( Gia_Man_t * p )
 {
+    extern void Gia_ManCollapseTestTest( Gia_Man_t * p );
+
     Vec_Int_t * vSupp, * vSuppRefs;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
@@ -272,7 +274,7 @@ void Gia_ManComputeDomsTry( Gia_Man_t * p )
         if ( !Gia_ObjIsAnd(pObj) )
             continue;
         nSize = Gia_NodeMffcSizeSupp( p, pObj, vSupp, vSuppRefs );
-        if ( nSize < 30 || nSize > 100 )
+        if ( nSize < 10 )//|| nSize > 100 )
             continue;
         // sort by cost
         Vec_IntSelectSortCost2( Vec_IntArray(vSupp), Vec_IntSize(vSupp), Vec_IntArray(vSuppRefs) );
@@ -280,8 +282,8 @@ void Gia_ManComputeDomsTry( Gia_Man_t * p )
         printf( "Obj %6d : ", i );
         printf( "Cone = %4d  ", nSize );
         printf( "Supp = %4d  ", Vec_IntSize(vSupp) );
-        Vec_IntForEachEntry( vSuppRefs, Entry, k )
-            printf( "%d(%d) ", -Entry, Gia_ObjLevelId(p, Vec_IntEntry(vSupp, k)) );
+//        Vec_IntForEachEntry( vSuppRefs, Entry, k )
+//            printf( "%d(%d) ", -Entry, Gia_ObjLevelId(p, Vec_IntEntry(vSupp, k)) );
         printf( "\n" );
 
         // selected k
@@ -289,10 +291,13 @@ void Gia_ManComputeDomsTry( Gia_Man_t * p )
             if ( Vec_IntEntry(vSuppRefs, k) == 1 )
                 break;
         k = Abc_MinInt( k, 3 );
+        k = 0;
 
         // dump
         pNew = Gia_ManDomDerive( p, pObj, vSupp, k );
         Gia_DumpAiger( pNew, "mffc", i, 6 );
+        Gia_ManCollapseTestTest( pNew );
+
         Gia_ManStop( pNew );
     }
     Vec_IntFree( vSuppRefs );