diff options
Diffstat (limited to 'src/bool/dec/decFactor.c')
| -rw-r--r-- | src/bool/dec/decFactor.c | 399 |
1 files changed, 399 insertions, 0 deletions
diff --git a/src/bool/dec/decFactor.c b/src/bool/dec/decFactor.c new file mode 100644 index 00000000..faed9e74 --- /dev/null +++ b/src/bool/dec/decFactor.c @@ -0,0 +1,399 @@ +/**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 "src/base/abc/abc.h" +#include "src/base/main/main.h" +#include "src/misc/mvc/mvc.h" +#include "src/misc/extra/extraBdd.h" +#include "dec.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// 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 ABC_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 = (Dec_Man_t *)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 = (Dec_Man_t *)Abc_FrameReadManDec(); + Vec_Int_t * vEdgeCubes = pManDec->vCubes; + Vec_Int_t * vEdgeLits = pManDec->vLits; + 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 = (Dec_Man_t *)Abc_FrameReadManDec(); + Mvc_Manager_t * pMem = (Mvc_Manager_t *)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 ) +{ + extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars ); + extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ); + DdManager * dd = (DdManager *)Abc_FrameReadManDd(); + DdNode * bFunc1, * bFunc2; + int RetValue; + bFunc1 = Abc_ConvertSopToBdd( dd, pSop, NULL ); 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 /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |