summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaShrink7.c462
-rw-r--r--src/misc/vec/vecHash.h253
-rw-r--r--src/misc/vec/vecHsh4.h213
3 files changed, 652 insertions, 276 deletions
diff --git a/src/aig/gia/giaShrink7.c b/src/aig/gia/giaShrink7.c
index f8520036..ddc7da4a 100644
--- a/src/aig/gia/giaShrink7.c
+++ b/src/aig/gia/giaShrink7.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
-#include "misc/vec/vecHsh4.h"
+#include "misc/vec/vecHash.h"
#include "misc/util/utilTruth.h"
@@ -35,8 +35,10 @@ struct Unm_Man_t_
{
Gia_Man_t * pGia; // user's AIG
Gia_Man_t * pNew; // constructed AIG
- Hsh_Int4Man_t * pHash; // hash table
+ Hash_IntMan_t * pHash; // hash table
int nNewSize; // expected size of new manager
+ Vec_Int_t * vUsed; // used nodes
+ Vec_Int_t * vId2Used; // mapping of obj IDs into used node IDs
Vec_Wrd_t * vTruths; // truth tables
Vec_Int_t * vLeaves; // temporary storage for leaves
abctime clkStart; // starting the clock
@@ -50,6 +52,202 @@ extern word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * v
/**Function*************************************************************
+ Synopsis [Check if the function is decomposable with the given pair.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Unm_ManCheckAnd( word t, int i, int j, word * pOut )
+{
+ word c0 = Abc_Tt6Cofactor0( t, i );
+ word c1 = Abc_Tt6Cofactor1( t, i );
+ word c00 = Abc_Tt6Cofactor0( c0, j );
+ word c01 = Abc_Tt6Cofactor1( c0, j );
+ word c10 = Abc_Tt6Cofactor0( c1, j );
+ word c11 = Abc_Tt6Cofactor1( c1, j );
+ if ( c00 == c01 && c00 == c10 ) // i * j
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
+ return 0;
+ }
+ if ( c11 == c00 && c11 == c10 ) // i * !j
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01);
+ return 1;
+ }
+ if ( c11 == c00 && c11 == c01 ) // !i * j
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
+ return 2;
+ }
+ if ( c11 == c01 && c11 == c10 ) // !i * !j
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00);
+ return 3;
+ }
+ if ( c00 == c11 && c01 == c10 )
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
+ return 4;
+ }
+ return -1;
+}
+static inline int Unm_ManCheckMux( word t, int i, word * pOut )
+{
+ word c0 = Abc_Tt6Cofactor0( t, i );
+ word c1 = Abc_Tt6Cofactor1( t, i );
+ word c00, c01, c10, c11;
+ int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1;
+ for ( k = 0; k < 6; k++ )
+ {
+ if ( k == i ) continue;
+ fPres0 = Abc_Tt6HasVar( c0, k );
+ fPres1 = Abc_Tt6HasVar( c1, k );
+ if ( fPres0 && !fPres1 )
+ {
+ if ( iVar0 >= 0 )
+ return -1;
+ iVar0 = k;
+ }
+ if ( !fPres0 && fPres1 )
+ {
+ if ( iVar1 >= 0 )
+ return -1;
+ iVar1 = k;
+ }
+ }
+ if ( iVar0 == -1 || iVar1 == -1 )
+ return -1;
+ c00 = Abc_Tt6Cofactor0( c0, iVar0 );
+ c01 = Abc_Tt6Cofactor1( c0, iVar0 );
+ c10 = Abc_Tt6Cofactor0( c1, iVar1 );
+ c11 = Abc_Tt6Cofactor1( c1, iVar1 );
+ if ( c00 == c10 && c01 == c11 ) // ITE(i, iVar1, iVar0)
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
+ return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0);
+ }
+ if ( c00 == ~c10 && c01 == ~c11 ) // ITE(i, iVar1, !iVar0)
+ {
+ if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
+ return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1);
+ }
+ return -1;
+}
+void Unm_ManCheckTest2()
+{
+ word t, t1, Out, Var0, Var1, Var0_, Var1_;
+ int iVar0, iVar1, i, Res;
+ for ( iVar0 = 0; iVar0 < 6; iVar0++ )
+ for ( iVar1 = 0; iVar1 < 6; iVar1++ )
+ {
+ if ( iVar0 == iVar1 )
+ continue;
+ Var0 = s_Truths6[iVar0];
+ Var1 = s_Truths6[iVar1];
+ for ( i = 0; i < 5; i++ )
+ {
+ Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0;
+ Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1;
+
+ t = Var0_ & Var1_;
+ if ( i == 4 )
+ t = ~(Var0_ ^ Var1_);
+
+// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
+
+ Res = Unm_ManCheckAnd( t, iVar0, iVar1, &Out );
+ if ( Res == -1 )
+ {
+ printf( "No decomposition\n" );
+ continue;
+ }
+
+ Var0_ = s_Truths6[iVar0];
+ Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_;
+
+ Var1_ = s_Truths6[iVar1];
+ Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_;
+
+ t1 = Var0_ & Var1_;
+ if ( Res == 4 )
+ t1 = Var0_ ^ Var1_;
+
+ t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0));
+
+// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
+
+ if ( t1 != t )
+ printf( "Verification failed.\n" );
+ else
+ printf( "Verification succeeded.\n" );
+ }
+ }
+}
+void Unm_ManCheckTest()
+{
+ word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_;
+ int iVar0, iVar1, iCtrl, i, Res;
+ for ( iCtrl = 0; iCtrl < 6; iCtrl++ )
+ for ( iVar0 = 0; iVar0 < 6; iVar0++ )
+ for ( iVar1 = 0; iVar1 < 6; iVar1++ )
+ {
+ if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 )
+ continue;
+ Ctrl = s_Truths6[iCtrl];
+ Var0 = s_Truths6[iVar0];
+ Var1 = s_Truths6[iVar1];
+ for ( i = 0; i < 8; i++ )
+ {
+ Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl;
+ Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0;
+ Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1;
+
+ t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
+
+// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
+
+ Res = Unm_ManCheckMux( t, iCtrl, &Out );
+ if ( Res == -1 )
+ {
+ printf( "No decomposition\n" );
+ continue;
+ }
+
+// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
+
+ Ctrl_ = s_Truths6[iCtrl];
+ Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
+ Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_;
+
+ Res >>= 16;
+ Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
+ Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_;
+
+ t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
+
+// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
+// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
+
+ t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl));
+
+// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
+
+ if ( t1 != t )
+ printf( "Verification failed.\n" );
+ else
+ printf( "Verification succeeded.\n" );
+ }
+ }
+}
+
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -76,9 +274,8 @@ Unm_Man_t * Unm_ManAlloc( Gia_Man_t * pGia )
Gia_ManIncrementTravId( p->pNew );
p->pNew->nObjs = 1;
// start hashing
- p->pHash = Hsh_Int4ManStart( 1000 );
+ p->pHash = Hash_IntManStart( 1000 );
// truth tables
- p->vTruths = Vec_WrdStart( Gia_ManObjNum(pGia) );
p->vLeaves = Vec_IntStart( 10 );
return p;
}
@@ -91,8 +288,10 @@ Gia_Man_t * Unm_ManFree( Unm_Man_t * p )
// truth tables
Vec_WrdFreeP( &p->vTruths );
Vec_IntFreeP( &p->vLeaves );
+ Vec_IntFreeP( &p->vUsed );
+ Vec_IntFreeP( &p->vId2Used );
// free data structures
- Hsh_Int4ManStop( p->pHash );
+ Hash_IntManStop( p->pHash );
ABC_FREE( p );
Gia_ManStop( pTemp );
@@ -103,7 +302,7 @@ Gia_Man_t * Unm_ManFree( Unm_Man_t * p )
/**Function*************************************************************
- Synopsis [Computes truth tables for all LUTs.]
+ Synopsis [Computes information about node pairs.]
Description []
@@ -112,33 +311,138 @@ Gia_Man_t * Unm_ManFree( Unm_Man_t * p )
SeeAlso []
***********************************************************************/
-void Unm_ManComputeTruths( Unm_Man_t * p )
+int Unm_ManPrintPairStats( Hash_IntMan_t * pHash, int nTotal0, int nPairs0, int nPairs1, int fUseLit )
+{
+ int i, Num, nRefs, nPairs = 0, nTotal = 0, Counter[21] = {0};
+ Num = Hash_IntManEntryNum( pHash );
+ for ( i = 1; i <= Num; i++ )
+ {
+ nRefs = Abc_MinInt( 20, Hash_IntObjData2(pHash, i) );
+ nTotal += nRefs;
+ Counter[nRefs]++;
+ nPairs += (nRefs > 1);
+/*
+ if ( fUseLit )
+ printf( "(%c%c, %c%c) %d\n",
+ Abc_LitIsCompl(Hash_IntObjData0(pHash, i)-2) ? '!' : ' ',
+ 'a' + Abc_Lit2Var(Hash_IntObjData0(pHash, i)-2),
+ Abc_LitIsCompl(Hash_IntObjData1(pHash, i)-2) ? '!' : ' ',
+ 'a' + Abc_Lit2Var(Hash_IntObjData1(pHash, i)-2), nRefs );
+ else
+ printf( "( %c, %c) %d\n",
+ 'a' + Hash_IntObjData0(pHash, i)-1,
+ 'a' + Hash_IntObjData1(pHash, i)-1, nRefs );
+*/
+// printf( "(%4d, %4d) %d\n", Hash_IntObjData0(pHash, i), Hash_IntObjData1(pHash, i), nRefs );
+
+ }
+ printf( "Statistics for pairs appearing less than 20 times:\n" );
+ for ( i = 0; i < 21; i++ )
+ if ( Counter[i] > 0 )
+ printf( "%3d : %7d %7.2f %%\n", i, Counter[i], 100.0 * Counter[i] * i / Abc_MaxInt(nTotal, 1) );
+ printf( "Pairs: Total = %8d Init = %8d %7.2f %% Final = %8d %7.2f %% Real = %8d %7.2f %%\n", nTotal0,
+ nPairs0, 100.0 * nPairs0 / Abc_MaxInt(nTotal0, 1),
+ nPairs, 100.0 * nPairs / Abc_MaxInt(nTotal0, 1),
+ nPairs1, 100.0 * nPairs1 / Abc_MaxInt(nTotal0, 1) );
+ return nPairs;
+}
+Vec_Int_t * Unm_ManComputePairs( Unm_Man_t * p, int fVerbose )
{
- Vec_Wrd_t * vTruths2;
Gia_Obj_t * pObj;
- int i, k, iNode;
- word uTruth;
- vTruths2 = Vec_WrdStart( Gia_ManObjNum(p->pGia) );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vNum2Obj = Vec_IntStart( 1 );
+ Hash_IntMan_t * pHash = Hash_IntManStart( 1000 );
+ int nTotal = 0, nPairs0 = 0, nPairs = 0;
+ int i, k, j, FanK, FanJ, Num, nRefs;
+ Gia_ManSetRefsMapped( p->pGia );
Gia_ManForEachLut( p->pGia, i )
{
+ nTotal += Gia_ObjLutSize(p->pGia, i) * (Gia_ObjLutSize(p->pGia, i) - 1) / 2;
pObj = Gia_ManObj( p->pGia, i );
// collect leaves of this gate
Vec_IntClear( p->vLeaves );
- Gia_LutForEachFanin( p->pGia, i, iNode, k )
+ Gia_LutForEachFanin( p->pGia, i, Num, k )
+ if ( Gia_ObjRefNumId(p->pGia, Num) > 1 )
+ Vec_IntPush( p->vLeaves, Num );
+ if ( Vec_IntSize(p->vLeaves) < 2 )
+ continue;
+ nPairs0 += Vec_IntSize(p->vLeaves) * (Vec_IntSize(p->vLeaves) - 1) / 2;
+ // enumerate pairs
+ Vec_IntForEachEntry( p->vLeaves, FanK, k )
+ Vec_IntForEachEntryStart( p->vLeaves, FanJ, j, k+1 )
+ {
+ if ( FanK > FanJ )
+ ABC_SWAP( int, FanK, FanJ );
+ Num = Hash_Int2ManInsert( pHash, FanK, FanJ, 0 );
+ nRefs = Hash_Int2ObjInc(pHash, Num);
+ if ( nRefs == 0 )
+ {
+ assert( Num == Hash_IntManEntryNum(pHash) );
+ assert( Num == Vec_IntSize(vNum2Obj) );
+ Vec_IntPush( vNum2Obj, i );
+ continue;
+ }
+ if ( nRefs == 1 )
+ {
+ assert( Num < Vec_IntSize(vNum2Obj) );
+ Vec_IntPush( vPairs, Vec_IntEntry(vNum2Obj, Num) );
+ Vec_IntPush( vPairs, FanK );
+ Vec_IntPush( vPairs, FanJ);
+ }
+ Vec_IntPush( vPairs, i );
+ Vec_IntPush( vPairs, FanK );
+ Vec_IntPush( vPairs, FanJ );
+ }
+ }
+ Vec_IntFree( vNum2Obj );
+ if ( fVerbose )
+ nPairs = Unm_ManPrintPairStats( pHash, nTotal, nPairs0, Vec_IntSize(vPairs) / 3, 0 );
+ Hash_IntManStop( pHash );
+ return vPairs;
+}
+// finds used nodes
+Vec_Int_t * Unm_ManFindUsedNodes( Vec_Int_t * vPairs, int nObjs )
+{
+ Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
+ Vec_Str_t * vMarks = Vec_StrStart( nObjs ); int i;
+ for ( i = 0; i < Vec_IntSize(vPairs); i += 3 )
+ Vec_StrWriteEntry( vMarks, Vec_IntEntry(vPairs, i), 1 );
+ for ( i = 0; i < nObjs; i++ )
+ if ( Vec_StrEntry( vMarks, i ) )
+ Vec_IntPush( vNodes, i );
+ Vec_StrFree( vMarks );
+ printf( "The number of used nodes = %d\n", Vec_IntSize(vNodes) );
+ return vNodes;
+}
+// computes truth table for selected nodes
+Vec_Wrd_t * Unm_ManComputeTruths( Unm_Man_t * p )
+{
+ Vec_Wrd_t * vTruthsTemp, * vTruths;
+ int i, k, iObj, iNode;
+ word uTruth;
+ vTruths = Vec_WrdAlloc( Vec_IntSize(p->vUsed) );
+ vTruthsTemp = Vec_WrdStart( Gia_ManObjNum(p->pGia) );
+ Vec_IntForEachEntry( p->vUsed, iObj, i )
+ {
+ assert( Gia_ObjIsLut(p->pGia, iObj) );
+ // collect leaves of this gate
+ Vec_IntClear( p->vLeaves );
+ Gia_LutForEachFanin( p->pGia, iObj, iNode, k )
Vec_IntPush( p->vLeaves, iNode );
assert( Vec_IntSize(p->vLeaves) <= 6 );
// compute truth table
- uTruth = Shr_ManComputeTruth6( p->pGia, pObj, p->vLeaves, vTruths2 );
- Vec_WrdWriteEntry( p->vTruths, i, uTruth );
+ uTruth = Shr_ManComputeTruth6( p->pGia, Gia_ManObj(p->pGia, iObj), p->vLeaves, vTruthsTemp );
+ Vec_WrdPush( vTruths, uTruth );
// if ( i % 100 == 0 )
// Kit_DsdPrintFromTruth( (unsigned *)&uTruth, 6 ), printf( "\n" );
}
- Vec_WrdFreeP( &vTruths2 );
+ Vec_WrdFreeP( &vTruthsTemp );
+ return vTruths;
}
/**Function*************************************************************
- Synopsis [Computes information about node pairs.]
+ Synopsis [Collects decomposable pairs.]
Description []
@@ -147,59 +451,91 @@ void Unm_ManComputeTruths( Unm_Man_t * p )
SeeAlso []
***********************************************************************/
-int Unm_ManPrintPairStats( Unm_Man_t * p )
-{
- int i, Num, nRefs, nPairs = 0, nTotal = 0, Counter[51] = {0};
- Num = Hsh_Int4ManEntryNum( p->pHash );
- for ( i = 1; i <= Num; i++ )
- {
- nRefs = Abc_MinInt( 50, Hsh_Int4ObjRes(p->pHash, i) );
- nTotal += nRefs;
- Counter[nRefs]++;
- nPairs += (nRefs > 1);
-// printf( "(%c, %c) %d\n", 'a' + Hsh_Int4ObjData0(p->pHash, i)-1, 'a' + Hsh_Int4ObjData1(p->pHash, i)-1, nRefs );
-// printf( "(%4d, %4d) %d\n", Hsh_Int4ObjData0(p->pHash, i), Hsh_Int4ObjData1(p->pHash, i), nRefs );
- }
- for ( i = 0; i < 51; i++ )
- if ( Counter[i] > 0 )
- printf( "%3d : %7d %7.2f %%\n", i, Counter[i], 100.0 * Counter[i] * i / nTotal );
- return nPairs;
-}
-void Unm_ManComputePairs( Unm_Man_t * p )
+Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbose )
{
- Gia_Obj_t * pObj;
- int i, k, j, FanK, FanJ, Num;
- word Total = 0, Pairs = 0, Pairs2 = 0;
- Gia_ManSetRefsMapped( p->pGia );
- Gia_ManForEachLut( p->pGia, i )
+ word uTruth; int nNonUnique = 0;
+ int i, k, j, s, iObj, iNode, iUsed, FanK, FanJ, Res, Num, nRefs;
+ Vec_Int_t * vNum2Obj = Vec_IntStart( 1 );
+ Vec_Int_t * vPairs2 = Vec_IntAlloc( 1000 );
+ assert( Hash_IntManEntryNum(p->pHash) == 0 );
+ for ( i = 0; i < Vec_IntSize(vPairs); i += 3 )
{
- Total += Gia_ObjLutSize(p->pGia, i) * (Gia_ObjLutSize(p->pGia, i) - 1) / 2;
- pObj = Gia_ManObj( p->pGia, i );
+ iObj = Vec_IntEntry( vPairs, i );
+ assert( Gia_ObjIsLut(p->pGia, iObj) );
// collect leaves of this gate
Vec_IntClear( p->vLeaves );
- Gia_LutForEachFanin( p->pGia, i, Num, k )
- if ( Gia_ObjRefNumId(p->pGia, Num) > 1 )
- Vec_IntPush( p->vLeaves, Num );
- if ( Vec_IntSize(p->vLeaves) < 2 )
+ Gia_LutForEachFanin( p->pGia, iObj, iNode, s )
+ Vec_IntPush( p->vLeaves, iNode );
+ assert( Vec_IntSize(p->vLeaves) <= 6 );
+ FanK = Vec_IntEntry(vPairs, i+1);
+ FanJ = Vec_IntEntry(vPairs, i+2);
+ k = Vec_IntFind( p->vLeaves, FanK );
+ j = Vec_IntFind( p->vLeaves, FanJ );
+ assert( FanK < FanJ );
+ iUsed = Vec_IntEntry( p->vId2Used, iObj );
+ uTruth = Vec_WrdEntry( p->vTruths, iUsed );
+ Res = Unm_ManCheckAnd( uTruth, k, j, NULL );
+ if ( Res == -1 )
continue;
- Pairs += Vec_IntSize(p->vLeaves) * (Vec_IntSize(p->vLeaves) - 1) / 2;
- // enumerate pairs
- Vec_IntForEachEntry( p->vLeaves, FanK, k )
- Vec_IntForEachEntryStart( p->vLeaves, FanJ, j, k+1 )
+ // derive literals
+ FanK = Abc_Var2Lit( FanK, ((Res >> 0) & 1) );
+ FanJ = Abc_Var2Lit( FanJ, ((Res >> 1) & 1) );
+ if ( Res == 4 )
+ ABC_SWAP( int, FanK, FanJ );
+ Num = Hash_Int2ManInsert( p->pHash, FanK, FanJ, 0 );
+ nRefs = Hash_Int2ObjInc(p->pHash, Num);
+ if ( nRefs == 0 )
{
- if ( FanK > FanJ )
- ABC_SWAP( int, FanK, FanJ );
- Num = Hsh_Int4ManInsert( p->pHash, FanK, FanJ, 0 );
- Hsh_Int4ObjInc( p->pHash, Num );
+ assert( Num == Hash_IntManEntryNum(p->pHash) );
+ assert( Num == Vec_IntSize(vNum2Obj) );
+ Vec_IntPush( vNum2Obj, iObj );
+ continue;
}
+ if ( nRefs == 1 )
+ {
+ assert( Num < Vec_IntSize(vNum2Obj) );
+ Vec_IntPush( vPairs2, Vec_IntEntry(vNum2Obj, Num) );
+ Vec_IntPush( vPairs2, FanK );
+ Vec_IntPush( vPairs2, FanJ );
+ nNonUnique++;
+ }
+ Vec_IntPush( vPairs2, iObj );
+ Vec_IntPush( vPairs2, FanK );
+ Vec_IntPush( vPairs2, FanJ );
}
- Total = Abc_MaxWord( Total, 1 );
- Pairs2 = Unm_ManPrintPairStats( p );
- printf( "Total = %8d Pairs = %8d %7.2f %% Pairs2 = %8d %7.2f %%\n", (int)Total,
- (int)Pairs, 100.0 * (int)Pairs / (int)Total,
- (int)Pairs2, 100.0 * (int)Pairs2 / (int)Total );
- // print statistics
-
+ Vec_IntFree( vNum2Obj );
+ if ( fVerbose )
+ Unm_ManPrintPairStats( p->pHash, Vec_IntSize(vPairs)/3, Hash_IntManEntryNum(p->pHash), Vec_IntSize(vPairs2)/3, 1 );
+// Hash_IntManStop( pHash );
+ return vPairs2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute truth tables for the selected nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Unm_ManWork( Unm_Man_t * p )
+{
+ Vec_Int_t * vPairs, * vPairs2;
+ // find the duplicated pairs
+ vPairs = Unm_ManComputePairs( p, 1 );
+ // find the used nodes
+ p->vUsed = Unm_ManFindUsedNodes( vPairs, Gia_ManObjNum(p->pGia) );
+ p->vId2Used = Vec_IntInvert( p->vUsed, -1 );
+ Vec_IntFillExtra( p->vId2Used, Gia_ManObjNum(p->pGia), -1 );
+ // compute truth tables for used nodes
+ p->vTruths = Unm_ManComputeTruths( p );
+ // derive new pairs
+ vPairs2 = Unm_ManCollectDecomp( p, vPairs, 1 );
+ Vec_IntFreeP( &vPairs );
+ Vec_IntFreeP( &vPairs2 );
}
@@ -218,8 +554,8 @@ Gia_Man_t * Unm_ManTest( Gia_Man_t * pGia )
{
Unm_Man_t * p;
p = Unm_ManAlloc( pGia );
-// Unm_ManComputeTruths( p );
- Unm_ManComputePairs( p );
+ Unm_ManWork( p );
+
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
return Unm_ManFree( p );
}
diff --git a/src/misc/vec/vecHash.h b/src/misc/vec/vecHash.h
new file mode 100644
index 00000000..e695f154
--- /dev/null
+++ b/src/misc/vec/vecHash.h
@@ -0,0 +1,253 @@
+/**CFile****************************************************************
+
+ FileName [vecHash.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Resizable arrays.]
+
+ Synopsis [Hashing integer pairs/triples into an integer.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: vecHash.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__misc__vec__vecHash_h
+#define ABC__misc__vec__vecHash_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Hash_IntObj_t_ Hash_IntObj_t;
+struct Hash_IntObj_t_
+{
+ int iData0;
+ int iData1;
+ int iData2;
+ int iNext;
+};
+
+typedef struct Hash_IntMan_t_ Hash_IntMan_t;
+struct Hash_IntMan_t_
+{
+ Vec_Int_t * vTable; // hash table
+ Vec_Int_t * vObjs; // hash objects
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hash_IntObj_t * Hash_IntObj( Hash_IntMan_t * p, int i ) { return i ? (Hash_IntObj_t *)Vec_IntEntryP(p->vObjs, 4*i) : NULL; }
+static inline int Hash_IntObjData0( Hash_IntMan_t * p, int i ) { return Hash_IntObj(p, i)->iData0; }
+static inline int Hash_IntObjData1( Hash_IntMan_t * p, int i ) { return Hash_IntObj(p, i)->iData1; }
+static inline int Hash_IntObjData2( Hash_IntMan_t * p, int i ) { return Hash_IntObj(p, i)->iData2; }
+
+static inline int Hash_Int2ObjInc( Hash_IntMan_t * p, int i ) { return Hash_IntObj(p, i)->iData2++; }
+static inline int Hash_Int2ObjDec( Hash_IntMan_t * p, int i ) { return --Hash_IntObj(p, i)->iData2; }
+static inline void Hash_Int2ObjSetData2( Hash_IntMan_t * p, int i, int d ) { Hash_IntObj(p, i)->iData2 = d; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Hashing data entries composed of nSize integers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Hash_IntMan_t * Hash_IntManStart( int nSize )
+{
+ Hash_IntMan_t * p; nSize += 100;
+ p = ABC_CALLOC( Hash_IntMan_t, 1 );
+ p->vTable = Vec_IntStart( Abc_PrimeCudd(nSize) );
+ p->vObjs = Vec_IntAlloc( 4*nSize );
+ Vec_IntFill( p->vObjs, 4, 0 );
+ return p;
+}
+static inline void Hash_IntManStop( Hash_IntMan_t * p )
+{
+ Vec_IntFree( p->vObjs );
+ Vec_IntFree( p->vTable );
+ ABC_FREE( p );
+}
+static inline int Hash_IntManEntryNum( Hash_IntMan_t * p )
+{
+ return Vec_IntSize(p->vObjs)/4 - 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Hash_Int2ManHash( int iData0, int iData1, int nTableSize )
+{
+ return (4177 * (unsigned)iData0 + 7873 * (unsigned)iData1) % (unsigned)nTableSize;
+}
+static inline int * Hash_Int2ManLookup( Hash_IntMan_t * p, int iData0, int iData1 )
+{
+ Hash_IntObj_t * pObj;
+ int * pPlace = Vec_IntEntryP( p->vTable, Hash_Int2ManHash(iData0, iData1, Vec_IntSize(p->vTable)) );
+ for ( ; (pObj = Hash_IntObj(p, *pPlace)); pPlace = &pObj->iNext )
+ if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 )
+ return pPlace;
+ assert( *pPlace == 0 );
+ return pPlace;
+}
+static inline int Hash_Int2ManInsert( Hash_IntMan_t * p, int iData0, int iData1, int iData2 )
+{
+ Hash_IntObj_t * pObj;
+ int i, nObjs, * pPlace;
+ nObjs = Vec_IntSize(p->vObjs)/4;
+ if ( nObjs > Vec_IntSize(p->vTable) )
+ {
+// printf( "Resizing...\n" );
+ Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), 0 );
+ for ( i = 1; i < nObjs; i++ )
+ {
+ pObj = Hash_IntObj( p, i );
+ pObj->iNext = 0;
+ pPlace = Hash_Int2ManLookup( p, pObj->iData0, pObj->iData1 );
+ assert( *pPlace == 0 );
+ *pPlace = i;
+ }
+ }
+ pPlace = Hash_Int2ManLookup( p, iData0, iData1 );
+ if ( *pPlace )
+ return *pPlace;
+ *pPlace = nObjs;
+ Vec_IntPush( p->vObjs, iData0 );
+ Vec_IntPush( p->vObjs, iData1 );
+ Vec_IntPush( p->vObjs, iData2 );
+ Vec_IntPush( p->vObjs, 0 );
+ return nObjs;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Hsh_Int3ManHash( int iData0, int iData1, int iData2, int nTableSize )
+{
+ return (4177 * (unsigned)iData0 + 7873 * (unsigned)iData1 + 1699 * (unsigned)iData2) % (unsigned)nTableSize;
+}
+static inline int * Hsh_Int3ManLookup( Hash_IntMan_t * p, int iData0, int iData1, int iData2 )
+{
+ Hash_IntObj_t * pObj;
+ int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int3ManHash(iData0, iData1, iData2, Vec_IntSize(p->vTable)) );
+ for ( ; (pObj = Hash_IntObj(p, *pPlace)); pPlace = &pObj->iNext )
+ if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 && pObj->iData2 == iData2 )
+ return pPlace;
+ assert( *pPlace == 0 );
+ return pPlace;
+}
+static inline int Hsh_Int3ManInsert( Hash_IntMan_t * p, int iData0, int iData1, int iData2 )
+{
+ Hash_IntObj_t * pObj;
+ int i, nObjs, * pPlace;
+ nObjs = Vec_IntSize(p->vObjs)/4;
+ if ( nObjs > Vec_IntSize(p->vTable) )
+ {
+// printf( "Resizing...\n" );
+ Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), 0 );
+ for ( i = 1; i < nObjs; i++ )
+ {
+ pObj = Hash_IntObj( p, i );
+ pObj->iNext = 0;
+ pPlace = Hsh_Int3ManLookup( p, pObj->iData0, pObj->iData1, pObj->iData2 );
+ assert( *pPlace == 0 );
+ *pPlace = i;
+ }
+ }
+ pPlace = Hsh_Int3ManLookup( p, iData0, iData1, iData2 );
+ if ( *pPlace )
+ return *pPlace;
+ *pPlace = nObjs;
+ Vec_IntPush( p->vObjs, iData0 );
+ Vec_IntPush( p->vObjs, iData1 );
+ Vec_IntPush( p->vObjs, iData2 );
+ Vec_IntPush( p->vObjs, 0 );
+ return nObjs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Test procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Hash_IntManHashArrayTest()
+{
+ Hash_IntMan_t * p;
+ int RetValue;
+
+ p = Hash_IntManStart( 10 );
+
+ RetValue = Hash_Int2ManInsert( p, 10, 11, 12 );
+ assert( RetValue );
+
+ RetValue = Hash_Int2ManInsert( p, 20, 21, 22 );
+ assert( RetValue );
+
+ RetValue = Hash_Int2ManInsert( p, 10, 11, 12 );
+ assert( !RetValue );
+
+ Hash_IntManStop( p );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
diff --git a/src/misc/vec/vecHsh4.h b/src/misc/vec/vecHsh4.h
deleted file mode 100644
index 2e79ee4a..00000000
--- a/src/misc/vec/vecHsh4.h
+++ /dev/null
@@ -1,213 +0,0 @@
-/**CFile****************************************************************
-
- FileName [vecHsh4.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Resizable arrays.]
-
- Synopsis [Hashing pairs of integers into an integer.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: vecHsh4.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef ABC__misc__vec__vecHsh4_h
-#define ABC__misc__vec__vecHsh4_h
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Hsh_Int4Obj_t_ Hsh_Int4Obj_t;
-struct Hsh_Int4Obj_t_
-{
- int iData0;
- int iData1;
- int iRes;
- int iNext;
-};
-
-typedef struct Hsh_Int4Man_t_ Hsh_Int4Man_t;
-struct Hsh_Int4Man_t_
-{
- Vec_Int_t * vTable; // hash table
- Vec_Int_t * vObjs; // hash objects
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Hsh_Int4Obj_t * Hsh_Int4Obj( Hsh_Int4Man_t * p, int iObj ) { return iObj ? (Hsh_Int4Obj_t *)Vec_IntEntryP(p->vObjs, 4*iObj) : NULL; }
-static inline int Hsh_Int4ObjData0( Hsh_Int4Man_t * p, int i ) { return Hsh_Int4Obj(p, i)->iData0; }
-static inline int Hsh_Int4ObjData1( Hsh_Int4Man_t * p, int i ) { return Hsh_Int4Obj(p, i)->iData1; }
-static inline int Hsh_Int4ObjRes( Hsh_Int4Man_t * p, int i ) { return Hsh_Int4Obj(p, i)->iRes; }
-static inline void Hsh_Int4ObjInc( Hsh_Int4Man_t * p, int i ) { Hsh_Int4Obj(p, i)->iRes++; }
-static inline void Hsh_Int4ObjDec( Hsh_Int4Man_t * p, int i ) { Hsh_Int4Obj(p, i)->iRes--; }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Hashing data entries composed of nSize integers.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Hsh_Int4Man_t * Hsh_Int4ManStart( int nSize )
-{
- Hsh_Int4Man_t * p; nSize += 100;
- p = ABC_CALLOC( Hsh_Int4Man_t, 1 );
- p->vTable = Vec_IntStart( Abc_PrimeCudd(nSize) );
- p->vObjs = Vec_IntAlloc( 4*nSize );
- Vec_IntFill( p->vObjs, 4, 0 );
- return p;
-}
-static inline void Hsh_Int4ManStop( Hsh_Int4Man_t * p )
-{
- Vec_IntFree( p->vObjs );
- Vec_IntFree( p->vTable );
- ABC_FREE( p );
-}
-static inline int Hsh_Int4ManEntryNum( Hsh_Int4Man_t * p )
-{
- return Vec_IntSize(p->vObjs)/4 - 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Hsh_Int4ManHash( int iData0, int iData1, int nTableSize )
-{
- return (4177 * (unsigned)iData0 + 7873 * (unsigned)iData1) % (unsigned)nTableSize;
-}
-static inline int * Hsh_Int4ManLookup( Hsh_Int4Man_t * p, int iData0, int iData1 )
-{
- Hsh_Int4Obj_t * pObj;
- int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) );
- for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext )
- if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 )
- return pPlace;
- assert( *pPlace == 0 );
- return pPlace;
-}
-static inline int Hsh_Int4ManFind( Hsh_Int4Man_t * p, int iData0, int iData1 )
-{
- Hsh_Int4Obj_t * pObj;
- int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) );
- for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext )
- if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 )
- return pObj->iRes;
- assert( *pPlace == 0 );
- return -1;
-}
-static inline int Hsh_Int4ManInsert( Hsh_Int4Man_t * p, int iData0, int iData1, int iRes )
-{
- Hsh_Int4Obj_t * pObj;
- int i, nObjs, * pPlace;
- nObjs = Vec_IntSize(p->vObjs)/4;
- if ( nObjs > Vec_IntSize(p->vTable) )
- {
-// printf( "Resizing...\n" );
- Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), 0 );
- for ( i = 1; i < nObjs; i++ )
- {
- pObj = Hsh_Int4Obj( p, i );
- pObj->iNext = 0;
- pPlace = Hsh_Int4ManLookup( p, pObj->iData0, pObj->iData1 );
- assert( *pPlace == 0 );
- *pPlace = i;
- }
- }
- pPlace = Hsh_Int4ManLookup( p, iData0, iData1 );
- if ( *pPlace )
- return *pPlace;
- *pPlace = nObjs;
- Vec_IntPush( p->vObjs, iData0 );
- Vec_IntPush( p->vObjs, iData1 );
- Vec_IntPush( p->vObjs, iRes );
- Vec_IntPush( p->vObjs, 0 );
- return nObjs;
-}
-
-/**Function*************************************************************
-
- Synopsis [Test procedure.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Hsh_Int4ManHashArrayTest()
-{
- Hsh_Int4Man_t * p;
- int RetValue;
-
- p = Hsh_Int4ManStart( 10 );
-
- RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 );
- assert( RetValue );
-
- RetValue = Hsh_Int4ManInsert( p, 20, 21, 22 );
- assert( RetValue );
-
- RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 );
- assert( !RetValue );
-
- RetValue = Hsh_Int4ManFind( p, 20, 21 );
- assert( RetValue == 22 );
-
- RetValue = Hsh_Int4ManFind( p, 20, 22 );
- assert( RetValue == -1 );
-
- Hsh_Int4ManStop( p );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-ABC_NAMESPACE_HEADER_END
-
-#endif
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 02:52:40 +0000