Version abc70831

2 files changed, 81 insertions, 8 deletions

diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2f7bbef4..c08bead2 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -143,6 +143,7 @@ static inline int             Kit_DsdLitRegular( int Lit )           { return Li
  
 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 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]; }
 static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )             { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );                      }
 static inline int             Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit )   { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
@@ -429,6 +430,25 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
 }
+static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
+{
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
+    if ( iVar < 5 )
+    {
+        for ( k = 0; k < nWords; k++ )
+            pTruth[k] = Masks[iVar];
+    }
+    else
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( k & (1 << (iVar-5)) )
+                pTruth[k] = ~(unsigned)0;
+            else
+                pTruth[k] = 0;
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                           ITERATORS                              ///
@@ -453,12 +473,13 @@ 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, int fMSBonTop );
 /*=== kitDsd.c ==========================================================*/
-extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars );
+extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars, int nNodes );
 extern void            Kit_DsdManFree( Kit_DsdMan_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
 extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
 extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
 extern void            Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
+extern void            Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
 extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 06377cba..354ab6ef 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
+Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
 {
     Kit_DsdMan_t * p;
     p = ALLOC( Kit_DsdMan_t, 1 );
@@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
     p->nVars = nVars;
     p->nWords = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords );
+    p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
     return p;
 }
 
@@ -472,11 +472,40 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
   SeeAlso     []
 
 ***********************************************************************/
+void Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar )
+{
+    unsigned * pTruthRes;
+    int i;
+    // if support is specified, request that supports are available
+    if ( uSupp )
+        Kit_DsdGetSupports( pNtk );
+    // assign elementary truth tables
+    assert( pNtk->nVars <= p->nVars );
+    for ( i = 0; i < (int)pNtk->nVars; i++ )
+        Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+    // compute truth table for each node
+    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
+    // complement the truth table if needed
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
 {
     Kit_DsdMan_t * p;
     unsigned * pTruth;
-    p = Kit_DsdManAlloc( pNtk->nVars );
+    p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
     Kit_DsdManFree( p );
@@ -501,6 +530,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
+{
+    unsigned * pTruth;
+    Kit_DsdObj_t * pRoot;
+    Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar );
+    pRoot = Kit_DsdNtkRoot( pNtk );
+    pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+0 );
+    Kit_TruthCopy( pTruthCo, pTruth, p->nVars );
+    pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+1 );
+    Kit_TruthCopy( pTruthDec, pTruth, p->nVars );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of blocks of the given number of inputs.]
 
   Description []
@@ -1620,7 +1672,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
 //    printf( "Eval = %d.\n", Result );
 
     // recompute the truth table
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
@@ -1645,7 +1697,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
 {
     Kit_DsdMan_t * p;
     unsigned * pTruthC;
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
@@ -1687,7 +1739,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 //        Kit_DsdTestCofs( pNtk, pTruth );
 
     // recompute the truth table
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
 //    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
 //    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
@@ -1757,7 +1809,7 @@ void Kit_DsdPrecompute4Vars()
             printf( "\n" );
 */
 
-        p = Kit_DsdManAlloc( 4 );
+        p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
         pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
         if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
             printf( "Verification failed.\n" );