Version abc70930

7 files changed, 0 insertions, 1922 deletions

diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
deleted file mode 100644
index 41d22649..00000000
--- a/src/opt/dec/dec.h
+++ /dev/null
@@ -1,719 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [dec.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [A simple decomposition tree/node data structure and its APIs.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: dec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __DEC_H__
-#define __DEC_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         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_
-{
-    Dec_Edge_t        eEdge0;          // the left child of the node
-    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
-    // 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;
-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
-};
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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_Ntk_t * pNtk, Dec_Graph_t * pGraph );
-extern Abc_Obj_t *    Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, 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, bool fUpdateLevel, 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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates an edge pointing to the node in the given polarity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )   
-{
-    Dec_Edge_t eEdge = { fCompl, Node }; 
-    return eEdge; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the edge into unsigned integer.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )   
-{
-    return (eEdge.Node << 1) | eEdge.fCompl; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts unsigned integer into the edge.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )   
-{
-    return Dec_EdgeCreate( Edge >> 1, Edge & 1 ); 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the edge into unsigned integer.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )   
-{
-    return *(unsigned *)&eEdge;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts unsigned integer into the edge.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )   
-{
-    return *(Dec_Edge_t *)&Edge;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a graph with the given number of leaves.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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    [Creates constant 0 graph.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Graph_t * Dec_GraphCreateConst0()   
-{
-    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    [Creates constant 1 graph.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Graph_t * Dec_GraphCreateConst1()   
-{
-    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 1 if the graph is a constant.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )   
-{
-    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    [Returns 1 if the graph is constant 1.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
-{
-    return pGraph->fConst && !pGraph->eRoot.fCompl;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the graph is complemented.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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    [Returns the number of leaves.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )   
-{
-    return pGraph->nLeaves;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )   
-{
-    return pGraph->nSize - pGraph->nLeaves;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the pointer to the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )   
-{
-    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    [Returns the number of the given node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
-{
-    return pNode - pGraph->pNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check if the graph represents elementary variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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 )
-{
-    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;
-    // 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, 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                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
deleted file mode 100644
index bd960c14..00000000
--- a/src/opt/dec/decAbc.c
+++ /dev/null
@@ -1,305 +0,0 @@
-/**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"
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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_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(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 );
-    }
-    // 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) );
-}
-
-/**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(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 );
-        }
-        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, bool fUpdateLevel, 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, pGraph );
-    // remove the old nodes
-    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
deleted file mode 100644
index dca422ea..00000000
--- a/src/opt/dec/decFactor.c
+++ /dev/null
@@ -1,392 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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();
-    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();
-    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) );
-        }
-    // 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();
-    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();
-    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
deleted file mode 100644
index 65857461..00000000
--- a/src/opt/dec/decMan.c
+++ /dev/null
@@ -1,83 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 2d8f09b3..00000000
--- a/src/opt/dec/decPrint.c
+++ /dev/null
@@ -1,284 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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_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);
-    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     []
-
-***********************************************************************/
-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];
-    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
deleted file mode 100644
index 463bc7e2..00000000
--- a/src/opt/dec/decUtil.c
+++ /dev/null
@@ -1,134 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 1e0722d5..00000000
--- a/src/opt/dec/module.make
+++ /dev/null
@@ -1,5 +0,0 @@
-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