Version abc80130_2

6 files changed, 312 insertions, 49 deletions

diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 6ecc9678..d0d9981d 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -21,6 +21,10 @@
 #ifndef __DEC_H__
 #define __DEC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -47,11 +51,15 @@ 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    : 16;   // the level of this node in the global AIG
+    unsigned          Level    : 14;   // 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;
@@ -95,9 +103,6 @@ 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 ========================================================*/
@@ -106,11 +111,10 @@ 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -308,7 +312,7 @@ static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst;
 }
@@ -324,7 +328,7 @@ static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst && pGraph->eRoot.fCompl;
 }
@@ -340,7 +344,7 @@ static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst && !pGraph->eRoot.fCompl;
 }
@@ -356,7 +360,7 @@ static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
 {
     return pGraph->eRoot.fCompl;
 }
@@ -469,7 +473,7 @@ static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )   
 {
     return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
 }
@@ -485,7 +489,7 @@ static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
+static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
 {
     return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
 }
@@ -627,24 +631,84 @@ 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 )
-{
-    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 );
+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
 }
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 9931b136..6adb0f98 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,13 +18,14 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "ivy.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -39,14 +40,14 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph )
+Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, 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(pMan), Dec_GraphIsComplement(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) );
@@ -55,7 +56,45 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, 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( pMan, pAnd0, pAnd1 );
+        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;
     }
     // complement the result if necessary
     return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
@@ -119,14 +158,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(pMan) )
+            if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pRoot->pNtk) )
                 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;
@@ -148,21 +187,118 @@ 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, int nGain )
+void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, 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->pManFunc, pGraph );
+    pRootNew = Dec_GraphToNetwork( pNtk, pGraph );
     // remove the old nodes
-    Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
+    Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
     // 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 f6654476..768dcd9b 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     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(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeCubes = pManDec->vCubes;
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
@@ -258,16 +258,15 @@ 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) );
-            Vec_IntPush( vEdgeLits, iBit );
+            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
         }
     // balance the factored forms
     return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
@@ -323,7 +322,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(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
     Mvc_Cover_t * pMvc;
     Mvc_Cube_t * pMvcCube;
@@ -365,7 +364,8 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() );
+    extern DdNode *       Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
+    DdManager * dd = Abc_FrameReadManDd();
     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 1d44d5cb..65857461 100644
--- a/src/opt/dec/decMan.c
+++ b/src/opt/dec/decMan.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c
index 6fb20327..2d8f09b3 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -101,7 +101,7 @@ void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char
   SeeAlso     []
 
 ***********************************************************************/
-void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+void Dec_GraphPrint2_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,6 +165,69 @@ void Dec_GraphPrint_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 02c3346e..463bc7e2 100644
--- a/src/opt/dec/decUtil.c
+++ b/src/opt/dec/decUtil.c
@@ -24,7 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************