Version abc50729

4 files changed, 1204 insertions, 0 deletions

diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h
new file mode 100644
index 00000000..81e1a2dc
--- /dev/null
+++ b/src/sop/ft/ft.h
@@ -0,0 +1,105 @@
+/**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 a SOP is an array (Vec_Int_t) of entries 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 have 0s. This representation 
+    makes it each to translate the factored form into an AIG.
+
+    The node structure 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 cannot be represented. Constant functions should be detected
+    before calling the factoring procedure.
+*/
+
+// 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 );
+/*=== 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
new file mode 100644
index 00000000..04779fe0
--- /dev/null
+++ b/src/sop/ft/ftFactor.c
@@ -0,0 +1,842 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        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 );
+static void              Ft_FactorComplement( Vec_Int_t * vForm );
+static Vec_Int_t *       Ft_FactorConst( int fConst1 );
+
+// 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;
+
+    // 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;
+    int nVars = Ft_FactorGetNumVars( vForm );
+    assert( nVars >= 0 );
+    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    [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
new file mode 100644
index 00000000..e08ceaae
--- /dev/null
+++ b/src/sop/ft/ftPrint.c
@@ -0,0 +1,255 @@
+/**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;
+    char Buffer[5];
+    int Pos, i, LitSizeMax, LitSizeCur, nVars;
+    int fMadeupNames;
+
+    // sanity checks
+    nVars = Ft_FactorGetNumVars( vForm );
+    assert( nVars >= 0 );
+    assert( vForm->nSize > nVars );
+
+    // create the names if not given by the user
+    fMadeupNames = 0;
+    if ( pNamesIn == NULL )
+    {
+        fMadeupNames = 1;
+        pNamesIn = ALLOC( char *, nVars );
+        for ( i = 0; i < nVars; i++ )
+        {
+            if ( nVars < 26 )
+            {
+                Buffer[0] = 'a' + i;
+                Buffer[1] = 0;
+            }
+            else
+            {
+                Buffer[0] = 'a' + i%26;
+                Buffer[1] = '0' + i/26;
+                Buffer[2] = 0;
+            }
+            pNamesIn[i] = util_strsav( Buffer );
+        }
+    }
+
+    // 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 ( fMadeupNames )
+    {
+        for ( i = 0; i < nVars; i++ )
+            free( pNamesIn[i] );
+        free( pNamesIn );
+    }
+}
+
+/**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
new file mode 100644
index 00000000..37e78ce6
--- /dev/null
+++ b/src/sop/ft/module.make
@@ -0,0 +1,2 @@
+SRC +=  src/sop/ft/ftFactor.c \
+    src/sop/ft/ftPrint.c