src/opt/dec/decFactor.c File Reference

#include "abc.h"
#include "main.h"
#include "mvc.h"
#include "dec.h"
Include dependency graph for decFactor.c:

Go to the source code of this file.

Functions

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)
Dec_Graph_t * Dec_Factor (char *pSop)

Function Documentation

Mvc_Cover_t * Dec_ConvertSopToMvc ( char *  pSop  )  [static]

Function*************************************************************

Synopsis [Converts SOP into MVC.]

Description []

SideEffects []

SeeAlso []

Definition at line 323 of file decFactor.c.

00324 {
00325     Dec_Man_t * pManDec = Abc_FrameReadManDec();
00326     Mvc_Manager_t * pMem = pManDec->pMvcMem;
00327     Mvc_Cover_t * pMvc;
00328     Mvc_Cube_t * pMvcCube;
00329     char * pCube;
00330     int nVars, Value, v;
00331 
00332     // start the cover
00333     nVars = Abc_SopGetVarNum(pSop);
00334     pMvc = Mvc_CoverAlloc( pMem, nVars * 2 );
00335     // check the logic function of the node
00336     Abc_SopForEachCube( pSop, nVars, pCube )
00337     {
00338         // create and add the cube
00339         pMvcCube = Mvc_CubeAlloc( pMvc );
00340         Mvc_CoverAddCubeTail( pMvc, pMvcCube );
00341         // fill in the literals
00342         Mvc_CubeBitFill( pMvcCube );
00343         Abc_CubeForEachVar( pCube, Value, v )
00344         {
00345             if ( Value == '0' )
00346                 Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 );
00347             else if ( Value == '1' )
00348                 Mvc_CubeBitRemove( pMvcCube, v * 2 );
00349         }
00350     }
00351     return pMvc;
00352 }

Dec_Graph_t* Dec_Factor ( char *  pSop  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Factors the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file decFactor.c.

00052 {
00053     Mvc_Cover_t * pCover;
00054     Dec_Graph_t * pFForm;
00055     Dec_Edge_t eRoot;
00056 
00057     // derive the cover from the SOP representation
00058     pCover = Dec_ConvertSopToMvc( pSop );
00059 
00060     // make sure the cover is CCS free (should be done before CST)
00061     Mvc_CoverContain( pCover );
00062     // check for trivial functions
00063     if ( Mvc_CoverIsEmpty(pCover) )
00064     {
00065         Mvc_CoverFree( pCover );
00066         return Dec_GraphCreateConst0();
00067     }
00068     if ( Mvc_CoverIsTautology(pCover) )
00069     {
00070         Mvc_CoverFree( pCover );
00071         return Dec_GraphCreateConst1();
00072     }
00073 
00074     // perform CST
00075     Mvc_CoverInverse( pCover ); // CST
00076     // start the factored form
00077     pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
00078     // factor the cover
00079     eRoot = Dec_Factor_rec( pFForm, pCover );
00080     // finalize the factored form
00081     Dec_GraphSetRoot( pFForm, eRoot );
00082     // complement the factored form if SOP is complemented
00083     if ( Abc_SopIsComplement(pSop) )
00084         Dec_GraphComplement( pFForm );
00085     // verify the factored form
00086 //    if ( !Dec_FactorVerify( pSop, pFForm ) )
00087 //        printf( "Verification has failed.\n" );
00088 //    Mvc_CoverInverse( pCover ); // undo CST
00089     Mvc_CoverFree( pCover );
00090     return pFForm;
00091 }

Dec_Edge_t Dec_Factor_rec ( Dec_Graph_t *  pFForm,
Mvc_Cover_t *  pCover 
) [static]

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

] DECLARATIONS ///

Function*************************************************************

Synopsis [Internal recursive factoring procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file decFactor.c.

00105 {
00106     Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
00107     Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
00108     Dec_Edge_t eNodeAnd, eNode;
00109 
00110     // make sure the cover contains some cubes
00111     assert( Mvc_CoverReadCubeNum(pCover) );
00112 
00113     // get the divisor
00114     pDiv = Mvc_CoverDivisor( pCover );
00115     if ( pDiv == NULL )
00116         return Dec_FactorTrivial( pFForm, pCover );
00117 
00118     // divide the cover by the divisor
00119     Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem );
00120     assert( Mvc_CoverReadCubeNum(pQuo) );
00121 
00122     Mvc_CoverFree( pDiv );
00123     Mvc_CoverFree( pRem );
00124 
00125     // check the trivial case
00126     if ( Mvc_CoverReadCubeNum(pQuo) == 1 )
00127     {
00128         eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo );
00129         Mvc_CoverFree( pQuo );
00130         return eNode;
00131     }
00132 
00133     // make the quotient cube free
00134     Mvc_CoverMakeCubeFree( pQuo );
00135 
00136     // divide the cover by the quotient
00137     Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem );
00138 
00139     // check the trivial case
00140     if ( Mvc_CoverIsCubeFree( pDiv ) )
00141     {
00142         eNodeDiv = Dec_Factor_rec( pFForm, pDiv );
00143         eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
00144         Mvc_CoverFree( pDiv );
00145         Mvc_CoverFree( pQuo );
00146         eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
00147         if ( Mvc_CoverReadCubeNum(pRem) == 0 )
00148         {
00149             Mvc_CoverFree( pRem );
00150             return eNodeAnd;
00151         }
00152         else
00153         {
00154             eNodeRem = Dec_Factor_rec( pFForm, pRem );
00155             Mvc_CoverFree( pRem );
00156             return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
00157         }
00158     }
00159 
00160     // get the common cube
00161     pCom = Mvc_CoverCommonCubeCover( pDiv );
00162     Mvc_CoverFree( pDiv );
00163     Mvc_CoverFree( pQuo );
00164     Mvc_CoverFree( pRem );
00165 
00166     // solve the simple problem
00167     eNode = Dec_FactorLF_rec( pFForm, pCover, pCom );
00168     Mvc_CoverFree( pCom );
00169     return eNode;
00170 }

Dec_Edge_t Dec_FactorLF_rec ( Dec_Graph_t *  pFForm,
Mvc_Cover_t *  pCover,
Mvc_Cover_t *  pSimple 
) [static]

Function*************************************************************

Synopsis [Internal recursive factoring procedure for the leaf case.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file decFactor.c.

00185 {
00186     Dec_Man_t * pManDec = Abc_FrameReadManDec();
00187     Vec_Int_t * vEdgeLits  = pManDec->vLits;
00188     Mvc_Cover_t * pDiv, * pQuo, * pRem;
00189     Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
00190     Dec_Edge_t eNodeAnd;
00191 
00192     // get the most often occurring literal
00193     pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple );
00194     // divide the cover by the literal
00195     Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem );
00196     // get the node pointer for the literal
00197     eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits );
00198     Mvc_CoverFree( pDiv );
00199     // factor the quotient and remainder
00200     eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
00201     Mvc_CoverFree( pQuo );
00202     eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
00203     if ( Mvc_CoverReadCubeNum(pRem) == 0 )
00204     {
00205         Mvc_CoverFree( pRem );
00206         return eNodeAnd;
00207     }
00208     else
00209     {
00210         eNodeRem = Dec_Factor_rec( pFForm, pRem );
00211         Mvc_CoverFree( pRem );
00212         return Dec_GraphAddNodeOr( pFForm,  eNodeAnd, eNodeRem );
00213     }
00214 }

Dec_Edge_t Dec_FactorTrivial ( Dec_Graph_t *  pFForm,
Mvc_Cover_t *  pCover 
) [static]

Function*************************************************************

Synopsis [Factoring the cover, which has no algebraic divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file decFactor.c.

00230 {
00231     Dec_Man_t * pManDec = Abc_FrameReadManDec();
00232     Vec_Int_t * vEdgeCubes = pManDec->vCubes;
00233     Vec_Int_t * vEdgeLits  = pManDec->vLits;
00234     Mvc_Manager_t * pMem = pManDec->pMvcMem;
00235     Dec_Edge_t eNode;
00236     Mvc_Cube_t * pCube;
00237     // create the factored form for each cube
00238     Vec_IntClear( vEdgeCubes );
00239     Mvc_CoverForEachCube( pCover, pCube )
00240     {
00241         eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits );
00242         Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
00243     }
00244     // balance the factored forms
00245     return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
00246 }

Dec_Edge_t Dec_FactorTrivialCube ( Dec_Graph_t *  pFForm,
Mvc_Cover_t *  pCover,
Mvc_Cube_t *  pCube,
Vec_Int_t *  vEdgeLits 
) [static]

Function*************************************************************

Synopsis [Factoring the cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file decFactor.c.

00260 {
00261     Dec_Edge_t eNode;
00262     int iBit, Value;
00263     // create the factored form for each literal
00264     Vec_IntClear( vEdgeLits );
00265     Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
00266         if ( Value )
00267         {
00268             eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
00269             Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
00270         }
00271     // balance the factored forms
00272     return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
00273 }

Dec_Edge_t Dec_FactorTrivialTree_rec ( Dec_Graph_t *  pFForm,
Dec_Edge_t *  peNodes,
int  nNodes,
int  fNodeOr 
) [static]

Function*************************************************************

Synopsis [Create the well-balanced tree of nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file decFactor.c.

00287 {
00288     Dec_Edge_t eNode1, eNode2;
00289     int nNodes1, nNodes2;
00290 
00291     if ( nNodes == 1 )
00292         return peNodes[0];
00293 
00294     // split the nodes into two parts
00295     nNodes1 = nNodes/2;
00296     nNodes2 = nNodes - nNodes1;
00297 //    nNodes2 = nNodes/2;
00298 //    nNodes1 = nNodes - nNodes2;
00299 
00300     // recursively construct the tree for the parts
00301     eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes,           nNodes1, fNodeOr );
00302     eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
00303 
00304     if ( fNodeOr )
00305         return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
00306     else
00307         return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
00308 }

int Dec_FactorVerify ( char *  pSop,
Dec_Graph_t *  pFForm 
) [static]

Function*************************************************************

Synopsis [Verifies that the factoring is correct.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file decFactor.c.

00366 {
00367     DdManager * dd = Abc_FrameReadManDd();
00368     DdNode * bFunc1, * bFunc2;
00369     int RetValue;
00370     bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
00371     bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );   Cudd_Ref( bFunc2 );
00372 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
00373 //Extra_bddPrint( dd, bFunc2 ); printf("\n");
00374     RetValue = (bFunc1 == bFunc2);
00375     if ( bFunc1 != bFunc2 )
00376     {
00377         int s;
00378         Extra_bddPrint( dd, bFunc1 ); printf("\n");
00379         Extra_bddPrint( dd, bFunc2 ); printf("\n");
00380         s  = 0;
00381     }
00382     Cudd_RecursiveDeref( dd, bFunc1 );
00383     Cudd_RecursiveDeref( dd, bFunc2 );
00384     return RetValue;
00385 }

Generated on Tue Jan 5 12:19:25 2010 for abc70930 by  doxygen 1.6.1