diff options
Diffstat (limited to 'src/opt/kit')
-rw-r--r-- | src/opt/kit/kit.h | 12 | ||||
-rw-r--r-- | src/opt/kit/kitBdd.c | 32 | ||||
-rw-r--r-- | src/opt/kit/kitFactor.c | 1 | ||||
-rw-r--r-- | src/opt/kit/kitGraph.c | 33 | ||||
-rw-r--r-- | src/opt/kit/kitIsop.c | 7 |
5 files changed, 62 insertions, 23 deletions
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h index d97fca58..58c55cd2 100644 --- a/src/opt/kit/kit.h +++ b/src/opt/kit/kit.h @@ -91,6 +91,9 @@ struct Kit_Graph_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define KIT_MIN(a,b) (((a) < (b))? (a) : (b)) +#define KIT_MAX(a,b) (((a) > (b))? (a) : (b)) + #ifndef ALLOC #define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) #endif @@ -143,8 +146,10 @@ static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i ) static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; } static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; } static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; } -static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); } -static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) );} +static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); } +static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); } +static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); } +static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); } static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } @@ -272,7 +277,7 @@ static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * p /*=== kitBdd.c ==========================================================*/ extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars ); extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph ); -extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars ); +extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop ); /*=== kitFactor.c ==========================================================*/ extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory ); /*=== kitGraph.c ==========================================================*/ @@ -288,6 +293,7 @@ extern Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEd extern Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type ); extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ); extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); +extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf ); /*=== kitHop.c ==========================================================*/ /*=== kitIsop.c ==========================================================*/ extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); diff --git a/src/opt/kit/kitBdd.c b/src/opt/kit/kitBdd.c index ed978740..9c8d4f7a 100644 --- a/src/opt/kit/kitBdd.c +++ b/src/opt/kit/kitBdd.c @@ -135,26 +135,26 @@ DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph ) SeeAlso [] ***********************************************************************/ -DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal ) +DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop ) { DdNode * bF0, * bF1, * bF; - if ( nVars == 0 ) + int Var; + if ( nVars <= 5 ) { - if ( pTruth[iBit>>5] & (1 << iBit&31) ) - return b1; - return b0; - } - if ( nVars == 5 ) - { - if ( pTruth[iBit>>5] == 0xFFFFFFFF ) - return b1; - if ( pTruth[iBit>>5] == 0 ) + unsigned uTruth, uMask; + uMask = ((~(unsigned)0) >> (32 - (1<<nVars))); + uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask; + if ( uTruth == 0 ) return b0; + if ( uTruth == uMask ) + return b1; } + // find the variable to use + Var = fMSBonTop? nVarsTotal-nVars : nVars-1; // other special cases can be added - bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal ); Cudd_Ref( bF0 ); - bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal ); Cudd_Ref( bF1 ); - bF = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 ); Cudd_Ref( bF ); + bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal, fMSBonTop ); Cudd_Ref( bF0 ); + bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop ); Cudd_Ref( bF1 ); + bF = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 ); Cudd_Ref( bF ); Cudd_RecursiveDeref( dd, bF0 ); Cudd_RecursiveDeref( dd, bF1 ); Cudd_Deref( bF ); @@ -176,9 +176,9 @@ DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nV SeeAlso [] ***********************************************************************/ -DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars ) +DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop ) { - return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars ); + return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop ); } /**Function************************************************************* diff --git a/src/opt/kit/kitFactor.c b/src/opt/kit/kitFactor.c index 618a4272..cbac918d 100644 --- a/src/opt/kit/kitFactor.c +++ b/src/opt/kit/kitFactor.c @@ -197,6 +197,7 @@ Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, i { Kit_Edge_t eNode1, eNode2; int i, iLit, nLits, nLits1, nLits2; + assert( uCube ); // count the number of literals in this interval nLits = 0; for ( i = nStart; i < nFinish; i++ ) diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c index e2172ca3..1123b90e 100644 --- a/src/opt/kit/kitGraph.c +++ b/src/opt/kit/kitGraph.c @@ -354,13 +354,40 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor Kit_Graph_t * pGraph; int RetValue; // derive SOP - RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); - assert( RetValue == 0 ); + RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); // tried 1 and found not useful in "renode" + if ( RetValue == -1 ) + return NULL; + assert( RetValue == 0 || RetValue == 1 ); // derive factored form - pGraph = Kit_SopFactor( vMemory, 0, nVars, vMemory ); + pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory ); return pGraph; } +/**Function************************************************************* + + Synopsis [Derives the maximum depth from the leaf to the root.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf ) +{ + int Depth0, Depth1, Depth; + if ( pNode == pLeaf ) + return 0; + if ( Kit_GraphNodeIsVar(pGraph, pNode) ) + return -100; + Depth0 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin0(pGraph, pNode), pLeaf ); + Depth1 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin1(pGraph, pNode), pLeaf ); + Depth = KIT_MAX( Depth0, Depth1 ); + Depth = (Depth == -100) ? -100 : Depth + 1; + return Depth; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/kit/kitIsop.c b/src/opt/kit/kitIsop.c index 420cb16f..d54932ee 100644 --- a/src/opt/kit/kitIsop.c +++ b/src/opt/kit/kitIsop.c @@ -67,9 +67,14 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB if ( pcRes->nCubes == -1 ) { vMemory->nSize = -1; - return 0; + return -1; } assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) ) + { + Vec_IntShrink( vMemory, pcRes->nCubes ); + return 0; + } if ( fTryBoth ) { // compute ISOP for the complemented polarity |