Adding command 'testdec'.

2 files changed, 93 insertions, 8 deletions

diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index dfee532e..8151f1d2 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -112,17 +112,17 @@ struct Kit_DsdObj_t_
     unsigned       Offset     : 8;  // offset to the truth table
     unsigned       nRefs      : 8;  // offset to the truth table
     unsigned       nFans      : 6;  // the number of fanins of this node
-    unsigned char  pFans[0];        // the fanin literals
+    unsigned short pFans[0];        // the fanin literals
 };
 
 // DSD network
 typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
 struct Kit_DsdNtk_t_
 {
-    unsigned char  nVars;           // at most 16 (perhaps 18?)
-    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
-    unsigned char  nNodes;          // the number of nodes
-    unsigned char  Root;            // the root of the tree
+    unsigned short nVars;           // at most 16 (perhaps 18?)
+    unsigned short nNodesAlloc;     // the number of allocated nodes (at most nVars)
+    unsigned short nNodes;          // the number of nodes
+    unsigned short Root;            // the root of the tree
     unsigned *     pMem;            // memory for the truth tables (memory manager?)
     unsigned *     pSupps;          // supports of the nodes
     Kit_DsdObj_t** pNodes;          // the nodes
@@ -142,7 +142,7 @@ struct Kit_DsdMan_t_
     Vec_Int_t *    vNodes;          // temporary array for BDD nodes
 };
  
-static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
+static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 1) + ((nFans & 1) > 0);                    }
 static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
 static inline int             Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
 static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )      { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
@@ -538,6 +538,7 @@ extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
 extern Kit_DsdObj_t *  Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
+extern int             Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c
index 3df16d8c..d026afbc 100644
--- a/src/bool/kit/kitDsd.c
+++ b/src/bool/kit/kitDsd.c
@@ -1485,7 +1485,7 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, unsigned piLitsRes[] )
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] )
 {
     int nSuppSizes[16], Priority[16], pOrder[16];
     int i, k, iVarBest, SuppMax, PrioMax;
@@ -1827,6 +1827,90 @@ int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned iLit, i, RetValue;
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    if ( pObj == NULL )
+        return 0;
+    if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR )
+        return 0;
+    if ( pObj->nFans < 2 ) // why this happens? - need to figure out
+        return 0; 
+    assert( pObj->nFans > 1 );
+    if ( pObj->Type == KIT_DSD_AND )
+        RetValue = ((int)pObj->nFans - 1);
+    else if ( pObj->Type == KIT_DSD_XOR )
+        RetValue = ((int)pObj->nFans - 1) * 3;
+    else if ( pObj->Type == KIT_DSD_PRIME )
+    {
+        // assuming MUX decomposition
+        assert( (int)pObj->nFans == 3 );
+        RetValue = 3;
+    }
+    else assert( 0 );
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
+{
+    return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    int i, Counter = 0;
+    for ( i = 0; i < pNtk->nNodes; i++ )
+    {
+        pObj = pNtk->pNodes[i];
+        if ( pObj->Type == KIT_DSD_AND )
+            Counter += ((int)pObj->nFans - 1);
+        else if ( pObj->Type == KIT_DSD_XOR )
+            Counter += ((int)pObj->nFans - 1) * 3;
+        else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
+            Counter += 3;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
 
   Description []
@@ -1883,7 +1967,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux )
 {
     Kit_DsdObj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);