path: root/src/sop/ft/ftFactor.c

/**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                                ///
////////////////////////////////////////////////////////////////////////