Add a new module which implements the fast extract with cube hashing (fxch) algorithm.

Removes old partial implementation of this algorithm from the "pla" module.

4 files changed, 134 insertions, 38 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5abc941b..cc687689 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23,6 +23,7 @@
 #include "base/main/mainInt.h"
 #include "proof/fraig/fraig.h"
 #include "opt/fxu/fxu.h"
+#include "opt/fxch/Fxch.h"
 #include "opt/cut/cut.h"
 #include "map/fpga/fpga.h"
 #include "map/if/if.h"
@@ -106,6 +107,7 @@ static int Abc_CommandRenode                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandCleanup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSweep                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFxch                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEliminate              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSparsify               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -740,6 +742,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "fxch",          Abc_CommandFxch,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "eliminate",     Abc_CommandEliminate,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sparsify",      Abc_CommandSparsify,         1 );
@@ -4130,6 +4133,103 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_NtkFxchPerform( Abc_Ntk_t * pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+
+    int c,
+        nMaxDivExt,
+        SMode = 0,
+        fVerbose = 0,
+        fVeryVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "NSvwh")) != EOF )
+    {
+        switch (c)
+        {
+            case 'N':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                nMaxDivExt = atoi( argv[globalUtilOptind] );
+                globalUtilOptind++;
+
+                if ( nMaxDivExt < 0 )
+                    goto usage;
+                break;
+
+            case 'S':
+                SMode ^= 1;
+                break;
+
+            case 'v':
+                fVerbose ^= 1;
+                break;
+
+            case 'w':
+                fVeryVerbose ^= 1;
+                break;
+
+            case 'h':
+                goto usage;
+                break;
+
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkNodeNum( pNtk ) == 0 )
+    {
+        Abc_Print( -1, "The network does not have internal nodes.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic( pNtk ) )
+    {
+        Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\" or \"if\").\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSopLogic( pNtk ) )
+    {
+        Abc_Print( -1, "Fast extract can only be applied to a logic network with SOP local functions (run \"bdd; sop\").\n" );
+        return 1;
+    }
+
+    Abc_NtkFxchPerform( pNtk, nMaxDivExt, SMode, fVerbose, fVeryVerbose );
+
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: fxch [-N <num>] [-vwh]\n");
+    Abc_Print( -2, "\t           performs fast extract with cube hashing on the current network\n");
+    Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = %d]\n", nMaxDivExt );
+    Abc_Print( -2, "\t-S       : memory saving mode (slower) [default = %d]\n", SMode );
+    Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : print additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/pla/module.make b/src/base/pla/module.make
index b34d30d0..a552b27f 100644
--- a/src/base/pla/module.make
+++ b/src/base/pla/module.make
@@ -1,8 +1,7 @@
 SRC +=    src/base/pla/plaCom.c \
     src/base/pla/plaHash.c \
-    src/base/pla/plaFxch.c \
     src/base/pla/plaMan.c \
     src/base/pla/plaMerge.c \
     src/base/pla/plaSimple.c \
     src/base/pla/plaRead.c \
-    src/base/pla/plaWrite.c 
+    src/base/pla/plaWrite.c
diff --git a/src/base/pla/pla.h b/src/base/pla/pla.h
index 2806df2f..2df1d096 100644
--- a/src/base/pla/pla.h
+++ b/src/base/pla/pla.h
@@ -9,7 +9,7 @@
   Synopsis    [Scalable SOP transformations.]
 
   Author      [Alan Mishchenko]
-  
+
   Affiliation [UC Berkeley]
 
   Date        [Ver. 1.0. Started - March 18, 2015.]
@@ -34,7 +34,7 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-ABC_NAMESPACE_HEADER_START 
+ABC_NAMESPACE_HEADER_START
 
 #define MASK55 ABC_CONST(0x5555555555555555)
 
@@ -43,25 +43,25 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 
 // file types
-typedef enum { 
-    PLA_FILE_FD = 0, 
-    PLA_FILE_F,      
-    PLA_FILE_FR,     
-    PLA_FILE_FDR,      
-    PLA_FILE_NONE     
-} Pla_File_t; 
+typedef enum {
+    PLA_FILE_FD = 0,
+    PLA_FILE_F,
+    PLA_FILE_FR,
+    PLA_FILE_FDR,
+    PLA_FILE_NONE
+} Pla_File_t;
 
 // literal types
-typedef enum { 
-    PLA_LIT_DASH = 0, 
-    PLA_LIT_ZERO,     
-    PLA_LIT_ONE,      
-    PLA_LIT_FULL      
-} Pla_Lit_t; 
+typedef enum {
+    PLA_LIT_DASH = 0,
+    PLA_LIT_ZERO,
+    PLA_LIT_ONE,
+    PLA_LIT_FULL
+} Pla_Lit_t;
 
 
 typedef struct Pla_Man_t_ Pla_Man_t;
-struct Pla_Man_t_ 
+struct Pla_Man_t_
 {
     char *           pName;      // model name
     char *           pSpec;      // input file
@@ -112,17 +112,17 @@ static inline void   Pla_CubeXorLit( word * p, int i, Pla_Lit_t d )  { p[i>>5] ^
 ////////////////////////////////////////////////////////////////////////
 
 #define Pla_ForEachCubeIn( p, pCube, i )                            \
-    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeIn(p, i)), 1); i++ ) 
+    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeIn(p, i)), 1); i++ )
 #define Pla_ForEachCubeInStart( p, pCube, i, Start )                \
-    for ( i = Start; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeIn(p, i)), 1); i++ ) 
+    for ( i = Start; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeIn(p, i)), 1); i++ )
 
 #define Pla_ForEachCubeOut( p, pCube, i )                           \
-    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeOut(p, i)), 1); i++ ) 
+    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCube) = Pla_CubeOut(p, i)), 1); i++ )
 #define Pla_ForEachCubeInOut( p, pCubeIn, pCubeOut, i )             \
-    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCubeIn) = Pla_CubeIn(p, i)), 1)  && (((pCubeOut) = Pla_CubeOut(p, i)), 1); i++ ) 
+    for ( i = 0; (i < Pla_ManCubeNum(p))  && (((pCubeIn) = Pla_CubeIn(p, i)), 1)  && (((pCubeOut) = Pla_CubeOut(p, i)), 1); i++ )
 
 #define Pla_CubeForEachLit( nVars, pCube, Lit, i )                  \
-    for ( i = 0; (i < nVars)  && (((Lit) = Pla_CubeGetLit(pCube, i)), 1); i++ ) 
+    for ( i = 0; (i < nVars)  && (((Lit) = Pla_CubeGetLit(pCube, i)), 1); i++ )
 #define Pla_CubeForEachLitIn( p, pCube, Lit, i )                    \
     Pla_CubeForEachLit( Pla_ManInNum(p), pCube, Lit, i )
 #define Pla_CubeForEachLitOut( p, pCube, Lit, i )                   \
@@ -138,7 +138,7 @@ static inline void   Pla_CubeXorLit( word * p, int i, Pla_Lit_t d )  { p[i>>5] ^
   Synopsis    [Checks if cubes are distance-1.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
@@ -175,7 +175,7 @@ static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * p
         if ( fFound )
             return 0;
         // check if the number of 1s is one, which means exactly one opposite literal (0/1) but may have other diffs (-/0 or -/1)
-        Test = ((p[c] ^ q[c]) & ((p[c] ^ q[c]) >> 1)) & MASK55; 
+        Test = ((p[c] ^ q[c]) & ((p[c] ^ q[c]) >> 1)) & MASK55;
         if ( !Pla_OnlyOneOne(Test) )
             return 0;
         fFound = 1;
@@ -185,12 +185,12 @@ static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * p
 }
 static inline int Pla_TtCountOnesOne( word x )
 {
-    x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));   
-    x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));    
-    x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);    
+    x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
+    x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
+    x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
     x = x + (x >> 8);
     x = x + (x >> 16);
-    x = x + (x >> 32); 
+    x = x + (x >> 32);
     return (int)(x & 0xFF);
 }
 static inline int Pla_TtCountOnes( word * p, int nWords )
@@ -200,13 +200,13 @@ static inline int Pla_TtCountOnes( word * p, int nWords )
         Count += Pla_TtCountOnesOne( p[i] );
     return Count;
 }
-            
+
 /**Function*************************************************************
 
   Synopsis    [Manager APIs.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
@@ -268,8 +268,7 @@ static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose )
 }
 
 
-/*=== plaFxch.c ========================================================*/
-extern int                 Pla_ManPerformFxch( Pla_Man_t * p );
+
 /*=== plaHash.c ========================================================*/
 extern int                 Pla_ManHashDist1NumTest( Pla_Man_t * p );
 extern void                Pla_ManComputeDist1Test( Pla_Man_t * p );
@@ -296,4 +295,3 @@ ABC_NAMESPACE_HEADER_END
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
diff --git a/src/base/pla/plaCom.c b/src/base/pla/plaCom.c
index 77fd921c..9060f371 100644
--- a/src/base/pla/plaCom.c
+++ b/src/base/pla/plaCom.c
@@ -9,7 +9,7 @@
   Synopsis    [Scalable SOP transformations.]
 
   Author      [Alan Mishchenko]
-  
+
   Affiliation [UC Berkeley]
 
   Date        [Ver. 1.0. Started - March 18, 2015.]
@@ -396,7 +396,7 @@ usage:
 
   Description []
 
-  SideEffects []    
+  SideEffects []
 
   SeeAlso     []
 
@@ -488,7 +488,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Pla_ManFxPerformSimple( nVars );
     //Pla_ManConvertFromBits( p );
     //Pla_ManConvertToBits( p );
-    Pla_ManPerformFxch( p );
+    //Pla_ManPerformFxch( p );
     return 0;
 usage:
     Abc_Print( -2, "usage: |test [-N num] [-vh]\n" );
@@ -505,4 +505,3 @@ usage:
 
 
 ABC_NAMESPACE_IMPL_END
-