Version abc50902

4 files changed, 0 insertions, 1214 deletions

diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h
deleted file mode 100644
index da162e99..00000000
--- a/src/sop/ft/ft.h
+++ /dev/null
@@ -1,109 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ft.h]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Data structure for algebraic factoring.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: ft.h,v 1.1 2003/05/22 19:20:04 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __FT_H__
-#define __FT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Ft_Node_t_ Ft_Node_t;
-struct Ft_Node_t_
-{
-    // the first child
-    unsigned   fCompl0  :  1;    // complemented attribute
-    unsigned   iFanin0  : 11;    // fanin number
-    // the second child
-    unsigned   fCompl1  :  1;    // complemented attribute
-    unsigned   iFanin1  : 11;    // fanin number (1-based)
-    // other info
-    unsigned   fIntern  :  1;    // marks any node that is not an elementary var
-    unsigned   fConst   :  1;    // marks the constant 1 function
-    unsigned   fCompl   :  1;    // marks the complement of topmost node
-    // printing info
-    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 unused
-};
-
-/*
-    The factored form of an SOP is an array (Vec_Int_t) of entries of type Ft_Node_t.
-    If the SOP has n input variables (some of them may not be in the true support)
-    the first n entries of the factored form array are zeros. The other entries of the array
-    represent the internal AND nodes of the factored form, and possibly the constant node.
-    This representation makes it easy to translate the factored form into an AIG.
-    The factored AND nodes contains fanins of the node and their complemented attributes 
-    (using AIG semantics). The elementary variable (buffer or interver) are represented 
-    as a node with the same fanins. For example: x' = AND( x', x' ).
-    The constant node is represented a special node with the constant flag set. 
-    If the constant node and the elementary variable are present, no other internal 
-    AND nodes are allowed in the factored form.
-*/
-
-// working with complemented attributes of objects
-static inline bool        Ptr_IsComplement( void * p )    { return (bool)(((unsigned)p) & 01);     }
-static inline void *      Ptr_Regular( void * p )         { return (void *)((unsigned)(p) & ~01);  }
-static inline void *      Ptr_Not( void * p )             { return (void *)((unsigned)(p) ^  01);  }
-static inline void *      Ptr_NotCond( void * p, int c )  { return (void *)((unsigned)(p) ^ (c));  }
-
-static inline Ft_Node_t * Ft_NodeRead( Vec_Int_t * vForm, int i )   {  return (Ft_Node_t *)vForm->pArray + i;  }
-static inline Ft_Node_t * Ft_NodeReadLast( Vec_Int_t * vForm )      {  return (Ft_Node_t *)vForm->pArray + vForm->nSize - 1;  }
-static inline Ft_Node_t * Ft_NodeFanin0( Vec_Int_t * vForm, Ft_Node_t * pNode )   { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin0;  }
-static inline Ft_Node_t * Ft_NodeFanin1( Vec_Int_t * vForm, Ft_Node_t * pNode )   { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin1;  }
-
-static inline Ft_Node_t   Ft_Int2Node( int Num  )                   {  return *((Ft_Node_t *)&Num);  }
-static inline int         Ft_Node2Int( Ft_Node_t Node )             {  return *((int *)&Node);       }
-static inline void        Ft_NodeClean( Ft_Node_t * pNode )         {  *((int *)pNode) = 0;          }
-
-////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== ftFactor.c =====================================================*/
-extern void               Ft_FactorStartMan();
-extern void               Ft_FactorStopMan();
-extern Vec_Int_t *        Ft_Factor( char * pSop );
-extern int                Ft_FactorGetNumNodes( Vec_Int_t * vForm );
-extern int                Ft_FactorGetNumVars( Vec_Int_t * vForm );
-extern void               Ft_FactorComplement( Vec_Int_t * vForm );
-extern Vec_Int_t *        Ft_FactorConst( int fConst1 );
-extern Vec_Int_t *        Ft_FactorVar( int iVar, int nVars, int fCompl );
-/*=== ftPrint.c =====================================================*/
-extern void               Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut );
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-#endif
-
diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c
deleted file mode 100644
index 0a32e1c8..00000000
--- a/src/sop/ft/ftFactor.c
+++ /dev/null
@@ -1,867 +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 "mvc.h"
-#include "ft.h"
-#include "dec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// the types of nodes in FFs
-enum { FT_NODE_NONE, FT_NODE_AND, FT_NODE_OR, FT_NODE_INV, FT_NODE_LEAF, FT_NODE_0, FT_NODE_1 };
-
-static Ft_Node_t *       Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover );
-static Ft_Node_t *       Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
-
-static Ft_Node_t *       Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover );
-static Ft_Node_t *       Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
-static Ft_Node_t *       Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd );
-static Ft_Node_t *       Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover );
-static Ft_Node_t *       Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
-
-static Ft_Node_t *       Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 );
-static Ft_Node_t *       Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit );
-static void              Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pNode, int nVars );
-
-// temporary procedures that work with the covers
-static Mvc_Cover_t *     Ft_ConvertSopToMvc( char * pSop );
-static int               Ft_FactorVerify( char * pSop, Vec_Int_t * vForm );
-
-// temporary managers
-static Mvc_Manager_t *   pMem = NULL;
-static DdManager *       dd = NULL;
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Factors the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ft_Factor( char * pSop )
-{
-    Vec_Int_t * vForm;
-    Ft_Node_t * pNode;
-    Mvc_Cover_t * pCover;
-    int nVars = Abc_SopGetVarNum( pSop );
-
-    // derive the cover from the SOP representation
-    pCover = Ft_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 Ft_FactorConst( 0 );
-    }
-    if ( Mvc_CoverIsTautology(pCover) )
-    {
-        Mvc_CoverFree( pCover );
-        return Ft_FactorConst( 1 );
-    }
-
-    // perform CST
-    Mvc_CoverInverse( pCover ); // CST
-
-    // start the factored form
-    vForm = Vec_IntAlloc( 1000 );
-    Vec_IntFill( vForm, nVars, 0 );
-    // factor the cover
-    pNode = Ft_Factor_rec( vForm, pCover );
-    // finalize the factored form
-    Ft_FactorFinalize( vForm, pNode, nVars );
-    // check if the cover was originally complented
-    if ( Abc_SopGetPhase(pSop) == 0 )
-        Ft_FactorComplement( vForm );
-
-    // verify the factored form
-//    if ( !Ft_FactorVerify( pSop, vForm ) )
-//        printf( "Verification has failed.\n" );
-
-//    Mvc_CoverInverse( pCover ); // undo CST
-    Mvc_CoverFree( pCover );
-    return vForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover )
-{
-    Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
-    Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem;
-    Ft_Node_t * pNodeAnd, * pNode;
-
-    // make sure the cover contains some cubes
-    assert( Mvc_CoverReadCubeNum(pCover) );
-
-    // get the divisor
-    pDiv = Mvc_CoverDivisor( pCover );
-    if ( pDiv == NULL )
-        return Ft_FactorTrivial( vForm, 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 )
-    {
-        pNode = Ft_FactorLF_rec( vForm, pCover, pQuo );
-        Mvc_CoverFree( pQuo );
-        return pNode;
-    }
-
-    // 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 ) )
-    {
-        pNodeDiv = Ft_Factor_rec( vForm, pDiv );
-        pNodeQuo = Ft_Factor_rec( vForm, pQuo );
-        Mvc_CoverFree( pDiv );
-        Mvc_CoverFree( pQuo );
-        pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo );
-        if ( Mvc_CoverReadCubeNum(pRem) == 0 )
-        {
-            Mvc_CoverFree( pRem );
-            return pNodeAnd;
-        }
-        else
-        {
-            pNodeRem = Ft_Factor_rec( vForm, pRem );
-            Mvc_CoverFree( pRem );
-            return Ft_FactorNodeCreate( vForm, FT_NODE_OR,  pNodeAnd, pNodeRem );
-        }
-    }
-
-    // get the common cube
-    pCom = Mvc_CoverCommonCubeCover( pDiv );
-    Mvc_CoverFree( pDiv );
-    Mvc_CoverFree( pQuo );
-    Mvc_CoverFree( pRem );
-
-    // solve the simple problem
-    pNode = Ft_FactorLF_rec( vForm, pCover, pCom );
-    Mvc_CoverFree( pCom );
-    return pNode;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure for the leaf case.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
-{
-    Mvc_Cover_t * pDiv, * pQuo, * pRem;
-    Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem;
-    Ft_Node_t * pNodeAnd;
-
-    // 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
-    pNodeDiv = Ft_FactorTrivialCube( vForm, pDiv, Mvc_CoverReadCubeHead(pDiv) );
-    Mvc_CoverFree( pDiv );
-    // factor the quotient and remainder
-    pNodeQuo = Ft_Factor_rec( vForm, pQuo );
-    Mvc_CoverFree( pQuo );
-    pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo );
-    if ( Mvc_CoverReadCubeNum(pRem) == 0 )
-    {
-        Mvc_CoverFree( pRem );
-        return pNodeAnd;
-    }
-    else
-    {
-        pNodeRem = Ft_Factor_rec( vForm, pRem );
-        Mvc_CoverFree( pRem );
-        return Ft_FactorNodeCreate( vForm, FT_NODE_OR,  pNodeAnd, pNodeRem );
-    }
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cover, which has no algebraic divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover )
-{
-    Ft_Node_t ** ppNodes;
-    Ft_Node_t * pNode;
-    Mvc_Cube_t * pCube;
-    int i, nNodes;
-
-    // create space to put the cubes
-    nNodes = Mvc_CoverReadCubeNum(pCover);
-    assert( nNodes > 0 );
-    ppNodes = ALLOC( Ft_Node_t *, nNodes );
-    // create the factored form for each cube
-    i = 0;
-    Mvc_CoverForEachCube( pCover, pCube )
-        ppNodes[i++] = Ft_FactorTrivialCube( vForm, pCover, pCube );
-    assert( i == nNodes );
-    // balance the factored forms
-    pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, nNodes, 0 );
-    free( ppNodes );
-    return pNode;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
-{
-    Ft_Node_t ** ppNodes;
-    Ft_Node_t * pNode;
-    int iBit, Value, i;
-
-    // create space to put each literal
-    ppNodes = ALLOC( Ft_Node_t *, pCover->nBits );
-    // create the factored form for each literal
-    i = 0;
-    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
-    {
-        if ( Value )
-            ppNodes[i++] = Ft_FactorLeafCreate( vForm, iBit );
-    }
-    assert( i > 0 && i < pCover->nBits );
-    // balance the factored forms
-    pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, i, 1 );
-    free( ppNodes );
-    return pNode;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Create the well-balanced tree of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd )
-{
-    Ft_Node_t * pNode1, * pNode2;
-    int nNodes1, nNodes2;
-
-    if ( nNodes == 1 )
-        return ppNodes[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
-    pNode1 = Ft_FactorTrivialTree_rec( vForm, ppNodes,           nNodes1, fAnd );
-    pNode2 = Ft_FactorTrivialTree_rec( vForm, ppNodes + nNodes1, nNodes2, fAnd );
-
-    return Ft_FactorNodeCreate( vForm, fAnd? FT_NODE_AND : FT_NODE_OR, pNode1, pNode2 );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cover, which has no algebraic divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover )
-{
-    Ft_Node_t * pNode;
-    Mvc_Cube_t * pCube;
-
-    // iterate through the cubes
-    pNode = NULL;
-    Mvc_CoverForEachCube( pCover, pCube )
-    {
-        if ( pNode == NULL )
-            pNode = Ft_FactorTrivialCube( vForm, pCover, pCube );
-        else
-            pNode = Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNode, Ft_FactorTrivialCubeCascade( vForm, pCover, pCube ) );
-    }
-    assert( pNode ); // if this assertion fails, the input cover is not SCC-free
-    return pNode;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
-{
-    Ft_Node_t * pNode;
-    int iBit, Value;
-
-    // iterate through the literals
-    pNode = NULL;
-    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
-    {
-        if ( Value )
-        {
-            if ( pNode == NULL )
-                pNode = Ft_FactorLeafCreate( vForm, iBit );
-            else
-                pNode = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNode, Ft_FactorLeafCreate( vForm, iBit ) );
-        }
-    }
-    assert( pNode ); // if this assertion fails, the input cover is not SCC-free
-    return pNode;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 )
-{
-    Ft_Node_t * pNode;
-    // get the new node
-    Vec_IntPush( vForm, 0 );
-    pNode = Ft_NodeReadLast( vForm );
-    // set the inputs and other info
-    pNode->iFanin0 = (Ft_Node_t *)Ptr_Regular(pNode1) - (Ft_Node_t *)vForm->pArray;
-    pNode->iFanin1 = (Ft_Node_t *)Ptr_Regular(pNode2) - (Ft_Node_t *)vForm->pArray;
-    assert( pNode->iFanin0 < (unsigned)vForm->nSize );
-    assert( pNode->iFanin1 < (unsigned)vForm->nSize );
-    pNode->fIntern = 1;
-    pNode->fCompl  = 0;
-    pNode->fConst  = 0;
-    pNode->fEdge0  = Ptr_IsComplement(pNode1);
-    pNode->fEdge1  = Ptr_IsComplement(pNode2);
-    // consider specific gates
-    if ( Type == FT_NODE_OR )
-    {
-        pNode->fCompl0 = !Ptr_IsComplement(pNode1);
-        pNode->fCompl1 = !Ptr_IsComplement(pNode2);
-        pNode->fNodeOr = 1;
-        return Ptr_Not( pNode );
-    }
-    if ( Type == FT_NODE_AND )
-    {
-        pNode->fCompl0 = Ptr_IsComplement(pNode1);
-        pNode->fCompl1 = Ptr_IsComplement(pNode2);
-        pNode->fNodeOr = 0;
-        return pNode;
-    }
-    assert( 0 );
-    return NULL;
-
-/*
-    Vec_Int_t * vForm;
-    assert( pNode1 && pNode2 );
-    pNode = MEM_ALLOC( vForm->pMem, void, 1 );
-    memset( pNode, 0, sizeof(void) );
-    pNode->Type = Type;
-    pNode->pOne = pNode1;
-    pNode->pTwo = pNode2;
-    // update FF statistics
-    if ( pNode->Type == FT_NODE_LEAF )
-        vForm->nNodes++;
-    return pNode;
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ft_Node_t * Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit )
-{
-    return Ptr_NotCond( Ft_NodeRead(vForm, iLit/2), iLit%2 ); // using CST
-
-/*
-    Vm_VarMap_t * pVm;
-    int * pValuesFirst, * pValues;
-    int nValuesIn, nVarsIn;
-    Vec_Int_t * vForm;
-    int iVar;
-    pVm = vForm->pVm;
-    pValues      = Vm_VarMapReadValuesArray(pVm);
-    pValuesFirst = Vm_VarMapReadValuesFirstArray(pVm);
-    nValuesIn    = Vm_VarMapReadValuesInNum(pVm);
-    nVarsIn      = Vm_VarMapReadVarsInNum(pVm);
-    assert( iLit < nValuesIn );
-    for ( iVar = 0; iVar < nVarsIn; iVar++ )
-        if ( iLit < pValuesFirst[iVar] + pValues[iVar] )
-            break;
-    assert( iVar < nVarsIn );
-    pNode = Ft_FactorNodeCreate( vForm, FT_NODE_LEAF, NULL, NULL );
-    pNode->VarNum  = iVar;
-    pNode->nValues = pValues[iVar];
-    pNode->uData   = FT_MV_MASK(pNode->nValues) ^ (1 << (iLit - pValuesFirst[iVar]));
-    return pNode;
-*/
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Adds a single-variable literal if necessary.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pRoot, int nVars )
-{
-    Ft_Node_t * pRootR = Ptr_Regular(pRoot);
-    int iNode = pRootR - (Ft_Node_t *)vForm->pArray;
-    Ft_Node_t * pNode;
-    if ( iNode >= nVars )
-    {
-        // set the complemented attribute
-        pRootR->fCompl = Ptr_IsComplement(pRoot);
-        return;
-    }
-    // create a new node
-    Vec_IntPush( vForm, 0 );
-    pNode = Ft_NodeReadLast( vForm );
-    pNode->iFanin0 = iNode;
-    pNode->iFanin1 = iNode;
-    pNode->fIntern = 1;
-    pNode->fCompl  = Ptr_IsComplement(pRoot);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the number of variables in the factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ft_FactorGetNumVars( Vec_Int_t * vForm )
-{
-    int i;
-    for ( i = 0; i < vForm->nSize; i++ )
-        if ( vForm->pArray[i] )
-            break;
-    return i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the number of variables in the factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ft_FactorGetNumNodes( Vec_Int_t * vForm )
-{
-    Ft_Node_t * pNode;
-    int i;
-    pNode = Ft_NodeReadLast(vForm);
-    if ( pNode->fConst )
-        return 0;
-    if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal
-        return 1;
-    for ( i = 0; i < vForm->nSize; i++ )
-        if ( vForm->pArray[i] )
-            break;
-    return vForm->nSize - i + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Complements the factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorComplement( Vec_Int_t * vForm )
-{
-    Ft_Node_t * pNode;
-    pNode = Ft_NodeReadLast(vForm);
-    pNode->fCompl ^= 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a constant 0 or 1 factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ft_FactorConst( int fConst1 )
-{
-    Vec_Int_t * vForm;
-    Ft_Node_t * pNode;
-    // create the constant node
-    vForm = Vec_IntAlloc( 1 );
-    Vec_IntPush( vForm, 0 );
-    pNode = Ft_NodeReadLast( vForm );
-    pNode->fIntern = 1;
-    pNode->fConst  = 1;
-    pNode->fCompl  = !fConst1;
-    return vForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a constant 0 or 1 factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ft_FactorVar( int iVar, int nVars, int fCompl )
-{
-    Vec_Int_t * vForm;
-    Ft_Node_t * pNode;
-    // create the elementary variable node
-    vForm = Vec_IntAlloc( nVars + 1 );
-    Vec_IntFill( vForm, nVars + 1, 0 );
-    pNode = Ft_NodeReadLast( vForm );
-    pNode->iFanin0 = iVar;
-    pNode->iFanin1 = iVar;
-    pNode->fIntern = 1;
-    pNode->fCompl  = fCompl;
-    return vForm;
-}
-
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Start the MVC manager used in the factoring package.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorStartMan()
-{
-    assert( pMem == NULL );
-    pMem = Mvc_ManagerStart();
-    dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the MVC maanager used in the factoring package.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorStopMan()
-{
-    assert( pMem );
-    Mvc_ManagerFree( pMem );
-    Cudd_Quit( dd );
-    pMem = NULL;
-    dd = NULL;
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Converts SOP into MVC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Mvc_Cover_t * Ft_ConvertSopToMvc( char * pSop )
-{
-    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 );
-        }
-    }
-//Mvc_CoverPrint( pMvc );
-    return pMvc;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Converts SOP into BDD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Ft_ConvertSopToBdd( DdManager * dd, char * pSop )
-{
-    DdNode * bSum, * bCube, * bTemp, * bVar;
-    char * pCube;
-    int nVars, Value, v;
-    // start the cover
-    nVars = Abc_SopGetVarNum(pSop);
-    // check the logic function of the node
-    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
-    Abc_SopForEachCube( pSop, nVars, pCube )
-    {
-        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
-        Abc_CubeForEachVar( pCube, Value, v )
-        {
-            if ( Value == '0' )
-                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
-            else if ( Value == '1' )
-                bVar = Cudd_bddIthVar( dd, v );
-            else
-                continue;
-            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
-            Cudd_RecursiveDeref( dd, bTemp );
-        }
-        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   Cudd_Ref( bSum );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bCube );
-    }
-    // complement the result if necessary
-    bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
-    Cudd_Deref( bSum );
-    return bSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts SOP into BDD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Ft_ConvertFormToBdd( DdManager * dd, Vec_Int_t * vForm )
-{
-    Vec_Ptr_t * vFuncs;
-    DdNode * bFunc, * bFunc0, * bFunc1;
-    Ft_Node_t * pNode;
-    int i, nVars;
-
-    // sanity checks
-    nVars = Ft_FactorGetNumVars( vForm );
-    assert( nVars >= 0 );
-    assert( vForm->nSize > nVars );
-
-    // check for constant function
-    pNode = Ft_NodeRead( vForm, 0 );
-    if ( pNode->fConst )
-        return Cudd_NotCond( dd->one, pNode->fCompl );
-
-    // start the array of elementary variables
-    vFuncs = Vec_PtrAlloc( 20 );
-    for ( i = 0; i < nVars; i++ )
-        Vec_PtrPush( vFuncs, Cudd_bddIthVar(dd, i) );
-
-    // compute the functions of other nodes
-    for ( i = nVars; i < vForm->nSize; i++ )
-    {
-        pNode  = Ft_NodeRead( vForm, i );
-        bFunc0 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin0], pNode->fCompl0 ); 
-        bFunc1 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin1], pNode->fCompl1 ); 
-        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-        Vec_PtrPush( vFuncs, bFunc );
-    }
-    assert( vForm->nSize = vFuncs->nSize );
-
-    // deref the intermediate results
-    for ( i = nVars; i < vForm->nSize-1; i++ )
-        Cudd_RecursiveDeref( dd, (DdNode *)vFuncs->pArray[i] );
-    Vec_PtrFree( vFuncs );
-
-    // complement the result if necessary
-    pNode = Ft_NodeReadLast( vForm );
-    bFunc = Cudd_NotCond( bFunc, pNode->fCompl );
-
-    // return the result
-    Cudd_Deref( bFunc );
-    return bFunc;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ft_FactorVerify( char * pSop, Vec_Int_t * vForm )
-{
-    DdNode * bFunc1, * bFunc2;
-    int RetValue;
-    bFunc1 = Ft_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
-    bFunc2 = Ft_ConvertFormToBdd( dd, vForm );  Cudd_Ref( bFunc2 );
-//Extra_bddPrint( dd, bFunc1 ); printf("\n");
-//Extra_bddPrint( dd, bFunc2 ); printf("\n");
-    RetValue = (bFunc1 == bFunc2);
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    Cudd_RecursiveDeref( dd, bFunc2 );
-    return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sop/ft/ftPrint.c b/src/sop/ft/ftPrint.c
deleted file mode 100644
index 78f91b8f..00000000
--- a/src/sop/ft/ftPrint.c
+++ /dev/null
@@ -1,236 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ftPrint.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures to print the factored tree.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: ftPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "ft.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void   Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax );
-static int    Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] );
-static void   Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax );
-static int    Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fCompl );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut )
-{
-    Ft_Node_t * pNode;
-    Vec_Ptr_t * vNamesIn = NULL;
-    int LitSizeMax, LitSizeCur, nVars, Pos, i;
-
-    // sanity checks
-    nVars = Ft_FactorGetNumVars( vForm );
-    assert( nVars >= 0 );
-    assert( vForm->nSize > nVars );
-
-    // create the names if not given by the user
-    if ( pNamesIn == NULL )
-    {
-        vNamesIn = Abc_NodeGetFakeNames( nVars );
-        pNamesIn = (char **)vNamesIn->pArray;
-    }
-    if ( pNameOut == NULL )
-        pNameOut = "F";
-
-    // get the size of the longest literal
-    LitSizeMax = 0;
-    for ( i = 0; i < nVars; i++ )
-    {
-        LitSizeCur = strlen(pNamesIn[i]);
-        if ( LitSizeMax < LitSizeCur )
-            LitSizeMax = LitSizeCur;
-    }
-    if ( LitSizeMax > 50 )
-        LitSizeMax = 20;
-
-    // print the output name
-    pNode = Ft_NodeReadLast(vForm);
-    if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal
-    {
-        Pos = Ft_FactorPrintOutputName( pFile, pNameOut, 0 );
-        Ft_FactorPrintGetLeafName( pFile, vForm, Ft_NodeFanin0(vForm,pNode), pNode->fCompl, pNamesIn );
-    }
-    else // constant or non-trivial form
-    {
-        Pos = Ft_FactorPrintOutputName( pFile, pNameOut, pNode->fCompl );
-        Ft_FactorPrint_rec( pFile, vForm, pNode, 0, pNamesIn, &Pos, LitSizeMax );
-    }
-    fprintf( pFile, "\n" );
-
-    if ( vNamesIn )
-        Abc_NodeFreeNames( vNamesIn );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
-{
-    Ft_Node_t * pNode0, * pNode1;
-
-    if ( pNode->fConst ) // FT_NODE_0 )
-    {
-        if ( fCompl )
-            fprintf( pFile, "Constant 0" );
-        else
-            fprintf( pFile, "Constant 1" );
-        return;
-    }
-    if ( !pNode->fIntern ) // FT_NODE_LEAF )
-    {
-        (*pPos) += Ft_FactorPrintGetLeafName( pFile, vForm, pNode, fCompl, pNamesIn );
-        return;
-    }
-
-    pNode0 = Ft_NodeFanin0( vForm, pNode );
-    pNode1 = Ft_NodeFanin1( vForm, pNode );
-    if ( !pNode->fNodeOr ) // FT_NODE_AND )
-    {
-        if ( !pNode0->fNodeOr ) // != FT_NODE_OR )
-            Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax );
-        else
-        {
-            fprintf( pFile, "(" );
-            (*pPos)++;
-            Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax );
-            fprintf( pFile, ")" );
-            (*pPos)++;
-        }
-        fprintf( pFile, " " );
-        (*pPos)++;
-
-        Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax );
-
-        if ( !pNode1->fNodeOr ) // != FT_NODE_OR )
-            Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax );
-        else
-        {
-            fprintf( pFile, "(" );
-            (*pPos)++;
-            Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax );
-            fprintf( pFile, ")" );
-            (*pPos)++;
-        }
-        return;
-    }
-    if ( pNode->fNodeOr ) // FT_NODE_OR )
-    {
-        Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax );
-        fprintf( pFile, " + " );
-        (*pPos) += 3;
-
-        Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax );
-
-        Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax );
-        return;
-    }
-    assert( 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] )
-{
-    static char Buffer[100];
-    int iVar;
-    assert( !Ptr_IsComplement(pNode) );
-    iVar = (Ft_Node_t *)pNode - (Ft_Node_t *)vForm->pArray;
-    sprintf( Buffer, "%s%s", pNamesIn[iVar], fCompl? "\'" : "" );
-    fprintf( pFile, "%s", Buffer );
-    return strlen( Buffer );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ft_FactorPrintUpdatePos( 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 factored form or cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ft_FactorPrintOutputName( 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/sop/ft/module.make b/src/sop/ft/module.make
deleted file mode 100644
index 37e78ce6..00000000
--- a/src/sop/ft/module.make
+++ /dev/null
@@ -1,2 +0,0 @@
-SRC +=  src/sop/ft/ftFactor.c \
-    src/sop/ft/ftPrint.c