summaryrefslogtreecommitdiffstats
path: root/src/opt/dec
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/dec')
-rw-r--r--src/opt/dec/dec.h118
-rw-r--r--src/opt/dec/decAbc.c154
-rw-r--r--src/opt/dec/decFactor.c18
-rw-r--r--src/opt/dec/decMan.c2
-rw-r--r--src/opt/dec/decPrint.c67
-rw-r--r--src/opt/dec/decUtil.c2
6 files changed, 49 insertions, 312 deletions
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index d0d9981d..6ecc9678 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -21,10 +21,6 @@
#ifndef __DEC_H__
#define __DEC_H__
-#ifdef __cplusplus
-extern "C" {
-#endif
-
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -51,15 +47,11 @@ struct Dec_Node_t_
Dec_Edge_t eEdge1; // the right child of the node
// other info
void * pFunc; // the function of the node (BDD or AIG)
- unsigned Level : 14; // the level of this node in the global AIG
+ unsigned Level : 16; // the level of this node in the global AIG
// printing info
unsigned fNodeOr : 1; // marks the original OR node
unsigned fCompl0 : 1; // marks the original complemented edge
unsigned fCompl1 : 1; // marks the original complemented edge
- // latch info
- unsigned nLat0 : 5; // the number of latches on the first edge
- unsigned nLat1 : 5; // the number of latches on the second edge
- unsigned nLat2 : 5; // the number of latches on the output edge
};
typedef struct Dec_Graph_t_ Dec_Graph_t;
@@ -103,6 +95,9 @@ struct Dec_Man_t_
////////////////////////////////////////////////////////////////////////
/*=== decAbc.c ========================================================*/
+extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph );
+extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
/*=== decFactor.c ========================================================*/
extern Dec_Graph_t * Dec_Factor( char * pSop );
/*=== decMan.c ========================================================*/
@@ -111,10 +106,11 @@ extern void Dec_ManStop( Dec_Man_t * p );
/*=== decPrint.c ========================================================*/
extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut );
/*=== decUtil.c ========================================================*/
+extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -312,7 +308,7 @@ static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
+static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
{
return pGraph->fConst;
}
@@ -328,7 +324,7 @@ static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
+static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )
{
return pGraph->fConst && pGraph->eRoot.fCompl;
}
@@ -344,7 +340,7 @@ static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
+static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )
{
return pGraph->fConst && !pGraph->eRoot.fCompl;
}
@@ -360,7 +356,7 @@ static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )
+static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.fCompl;
}
@@ -473,7 +469,7 @@ static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
+static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
}
@@ -489,7 +485,7 @@ static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
SeeAlso []
***********************************************************************/
-static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
+static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
}
@@ -631,84 +627,24 @@ static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eE
SeeAlso []
***********************************************************************/
-static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
-{
- Dec_Edge_t eNode0, eNode1, eNode;
- if ( Type == 0 )
- {
- // derive the first AND
- eEdge0.fCompl ^= 1;
- eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
- eEdge0.fCompl ^= 1;
- // derive the second AND
- eEdge1.fCompl ^= 1;
- eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
- // derive the final OR
- eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
- }
- else
- {
- // derive the first AND
- eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
- // derive the second AND
- eEdge0.fCompl ^= 1;
- eEdge1.fCompl ^= 1;
- eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
- // derive the final OR
- eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
- eNode.fCompl ^= 1;
- }
- return eNode;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates an XOR node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
-{
- Dec_Edge_t eNode0, eNode1, eNode;
- if ( Type == 0 )
- {
- // derive the first AND
- eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
- // derive the second AND
- eEdgeC.fCompl ^= 1;
- eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
- // derive the final OR
- eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
- }
- else
- {
- // complement the arguments
- eEdgeT.fCompl ^= 1;
- eEdgeE.fCompl ^= 1;
- // derive the first AND
- eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
- // derive the second AND
- eEdgeC.fCompl ^= 1;
- eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
- // derive the final OR
- eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
- eNode.fCompl ^= 1;
- }
- return eNode;
-}
-
-#ifdef __cplusplus
+static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
+{
+ Dec_Edge_t eNode0, eNode1;
+ // derive the first AND
+ eEdge0.fCompl = !eEdge0.fCompl;
+ eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+ eEdge0.fCompl = !eEdge0.fCompl;
+ // derive the second AND
+ eEdge1.fCompl = !eEdge1.fCompl;
+ eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+ eEdge1.fCompl = !eEdge1.fCompl;
+ // derive the final OR
+ return Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
-#endif
-
-#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+#endif
+
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 6adb0f98..9931b136 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,14 +18,13 @@
#include "abc.h"
#include "dec.h"
-#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -40,14 +39,14 @@
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
+Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph )
{
Abc_Obj_t * pAnd0, * pAnd1;
Dec_Node_t * pNode;
int i;
// check for constant function
if ( Dec_GraphIsConst(pGraph) )
- return Abc_ObjNotCond( Abc_AigConst1(pNtk), Dec_GraphIsComplement(pGraph) );
+ return Abc_ObjNotCond( Abc_AigConst1(pMan), Dec_GraphIsComplement(pGraph) );
// check for a literal
if ( Dec_GraphIsVar(pGraph) )
return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
@@ -56,45 +55,7 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
{
pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
- pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
- }
- // complement the result if necessary
- return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Transforms the decomposition graph into the AIG.]
-
- Description [AIG nodes for the fanins should be assigned to pNode->pFunc
- of the leaves of the graph before calling this procedure.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
-{
- Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
- Dec_Node_t * pNode;
- int i;
- // check for constant function
- if ( Dec_GraphIsConst(pGraph) )
- return Abc_ObjNotCond( Abc_AigConst1(pNtk), Dec_GraphIsComplement(pGraph) );
- // check for a literal
- if ( Dec_GraphIsVar(pGraph) )
- return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
- // build the AIG nodes corresponding to the AND gates of the graph
- Dec_GraphForEachNode( pGraph, pNode, i )
- {
- pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
- pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
-// pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
- pAnd = Abc_NtkCreateNode( pNtk );
- Abc_ObjAddFanin( pAnd, pAnd0 );
- Abc_ObjAddFanin( pAnd, pAnd1 );
- pNode->pFunc = pAnd;
+ pNode->pFunc = Abc_AigAnd( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
@@ -158,14 +119,14 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level );
if ( pAnd )
{
- if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pRoot->pNtk) )
+ if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) )
LevelNew = 0;
else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) )
LevelNew = (int)Abc_ObjRegular(pAnd0)->Level;
else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
-// assert( LevelNew == LevelOld );
+ assert( LevelNew == LevelOld );
}
if ( LevelNew > LevelMax )
return -1;
@@ -187,118 +148,21 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
SeeAlso []
***********************************************************************/
-void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
+void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
{
- extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
Abc_Obj_t * pRootNew;
Abc_Ntk_t * pNtk = pRoot->pNtk;
int nNodesNew, nNodesOld;
nNodesOld = Abc_NtkNodeNum(pNtk);
// create the new structure of nodes
- pRootNew = Dec_GraphToNetwork( pNtk, pGraph );
+ pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph );
// remove the old nodes
- Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
+ Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
// compare the gains
nNodesNew = Abc_NtkNodeNum(pNtk);
assert( nGain <= nNodesOld - nNodesNew );
}
-
-/**Function*************************************************************
-
- Synopsis [Transforms the decomposition graph into the AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Dec_Graph_t * pGraph )
-{
- Dec_Node_t * pNode;
- Hop_Obj_t * pAnd0, * pAnd1;
- int i;
- // check for constant function
- if ( Dec_GraphIsConst(pGraph) )
- return Hop_NotCond( Hop_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
- // check for a literal
- if ( Dec_GraphIsVar(pGraph) )
- return Hop_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
- // build the AIG nodes corresponding to the AND gates of the graph
- Dec_GraphForEachNode( pGraph, pNode, i )
- {
- pAnd0 = Hop_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
- pAnd1 = Hop_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
- pNode->pFunc = Hop_And( pMan, pAnd0, pAnd1 );
- }
- // complement the result if necessary
- return Hop_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Strashes one logic node using its SOP.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop )
-{
- Hop_Obj_t * pFunc;
- Dec_Graph_t * pFForm;
- Dec_Node_t * pNode;
- int i;
- // perform factoring
- pFForm = Dec_Factor( pSop );
- // collect the fanins
- Dec_GraphForEachLeaf( pFForm, pNode, i )
- pNode->pFunc = Hop_IthVar( pMan, i );
- // perform strashing
- pFunc = Dec_GraphToNetworkAig( pMan, pFForm );
- Dec_GraphFree( pFForm );
- return pFunc;
-}
-
-/**Function*************************************************************
-
- Synopsis [Transforms the decomposition graph into the AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
-{
- Dec_Node_t * pNode;
- Ivy_Obj_t * pAnd0, * pAnd1;
- int i;
- // check for constant function
- if ( Dec_GraphIsConst(pGraph) )
- return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
- // check for a literal
- if ( Dec_GraphIsVar(pGraph) )
- return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
- // build the AIG nodes corresponding to the AND gates of the graph
- Dec_GraphForEachNode( pGraph, pNode, i )
- {
- pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
- pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
- pNode->pFunc = Ivy_And( pMan, pAnd0, pAnd1 );
- }
- // complement the result if necessary
- return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index 768dcd9b..f6654476 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -34,7 +34,7 @@ static int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm );
static Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -183,7 +183,7 @@ Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
***********************************************************************/
Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
{
- Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
Vec_Int_t * vEdgeLits = pManDec->vLits;
Mvc_Cover_t * pDiv, * pQuo, * pRem;
Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
@@ -228,7 +228,7 @@ Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cov
***********************************************************************/
Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
{
- Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
Vec_Int_t * vEdgeCubes = pManDec->vCubes;
Vec_Int_t * vEdgeLits = pManDec->vLits;
Mvc_Manager_t * pMem = pManDec->pMvcMem;
@@ -258,15 +258,16 @@ Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
***********************************************************************/
Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits )
{
- Dec_Edge_t eNode;
+// Dec_Edge_t eNode;
int iBit, Value;
// create the factored form for each literal
Vec_IntClear( vEdgeLits );
Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
if ( Value )
{
- eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
- Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
+// eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+// Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
+ Vec_IntPush( vEdgeLits, iBit );
}
// balance the factored forms
return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
@@ -322,7 +323,7 @@ Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes
***********************************************************************/
Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
{
- Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
Mvc_Manager_t * pMem = pManDec->pMvcMem;
Mvc_Cover_t * pMvc;
Mvc_Cube_t * pMvcCube;
@@ -364,8 +365,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
***********************************************************************/
int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
{
- extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
- DdManager * dd = Abc_FrameReadManDd();
+ DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() );
DdNode * bFunc1, * bFunc2;
int RetValue;
bFunc1 = Abc_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 );
diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c
index 65857461..1d44d5cb 100644
--- a/src/opt/dec/decMan.c
+++ b/src/opt/dec/decMan.c
@@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c
index 2d8f09b3..6fb20327 100644
--- a/src/opt/dec/decPrint.c
+++ b/src/opt/dec/decPrint.c
@@ -29,7 +29,7 @@ static void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax
static int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -101,7 +101,7 @@ void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char
SeeAlso []
***********************************************************************/
-void Dec_GraphPrint2_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
{
Dec_Node_t * pNode0, * pNode1;
pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
@@ -165,69 +165,6 @@ void Dec_GraphPrint2_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode
SeeAlso []
***********************************************************************/
-void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
-{
- Dec_Node_t * pNode0, * pNode1;
- Dec_Node_t * pNode00, * pNode01, * pNode10, * pNode11;
- pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
- pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node);
- if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF )
- {
- (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn );
- return;
- }
- if ( !Dec_GraphNodeIsVar(pGraph, pNode0) && !Dec_GraphNodeIsVar(pGraph, pNode1) )
- {
- pNode00 = Dec_GraphNode(pGraph, pNode0->eEdge0.Node);
- pNode01 = Dec_GraphNode(pGraph, pNode0->eEdge1.Node);
- pNode10 = Dec_GraphNode(pGraph, pNode1->eEdge0.Node);
- pNode11 = Dec_GraphNode(pGraph, pNode1->eEdge1.Node);
- if ( (pNode00 == pNode10 || pNode00 == pNode11) && (pNode01 == pNode10 || pNode01 == pNode11) )
- {
- fprintf( pFile, "(" );
- (*pPos)++;
- Dec_GraphPrint_rec( pFile, pGraph, pNode00, pNode00->fCompl0, pNamesIn, pPos, LitSizeMax );
- fprintf( pFile, " # " );
- (*pPos) += 3;
- Dec_GraphPrint_rec( pFile, pGraph, pNode01, pNode01->fCompl1, pNamesIn, pPos, LitSizeMax );
- fprintf( pFile, ")" );
- (*pPos)++;
- return;
- }
- }
- if ( fCompl )
- {
- fprintf( pFile, "(" );
- (*pPos)++;
- Dec_GraphPrint_rec( pFile, pGraph, pNode0, !pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
- fprintf( pFile, " + " );
- (*pPos) += 3;
- Dec_GraphPrint_rec( pFile, pGraph, pNode1, !pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
- fprintf( pFile, ")" );
- (*pPos)++;
- }
- else
- {
- fprintf( pFile, "(" );
- (*pPos)++;
- Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
- Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
- fprintf( pFile, ")" );
- (*pPos)++;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] )
{
static char Buffer[100];
diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c
index 463bc7e2..02c3346e 100644
--- a/src/opt/dec/decUtil.c
+++ b/src/opt/dec/decUtil.c
@@ -24,7 +24,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 17:45:28 +0000