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.

Makefile

@@ -20,7 +20,7 @@ MODULES := \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
 	src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
 	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
-	src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
+	src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
 	src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \

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

src/base/pla/module.make

 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/pla.h

@@ -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                                ///
 ////////////////////////////////////////////////////////////////////////
-

src/base/pla/plaCom.c

@@ -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
-

src/opt/fxch/Fxch.c

+/**CFile****************************************************************
+
+  FileName    [ Fxch.c ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ The entrance into the fast extract module. ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+
+#include "Fxch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [ Performs fast extract with cube hashing on a set
+                of covers. ]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_FastExtract( Vec_Wec_t* vCubes,
+                      int ObjIdMax,
+                      int nMaxDivExt,
+                      int SMode, 
+                      int fVerbose,
+                      int fVeryVerbose )
+{
+    abctime TempTime;
+    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, SMode );
+
+    TempTime = Abc_Clock();
+    Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax );
+    Fxch_ManGenerateLitHashKeys( pFxchMan );
+    Fxch_ManComputeLevel( pFxchMan );
+    Fxch_ManSCHashTablesInit( pFxchMan );
+    Fxch_ManDivCreate( pFxchMan );
+    pFxchMan->timeInit = Abc_Clock() - TempTime;
+
+    if ( fVeryVerbose )
+        Fxch_ManPrintDivs( pFxchMan );
+
+    if ( fVerbose )
+        Fxch_ManPrintStats( pFxchMan );
+
+    TempTime = Abc_Clock();
+    for ( int i = 0; i < nMaxDivExt && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
+    {
+        int iDiv = Vec_QuePop( pFxchMan->vDivPrio );
+
+        if ( fVeryVerbose )
+            Fxch_DivPrint( pFxchMan, iDiv );
+
+        Fxch_ManUpdate( pFxchMan, iDiv );
+    }
+    pFxchMan->timeExt = Abc_Clock() - TempTime;
+
+    if ( fVerbose )
+    {
+        Fxch_ManPrintStats( pFxchMan );
+        Abc_PrintTime( 1, "\n[FXCH] Elapsed Time", pFxchMan->timeInit + pFxchMan->timeExt );
+        Abc_PrintTime( 1, "[FXCH]    +-> Init", pFxchMan->timeInit );
+        Abc_PrintTime( 1, "[FXCH]    +-> Extr", pFxchMan->timeExt );
+    }
+
+    Fxch_ManSCHashTablesFree( pFxchMan );
+    Fxch_ManFree( pFxchMan );
+    Vec_WecRemoveEmpty( vCubes );
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Retrives the necessary information for the fast extract
+                with cube hashing. ]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk,
+                        int nMaxDivExt,
+                        int SMode,
+                        int fVerbose,
+                        int fVeryVerbose )
+{
+    Vec_Wec_t* vCubes;
+
+    assert( Abc_NtkIsSopLogic( pNtk ) );
+
+    if ( !Abc_NtkFxCheck( pNtk ) )
+    {
+        printf( "Abc_NtkFxchPerform(): Nodes have duplicated fanins. FXCH is not performed.\n" );
+        return 0;
+    }
+
+    vCubes = Abc_NtkFxRetrieve( pNtk );
+    if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, SMode, fVerbose, fVeryVerbose ) > 0 )
+    {
+        Abc_NtkFxInsert( pNtk, vCubes );
+        Vec_WecFree( vCubes );
+
+        if ( !Abc_NtkCheck( pNtk ) )
+            printf( "Abc_NtkFxchPerform(): The network check has failed.\n" );
+
+        return 1;
+    }
+    else
+        printf( "Warning: The network has not been changed by \"fxch\".\n" );
+
+    Vec_WecFree( vCubes );
+
+    return 0;
+}
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END

src/opt/fxch/Fxch.h

+/**CFile****************************************************************
+
+  FileName    [ Fxch.h ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ External declarations of fast extract with cube hashing. ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+
+#ifndef ABC__opt__fxch__fxch_h
+#define ABC__opt__fxch__fxch_h
+
+#include "base/abc/abc.h"
+
+#include "misc/vec/vecHsh.h"
+#include "misc/vec/vecQue.h"
+#include "misc/vec/vecVec.h"
+#include "misc/vec/vecWec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    TYPEDEF DECLARATIONS                          ///
+////////////////////////////////////////////////////////////////////////
+typedef struct Fxch_Man_t_               Fxch_Man_t;
+typedef struct Fxch_SubCube_t_           Fxch_SubCube_t;
+typedef struct Fxch_SCHashTable_t_       Fxch_SCHashTable_t;
+typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t;
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURES DEFINITIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/* Sub-Cube Structure
+ *
+ *   In the context of this program, a sub-cube is a cube derived from 
+ *   another cube by removing one or two literals. Since a cube is represented
+ *   as a vector of literals, one might think that a sub-cube would also be 
+ *   represented in the same way. However, in order to same memory, we only 
+ *   store a sub-cube identifier and the data necessary to generate the sub-cube:
+ *        - The index number of the orignal cube in the cover. (iCube)
+ *        - Identifiers of which literal(s) was(were) removed. (iLit0, iLit1)
+ *
+ *   The sub-cube identifier is generated by adding the unique identifiers of 
+ *   its literals. 
+ *
+ */
+struct Fxch_SubCube_t_
+{
+    unsigned int Id,          
+                 iCube;      
+    unsigned int iLit0 : 16,
+                 iLit1 : 16;
+};
+
+/* Sub-cube Hash Table
+ *
+ */
+struct Fxch_SCHashTable_Entry_t_
+{
+    Fxch_SubCube_t SCData;
+
+    unsigned int iTable : 31,
+                 Used   :  1;
+    unsigned int iPrev,
+                 iNext;
+};
+
+struct Fxch_SCHashTable_t_
+{
+    Fxch_Man_t* pFxchMan;
+    /* Internal data */
+    Fxch_SCHashTable_Entry_t* pBins;
+    unsigned int nEntries,
+                 SizeMask;
+    Vec_Int_t*   vCubeLinks;
+
+    /* Temporary data */
+    Vec_Int_t    vSubCube0;
+    Vec_Int_t    vSubCube1;
+};
+
+struct Fxch_Man_t_
+{
+    /* user's data */
+    Vec_Wec_t* vCubes;
+    int LitCountMax;
+
+    /* internal data */
+    Fxch_SCHashTable_t* pSCHashTable;
+
+    Vec_Wec_t*    vLits;        /* lit -> cube */
+    Vec_Int_t*    vLitCount;    /* literal counts (currently not used) */
+    Vec_Int_t*    vLitHashKeys; /* Literal hash keys used to generate subcube hash */
+
+    Hsh_VecMan_t* pDivHash;
+    Vec_Flt_t*    vDivWeights;   /* divisor weights */
+    Vec_Que_t*    vDivPrio;      /* priority queue for divisors by weight */
+    Vec_Wec_t*    vDivCubePairs; /* cube pairs for each div */
+
+    Vec_Int_t*    vLevels;       /* variable levels */
+
+    // temporary data to update the data-structure when a divisor is extracted
+    Vec_Int_t*     vCubesS;     /* cubes for the given single cube divisor */
+    Vec_Int_t*     vPairs;     /* cube pairs for the given double cube divisor */
+    Vec_Int_t*     vCubeFree;  // cube-free divisor
+    Vec_Int_t*     vDiv;       // selected divisor
+
+    /* Config */
+    char    SMode;        /* Saving Memory mode */
+
+    /* Statistics */
+    abctime timeInit;   /* Initialization time */
+    abctime timeExt;    /* Extraction time */
+    int     nVars;      // original problem variables
+    int     nLits;      // the number of SOP literals
+    int     nPairsS;    // number of lit pairs
+    int     nPairsD;    // number of cube pairs
+    int     nExtDivs;   /* Number of extracted divisor */
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+/* The following functions are from abcFx.c
+ * They are use in order to retrive SOP information for fast_extract
+ * Since I want an implementation that change only the core part of
+ * the algorithm I'm using this */
+extern Vec_Wec_t* Abc_NtkFxRetrieve( Abc_Ntk_t* pNtk );
+extern void       Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes );
+extern int        Abc_NtkFxCheck( Abc_Ntk_t* pNtk );
+
+/*===== Fxch.c =======================================================*/
+int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
+int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
+
+/*===== FxchDiv.c ====================================================================================================*/
+int  Fxch_DivCreate( Fxch_Man_t* pFxchMan,  Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 );
+int  Fxch_DivAdd( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
+int  Fxch_DivRemove( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
+void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube1 );
+int  Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl );
+void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv );
+
+/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ 
+void Fxch_DivFindPivots( Vec_Int_t* vDiv, int* pLit0, int* pLit1 );
+int  Fxch_DivFind( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vCubeFree );
+void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubes_Lit0, Vec_Int_t* vCubes_Lit1 );
+
+/*===== FxchMan.c ====================================================================================================*/
+Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, char SMode );
+void  Fxch_ManFree( Fxch_Man_t* pFxchMan );
+void  Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars );
+void  Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan );
+void  Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan );
+void  Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan );
+void  Fxch_ManDivCreate( Fxch_Man_t* pFxchMan );
+int   Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeFree );
+int   Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan, Vec_Int_t* vCube );
+void  Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan );
+void  Fxch_ManUpdate( Fxch_Man_t* pFxchMan, int iDiv );
+void  Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan );
+void  Fxch_ManPrintStats( Fxch_Man_t* pFxchMan );
+
+static inline Vec_Int_t* Fxch_ManGetCube( Fxch_Man_t* pFxchMan,
+                                          int iCube )
+{
+    return Vec_WecEntry( pFxchMan->vCubes, iCube );
+}
+
+static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan,
+                                  int iCube,
+                                  int iLit )
+{
+    return Vec_IntEntry( Vec_WecEntry(pFxchMan->vCubes, iCube), iLit );
+}
+
+/*===== FxchSCHashTable.c ============================================*/
+Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeLinks, int nEntries );
+
+void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* );
+
+int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
+                            Vec_Wec_t* vCubes,
+                            unsigned int SubCubeID, 
+                            unsigned int iSubCube,
+                            unsigned int iCube, 
+                            unsigned int iLit0, 
+                            unsigned int iLit1,
+                            char fUpdate );
+
+int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
+                            Vec_Wec_t* vCubes,
+                            unsigned int SubCubeID, 
+                            unsigned int iSubCube,
+                            unsigned int iCube, 
+                            unsigned int iLit0, 
+                            unsigned int iLit1,
+                            char fUpdate );
+
+unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* );
+void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/fxch/module.make

+SRC +=  src/opt/fxch/Fxch.c \
+    src/opt/fxch/FxchDiv.c \
+    src/opt/fxch/FxchMan.c  \
+    src/opt/fxch/FxchSCHashTable.c \