Version abc70930

1 files changed, 0 insertions, 392 deletions

diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
deleted file mode 100644
index dca422ea..00000000
--- a/src/opt/dec/decFactor.c
+++ /dev/null
@@ -1,392 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ftFactor.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures for algebraic factoring.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "main.h"
-#include "mvc.h"
-#include "dec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Dec_Edge_t       Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
-static Dec_Edge_t       Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
-static Dec_Edge_t       Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
-static Dec_Edge_t       Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits );
-static Dec_Edge_t       Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
-static int              Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm );
-static Mvc_Cover_t *    Dec_ConvertSopToMvc( char * pSop );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Factors the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Dec_Factor( char * pSop )
-{
-    Mvc_Cover_t * pCover;
-    Dec_Graph_t * pFForm;
-    Dec_Edge_t eRoot;
-
-    // derive the cover from the SOP representation
-    pCover = Dec_ConvertSopToMvc( pSop );
-
-    // make sure the cover is CCS free (should be done before CST)
-    Mvc_CoverContain( pCover );
-    // check for trivial functions
-    if ( Mvc_CoverIsEmpty(pCover) )
-    {
-        Mvc_CoverFree( pCover );
-        return Dec_GraphCreateConst0();
-    }
-    if ( Mvc_CoverIsTautology(pCover) )
-    {
-        Mvc_CoverFree( pCover );
-        return Dec_GraphCreateConst1();
-    }
-
-    // perform CST
-    Mvc_CoverInverse( pCover ); // CST
-    // start the factored form
-    pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
-    // factor the cover
-    eRoot = Dec_Factor_rec( pFForm, pCover );
-    // finalize the factored form
-    Dec_GraphSetRoot( pFForm, eRoot );
-    // complement the factored form if SOP is complemented
-    if ( Abc_SopIsComplement(pSop) )
-        Dec_GraphComplement( pFForm );
-    // verify the factored form
-//    if ( !Dec_FactorVerify( pSop, pFForm ) )
-//        printf( "Verification has failed.\n" );
-//    Mvc_CoverInverse( pCover ); // undo CST
-    Mvc_CoverFree( pCover );
-    return pFForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
-{
-    Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
-    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
-    Dec_Edge_t eNodeAnd, eNode;
-
-    // make sure the cover contains some cubes
-    assert( Mvc_CoverReadCubeNum(pCover) );
-
-    // get the divisor
-    pDiv = Mvc_CoverDivisor( pCover );
-    if ( pDiv == NULL )
-        return Dec_FactorTrivial( pFForm, pCover );
-
-    // divide the cover by the divisor
-    Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem );
-    assert( Mvc_CoverReadCubeNum(pQuo) );
-
-    Mvc_CoverFree( pDiv );
-    Mvc_CoverFree( pRem );
-
-    // check the trivial case
-    if ( Mvc_CoverReadCubeNum(pQuo) == 1 )
-    {
-        eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo );
-        Mvc_CoverFree( pQuo );
-        return eNode;
-    }
-
-    // make the quotient cube free
-    Mvc_CoverMakeCubeFree( pQuo );
-
-    // divide the cover by the quotient
-    Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem );
-
-    // check the trivial case
-    if ( Mvc_CoverIsCubeFree( pDiv ) )
-    {
-        eNodeDiv = Dec_Factor_rec( pFForm, pDiv );
-        eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
-        Mvc_CoverFree( pDiv );
-        Mvc_CoverFree( pQuo );
-        eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-        if ( Mvc_CoverReadCubeNum(pRem) == 0 )
-        {
-            Mvc_CoverFree( pRem );
-            return eNodeAnd;
-        }
-        else
-        {
-            eNodeRem = Dec_Factor_rec( pFForm, pRem );
-            Mvc_CoverFree( pRem );
-            return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
-        }
-    }
-
-    // get the common cube
-    pCom = Mvc_CoverCommonCubeCover( pDiv );
-    Mvc_CoverFree( pDiv );
-    Mvc_CoverFree( pQuo );
-    Mvc_CoverFree( pRem );
-
-    // solve the simple problem
-    eNode = Dec_FactorLF_rec( pFForm, pCover, pCom );
-    Mvc_CoverFree( pCom );
-    return eNode;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure for the leaf case.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
-{
-    Dec_Man_t * pManDec = Abc_FrameReadManDec();
-    Vec_Int_t * vEdgeLits  = pManDec->vLits;
-    Mvc_Cover_t * pDiv, * pQuo, * pRem;
-    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
-    Dec_Edge_t eNodeAnd;
-
-    // get the most often occurring literal
-    pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple );
-    // divide the cover by the literal
-    Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem );
-    // get the node pointer for the literal
-    eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits );
-    Mvc_CoverFree( pDiv );
-    // factor the quotient and remainder
-    eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
-    Mvc_CoverFree( pQuo );
-    eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-    if ( Mvc_CoverReadCubeNum(pRem) == 0 )
-    {
-        Mvc_CoverFree( pRem );
-        return eNodeAnd;
-    }
-    else
-    {
-        eNodeRem = Dec_Factor_rec( pFForm, pRem );
-        Mvc_CoverFree( pRem );
-        return Dec_GraphAddNodeOr( pFForm,  eNodeAnd, eNodeRem );
-    }
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cover, which has no algebraic divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
-{
-    Dec_Man_t * pManDec = Abc_FrameReadManDec();
-    Vec_Int_t * vEdgeCubes = pManDec->vCubes;
-    Vec_Int_t * vEdgeLits  = pManDec->vLits;
-    Mvc_Manager_t * pMem = pManDec->pMvcMem;
-    Dec_Edge_t eNode;
-    Mvc_Cube_t * pCube;
-    // create the factored form for each cube
-    Vec_IntClear( vEdgeCubes );
-    Mvc_CoverForEachCube( pCover, pCube )
-    {
-        eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits );
-        Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
-    }
-    // balance the factored forms
-    return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits )
-{
-    Dec_Edge_t eNode;
-    int iBit, Value;
-    // create the factored form for each literal
-    Vec_IntClear( vEdgeLits );
-    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
-        if ( Value )
-        {
-            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
-            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
-        }
-    // balance the factored forms
-    return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Create the well-balanced tree of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
-{
-    Dec_Edge_t eNode1, eNode2;
-    int nNodes1, nNodes2;
-
-    if ( nNodes == 1 )
-        return peNodes[0];
-
-    // split the nodes into two parts
-    nNodes1 = nNodes/2;
-    nNodes2 = nNodes - nNodes1;
-//    nNodes2 = nNodes/2;
-//    nNodes1 = nNodes - nNodes2;
-
-    // recursively construct the tree for the parts
-    eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes,           nNodes1, fNodeOr );
-    eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
-
-    if ( fNodeOr )
-        return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
-    else
-        return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Converts SOP into MVC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
-{
-    Dec_Man_t * pManDec = Abc_FrameReadManDec();
-    Mvc_Manager_t * pMem = pManDec->pMvcMem;
-    Mvc_Cover_t * pMvc;
-    Mvc_Cube_t * pMvcCube;
-    char * pCube;
-    int nVars, Value, v;
-
-    // start the cover
-    nVars = Abc_SopGetVarNum(pSop);
-    pMvc = Mvc_CoverAlloc( pMem, nVars * 2 );
-    // check the logic function of the node
-    Abc_SopForEachCube( pSop, nVars, pCube )
-    {
-        // create and add the cube
-        pMvcCube = Mvc_CubeAlloc( pMvc );
-        Mvc_CoverAddCubeTail( pMvc, pMvcCube );
-        // fill in the literals
-        Mvc_CubeBitFill( pMvcCube );
-        Abc_CubeForEachVar( pCube, Value, v )
-        {
-            if ( Value == '0' )
-                Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 );
-            else if ( Value == '1' )
-                Mvc_CubeBitRemove( pMvcCube, v * 2 );
-        }
-    }
-    return pMvc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
-{
-    DdManager * dd = Abc_FrameReadManDd();
-    DdNode * bFunc1, * bFunc2;
-    int RetValue;
-    bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
-    bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );   Cudd_Ref( bFunc2 );
-//Extra_bddPrint( dd, bFunc1 ); printf("\n");
-//Extra_bddPrint( dd, bFunc2 ); printf("\n");
-    RetValue = (bFunc1 == bFunc2);
-    if ( bFunc1 != bFunc2 )
-    {
-        int s;
-        Extra_bddPrint( dd, bFunc1 ); printf("\n");
-        Extra_bddPrint( dd, bFunc2 ); printf("\n");
-        s  = 0;
-    }
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    Cudd_RecursiveDeref( dd, bFunc2 );
-    return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-