Version abc50902

7 files changed, 1407 insertions, 143 deletions

diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 26af6b1c..6ecc9678 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -33,83 +33,89 @@
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Dec_Edge_t_ Dec_Edge_t;
+struct Dec_Edge_t_
+{
+    unsigned          fCompl   :  1;   // the complemented bit
+    unsigned          Node     : 30;   // the decomposition node pointed by the edge
+};
+
 typedef struct Dec_Node_t_ Dec_Node_t;
 struct Dec_Node_t_
 {
-    // the first child
-    unsigned   fCompl0  :  1;    // complemented attribute of the first fanin
-    unsigned   iFanin0  : 11;    // the number of the first fanin
-    // the second child
-    unsigned   fCompl1  :  1;    // complemented attribute of the second fanin
-    unsigned   iFanin1  : 11;    // the number of the second fanin
+    Dec_Edge_t        eEdge0;          // the left child of the node
+    Dec_Edge_t        eEdge1;          // the right child of the node
     // other info
-    unsigned   fIntern  :  1;    // marks all internal nodes (to distinquish them from elementary vars) 
-    unsigned   fConst   :  1;    // marks the constant 1 function (topmost node only)
-    unsigned   fCompl   :  1;    // marks the complement of topmost node (topmost node only)
-    // printing info (factored forms only)
-    unsigned   fNodeOr  :  1;    // marks the original OR node
-    unsigned   fEdge0   :  1;    // marks the original complemented edge
-    unsigned   fEdge1   :  1;    // marks the original complemented edge
-    // some bits are left unused
+    void *            pFunc;           // the function of the node (BDD or 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
+};
+
+typedef struct Dec_Graph_t_ Dec_Graph_t;
+struct Dec_Graph_t_
+{
+    int               fConst;          // marks the constant 1 graph
+    int               nLeaves;         // the number of leaves
+    int               nSize;           // the number of nodes (including the leaves) 
+    int               nCap;            // the number of allocated nodes
+    Dec_Node_t *      pNodes;          // the array of leaves and internal nodes
+    Dec_Edge_t        eRoot;           // the pointer to the topmost node
+};
+
+typedef struct Dec_Man_t_ Dec_Man_t;
+struct Dec_Man_t_
+{
+    void *            pMvcMem;         // memory manager for MVC cover (used for factoring)
+    Vec_Int_t *       vCubes;          // storage for cubes
+    Vec_Int_t *       vLits;           // storage for literals 
+    // precomputation information about 4-variable functions
+    unsigned short *  puCanons;        // canonical forms
+    char *            pPhases;         // canonical phases
+    char *            pPerms;          // canonical permutations
+    unsigned char *   pMap;            // mapping of functions into class numbers
 };
 
-/*
-    The decomposition tree data structure is designed to represent relatively small
-    (up to 100 nodes) AIGs used for factoring, rewriting, and decomposition.
-
-    For simplicity, the nodes of the decomposition tree are written in DFS order 
-    into an integer vector (Vec_Int_t). The decomposition node (Dec_Node_t)
-    is typecast into an integer when written into the array.
-    
-    This representation can be readily translated into the main AIG represented 
-    in the ABC network. Because of the linear order of the decomposition nodes 
-    in the array, it is easy to put the existing AIG nodes in correspondence with 
-    them. This process begins by first putting leaves of the decomposition tree 
-    in correpondence with the fanins of the cut used to derive the function, 
-    which was decomposed. Next for each internal node of the decomposition tree, 
-    we find or create a corresponding node in the AIG. Finally, the root node of 
-    the tree replaces the original root node of the cut, which was decomposed.
-
-    To achieve the above scenario, we reserve the first n entries for the array
-    to the fanins of the cut (the number of fanins is n). These entries are left
-    empty in the array (that is, they are represented by 0 integer). Each entry
-    after the fanins is an internal node (flag fIntern is set to 1). The internal
-    nodes can have complemented inputs (denoted by flags fComp0 and fCompl1).
-    The last node can be complemented (fCompl), which is true if the root node
-    of the decomposition tree is represented by a complemented AIG node.
-
-    Two cases have to be specially considered: a constant function and a function
-    equal to an elementary variables (possibly complemented). In these two cases,
-    the decomposition tree/array has exactly n+1 nodes, where n in the number of 
-    fanins. (A constant function may depend on n variable, in which case these
-    are redundant variables. Similarly, a function can be a function in n-D space
-    but in fact depend only on one variable in this space.)
-
-    When the function is a constant, the last node has a flag fConst set to 1.
-    In this case the complemented flag (fCompl) shows the value of the constant.
-    (fCompl = 0 means costant 1; fCompl = 1 means constant 0).
-    When the function if an elementary variable, the last node has both pointers
-    pointing to the same elementary node, while the complemented flag (fCompl)
-    shows whether the variable is complemented. For example: x' = Not( AND(x, x) ).
-
-    When manipulating the decomposition tree, it is convenient to return the 
-    intermediate results of decomposition as an integer, which includes the number 
-    of the Dec_Node_t in the array of decomposition nodes and the complemented flag.
-    Factoring is a special case of decomposition, which demonstrates this kind
-    of manipulation.
-*/
 
 ////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFITIONS                             ///
+///                        ITERATORS                                 ///
 ////////////////////////////////////////////////////////////////////////
 
+// interator throught the leaves
+#define Dec_GraphForEachLeaf( pGraph, pLeaf, i )                                              \
+    for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ )
+// interator throught the internal nodes
+#define Dec_GraphForEachNode( pGraph, pAnd, i )                                               \
+    for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== 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 ========================================================*/
+extern Dec_Man_t *    Dec_ManStart();
+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*************************************************************
 
-  Synopsis    [Cleans the decomposition node.]
+  Synopsis    [Creates an edge pointing to the node in the given polarity.]
 
   Description []
                
@@ -117,12 +123,16 @@ struct Dec_Node_t_
 
   SeeAlso     []
 
-***********************************************************************/ 
-static inline void         Dec_NodeClean( Dec_Node_t * pNode )       {  *((int *)pNode) = 0;           }
+***********************************************************************/
+static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )   
+{
+    Dec_Edge_t eEdge = { fCompl, Node }; 
+    return eEdge; 
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Convert between an interger and an decomposition node.]
+  Synopsis    [Converts the edge into unsigned integer.]
 
   Description []
                
@@ -131,12 +141,14 @@ static inline void         Dec_NodeClean( Dec_Node_t * pNode )       {  *((int *
   SeeAlso     []
 
 ***********************************************************************/
-static inline Dec_Node_t   Dec_Int2Node( int Num )                   {  return *((Dec_Node_t *)&Num);  }
-static inline int          Dec_Node2Int( Dec_Node_t Node )           {  return *((int *)&Node);        }
+static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )   
+{
+    return (eEdge.Node << 1) | eEdge.fCompl; 
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the i-th decomposition node.]
+  Synopsis    [Converts unsigned integer into the edge.]
 
   Description []
                
@@ -145,11 +157,14 @@ static inline int          Dec_Node2Int( Dec_Node_t Node )           {  return *
   SeeAlso     []
 
 ***********************************************************************/
-static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i )   {  return (Dec_Node_t *)vDec->pArray + i;  }
+static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )   
+{
+    return Dec_EdgeCreate( Edge >> 1, Edge & 1 ); 
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the last decomposition node.]
+  Synopsis    [Converts the edge into unsigned integer.]
 
   Description []
                
@@ -158,11 +173,14 @@ static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i )   {  return (
   SeeAlso     []
 
 ***********************************************************************/
-static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec )      {  return (Dec_Node_t *)vDec->pArray + vDec->nSize - 1;  }
+static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )   
+{
+    return *(unsigned *)&eEdge;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the fanins of the i-th decomposition node.]
+  Synopsis    [Converts unsigned integer into the edge.]
 
   Description []
                
@@ -171,12 +189,14 @@ static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec )      {  return (
   SeeAlso     []
 
 ***********************************************************************/
-static inline Dec_Node_t * Dec_NodeFanin0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin0;  }
-static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin1;  }
+static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )   
+{
+    return *(Dec_Edge_t *)&Edge;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the complemented attributes of the i-th decomposition node.]
+  Synopsis    [Creates a graph with the given number of leaves.]
 
   Description []
                
@@ -185,12 +205,22 @@ static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( D
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool         Dec_NodeFaninC0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl0;  }
-static inline bool         Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl1;  }
+static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )   
+{
+    Dec_Graph_t * pGraph;
+    pGraph = ALLOC( Dec_Graph_t, 1 );
+    memset( pGraph, 0, sizeof(Dec_Graph_t) );
+    pGraph->nLeaves = nLeaves;
+    pGraph->nSize = nLeaves;
+    pGraph->nCap = 2 * nLeaves + 50;
+    pGraph->pNodes = ALLOC( Dec_Node_t, pGraph->nCap );
+    memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
+    return pGraph;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of leaf variables.]
+  Synopsis    [Creates constant 0 graph.]
 
   Description []
                
@@ -199,18 +229,19 @@ static inline bool         Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert(
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Dec_TreeNumVars( Vec_Int_t * vDec )
+static inline Dec_Graph_t * Dec_GraphCreateConst0()   
 {
-    int i;
-    for ( i = 0; i < vDec->nSize; i++ )
-        if ( vDec->pArray[i] )
-            break;
-    return i;
+    Dec_Graph_t * pGraph;
+    pGraph = ALLOC( Dec_Graph_t, 1 );
+    memset( pGraph, 0, sizeof(Dec_Graph_t) );
+    pGraph->fConst = 1;
+    pGraph->eRoot.fCompl = 1;
+    return pGraph;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of AND nodes in the tree.]
+  Synopsis    [Creates constant 1 graph.]
 
   Description []
                
@@ -219,20 +250,56 @@ static inline int Dec_TreeNumVars( Vec_Int_t * vDec )
   SeeAlso     []
 
 ***********************************************************************/
-static int Dec_TreeNumAnds( Vec_Int_t * vDec )
+static inline Dec_Graph_t * Dec_GraphCreateConst1()   
 {
-    Dec_Node_t * pNode;
-    pNode = Dec_NodeReadLast(vDec);
-    if ( pNode->fConst ) // constant
-        return 0;
-    if ( pNode->iFanin0 == pNode->iFanin1 ) // literal
-        return 0;
-    return vDec->nSize - Dec_TreeNumVars(vDec);
+    Dec_Graph_t * pGraph;
+    pGraph = ALLOC( Dec_Graph_t, 1 );
+    memset( pGraph, 0, sizeof(Dec_Graph_t) );
+    pGraph->fConst = 1;
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the literal graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )   
+{
+    Dec_Graph_t * pGraph;
+    assert( 0 <= iLeaf && iLeaf < nLeaves );
+    pGraph = Dec_GraphCreate( nLeaves );
+    pGraph->eRoot.Node   = iLeaf;
+    pGraph->eRoot.fCompl = fCompl;
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a graph with the given number of leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Dec_GraphFree( Dec_Graph_t * pGraph )   
+{
+    FREE( pGraph->pNodes );
+    free( pGraph );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of literals in the factored form.]
+  Synopsis    [Returns 1 if the graph is a constant.]
 
   Description []
                
@@ -241,16 +308,30 @@ static int Dec_TreeNumAnds( Vec_Int_t * vDec )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec )
+static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )   
 {
-    return 1 + Dec_TreeNumAnds( vDec );
+    return pGraph->fConst;
 }
 
+/**Function*************************************************************
 
+  Synopsis    [Returns 1 if the graph is constant 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
+{
+    return pGraph->fConst && pGraph->eRoot.fCompl;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the output node of the decomposition tree is complemented.]
+  Synopsis    [Returns 1 if the graph is constant 1.]
 
   Description []
                
@@ -259,11 +340,14 @@ static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm )  { return Dec_NodeReadLast(vForm)->fCompl;  }
+static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
+{
+    return pGraph->fConst && !pGraph->eRoot.fCompl;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Complements the output node of the decomposition tree.]
+  Synopsis    [Returns 1 if the graph is complemented.]
 
   Description []
                
@@ -272,12 +356,31 @@ static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm )  { return Dec_NodeR
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Dec_TreeComplement( Vec_Int_t * vForm )    {  Dec_NodeReadLast(vForm)->fCompl ^= 1;   }
+static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
+{
+    return pGraph->eRoot.fCompl;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the graph is complemented.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Dec_GraphComplement( Dec_Graph_t * pGraph )   
+{
+    pGraph->eRoot.fCompl ^= 1;
+}
 
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the output node is a constant.]
+  Synopsis    [Returns the number of leaves.]
 
   Description []
                
@@ -286,13 +389,14 @@ static inline void Dec_TreeComplement( Vec_Int_t * vForm )    {  Dec_NodeReadLas
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_TreeIsConst( Vec_Int_t * vForm )             {   return Dec_NodeReadLast(vForm)->fConst;  }
-static inline bool Dec_TreeIsConst0( Vec_Int_t * vForm )            {   return Dec_NodeReadLast(vForm)->fConst &&  Dec_NodeReadLast(vForm)->fCompl;  }
-static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm )            {   return Dec_NodeReadLast(vForm)->fConst && !Dec_NodeReadLast(vForm)->fCompl;  }
+static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )   
+{
+    return pGraph->nLeaves;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a constant 0 decomposition tree.]
+  Synopsis    [Returns the number of internal nodes.]
 
   Description []
                
@@ -301,23 +405,14 @@ static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm )            {   return D
   SeeAlso     []
 
 ***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateConst0()
+static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )   
 {
-    Vec_Int_t * vForm;
-    Dec_Node_t * pNode;
-    // create the constant node
-    vForm = Vec_IntAlloc( 1 );
-    Vec_IntPush( vForm, 0 );
-    pNode = Dec_NodeReadLast( vForm );
-    pNode->fIntern = 1;
-    pNode->fConst  = 1;
-    pNode->fCompl  = 1;
-    return vForm;
+    return pGraph->nSize - pGraph->nLeaves;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a constant 1 decomposition tree.]
+  Synopsis    [Returns the pointer to the node.]
 
   Description []
                
@@ -326,24 +421,30 @@ static inline Vec_Int_t * Dec_TreeCreateConst0()
   SeeAlso     []
 
 ***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateConst1()
+static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )   
 {
-    Vec_Int_t * vForm;
-    Dec_Node_t * pNode;
-    // create the constant node
-    vForm = Vec_IntAlloc( 1 );
-    Vec_IntPush( vForm, 0 );
-    pNode = Dec_NodeReadLast( vForm );
-    pNode->fIntern = 1;
-    pNode->fConst  = 1;
-    pNode->fCompl  = 0;
-    return vForm;
+    return pGraph->pNodes + i;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph )   
+{
+    return pGraph->pNodes + pGraph->nSize - 1;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the decomposition tree is an elementary var.]
+  Synopsis    [Returns the number of the given node.]
 
   Description []
                
@@ -352,14 +453,14 @@ static inline Vec_Int_t * Dec_TreeCreateConst1()
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_TreeIsVar( Vec_Int_t * vForm )
+static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
 {
-    return Dec_NodeReadLast(vForm)->iFanin0 == Dec_NodeReadLast(vForm)->iFanin1;
+    return pNode - pGraph->pNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the decomposition tree to represent an elementary var.]
+  Synopsis    [Check if the graph represents elementary variable.]
 
   Description []
                
@@ -368,19 +469,177 @@ static inline bool Dec_TreeIsVar( Vec_Int_t * vForm )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateVar( int iVar, int nVars, int fCompl )
+static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )   
+{
+    return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the graph represents elementary variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
+{
+    return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the elementary variable elementary variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph )   
+{
+    assert( Dec_GraphIsVar( pGraph ) );
+    return Dec_GraphNode( pGraph, pGraph->eRoot.Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the elementary variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph )   
+{
+    assert( Dec_GraphIsVar( pGraph ) );
+    return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the root of the graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot )   
+{
+    pGraph->eRoot = eRoot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends a new node to the graph.]
+
+  Description [This procedure is meant for internal use.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )   
+{
+    Dec_Node_t * pNode;
+    if ( pGraph->nSize == pGraph->nCap )
+    {
+        pGraph->pNodes = REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
+        pGraph->nCap   = 2 * pGraph->nCap;
+    }
+    pNode = pGraph->pNodes + pGraph->nSize++;
+    memset( pNode, 0, sizeof(Dec_Node_t) );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an AND node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
+{
+    Dec_Node_t * pNode;
+    // get the new node
+    pNode = Dec_GraphAppendNode( pGraph );
+    // set the inputs and other info
+    pNode->eEdge0 = eEdge0;
+    pNode->eEdge1 = eEdge1;
+    pNode->fCompl0 = eEdge0.fCompl;
+    pNode->fCompl1 = eEdge1.fCompl;
+    return Dec_EdgeCreate( pGraph->nSize - 1, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an OR node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
 {
-    Vec_Int_t * vForm;
     Dec_Node_t * pNode;
-    // create the elementary variable node
-    vForm = Vec_IntAlloc( nVars + 1 );
-    Vec_IntFill( vForm, nVars + 1, 0 );
-    pNode = Dec_NodeReadLast( vForm );
-    pNode->iFanin0 = iVar;
-    pNode->iFanin1 = iVar;
-    pNode->fIntern = 1;
-    pNode->fCompl  = fCompl;
-    return vForm;
+    // get the new node
+    pNode = Dec_GraphAppendNode( pGraph );
+    // set the inputs and other info
+    pNode->eEdge0 = eEdge0;
+    pNode->eEdge1 = eEdge1;
+    pNode->fCompl0 = eEdge0.fCompl;
+    pNode->fCompl1 = eEdge1.fCompl;
+    // make adjustments for the OR gate
+    pNode->fNodeOr = 1;
+    pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
+    pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
+    return Dec_EdgeCreate( pGraph->nSize - 1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an XOR node.]
+
+  Description []
+               
+  SideEffects []
+
+  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 );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
new file mode 100644
index 00000000..9931b136
--- /dev/null
+++ b/src/opt/dec/decAbc.c
@@ -0,0 +1,170 @@
+/**CFile****************************************************************
+
+  FileName    [decAbc.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Interface between the decomposition package and ABC network.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: decAbc.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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_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(pMan), 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( pMan, pAnd0, pAnd1 );
+    }
+    // complement the result if necessary
+    return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of new nodes added when using this graph.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
+  of the leaves of the graph before calling this procedure. 
+  Returns -1 if the number of nodes and levels exceeded the given limit or 
+  the number of levels exceeded the maximum allowed level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+    Abc_Aig_t * pMan = pRoot->pNtk->pManFunc;
+    Dec_Node_t * pNode, * pNode0, * pNode1;
+    Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+    int i, Counter, LevelNew, LevelOld;
+    // check for constant function or a literal
+    if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+        return 0;
+    // set the levels of the leaves
+    Dec_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->Level = Abc_ObjRegular(pNode->pFunc)->Level;
+    // compute the AIG size after adding the internal nodes
+    Counter = 0;
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        // get the children of this node
+        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+        // get the AIG nodes corresponding to the children 
+        pAnd0 = pNode0->pFunc; 
+        pAnd1 = pNode1->pFunc; 
+        if ( pAnd0 && pAnd1 )
+        {
+            // if they are both present, find the resulting node
+            pAnd0 = Abc_ObjNotCond( pAnd0, pNode->eEdge0.fCompl );
+            pAnd1 = Abc_ObjNotCond( pAnd1, pNode->eEdge1.fCompl );
+            pAnd  = Abc_AigAndLookup( pMan, pAnd0, pAnd1 );
+            // return -1 if the node is the same as the original root
+            if ( Abc_ObjRegular(pAnd) == pRoot )
+                return -1;
+        }
+        else
+            pAnd = NULL;
+        // count the number of added nodes
+        if ( pAnd == NULL || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pAnd)) )
+        {
+            if ( ++Counter > NodeMax )
+                return -1;
+        }
+        // count the number of new levels
+        LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level );
+        if ( pAnd )
+        {
+            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 );
+        }
+        if ( LevelNew > LevelMax )
+            return -1;
+        pNode->pFunc = pAnd;
+        pNode->Level = LevelNew;
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
+{
+    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 );
+    // remove the old nodes
+    Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
+    // compare the gains
+    nNodesNew = Abc_NtkNodeNum(pNtk);
+    assert( nGain <= nNodesOld - nNodesNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
new file mode 100644
index 00000000..f6654476
--- /dev/null
+++ b/src/opt/dec/decFactor.c
@@ -0,0 +1,393 @@
+/**CFile****************************************************************
+
+  FileName    [ftFactor.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures for algebraic factoring.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "main.h"
+#include "mvc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Dec_Edge_t       Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
+static Dec_Edge_t       Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
+static Dec_Edge_t       Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
+static Dec_Edge_t       Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits );
+static Dec_Edge_t       Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
+static int              Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm );
+static Mvc_Cover_t *    Dec_ConvertSopToMvc( char * pSop );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Factors the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Dec_Factor( char * pSop )
+{
+    Mvc_Cover_t * pCover;
+    Dec_Graph_t * pFForm;
+    Dec_Edge_t eRoot;
+
+    // derive the cover from the SOP representation
+    pCover = Dec_ConvertSopToMvc( pSop );
+
+    // make sure the cover is CCS free (should be done before CST)
+    Mvc_CoverContain( pCover );
+    // check for trivial functions
+    if ( Mvc_CoverIsEmpty(pCover) )
+    {
+        Mvc_CoverFree( pCover );
+        return Dec_GraphCreateConst0();
+    }
+    if ( Mvc_CoverIsTautology(pCover) )
+    {
+        Mvc_CoverFree( pCover );
+        return Dec_GraphCreateConst1();
+    }
+
+    // perform CST
+    Mvc_CoverInverse( pCover ); // CST
+    // start the factored form
+    pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
+    // factor the cover
+    eRoot = Dec_Factor_rec( pFForm, pCover );
+    // finalize the factored form
+    Dec_GraphSetRoot( pFForm, eRoot );
+    // complement the factored form if SOP is complemented
+    if ( Abc_SopIsComplement(pSop) )
+        Dec_GraphComplement( pFForm );
+    // verify the factored form
+//    if ( !Dec_FactorVerify( pSop, pFForm ) )
+//        printf( "Verification has failed.\n" );
+//    Mvc_CoverInverse( pCover ); // undo CST
+    Mvc_CoverFree( pCover );
+    return pFForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Internal recursive factoring procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
+    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+    Dec_Edge_t eNodeAnd, eNode;
+
+    // make sure the cover contains some cubes
+    assert( Mvc_CoverReadCubeNum(pCover) );
+
+    // get the divisor
+    pDiv = Mvc_CoverDivisor( pCover );
+    if ( pDiv == NULL )
+        return Dec_FactorTrivial( pFForm, pCover );
+
+    // divide the cover by the divisor
+    Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem );
+    assert( Mvc_CoverReadCubeNum(pQuo) );
+
+    Mvc_CoverFree( pDiv );
+    Mvc_CoverFree( pRem );
+
+    // check the trivial case
+    if ( Mvc_CoverReadCubeNum(pQuo) == 1 )
+    {
+        eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo );
+        Mvc_CoverFree( pQuo );
+        return eNode;
+    }
+
+    // make the quotient cube free
+    Mvc_CoverMakeCubeFree( pQuo );
+
+    // divide the cover by the quotient
+    Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem );
+
+    // check the trivial case
+    if ( Mvc_CoverIsCubeFree( pDiv ) )
+    {
+        eNodeDiv = Dec_Factor_rec( pFForm, pDiv );
+        eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
+        Mvc_CoverFree( pDiv );
+        Mvc_CoverFree( pQuo );
+        eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+        if ( Mvc_CoverReadCubeNum(pRem) == 0 )
+        {
+            Mvc_CoverFree( pRem );
+            return eNodeAnd;
+        }
+        else
+        {
+            eNodeRem = Dec_Factor_rec( pFForm, pRem );
+            Mvc_CoverFree( pRem );
+            return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+        }
+    }
+
+    // get the common cube
+    pCom = Mvc_CoverCommonCubeCover( pDiv );
+    Mvc_CoverFree( pDiv );
+    Mvc_CoverFree( pQuo );
+    Mvc_CoverFree( pRem );
+
+    // solve the simple problem
+    eNode = Dec_FactorLF_rec( pFForm, pCover, pCom );
+    Mvc_CoverFree( pCom );
+    return eNode;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Internal recursive factoring procedure for the leaf case.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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());
+    Vec_Int_t * vEdgeLits  = pManDec->vLits;
+    Mvc_Cover_t * pDiv, * pQuo, * pRem;
+    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+    Dec_Edge_t eNodeAnd;
+
+    // get the most often occurring literal
+    pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple );
+    // divide the cover by the literal
+    Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem );
+    // get the node pointer for the literal
+    eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits );
+    Mvc_CoverFree( pDiv );
+    // factor the quotient and remainder
+    eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
+    Mvc_CoverFree( pQuo );
+    eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+    if ( Mvc_CoverReadCubeNum(pRem) == 0 )
+    {
+        Mvc_CoverFree( pRem );
+        return eNodeAnd;
+    }
+    else
+    {
+        eNodeRem = Dec_Factor_rec( pFForm, pRem );
+        Mvc_CoverFree( pRem );
+        return Dec_GraphAddNodeOr( pFForm,  eNodeAnd, eNodeRem );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Factoring the cover, which has no algebraic divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
+{
+    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;
+    Dec_Edge_t eNode;
+    Mvc_Cube_t * pCube;
+    // create the factored form for each cube
+    Vec_IntClear( vEdgeCubes );
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits );
+        Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
+    }
+    // balance the factored forms
+    return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Factoring the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    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 );
+        }
+    // balance the factored forms
+    return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Create the well-balanced tree of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
+{
+    Dec_Edge_t eNode1, eNode2;
+    int nNodes1, nNodes2;
+
+    if ( nNodes == 1 )
+        return peNodes[0];
+
+    // split the nodes into two parts
+    nNodes1 = nNodes/2;
+    nNodes2 = nNodes - nNodes1;
+//    nNodes2 = nNodes/2;
+//    nNodes1 = nNodes - nNodes2;
+
+    // recursively construct the tree for the parts
+    eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes,           nNodes1, fNodeOr );
+    eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
+
+    if ( fNodeOr )
+        return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
+    else
+        return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts SOP into MVC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
+{
+    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Mvc_Manager_t * pMem = pManDec->pMvcMem;
+    Mvc_Cover_t * pMvc;
+    Mvc_Cube_t * pMvcCube;
+    char * pCube;
+    int nVars, Value, v;
+
+    // start the cover
+    nVars = Abc_SopGetVarNum(pSop);
+    pMvc = Mvc_CoverAlloc( pMem, nVars * 2 );
+    // check the logic function of the node
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        // create and add the cube
+        pMvcCube = Mvc_CubeAlloc( pMvc );
+        Mvc_CoverAddCubeTail( pMvc, pMvcCube );
+        // fill in the literals
+        Mvc_CubeBitFill( pMvcCube );
+        Abc_CubeForEachVar( pCube, Value, v )
+        {
+            if ( Value == '0' )
+                Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 );
+            else if ( Value == '1' )
+                Mvc_CubeBitRemove( pMvcCube, v * 2 );
+        }
+    }
+    return pMvc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the factoring is correct.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
+{
+    DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() );
+    DdNode * bFunc1, * bFunc2;
+    int RetValue;
+    bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
+    bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );   Cudd_Ref( bFunc2 );
+//Extra_bddPrint( dd, bFunc1 ); printf("\n");
+//Extra_bddPrint( dd, bFunc2 ); printf("\n");
+    RetValue = (bFunc1 == bFunc2);
+    if ( bFunc1 != bFunc2 )
+    {
+        int s;
+        Extra_bddPrint( dd, bFunc1 ); printf("\n");
+        Extra_bddPrint( dd, bFunc2 ); printf("\n");
+        s  = 0;
+    }
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    Cudd_RecursiveDeref( dd, bFunc2 );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c
new file mode 100644
index 00000000..1d44d5cb
--- /dev/null
+++ b/src/opt/dec/decMan.c
@@ -0,0 +1,83 @@
+/**CFile****************************************************************
+
+  FileName    [decMan.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Decomposition manager.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: decMan.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "mvc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the MVC manager used in the factoring package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Man_t * Dec_ManStart()
+{
+    Dec_Man_t * p;
+    int clk = clock();
+    p = ALLOC( Dec_Man_t, 1 );
+    p->pMvcMem = Mvc_ManagerStart();
+    p->vCubes = Vec_IntAlloc( 8 );
+    p->vLits = Vec_IntAlloc( 8 );
+    // canonical forms, phases, perms
+    Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
+//PRT( "NPN classes precomputation time", clock() - clk ); 
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the MVC maanager used in the factoring package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dec_ManStop( Dec_Man_t * p )
+{
+    Mvc_ManagerFree( p->pMvcMem );
+    Vec_IntFree( p->vCubes );
+    Vec_IntFree( p->vLits );
+    free( p->puCanons );
+    free( p->pPhases );
+    free( p->pPerms );
+    free( p->pMap );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c
new file mode 100644
index 00000000..6fb20327
--- /dev/null
+++ b/src/opt/dec/decPrint.c
@@ -0,0 +1,221 @@
+/**CFile****************************************************************
+
+  FileName    [decPrint.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures to print the decomposition graphs (factored forms).]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: decPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void   Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax );
+static int    Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] );
+static void   Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax );
+static int    Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decomposition graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut )
+{
+    Vec_Ptr_t * vNamesIn = NULL;
+    int LitSizeMax, LitSizeCur, Pos, i;
+
+    // create the names if not given by the user
+    if ( pNamesIn == NULL )
+    {
+        vNamesIn = Abc_NodeGetFakeNames( Dec_GraphLeaveNum(pGraph) );
+        pNamesIn = (char **)vNamesIn->pArray;
+    }
+    if ( pNameOut == NULL )
+        pNameOut = "F";
+
+    // get the size of the longest literal
+    LitSizeMax = 0;
+    for ( i = 0; i < Dec_GraphLeaveNum(pGraph); i++ )
+    {
+        LitSizeCur = strlen(pNamesIn[i]);
+        if ( LitSizeMax < LitSizeCur )
+            LitSizeMax = LitSizeCur;
+    }
+    if ( LitSizeMax > 50 )
+        LitSizeMax = 20;
+
+    // write the decomposition graph (factored form)
+    if ( Dec_GraphIsConst(pGraph) ) // constant
+    {
+        Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 );
+        fprintf( pFile, "Constant %d", !Dec_GraphIsComplement(pGraph) );
+    }
+    else if ( Dec_GraphIsVar(pGraph) ) // literal
+    {
+        Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 );
+        Dec_GraphPrintGetLeafName( pFile, Dec_GraphVarInt(pGraph), Dec_GraphIsComplement(pGraph), pNamesIn );
+    }
+    else
+    {
+        Pos = Dec_GraphPrintOutputName( pFile, pNameOut, Dec_GraphIsComplement(pGraph) );
+        Dec_GraphPrint_rec( pFile, pGraph, Dec_GraphNodeLast(pGraph), 0, pNamesIn, &Pos, LitSizeMax );
+    }
+    fprintf( pFile, "\n" );
+
+    if ( vNamesIn )
+        Abc_NodeFreeNames( vNamesIn );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  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;
+    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 ( !pNode->fNodeOr ) // FT_NODE_AND )
+    {
+        if ( !pNode0->fNodeOr ) // != FT_NODE_OR )
+            Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+        else
+        {
+            fprintf( pFile, "(" );
+            (*pPos)++;
+            Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+            fprintf( pFile, ")" );
+            (*pPos)++;
+        }
+        fprintf( pFile, " " );
+        (*pPos)++;
+
+        Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax );
+
+        if ( !pNode1->fNodeOr ) // != FT_NODE_OR )
+            Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+        else
+        {
+            fprintf( pFile, "(" );
+            (*pPos)++;
+            Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+            fprintf( pFile, ")" );
+            (*pPos)++;
+        }
+        return;
+    }
+    if ( pNode->fNodeOr ) // FT_NODE_OR )
+    {
+        Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+        fprintf( pFile, " + " );
+        (*pPos) += 3;
+
+        Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax );
+
+        Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+        return;
+    }
+    assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] )
+{
+    static char Buffer[100];
+    sprintf( Buffer, "%s%s", pNamesIn[iLeaf], fCompl? "\'" : "" );
+    fprintf( pFile, "%s", Buffer );
+    return strlen( Buffer );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax )
+{
+    int i;
+    if ( *pPos + LitSizeMax < 77 )
+        return;
+    fprintf( pFile, "\n" );
+    for ( i = 0; i < 10; i++ )
+        fprintf( pFile, " " );
+    *pPos = 10;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the printout for a decomposition graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl )
+{
+    if ( pNameOut == NULL )
+        return 0;
+    fprintf( pFile, "%6s%s = ", pNameOut, fCompl? "\'" : " " );
+    return 10;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c
new file mode 100644
index 00000000..02c3346e
--- /dev/null
+++ b/src/opt/dec/decUtil.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+  FileName    [decUtil.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Decomposition unitilies.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: decUtil.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts graph to BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    Dec_Node_t * pNode;
+    int i;
+
+    // sanity checks
+    assert( Dec_GraphLeaveNum(pGraph) >= 0 );
+    assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );
+
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) );
+
+    // assign the elementary variables
+    Dec_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = Cudd_bddIthVar( dd, i );
+
+    // compute the function for each internal node
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( pNode->pFunc );
+    }
+
+    // deref the intermediate results
+    bFunc = pNode->pFunc;   Cudd_Ref( bFunc );
+    Dec_GraphForEachNode( pGraph, pNode, i )
+        Cudd_RecursiveDeref( dd, pNode->pFunc );
+    Cudd_Deref( bFunc );
+
+    // complement the result if necessary
+    return Cudd_NotCond( bFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph )
+{
+    unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned uTruth, uTruth0, uTruth1;
+    Dec_Node_t * pNode;
+    int i;
+
+    // sanity checks
+    assert( Dec_GraphLeaveNum(pGraph) >= 0 );
+    assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );
+    assert( Dec_GraphLeaveNum(pGraph) <= 5 );
+
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Dec_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Dec_GraphIsComplement(pGraph)? ~uTruths[Dec_GraphVarInt(pGraph)] : uTruths[Dec_GraphVarInt(pGraph)];
+
+    // assign the elementary variables
+    Dec_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = (void *)uTruths[i];
+
+    // compute the function for each internal node
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        uTruth0 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
+        uTruth1 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
+        uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
+        uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
+        uTruth = uTruth0 & uTruth1;
+        pNode->pFunc = (void *)uTruth;
+    }
+
+    // complement the result if necessary
+    return Dec_GraphIsComplement(pGraph)? ~uTruth : uTruth;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/module.make b/src/opt/dec/module.make
index d6d908e7..1e0722d5 100644
--- a/src/opt/dec/module.make
+++ b/src/opt/dec/module.make
@@ -1 +1,5 @@
-SRC += 
+SRC +=  src/opt/dec/decAbc.c \
+        src/opt/dec/decFactor.c \
+        src/opt/dec/decMan.c \
+        src/opt/dec/decPrint.c \
+        src/opt/dec/decUtil.c