diff options
Diffstat (limited to 'src/opt/dec/decFactor.c')
| -rw-r--r-- | src/opt/dec/decFactor.c | 392 |
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 /// -//////////////////////////////////////////////////////////////////////// - - |