summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--src/base/abci/abc.c100
-rw-r--r--src/base/pla/module.make3
-rw-r--r--src/base/pla/pla.h62
-rw-r--r--src/base/pla/plaCom.c7
-rw-r--r--src/opt/fxch/Fxch.c140
-rw-r--r--src/opt/fxch/Fxch.h218
-rw-r--r--src/opt/fxch/FxchDiv.c582
-rw-r--r--src/opt/fxch/FxchMan.c600
-rw-r--r--src/opt/fxch/FxchSCHashTable.c401
-rw-r--r--src/opt/fxch/module.make4
11 files changed, 2080 insertions, 39 deletions
diff --git a/Makefile b/Makefile
index 0a1fcb32..568ab2d7 100644
--- a/Makefile
+++ b/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 \
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
-
diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c
new file mode 100644
index 00000000..9d674720
--- /dev/null
+++ b/src/opt/fxch/Fxch.c
@@ -0,0 +1,140 @@
+/**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
diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h
new file mode 100644
index 00000000..be229b98
--- /dev/null
+++ b/src/opt/fxch/Fxch.h
@@ -0,0 +1,218 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c
new file mode 100644
index 00000000..072198ef
--- /dev/null
+++ b/src/opt/fxch/FxchDiv.c
@@ -0,0 +1,582 @@
+/**CFile****************************************************************************************************************
+
+ FileName [ FxchDiv.c ]
+
+ PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+ Synopsis [ Divisor handling functions ]
+
+ 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
+////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree )
+{
+ int * L = Vec_IntArray(vCubeFree);
+ int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1;
+ assert( Vec_IntSize(vCubeFree) == 4 );
+ if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars
+ {
+ if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) )
+ return -1;
+ LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]);
+ if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) )
+ {
+ assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) );
+ LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]);
+ }
+ else
+ {
+ assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) );
+ assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) );
+ LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]);
+ }
+ }
+ else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) )
+ {
+ if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) )
+ return -1;
+ LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]);
+ if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) )
+ LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]);
+ else
+ LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]);
+ }
+ else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) )
+ {
+ if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) )
+ return -1;
+ LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]);
+ if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) )
+ LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]);
+ else
+ LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]);
+ }
+ else
+ return -1;
+ assert( LitA0 == Abc_LitNot(LitB0) );
+ if ( Abc_LitIsCompl(LitA0) )
+ {
+ ABC_SWAP( int, LitA0, LitB0 );
+ ABC_SWAP( int, LitA1, LitB1 );
+ }
+ assert( !Abc_LitIsCompl(LitA0) );
+ if ( Abc_LitIsCompl(LitA1) )
+ {
+ LitA1 = Abc_LitNot(LitA1);
+ LitB1 = Abc_LitNot(LitB1);
+ RetValue = 1;
+ }
+ assert( !Abc_LitIsCompl(LitA1) );
+ // arrange literals in such as a way that
+ // - the first two literals are control literals from different cubes
+ // - the third literal is non-complented data input
+ // - the forth literal is possibly complemented data input
+ L[0] = Abc_Var2Lit( LitA0, 0 );
+ L[1] = Abc_Var2Lit( LitB0, 1 );
+ L[2] = Abc_Var2Lit( LitA1, 0 );
+ L[3] = Abc_Var2Lit( LitB1, 1 );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Creates a Divisor. ]
+
+ Description [ This functions receive as input two sub-cubes and creates
+ a divisor using their information. The divisor is stored
+ in vCubeFree vector of the pFxchMan structure.
+
+ It returns the base value, which is the number of elements
+ that the cubes pair used to generate the devisor have in
+ common. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
+ Fxch_SubCube_t* pSubCube0,
+ Fxch_SubCube_t* pSubCube1 )
+{
+ int Base = 0;
+
+ Vec_IntClear( pFxchMan->vCubeFree );
+
+ int SC0_Lit0,
+ SC0_Lit1,
+ SC1_Lit0,
+ SC1_Lit1;
+
+ SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
+ SC0_Lit1 = 0;
+ SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
+ SC1_Lit1 = 0;
+
+ if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
+ {
+ Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+ Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+ }
+ else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
+ {
+ SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
+ SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
+
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
+
+ int RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
+ if ( RetValue == -1 )
+ return -1;
+ }
+ else
+ {
+ if ( pSubCube0->iLit1 > 0 )
+ {
+ SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
+
+ Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+ if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
+ Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
+ else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
+ Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+ }
+ else
+ {
+ SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
+
+ Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+ if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
+ Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
+ else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
+ Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+ }
+ }
+
+ if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
+ return -1;
+
+ if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
+ {
+ Vec_IntSort( pFxchMan->vCubeFree, 0 );
+
+ Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
+ Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
+ }
+
+ int Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) ),
+ Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
+ if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
+ {
+ Base = Abc_MinInt( Cube0Size, Cube1Size )
+ -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */
+ }
+ else
+ return -1;
+
+ return Base;
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Add a divisor to the divisors hash table. ]
+
+ Description [ This functions will try to add the divisor store in
+ vCubeFree to the divisor hash table. If the divisor
+ is already present in the hash table it will just
+ increment its weight, otherwise it will add the divisor
+ and asign an initial weight. ]
+
+ SideEffects [ If the fUpdate option is set, the function will also
+ update the divisor priority queue. ]
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
+ int fUpdate,
+ int fSingleCube,
+ int fBase )
+{
+ int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
+
+ /* Verify if the divisor already exist */
+ if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
+ {
+ if ( pFxchMan->SMode == 0 )
+ Vec_WecPushLevel( pFxchMan->vDivCubePairs );
+
+ /* Assign initial weight */
+ if ( fSingleCube )
+ {
+ Vec_FltPush( pFxchMan->vDivWeights,
+ -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
+ -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
+ }
+ else
+ {
+ Vec_FltPush( pFxchMan->vDivWeights,
+ -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
+ -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
+ }
+
+ }
+
+ /* Increment weight */
+ if ( fSingleCube )
+ Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
+ else
+ Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
+
+ assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
+
+ if ( fUpdate )
+ if ( pFxchMan->vDivPrio )
+ {
+ if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
+ Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
+ else
+ Vec_QuePush( pFxchMan->vDivPrio, iDiv );
+ }
+
+ return iDiv;
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Removes a divisor to the divisors hash table. ]
+
+ Description [ This function don't effectively removes a divisor from
+ the hash table (the hash table implementation don't
+ support such operation). It only assures its existence
+ and decrement its weight. ]
+
+ SideEffects [ If the fUpdate option is set, the function will also
+ update the divisor priority queue. ]
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_DivRemove( Fxch_Man_t* pFxchMan,
+ int fUpdate,
+ int fSingleCube,
+ int fBase )
+{
+ int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
+
+ assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
+
+ /* Decrement weight */
+ if ( fSingleCube )
+ Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
+ else
+ Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
+
+ if ( fUpdate )
+ if ( pFxchMan->vDivPrio )
+ {
+ if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
+ Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
+ }
+
+ return iDiv;
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Separete the cubes in present in a divisor ]
+
+ Description [ In this implementation *all* stored divsors are composed
+ of two cubes.
+
+ In order to save space and to be able to use the Vec_Int_t
+ hash table both cubes are stored in the same vector - using
+ a little hack to differentiate which literal belongs to each
+ cube.
+
+ This function separetes the two cubes in their own vectors
+ so that they can be added to the cover.
+
+ *Note* that this also applies to single cube
+ divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fxch_DivSepareteCubes( Vec_Int_t* vDiv,
+ Vec_Int_t* vCube0,
+ Vec_Int_t* vCube1 )
+{
+ int* pArray;
+ int i,
+ Lit;
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ if ( Abc_LitIsCompl(Lit) )
+ Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
+ else
+ Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
+
+ if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
+ {
+ assert( Vec_IntSize( vCube1 ) == 3 );
+
+ pArray = Vec_IntArray( vCube0 );
+ if ( pArray[1] > pArray[2] )
+ ABC_SWAP( int, pArray[1], pArray[2] );
+
+ pArray = Vec_IntArray( vCube1 );
+ if ( pArray[1] > pArray[2] )
+ ABC_SWAP( int, pArray[1], pArray[2] );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Removes the literals present in the divisor from their
+ original cubes. ]
+
+ Description [ This function returns the numeber of removed literals
+ which should be equal to the size of the divisor. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_DivRemoveLits( Vec_Int_t* vCube0,
+ Vec_Int_t* vCube1,
+ Vec_Int_t* vDiv,
+ int *fCompl )
+{
+ int i,
+ Lit,
+ CountP = 0,
+ CountN = 0,
+ Count = 0,
+ ret = 0;
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
+ CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
+ else
+ CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
+
+ if ( Vec_IntSize( vDiv ) == 2 )
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ {
+ Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
+ Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
+ }
+
+ ret = Count + CountP + CountN;
+
+ if ( Vec_IntSize( vDiv ) == 4 )
+ {
+ int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
+ Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
+ Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
+ Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
+
+ if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
+ *fCompl = 1;
+
+ if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
+ {
+ *fCompl = 1;
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
+ }
+ }
+
+ return ret;
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Print the divisor identified by iDiv. ]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
+ int iDiv )
+{
+ Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
+ int i,
+ Lit;
+
+ printf( "Div %7d : ", iDiv );
+ printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ if ( !Abc_LitIsCompl( Lit ) )
+ printf( "%d(1)", Abc_Lit2Var( Lit ) );
+
+ printf( " + " );
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ if ( Abc_LitIsCompl( Lit ) )
+ printf( "%d(2)", Abc_Lit2Var( Lit ) );
+
+ printf( " Lits =%7d ", pFxchMan->nLits );
+ printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) );
+}
+
+/* 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 i,
+ Lit;
+ * pLit0 = -1;
+ * pLit1 = -1;
+
+ Vec_IntForEachEntry( vDiv, Lit, i )
+ {
+ if ( Abc_LitIsCompl( Lit ) )
+ {
+ if ( *pLit1 == -1 )
+ *pLit1 = Abc_Lit2Var( Lit );
+ }
+ else
+ {
+ if ( *pLit0 == -1 )
+ *pLit0 = Abc_Lit2Var( Lit );
+ }
+ if ( *pLit0 >= 0 && *pLit1 >= 0 )
+ return;
+ }
+}
+
+int Fxch_DivFind( Vec_Int_t* vCube0,
+ Vec_Int_t* vCube1,
+ Vec_Int_t* vCubeFree )
+{
+ int Counter = 0,
+ fAttr0 = 0,
+ fAttr1 = 1;
+ int* pBeg1 = vCube0->pArray + 1,
+ * pBeg2 = vCube1->pArray + 1,
+ * pEnd1 = vCube0->pArray + vCube0->nSize,
+ * pEnd2 = vCube1->pArray + vCube1->nSize;
+
+ Vec_IntClear( vCubeFree );
+
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ {
+ pBeg1++;
+ pBeg2++;
+ Counter++;
+ }
+ else if ( *pBeg1 < *pBeg2 )
+ Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) );
+ else
+ {
+ if ( Vec_IntSize( vCubeFree ) == 0 )
+ fAttr0 = 1, fAttr1 = 0;
+ Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1) );
+ }
+ }
+ while ( pBeg1 < pEnd1 )
+ Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) );
+ while ( pBeg2 < pEnd2 )
+ Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1 ) );
+
+ assert( !Abc_LitIsCompl( Vec_IntEntry(vCubeFree, 0) ) );
+ return Counter;
+}
+
+void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan,
+ Vec_Int_t* vCubes_Lit0,
+ Vec_Int_t* vCubes_Lit1 )
+{
+ int* pBeg1 = vCubes_Lit0->pArray + 1,
+ * pBeg2 = vCubes_Lit1->pArray + 1,
+ * pEnd1 = vCubes_Lit0->pArray + vCubes_Lit0->nSize,
+ * pEnd2 = vCubes_Lit1->pArray + vCubes_Lit1->nSize;
+
+ Vec_IntClear( pFxchMan->vPairs );
+
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ),
+ CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ),
+ i, k;
+
+ if ( CubeId1 == CubeId2 )
+ {
+ for ( i = 1; pBeg1+i < pEnd1; i++ )
+ if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg1[i], 0) )
+ break;
+
+ for ( k = 1; pBeg2+k < pEnd2; k++ )
+ if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) )
+ break;
+
+ for ( int i_ = 0; i_ < i; i_++ )
+ for ( int k_ = 0; k_ < k; k_++ )
+ {
+ if ( pBeg1[i_] == pBeg2[k_] )
+ continue;
+ Fxch_DivFind( Vec_WecEntry( pFxchMan->vCubes, pBeg1[i_] ),
+ Vec_WecEntry( pFxchMan->vCubes, pBeg2[k_] ),
+ pFxchMan->vCubeFree );
+
+ if ( Vec_IntSize( pFxchMan->vCubeFree ) == 4 )
+ Fxch_DivNormalize( pFxchMan->vCubeFree );
+
+ if ( !Vec_IntEqual( pFxchMan->vDiv, pFxchMan->vCubeFree ) )
+ continue;
+
+ Vec_IntPush( pFxchMan->vPairs, pBeg1[i_] );
+ Vec_IntPush( pFxchMan->vPairs, pBeg2[k_] );
+ }
+ pBeg1 += i;
+ pBeg2 += k;
+ }
+ else if ( CubeId1 < CubeId2 )
+ pBeg1++;
+ else
+ pBeg2++;
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c
new file mode 100644
index 00000000..6437950d
--- /dev/null
+++ b/src/opt/fxch/FxchMan.c
@@ -0,0 +1,600 @@
+/**CFile****************************************************************
+
+ FileName [ FxchMan.c ]
+
+ PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+ Synopsis [ Fxch Manager implementation ]
+
+ 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
+
+////////////////////////////////////////////////////////////////////////
+/// LOCAL FUNCTIONS DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan,
+ unsigned int SubCubeID,
+ unsigned int iSubCube,
+ unsigned int iCube,
+ unsigned int iLit0,
+ unsigned int iLit1,
+ char fAdd,
+ char fUpdate )
+{
+ int ret = 0;
+
+ if ( fAdd )
+ {
+ ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes,
+ SubCubeID, iSubCube,
+ iCube, iLit0, iLit1, fUpdate );
+ }
+ else
+ {
+ ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes,
+ SubCubeID, iSubCube,
+ iCube, iLit0, iLit1, fUpdate );
+ }
+
+ return ret;
+}
+
+
+static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan,
+ int iCube,
+ int fAdd,
+ int fUpdate )
+{
+ Vec_Int_t* vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
+ int i, k,
+ Lit0,
+ Lit1,
+ fSingleCube = 1,
+ fBase = 0;
+
+ if ( Vec_IntSize(vCube) < 2 )
+ return 0;
+
+ Vec_IntForEachEntryStart( vCube, Lit0, i, 1)
+ Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) )
+ {
+ assert( Lit0 < Lit1 );
+
+ Vec_IntClear( pFxchMan->vCubeFree );
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit0 ), 0 ) );
+ Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit1 ), 1 ) );
+
+ if (fAdd)
+ {
+ Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase );
+ pFxchMan->nPairsS++;
+ }
+ else
+ {
+ Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase );
+ pFxchMan->nPairsS--;
+ }
+ }
+
+ return Vec_IntSize( vCube ) * ( Vec_IntSize( vCube ) - 1 ) / 2;
+}
+
+static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
+ int iCube,
+ int fAdd,
+ int fUpdate )
+{
+ Vec_Int_t* vLitHashKeys = pFxchMan->vLitHashKeys,
+ * vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
+ int SubCubeID = 0,
+ nHashedSC = 0,
+ iLit0,
+ Lit0;
+
+ Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
+ SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
+
+ Fxch_ManSCAddRemove( pFxchMan,
+ SubCubeID, nHashedSC++,
+ iCube, 0, 0,
+ fAdd, fUpdate );
+
+ Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
+ {
+ /* 1 Lit remove */
+ SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 );
+
+ pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
+ SubCubeID, nHashedSC++,
+ iCube, iLit0, 0,
+ fAdd, fUpdate );
+
+ if ( Vec_IntSize( vCube ) > 3 )
+ {
+ int Lit1,
+ iLit1;
+
+ Vec_IntForEachEntryStart( vCube, Lit1, iLit1, iLit0 + 1)
+ {
+ /* 2 Lit remove */
+ SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 );
+
+ pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
+ SubCubeID, nHashedSC++,
+ iCube, iLit0, iLit1,
+ fAdd, fUpdate );
+
+ SubCubeID += Vec_IntEntry( vLitHashKeys, Lit1 );
+ }
+ }
+
+ SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
+ }
+}
+
+static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes,
+ Vec_Int_t* vLit2Cube )
+{
+ int i,
+ k = 0,
+ CubeId;
+
+ Vec_IntForEachEntry( vLit2Cube, CubeId, i )
+ if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
+ Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
+
+ Vec_IntShrink( vLit2Cube, k );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// PUBLIC INTERFACE ///
+////////////////////////////////////////////////////////////////////////
+Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes,
+ char SMode )
+{
+ Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 );
+
+ pFxchMan->vCubes = vCubes;
+ pFxchMan->pDivHash = Hsh_VecManStart( 1000 );
+ pFxchMan->vDivWeights = Vec_FltAlloc( 1000 );
+
+ pFxchMan->SMode = SMode;
+ if ( pFxchMan->SMode == 0 )
+ pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 );
+
+ pFxchMan->vCubeFree = Vec_IntAlloc( 100 );
+ pFxchMan->vDiv = Vec_IntAlloc( 100 );
+ pFxchMan->vCubesS = Vec_IntAlloc( 100 );
+ pFxchMan->vPairs = Vec_IntAlloc( 100 );
+
+ return pFxchMan;
+}
+
+void Fxch_ManFree( Fxch_Man_t* pFxchMan )
+{
+ Vec_WecFree( pFxchMan->vLits );
+ Vec_IntFree( pFxchMan->vLitCount );
+ Vec_IntFree( pFxchMan->vLitHashKeys );
+
+ Hsh_VecManStop( pFxchMan->pDivHash );
+ Vec_FltFree( pFxchMan->vDivWeights );
+ Vec_QueFree( pFxchMan->vDivPrio );
+
+ if ( pFxchMan->SMode == 0 )
+ Vec_WecFree( pFxchMan->vDivCubePairs );
+
+ Vec_IntFree( pFxchMan->vLevels );
+
+ Vec_IntFree( pFxchMan->vCubeFree );
+ Vec_IntFree( pFxchMan->vDiv );
+ Vec_IntFree( pFxchMan->vCubesS );
+ Vec_IntFree( pFxchMan->vPairs );
+
+ ABC_FREE( pFxchMan );
+}
+
+void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan,
+ int nVars )
+{
+
+ Vec_Int_t* vCube;
+ int i, k,
+ Lit,
+ Count;
+
+ pFxchMan->nVars = 0;
+ pFxchMan->nLits = 0;
+ Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+ {
+ assert( Vec_IntSize(vCube) > 0 );
+ pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Vec_IntEntry( vCube, 0 ) );
+ pFxchMan->nLits += Vec_IntSize(vCube) - 1;
+ Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+ pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Abc_Lit2Var( Lit ) );
+ }
+
+ assert( pFxchMan->nVars < nVars );
+ pFxchMan->nVars = nVars;
+
+ /* Count the number of time each literal appears on the SOP */
+ pFxchMan->vLitCount = Vec_IntStart( 2 * pFxchMan->nVars );
+ Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+ Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+ Vec_IntAddToEntry( pFxchMan->vLitCount, Lit, 1 );
+
+ /* Allocate space to the array of arrays wich maps Literals into cubes which uses them */
+ pFxchMan->vLits = Vec_WecStart( 2 * pFxchMan->nVars );
+ Vec_IntForEachEntry( pFxchMan->vLitCount, Count, Lit )
+ Vec_IntGrow( Vec_WecEntry( pFxchMan->vLits, Lit ), Count );
+
+ /* Maps Literals into cubes which uses them */
+ Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+ Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+ Vec_WecPush( pFxchMan->vLits, Lit, i );
+}
+
+void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan )
+{
+ /* Generates the random number which will be used for hashing cubes */
+ Gia_ManRandom( 1 );
+ pFxchMan->vLitHashKeys = Vec_IntAlloc( ( 2 * pFxchMan->nVars ) );
+ for ( int i = 0; i < (2 * pFxchMan->nVars); i++ )
+ Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+}
+
+void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan )
+{
+ Vec_Wec_t* vCubes = pFxchMan->vCubes;
+ Vec_Int_t* vCube,
+ * vCubeLinks;
+ int iCube,
+ nTotalHashed = 0;
+
+ vCubeLinks = Vec_IntAlloc( Vec_WecSize( vCubes ) + 1 );
+ Vec_WecForEachLevel( vCubes, vCube, iCube )
+ {
+ int nLits = Vec_IntSize( vCube ) - 1,
+ nSubCubes = nLits == 2? nLits : ( nLits * nLits + nLits ) / 2;
+
+ Vec_IntPush( vCubeLinks, ( nTotalHashed + 1 ) );
+ nTotalHashed += nSubCubes + 1;
+ }
+
+ pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, vCubeLinks, nTotalHashed );
+}
+
+void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan )
+{
+ Fxch_SCHashTableDelete( pFxchMan->pSCHashTable );
+}
+
+void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan )
+{
+ Vec_Int_t* vCube;
+ float Weight;
+ int fAdd = 1,
+ fUpdate = 0,
+ iCube;
+
+ Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
+ {
+ Fxch_ManDivSingleCube( pFxchMan, iCube, fAdd, fUpdate );
+ Fxch_ManDivDoubleCube( pFxchMan, iCube, fAdd, fUpdate );
+ }
+
+ pFxchMan->vDivPrio = Vec_QueAlloc( Vec_FltSize( pFxchMan->vDivWeights ) );
+ Vec_QueSetPriority( pFxchMan->vDivPrio, Vec_FltArrayP( pFxchMan->vDivWeights ) );
+ Vec_FltForEachEntry( pFxchMan->vDivWeights, Weight, iCube )
+ {
+ if ( Weight > 0.0 )
+ Vec_QuePush( pFxchMan->vDivPrio, iCube );
+ }
+}
+
+/* Level Computation */
+int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan,
+ Vec_Int_t* vCubeFree )
+{
+ int i,
+ Lit,
+ Level = 0;
+
+ Vec_IntForEachEntry( vCubeFree, Lit, i )
+ Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Abc_Lit2Var( Lit ) ) ) );
+
+ return Abc_MinInt( Level, 800 );
+}
+
+int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan,
+ Vec_Int_t * vCube )
+{
+ int k,
+ Lit,
+ Level = 0;
+
+ Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+ Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Lit ) ) );
+
+ return Level;
+}
+
+void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan )
+{
+ Vec_Int_t* vCube;
+ int i,
+ iVar,
+ iFirst = 0;
+
+ iVar = Vec_IntEntry( Vec_WecEntry( pFxchMan->vCubes, 0 ), 0 );
+ pFxchMan->vLevels = Vec_IntStart( pFxchMan->nVars );
+
+ Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+ {
+ if ( iVar != Vec_IntEntry( vCube, 0 ) )
+ {
+ Vec_IntAddToEntry( pFxchMan->vLevels, iVar, i - iFirst );
+ iVar = Vec_IntEntry( vCube, 0 );
+ iFirst = i;
+ }
+ Vec_IntUpdateEntry( pFxchMan->vLevels, iVar, Fxch_ManComputeLevelCube( pFxchMan, vCube ) );
+ }
+}
+
+void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
+ int iDiv )
+{
+ int i,
+ iCube0,
+ iCube1,
+ Lit0 = -1,
+ Lit1 = -1;
+
+ Vec_Int_t* vCube0,
+ * vCube1,
+ * vLitP,
+ * vLitN,
+ * vDivCubePairs;
+
+ /* Get the selected candidate (divisor) */
+ Vec_IntClear( pFxchMan->vDiv );
+ Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) );
+
+ /* Find cubes associated with the single divisor */
+ Vec_IntClear( pFxchMan->vCubesS );
+ if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
+ {
+ Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) );
+ Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) );
+
+ Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) );
+ Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) );
+ Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ),
+ Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ),
+ pFxchMan->vCubesS );
+ }
+ else
+ Fxch_DivFindPivots( pFxchMan->vDiv, &Lit0, &Lit1 );
+
+ assert( Lit0 >= 0 && Lit1 >= 0 );
+
+ /* Find pairs associated with the divisor */
+ Vec_IntClear( pFxchMan->vPairs );
+ if ( pFxchMan->SMode == 1 )
+ {
+ Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit0) );
+ Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit1) );
+ Fxch_DivFindCubePairs( pFxchMan, Vec_WecEntry( pFxchMan->vLits, Lit0 ), Vec_WecEntry( pFxchMan->vLits, Lit1 ) );
+ }
+ else
+ {
+ vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv );
+ Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs );
+ Vec_IntErase( vDivCubePairs );
+ }
+
+ Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
+ {
+ assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) );
+ if (iCube0 > iCube1)
+ {
+ Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1);
+ Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0);
+ }
+ }
+
+ Vec_IntUniqifyPairs( pFxchMan->vPairs );
+ assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 );
+
+ /* subtract cost of single-cube divisors */
+ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+ Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */
+
+ Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
+ Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1), /* remove (fAdd = 0) - fUpdate = 1 */
+ Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */
+
+ /* subtract cost of double-cube divisors */
+ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+ {
+ if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+ Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
+ }
+
+ Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+ {
+ if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+ Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
+
+ }
+
+ /* Create a new variable */
+ int iVarNew = pFxchMan->nVars;
+ pFxchMan->nVars++;
+
+ /* Create new Lit hash keys */
+ Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+ Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+
+ /* Create new Cube */
+ vCube0 = Vec_WecPushLevel( pFxchMan->vCubes );
+ Vec_IntPush( vCube0, iVarNew );
+
+ int Level;
+ if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
+ {
+ if ( Lit0 > Lit1 )
+ ABC_SWAP(int, Lit0, Lit1);
+
+ Vec_IntPush( vCube0, Abc_LitNot( Lit0 ) );
+ Vec_IntPush( vCube0, Abc_LitNot( Lit1 ) );
+ Level = 1 + Fxch_ManComputeLevelCube( pFxchMan, vCube0 );
+ }
+ else
+ {
+ vCube1 = Vec_WecPushLevel( pFxchMan->vCubes );
+ vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 );
+ Vec_IntPush( vCube1, iVarNew );
+ Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 );
+ Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ),
+ Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) );
+ }
+ assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew );
+ Vec_IntPush( pFxchMan->vLevels, Level );
+
+ pFxchMan->nLits += Vec_IntSize( pFxchMan->vDiv );
+
+ /* Create new literals */
+ vLitP = Vec_WecPushLevel( pFxchMan->vLits );
+ vLitN = Vec_WecPushLevel( pFxchMan->vLits );
+ vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 );
+
+ /* Extract divisor from single-cubes */
+ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+ {
+ int RetValue;
+
+ vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 );
+ RetValue = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) );
+ RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) );
+ assert( RetValue == 2 );
+
+ Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
+ Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+
+ pFxchMan->nLits--;
+ }
+
+ /* For each pair (Ci, Cj) */
+ /* Extract divisor from cube pairs */
+ int k = 0,
+ nCompls = 0;
+ Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
+ {
+ int RetValue, fCompl = 0;
+
+ vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 );
+ vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 );
+
+ RetValue = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl );
+ nCompls += fCompl;
+
+ assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) );
+
+ if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl )
+ {
+ Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) );
+ Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+ }
+ else
+ {
+ Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
+ Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+ }
+ pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2;
+
+ /* Remove second cube */
+ Vec_IntClear( vCube1 );
+ Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+ }
+ assert( k == Vec_IntSize( pFxchMan->vPairs ) / 2 );
+ Vec_IntShrink( pFxchMan->vPairs, k );
+
+ /* Add cost of single-cube divisors */
+ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+ Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+ Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+ Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+ /* Add cost of double-cube divisors */
+ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+ if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+ Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+ Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+ if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+ Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+ /* If it's a double-cube devisor add its cost */
+ if ( Vec_IntSize( pFxchMan->vDiv ) > 2 )
+ {
+ iCube0 = Vec_WecSize( pFxchMan->vCubes ) - 2;
+ iCube1 = Vec_WecSize( pFxchMan->vCubes ) - 1;
+
+ Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+ Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+ vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 );
+ Vec_IntForEachEntryStart( vCube0, Lit0, i, 1 )
+ Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+
+ vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 );
+ Vec_IntForEachEntryStart( vCube1, Lit0, i, 1 )
+ Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
+ }
+
+ /* remove these cubes from the lit array of the divisor */
+ Vec_IntForEachEntry( pFxchMan->vDiv, Lit0, i )
+ {
+ Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit0 ) ), pFxchMan->vPairs );
+ Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit0 ) ) ), pFxchMan->vPairs );
+ }
+
+ pFxchMan->nExtDivs++;
+}
+
+/* Print */
+void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan )
+{
+ int iDiv;
+
+ for ( iDiv = 0; iDiv < Vec_FltSize( pFxchMan->vDivWeights ); iDiv++ )
+ Fxch_DivPrint( pFxchMan, iDiv );
+}
+
+void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan )
+{
+ printf( "[FXCH] ");
+ printf( "Cubes =%8d ", Vec_WecSizeUsed( pFxchMan->vCubes ) );
+ printf( "Lits =%8d ", Vec_WecSizeUsed( pFxchMan->vLits ) );
+ printf( "Divs =%8d ", Hsh_VecSize( pFxchMan->pDivHash ) );
+ printf( "Divs+ =%8d ", Vec_QueSize( pFxchMan->vDivPrio ) );
+ printf( "Extr =%7d \n", pFxchMan->nExtDivs );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c
new file mode 100644
index 00000000..f9c3e7a2
--- /dev/null
+++ b/src/opt/fxch/FxchSCHashTable.c
@@ -0,0 +1,401 @@
+/**CFile****************************************************************
+
+ FileName [ FxchSCHashTable.c ]
+
+ PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+ Synopsis [ Sub-cubes hash table implementation ]
+
+ 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 ///
+////////////////////////////////////////////////////////////////////////
+static inline void MurmurHash3_x86_32 ( const void* key,
+ int len,
+ uint32_t seed,
+ void* out )
+{
+ const uint8_t* data = (const uint8_t*)key;
+ const int nblocks = len / 4;
+
+ uint32_t h1 = seed;
+
+ const uint32_t c1 = 0xcc9e2d51;
+ const uint32_t c2 = 0x1b873593;
+
+ //----------
+ // body
+
+ const uint32_t * blocks = (const uint32_t *)(data + nblocks*4);
+
+ for(int i = -nblocks; i; i++)
+ {
+ uint32_t k1 = blocks[i];
+
+ k1 *= c1;
+ k1 = (k1 << 15) | (k1 >> (32 - 15));
+ k1 *= c2;
+
+ h1 ^= k1;
+ h1 = (h1 << 13) | (h1 >> (32 - 13));
+ h1 = h1*5+0xe6546b64;
+ }
+
+ //----------
+ // tail
+
+ const uint8_t * tail = (const uint8_t*)(data + nblocks*4);
+
+ uint32_t k1 = 0;
+
+ switch(len & 3)
+ {
+ case 3: k1 ^= tail[2] << 16;
+ case 2: k1 ^= tail[1] << 8;
+ case 1: k1 ^= tail[0];
+ k1 *= c1; k1 = (k1 << 15) | (k1 >> (32 - 15)); k1 *= c2; h1 ^= k1;
+ };
+
+ //----------
+ // finalization
+
+ h1 ^= len;
+
+ h1 ^= h1 >> 16;
+ h1 *= 0x85ebca6b;
+ h1 ^= h1 >> 13;
+ h1 *= 0xc2b2ae35;
+ h1 ^= h1 >> 16;
+
+ *(uint32_t*)out = h1;
+}
+
+Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan,
+ Vec_Int_t* vCubeLinks,
+ int nEntries )
+{
+ Fxch_SCHashTable_t* pSCHashTable = ABC_CALLOC( Fxch_SCHashTable_t, 1 );
+ int nBits = Abc_Base2Log( nEntries + 1 ) + 1;
+
+
+ pSCHashTable->pFxchMan = pFxchMan;
+ pSCHashTable->SizeMask = (1 << nBits) - 1;
+ pSCHashTable->vCubeLinks = vCubeLinks;
+ pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 );
+
+ return pSCHashTable;
+}
+
+void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* pSCHashTable )
+{
+ Vec_IntFree( pSCHashTable->vCubeLinks );
+ Vec_IntErase( &pSCHashTable->vSubCube0 );
+ Vec_IntErase( &pSCHashTable->vSubCube1 );
+ ABC_FREE( pSCHashTable->pBins );
+ ABC_FREE( pSCHashTable );
+}
+
+static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t* pSCHashTable,
+ unsigned int SubCubeID )
+{
+ return pSCHashTable->pBins + (SubCubeID & pSCHashTable->SizeMask);
+}
+
+static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableEntry( Fxch_SCHashTable_t* pSCHashTable,
+ unsigned int iEntry )
+{
+ if ( ( iEntry > 0 ) && ( iEntry < ( pSCHashTable->SizeMask + 1 ) ) )
+ return pSCHashTable->pBins + iEntry;
+
+ return NULL;
+}
+
+static inline void Fxch_SCHashTableInsertLink( Fxch_SCHashTable_t* pSCHashTable,
+ unsigned int iEntry0,
+ unsigned int iEntry1 )
+{
+ Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ),
+ * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ),
+ * pEntry0Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry0->iNext );
+
+ assert( pEntry0Next->iPrev == iEntry0 );
+
+ pEntry1->iNext = pEntry0->iNext;
+ pEntry0->iNext = iEntry1;
+ pEntry1->iPrev = iEntry0;
+ pEntry0Next->iPrev = iEntry1;
+}
+
+static inline void Fxch_SCHashTableRemoveLink( Fxch_SCHashTable_t* pSCHashTable,
+ int iEntry0,
+ int iEntry1 )
+{
+ Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ),
+ * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ),
+ * pEntry1Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry1->iNext );
+
+ assert( pEntry0->iNext == iEntry1 );
+ assert( pEntry1->iPrev == iEntry0 );
+ assert( pEntry1Next->iPrev == iEntry1 );
+
+ pEntry0->iNext = pEntry1->iNext;
+ pEntry1->iNext = 0;
+ pEntry1Next->iPrev = pEntry1->iPrev;
+ pEntry1->iPrev = 0;
+}
+
+static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable,
+ Vec_Wec_t* vCubes,
+ Fxch_SubCube_t* pSCData0,
+ Fxch_SubCube_t* pSCData1 )
+{
+ Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ),
+ * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube );
+
+ if ( !Vec_IntSize( vCube0 ) ||
+ !Vec_IntSize( vCube1 ) ||
+ Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) ||
+ pSCData0->Id != pSCData1->Id )
+ return 0;
+
+ Vec_IntClear( &pSCHashTable->vSubCube0 );
+ Vec_IntClear( &pSCHashTable->vSubCube1 );
+
+ if ( pSCData0->iLit1 == 0 && pSCData1->iLit1 == 0 &&
+ Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Abc_LitNot( Vec_IntEntry( vCube1, pSCData1->iLit0 ) ) )
+ return 0;
+
+ if ( pSCData0->iLit1 > 0 && pSCData1->iLit1 > 0 &&
+ ( Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
+ Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ||
+ Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
+ Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) )
+ return 0;
+
+
+ if ( pSCData0->iLit0 > 0 )
+ Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 );
+ else
+ Vec_IntAppend( &pSCHashTable->vSubCube0, vCube0 );
+
+ if ( pSCData1->iLit0 > 0 )
+ Vec_IntAppendSkip( &pSCHashTable->vSubCube1, vCube1, pSCData1->iLit0 );
+ else
+ Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 );
+
+
+ if ( pSCData0->iLit1 > 0)
+ Vec_IntDrop( &pSCHashTable->vSubCube0,
+ pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 );
+
+ if ( pSCData1->iLit1 > 0 )
+ Vec_IntDrop( &pSCHashTable->vSubCube1,
+ pSCData1->iLit0 < pSCData1->iLit1 ? pSCData1->iLit1 - 1 : pSCData1->iLit1 );
+
+ Vec_IntDrop( &pSCHashTable->vSubCube0, 0 );
+ Vec_IntDrop( &pSCHashTable->vSubCube1, 0 );
+
+ return Vec_IntEqual( &pSCHashTable->vSubCube0, &pSCHashTable->vSubCube1 );
+}
+
+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 )
+{
+ unsigned int BinID;
+ MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
+
+ unsigned int iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
+ Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ),
+ * pNewEntry = Fxch_SCHashTableEntry( pSCHashTable, iNewEntry );
+
+ assert( pNewEntry->Used == 0 );
+
+ pNewEntry->SCData.Id = SubCubeID;
+ pNewEntry->SCData.iCube = iCube;
+ pNewEntry->SCData.iLit0 = iLit0;
+ pNewEntry->SCData.iLit1 = iLit1;
+
+ pNewEntry->Used = 1;
+ pSCHashTable->nEntries++;
+ if ( pBin->iTable == 0 )
+ {
+ pBin->iTable = iNewEntry;
+ pNewEntry->iNext = iNewEntry;
+ pNewEntry->iPrev = iNewEntry;
+ return 0;
+ }
+
+ Fxch_SCHashTable_Entry_t* pEntry;
+ unsigned int iEntry;
+ char Pairs = 0,
+ fStart = 1;
+ for ( iEntry = pBin->iTable; iEntry != pBin->iTable || fStart; iEntry = pEntry->iNext, fStart = 0 )
+ {
+ pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
+
+ if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) )
+ continue;
+
+ if ( pEntry->SCData.iLit0 == 0 )
+ {
+ printf("[FXCH] SCC detected\n");
+ continue;
+ }
+ if ( pNewEntry->SCData.iLit0 == 0 )
+ {
+ printf("[FXCH] SCC detected\n");
+ continue;
+ }
+
+ int Base;
+ if ( pEntry->SCData.iCube < pNewEntry->SCData.iCube )
+ Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNewEntry->SCData ) );
+ else
+ Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNewEntry->SCData ), &( pEntry->SCData ) );
+
+ if ( Base < 0 )
+ continue;
+
+ int iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
+
+ if ( pSCHashTable->pFxchMan->SMode == 0 )
+ {
+ Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube );
+ Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube );
+ }
+
+ Pairs++;
+ }
+ assert( iEntry == (unsigned int)( pBin->iTable ) );
+
+ pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
+ Fxch_SCHashTableInsertLink( pSCHashTable, pEntry->iPrev, iNewEntry );
+
+ return Pairs;
+}
+
+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 BinID;
+ MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
+
+ unsigned int iEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
+ Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ),
+ * pEntry = Fxch_SCHashTableEntry( pSCHashTable, iEntry );
+
+ assert( pEntry->Used == 1 );
+ assert( pEntry->SCData.iCube == iCube );
+
+ if ( pEntry->iNext == iEntry )
+ {
+ assert( pEntry->iPrev == iEntry );
+ pBin->iTable = 0;
+ pEntry->iNext = 0;
+ pEntry->iPrev = 0;
+ pEntry->Used = 0;
+ return 0;
+ }
+
+ Fxch_SCHashTable_Entry_t* pNextEntry;
+ int iNextEntry,
+ Pairs = 0,
+ fStart = 1;
+ for ( iNextEntry = pEntry->iNext; iNextEntry != iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 )
+ {
+ pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry );
+
+ if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) )
+ || pEntry->SCData.iLit0 == 0
+ || pNextEntry->SCData.iLit0 == 0 )
+ continue;
+
+ int Base;
+ if ( pNextEntry->SCData.iCube < pEntry->SCData.iCube )
+ Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNextEntry->SCData ), &( pEntry->SCData ) );
+ else
+ Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNextEntry->SCData ) );
+
+ if ( Base < 0 )
+ continue;
+
+ int iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
+
+ if ( pSCHashTable->pFxchMan->SMode == 0 )
+ {
+ int i,
+ iCube0,
+ iCube1;
+
+ Vec_Int_t* vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv );
+ Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i )
+ if ( ( iCube0 == pNextEntry->SCData.iCube && iCube1 == pEntry->SCData.iCube ) ||
+ ( iCube0 == pEntry->SCData.iCube && iCube1 == pNextEntry->SCData.iCube ) )
+ {
+ Vec_IntDrop( vDivCubePairs, i+1 );
+ Vec_IntDrop( vDivCubePairs, i );
+ }
+ if ( Vec_IntSize( vDivCubePairs ) == 0 )
+ Vec_IntErase( vDivCubePairs );
+ }
+
+ Pairs++;
+ }
+
+ if ( pBin->iTable == iEntry )
+ pBin->iTable = ( pEntry->iNext != iEntry ) ? pEntry->iNext : 0;
+
+ pEntry->Used = 0;
+ Fxch_SCHashTableRemoveLink( pSCHashTable, pEntry->iPrev, iEntry );
+ return Pairs;
+}
+
+unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* pHashTable )
+{
+ unsigned int Memory = sizeof ( Fxch_SCHashTable_t );
+
+ Memory += Vec_IntMemory( pHashTable->vCubeLinks );
+ Memory += sizeof( Fxch_SubCube_t ) * ( pHashTable->SizeMask + 1 );
+
+ return Memory;
+}
+
+void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* pHashTable )
+{
+ printf( "SubCube Hash Table at %p\n", ( void* )pHashTable );
+ printf("%20s %20s\n", "nEntries",
+ "Memory Usage (MB)" );
+
+ int Memory = Fxch_SCHashTableMemory( pHashTable );
+ printf("%20d %18.2f\n", pHashTable->nEntries,
+ ( ( double ) Memory / 1048576 ) );
+}
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/fxch/module.make b/src/opt/fxch/module.make
new file mode 100644
index 00000000..48f36b13
--- /dev/null
+++ b/src/opt/fxch/module.make
@@ -0,0 +1,4 @@
+SRC += src/opt/fxch/Fxch.c \
+ src/opt/fxch/FxchDiv.c \
+ src/opt/fxch/FxchMan.c \
+ src/opt/fxch/FxchSCHashTable.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 21:52:55 +0000