Added support for generating a library of real-life truth-tables.

5 files changed, 153 insertions, 6 deletions

diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 20da1b35..9e15e994 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_DsdPrintFromTruth2( FILE * pFile, 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 );
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index c8665c2f..413597a1 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -234,6 +234,86 @@ char * Kit_DsdWriteHex( char * pBuff, unsigned * pTruth, int nFans )
   SeeAlso     []
 
 ***********************************************************************/
+void Kit_DsdPrint2_rec( FILE * pFile, 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 );
+        fprintf( pFile, "%c", 'a' + Id );
+        return;
+    }
+
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        assert( pObj->nFans == 0 );
+        fprintf( pFile, "Const1" );
+        return;
+    }
+
+    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 )
+        fprintf( pFile, "[" );
+    else
+        fprintf( pFile, "(" );
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+    {
+        if ( Kit_DsdLitIsCompl(iLit) ) 
+            fprintf( pFile, "!" );
+        Kit_DsdPrint2_rec( pFile, pNtk, Kit_DsdLit2Var(iLit) );
+        if ( i < pObj->nFans - 1 )
+            fprintf( pFile, "%c", Symbol );
+    }
+    if ( pObj->Type == KIT_DSD_PRIME )
+        fprintf( pFile, "]" );
+    else
+        fprintf( pFile, ")" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrint2( FILE * pFile, Kit_DsdNtk_t * pNtk )
+{
+//    fprintf( pFile, "F = " );
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        fprintf( pFile, "!" );
+    Kit_DsdPrint2_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) );
+//    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_DsdPrint_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
 {
     Kit_DsdObj_t * pObj;
@@ -431,6 +511,28 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
+void Kit_DsdPrintFromTruth2( FILE * pFile, unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pTemp, * pTemp2;
+    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 0 );
+    pTemp2 = Kit_DsdExpand( pTemp );
+    Kit_DsdPrint2( pFile, pTemp2 );
+    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
+    Kit_DsdNtkFree( pTemp2 );
+    Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars )
 {
     Kit_DsdNtk_t * pTemp, * pTemp2;
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index bf83dbb4..a9255ce6 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -200,12 +200,16 @@ void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts )
     p->vTtElems->nSize = p->nVars;
     p->vTtElems->nCap = p->nVars;
     p->vTtElems->pArray = (void **)Extra_TruthElementary( p->nVars );        
-
+/*
     // allocate room for node truth tables
     if ( Abc_NtkObjNum(pNtk) > (1<<14) )
         p->vTtNodes = Vec_PtrAllocSimInfo( 2 * Abc_NtkObjNum(pNtk), p->nWords );
     else
         p->vTtNodes = Vec_PtrAllocSimInfo( 1<<14, p->nWords );
+*/
+    p->vTtNodes = Vec_PtrAlloc( 1000 );
+    for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
+        Vec_PtrPush( p->vTtNodes, ABC_ALLOC(unsigned, p->nWords) );
 
     // create hash table
     p->nBins = 50011;
@@ -269,6 +273,38 @@ p->timeTotal += clock() - clkTotal;
 
 /**Function*************************************************************
 
+  Synopsis    [Dump truth tables into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecDumpTruthTables( Abc_ManRec_t * p )
+{
+    FILE * pFile;
+    Abc_Obj_t * pObj;
+    unsigned * pTruth;
+    int i;
+    pFile = fopen( "tt16.txt", "wb" );
+    for ( i = 0; i < p->nBins; i++ )
+        for ( pObj = p->pBins[i]; pObj; pObj = pObj->pCopy )
+        {
+            pTruth = Vec_PtrEntry(p->vTtNodes, pObj->Id);
+            if ( Kit_TruthSupport(pTruth, 16) != (1<<16)-1 )
+                continue;
+            Extra_PrintHex( pFile, pTruth, 16 );
+            fprintf( pFile, " " );
+            Kit_DsdPrintFromTruth2( pFile, pTruth, 16 );
+            fprintf( pFile, "\n" );
+        }
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the given record.]
 
   Description []
@@ -281,9 +317,12 @@ p->timeTotal += clock() - clkTotal;
 void Abc_NtkRecStop()
 {
     assert( s_pMan != NULL );
+    Abc_NtkRecDumpTruthTables( s_pMan );
+
     if ( s_pMan->pNtk )
         Abc_NtkDelete( s_pMan->pNtk );
-    Vec_PtrFree( s_pMan->vTtNodes );
+//    Vec_PtrFree( s_pMan->vTtNodes );
+    Vec_PtrFreeFree( s_pMan->vTtNodes );
     Vec_PtrFree( s_pMan->vTtElems );
     ABC_FREE( s_pMan->pBins );
 
@@ -878,8 +917,11 @@ s_pMan->timeCanon += clock() - clk;
         if ( pObj->Id == nNodes )
         {
             // increase storage for truth tables
-            if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
-                Vec_PtrDoubleSimInfo(s_pMan->vTtNodes);
+//            if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
+//                Vec_PtrDoubleSimInfo(s_pMan->vTtNodes);
+            while ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
+                Vec_PtrPush( s_pMan->vTtNodes, ABC_ALLOC(unsigned, s_pMan->nWords) );
+
             // compute the truth table
             RetValue = Abc_NtkRecComputeTruth( pObj, s_pMan->vTtNodes, nInputs );
             if ( RetValue == 0 )
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 3d1a6ae3..37e7d34f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -929,6 +929,8 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
         goto usage;
     }
 
+    c = strlen(argv[globalUtilOptind]);
+
     // convert truth table to SOP
     if ( fHex )
         pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]);
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index dadcbdd1..c849a53d 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -70,7 +70,7 @@ char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc )
 ***********************************************************************/
 char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc )
 {
-    static char Prompt[1000];
+    static char Prompt[5000];
 #ifndef _WIN32
     static char * line = NULL;
 #endif
@@ -78,7 +78,7 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc )
     sprintf( Prompt, "abc %02d> ", pAbc->nSteps );
 #ifdef _WIN32
     fprintf( pAbc->Out, "%s", Prompt );
-    fgets( Prompt, 999, stdin );
+    fgets( Prompt, 5000, stdin );
     return Prompt;
 #else
     if (line != NULL) ABC_FREE(line);