Better logic cone proprocessor for 'satclp' to reduce runtime.

2 files changed, 483 insertions, 0 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index ff57fedb..ffb3e74d 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "misc/tim/tim.h"
+#include "misc/vec/vecWec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -3236,6 +3237,260 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes supports for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Obj_t * pObj; int i, Id;
+    Vec_Wec_t * vSuppsCo = Vec_WecStart( Gia_ManCoNum(p) );
+    Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
+    Gia_ManForEachCiId( p, Id, i )
+        Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
+    Gia_ManForEachAnd( p, pObj, Id )
+        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Id) ); 
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_IntAppend( Vec_WecEntry(vSuppsCo, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
+    Vec_WecFree( vSupps );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
+    return vSuppsCo;
+}
+int Gia_ManCoSuppSizeMax( Gia_Man_t * p, Vec_Wec_t * vSupps )
+{
+    Gia_Obj_t * pObj; 
+    Vec_Int_t * vSuppOne;
+    int i, nSuppMax = 1;
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        vSuppOne = Vec_WecEntry( vSupps, i );
+        nSuppMax = Abc_MaxInt( nSuppMax, Vec_IntSize(vSuppOne) );
+    }
+    return nSuppMax;
+}
+int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps )
+{
+    Gia_Obj_t * pObj; 
+    Vec_Int_t * vSuppOne;
+    int i, iCoMax = -1, nSuppMax = -1;
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        vSuppOne = Vec_WecEntry( vSupps, i );
+        if ( nSuppMax < Vec_IntSize(vSuppOne) )
+        {
+            nSuppMax = Vec_IntSize(vSuppOne);
+            iCoMax = i;
+        }
+    }
+    return iCoMax;
+}
+Vec_Int_t * Gia_ManSortCoBySuppSize( Gia_Man_t * p, Vec_Wec_t * vSupps )
+{
+    Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManCoNum(p) );
+    Vec_Wrd_t * vSortData = Vec_WrdAlloc( Gia_ManCoNum(p) );
+    Vec_Int_t * vSuppOne; word Entry; int i;
+    Vec_WecForEachLevel( vSupps, vSuppOne, i )
+        Vec_WrdPush( vSortData, ((word)i << 32) | Vec_IntSize(vSuppOne) );
+    Abc_QuickSort3( Vec_WrdArray(vSortData), Vec_WrdSize(vSortData), 1 );
+    Vec_WrdForEachEntry( vSortData, Entry, i )
+        Vec_IntPush( vOrder, (int)(Entry >> 32) );
+    Vec_WrdFree( vSortData );
+    return vOrder;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps each CO cone to depend on the first CI variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManDupHashDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+void Gia_ManDupCleanDfs_rec( Gia_Obj_t * pObj )
+{
+    if ( !~pObj->Value )
+        return;
+    pObj->Value = ~0;
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
+    Gia_ManDupCleanDfs_rec( Gia_ObjFanin1(pObj) );
+} 
+Gia_Man_t * Gia_ManDupStrashReduce( Gia_Man_t * p, Vec_Wec_t * vSupps, Vec_Int_t ** pvCoMap )
+{
+    Gia_Obj_t * pObj;
+    Gia_Man_t * pNew, * pTemp;
+    Vec_Int_t * vSuppOne, * vCoMapLit;
+    int i, k, iCi, iLit, nSuppMax;
+    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManFillValue( p );
+    vCoMapLit = Vec_IntAlloc( Gia_ManCoNum(p) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
+    for ( i = 0; i < nSuppMax; i++ )
+        Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        vSuppOne = Vec_WecEntry( vSupps, i );
+        if ( Vec_IntSize(vSuppOne) == 0 )
+            Vec_IntPush( vCoMapLit, Abc_Var2Lit(0, Gia_ObjFaninC0(pObj)) );
+        else if ( Vec_IntSize(vSuppOne) == 1 )
+            Vec_IntPush( vCoMapLit, Abc_Var2Lit(1, Gia_ObjFaninC0(pObj)) );
+        else
+        {
+            Vec_IntForEachEntry( vSuppOne, iCi, k )
+                Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
+            Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+            assert( Gia_ObjFanin0Copy(pObj) < 2 * Gia_ManObjNum(pNew) );
+            Vec_IntPush( vCoMapLit, Gia_ObjFanin0Copy(pObj) );
+            Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
+        }
+    }
+    Gia_ManHashStop( pNew );
+    assert( Vec_IntSize(vCoMapLit) == Gia_ManCoNum(p) );
+    if ( pvCoMap == NULL ) // do not remap
+    {
+        Vec_IntForEachEntry( vCoMapLit, iLit, i )
+            Gia_ManAppendCo( pNew, iLit );
+    }
+    else // remap
+    {
+        Vec_Int_t * vCoMapRes = Vec_IntAlloc( Gia_ManCoNum(p) );      // map old CO into new CO 
+        Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(pNew) ); // map new lit into new CO
+        Vec_IntForEachEntry( vCoMapLit, iLit, i )
+        {
+            if ( Vec_IntEntry(vMap, iLit) == -1 )
+            {
+                Vec_IntWriteEntry( vMap, iLit, Gia_ManCoNum(pNew) );
+                Gia_ManAppendCo( pNew, iLit );
+            }
+            Vec_IntPush( vCoMapRes, Vec_IntEntry(vMap, iLit) );
+        }
+        Vec_IntFree( vMap );
+        *pvCoMap = vCoMapRes;
+    }
+    Vec_IntFree( vCoMapLit );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Gia_ManIsoStrashReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+{
+    Vec_Int_t * vCoMap;
+    Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
+    Gia_Man_t * pNew = Gia_ManDupStrashReduce( p, vSupps, &vCoMap );
+    Vec_IntFree( vCoMap );
+    Vec_WecFree( vSupps );
+    *pvPosEquivs = NULL;
+    return pNew;
+}
+
+int Gia_ManIsoStrashReduceOne( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+    int k, iCi, iLit;
+    assert( Gia_ObjIsCo(pObj) );
+    if ( Vec_IntSize(vSupp) == 0 )
+        return Abc_Var2Lit(0, Gia_ObjFaninC0(pObj));
+    if ( Vec_IntSize(vSupp) == 1 )
+        return Abc_Var2Lit(1, Gia_ObjFaninC0(pObj));
+    Vec_IntForEachEntry( vSupp, iCi, k )
+        Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
+    Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    iLit = Gia_ObjFanin0Copy(pObj);
+    Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
+    return iLit;
+}
+Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 );
+    Vec_Int_t * vSuppOne, * vMap = Vec_IntAlloc( 10000 );
+    int i, iLit, nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
+    // count how many times each support size appears
+    Vec_Int_t * vSizeCount = Vec_IntStart( nSuppMax + 1 );
+    Vec_WecForEachLevel( vSupps, vSuppOne, i )
+        Vec_IntAddToEntry( vSizeCount, Vec_IntSize(vSuppOne), 1 );
+    // create array of unique outputs
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nSuppMax; i++ )
+        Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        vSuppOne = Vec_WecEntry( vSupps, i );
+        if ( Vec_IntEntry(vSizeCount, Vec_IntSize(vSuppOne)) == 1 )
+        {
+            Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
+            continue;
+        }
+        iLit = Gia_ManIsoStrashReduceOne( pNew, p, pObj, vSuppOne );
+        Vec_IntFillExtra( vMap, iLit + 1, -1 );
+        if ( Vec_IntEntry(vMap, iLit) == -1 )
+        {
+            Vec_IntWriteEntry( vMap, iLit, Vec_WecSize(vPosEquivs) );
+            Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
+            continue;
+        }
+        Vec_IntPush( Vec_WecEntry(vPosEquivs, Vec_IntEntry(vMap, iLit)), i );
+    }
+    Gia_ManHashStop( pNew );
+    Gia_ManStop( pNew );
+    Vec_IntFree( vSizeCount );
+    Vec_IntFree( vMap );
+    return vPosEquivs;
+}
+Gia_Man_t * Gia_ManIsoStrashReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+{
+    Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
+    Vec_Wec_t * vPosEquivs = Gia_ManIsoStrashReduceInt( p, vSupps, fVerbose );
+    // find the first outputs and derive GIA
+    Vec_Int_t * vFirsts = Vec_WecCollectFirsts( vPosEquivs );
+    Gia_Man_t * pNew = Gia_ManDupCones( p, Vec_IntArray(vFirsts), Vec_IntSize(vFirsts), 0 );
+    Vec_IntFree( vFirsts );
+    Vec_WecFree( vSupps );
+    // report and return    
+    if ( fVerbose )
+    { 
+        printf( "Nontrivial classes:\n" );
+        Vec_WecPrint( vPosEquivs, 1 );
+    }
+    if ( pvPosEquivs )
+        *pvPosEquivs = Vec_WecConvertToVecPtr( vPosEquivs );
+    Vec_WecFree( vPosEquivs );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 804b0bd3..d1e6be2f 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -242,6 +242,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
 #endif
 
 
+#if 0
 
 /**Function*************************************************************
 
@@ -526,6 +527,233 @@ Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
     return pNtkNew;
 }
 
+#endif
+
+
+
+extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose );
+extern int         Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps );
+extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose );
+
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClpGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
+{
+    int iLit0, iLit1;
+    if ( pNode->iTemp >= 0 )
+        return pNode->iTemp;
+    assert( Abc_ObjIsNode( pNode ) );
+    iLit0 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
+    iLit1 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin1(pNode) );
+    iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) );
+    iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) );
+    return (pNode->iTemp = Gia_ManAppendAnd(pNew, iLit0, iLit1));
+}
+Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
+{
+    int i, iLit;
+    Gia_Man_t * pNew;
+    Abc_Obj_t * pNode;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( pNtk->pName );
+    pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        pNode->iTemp = -1;
+    Abc_AigConst1(pNtk)->iTemp = 1;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->iTemp = Gia_ManAppendCi(pNew);
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        iLit = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
+        iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) );
+        Gia_ManAppendCo( pNew, iLit );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes SOPs for each output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
+{
+    Vec_Str_t * vSop;
+    abctime clk = Abc_Clock();
+    extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+    Gia_Man_t * pGia  = Gia_ManDupCones( p, &iCo, 1, 1 );
+    if ( fVerbose )
+        printf( "Output %4d:  Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
+    vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+    Gia_ManStop( pGia );
+    if ( vSop == NULL )
+        return NULL;
+    if ( Vec_StrSize(vSop) == 4 ) // constant
+        Vec_IntClear(vSupp);
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return vSop; 
+}
+Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vSops = NULL, * vSopsRepr;
+    Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
+    int i, k, Entry, iCo, * pOrder;
+    Vec_Wec_t * vClasses;
+    // check the largest output
+    if ( nCubeLim > 0 && nCostMax > 0 )
+    {
+        int iCoMax   = Gia_ManCoLargestSupp( p, vSupps );
+        int iObjMax  = Gia_ObjId( p, Gia_ManCo(p, iCoMax) );
+        int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
+        int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 );
+        word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
+        if ( Cost > (word)nCostMax )
+        {
+            printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d  >  %d).\n", 
+                nNodeMax, nSuppMax, nCubeLim, nCostMax );
+            return NULL;
+        }
+    }
+    // derive classes of outputs
+    vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
+    // derive representatives
+    vReprs = Vec_WecCollectFirsts( vClasses );
+    vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) );
+    Vec_IntForEachEntry( vReprs, Entry, i )
+        Vec_IntPush( vReprSuppSizes, Vec_IntSize(Vec_WecEntry(vSupps, Entry)) );
+    pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
+    Vec_IntFree( vReprSuppSizes );
+    // consider SOPs for representatives
+    vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
+    Extra_ProgressBarUpdate( pProgress, 0, NULL );
+    for ( i = 0; i < Vec_IntSize(vReprs); i++ )
+    {
+        int iEntry        = pOrder[Vec_IntSize(vReprs) - 1 - i];
+        int iCoThis       = Vec_IntEntry( vReprs, iEntry );
+        Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis );
+        Vec_Str_t * vSop  = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
+        if ( vSop == NULL )
+            goto finish;
+        assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Vec_PtrWriteEntry( vSopsRepr, iEntry, Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ) );
+        Vec_StrFree( vSop );
+    }
+    Extra_ProgressBarStop( pProgress );
+    // derive SOPs for each output
+    vSops = Vec_PtrStart( Gia_ManCoNum(p) );
+    Vec_WecForEachLevel ( vClasses, vClass, i )
+        Vec_IntForEachEntry( vClass, iCo, k )
+            Vec_PtrWriteEntry( vSops, iCo, Vec_PtrEntry(vSopsRepr, i) );
+    assert( Vec_PtrCountZero(vSops) == 0 );
+/*
+    // verify
+    for ( i = 0; i < Gia_ManCoNum(p); i++ )
+    {
+        Vec_Int_t * vSupp = Vec_WecEntry( vSupps, i );
+        char * pSop = (char *)Vec_PtrEntry( vSops, i );
+        assert( Vec_IntSize(vSupp) == Abc_SopGetVarNum(pSop) );
+    }
+*/
+    // cleanup
+finish:
+    ABC_FREE( pOrder );
+    Vec_IntFree( vReprs );
+    Vec_WecFree( vClasses );
+    Vec_PtrFree( vSopsRepr );
+    return vSops;
+}
+Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Gia_Man_t * pGia;
+    Vec_Wec_t * vSupps;
+    Vec_Int_t * vSupp;
+    Vec_Ptr_t * vSops;
+    Abc_Obj_t * pNode, * pNodeNew, * pDriver;
+    int i, k, iCi; 
+    pGia    = Abc_NtkClpGia( pNtk );
+    vSupps  = Gia_ManCreateCoSupps( pGia, fVerbose );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    vSops   = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+    Gia_ManStop( pGia );
+    if ( vSops == NULL )
+    {
+        Vec_WecFree( vSupps );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pDriver = Abc_ObjFanin0(pNode);
+        if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) )
+        {
+            Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
+            continue;
+        }
+        if ( Abc_ObjIsCi(pDriver) )
+        {
+            pNodeNew = Abc_NtkCreateNode( pNtkNew );
+            Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); 
+            pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
+            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+            continue;
+        }
+        if ( pDriver == Abc_AigConst1(pNtk) )
+        {
+            pNodeNew = Abc_NtkCreateNode( pNtkNew );
+            pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" );
+            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+            continue;
+        }
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        vSupp = Vec_WecEntry( vSupps, i );
+        Vec_IntForEachEntry( vSupp, iCi, k )
+            Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
+        pNodeNew->pData = Vec_PtrEntry( vSops, i );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+    Vec_WecFree( vSupps );
+    Vec_PtrFree( vSops );
+    return pNtkNew;
+}
+Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+    if ( pNtkNew == NULL )
+        return NULL;
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkCollapseSat: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///