Exploration of functions.

2 files changed, 208 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 35467415..96fbd101 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10320,8 +10320,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int nCutMax      =  1;
     int nLeafMax     = 10;
-    int nDivMax      = 50;
-    int nDecMax      = 20;
+    int nDivMax      =  2;
+    int nDecMax      =  3;
     int fNewAlgo     =  0;
     int fNewOrder    =  0;
     int fVerbose     =  0;
@@ -10461,8 +10461,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
     {
-        extern void Abc_EnumerateFunctions( int nVars );
-        Abc_EnumerateFunctions( nDecMax );
+        extern void Abc_EnumerateFuncs( int nDecMax, int nDivMax, int fVerbose );
+        Abc_EnumerateFuncs( nDecMax, nDivMax, fVerbose );
     }
     if ( pNtk )
     {
diff --git a/src/misc/extra/extraUtilEnum.c b/src/misc/extra/extraUtilEnum.c
index f4ce65cd..432cb4d1 100644
--- a/src/misc/extra/extraUtilEnum.c
+++ b/src/misc/extra/extraUtilEnum.c
@@ -24,6 +24,7 @@
 #include <assert.h>
 #include "misc/vec/vec.h"
 #include "misc/vec/vecHsh.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -414,6 +415,209 @@ void Abc_EnumerateFunctions( int nDecMax )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#define ABC_ENUM_MAX 32
+static word s_Truths6[6] = {
+    ABC_CONST(0xAAAAAAAAAAAAAAAA),
+    ABC_CONST(0xCCCCCCCCCCCCCCCC),
+    ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    ABC_CONST(0xFF00FF00FF00FF00),
+    ABC_CONST(0xFFFF0000FFFF0000),
+    ABC_CONST(0xFFFFFFFF00000000)
+};
+typedef struct Abc_EnuMan_t_ Abc_EnuMan_t;
+struct Abc_EnuMan_t_
+{
+    int              nVars;        // support size
+    int              nVarsFree;    // number of PIs used
+    int              fVerbose;     // verbose flag
+    int              nNodeMax;     // the max number of nodes
+    int              nNodes;       // current number of gates
+    int              nTops;        // the number of fanoutless gates
+    int              pFans0[ABC_ENUM_MAX];   // fanins
+    int              pFans1[ABC_ENUM_MAX];   // fanins 
+    int              fCompl0[ABC_ENUM_MAX];  // complements
+    int              fCompl1[ABC_ENUM_MAX];  // complements
+    int              pRefs[ABC_ENUM_MAX];    // references
+    word             pTruths[ABC_ENUM_MAX];  // truth tables
+    word             nTries;       // attempts to build a gate
+    word             nBuilds;      // actually built gates
+    word             nFinished;    // finished structures
+};
+static inline void Abc_EnumRef( Abc_EnuMan_t * p, int i )
+{
+    assert( p->pRefs[i] >= 0 );
+    if ( p->pRefs[i]++ == 0 )
+        p->nTops--;
+}
+static inline void Abc_EnumDeref( Abc_EnuMan_t * p, int i )
+{
+    if ( --p->pRefs[i] == 0 )
+        p->nTops++;
+    assert( p->pRefs[i] >= 0 );
+}
+static inline void Abc_EnumRefNode( Abc_EnuMan_t * p, int i )
+{
+    Abc_EnumRef( p, p->pFans0[i] );
+    Abc_EnumRef( p, p->pFans1[i] );
+    p->nTops++;
+    p->nNodes++; 
+    assert( i < p->nNodes );
+}
+static inline void Abc_EnumDerefNode( Abc_EnuMan_t * p, int i )
+{
+    assert( i < p->nNodes );
+    Abc_EnumDeref( p, p->pFans0[i] );
+    Abc_EnumDeref( p, p->pFans1[i] );
+    p->nTops--;
+    p->nNodes--; 
+}
+static inline void Abc_EnumPrintOne( Abc_EnuMan_t * p )
+{
+    int i;
+    Kit_DsdPrintFromTruth( (unsigned *)(p->pTruths + p->nNodes - 1), p->nVars ); 
+    for ( i = p->nVars; i < p->nNodes; i++ )
+        printf( "  %c=%s%c%s%c", 'a'+i, p->fCompl0[i]?"!":"", 'a'+p->pFans0[i], p->fCompl1[i]?"!":"", 'a'+p->pFans1[i] );
+    printf( "\n" );
+}
+void Abc_EnumerateFuncs_rec( Abc_EnuMan_t * p )
+{
+    word uTruth, uTemp;
+    word * pTruth = p->pTruths;
+    int f = p->nVarsFree;
+    int n = p->nNodes;
+    int i, k, c0, c1, t, a, b;
+    p->nBuilds++;
+    // terminate when enough and no new tops
+    if ( n == p->nNodeMax && p->nTops == 1 )
+    {
+        if ( p->fVerbose )
+            Abc_EnumPrintOne( p );
+        p->nFinished++;
+        return;
+    }
+    if ( p->nTops > p->nNodeMax - n + 1 )
+        return;
+    assert( n < p->nNodeMax );
+    // try new gates with two inputs
+    if ( f >= 2 )
+    {
+        p->pFans0[n]  = f - 2;
+        p->pFans1[n]  = f - 1;
+        p->fCompl0[n] = 0;
+        p->fCompl1[n] = 0;
+        p->pTruths[n] = pTruth[f - 2] & pTruth[f - 1];
+        p->nVarsFree -= 2;
+        Abc_EnumRefNode( p, n );
+        Abc_EnumerateFuncs_rec( p );
+        Abc_EnumDerefNode( p, n );
+        p->nVarsFree += 2;
+        return;
+    }
+    // try new gates with one input
+    if ( f > 0 )
+    {
+        for ( i = f; i < n; i++ )
+        for ( c0 = 0; c0 < 2; c0++ )
+        {
+            uTruth = pTruth[f - 1] & (c0 ? ~pTruth[i] : pTruth[i]);
+            p->pFans0[n]  = f - 1;
+            p->pFans1[n]  = i;
+            p->fCompl0[n] = 0;
+            p->fCompl1[n] = c0;
+            p->pTruths[n] = uTruth;
+            p->nVarsFree--;
+            Abc_EnumRefNode( p, n );
+            Abc_EnumerateFuncs_rec( p );
+            Abc_EnumDerefNode( p, n );
+            p->nVarsFree++;
+        }
+        return;
+    }
+    // try new gates without inputs
+    for ( i = f; i < n; i++ )
+    for ( k = i+1; k < n; k++ )
+    for ( c0 = 0; c0 < 2; c0++ )
+    for ( c1 = 0; c1 < 2; c1++ )
+    {
+        uTruth = (c0 ? ~pTruth[i] : pTruth[i]) & (c1 ? ~pTruth[k] : pTruth[k]);
+        if ( uTruth == 0 || ~uTruth == 0 )
+            continue;
+        for ( t = f; t < n; t++ )
+            if ( uTruth == p->pTruths[t] || ~uTruth == p->pTruths[t] )
+                break;
+        if ( t < n )
+            continue;
+        for ( a = f; a <= i; a++ )
+        {
+            for ( b = a + 1; b <= k; b++ )
+            {
+                if ( a == i && b == k )
+                    continue;
+                uTemp = p->pTruths[a] & p->pTruths[b];
+                if ( uTruth == uTemp || ~uTruth == uTemp )
+                    break;
+                uTemp = p->pTruths[a] & ~p->pTruths[b];
+                if ( uTruth == uTemp || ~uTruth == uTemp )
+                    break;
+                uTemp = ~p->pTruths[a] & p->pTruths[b];
+                if ( uTruth == uTemp || ~uTruth == uTemp )
+                    break;
+                uTemp = ~p->pTruths[a] & ~p->pTruths[b];
+                if ( uTruth == uTemp || ~uTruth == uTemp )
+                    break;
+            }
+            if ( b <= k )
+                break;
+        }
+        if ( a <= i )
+            continue;
+        p->pFans0[n] = i;
+        p->pFans1[n] = k;
+        p->fCompl0[n] = c0;
+        p->fCompl1[n] = c1;
+        p->pTruths[n] = uTruth;
+        Abc_EnumRefNode( p, n );
+        Abc_EnumerateFuncs_rec( p );
+        Abc_EnumDerefNode( p, n );
+    }
+}
+void Abc_EnumerateFuncs( int nVars, int nGates, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Abc_EnuMan_t P, * p = &P; int i;
+    if ( nVars > nGates + 1 )
+    {
+        printf( "The gate count %d is not enough to have functions with %d inputs.\n", nGates, nVars );
+        return;
+    }
+    assert( nVars >= 3 && nVars <= 6 );
+    assert( nGates > 0 && nVars + nGates < 16 );
+    memset( p, 0, sizeof(Abc_EnuMan_t) );
+    p->fVerbose  = fVerbose;
+    p->nVars     = nVars;
+    p->nVarsFree = nVars;
+    p->nNodeMax  = nVars + nGates;
+    p->nNodes    = nVars;
+    p->nTops     = nVars;
+    for ( i = 0; i < nVars; i++ )
+        p->pTruths[i] = s_Truths6[i];
+    Abc_EnumerateFuncs_rec( p );
+    printf( "Vars = %d.  Gates = %d.  Tries = %u. Builds = %u.  Finished = %d. ", 
+        nVars, nGates, (unsigned)p->nTries, (unsigned)p->nBuilds, (unsigned)p->nFinished );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////