Adding command 'testdec'.

src/base/abci/abc.c

@@ -4811,7 +4811,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_DecTest( char * pFileName, int DecType );
+    extern int Abc_DecTest( char * pFileName, int DecType, int fVerbose );
     char * pFileName;
     int c;
     int fVerbose = 0;
@@ -4849,17 +4849,17 @@ int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the testbench
-    Abc_DecTest( pFileName, DecType );
+    Abc_DecTest( pFileName, DecType, fVerbose );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: testdec [-A <num>] [-vh] <file_name>\n" );
     Abc_Print( -2, "\t           testbench for Boolean decomposition algorithms\n" );
-    Abc_Print( -2, "\t-A <num> : number of decomposition algorithm [default = %d]\n", DecType );
-    Abc_Print( -2, "\t      0  : none (just read the input file)\n" );
-    Abc_Print( -2, "\t      1  : algebraic factoring applied to ISOP\n" );
-    Abc_Print( -2, "\t      2  : bi-decomposition with cofactoring\n" );
-    Abc_Print( -2, "\t      3  : disjoint-support decomposition\n" );
+    Abc_Print( -2, "\t-A <num> : decomposition algorithm [default = %d]\n", DecType );
+    Abc_Print( -2, "\t               0: none (reading and writing the file)\n" );
+    Abc_Print( -2, "\t               1: algebraic factoring applied to ISOP\n" );
+    Abc_Print( -2, "\t               2: bi-decomposition with cofactoring\n" );
+    Abc_Print( -2, "\t               3: disjoint-support decomposition with cofactoring\n" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;

src/bool/bdc/bdc.h

@@ -67,10 +67,12 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )    { return (Bdc_F
 /*=== bdcCore.c ==========================================================*/
 extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
 extern void        Bdc_ManFree( Bdc_Man_t * p );
+extern void        Bdc_ManDecPrint( Bdc_Man_t * p );
 extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
 extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
 extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
 extern int         Bdc_ManNodeNum( Bdc_Man_t * p );
+extern int         Bdc_ManAndNum( Bdc_Man_t * p );
 extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
 extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
 extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );

src/bool/bdc/bdcCore.c

@@ -46,6 +46,7 @@ ABC_NAMESPACE_IMPL_START
 Bdc_Fun_t *  Bdc_ManFunc( Bdc_Man_t * p, int i )               { return Bdc_FunWithId(p, i); }
 Bdc_Fun_t *  Bdc_ManRoot( Bdc_Man_t * p )                      { return p->pRoot;            }
 int          Bdc_ManNodeNum( Bdc_Man_t * p )                   { return p->nNodes;           }
+int          Bdc_ManAndNum( Bdc_Man_t * p )                    { return p->nNodes-p->nVars-1;}
 Bdc_Fun_t *  Bdc_FuncFanin0( Bdc_Fun_t * p )                   { return p->pFan0;            }
 Bdc_Fun_t *  Bdc_FuncFanin1( Bdc_Fun_t * p )                   { return p->pFan1;            }
 void *       Bdc_FuncCopy( Bdc_Fun_t * p )                     { return p->pCopy;            }
@@ -186,7 +187,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
 
 /**Function*************************************************************
 
-  Synopsis    [Clears the manager.]
+  Synopsis    [Prints bi-decomposition in a simple format.]
 
   Description []
                
@@ -195,7 +196,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
   SeeAlso     []
 
 ***********************************************************************/
-void Bdc_ManDecPrint( Bdc_Man_t * p )
+void Bdc_ManDecPrintSimple( Bdc_Man_t * p )
 {
     Bdc_Fun_t * pNode;
     int i;
@@ -211,7 +212,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
             printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
             printf( " %s%d   ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
         }
-        Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
+//        Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
         printf( "\n" );
     }
     printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
@@ -219,6 +220,65 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints bi-decomposition recursively.]
+
+  Description [This procedure prints bi-decomposition as a factored form.
+  In doing so, logic sharing, if present, will be replicated several times.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecPrint_rec( Bdc_Man_t * p, Bdc_Fun_t * pNode )
+{
+    if ( pNode->Type == BDC_TYPE_PI )
+        printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 );
+    else if ( pNode->Type == BDC_TYPE_AND )
+    {
+        Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode );
+        Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode );
+
+        if ( Bdc_IsComplement(pNode0) )
+            printf( "!" );
+        if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+            printf( "(" );
+        Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) );
+        if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+            printf( ")" );
+
+        if ( Bdc_IsComplement(pNode1) )
+            printf( "!" );
+        if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+            printf( "(" );
+        Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) );
+        if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+            printf( ")" );
+    }
+    else assert( 0 );
+}
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+    Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot);
+
+    printf( "F = " );
+    if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0
+        printf( "Constant %d", !Bdc_IsComplement(p->pRoot) );
+    else if ( pRoot->Type == BDC_TYPE_PI ) // literal
+        printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 );
+    else
+    {
+        if ( Bdc_IsComplement(p->pRoot) )
+            printf( "!(" );
+        Bdc_ManDecPrint_rec( p, pRoot );
+        if ( Bdc_IsComplement(p->pRoot) )
+            printf( ")" );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs decomposition of one function.]
 
   Description []

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[] );

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);