summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/kit/kit.h12
-rw-r--r--src/opt/kit/kitBdd.c32
-rw-r--r--src/opt/kit/kitFactor.c1
-rw-r--r--src/opt/kit/kitGraph.c33
-rw-r--r--src/opt/kit/kitIsop.c7
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 22:56:19 +0000