summaryrefslogtreecommitdiffstats
path: root/src/base/pla
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/pla')
-rw-r--r--src/base/pla/module.make2
-rw-r--r--src/base/pla/pla.h54
-rw-r--r--src/base/pla/plaCom.c25
-rw-r--r--src/base/pla/plaFxch.c854
-rw-r--r--src/base/pla/plaHash.c144
-rw-r--r--src/base/pla/plaMan.c60
-rw-r--r--src/base/pla/plaSimple.c339
-rw-r--r--src/base/pla/plaWrite.c2
8 files changed, 1441 insertions, 39 deletions
diff --git a/src/base/pla/module.make b/src/base/pla/module.make
index ab883fef..b34d30d0 100644
--- a/src/base/pla/module.make
+++ b/src/base/pla/module.make
@@ -1,6 +1,8 @@
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
diff --git a/src/base/pla/pla.h b/src/base/pla/pla.h
index bf81f16d..2806df2f 100644
--- a/src/base/pla/pla.h
+++ b/src/base/pla/pla.h
@@ -74,20 +74,33 @@ struct Pla_Man_t_
Vec_Int_t vHashes; // hash values
Vec_Wrd_t vInBits; // input bits
Vec_Wrd_t vOutBits; // output bits
- Vec_Wec_t vLits; // cubes as interger arrays
- Vec_Wec_t vOccurs; // occurent counters for the literals
+ Vec_Wec_t vCubeLits; // cubes as interger arrays
+ Vec_Wec_t vOccurs; // occurence counters for the literals
+ Vec_Int_t vDivs; // divisor definitions
};
+static inline char * Pla_ManName( Pla_Man_t * p ) { return p->pName; }
static inline int Pla_ManInNum( Pla_Man_t * p ) { return p->nIns; }
static inline int Pla_ManOutNum( Pla_Man_t * p ) { return p->nOuts; }
static inline int Pla_ManCubeNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vCubes ); }
+static inline int Pla_ManDivNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vDivs ); }
static inline word * Pla_CubeIn( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vInBits, i * p->nInWords); }
static inline word * Pla_CubeOut( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vOutBits, i * p->nOutWords); }
-static inline int Pla_CubeGetLit( word * p, int k ) { return (int)(p[k>>5] >> ((k<<1) & 63)) & 3; }
-static inline void Pla_CubeSetLit( word * p, int k, Pla_Lit_t d ) { p[k>>5] |= (((word)d)<<((k<<1) & 63)); }
-static inline void Pla_CubeXorLit( word * p, int k, Pla_Lit_t d ) { p[k>>5] ^= (((word)d)<<((k<<1) & 63)); }
+static inline int Pla_CubeNum( int hCube ) { return hCube >> 8; }
+static inline int Pla_CubeLit( int hCube ) { return hCube & 0xFF; }
+static inline int Pla_CubeHandle( int iCube, int iLit ) { assert( !(iCube >> 24) && !(iLit >> 8) ); return iCube << 8 | iLit; }
+
+// read/write/flip i-th bit of a bit string table
+static inline int Pla_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; }
+static inline void Pla_TtSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); }
+static inline void Pla_TtXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); }
+
+// read/write/flip i-th literal in a cube
+static inline int Pla_CubeGetLit( word * p, int i ) { return (int)(p[i>>5] >> ((i<<1) & 63)) & 3; }
+static inline void Pla_CubeSetLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] |= (((word)d)<<((i<<1) & 63)); }
+static inline void Pla_CubeXorLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] ^= (((word)d)<<((i<<1) & 63)); }
////////////////////////////////////////////////////////////////////////
@@ -170,6 +183,23 @@ static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * p
}
return fFound;
}
+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 >> 8);
+ x = x + (x >> 16);
+ x = x + (x >> 32);
+ return (int)(x & 0xFF);
+}
+static inline int Pla_TtCountOnes( word * p, int nWords )
+{
+ int i, Count = 0;
+ for ( i = 0; i < nWords; i++ )
+ Count += Pla_TtCountOnesOne( p[i] );
+ return Count;
+}
/**Function*************************************************************
@@ -202,8 +232,9 @@ static inline void Pla_ManFree( Pla_Man_t * p )
Vec_IntErase( &p->vHashes );
Vec_WrdErase( &p->vInBits );
Vec_WrdErase( &p->vOutBits );
- Vec_WecErase( &p->vLits );
+ Vec_WecErase( &p->vCubeLits );
Vec_WecErase( &p->vOccurs );
+ Vec_IntErase( &p->vDivs );
ABC_FREE( p->pName );
ABC_FREE( p->pSpec );
ABC_FREE( p );
@@ -226,26 +257,33 @@ static inline int Pla_ManLitOutNum( Pla_Man_t * p )
}
static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose )
{
- printf( "%-16s : ", p->pName );
+ printf( "%-16s : ", Pla_ManName(p) );
printf( "In =%4d ", Pla_ManInNum(p) );
printf( "Out =%4d ", Pla_ManOutNum(p) );
printf( "Cube =%8d ", Pla_ManCubeNum(p) );
printf( "LitIn =%8d ", Pla_ManLitInNum(p) );
printf( "LitOut =%8d ", Pla_ManLitOutNum(p) );
+ printf( "Div =%6d ", Pla_ManDivNum(p) );
printf( "\n" );
}
+/*=== 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 );
/*=== plaMan.c ========================================================*/
-extern Pla_Man_t * Pla_ManPrimeDetector( int nVars );
+extern Vec_Bit_t * Pla_ManPrimesTable( int nVars );
+extern Pla_Man_t * Pla_ManPrimesDetector( int nVars );
extern Pla_Man_t * Pla_ManGenerate( int nIns, int nOuts, int nCubes, int fVerbose );
extern void Pla_ManConvertFromBits( Pla_Man_t * p );
extern void Pla_ManConvertToBits( Pla_Man_t * p );
extern int Pla_ManDist1NumTest( Pla_Man_t * p );
/*=== plaMerge.c ========================================================*/
extern int Pla_ManDist1Merge( Pla_Man_t * p );
+/*=== plaSimple.c ========================================================*/
+extern int Pla_ManFxPerformSimple( int nVars );
/*=== plaRead.c ========================================================*/
extern Pla_Man_t * Pla_ReadPla( char * pFileName );
/*=== plaWrite.c ========================================================*/
diff --git a/src/base/pla/plaCom.c b/src/base/pla/plaCom.c
index 5ccfe98b..6d2d4b62 100644
--- a/src/base/pla/plaCom.c
+++ b/src/base/pla/plaCom.c
@@ -359,7 +359,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if ( fPrimes )
- p = Pla_ManPrimeDetector( nInputs );
+ p = Pla_ManPrimesDetector( nInputs );
else
{
Gia_ManRandom( 1 );
@@ -444,12 +444,23 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Pla_Man_t * p = Pla_AbcGetMan(pAbc);
- int c, fVerbose = 0;
+ int c, nVars = 4, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
{
switch ( c )
{
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVars < 0 )
+ goto usage;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -459,18 +470,22 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
+/*
if ( p == NULL )
{
Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
return 0;
}
- Pla_ManHashDist1NumTest( p );
+*/
+ //Pla_ManFxPerformSimple( nVars );
//Pla_ManConvertFromBits( p );
//Pla_ManConvertToBits( p );
+ Pla_ManPerformFxch( p );
return 0;
usage:
- Abc_Print( -2, "usage: |test [-vh]\n" );
+ Abc_Print( -2, "usage: |test [-N num] [-vh]\n" );
Abc_Print( -2, "\t experiments with SOPs\n" );
+ Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/pla/plaFxch.c b/src/base/pla/plaFxch.c
new file mode 100644
index 00000000..fd06b9a5
--- /dev/null
+++ b/src/base/pla/plaFxch.c
@@ -0,0 +1,854 @@
+/**CFile****************************************************************
+
+ FileName [plaFxch.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SOP manager.]
+
+ Synopsis [Scalable SOP transformations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - March 18, 2015.]
+
+ Revision [$Id: plaFxch.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pla.h"
+#include "misc/vec/vecHash.h"
+#include "misc/vec/vecQue.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fxch_Obj_t_ Fxch_Obj_t;
+struct Fxch_Obj_t_
+{
+ unsigned Table : 30;
+ unsigned MarkN : 1;
+ unsigned MarkP : 1;
+ int Next;
+ int Prev;
+ int Cube;
+};
+
+typedef struct Fxch_Man_t_ Fxch_Man_t;
+struct Fxch_Man_t_
+{
+ // user's data
+ Vec_Wec_t vCubes; // cube -> lit
+ // internal data
+ Vec_Wec_t vLits; // lit -> cube
+ Vec_Int_t vRands; // random numbers for each literal
+ Vec_Int_t vCubeLinks; // first link for each cube
+ Fxch_Obj_t * pBins; // hash table (lits -> cube + lit)
+ Hash_IntMan_t * vHash; // divisor hash table
+ Vec_Que_t * vPrio; // priority queue for divisors by weight
+ Vec_Flt_t vWeights; // divisor weights
+ Vec_Wec_t vPairs; // cube pairs for each div
+ Vec_Wrd_t vDivs; // extracted divisors
+ // temporary data
+ Vec_Int_t vCubesS; // cube pairs for single
+ Vec_Int_t vCubesD; // cube pairs for double
+ Vec_Int_t vCube1; // first cube
+ Vec_Int_t vCube2; // second cube
+ // statistics
+ abctime timeStart; // starting time
+ int SizeMask; // hash table mask
+ int nVars; // original problem variables
+ int nLits; // the number of SOP literals
+ int nCompls; // the number of complements
+ int nPairsS; // number of lit pairs
+ int nPairsD; // number of cube pairs
+};
+
+#define Fxch_ManForEachCubeVec( vVec, vCubes, vCube, i ) \
+ for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )
+
+static inline Vec_Int_t * Fxch_ManCube( Fxch_Man_t * p, int hCube ) { return Vec_WecEntry(&p->vCubes, Pla_CubeNum(hCube)); }
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the current state of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fxch_ManWriteBlif( char * pFileName, Vec_Wec_t * vCubes, Vec_Wrd_t * vDivs )
+{
+ // find the number of original variables
+ int nVarsInit = Vec_WrdCountZero(vDivs);
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+ else
+ {
+ char * pLits = "-01?";
+ Vec_Str_t * vStr;
+ Vec_Int_t * vCube;
+ int i, k, Lit;
+ word Div;
+ // comment
+ fprintf( pFile, "# BLIF file written via PLA package in ABC on " );
+ fprintf( pFile, "%s", Extra_TimeStamp() );
+ fprintf( pFile, "\n\n" );
+ // header
+ fprintf( pFile, ".model %s\n", pFileName );
+ fprintf( pFile, ".inputs" );
+ for ( i = 0; i < nVarsInit; i++ )
+ fprintf( pFile, " i%d", i );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, ".outputs o" );
+ fprintf( pFile, "\n" );
+ // SOP header
+ fprintf( pFile, ".names" );
+ for ( i = 0; i < Vec_WrdSize(vDivs); i++ )
+ fprintf( pFile, " i%d", i );
+ fprintf( pFile, " o\n" );
+ // SOP cubes
+ vStr = Vec_StrStart( Vec_WrdSize(vDivs) + 1 );
+ Vec_WecForEachLevel( vCubes, vCube, i )
+ {
+ if ( !Vec_IntSize(vCube) )
+ continue;
+ for ( k = 0; k < Vec_WrdSize(vDivs); k++ )
+ Vec_StrWriteEntry( vStr, k, '-' );
+ Vec_IntForEachEntry( vCube, Lit, k )
+ Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
+ fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) );
+ }
+ Vec_StrFree( vStr );
+ // divisors
+ Vec_WrdForEachEntryStart( vDivs, Div, i, nVarsInit )
+ {
+ int pLits[2] = { (int)(Div & 0xFFFFFFFF), (int)(Div >> 32) };
+ fprintf( pFile, ".names" );
+ fprintf( pFile, " i%d", Abc_Lit2Var(pLits[0]) );
+ fprintf( pFile, " i%d", Abc_Lit2Var(pLits[1]) );
+ fprintf( pFile, " i%d\n", i );
+ fprintf( pFile, "%d%d 1\n", !Abc_LitIsCompl(pLits[0]), !Abc_LitIsCompl(pLits[1]) );
+ }
+ fprintf( pFile, ".end\n\n" );
+ fclose( pFile );
+ printf( "Written BLIF file \"%s\".\n", pFileName );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starting the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fxch_Man_t * Fxch_ManStart( Vec_Wec_t * vCubes, Vec_Wec_t * vLits )
+{
+ Vec_Int_t * vCube; int i, LogSize;
+ Fxch_Man_t * p = ABC_CALLOC( Fxch_Man_t, 1 );
+ p->vCubes = *vCubes;
+ p->vLits = *vLits;
+ p->nVars = Vec_WecSize(vLits)/2;
+ p->nLits = 0;
+ // random numbers
+ Gia_ManRandom( 1 );
+ Vec_IntGrow( &p->vRands, 2*p->nVars );
+ for ( i = 0; i < 2*p->nVars; i++ )
+ Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); // assert( LogSize <= 26 );
+ // create cube links
+ Vec_IntGrow( &p->vCubeLinks, Vec_WecSize(&p->vCubes) );
+ Vec_WecForEachLevel( vCubes, vCube, i )
+ {
+ Vec_IntPush( &p->vCubeLinks, p->nLits+1 );
+ p->nLits += Vec_IntSize(vCube);
+ }
+ assert( Vec_IntSize(&p->vCubeLinks) == Vec_WecSize(&p->vCubes) );
+ // create table
+ LogSize = Abc_Base2Log( p->nLits+1 );
+ assert( LogSize <= 26 );
+ p->SizeMask = (1 << LogSize) - 1;
+ p->pBins = ABC_CALLOC( Fxch_Obj_t, p->SizeMask + 1 );
+ assert( p->nLits+1 < p->SizeMask+1 );
+ // divisor weights and cube pairs
+ Vec_FltGrow( &p->vWeights, 1000 );
+ Vec_FltPush( &p->vWeights, -1 );
+ Vec_WecGrow( &p->vPairs, 1000 );
+ Vec_WecPushLevel( &p->vPairs );
+ // prepare divisors
+ Vec_WrdGrow( &p->vDivs, p->nVars + 1000 );
+ Vec_WrdFill( &p->vDivs, p->nVars, 0 );
+ return p;
+}
+void Fxch_ManStop( Fxch_Man_t * p )
+{
+ Vec_WecErase( &p->vCubes );
+ Vec_WecErase( &p->vLits );
+ Vec_IntErase( &p->vRands );
+ Vec_IntErase( &p->vCubeLinks );
+ Hash_IntManStop( p->vHash );
+ Vec_QueFree( p->vPrio );
+ Vec_FltErase( &p->vWeights );
+ Vec_WecErase( &p->vPairs );
+ Vec_WrdErase( &p->vDivs );
+ Vec_IntErase( &p->vCubesS );
+ Vec_IntErase( &p->vCubesD );
+ Vec_IntErase( &p->vCube1 );
+ Vec_IntErase( &p->vCube2 );
+ ABC_FREE( p->pBins );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Fxch_TabCompare( Fxch_Man_t * p, int hCube1, int hCube2 )
+{
+ Vec_Int_t * vCube1 = Fxch_ManCube( p, hCube1 );
+ Vec_Int_t * vCube2 = Fxch_ManCube( p, hCube2 );
+ if ( !Vec_IntSize(vCube1) || !Vec_IntSize(vCube2) || Vec_IntSize(vCube1) != Vec_IntSize(vCube2) )
+ return 0;
+ Vec_IntClear( &p->vCube1 );
+ Vec_IntClear( &p->vCube2 );
+ Vec_IntAppendSkip( &p->vCube1, vCube1, Pla_CubeLit(hCube1) );
+ Vec_IntAppendSkip( &p->vCube2, vCube2, Pla_CubeLit(hCube2) );
+ return Vec_IntEqual( &p->vCube1, &p->vCube2 );
+}
+static inline void Fxch_CompressCubes( Fxch_Man_t * p, Vec_Int_t * vLit2Cube )
+{
+ int i, hCube, k = 0;
+ Vec_IntForEachEntry( vLit2Cube, hCube, i )
+ if ( Vec_IntSize(Vec_WecEntry(&p->vCubes, hCube)) > 0 )
+ Vec_IntWriteEntry( vLit2Cube, k++, hCube );
+ Vec_IntShrink( vLit2Cube, k );
+}
+static inline int Fxch_CollectSingles( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+ int * pBeg1 = vArr1->pArray;
+ int * pBeg2 = vArr2->pArray;
+ int * pEnd1 = vArr1->pArray + vArr1->nSize;
+ int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ int * pBeg1New = vArr1->pArray;
+ int * pBeg2New = vArr2->pArray;
+ Vec_IntClear( vArr );
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( Pla_CubeNum(*pBeg1) == Pla_CubeNum(*pBeg2) )
+ Vec_IntPushTwo( vArr, *pBeg1, *pBeg2 ), pBeg1++, pBeg2++;
+ else if ( *pBeg1 < *pBeg2 )
+ *pBeg1New++ = *pBeg1++;
+ else
+ *pBeg2New++ = *pBeg2++;
+ }
+ while ( pBeg1 < pEnd1 )
+ *pBeg1New++ = *pBeg1++;
+ while ( pBeg2 < pEnd2 )
+ *pBeg2New++ = *pBeg2++;
+ Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray );
+ Vec_IntShrink( vArr2, pBeg2New - vArr2->pArray );
+ return Vec_IntSize(vArr);
+}
+static inline void Fxch_CollectDoubles( Fxch_Man_t * p, Vec_Int_t * vPairs, Vec_Int_t * vRes, int Lit0, int Lit1 )
+{
+ int i, hCube1, hCube2;
+ Vec_IntClear( vRes );
+ Vec_IntForEachEntryDouble( vPairs, hCube1, hCube2, i )
+ if ( Fxch_TabCompare(p, hCube1, hCube2) &&
+ Vec_IntEntry(Fxch_ManCube(p, hCube1), Pla_CubeLit(hCube1)) == Lit0 &&
+ Vec_IntEntry(Fxch_ManCube(p, hCube2), Pla_CubeLit(hCube2)) == Lit1 )
+ Vec_IntPushTwo( vRes, hCube1, hCube2 );
+ Vec_IntClear( vPairs );
+ // order pairs in the increasing order of the first cube
+ //Vec_IntSortPairs( vRes );
+}
+static inline void Fxch_CompressLiterals2( Vec_Int_t * p, int iInd1, int iInd2 )
+{
+ int i, Lit, k = 0;
+ assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) );
+ if ( iInd2 != -1 )
+ assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) );
+ Vec_IntForEachEntry( p, Lit, i )
+ if ( i != iInd1 && i != iInd2 )
+ Vec_IntWriteEntry( p, k++, Lit );
+ Vec_IntShrink( p, k );
+}
+static inline void Fxch_CompressLiterals( Vec_Int_t * p, int iLit1, int iLit2 )
+{
+ int i, Lit, k = 0;
+ Vec_IntForEachEntry( p, Lit, i )
+ if ( Lit != iLit1 && Lit != iLit2 )
+ Vec_IntWriteEntry( p, k++, Lit );
+ assert( Vec_IntSize(p) == k + 2 );
+ Vec_IntShrink( p, k );
+}
+static inline void Fxch_FilterCubes( Fxch_Man_t * p, Vec_Int_t * vCubesS, int Lit0, int Lit1 )
+{
+ Vec_Int_t * vCube;
+ int i, k, Lit, iCube, n = 0;
+ int fFound0, fFound1;
+ Vec_IntForEachEntry( vCubesS, iCube, i )
+ {
+ vCube = Vec_WecEntry( &p->vCubes, iCube );
+ fFound0 = fFound1 = 0;
+ Vec_IntForEachEntry( vCube, Lit, k )
+ {
+ if ( Lit == Lit0 )
+ fFound0 = 1;
+ else if ( Lit == Lit1 )
+ fFound1 = 1;
+ }
+ if ( fFound0 && fFound1 )
+ Vec_IntWriteEntry( vCubesS, n++, Pla_CubeHandle(iCube, 255) );
+ }
+ Vec_IntShrink( vCubesS, n );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Divisor addition removal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_DivisorAdd( Fxch_Man_t * p, int Lit0, int Lit1, int Weight )
+{
+ int iDiv;
+ assert( Lit0 != Lit1 );
+ if ( Lit0 < Lit1 )
+ iDiv = Hash_Int2ManInsert( p->vHash, Lit0, Lit1, 0 );
+ else
+ iDiv = Hash_Int2ManInsert( p->vHash, Lit1, Lit0, 0 );
+ if ( iDiv == Vec_FltSize(&p->vWeights) )
+ {
+ Vec_FltPush( &p->vWeights, -2 );
+ Vec_WecPushLevel( &p->vPairs );
+ assert( Vec_FltSize(&p->vWeights) == Vec_WecSize(&p->vPairs) );
+ }
+ Vec_FltAddToEntry( &p->vWeights, iDiv, Weight );
+ if ( p->vPrio )
+ {
+ if ( Vec_QueIsMember(p->vPrio, iDiv) )
+ Vec_QueUpdate( p->vPrio, iDiv );
+ else
+ Vec_QuePush( p->vPrio, iDiv );
+ //assert( iDiv < Vec_QueSize(p->vPrio) );
+ }
+ return iDiv;
+}
+void Fxch_DivisorRemove( Fxch_Man_t * p, int Lit0, int Lit1, int Weight )
+{
+ int iDiv;
+ assert( Lit0 != Lit1 );
+ if ( Lit0 < Lit1 )
+ iDiv = *Hash_Int2ManLookup( p->vHash, Lit0, Lit1 );
+ else
+ iDiv = *Hash_Int2ManLookup( p->vHash, Lit1, Lit0 );
+ assert( iDiv > 0 && iDiv < Vec_FltSize(&p->vWeights) );
+ Vec_FltAddToEntry( &p->vWeights, iDiv, -Weight );
+ if ( Vec_QueIsMember(p->vPrio, iDiv) )
+ Vec_QueUpdate( p->vPrio, iDiv );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starting the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Fxch_Obj_t * Fxch_TabBin( Fxch_Man_t * p, int Value ) { return p->pBins + (Value & p->SizeMask); }
+static inline Fxch_Obj_t * Fxch_TabEntry( Fxch_Man_t * p, int i ) { return i ? p->pBins + i : NULL; }
+static inline int Fxch_TabEntryId( Fxch_Man_t * p, Fxch_Obj_t * pEnt ) { assert(pEnt > p->pBins); return pEnt - p->pBins; }
+
+static inline void Fxch_TabMarkPair( Fxch_Man_t * p, int i, int j )
+{
+ Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+ Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+ assert( pI->Next == j );
+ assert( pJ->Prev == i );
+ assert( pI->MarkN == 0 );
+ assert( pI->MarkP == 0 );
+ assert( pJ->MarkN == 0 );
+ assert( pJ->MarkP == 0 );
+ pI->MarkN = 1;
+ pJ->MarkP = 1;
+}
+static inline void Fxch_TabUnmarkPair( Fxch_Man_t * p, int i, int j )
+{
+ Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+ Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+ assert( pI->Next == j );
+ assert( pJ->Prev == i );
+ assert( pI->MarkN == 1 );
+ assert( pI->MarkP == 0 );
+ assert( pJ->MarkN == 0 );
+ assert( pJ->MarkP == 1 );
+ pI->MarkN = 0;
+ pJ->MarkP = 0;
+}
+static inline void Fxch_TabInsertLink( Fxch_Man_t * p, int i, int j, int fSkipCheck )
+{
+ Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+ Fxch_Obj_t * pN = Fxch_TabEntry(p, pI->Next);
+ Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+ //assert( pJ->Cube != 0 );
+ assert( pN->Prev == i );
+ assert( fSkipCheck || pI->MarkN == 0 );
+ assert( fSkipCheck || pN->MarkP == 0 );
+ assert( fSkipCheck || pJ->MarkN == 0 );
+ assert( fSkipCheck || pJ->MarkP == 0 );
+ pJ->Next = pI->Next; pI->Next = j;
+ pJ->Prev = i; pN->Prev = j;
+}
+static inline void Fxch_TabExtractLink( Fxch_Man_t * p, int i, int j )
+{
+ Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+ Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+ Fxch_Obj_t * pN = Fxch_TabEntry(p, pJ->Next);
+ //assert( pJ->Cube != 0 );
+ assert( pI->Next == j );
+ assert( pJ->Prev == i );
+ assert( pN->Prev == j );
+ assert( pI->MarkN == 0 );
+ assert( pJ->MarkP == 0 );
+ assert( pJ->MarkN == 0 );
+ assert( pN->MarkP == 0 );
+ pI->Next = pJ->Next; pJ->Next = 0;
+ pN->Prev = pJ->Prev; pJ->Prev = 0;
+}
+static inline void Fxch_TabInsert( Fxch_Man_t * p, int iLink, int Value, int hCube )
+{
+ int iEnt, iDiv, Lit0, Lit1, fStart = 1;
+ Fxch_Obj_t * pEnt;
+ Fxch_Obj_t * pBin = Fxch_TabBin( p, Value );
+ Fxch_Obj_t * pCell = Fxch_TabEntry( p, iLink );
+ assert( pCell->MarkN == 0 );
+ assert( pCell->MarkP == 0 );
+ assert( pCell->Cube == 0 );
+ pCell->Cube = hCube;
+ if ( pBin->Table == 0 )
+ {
+ pBin->Table = pCell->Next = pCell->Prev = iLink;
+ return;
+ }
+ // find equal cubes
+ for ( iEnt = pBin->Table; iEnt != (int)pBin->Table || fStart; iEnt = pEnt->Next, fStart = 0 )
+ {
+ pEnt = Fxch_TabBin( p, iEnt );
+ if ( pEnt->MarkN || pEnt->MarkP || !Fxch_TabCompare(p, pEnt->Cube, hCube) )
+ continue;
+ Fxch_TabInsertLink( p, iEnt, iLink, 0 );
+ Fxch_TabMarkPair( p, iEnt, iLink );
+ // get literals
+ Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube), Pla_CubeLit(hCube) );
+ Lit1 = Vec_IntEntry( Fxch_ManCube(p, pEnt->Cube), Pla_CubeLit(pEnt->Cube) );
+ // increment divisor weight
+ iDiv = Fxch_DivisorAdd( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) );
+ // add divisor pair
+ assert( iDiv < Vec_WecSize(&p->vPairs) );
+ if ( Lit0 < Lit1 )
+ {
+ Vec_WecPush( &p->vPairs, iDiv, hCube );
+ Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube );
+ }
+ else
+ {
+ Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube );
+ Vec_WecPush( &p->vPairs, iDiv, hCube );
+ }
+ p->nPairsD++;
+ return;
+ }
+ assert( iEnt == (int)pBin->Table );
+ pEnt = Fxch_TabBin( p, iEnt );
+ Fxch_TabInsertLink( p, pEnt->Prev, iLink, 1 );
+}
+static inline void Fxch_TabExtract( Fxch_Man_t * p, int iLink, int Value, int hCube )
+{
+ int Lit0, Lit1;
+ Fxch_Obj_t * pPair = NULL;
+ Fxch_Obj_t * pBin = Fxch_TabBin( p, Value );
+ Fxch_Obj_t * pLink = Fxch_TabEntry( p, iLink );
+ assert( pLink->Cube == hCube );
+ if ( pLink->MarkN )
+ {
+ pPair = Fxch_TabEntry( p, pLink->Next );
+ Fxch_TabUnmarkPair( p, iLink, pLink->Next );
+ }
+ else if ( pLink->MarkP )
+ {
+ pPair = Fxch_TabEntry( p, pLink->Prev );
+ Fxch_TabUnmarkPair( p, pLink->Prev, iLink );
+ }
+ if ( (int)pBin->Table == iLink )
+ pBin->Table = pLink->Next != iLink ? pLink->Next : 0;
+ if ( pLink->Next == iLink )
+ {
+ assert( pLink->Prev == iLink );
+ pLink->Next = pLink->Prev = 0;
+ }
+ else
+ Fxch_TabExtractLink( p, pLink->Prev, iLink );
+ pLink->Cube = 0;
+ if ( pPair == NULL )
+ return;
+ assert( Fxch_TabCompare(p, pPair->Cube, hCube) );
+ // get literals
+ Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube), Pla_CubeLit(hCube) );
+ Lit1 = Vec_IntEntry( Fxch_ManCube(p, pPair->Cube), Pla_CubeLit(pPair->Cube) );
+ // decrement divisor weight
+ Fxch_DivisorRemove( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) );
+ p->nPairsD--;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starting the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fxch_TabSingleDivisors( Fxch_Man_t * p, int iCube, int fAdd )
+{
+ Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube );
+ int i, k, Lit, Lit2;
+ if ( Vec_IntSize(vCube) < 2 )
+ return 0;
+ Vec_IntForEachEntry( vCube, Lit, i )
+ Vec_IntForEachEntryStart( vCube, Lit2, k, i+1 )
+ {
+ assert( Lit < Lit2 );
+ if ( fAdd )
+ Fxch_DivisorAdd( p, Lit, Lit2, 1 ), p->nPairsS++;
+ else
+ Fxch_DivisorRemove( p, Lit, Lit2, 1 ), p->nPairsS--;
+ }
+ return Vec_IntSize(vCube) * (Vec_IntSize(vCube) - 1) / 2;
+}
+int Fxch_TabDoubleDivisors( Fxch_Man_t * p, int iCube, int fAdd )
+{
+ Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube );
+ int iLinkFirst = Vec_IntEntry( &p->vCubeLinks, iCube );
+ int k, Lit, Value = 0;
+ Vec_IntForEachEntry( vCube, Lit, k )
+ Value += Vec_IntEntry(&p->vRands, Lit);
+ Vec_IntForEachEntry( vCube, Lit, k )
+ {
+ Value -= Vec_IntEntry(&p->vRands, Lit);
+ if ( fAdd )
+ Fxch_TabInsert( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) );
+ else
+ Fxch_TabExtract( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) );
+ Value += Vec_IntEntry(&p->vRands, Lit);
+ }
+ return 1;
+}
+void Fxch_ManCreateDivisors( Fxch_Man_t * p )
+{
+ float Weight; int i;
+ // alloc hash table
+ assert( p->vHash == NULL );
+ p->vHash = Hash_IntManStart( 1000 );
+ // create single-cube two-literal divisors
+ for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ )
+ Fxch_TabSingleDivisors( p, i, 1 ); // add - no update
+ // create two-cube divisors
+ for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ )
+ Fxch_TabDoubleDivisors( p, i, 1 ); // add - no update
+ // create queue with all divisors
+ p->vPrio = Vec_QueAlloc( Vec_FltSize(&p->vWeights) );
+ Vec_QueSetPriority( p->vPrio, Vec_FltArrayP(&p->vWeights) );
+ Vec_FltForEachEntry( &p->vWeights, Weight, i )
+ if ( Weight > 0.0 )
+ Vec_QuePush( p->vPrio, i );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Updates the data-structure when one divisor is selected.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fxch_ManUpdate( Fxch_Man_t * p, int iDiv )
+{
+ Vec_Int_t * vCube1, * vCube2, * vLitP, * vLitN;
+ int nLitsNew = p->nLits - (int)Vec_FltEntry(&p->vWeights, iDiv);
+ int i, Lit0, Lit1, hCube1, hCube2, iVarNew;
+ //float Diff = Vec_FltEntry(&p->vWeights, iDiv) - (float)((int)Vec_FltEntry(&p->vWeights, iDiv));
+ //assert( Diff > 0.0 && Diff < 1.0 );
+
+ // get the divisor and select pivot variables
+ Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF );
+ Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF );
+ Lit0 = Hash_IntObjData0( p->vHash, iDiv );
+ Lit1 = Hash_IntObjData1( p->vHash, iDiv );
+ assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 );
+ Vec_WrdPush( &p->vDivs, ((word)Lit1 << 32) | (word)Lit0 );
+
+ // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
+ // although it is not strictly correct, it seems to be fine to just skip such divisors
+// if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->vHash, iDiv)) == 2 )
+// return;
+
+ // collect single-cube-divisor cubes
+ vLitP = Vec_WecEntry(&p->vLits, Lit0);
+ vLitN = Vec_WecEntry(&p->vLits, Lit1);
+ Fxch_CompressCubes( p, vLitP );
+ Fxch_CompressCubes( p, vLitN );
+// Fxch_CollectSingles( vLitP, vLitN, &p->vCubesS );
+// assert( Vec_IntSize(&p->vCubesS) % 2 == 0 );
+ Vec_IntTwoRemoveCommon( vLitP, vLitN, &p->vCubesS );
+ Fxch_FilterCubes( p, &p->vCubesS, Lit0, Lit1 );
+
+ // collect double-cube-divisor cube pairs
+ Fxch_CollectDoubles( p, Vec_WecEntry(&p->vPairs, iDiv), &p->vCubesD, Abc_LitNot(Lit0), Abc_LitNot(Lit1) );
+ assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
+ Vec_IntUniqifyPairs( &p->vCubesD );
+ assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
+
+ // subtract cost of single-cube divisors
+// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+ Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+ Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ); // remove - update
+ Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+ Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ), // remove - update
+ Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube2), 0 ); // remove - update
+
+ // subtract cost of double-cube divisors
+// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+ Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+ {
+ //printf( "%d ", Pla_CubeNum(hCube1) );
+ Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ); // remove - update
+ }
+ //printf( "\n" );
+
+ Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+ {
+ //printf( "%d ", Pla_CubeNum(hCube1) );
+ //printf( "%d ", Pla_CubeNum(hCube2) );
+ Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ), // remove - update
+ Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube2), 0 ); // remove - update
+ }
+ //printf( "\n" );
+
+ // create new literals
+ p->nLits += 2;
+ iVarNew = Vec_WecSize( &p->vLits ) / 2;
+ vLitP = Vec_WecPushLevel( &p->vLits );
+ vLitN = Vec_WecPushLevel( &p->vLits );
+ vLitP = Vec_WecEntry( &p->vLits, Vec_WecSize(&p->vLits) - 2 );
+ // update single-cube divisor cubes
+// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+ Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+ {
+// int Lit0s, Lit1s;
+ vCube1 = Fxch_ManCube( p, hCube1 );
+// Lit0s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube1));
+// Lit1s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube2));
+// assert( Pla_CubeNum(hCube1) == Pla_CubeNum(hCube2) );
+// assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Lit0 );
+// assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube2)) == Lit1 );
+ Fxch_CompressLiterals( vCube1, Lit0, Lit1 );
+// Vec_IntPush( vLitP, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
+ Vec_IntPush( vLitP, Pla_CubeNum(hCube1) );
+ Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 0) );
+
+ //if ( Pla_CubeNum(hCube1) == 3 )
+ // printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
+
+ p->nLits--;
+ }
+ // update double-cube divisor cube pairs
+ Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+ {
+ vCube1 = Fxch_ManCube( p, hCube1 );
+ vCube2 = Fxch_ManCube( p, hCube2 );
+ assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Abc_LitNot(Lit0) );
+ assert( Vec_IntEntry(vCube2, Pla_CubeLit(hCube2)) == Abc_LitNot(Lit1) );
+ Fxch_CompressLiterals2( vCube1, Pla_CubeLit(hCube1), -1 );
+// Vec_IntPush( vLitN, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
+ Vec_IntPush( vLitN, Pla_CubeNum(hCube1) );
+ Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 1) );
+ p->nLits -= Vec_IntSize(vCube2);
+
+ //if ( Pla_CubeNum(hCube1) == 3 )
+ // printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
+
+ // remove second cube
+ Vec_IntClear( vCube2 );
+ }
+ Vec_IntSort( vLitN, 0 );
+ Vec_IntSort( vLitP, 0 );
+
+ // add cost of single-cube divisors
+// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+ Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+ Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update
+ Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+ Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update
+
+ // add cost of double-cube divisors
+// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+ Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+ Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update
+ Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+ Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update
+
+ // check predicted improvement: (new SOP lits == old SOP lits - divisor weight)
+ //assert( p->nLits == nLitsNew );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the improved fast_extract algorithm.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Fxch_PrintStats( Fxch_Man_t * p, abctime clk )
+{
+ printf( "Num =%6d ", Vec_WrdSize(&p->vDivs) - p->nVars );
+ printf( "Cubes =%8d ", Vec_WecSizeUsed(&p->vCubes) );
+ printf( "Lits =%8d ", p->nLits );
+ printf( "Divs =%8d ", Hash_IntManEntryNum(p->vHash) );
+ printf( "Divs+ =%8d ", Vec_QueSize(p->vPrio) );
+ printf( "PairS =%6d ", p->nPairsS );
+ printf( "PairD =%6d ", p->nPairsD );
+ Abc_PrintTime( 1, "Time", clk );
+// printf( "\n" );
+}
+static inline void Fxch_PrintDivOne( Fxch_Man_t * p, int iDiv )
+{
+ int i;
+ int Lit0 = Hash_IntObjData0( p->vHash, iDiv );
+ int Lit1 = Hash_IntObjData1( p->vHash, iDiv );
+ assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 );
+ printf( "Div %4d : ", iDiv );
+ printf( "Weight %12.5f ", Vec_FltEntry(&p->vWeights, iDiv) );
+ printf( "Pairs = %5d ", Vec_IntSize(Vec_WecEntry(&p->vPairs, iDiv))/2 );
+ for ( i = 0; i < Vec_WrdSize(&p->vDivs); i++ )
+ {
+ if ( i == Abc_Lit2Var(Lit0) )
+ printf( "%d", !Abc_LitIsCompl(Lit0) );
+ else if ( i == Abc_Lit2Var(Lit1) )
+ printf( "%d", !Abc_LitIsCompl(Lit1) );
+ else
+ printf( "-" );
+ }
+ printf( "\n" );
+}
+static void Fxch_PrintDivisors( Fxch_Man_t * p )
+{
+ int iDiv;
+ for ( iDiv = 1; iDiv < Vec_FltSize(&p->vWeights); iDiv++ )
+ Fxch_PrintDivOne( p, iDiv );
+ printf( "\n" );
+}
+
+int Fxch_ManFastExtract( Fxch_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ int nNewNodesMax = ABC_INFINITY;
+ abctime clk = Abc_Clock();
+ int i, iDiv;
+ Fxch_ManCreateDivisors( p );
+// Fxch_PrintDivisors( p );
+ if ( fVerbose )
+ Fxch_PrintStats( p, Abc_Clock() - clk );
+ p->timeStart = Abc_Clock();
+ for ( i = 0; i < nNewNodesMax && Vec_QueTopPriority(p->vPrio) > 0.0; i++ )
+ {
+ iDiv = Vec_QuePop(p->vPrio);
+ //if ( fVerbose )
+ // Fxch_PrintStats( p, Abc_Clock() - clk );
+ if ( fVeryVerbose )
+ Fxch_PrintDivOne( p, iDiv );
+ Fxch_ManUpdate( p, iDiv );
+ }
+ if ( fVerbose )
+ Fxch_PrintStats( p, Abc_Clock() - clk );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the improved fast_extract algorithm.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pla_ManPerformFxch( Pla_Man_t * p )
+{
+ char pFileName[1000];
+ Fxch_Man_t * pFxch;
+ Pla_ManConvertFromBits( p );
+ pFxch = Fxch_ManStart( &p->vCubeLits, &p->vOccurs );
+ Vec_WecZero( &p->vCubeLits );
+ Vec_WecZero( &p->vOccurs );
+ Fxch_ManFastExtract( pFxch, 1, 0 );
+ sprintf( pFileName, "%s.blif", Pla_ManName(p) );
+ //Fxch_ManWriteBlif( pFileName, &pFxch->vCubes, &pFxch->vDivs );
+ Fxch_ManStop( pFxch );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/pla/plaHash.c b/src/base/pla/plaHash.c
index d05bd9c9..b51ba4c1 100644
--- a/src/base/pla/plaHash.c
+++ b/src/base/pla/plaHash.c
@@ -63,7 +63,7 @@ static unsigned s_PlaHashValues[PLA_HASH_VALUE_NUM] =
0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d
};
-static inline int Pla_HashValue( int i ) { assert( i >= 0 && i < PLA_HASH_VALUE_NUM ); return s_PlaHashValues[i] & 0xFFFFFF; }
+static inline int Pla_HashValue( int i ) { assert( i >= 0 && i < PLA_HASH_VALUE_NUM ); return s_PlaHashValues[i] & 0x3FFFFFF; }
#define PLA_LIT_UNUSED 0xFFFF
@@ -107,7 +107,7 @@ static inline Tab_Obj_t * Tab_ManEntry( Tab_Man_t * p, int i ) { return i ? p
static inline Tab_Man_t * Tab_ManAlloc( int LogSize, Pla_Man_t * pMan )
{
Tab_Man_t * p = ABC_CALLOC( Tab_Man_t, 1 );
- assert( LogSize >= 4 && LogSize <= 24 );
+ assert( LogSize >= 4 && LogSize <= 26 );
p->SizeMask = (1 << LogSize) - 1;
p->pBins = ABC_CALLOC( Tab_Obj_t, p->SizeMask + 1 );
p->nBins = 1;
@@ -119,11 +119,12 @@ static inline void Tab_ManFree( Tab_Man_t * p )
ABC_FREE( p->pBins );
ABC_FREE( p );
}
-static inline void Tab_ManHashInsert( Tab_Man_t * p, int Value, int iCube )
+static inline void Tab_ManHashInsert( Tab_Man_t * p, int Value, int iCube, int iVar )
{
Tab_Obj_t * pBin = Tab_ManBin( p, Value );
Tab_Obj_t * pCell = p->pBins + p->nBins;
pCell->Cube = iCube;
+ pCell->VarA = iVar;
pCell->Next = pBin->Table;
pBin->Table = p->nBins++;
}
@@ -131,10 +132,17 @@ static inline int Tab_ManHashLookup( Tab_Man_t * p, int Value, Vec_Int_t * vCube
{
Tab_Obj_t * pEnt, * pBin = Tab_ManBin( p, Value );
for ( pEnt = Tab_ManEntry(p, pBin->Table); pEnt; pEnt = Tab_ManEntry(p, pEnt->Next) )
- if ( Vec_IntEqual( Vec_WecEntry(&p->pMan->vLits, pEnt->Cube), vCube ) )
+ if ( Vec_IntEqual( Vec_WecEntry(&p->pMan->vCubeLits, pEnt->Cube), vCube ) )
return 1;
return 0;
}
+static inline void Tab_ManHashCollect( Tab_Man_t * p, int iBin, Vec_Int_t * vEntries )
+{
+ Tab_Obj_t * pEnt, * pBin = Tab_ManBin( p, iBin );
+ Vec_IntClear( vEntries );
+ for ( pEnt = Tab_ManEntry(p, pBin->Table); pEnt; pEnt = Tab_ManEntry(p, pEnt->Next) )
+ Vec_IntPushTwo( vEntries, pEnt->Cube, pEnt->VarA );
+}
/**Function*************************************************************
@@ -160,11 +168,11 @@ void Pla_ManHashCubes( Pla_Man_t * p, Tab_Man_t * pTab )
Vec_Int_t * vCube; int i, Value;
Vec_IntClear( &p->vHashes );
Vec_IntGrow( &p->vHashes, Pla_ManCubeNum(p) );
- Vec_WecForEachLevel( &p->vLits, vCube, i )
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
{
Value = Pla_CubeHashValue(vCube);
Vec_IntPush( &p->vHashes, Value );
- Tab_ManHashInsert( pTab, Value, i );
+ Tab_ManHashInsert( pTab, Value, i, PLA_LIT_UNUSED );
}
}
int Pla_ManHashDistance1( Pla_Man_t * p )
@@ -174,11 +182,11 @@ int Pla_ManHashDistance1( Pla_Man_t * p )
Vec_Int_t * vCubeCopy = Vec_IntAlloc( p->nIns );
int nBits = Abc_Base2Log( Pla_ManCubeNum(p) ) + 2;
int i, k, Lit, Value, ValueCopy, Count = 0;
- assert( nBits <= 24 );
+ assert( nBits <= 26 );
pTab = Tab_ManAlloc( nBits, p );
Pla_ManConvertFromBits( p );
Pla_ManHashCubes( p, pTab );
- Vec_WecForEachLevel( &p->vLits, vCube, i )
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
{
Vec_IntClear( vCubeCopy );
Vec_IntAppend( vCubeCopy, vCube );
@@ -210,6 +218,126 @@ int Pla_ManHashDist1NumTest( Pla_Man_t * p )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pla_PrintCube( Vec_Int_t * vLits, int nVars, int iVar )
+{
+ int v, Lit;
+ Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
+ Vec_StrFill( vStr, nVars, '-' );
+ Vec_IntForEachEntry( vLits, Lit, v )
+ Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
+ fprintf( stdout, "%s %d\n", Vec_StrArray(vStr), iVar );
+ Vec_StrFree( vStr );
+}
+void Pla_ManHashCubes2( Pla_Man_t * p, Tab_Man_t * pTab )
+{
+ Vec_Int_t * vCube;
+ int i, v, Lit, Value;
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
+ {
+ Value = Pla_CubeHashValue(vCube);
+ Vec_IntForEachEntry( vCube, Lit, v )
+ {
+ Value -= Pla_HashValue(Lit);
+ Tab_ManHashInsert( pTab, Value, i, v );
+ Value += Pla_HashValue(Lit);
+ }
+ }
+}
+void Vec_IntCopySkip( Vec_Int_t * vCube, int iVar, Vec_Int_t * vRes )
+{
+ int i;
+ Vec_IntClear( vRes );
+ for ( i = 0; i < Vec_IntSize(vCube); i++ )
+ if ( i != iVar )
+ Vec_IntPush( vRes, Vec_IntEntry(vCube, i) );
+}
+Vec_Int_t * Pla_ManComputeDistance1Int( Pla_Man_t * p )
+{
+ Tab_Man_t * pTab;
+ Vec_Int_t * vCube1, * vCube2;
+ Vec_Int_t * vTemp1 = Vec_IntAlloc( 100 );
+ Vec_Int_t * vTemp2 = Vec_IntAlloc( 100 );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vCounts = Vec_IntStart( Vec_WecSize(&p->vCubeLits) );
+ Vec_Int_t * vEntries = Vec_IntAlloc( p->nIns );
+ int nBits = Abc_Base2Log( Vec_WecSizeSize(&p->vCubeLits) ) + 2;
+ int v, i, k, Count = 0;
+ int iCube1, iCube2, iVar1, iVar2;
+ assert( nBits <= 26 );
+ pTab = Tab_ManAlloc( nBits, p );
+ //Pla_ManConvertFromBits( p );
+ Pla_ManHashCubes2( p, pTab );
+ // iterate through the hash bins
+ for ( v = 0; v <= pTab->SizeMask; v++ )
+ {
+ Tab_ManHashCollect( pTab, v, vEntries );
+ for ( i = 0; i < Vec_IntSize(vEntries)/2; i++ )
+ for ( k = i+1; k < Vec_IntSize(vEntries)/2; k++ )
+ {
+ iCube1 = Vec_IntEntry(vEntries, 2*i);
+ iCube2 = Vec_IntEntry(vEntries, 2*k);
+ iVar1 = Vec_IntEntry(vEntries, 2*i+1);
+ iVar2 = Vec_IntEntry(vEntries, 2*k+1);
+
+ vCube1 = Vec_WecEntry(&p->vCubeLits, iCube1);
+ vCube2 = Vec_WecEntry(&p->vCubeLits, iCube2);
+/*
+ Pla_PrintCube( vCube1, p->nIns, iVar1 );
+ Pla_PrintCube( vCube2, p->nIns, iVar2 );
+ printf( "\n" );
+*/
+ if ( Vec_IntSize(vCube1) != Vec_IntSize(vCube2) )
+ continue;
+ Vec_IntCopySkip( vCube1, iVar1, vTemp1 );
+ Vec_IntCopySkip( vCube2, iVar2, vTemp2 );
+ if ( !Vec_IntEqual( vTemp1, vTemp2 ) )
+ continue;
+
+ printf( "%d %d ", iCube1, iCube2 );
+
+ Vec_IntPushTwo( vPairs, iCube1, iVar1 );
+ Vec_IntPushTwo( vPairs, iCube2, iVar2 );
+
+ Vec_IntAddToEntry( vCounts, iCube1, 1 );
+ Vec_IntAddToEntry( vCounts, iCube2, 1 );
+ }
+ }
+ Vec_IntPrint( vCounts );
+
+ Vec_IntFree( vCounts );
+ Vec_IntFree( vTemp1 );
+ Vec_IntFree( vTemp2 );
+ Vec_IntFree( vEntries );
+ Tab_ManFree( pTab );
+ return vPairs;
+}
+Vec_Int_t * Pla_ManComputeDistance1( Pla_Man_t * p )
+{
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vPairs = Pla_ManComputeDistance1Int( p );
+ printf( "Found %d pairs among %d cubes using cube hashing. ", Vec_IntSize(vPairs)/4, Pla_ManCubeNum(p) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return vPairs;
+}
+void Pla_ManComputeDist1Test( Pla_Man_t * p )
+{
+ Vec_Int_t * vPairs;
+ Pla_ManConvertFromBits( p );
+ vPairs = Pla_ManComputeDistance1( p );
+ Vec_IntFree( vPairs );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/pla/plaMan.c b/src/base/pla/plaMan.c
index bc3cd8ad..23ea8368 100644
--- a/src/base/pla/plaMan.c
+++ b/src/base/pla/plaMan.c
@@ -41,19 +41,28 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Vec_Int_t * Pla_GenPrimes( int nVars )
+Vec_Bit_t * Pla_ManPrimesTable( int nVars )
{
- int i, n, nBits = ( 1 << nVars );
- Vec_Bit_t * vMap = Vec_BitStart( nBits );
- Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 );
- Vec_BitWriteEntry(vMap, 0, 1);
- Vec_BitWriteEntry(vMap, 1, 1);
+ int i, n, nBits = 1 << nVars;
+ Vec_Bit_t * vMap = Vec_BitStartFull( Abc_MaxInt(64, nBits) );
+ for ( i = nBits; i < 64; i++ )
+ Vec_BitWriteEntry( vMap, i, 0 );
+ Vec_BitShrink( vMap, nBits );
+ Vec_BitWriteEntry( vMap, 0, 0 );
+ Vec_BitWriteEntry( vMap, 1, 0 );
for ( n = 2; n < nBits; n++ )
- if ( !Vec_BitEntry(vMap, n) )
+ if ( Vec_BitEntry(vMap, n) )
for ( i = 2*n; i < nBits; i += n )
- Vec_BitWriteEntry(vMap, i, 1);
+ Vec_BitWriteEntry( vMap, i, 0 );
+ return vMap;
+}
+Vec_Int_t * Pla_GenPrimes( int nVars )
+{
+ int n, nBits = ( 1 << nVars );
+ Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 );
+ Vec_Bit_t * vMap = Pla_ManPrimesTable( nVars );
for ( n = 2; n < nBits; n++ )
- if ( !Vec_BitEntry(vMap, n) )
+ if ( Vec_BitEntry(vMap, n) )
Vec_IntPush( vPrimes, n );
printf( "Primes up to 2^%d = %d\n", nVars, Vec_IntSize(vPrimes) );
// Abc_GenCountHits1( vMap, vPrimes, nVars );
@@ -75,7 +84,7 @@ Pla_Man_t * Pla_GenFromMinterms( char * pName, Vec_Int_t * vMints, int nVars )
Pla_CubeSetLit( pCube, 0, PLA_LIT_ONE );
return p;
}
-Pla_Man_t * Pla_ManPrimeDetector( int nVars )
+Pla_Man_t * Pla_ManPrimesDetector( int nVars )
{
char pName[1000];
Pla_Man_t * p;
@@ -117,10 +126,13 @@ Vec_Bit_t * Pla_GenRandom( int nVars, int nNums, int fNonZero )
}
Pla_Man_t * Pla_ManGenerate( int nInputs, int nOutputs, int nCubes, int fVerbose )
{
+ Pla_Man_t * p;
Vec_Bit_t * vBits;
int i, k, Count;
word * pCube;
- Pla_Man_t * p = Pla_ManAlloc( "rand", nInputs, nOutputs, nCubes );
+ char Buffer[1000];
+ sprintf( Buffer, "%s_%d_%d_%d", "rand", nInputs, nOutputs, nCubes );
+ p = Pla_ManAlloc( Buffer, nInputs, nOutputs, nCubes );
// generate nCube random input minterms
vBits = Pla_GenRandom( nInputs, nCubes, 0 );
for ( i = Count = 0; i < Vec_BitSize(vBits); i++ )
@@ -167,26 +179,40 @@ Pla_Man_t * Pla_ManGenerate( int nInputs, int nOutputs, int nCubes, int fVerbose
***********************************************************************/
void Pla_ManConvertFromBits( Pla_Man_t * p )
{
- word * pCube; int i, k, Lit;
- Vec_WecClear( &p->vLits );
+ Vec_Int_t * vCube;
+ word * pCube; int i, k, Lit, Count;
+ Vec_WecClear( &p->vCubeLits );
Vec_WecClear( &p->vOccurs );
- Vec_WecInit( &p->vLits, Pla_ManCubeNum(p) );
+ Vec_WecInit( &p->vCubeLits, Pla_ManCubeNum(p) );
Vec_WecInit( &p->vOccurs, 2*Pla_ManInNum(p) );
Pla_ForEachCubeIn( p, pCube, i )
+ {
+ vCube = Vec_WecEntry( &p->vCubeLits, i );
+
+ Count = 0;
+ Pla_CubeForEachLitIn( p, pCube, Lit, k )
+ if ( Lit != PLA_LIT_DASH )
+ Count++;
+ Vec_IntGrow( vCube, Count );
+
+ Count = 0;
Pla_CubeForEachLitIn( p, pCube, Lit, k )
if ( Lit != PLA_LIT_DASH )
{
Lit = Abc_Var2Lit( k, Lit == PLA_LIT_ZERO );
- Vec_WecPush( &p->vLits, i, Lit );
+ Vec_WecPush( &p->vCubeLits, i, Lit );
+// Vec_WecPush( &p->vOccurs, Lit, Pla_CubeHandle(i, Count++) );
Vec_WecPush( &p->vOccurs, Lit, i );
}
+ assert( Vec_IntSize(vCube) == Vec_IntCap(vCube) );
+ }
}
void Pla_ManConvertToBits( Pla_Man_t * p )
{
Vec_Int_t * vCube; int i, k, Lit;
- Vec_IntFillNatural( &p->vCubes, Vec_WecSize(&p->vLits) );
+ Vec_IntFillNatural( &p->vCubes, Vec_WecSize(&p->vCubeLits) );
Vec_WrdFill( &p->vInBits, Pla_ManCubeNum(p) * p->nInWords, 0 );
- Vec_WecForEachLevel( &p->vLits, vCube, i )
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
Vec_IntForEachEntry( vCube, Lit, k )
Pla_CubeSetLit( Pla_CubeIn(p, i), Abc_Lit2Var(Lit), Abc_LitIsCompl(Lit) ? PLA_LIT_ZERO : PLA_LIT_ONE );
}
diff --git a/src/base/pla/plaSimple.c b/src/base/pla/plaSimple.c
new file mode 100644
index 00000000..8fea5c1f
--- /dev/null
+++ b/src/base/pla/plaSimple.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+ FileName [plaSimple.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SOP manager.]
+
+ Synopsis [Scalable SOP transformations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - March 18, 2015.]
+
+ Revision [$Id: plaSimple.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pla.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Dump PLA manager into a BLIF file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pla_ManDumpPla( Pla_Man_t * p, char * pFileName )
+{
+ // find the number of original variables
+ int nVarsInit = Pla_ManDivNum(p) ? Vec_IntCountZero(&p->vDivs) : Pla_ManInNum(p);
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+ else
+ {
+ char * pLits = "-01?";
+ Vec_Str_t * vStr;
+ Vec_Int_t * vCube;
+ int i, k, Lit;
+ // comment
+ fprintf( pFile, "# PLA file written via PLA package in ABC on " );
+ fprintf( pFile, "%s", Extra_TimeStamp() );
+ fprintf( pFile, "\n\n" );
+ // header
+ fprintf( pFile, ".i %d\n", Pla_ManInNum(p) );
+ fprintf( pFile, ".o %d\n", 1 );
+ fprintf( pFile, ".p %d\n", Vec_WecSize(&p->vCubeLits) );
+ // SOP
+ vStr = Vec_StrStart( Pla_ManInNum(p) + 1 );
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
+ {
+ if ( !Vec_IntSize(vCube) )
+ continue;
+ for ( k = 0; k < Pla_ManInNum(p); k++ )
+ Vec_StrWriteEntry( vStr, k, '-' );
+ Vec_IntForEachEntry( vCube, Lit, k )
+ Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
+ fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) );
+ }
+ Vec_StrFree( vStr );
+ fprintf( pFile, ".e\n\n" );
+ fclose( pFile );
+ printf( "Written file \"%s\".\n", pFileName );
+ }
+}
+void Pla_ManDumpBlif( Pla_Man_t * p, char * pFileName )
+{
+ // find the number of original variables
+ int nVarsInit = Pla_ManDivNum(p) ? Vec_IntCountZero(&p->vDivs) : Pla_ManInNum(p);
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+ else
+ {
+ char * pLits = "-01?";
+ Vec_Str_t * vStr;
+ Vec_Int_t * vCube;
+ int i, k, Lit, Div;
+ // comment
+ fprintf( pFile, "# BLIF file written via PLA package in ABC on " );
+ fprintf( pFile, "%s", Extra_TimeStamp() );
+ fprintf( pFile, "\n\n" );
+ // header
+ fprintf( pFile, ".model %s\n", Pla_ManName(p) );
+ fprintf( pFile, ".inputs" );
+ for ( i = 0; i < nVarsInit; i++ )
+ fprintf( pFile, " i%d", i );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, ".outputs o" );
+ fprintf( pFile, "\n" );
+ // SOP
+ fprintf( pFile, ".names" );
+ for ( i = 0; i < Pla_ManInNum(p); i++ )
+ fprintf( pFile, " i%d", i );
+ fprintf( pFile, " o\n" );
+ vStr = Vec_StrStart( Pla_ManInNum(p) + 1 );
+ Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
+ {
+ for ( k = 0; k < Pla_ManInNum(p); k++ )
+ Vec_StrWriteEntry( vStr, k, '-' );
+ Vec_IntForEachEntry( vCube, Lit, k )
+ Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
+ fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) );
+ }
+ Vec_StrFree( vStr );
+ // divisors
+ Vec_IntForEachEntryStart( &p->vDivs, Div, i, nVarsInit )
+ {
+ int pLits[3] = { (Div >> 2) & 0x3FF, (Div >> 12) & 0x3FF, (Div >> 22) & 0x3FF };
+ fprintf( pFile, ".names" );
+ fprintf( pFile, " i%d", Abc_Lit2Var(pLits[0]) );
+ fprintf( pFile, " i%d", Abc_Lit2Var(pLits[1]) );
+ if ( (Div & 3) == 3 ) // MUX
+ fprintf( pFile, " i%d", Abc_Lit2Var(pLits[2]) );
+ fprintf( pFile, " i%d\n", i );
+ if ( (Div & 3) == 1 ) // AND
+ fprintf( pFile, "%d%d 1\n", !Abc_LitIsCompl(pLits[0]), !Abc_LitIsCompl(pLits[1]) );
+ else if ( (Div & 3) == 2 ) // XOR
+ {
+ assert( !Abc_LitIsCompl(pLits[0]) );
+ assert( !Abc_LitIsCompl(pLits[1]) );
+ fprintf( pFile, "10 1\n01 1\n" );
+ }
+ else if ( (Div & 3) == 3 ) // MUX
+ {
+ assert( !Abc_LitIsCompl(pLits[1]) );
+ assert( !Abc_LitIsCompl(pLits[2]) );
+ fprintf( pFile, "%d-0 1\n-11 1\n", !Abc_LitIsCompl(pLits[0]) );
+ }
+ else assert( 0 );
+ }
+ fprintf( pFile, ".end\n\n" );
+ fclose( pFile );
+ printf( "Written file \"%s\".\n", pFileName );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms truth table into an SOP manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pla_ManExpendDirNum( word * pOn, int nBits, int iMint, int * pVars )
+{
+ int v, nVars = 0;
+ for ( v = 0; v < nBits; v++ )
+ if ( Pla_TtGetBit(pOn, iMint ^ (1 << v)) )
+ pVars[nVars++] = v;
+ return nVars;
+}
+void Pla_PrintBinary( word * pT, int nBits )
+{
+ int v;
+ for ( v = 0; v < nBits; v++ )
+ printf( "%d", Pla_TtGetBit(pT, v) );
+ printf( "\n" );
+}
+Vec_Wrd_t * Pla_ManFxMinimize( word * pOn, int nVars )
+{
+ int i, v, iMint, iVar, nMints = (1 << nVars);
+ int nWords = Abc_Bit6WordNum( nMints );
+ Vec_Wrd_t * vCubes = Vec_WrdAlloc( 1000 );
+ word * pDc = ABC_CALLOC( word, nWords );
+ int Count[32] = {0};
+ int Cubes[32] = {0};
+ Vec_Int_t * vStore = Vec_IntAlloc( 1000 );
+
+ // count the number of expansion directions
+ for ( i = 0; i < nMints; i++ )
+ if ( Pla_TtGetBit(pOn, i) && !Pla_TtGetBit(pDc, i) )
+ {
+ int pDirs[32], nDirs = Pla_ManExpendDirNum(pOn, nVars, i, pDirs);
+ Count[nDirs]++;
+ if ( nDirs == 0 )
+ {
+ Pla_TtSetBit(pDc, i);
+ Cubes[0]++;
+ // save
+ Vec_IntPushTwo( vStore, i, -1 );
+ continue;
+ }
+ if ( nDirs == 1 )
+ {
+ //Pla_PrintBinary( (word *)&i, nVars );
+ //printf( " %d \n", pDirs[0] );
+
+ Pla_TtSetBit(pDc, i);
+ Pla_TtSetBit(pDc, i ^ (1 << pDirs[0]));
+ Cubes[1]++;
+ // save
+ Vec_IntPushTwo( vStore, i, pDirs[0] );
+ continue;
+ }
+ if ( nDirs == 2 && Pla_TtGetBit(pOn, i ^ (1 << pDirs[0]) ^ (1 << pDirs[1])) )
+ {
+ assert( 0 );
+ Pla_TtSetBit(pDc, i);
+ Pla_TtSetBit(pDc, i ^ (1 << pDirs[0]));
+ Pla_TtSetBit(pDc, i ^ (1 << pDirs[1]));
+ Pla_TtSetBit(pDc, i ^ (1 << pDirs[0]) ^ (1 << pDirs[1]));
+ Cubes[2]++;
+ continue;
+ }
+ }
+
+ // go through the remaining cubes
+ for ( i = 0; i < nMints; i++ )
+ if ( Pla_TtGetBit(pOn, i) && !Pla_TtGetBit(pDc, i) )
+ {
+ int pDirs[32], nDirs = Pla_ManExpendDirNum(pOn, nVars, i, pDirs);
+ // find direction, which is not taken
+ for ( v = 0; v < nDirs; v++ )
+ if ( Pla_TtGetBit(pOn, i ^ (1 << pDirs[v])) && !Pla_TtGetBit(pDc, i ^ (1 << pDirs[v])) )
+ break;
+ // if there is no open directions, use any one
+ if ( v == nDirs )
+ v = 0;
+ // mark this one
+ Pla_TtSetBit(pDc, i);
+ Pla_TtSetBit(pDc, i ^ (1 << pDirs[v]));
+ Cubes[10]++;
+ // save
+ Vec_IntPushTwo( vStore, i, pDirs[v] );
+ continue;
+ }
+
+ printf( "\n" );
+ printf( "Truth = %d. ", Pla_TtCountOnes(pOn, nWords) );
+ printf( "Cover = %d. ", Pla_TtCountOnes(pDc, nWords) );
+ printf( "\n" );
+
+ printf( "Count: " );
+ for ( i = 0; i < 16; i++ )
+ if ( Count[i] )
+ printf( "%d=%d ", i, Count[i] );
+ printf( "\n" );
+
+ printf( "Cubes: " );
+ for ( i = 0; i < 16; i++ )
+ if ( Cubes[i] )
+ printf( "%d=%d ", i, Cubes[i] );
+ printf( "\n" );
+
+/*
+ // extract cubes one at a time
+ for ( i = 0; i < nMints; i++ )
+ if ( Pla_TtGetBit(pOn, i) )
+ {
+ word Cube = 0;
+ for ( v = 0; v < nVars; v++ )
+ if ( (i >> v) & 1 )
+ Pla_CubeSetLit( &Cube, v, PLA_LIT_ONE );
+ else
+ Pla_CubeSetLit( &Cube, v, PLA_LIT_ZERO );
+ Vec_WrdPush( vCubes, Cube );
+ }
+*/
+ Vec_IntForEachEntryDouble( vStore, iMint, iVar, i )
+ {
+ word Cube = 0;
+ for ( v = 0; v < nVars; v++ )
+ {
+ if ( v == iVar )
+ continue;
+ if ( (iMint >> v) & 1 )
+ Pla_CubeSetLit( &Cube, v, PLA_LIT_ONE );
+ else
+ Pla_CubeSetLit( &Cube, v, PLA_LIT_ZERO );
+ }
+ Vec_WrdPush( vCubes, Cube );
+ }
+ Vec_IntFree( vStore );
+
+ // collect the minterms
+ ABC_FREE( pDc );
+ return vCubes;
+}
+Pla_Man_t * Pla_ManFxPrepare( int nVars )
+{
+ Pla_Man_t * p; char Buffer[1000];
+ Vec_Bit_t * vFunc = Pla_ManPrimesTable( nVars );
+ Vec_Wrd_t * vSop = Pla_ManFxMinimize( (word *)Vec_BitArray(vFunc), nVars );
+ word Cube, * pCube = &Cube; int i, k, Lit;
+ sprintf( Buffer, "primes%02d", nVars );
+ p = Pla_ManAlloc( Buffer, nVars, 1, Vec_WrdSize(vSop) );
+ Vec_WecInit( &p->vCubeLits, Pla_ManCubeNum(p) );
+ Vec_WecInit( &p->vOccurs, 2*Pla_ManInNum(p) );
+ Vec_WrdForEachEntry( vSop, Cube, i )
+ Pla_CubeForEachLit( nVars, pCube, Lit, k )
+ if ( Lit != PLA_LIT_DASH )
+ {
+ Lit = Abc_Var2Lit( k, Lit == PLA_LIT_ZERO );
+ Vec_WecPush( &p->vCubeLits, i, Lit );
+ Vec_WecPush( &p->vOccurs, Lit, i );
+ }
+ Vec_BitFree( vFunc );
+ Vec_WrdFree( vSop );
+ return p;
+}
+int Pla_ManFxPerformSimple( int nVars )
+{
+ char Buffer[100];
+ Pla_Man_t * p = Pla_ManFxPrepare( nVars );
+ sprintf( Buffer, "primesmin%02d.pla", nVars );
+ Pla_ManDumpPla( p, Buffer );
+ Pla_ManFree( p );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/pla/plaWrite.c b/src/base/pla/plaWrite.c
index ed301e87..48f429a4 100644
--- a/src/base/pla/plaWrite.c
+++ b/src/base/pla/plaWrite.c
@@ -49,7 +49,7 @@ Vec_Str_t * Pla_WritePlaInt( Pla_Man_t * p )
int i, k, Lit;
// write comments
Vec_StrPrintStr( vOut, "# SOP \"" );
- Vec_StrPrintStr( vOut, p->pName );
+ Vec_StrPrintStr( vOut, Pla_ManName(p) );
Vec_StrPrintStr( vOut, "\" written via PLA package in ABC on " );
Vec_StrPrintStr( vOut, Extra_TimeStamp() );
Vec_StrPrintStr( vOut, "\n\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 03:56:13 +0000