Version abc70407

1 files changed, 72 insertions, 69 deletions

diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 3540fa03..62ee653b 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -24,74 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
-typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
-typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
-
-// DSD node types
-typedef enum { 
-    KIT_DSD_NONE  = 0,  // 0: unknown
-    KIT_DSD_CONST1,     // 1: constant 1
-    KIT_DSD_VAR,        // 2: elementary variable
-    KIT_DSD_AND,        // 3: multi-input AND
-    KIT_DSD_XOR,        // 4: multi-input XOR
-    KIT_DSD_PRIME       // 5: arbitrary function of 3+ variables
-} Kit_Dsd_t;
-
-// DSD manager
-struct Kit_DsdMan_t_
-{
-    int            nVars;           // the maximum number of variables
-    int            nWords;          // the number of words in TTs
-    Vec_Ptr_t *    vTtElems;        // elementary truth tables
-    Vec_Ptr_t *    vTtNodes;        // the node truth tables
-};
-
-// DSD network
-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 *     pMem;            // memory for the truth tables (memory manager?)
-    Kit_DsdObj_t * pNodes[0];       // the nodes
-};
-
-// DSD node
-struct Kit_DsdObj_t_
-{ 
-    unsigned       Id         : 6;  // the number of this node
-    unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
-    unsigned       fMark      : 1;  // finished checking output
-    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
-};
-
-static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
-static inline int             Kit_DsdLit2Var( int Lit )              { return Lit >> 1;           }
-static inline int             Kit_DsdLitIsCompl( int Lit )           { return Lit & 1;            }
-static inline int             Kit_DsdLitNot( int Lit )               { return Lit ^ 1;            }
-static inline int             Kit_DsdLitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
-static inline int             Kit_DsdLitRegular( int Lit )           { return Lit & 0xfe;         }
- 
-static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
-static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
-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]; }
-static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )  { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );   }
-
-#define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
-    for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
-#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
-    for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
-
-extern unsigned *     Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
-extern void           Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
-extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
-extern void           Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -483,7 +415,7 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
         return nLutSize - 2;
     }
     assert( pObj->Type == KIT_DSD_PRIME );
-    if ( (int)pObj->nFans > nLutSize )
+    if ( (int)pObj->nFans > nLutSize ) //+ 1 )
     {
         *pCounter = 1000;
         return 0;
@@ -491,6 +423,8 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
     Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter );
     (*pCounter)++;
+//    if ( (int)pObj->nFans == nLutSize + 1 )
+//        (*pCounter)++;
     return nLutSize - pObj->nFans;
 }
 
@@ -518,6 +452,31 @@ int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of blocks of the given number of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned i, nSizeMax = 0;
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        if ( nSizeMax < pObj->nFans )
+            nSizeMax = pObj->nFans;
+    }
+    return nSizeMax;
+}
+
 
 /**Function*************************************************************
 
@@ -1208,6 +1167,50 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
   SeeAlso     []
 
 ***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize )
+{
+//    Kit_DsdMan_t * p;
+    Kit_DsdNtk_t * pNtk;//, * pTemp;
+//    unsigned * pTruthC;
+//    int Result;
+
+    // decompose the function
+    pNtk = Kit_DsdDecompose( pTruth, nVars );
+
+//    pNtk = Kit_DsdExpand( pTemp = pNtk );
+//    Kit_DsdNtkFree( pTemp );
+
+//    Result = Kit_DsdCountLuts( pNtk, nLutSize );
+
+//    printf( "\n" );
+//    Kit_DsdPrint( stdout, pNtk );
+//    printf( "Eval = %d.\n", Result );
+
+/*
+    // recompute the truth table
+    p = Kit_DsdManAlloc( nVars );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+    if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
+        printf( "Verification failed.\n" );
+    Kit_DsdManFree( p );
+*/
+
+//    Kit_DsdNtkFree( pNtk );
+//    return Result;
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_DsdTest( unsigned * pTruth, int nVars )
 {
     Kit_DsdMan_t * p;