summaryrefslogtreecommitdiffstats
path: root/src/opt/dec/decFactor.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
commite54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch)
treede3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/opt/dec/decFactor.c
parent7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff)
downloadabc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip
Version abc70930
Diffstat (limited to 'src/opt/dec/decFactor.c')
-rw-r--r--src/opt/dec/decFactor.c392
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 ///
-////////////////////////////////////////////////////////////////////////
-
-