Added new procedure and other small changes.

3 files changed, 138 insertions, 4 deletions

diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index f1075c2f..20da1b35 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -539,6 +539,7 @@ extern void            Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t *
 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 );
+extern void            Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index f16d94d9..c8665c2f 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -199,6 +199,32 @@ void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the hex unsigned into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_DsdWriteHex( char * pBuff, unsigned * pTruth, int nFans )
+{
+    int nDigits, Digit, k;
+    nDigits = (1 << nFans) / 4;
+    for ( k = nDigits - 1; k >= 0; k-- )
+    {
+        Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
+        if ( Digit < 10 )
+            *pBuff++ = '0' + Digit;
+        else
+            *pBuff++ = 'A' + Digit-10;
+    }
+    return pBuff;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Recursively print the DSD formula.]
 
   Description []
@@ -276,6 +302,83 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Recursively print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_DsdWrite_rec( char * pBuff, Kit_DsdNtk_t * pNtk, int Id )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned iLit, i;
+    char Symbol;
+
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    if ( pObj == NULL )
+    {
+        assert( Id < pNtk->nVars );
+        *pBuff++ = 'a' + Id;
+        return pBuff;
+    }
+
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        assert( pObj->nFans == 0 );
+        sprintf( pBuff, "%s", "Const1" );
+        return pBuff + strlen("Const1");
+    }
+
+    if ( pObj->Type == KIT_DSD_VAR )
+        assert( pObj->nFans == 1 );
+
+    if ( pObj->Type == KIT_DSD_AND )
+        Symbol = '*';
+    else if ( pObj->Type == KIT_DSD_XOR )
+        Symbol = '+';
+    else 
+        Symbol = ',';
+
+    if ( pObj->Type == KIT_DSD_PRIME )
+        pBuff = Kit_DsdWriteHex( pBuff, Kit_DsdObjTruth(pObj), pObj->nFans );
+
+    *pBuff++ = '(';
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+    {
+        if ( Kit_DsdLitIsCompl(iLit) ) 
+            *pBuff++ = '!';
+        pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Kit_DsdLit2Var(iLit) );
+        if ( i < pObj->nFans - 1 )
+            *pBuff++ = Symbol;
+    }
+    *pBuff++ = ')';
+    return pBuff;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdWrite( char * pBuff, Kit_DsdNtk_t * pNtk )
+{
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        *pBuff++ = '!';
+    pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Kit_DsdLit2Var(pNtk->Root) );
+    *pBuff = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Print the DSD formula.]
 
   Description []
@@ -319,6 +422,30 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pTemp, * pTemp2;
+//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
+    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
+//    Kit_DsdPrintExpanded( pTemp );
+    pTemp2 = Kit_DsdExpand( pTemp );
+    Kit_DsdWrite( pBuffer, pTemp2 );
+    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
+    Kit_DsdNtkFree( pTemp2 );
+    Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the truth table of the DSD node.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 26b21ac3..c525cda1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8669,7 +8669,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_NtkDarTest( pNtk );
 
 //    Bbl_ManTest( pNtk );
-
+/*
     {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     extern void Aig_ManComputeDomsForCofactoring( Aig_Man_t * p );
@@ -8678,12 +8678,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_ManComputeDomsForCofactoring( pAig );
     Aig_ManStop( pAig );
     }
-
+*/
 
 /*
 {
-    extern Abc_Ntk_t * Au_ManDeriveFromAig( Abc_Ntk_t * pAig );
-    pNtkRes = Au_ManDeriveFromAig( pNtk );
+    extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
+    pNtkRes = Au_ManTransformTest( pNtk );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8693,6 +8693,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 }
 */
+/*
+{
+    extern void Au_DsdVecTest( int nVars );
+    Au_DsdVecTest( 6 );
+}
+*/
 
 //    Abc_NtkCheckAbsorb( pNtk, 4 );
 /*