summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp148
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaIf.c15
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/base/abci/abc.c37
-rw-r--r--src/map/if/ifDec07.c296
-rw-r--r--src/misc/util/utilTruth.h13
-rw-r--r--src/opt/dau/dauDsd.c4
-rw-r--r--src/opt/dau/dauNonDsd.c642
-rw-r--r--src/opt/dau/module.make1
10 files changed, 949 insertions, 212 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 236bbe42..275f3896 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -733,154 +733,10 @@ SOURCE=.\src\base\test\test.c
# Begin Group "abc2"
# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2_.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifo.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Core.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Dup.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Equiv.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Extract.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Flatten.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Func.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Fx.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Gia.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Hash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Insert.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Logic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Map.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Mfs.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Multi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Ntk.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Part.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Print.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Rec.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Slack.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Strash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Time.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Truth.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Util.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Veri.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Verify.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Vero.c
-# End Source File
# End Group
# Begin Group "abc2d"
# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\abc2d.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\ast2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\util.c
-# End Source File
# End Group
# End Group
# Begin Group "bdd"
@@ -2227,6 +2083,10 @@ SOURCE=.\src\opt\dau\dauMerge.c
# End Source File
# Begin Source File
+SOURCE=.\src\opt\dau\dauNonDsd.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\opt\dau\dauTree.c
# End Source File
# End Group
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fb93e0c2..b10a0677 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -193,6 +193,7 @@ struct Gps_Par_t_
int fCut;
int fNpn;
int fLutProf;
+ int fDumpFile;
};
typedef struct Emb_Par_t_ Emb_Par_t;
@@ -1077,7 +1078,7 @@ extern void Gia_ManHashProfile( Gia_Man_t * p );
extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
/*=== giaIf.c ===========================================================*/
-extern void Gia_ManPrintMappingStats( Gia_Man_t * p );
+extern void Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile );
extern void Gia_ManPrintPackingStats( Gia_Man_t * p );
extern void Gia_ManPrintLutStats( Gia_Man_t * p );
extern int Gia_ManLutFaninCount( Gia_Man_t * p );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index d50e34c9..425445c9 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -303,7 +303,7 @@ int Gia_ManComputeOverlap( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-void Gia_ManPrintMappingStats( Gia_Man_t * p )
+void Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile )
{
int * pLevels;
int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
@@ -328,7 +328,8 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
Abc_Print( 1, "\n" );
-/*
+
+ if ( fDumpFile )
{
char * pFileName = "stats_map.txt";
static char FileNameOld[1000] = {0};
@@ -355,7 +356,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
}
fclose( pTable );
}
-*/
+
}
/**Function*************************************************************
@@ -782,6 +783,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t
for ( i = 0; i < 4; i++ )
{
int v = (int)((z >> (16+(i<<2))) & 7);
+ if ( v == 6 && Vec_IntSize(vLeaves) == 5 )
+ continue;
Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v) );
}
Truth = (z & 0xffff);
@@ -793,6 +796,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t
for ( i = 0; i < 4; i++ )
{
int v = (int)((z >> (48+(i<<2))) & 7);
+ if ( v == 6 && Vec_IntSize(vLeaves) == 5 )
+ continue;
if ( v == 7 )
Vec_IntPush( vLeavesTemp, iObjLit1 );
else
@@ -1204,8 +1209,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
word Truth = 0, * pTruthTable;
int i, k, Entry;
assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
- if ( pIfMan->pPars->fEnableCheck07 )
- pIfMan->pPars->fDeriveLuts = 0;
+// if ( pIfMan->pPars->fEnableCheck07 )
+// pIfMan->pPars->fDeriveLuts = 0;
// start mapping and packing
vMapping = Vec_IntStart( If_ManObjNum(pIfMan) );
vMapping2 = Vec_IntStart( 1 );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index e57fe27d..2eaf8eee 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -366,7 +366,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
if ( p->pSibls )
Gia_ManPrintChoiceStats( p );
if ( Gia_ManHasMapping(p) )
- Gia_ManPrintMappingStats( p );
+ Gia_ManPrintMappingStats( p, pPars->fDumpFile );
if ( pPars && pPars->fNpn && Gia_ManHasMapping(p) && Gia_ManLutSizeMax(p) <= 4 )
Gia_ManPrintNpnClasses( p );
if ( p->vPacking )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9633158..eb8c2a89 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -994,10 +994,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
if ( Sdm_ManCanRead() )
Sdm_ManRead();
- {
-// extern void Scl_LibertyTest();
-// Scl_LibertyTest();
- }
}
/**Function*************************************************************
@@ -2221,16 +2217,19 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCofactor;
int nCofLevel;
int fProfile;
+ int fPrintDec;
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
+ extern void Dau_DecTrySets( word * p, int nVars );
// set defaults
nCofLevel = 1;
fCofactor = 0;
fProfile = 0;
+ fPrintDec = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Npch" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Npcdh" ) ) != EOF )
{
switch ( c )
{
@@ -2245,11 +2244,14 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nCofLevel < 0 )
goto usage;
break;
+ case 'p':
+ fProfile ^= 1;
+ break;
case 'c':
fCofactor ^= 1;
break;
- case 'p':
- fProfile ^= 1;
+ case 'd':
+ fPrintDec ^= 1;
break;
case 'h':
goto usage;
@@ -2291,6 +2293,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
// Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
// Abc_Print( -1, "\n" );
+ if ( fPrintDec && Abc_ObjFaninNum(pObj) <= 6 )
+ Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) );
if ( fProfile )
Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
else if ( fCofactor )
@@ -2302,10 +2306,11 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: print_dsd [-pch] [-N <num>]\n" );
+ Abc_Print( -2, "usage: print_dsd [-pcdh] [-N <num>]\n" );
Abc_Print( -2, "\t print DSD formula for a single-output function with less than 16 variables\n" );
Abc_Print( -2, "\t-p : toggle printing profile [default = %s]\n", fProfile? "yes": "no" );
Abc_Print( -2, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggle printing decompositions [default = %s]\n", fPrintDec? "yes": "no" );
Abc_Print( -2, "\t-N <num> : the number of levels to cofactor [default = %d]\n", nCofLevel );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -25318,7 +25323,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
memset( pPars, 0, sizeof(Gps_Par_t) );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnlh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnldh" ) ) != EOF )
{
switch ( c )
{
@@ -25337,6 +25342,9 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
pPars->fLutProf ^= 1;
break;
+ case 'd':
+ pPars->fDumpFile ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -25352,13 +25360,14 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &ps [-tpcnlh]\n" );
+ Abc_Print( -2, "usage: &ps [-tpcnldh]\n" );
Abc_Print( -2, "\t prints stats of the current AIG\n" );
- Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" );
- Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" );
+ Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" );
Abc_Print( -2, "\t-c : toggle printing the size of frontier cut [default = %s]\n", pPars->fCut? "yes": "no" );
Abc_Print( -2, "\t-n : toggle printing NPN classes of functions [default = %s]\n", pPars->fNpn? "yes": "no" );
- Abc_Print( -2, "\t-l : toggle printing LUT size profile [default = %s]\n", pPars->fLutProf? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggle printing LUT size profile [default = %s]\n", pPars->fLutProf? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggle dumping statistics into a file [default = %s]\n", pPars->fDumpFile? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -33697,7 +33706,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// pTemp = Llb_ReachableStatesGia( pAbc->pGia );
// Abc_FrameUpdateGia( pAbc, pTemp );
// Unm_ManTest( pAbc->pGia );
- Agi_ManTest( pAbc->pGia );
+// Agi_ManTest( pAbc->pGia );
return 0;
usage:
Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c
index 1bbc93fb..6059b772 100644
--- a/src/map/if/ifDec07.c
+++ b/src/map/if/ifDec07.c
@@ -21,6 +21,7 @@
#include "if.h"
#include "misc/extra/extra.h"
#include "bool/kit/kit.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -115,7 +116,7 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
}
return r;
}
-void If_Dec6Verify( word t, word z )
+word If_Dec6Truth( word z )
{
word r, q, f[4];
int i, v;
@@ -124,20 +125,29 @@ void If_Dec6Verify( word t, word z )
{
v = (z >> (16+(i<<2))) & 7;
assert( v != 7 );
+ if ( v == 6 )
+ continue;
f[i] = Truth6[v];
}
q = If_Dec6ComposeLut4( (int)(z & 0xffff), f );
for ( i = 0; i < 4; i++ )
{
v = (z >> (48+(i<<2))) & 7;
+ if ( v == 6 )
+ continue;
f[i] = (v == 7) ? q : Truth6[v];
}
r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f );
+ return r;
+}
+void If_Dec6Verify( word t, word z )
+{
+ word r = If_Dec6Truth( z );
if ( r != t )
{
If_DecPrintConfig( z );
Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" );
- Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" );
+// Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" );
printf( "Verification failed!\n" );
}
@@ -677,43 +687,191 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
***********************************************************************/
// count the number of unique cofactors
-static inline int If_Dec5CofCount2( word t, int x, int y )
+static inline word If_Dec5CofCount2( word t, int x, int y, int * Pla2Var, word t0, int fDerive )
{
- int i, Mask;
+ int m, i, Mask;
assert( x >= 0 && x < 4 );
assert( y >= 0 && y < 4 );
+ for ( m = 0; m < 4; m++ )
+ {
+ for ( Mask = i = 0; i < 16; i++ )
+ if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
+ Mask |= (1 << ((t >> (i<<1)) & 3));
+ if ( BitCount8[Mask & 0xF] > 2 )
+ return 0;
+ }
+// Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
+ if ( !fDerive )
+ return 1;
+ else
+ {
+ int fHas2, fHas3;
+ // composition function C depends on {x, y, Out, v[0]}
+ // decomposed function D depends on {x, y, z1, z2}
+ word F[4] = { 0, ABC_CONST(0x5555555555555555), ABC_CONST(0xAAAAAAAAAAAAAAAA), ~((word)0) };
+ word C2[4], D2[4] = {0}, C1[2], D1[2], C, D, z;
+ int v, zz1 = -1, zz2 = -1;
+ // find two variables
+ for ( v = 0; v < 4; v++ )
+ if ( v != x && v != y )
+ { zz1 = v; break; }
+ for ( v = 1; v < 4; v++ )
+ if ( v != x && v != y && v != zz1 )
+ { zz2 = v; break; }
+ assert( zz1 != -1 && zz2 != -1 );
+ // find the cofactors
+ for ( m = 0; m < 4; m++ )
+ {
+ // for each cofactor, derive C2 and D2
+ for ( Mask = i = 0; i < 16; i++ )
+ if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
+ Mask |= (1 << ((t >> (i<<1)) & 3));
+ // find the values
+ if ( BitCount8[Mask & 0xF] == 1 )
+ {
+ C2[m] = F[Abc_Tt6FirstBit( Mask )];
+ D2[m] = ~(word)0;
+ }
+ else if ( BitCount8[Mask & 0xF] == 2 )
+ {
+ int Bit0 = Abc_Tt6FirstBit( Mask );
+ int Bit1 = Abc_Tt6FirstBit( Mask ^ (((word)1)<<Bit0) );
+ C2[m] = (F[Bit1] & Truth6[1]) | (F[Bit0] & ~Truth6[1]);
+ // find Bit1 appears
+ for ( Mask = i = 0; i < 16; i++ )
+ if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
+ if ( Bit1 == ((t >> (i<<1)) & 3) )
+ D2[m] |= (((word)1) << ( (((i >> zz2) & 1) << 1) | ((i >> zz1) & 1) ));
+ }
+ else assert( 0 );
+ D2[m] = Abc_Tt6Stretch( D2[m], 2 );
+ }
- for ( Mask = i = 0; i < 16; i++ )
- if ( !((i >> x) & 1) && !((i >> y) & 1) )
- Mask |= (1 << ((t >> (i<<1)) & 3));
- if ( BitCount8[Mask & 0xF] > 2 )
- return 0;
-
- for ( Mask = i = 0; i < 16; i++ )
- if ( ((i >> x) & 1) && !((i >> y) & 1) )
- Mask |= (1 << ((t >> (i<<1)) & 3));
- if ( BitCount8[Mask & 0xF] > 2 )
- return 0;
-
- for ( Mask = i = 0; i < 16; i++ )
- if ( !((i >> x) & 1) && ((i >> y) & 1) )
- Mask |= (1 << ((t >> (i<<1)) & 3));
- if ( BitCount8[Mask & 0xF] > 2 )
- return 0;
+ // combine
+ C1[0] = (C2[1] & Truth6[2]) | (C2[0] & ~Truth6[2]);
+ C1[1] = (C2[3] & Truth6[2]) | (C2[2] & ~Truth6[2]);
+ C = (C1[1] & Truth6[3]) | (C1[0] & ~Truth6[3]);
+
+ // combine
+ D1[0] = (D2[1] & Truth6[2]) | (D2[0] & ~Truth6[2]);
+ D1[1] = (D2[3] & Truth6[2]) | (D2[2] & ~Truth6[2]);
+ D = (D1[1] & Truth6[3]) | (D1[0] & ~Truth6[3]);
+
+// printf( "\n" );
+// Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n");
+// Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n");
+
+ // create configuration
+ // find one
+ fHas2 = Abc_TtHasVar(&D, 5, 2);
+ fHas3 = Abc_TtHasVar(&D, 5, 3);
+ if ( fHas2 && fHas3 )
+ {
+ z = D & 0xFFFF;
+ z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
+ z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
+ z |= (((word)Pla2Var[x+1]) << (16 + 4*2));
+ z |= (((word)Pla2Var[y+1]) << (16 + 4*3));
+ }
+ else if ( fHas2 && !fHas3 )
+ {
+ z = D & 0xFFFF;
+ z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
+ z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
+ z |= (((word)Pla2Var[x+1]) << (16 + 4*2));
+ z |= (((word)6) << (16 + 4*3));
+ }
+ else if ( !fHas2 && fHas3 )
+ {
+ Abc_TtSwapVars( &D, 5, 2, 3 );
+ z = D & 0xFFFF;
+ z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
+ z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
+ z |= (((word)Pla2Var[y+1]) << (16 + 4*2));
+ z |= (((word)6) << (16 + 4*3));
+ }
+ else
+ {
+ z = D & 0xFFFF;
+ z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
+ z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
+ z |= (((word)6) << (16 + 4*2));
+ z |= (((word)6) << (16 + 4*3));
+ }
- for ( Mask = i = 0; i < 16; i++ )
- if ( ((i >> x) & 1) && ((i >> y) & 1) )
- Mask |= (1 << ((t >> (i<<1)) & 3));
- if ( BitCount8[Mask & 0xF] > 2 )
- return 0;
+ // second one
+ fHas2 = Abc_TtHasVar(&C, 5, 2);
+ fHas3 = Abc_TtHasVar(&C, 5, 3);
+ if ( fHas2 && fHas3 )
+ {
+ z |= ((C & 0xFFFF) << 32);
+ z |= (((word)Pla2Var[0]) << (48 + 4*0));
+ z |= (((word)7) << (48 + 4*1));
+ z |= (((word)Pla2Var[x+1]) << (48 + 4*2));
+ z |= (((word)Pla2Var[y+1]) << (48 + 4*3));
+ }
+ else if ( fHas2 && !fHas3 )
+ {
+ z |= ((C & 0xFFFF) << 32);
+ z |= (((word)Pla2Var[0]) << (48 + 4*0));
+ z |= (((word)7) << (48 + 4*1));
+ z |= (((word)Pla2Var[x+1]) << (48 + 4*2));
+ z |= (((word)6) << (48 + 4*3));
+ }
+ else if ( !fHas2 && fHas3 )
+ {
+ Abc_TtSwapVars( &C, 5, 2, 3 );
+ z |= ((C & 0xFFFF) << 32);
+ z |= (((word)Pla2Var[0]) << (48 + 4*0));
+ z |= (((word)7) << (48 + 4*1));
+ z |= (((word)Pla2Var[y+1]) << (48 + 4*2));
+ z |= (((word)6) << (48 + 4*3));
+ }
+ else
+ {
+ z |= ((C & 0xFFFF) << 32);
+ z |= (((word)Pla2Var[0]) << (48 + 4*0));
+ z |= (((word)7) << (48 + 4*1));
+ z |= (((word)6) << (48 + 4*2));
+ z |= (((word)6) << (48 + 4*3));
+ }
- return 1;
+ // verify
+ {
+ word t1 = If_Dec6Truth( z );
+ if ( t1 != t0 )
+ {
+ printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)&C2[0], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&C2[1], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&C2[2], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&C2[3], 5 ); printf("\n");
+
+ printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)&D2[0], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&D2[1], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&D2[2], 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&D2[3], 5 ); printf("\n");
+
+ printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n");
+
+ printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)&t1, 5 ); printf("\n");
+ Kit_DsdPrintFromTruth( (unsigned *)&t0, 5 ); printf("\n");
+ }
+ assert( t1 == t0 );
+ }
+ return z;
+ }
}
word If_Dec5Perform( word t, int fDerive )
{
int Pla2Var[7], Var2Pla[7];
int i, j, v;
-// word t0 = t;
+ word t0 = t;
+/*
word c0, c1, c00, c01, c10, c11;
for ( i = 0; i < 5; i++ )
{
@@ -752,6 +910,7 @@ word If_Dec5Perform( word t, int fDerive )
return 1;
}
}
+*/
// start arrays
for ( i = 0; i < 7; i++ )
Pla2Var[i] = Var2Pla[i] = i;
@@ -762,9 +921,21 @@ word If_Dec5Perform( word t, int fDerive )
If_DecVerifyPerm( Pla2Var, Var2Pla );
for ( i = 0; i < 4; i++ )
for ( j = i + 1; j < 4; j++ )
- if ( If_Dec5CofCount2( t, i, j ) )
- return 1;
+ {
+ word z = If_Dec5CofCount2( t, i, j, Pla2Var, t0, fDerive );
+ if ( z )
+ {
+/*
+ if ( v == 0 && i == 1 && j == 2 )
+ {
+ Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
+ }
+*/
+ return z;
+ }
+ }
}
+
/*
// start arrays
for ( i = 0; i < 7; i++ )
@@ -808,10 +979,42 @@ word If_Dec5Perform( word t, int fDerive )
}
}
*/
+
// Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
return 0;
}
+word If_Dec5PerformEx()
+{
+ word z;
+ // find one
+ z = 0x17ac & 0xFFFF;
+ z |= (((word)3) << (16 + 4*0));
+ z |= (((word)4) << (16 + 4*1));
+ z |= (((word)1) << (16 + 4*2));
+ z |= (((word)2) << (16 + 4*3));
+ // second one
+ z |= ((0x179a & 0xFFFF) << 32);
+ z |= (((word)0) << (48 + 4*0));
+ z |= (((word)7) << (48 + 4*1));
+ z |= (((word)1) << (48 + 4*2));
+ z |= (((word)2) << (48 + 4*3));
+ return z;
+}
+void If_Dec5PerformTest()
+{
+ word z, t, t1;
+// s = If_Dec5PerformEx();
+// t = If_Dec6Truth( s );
+ t = 0xB0F3B0FFB0F3B0FF;
+
+ Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf("\n");
+
+ z = If_Dec5Perform( t, 1 );
+ t1 = If_Dec6Truth( z );
+ assert( t == t1 );
+}
+
/**Function*************************************************************
@@ -830,18 +1033,14 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea
return 1;
if ( nLeaves == 5 )
{
- word z, t = ((word *)pTruth)[0];
-// if ( If_Dec6CheckMux(t) >= 0 )
-// return 1;
- z = If_Dec6Perform( t, 1 );
+ word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
+ z = If_Dec5Perform( t, 1 );
If_Dec6Verify( t, z );
return z;
}
if ( nLeaves == 6 )
{
word z, t = ((word *)pTruth)[0];
-// if ( If_Dec6CheckMux(t) >= 0 )
-// return 1;
z = If_Dec6Perform( t, 1 );
If_Dec6Verify( t, z );
return z;
@@ -851,8 +1050,6 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea
word z, t[2];
t[0] = ((word *)pTruth)[0];
t[1] = ((word *)pTruth)[1];
- if ( If_Dec7CheckMux(t) >= 0 )
- return 1;
z = If_Dec7Perform( t, 1 );
If_Dec7Verify( t, z );
return z;
@@ -875,26 +1072,33 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea
int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
int fDerive = 0;
+ int v;
+ // skip non-support minimal
+ for ( v = 0; v < nLeaves; v++ )
+ if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) )
+ return 0;
+ // check
if ( nLeaves < 5 )
return 1;
if ( nLeaves == 5 )
{
- word t = ((word)pTruth[0] << 32) | (word)pTruth[0];
- if ( If_Dec5Perform( t, fDerive ) )
- return 1;
- return 0;
+ word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
+ z = If_Dec5Perform( t, fDerive );
+ if ( fDerive && z )
+ If_Dec6Verify( t, z );
+ return z != 0;
}
if ( nLeaves == 6 )
{
word z, t = ((word *)pTruth)[0];
- if ( If_Dec6CheckMux(t) >= 0 )
- return 1;
z = If_Dec6Perform( t, fDerive );
if ( fDerive && z )
{
// If_DecPrintConfig( z );
If_Dec6Verify( t, z );
}
+ if ( z == 0 )
+ Extra_PrintHex(stdout, (unsigned *)&t, 6), printf( " " ), Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
return z != 0;
}
if ( nLeaves == 7 )
@@ -902,8 +1106,8 @@ int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave
word z, t[2];
t[0] = ((word *)pTruth)[0];
t[1] = ((word *)pTruth)[1];
- if ( If_Dec7CheckMux(t) >= 0 )
- return 1;
+// if ( If_Dec7CheckMux(t) >= 0 )
+// return 1;
z = If_Dec7Perform( t, fDerive );
if ( fDerive && z )
If_Dec7Verify( t, z );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 07f36382..cded2ce8 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1064,6 +1064,19 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
return;
}
}
+// moves one var (v) to the given position (p)
+static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p )
+{
+ int iVar = V2P[v], jVar = p;
+ if ( iVar == jVar )
+ return;
+ Abc_TtSwapVars( pF, nVars, iVar, jVar );
+ V2P[P2V[iVar]] = jVar;
+ V2P[P2V[jVar]] = iVar;
+ P2V[iVar] ^= P2V[jVar];
+ P2V[jVar] ^= P2V[iVar];
+ P2V[iVar] ^= P2V[jVar];
+}
/**Function*************************************************************
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index dc34a22a..7ffe63be 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -1900,7 +1900,9 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteT
void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit )
{
char pRes[DAU_MAX_STR];
- Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes );
+ word pTemp[DAU_MAX_WORD];
+ Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
+ Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( pFile, "%s\n", pRes );
}
diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c
new file mode 100644
index 00000000..65821027
--- /dev/null
+++ b/src/opt/dau/dauNonDsd.c
@@ -0,0 +1,642 @@
+/**CFile****************************************************************
+
+ FileName [dauNonDsd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware unmapping.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: dauNonDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dauInt.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// the bit count for the first 256 integer numbers
+static int BitCount8[256] = {
+ 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+static inline BitCount16( int i ) { return BitCount8[i & 0xFF] + BitCount8[i >> 8]; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Checks decomposability with given BS variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Dau_DecGetMinterm( word * p, int g, int nVarsS, int uMaskAll )
+{
+ int m, c, v;
+ for ( m = c = v = 0; v < nVarsS; v++ )
+ if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable
+ {
+ if ( (g >> v) & 1 )
+ m |= (1 << c);
+ c++;
+ }
+ assert( c >= 2 );
+ p[m>>6] |= (((word)1)<<(m & 63));
+}
+static inline int Dau_DecCheckSet5( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+ int fFound0 = 0, fFound1 = 0;
+ int g, gMax = (1 << (nVars - nVarsF));
+ int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1;
+ word Mask2 = (((word)1) << (1 << nVarsF)) - 1;
+ word Cof0 = 0, Cof1 = 0, Value;
+ assert( nVarsF >= 1 && nVarsF <= 5 );
+ if ( pDec ) *pDec = 0;
+ for ( g = 0; g < gMax; g++ )
+ if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue
+ {
+ Value = (p[g>>Shift] >> ((g&Mask)<<nVarsF)) & Mask2;
+ if ( !fFound0 )
+ Cof0 = Value, fFound0 = 1;
+ else if ( Cof0 == Value )
+ continue;
+ else if ( !fFound1 )
+ {
+ Cof1 = Value, fFound1 = 1;
+ if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+ }
+ else if ( Cof1 == Value )
+ {
+ if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+ continue;
+ }
+ else
+ return 0;
+ }
+ if ( pCof0 )
+ {
+ assert( fFound0 );
+ Cof1 = fFound1 ? Cof1 : Cof0;
+ *pCof0 = Abc_Tt6Stretch( Cof0, nVarsF );
+ *pCof1 = Abc_Tt6Stretch( Cof1, nVarsF );
+ }
+ return 1;
+}
+static inline int Dau_DecCheckSet6( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+ int fFound0 = 0, fFound1 = 0;
+ int g, gMax = (1 << (nVars - nVarsF));
+ int nWords = Abc_TtWordNum(nVarsF);
+ word * Cof0 = NULL, * Cof1 = NULL;
+ assert( nVarsF >= 6 && nVarsF <= nVars - 2 );
+ if ( pDec ) *pDec = 0;
+ for ( g = 0; g < gMax; g++ )
+ if ( (g & uMaskAll) == uMaskValue )
+ {
+ if ( !fFound0 )
+ Cof0 = p + g * nWords, fFound0 = 1;
+ else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) )
+ continue;
+ else if ( !fFound1 )
+ {
+ Cof1 = p + g * nWords, fFound1 = 1;
+ if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+ }
+ else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) )
+ {
+ if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+ continue;
+ }
+ else
+ return 0;
+ }
+ if ( pCof0 )
+ {
+ assert( fFound0 );
+ Cof1 = fFound1 ? Cof1 : Cof0;
+ memcpy( pCof0, Cof0, sizeof(word) * nWords );
+ memcpy( pCof1, Cof1, sizeof(word) * nWords );
+ }
+ return 1;
+}
+static inline int Dau_DecCheckSetAny( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+ assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
+ if ( nVarsF < 6 )
+ return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
+ else
+ return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
+}
+int Dau_DecCheckSetTop( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word ** pCof0, word ** pCof1, word ** pDec )
+{
+ int i, pVarsS[16];
+ int v, m, mMax = (1 << nVarsS), uMaskValue;
+ assert( nVars >= 3 && nVars <= 16 );
+ assert( nVars == nVarsF + nVarsB );
+ assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
+ assert( nVarsB >= 2 && nVarsB <= nVars - 1 );
+ assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 );
+ if ( nVarsS == 0 )
+ return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 );
+ // collect shared variables
+ assert( maskS > 0 && maskS < (1 << nVarsB) );
+ for ( i = 0, v = 0; v < nVarsB; v++ )
+ if ( (maskS >> v) & 1 )
+ pVarsS[i++] = v;
+ assert( i == nVarsS );
+ // go through shared set minterms
+ for ( m = 0; m < mMax; m++ )
+ {
+ // generate share set mask
+ uMaskValue = 0;
+ for ( v = 0; v < nVarsS; v++ )
+ if ( (m >> v) & 1 )
+ uMaskValue |= (1 << pVarsS[v]);
+ assert( (maskS & uMaskValue) == uMaskValue );
+ // check decomposition
+ if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) )
+ return 0;
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Variable sets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Dau_DecCreateSet( int * pVarsB, int sizeB, int maskS )
+{
+ unsigned uSet = 0; int v;
+ for ( v = 0; v < sizeB; v++ )
+ {
+ uSet |= (1 << (pVarsB[v] << 1));
+ if ( (maskS >> v) & 1 )
+ uSet |= (1 << ((pVarsB[v] << 1)+1));
+ }
+ return uSet;
+}
+static inline int Dau_DecSetHas01( unsigned Mask )
+{
+ return (Mask & ((~Mask) >> 1) & 0x55555555);
+}
+static inline int Dau_DecSetIsContained( Vec_Int_t * vSets, unsigned New )
+// Old=abcD contains New=abcDE
+// Old=abcD contains New=abCD
+{
+ unsigned Old;
+ int i, Entry;
+ Vec_IntForEachEntry( vSets, Entry, i )
+ {
+ Old = (unsigned)Entry;
+ if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New))
+ return 1;
+ }
+ return 0;
+}
+void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine )
+{
+ int v, Counter = 0;
+ int nUnique = 0, nShared = 0, nFree = 0;
+ for ( v = 0; v < nVars; v++ )
+ {
+ int Value = ((set >> (v << 1)) & 3);
+ if ( Value == 1 )
+ nUnique++;
+ else if ( Value == 3 )
+ nShared++;
+ else if ( Value == 0 )
+ nFree++;
+ else assert( 0 );
+ }
+ printf( "S =%2d D =%2d C =%2d ", nShared, nUnique+nShared, nShared+nFree+1 );
+
+ printf( "x=" );
+ for ( v = 0; v < nVars; v++ )
+ {
+ int Value = ((set >> (v << 1)) & 3);
+ if ( Value == 1 )
+ printf( "%c", 'a' + v ), Counter++;
+ else if ( Value == 3 )
+ printf( "%c", 'A' + v ), Counter++;
+ else assert( Value == 0 );
+ }
+ printf( " y=x" );
+ for ( v = 0; v < nVars; v++ )
+ {
+ int Value = ((set >> (v << 1)) & 3);
+ if ( Value == 0 )
+ printf( "%c", 'a' + v ), Counter++;
+ else if ( Value == 3 )
+ printf( "%c", 'A' + v ), Counter++;
+ }
+ for ( ; Counter < 15; Counter++ )
+ printf( " " );
+ if ( fNewLine )
+ printf( "\n" );
+}
+unsigned Dau_DecReadSet( char * pStr )
+{
+ unsigned uSet = 0; int v;
+ for ( v = 0; pStr[v]; v++ )
+ {
+ if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
+ uSet |= (1 << ((pStr[v] - 'a') << 1));
+ else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' )
+ uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1));
+ else break;
+ }
+ return uSet;
+}
+void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars )
+{
+ int i, Entry;
+ printf( "The set contains %d entries:\n", Vec_IntSize(vSets) );
+ Vec_IntForEachEntry( vSets, Entry, i )
+ Dau_DecPrintSet( (unsigned)Entry, nVars, 1 );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find decomposable bound-sets of the given function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, int sizeB )
+{
+ int v, c = 0;
+ for ( v = 0; v < nVars; v++ )
+ if ( !((maskB >> v) & 1) )
+ Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
+ assert( c == nVars - sizeB );
+}
+Vec_Int_t * Dau_DecFindSets( word * p, int nVars )
+{
+ Vec_Int_t * vSets = Vec_IntAlloc( 32 );
+ int V2P[16], P2V[16], pVarsB[16];
+ int Limit = (1 << nVars);
+ int c, v, sizeB, sizeS, maskB, maskS;
+ unsigned setMixed;
+ for ( v = 0; v < nVars; v++ )
+ assert( Abc_TtHasVar( p, nVars, v ) );
+ // initialize permutation
+ for ( v = 0; v < nVars; v++ )
+ V2P[v] = P2V[v] = v;
+ // iterate through bound sets of each size in increasing order
+ for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size
+ for ( maskB = 0; maskB < Limit; maskB++ ) // bound set
+ if ( BitCount16(maskB) == sizeB )
+ {
+ // permute variables to have bound set on top
+ Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB );
+ // collect bound set vars on levels nVars-sizeB to nVars-1
+ for ( c = 0; c < sizeB; c++ )
+ pVarsB[c] = P2V[nVars-sizeB+c];
+ // check disjoint
+ if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) )
+ {
+ Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) );
+ continue;
+ }
+ if ( sizeB == 2 )
+ continue;
+ // iterate through shared sets of each size in the increasing order
+ for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ ) // shared set size
+// sizeS = 1;
+ for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set
+ if ( BitCount16(maskS) == sizeS )
+ {
+ setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS );
+// printf( "Considering %10d ", setMixed );
+// Dau_DecPrintSet( setMixed, nVars );
+ // check if it exists
+ if ( Dau_DecSetIsContained(vSets, setMixed) )
+ continue;
+ // check if it can be added
+ if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) )
+ Vec_IntPush( vSets, setMixed );
+ }
+ }
+ return vSets;
+}
+void Dau_DecFindSetsTest2()
+{
+ Vec_Int_t * vSets;
+ word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+ word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+ word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
+// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
+// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
+// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
+// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
+ int nVars = 5;
+
+ vSets = Dau_DecFindSets( &t, nVars );
+ Dau_DecPrintSets( vSets, nVars );
+ Vec_IntFree( vSets );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Replaces variables in the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_DecVarReplace( char * pStr, int * pPerm, int nVars )
+{
+ int v;
+ for ( v = 0; pStr[v]; v++ )
+ if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
+ {
+ assert( pStr[v] - 'a' < nVars );
+ pStr[v] = 'a' + pPerm[pStr[v] - 'a'];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Decomposes with the given bound-set.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dau_DecDecomposeSet( word * pInit, int nVars, unsigned uSet, word * pComp, word * pDec, int * pPermC, int * pPermD, int * pnVarsC, int * pnVarsD )
+{
+ word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64];
+ word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD;
+ int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16];
+ int nVarsU = 0, nVarsS = 0, nVarsF = 0;
+ int nWords = Abc_TtWordNum(nVars);
+ int v, d, c, Status, nDecs;
+ assert( nVars <= 16 );
+ for ( v = 0; v < nVars; v++ )
+ V2P[v] = P2V[v] = v;
+ memcpy( p, pInit, sizeof(word) * nWords );
+ // sort variables
+ for ( v = 0; v < nVars; v++ )
+ {
+ int Value = (uSet >> (v<<1)) & 3;
+ if ( Value == 0 )
+ pVarsF[nVarsF++] = v;
+ else if ( Value == 1 )
+ pVarsU[nVarsU++] = v;
+ else if ( Value == 3 )
+ pVarsS[nVarsS++] = v;
+ else assert(0);
+ }
+ assert( nVarsS >= 0 && nVarsS <= 6 );
+ assert( nVarsF + nVarsS + 1 <= 6 );
+ assert( nVarsU + nVarsS <= 6 );
+ // init space for decomposition functions
+ nDecs = (1 << nVarsS);
+ for ( d = 0; d < nDecs; d++ )
+ {
+ pCof0[d] = Cof0 + d;
+ pCof1[d] = Cof1 + d;
+ pDecs[d] = Decs + d;
+ }
+ // permute variables
+ c = 0;
+ for ( v = 0; v < nVarsF; v++ )
+ Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ );
+ for ( v = 0; v < nVarsS; v++ )
+ Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ );
+ for ( v = 0; v < nVarsU; v++ )
+ Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ );
+ assert( c == nVars );
+ // check decomposition
+ Status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs );
+ if ( !Status )
+ return 0;
+ // compute cofactors
+ assert( nVarsF + nVarsS < 6 );
+ for ( d = 0; d < nDecs; d++ )
+ {
+ Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]);
+ pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU );
+ }
+ // compute the resulting functions
+ pComp[0] = 0;
+ pDec[0] = 0;
+ for ( d = 0; d < nDecs; d++ )
+ {
+ // compute minterms for composition/decomposition function
+ MintC = MintD = ~((word)0);
+ for ( v = 0; v < nVarsS; v++ )
+ {
+ MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
+ MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
+ }
+ // derive functions
+ pComp[0] |= MintC & Cof[d];
+ pDec[0] |= MintD & pDecs[d][0];
+ }
+ // derive variable permutations
+ if ( pPermC )
+ {
+ for ( v = 0; v < nVarsF; v++ )
+ pPermC[v] = pVarsF[v];
+ for ( v = 0; v < nVarsS; v++ )
+ pPermC[nVarsF+v] = pVarsS[v];
+ pPermC[nVarsF + nVarsS] = nVars;
+ }
+ if ( pPermD )
+ {
+ for ( v = 0; v < nVarsU; v++ )
+ pPermD[v] = pVarsU[v];
+ for ( v = 0; v < nVarsS; v++ )
+ pPermD[nVarsU+v] = pVarsS[v];
+ }
+ if ( pnVarsC )
+ *pnVarsC = nVarsF + nVarsS + 1;
+ if ( pnVarsD )
+ *pnVarsD = nVarsU + nVarsS;
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Testing procedures.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD )
+{
+ word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16
+ int nWordsC = Abc_TtWordNum(nVars+1);
+ int nWordsD = Abc_TtWordNum(nVars);
+ assert( nVars < 16 );
+ memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC );
+ memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD );
+// Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" );
+// Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" );
+ if ( nVars >= 6 )
+ {
+ assert( nWordsD >= 1 );
+ assert( nWordsC > 1 );
+ Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD );
+ }
+ else
+ {
+ word pC0 = Abc_Tt6Stretch( pC[0], nVars );
+ word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars );
+ Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD );
+ }
+ if ( Abc_TtEqual(pInit, pRes, nWordsD) )
+ printf( " Verification successful\n" );
+ else
+ printf( " Verification failed\n" );
+ return 1;
+}
+int Dau_DecPerform( word * p, int nVars, unsigned uSet )
+{
+ word tComp = 0, tDec = 0;
+ char pDsdC[1000], pDsdD[1000];
+ int pPermC[16], pPermD[16], nVarsC, nVarsD;
+ int status, ResC, ResD;
+ status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec, pPermC, pPermD, &nVarsC, &nVarsD );
+// Dau_DecPrintSet( uSet, nVars );
+// printf( "Decomposition %s\n", status ? "exists" : "does not exist" );
+ if ( !status )
+ {
+ printf( " Decomposition does not exist\n" );
+ return 0;
+ }
+// Dau_DsdPrintFromTruth( stdout, p, nVars ); //printf( "\n" );
+// Dau_DsdPrintFromTruth( stdout, &tComp, nVars ); //printf( "\n" );
+// Dau_DsdPrintFromTruth( stdout, &tDec, nVars ); //printf( "\n" );
+ // decompose
+ ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC );
+ ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD );
+/*
+ printf( "%s\n", pDsdC );
+ printf( "%s\n", pDsdD );
+ for ( v = 0; v < nVarsC; v++ )
+ printf( "%d ", pPermC[v] );
+ printf( "\n" );
+ for ( v = 0; v < nVarsD; v++ )
+ printf( "%d ", pPermD[v] );
+ printf( "\n" );
+*/
+ // replace variables
+ Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
+ Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
+ printf( "%24s ", pDsdD );
+ printf( "%24s ", pDsdC );
+ Dau_DecVerify( p, nVars, pDsdC, pDsdD );
+ return 1;
+}
+void Dau_DecTrySets( word * p, int nVars )
+{
+ Vec_Int_t * vSets;
+ word t0 = *p;
+ int i, Entry;
+ vSets = Dau_DecFindSets( p, nVars );
+ Dau_DsdPrintFromTruth( stdout, &t0, nVars );
+ printf( "There are %d support-reducing decompositions:\n", Vec_IntSize(vSets) );
+ Vec_IntForEachEntry( vSets, Entry, i )
+ {
+ unsigned uSet = (unsigned)Entry;
+ Dau_DecPrintSet( uSet, nVars, 0 );
+ Dau_DecPerform( &t0, nVars, uSet );
+ }
+// printf( "\n" );
+ Vec_IntFree( vSets );
+}
+
+void Dau_DecFindSetsTest3()
+{
+ word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+ word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+ word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
+// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+ int nVars = 6;
+ char * pStr = "Bcd";
+// char * pStr = "Abcd";
+// char * pStr = "ab";
+ unsigned uSet = Dau_DecReadSet( pStr );
+ Dau_DecPerform( &t, nVars, uSet );
+}
+
+void Dau_DecFindSetsTest()
+{
+ int nVars = 6;
+// word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+// word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+// word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
+// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
+// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
+// word t = ABC_CONST(0x00000000901FFFFF); // some funct
+ word t = ABC_CONST(0x000030F00D0D3FFF); // some funct
+// word t = ABC_CONST(0x00000000690006FF); // some funct
+// word t = ABC_CONST(0x7000F80007FF0FFF); // some funct
+// word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var
+// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
+// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
+ Dau_DecTrySets( &t, nVars );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make
index f339810b..190e30e4 100644
--- a/src/opt/dau/module.make
+++ b/src/opt/dau/module.make
@@ -5,4 +5,5 @@ SRC += src/opt/dau/dauCanon.c \
src/opt/dau/dauEnum.c \
src/opt/dau/dauGia.c \
src/opt/dau/dauMerge.c \
+ src/opt/dau/dauNonDsd.c \
src/opt/dau/dauTree.c
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 13:00:16 +0000