Towards better Boolean matching.

src/base/abci/abc.c

@@ -5288,6 +5288,7 @@ usage:
     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               4: updated disjoint-support decomposition with cofactoring\n" );
+    Abc_Print( -2, "\t               5: enumerating decomposable variable sets\n" );
     Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\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");

src/base/abci/abcDec.c

@@ -481,6 +481,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
         pAlgoName = "DSD";
     else if ( DecType == 4 )
         pAlgoName = "fast DSD";
+    else if ( DecType == 5 )
+        pAlgoName = "analysis";
 
     if ( pAlgoName )
         printf( "Applying %-10s to %8d func%s of %2d vars...  ",  
@@ -558,6 +560,17 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
             nNodes += Dau_DsdCountAnds( pDsd );
         }
     }
+    else if ( DecType == 5 )
+    {
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            extern void Dau_DecTrySets( word * pInit, int nVars );
+            if ( fVerbose )
+                printf( "%7d :      ", i );
+            Dau_DecTrySets( p->pFuncs[i], p->nVars );
+            printf( "\n" );
+        }
+    }
     else assert( 0 );
 
     printf( "AIG nodes =%9d  ", nNodes );
@@ -608,7 +621,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose )
         printf( "Using truth tables from file \"%s\"...\n", pFileName );
     if ( DecType == 0 )
         { if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); }
-    else if ( DecType >= 1 && DecType <= 4 )
+    else if ( DecType >= 1 && DecType <= 5 )
         Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose );
     else
         printf( "Unknown decomposition type value (%d).\n", DecType );