Various changes.

4 files changed, 184 insertions, 0 deletions

diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h
index bd0f7d7d..cc3cfeab 100644
--- a/src/bool/bdc/bdc.h
+++ b/src/bool/bdc/bdc.h
@@ -79,6 +79,8 @@ extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );
 extern int         Bdc_FuncCopyInt( Bdc_Fun_t * p );
 extern void        Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
 extern void        Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy );
+extern int         Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose );
+extern Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars );
 
 /*=== working with saved copies ==========================================*/
 static inline int  Bdc_FunObjCopy( Bdc_Fun_t * pObj )     { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c
index 5a7a0c3a..cc94244d 100644
--- a/src/bool/bdc/bdcCore.c
+++ b/src/bool/bdc/bdcCore.c
@@ -364,6 +364,85 @@ void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
     Bdc_ManFree( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose )
+{
+    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    Bdc_Man_t * pManDec;
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    pPars->nVarsMax = nVars;
+    pManDec = Bdc_ManAlloc( pPars );
+    Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
+    nNodes = Bdc_ManAndNum( pManDec );
+    if ( fVerbose )
+        Bdc_ManDecPrint( pManDec );
+    Bdc_ManFree( pManDec );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManBidecResubInt( Bdc_Man_t * p, Vec_Int_t * vRes )
+{
+    int i, iRoot = Bdc_FunId(p,Bdc_Regular(p->pRoot)) - 1;
+    if ( iRoot == -1 )
+        Vec_IntPush( vRes, !Bdc_IsComplement(p->pRoot) );
+    else if ( iRoot < p->nVars )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
+    else
+    {
+        for ( i = p->nVars+1; i < p->nNodes; i++ )
+        {
+            Bdc_Fun_t * pNode = p->pNodes + i;
+            int iLit0 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) - 1, Bdc_IsComplement(pNode->pFan0) );
+            int iLit1 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) - 1, Bdc_IsComplement(pNode->pFan1) );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+        }
+        assert( 2 + iRoot == p->nNodes );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
+    }
+}
+Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars )
+{
+    Vec_Int_t * vRes = NULL;
+    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    Bdc_Man_t * pManDec; 
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    pPars->nVarsMax = nVars;
+    pManDec = Bdc_ManAlloc( pPars );
+    Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
+    if ( pManDec->pRoot != NULL )
+    {
+        //Bdc_ManDecPrint( pManDec );
+        nNodes = Bdc_ManAndNum( pManDec );
+        vRes = Vec_IntAlloc( 2*nNodes + 1 );
+        Bdc_ManBidecResubInt( pManDec, vRes );
+        assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
+    }
+    Bdc_ManFree( pManDec );
+    return vRes;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index 5436956a..ee82b084 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -574,6 +574,8 @@ extern int             Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t
 //extern Hop_Obj_t *     Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
 //extern Hop_Obj_t *     Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
 //extern Hop_Obj_t *     Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
+extern int             Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
+extern Vec_Int_t *     Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
 /*=== kitIsop.c ==========================================================*/
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
 extern int             Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth, int fReturnTt );
diff --git a/src/bool/kit/kitHop.c b/src/bool/kit/kitHop.c
index 4ac82ac9..4509dadf 100644
--- a/src/bool/kit/kitHop.c
+++ b/src/bool/kit/kitHop.c
@@ -136,6 +136,107 @@ int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, i
   SeeAlso     []
 
 ***********************************************************************/
+int Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
+{
+    Kit_Graph_t * pGraph;
+    int nNodes;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+    if ( pGraph == NULL )
+    {
+        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
+        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
+        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
+    }
+    // derive the AIG for the decomposition tree
+    nNodes = Kit_GraphNodeNum( pGraph );
+    Kit_GraphFree( pGraph );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_IsopResubInt( Kit_Graph_t * pGraph, Vec_Int_t * vRes )
+{
+    int nVars = Kit_GraphLeaveNum(pGraph);
+    assert( nVars >= 0 && nVars <= pGraph->nSize );
+    if ( Kit_GraphIsConst(pGraph) )
+        Vec_IntPush( vRes, Kit_GraphIsConst1(pGraph) );
+    else if ( Kit_GraphIsVar(pGraph) )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphVarInt(pGraph), Kit_GraphIsComplement(pGraph)) );
+    else
+    {
+        Kit_Node_t * pNode; int i;
+        Kit_GraphForEachNode( pGraph, pNode, i )
+        {
+            Kit_Node_t * pFan0 = Kit_GraphNodeFanin0( pGraph, pNode );
+            Kit_Node_t * pFan1 = Kit_GraphNodeFanin1( pGraph, pNode );
+            int iLit0 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan0), pNode->eEdge0.fCompl );
+            int iLit1 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan1), pNode->eEdge1.fCompl );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+        }
+        assert( pNode == Kit_GraphNode(pGraph, pGraph->eRoot.Node) );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphNodeInt(pGraph, pNode), Kit_GraphIsComplement(pGraph)) );
+    }
+}
+Vec_Int_t * Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
+{
+    Vec_Int_t * vRes = NULL;
+    Kit_Graph_t * pGraph;
+    int nNodes;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+    if ( pGraph == NULL )
+    {
+        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
+        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
+        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
+    }
+    // derive the AIG for the decomposition tree
+    nNodes = Kit_GraphNodeNum( pGraph );
+    vRes = Vec_IntAlloc( 2*nNodes + 1 );
+    Kit_IsopResubInt( pGraph, vRes );
+    assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
+    Kit_GraphFree( pGraph );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Hop_Obj_t * Kit_GraphToHopInternal( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
 {
     Kit_Node_t * pNode = NULL;