From 674bcbee379b9dcef418ddb62655ee0d3d59f96c Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 30 Sep 2021 18:02:33 -0700
Subject: Various changes.

---
 src/bool/bdc/bdc.h     |  2 ++
 src/bool/bdc/bdcCore.c | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 81 insertions(+)

(limited to 'src/bool/bdc')

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                                ///
-- 
cgit v1.2.3


From eb44a80bf2eb8723231e72bb095c97d1e4834d56 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 30 Sep 2021 18:08:26 -0700
Subject: Compiler warnings.

---
 src/bool/bdc/bdcCore.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/bool/bdc')

diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c
index cc94244d..cce0e306 100644
--- a/src/bool/bdc/bdcCore.c
+++ b/src/bool/bdc/bdcCore.c
@@ -377,7 +377,7 @@ void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
 ***********************************************************************/
 int Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose )
 {
-    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    int nNodes;
     Bdc_Man_t * pManDec;
     Bdc_Par_t Pars = {0}, * pPars = &Pars;
     pPars->nVarsMax = nVars;
@@ -426,7 +426,7 @@ void Bdc_ManBidecResubInt( Bdc_Man_t * p, Vec_Int_t * vRes )
 Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars )
 {
     Vec_Int_t * vRes = NULL;
-    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    int nNodes;
     Bdc_Man_t * pManDec; 
     Bdc_Par_t Pars = {0}, * pPars = &Pars;
     pPars->nVarsMax = nVars;
-- 
cgit v1.2.3