summaryrefslogtreecommitdiffstats
path: root/src/bool
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool')
-rw-r--r--src/bool/bdc/bdc.h2
-rw-r--r--src/bool/bdc/bdcCore.c79
-rw-r--r--src/bool/kit/kit.h2
-rw-r--r--src/bool/kit/kitHop.c101
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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 06:22:08 +0000