summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/aig/gia/giaIf.c20
-rw-r--r--src/base/abci/abc.c25
-rw-r--r--src/base/abci/abcDec.c3
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/map/if/ifDsd.c73
-rw-r--r--src/misc/extra/extraUtilThresh.c333
-rw-r--r--src/misc/extra/module.make1
-rw-r--r--src/misc/util/utilIsop.c58
-rw-r--r--src/misc/util/utilTruth.h95
10 files changed, 548 insertions, 65 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 4b6575c7..120d898a 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2795,6 +2795,10 @@ SOURCE=.\src\misc\extra\extraUtilSupp.c
# End Source File
# Begin Source File
+SOURCE=.\src\misc\extra\extraUtilThresh.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\misc\extra\extraUtilTruth.c
# End Source File
# Begin Source File
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index a5eafb5f..131dfd11 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -366,15 +366,16 @@ void Gia_ManPrintGetMuxFanins( Gia_Man_t * p, Gia_Obj_t * pObj, int * pFanins )
pFanins[1] = Gia_ObjId(p, Gia_Regular(pData1));
pFanins[2] = Gia_ObjId(p, Gia_Regular(pData0));
}
-int Gia_ManCountDupLut6( Gia_Man_t * p )
+int Gia_ManCountDupLut( Gia_Man_t * p )
{
int i, nCountDup = 0, nCountPis = 0, nCountMux = 0;
Gia_ManCleanMark01( p );
Gia_ManForEachLut( p, i )
- if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutIsMux(p, i) )
+ if ( Gia_ObjLutIsMux(p, i) )
{
Gia_Obj_t * pFanin;
int pFanins[3];
+ assert( Gia_ObjLutSize(p, i) == 2 || Gia_ObjLutSize(p, i) == 3 );
Gia_ManPrintGetMuxFanins( p, Gia_ManObj(p, i), pFanins );
Gia_ManObj(p, i)->fMark1 = 1;
@@ -401,21 +402,22 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
{
Gia_Obj_t * pObj;
int * pLevels;
- int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0, Ave = 0, nMuxF7 = 0;
+ int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0, Ave = 0, nMuxF = 0;
if ( !Gia_ManHasMapping(p) )
return;
pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachLut( p, i )
{
- if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutIsMux(p, i) )
+ if ( Gia_ObjLutIsMux(p, i) )
{
int pFanins[3];
+ assert( Gia_ObjLutSize(p, i) == 2 || Gia_ObjLutSize(p, i) == 3 );
Gia_ManPrintGetMuxFanins( p, Gia_ManObj(p, i), pFanins );
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[pFanins[0]]+1 );
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[pFanins[1]] );
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[pFanins[2]] );
LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
- nMuxF7++;
+ nMuxF++;
nFanins++;
continue;
}
@@ -437,8 +439,8 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
Abc_Print( 1, "Mapping (K=%d) : ", nLutSize );
SetConsoleTextAttribute( hConsole, 14 ); // yellow
Abc_Print( 1, "lut =%7d ", nLuts );
- if ( nMuxF7 )
- Abc_Print( 1, "mux =%7d ", nMuxF7 );
+ if ( nMuxF )
+ Abc_Print( 1, "muxF =%7d ", nMuxF );
SetConsoleTextAttribute( hConsole, 10 ); // green
Abc_Print( 1, "edge =%8d ", nFanins );
SetConsoleTextAttribute( hConsole, 12 ); // red
@@ -464,8 +466,8 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
Abc_Print( 1, "\n" );
#endif
- if ( nMuxF7 )
- Gia_ManCountDupLut6( p );
+ if ( nMuxF )
+ Gia_ManCountDupLut( p );
if ( pDumpFile )
{
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 15bfc76b..3408144a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16256,10 +16256,11 @@ usage:
***********************************************************************/
int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose );
If_DsdMan_t * pDsd = (If_DsdMan_t *)Abc_FrameReadManDsd();
- int c, nLimit = 0, nLutSize = -1, fCleanOccur = 0, fCleanMarks = 0, fVerbose = 0;
+ int c, nLimit = 0, nLutSize = -1, fCleanOccur = 0, fCleanMarks = 0, fInvMarks = 0, fUnate = 0, fThresh = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "LKomvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LKomiutvh" ) ) != EOF )
{
switch ( c )
{
@@ -16287,6 +16288,15 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fCleanMarks ^= 1;
break;
+ case 'i':
+ fInvMarks ^= 1;
+ break;
+ case 'u':
+ fUnate ^= 1;
+ break;
+ case 't':
+ fThresh ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -16309,15 +16319,24 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
If_DsdManCleanOccur( pDsd, fVerbose );
if ( fCleanMarks )
If_DsdManCleanMarks( pDsd, fVerbose );
+ if ( fInvMarks )
+ If_DsdManInvertMarks( pDsd, fVerbose );
+ if ( fUnate )
+ Id_DsdManTuneThresh( pDsd, 1, 0, fVerbose );
+ if ( fThresh )
+ Id_DsdManTuneThresh( pDsd, 0, 1, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: dsd_filter [-LK num] [-omvh]\n" );
+ Abc_Print( -2, "usage: dsd_filter [-LK num] [-omiutvh]\n" );
Abc_Print( -2, "\t filtering structured and modifying parameters of DSD manager\n" );
Abc_Print( -2, "\t-L num : remove structures with fewer occurrences that this [default = %d]\n", nLimit );
Abc_Print( -2, "\t-K num : new LUT size to set for the DSD manager [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-o : toggles cleaning occurrence counters [default = %s]\n", fCleanOccur? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cleaning matching marks [default = %s]\n", fCleanMarks? "yes": "no" );
+ Abc_Print( -2, "\t-i : toggles inverting matching marks [default = %s]\n", fInvMarks? "yes": "no" );
+ Abc_Print( -2, "\t-u : toggles marking unate functions [default = %s]\n", fUnate? "yes": "no" );
+ Abc_Print( -2, "\t-t : toggles marking threshold functions [default = %s]\n", fThresh? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 3ed73c26..5e4f848a 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -502,6 +502,9 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
vCover = Vec_IntAlloc( 1 << 16 );
for ( i = 0; i < p->nFuncs; i++ )
{
+// extern int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover );
+// Abc_IsopTest( p->pFuncs[i], p->nVars, vCover );
+// continue;
if ( fVerbose )
printf( "%7d : ", i );
pSopStr = Kit_PlaFromTruthNew( (unsigned *)p->pFuncs[i], p->nVars, vCover, vStr );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 909a54ce..d77ac536 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -550,6 +550,7 @@ extern If_DsdMan_t * If_DsdManLoad( char * pFileName );
extern void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew );
extern void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose );
extern void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose );
+extern void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose );
extern If_DsdMan_t * If_DsdManFilter( If_DsdMan_t * p, int Limit );
extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
extern char * If_DsdManFileName( If_DsdMan_t * p );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 90e30287..cfccc362 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -1230,6 +1230,15 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = 0;
}
+void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose )
+{
+ If_DsdObj_t * pObj;
+ int i;
+ ABC_FREE( p->pCellStr );
+ Vec_WrdFreeP( &p->vPerms );
+ If_DsdVecForEachObj( &p->vObjs, pObj, i )
+ pObj->fMark = !pObj->fMark;
+}
void If_DsdManFilter_rec( If_DsdMan_t * pNew, If_DsdMan_t * p, int i, Vec_Int_t * vMap )
{
If_DsdObj_t * pObj;
@@ -2698,6 +2707,70 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
#endif // pthreads are used
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose )
+{
+ extern int Extra_ThreshCheck( word * t, int nVars, int * pW );
+ int fVeryVerbose = 0;
+ int pW[16];
+ ProgressBar * pProgress = NULL;
+ If_DsdObj_t * pObj;
+ word * pTruth, Perm;
+ int i, nVars, Value;
+ abctime clk = Abc_Clock();
+ assert( fUnate != fThresh );
+ if ( p->nObjsPrev > 0 )
+ printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
+ // clean the attributes
+ If_DsdVecForEachObj( &p->vObjs, pObj, i )
+ if ( i >= p->nObjsPrev )
+ pObj->fMark = 0;
+ if ( p->vPerms == NULL )
+ p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
+ else
+ Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
+ pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
+ If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
+ {
+ if ( (i & 0xFF) == 0 )
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ nVars = If_DsdObjSuppSize(pObj);
+ pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+ if ( fVeryVerbose )
+ Dau_DsdPrintFromTruth( pTruth, nVars );
+ if ( fVerbose )
+ printf( "%6d : %2d ", i, nVars );
+ if ( fUnate )
+ Value = Abc_TtIsUnate( pTruth, nVars );
+ else if ( fThresh )
+ Value = Extra_ThreshCheck( pTruth, nVars, pW );
+ Perm = 0;
+ if ( fVeryVerbose )
+ printf( "\n" );
+ if ( Value )
+ If_DsdVecObjSetMark( &p->vObjs, i );
+ else
+ Vec_WrdWriteEntry( p->vPerms, i, Perm );
+ }
+ p->nObjsPrev = 0;
+ p->LutSize = 0;
+ Extra_ProgressBarStop( pProgress );
+ printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVeryVerbose )
+ If_DsdManPrintDistrib( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/extra/extraUtilThresh.c b/src/misc/extra/extraUtilThresh.c
new file mode 100644
index 00000000..88752b7d
--- /dev/null
+++ b/src/misc/extra/extraUtilThresh.c
@@ -0,0 +1,333 @@
+/**CFile****************************************************************
+
+ FileName [extraUtilThresh.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [extra]
+
+ Synopsis [Dealing with threshold functions.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - October 7, 2014.]
+
+ Revision [$Id: extraUtilThresh.c,v 1.0 2014/10/07 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Checks thresholdness of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_ThreshPrintChow( int Chow0, int * pChow, int nVars )
+{
+ int i;
+ for ( i = 0; i < nVars; i++ )
+ printf( "%d ", pChow[i] );
+ printf( " %d\n", Chow0 );
+}
+int Extra_ThreshComputeChow( word * t, int nVars, int * pChow )
+{
+ int i, k, Chow0 = 0, nMints = (1 << nVars);
+ memset( pChow, 0, sizeof(int) * nVars );
+ // compute Chow coefs
+ for ( i = 0; i < nMints; i++ )
+ if ( Abc_TtGetBit(t, i) )
+ for ( Chow0++, k = 0; k < nVars; k++ )
+ if ( (i >> k) & 1 )
+ pChow[k]++;
+ // compute modified Chow coefs
+ for ( k = 0; k < nVars; k++ )
+ pChow[k] = 2 * pChow[k] - Chow0;
+ return Chow0 - (1 << (nVars-1));
+}
+void Extra_ThreshSortByChow( word * t, int nVars, int * pChow )
+{
+ int i, nWords = Abc_TtWordNum(nVars);
+ while ( 1 )
+ {
+ int fChange = 0;
+ for ( i = 0; i < nVars - 1; i++ )
+ {
+ if ( pChow[i] >= pChow[i+1] )
+ continue;
+ ABC_SWAP( int, pChow[i], pChow[i+1] );
+ Abc_TtSwapAdjacent( t, nWords, i );
+ fChange = 1;
+ }
+ if ( !fChange )
+ return;
+ }
+}
+static inline int Extra_ThreshWeightedSum( int * pW, int nVars, int m )
+{
+ int i, Cost = 0;
+ for ( i = 0; i < nVars; i++ )
+ if ( (m >> i) & 1 )
+ Cost += pW[i];
+ return Cost;
+}
+int Extra_ThreshSelectWeights3( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars);
+ assert( nVars == 3 );
+ for ( pW[2] = 1; pW[2] <= nVars; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= nVars; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= nVars; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+// printf( "%c%d ", Abc_TtGetBit(t, m) ? '+' : '-', Extra_ThreshWeightedSum(pW, nVars, m) );
+ }
+// printf( " -%d +%d\n", Lmax, Lmin );
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights4( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars);
+ assert( nVars == 4 );
+ for ( pW[3] = 1; pW[3] <= nVars; pW[3]++ )
+ for ( pW[2] = pW[3]; pW[2] <= nVars; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= nVars; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= nVars; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+ }
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights5( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 0;
+ assert( nVars == 5 );
+ for ( pW[4] = 1; pW[4] <= Limit; pW[4]++ )
+ for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
+ for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+ }
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights6( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 3;
+ assert( nVars == 6 );
+ for ( pW[5] = 1; pW[5] <= Limit; pW[5]++ )
+ for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
+ for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
+ for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+ }
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights7( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 6;
+ assert( nVars == 7 );
+ for ( pW[6] = 1; pW[6] <= Limit; pW[6]++ )
+ for ( pW[5] = pW[6]; pW[5] <= Limit; pW[5]++ )
+ for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
+ for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
+ for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+ }
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights8( word * t, int nVars, int * pW )
+{
+ int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 1; // <<-- incomplete detection to save runtime!
+ assert( nVars == 8 );
+ for ( pW[7] = 1; pW[7] <= Limit; pW[7]++ )
+ for ( pW[6] = pW[7]; pW[6] <= Limit; pW[6]++ )
+ for ( pW[5] = pW[6]; pW[5] <= Limit; pW[5]++ )
+ for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
+ for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
+ for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
+ for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
+ for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
+ {
+ Lmin = 10000; Lmax = 0;
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( Abc_TtGetBit(t, m) )
+ Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
+ else
+ Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
+ if ( Lmax >= Lmin )
+ break;
+ }
+ if ( m < nMints )
+ continue;
+ assert( Lmax < Lmin );
+ return Lmin;
+ }
+ return 0;
+}
+int Extra_ThreshSelectWeights( word * t, int nVars, int * pW )
+{
+ if ( nVars <= 2 )
+ return (t[0] & 0xF) != 6 && (t[0] & 0xF) != 9;
+ if ( nVars == 3 )
+ return Extra_ThreshSelectWeights3( t, nVars, pW );
+ if ( nVars == 4 )
+ return Extra_ThreshSelectWeights4( t, nVars, pW );
+ if ( nVars == 5 )
+ return Extra_ThreshSelectWeights5( t, nVars, pW );
+ if ( nVars == 6 )
+ return Extra_ThreshSelectWeights6( t, nVars, pW );
+ if ( nVars == 7 )
+ return Extra_ThreshSelectWeights7( t, nVars, pW );
+ if ( nVars == 8 )
+ return Extra_ThreshSelectWeights8( t, nVars, pW );
+ return 0;
+}
+int Extra_ThreshCheck( word * t, int nVars, int * pW )
+{
+ int Chow[16], Chow0, nMints = (1 << nVars);
+ if ( !Abc_TtIsUnate(t, nVars) )
+ return 0;
+ Abc_TtMakePosUnate( t, nVars );
+ Chow0 = Extra_ThreshComputeChow( t, nVars, Chow );
+ Extra_ThreshSortByChow( t, nVars, Chow );
+ return Extra_ThreshSelectWeights( t, nVars, pW );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks unateness of a function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_ThreshCheckTest()
+{
+ int nVars = 5;
+ int T, Chow0, Chow[16], Weights[16];
+// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4];
+// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]);
+ word t = (s_Truths6[2] & s_Truths6[1]) | (s_Truths6[2] & s_Truths6[0] & s_Truths6[3]) | (s_Truths6[2] & s_Truths6[0] & ~s_Truths6[4]);
+// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]);
+// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]) |
+// (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[5]);
+ int i;
+ assert( nVars <= 8 );
+ for ( i = 0; i < nVars; i++ )
+ printf( "%d %d %d\n", i, Abc_TtPosVar(&t, nVars, i), Abc_TtNegVar(&t, nVars, i) );
+// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
+ Chow0 = Extra_ThreshComputeChow( &t, nVars, Chow );
+ if ( (T = Extra_ThreshCheck(&t, nVars, Weights)) )
+ Extra_ThreshPrintChow( T, Weights, nVars );
+ else
+ printf( "No threshold\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 1503cec1..87ba8559 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -18,5 +18,6 @@ SRC += src/misc/extra/extraBddAuto.c \
src/misc/extra/extraUtilProgress.c \
src/misc/extra/extraUtilReader.c \
src/misc/extra/extraUtilSupp.c \
+ src/misc/extra/extraUtilTrash.c \
src/misc/extra/extraUtilTruth.c \
src/misc/extra/extraUtilUtil.c
diff --git a/src/misc/util/utilIsop.c b/src/misc/util/utilIsop.c
index f42dcabe..a62fc84d 100644
--- a/src/misc/util/utilIsop.c
+++ b/src/misc/util/utilIsop.c
@@ -95,47 +95,6 @@ static inline void Abc_IsopAddLits( int * pCover, int nCost0, int nCost1, int Va
for ( c = 0; c < nCost1; c++ )
pCover[nCost0+c] |= (1 << Abc_Var2Lit(Var,1));
}
-int Abc_Isop6Cover2( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
-{
- word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
- int Var, nCost0, nCost1, nCost2;
- assert( nVars <= 6 );
- assert( (uOn & ~uOnDc) == 0 );
- if ( uOn == 0 )
- {
- pRes[0] = 0;
- return 0;
- }
- if ( uOnDc == ~(word)0 )
- {
- pRes[0] = ~(word)0;
- if ( pCover ) pCover[0] = 0;
- return (1 << 16);
- }
- assert( nVars > 0 );
- // find the topmost var
- for ( Var = nVars-1; Var >= 0; Var-- )
- if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
- break;
- assert( Var >= 0 );
- // cofactor
- uOn0 = Abc_Tt6Cofactor0( uOn, Var );
- uOn1 = Abc_Tt6Cofactor1( uOn , Var );
- uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
- uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
- // solve for cofactors
- nCost0 = Abc_Isop6Cover2( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
- if ( nCost0 >= nCostLim ) return nCostLim;
- nCost1 = Abc_Isop6Cover2( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
- if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
- nCost2 = Abc_Isop6Cover2( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
- if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
- // derive the final truth table
- *pRes = uRes2 | (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
- assert( (uOn & ~*pRes) == 0 && (*pRes & ~uOnDc) == 0 );
- Abc_IsopAddLits( pCover, nCost0, nCost1, Var );
- return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
-}
int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
{
word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
@@ -164,13 +123,10 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
uOn1 = Abc_Tt6Cofactor1( uOn , Var );
uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
-//R0 = bsop(L0&~(U1 | (L1 & ~U0)),U0,new_varbs)
// solve for cofactors
-// nCost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
- nCost0 = Abc_Isop6Cover( uOn0 & ~(uOnDc1 | (uOn1 & ~uOnDc0)), uOnDc0, &uRes0, Var, nCostLim, pCover );
+ nCost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
if ( nCost0 >= nCostLim ) return nCostLim;
-// nCost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
- nCost1 = Abc_Isop6Cover( uOn1 & ~(uOnDc0 | (uOn0 & ~uOnDc1)), uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
+ nCost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
nCost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
@@ -180,7 +136,6 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
Abc_IsopAddLits( pCover, nCost0, nCost1, Var );
return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
}
-
int Abc_Isop7Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
{
word uOn0, uOn1, uOn2, uOnDc2, uRes0, uRes1, uRes2;
@@ -622,13 +577,11 @@ int Abc_Isop( word * pFunc, int nVars, int Type, int nCubeLim, Vec_Int_t * vCove
***********************************************************************/
int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
{
- int fVerbose = 1;
+ int Cost, fVerbose = 0;
word pRes[1024];
- int Cost;
// if ( fVerbose )
// Dau_DsdPrintFromTruth( pFunc, nVars ), printf( " " );
-
Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
vCover->nSize = Cost >> 16;
assert( vCover->nSize <= vCover->nCap );
@@ -646,7 +599,7 @@ int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
printf( "%5d(%5d) ", Cost >> 16, Cost & 0xFFFF );
Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
-/*
+
Cost = Abc_EsopCheck( pFunc, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
vCover->nSize = Cost >> 16;
assert( vCover->nSize <= vCover->nCap );
@@ -663,12 +616,11 @@ int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
if ( fVerbose )
printf( "%5d(%5d) ", Cost >> 16, Cost & 0xFFFF );
Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
-*/
+
if ( fVerbose )
printf( "\n" );
//Kit_TruthIsopPrintCover( vCover, nVars, 0 );
-
return 1;
}
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 1416034d..0b52b3f4 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1597,6 +1597,101 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
/**Function*************************************************************
+ Synopsis [Checks unateness of a function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_Tt6PosVar( word t, int iVar )
+{
+ return ((t >> (1<<iVar)) & t & s_Truths6Neg[iVar]) == (t & s_Truths6Neg[iVar]);
+}
+static inline int Abc_Tt6NegVar( word t, int iVar )
+{
+ return ((t << (1<<iVar)) & t & s_Truths6[iVar]) == (t & s_Truths6[iVar]);
+}
+static inline int Abc_TtPosVar( word * t, int nVars, int iVar )
+{
+ assert( iVar < nVars );
+ if ( nVars <= 6 )
+ return Abc_Tt6PosVar( t[0], iVar );
+ if ( iVar < 6 )
+ {
+ int i, Shift = (1 << iVar);
+ int nWords = Abc_TtWordNum( nVars );
+ for ( i = 0; i < nWords; i++ )
+ if ( ((t[i] >> Shift) & t[i] & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + Abc_TtWordNum( nVars );
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( t[i] != (t[i] & t[Step+i]) )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtNegVar( word * t, int nVars, int iVar )
+{
+ assert( iVar < nVars );
+ if ( nVars <= 6 )
+ return Abc_Tt6NegVar( t[0], iVar );
+ if ( iVar < 6 )
+ {
+ int i, Shift = (1 << iVar);
+ int nWords = Abc_TtWordNum( nVars );
+ for ( i = 0; i < nWords; i++ )
+ if ( ((t[i] << Shift) & t[i] & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + Abc_TtWordNum( nVars );
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( (t[i] & t[Step+i]) != t[Step+i] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtIsUnate( word * t, int nVars )
+{
+ int i;
+ for ( i = 0; i < nVars; i++ )
+ if ( !Abc_TtNegVar(t, nVars, i) && !Abc_TtPosVar(t, nVars, i) )
+ return 0;
+ return 1;
+}
+static inline int Abc_TtIsPosUnate( word * t, int nVars )
+{
+ int i;
+ for ( i = 0; i < nVars; i++ )
+ if ( !Abc_TtPosVar(t, nVars, i) )
+ return 0;
+ return 1;
+}
+static inline void Abc_TtMakePosUnate( word * t, int nVars )
+{
+ int i, nWords = Abc_TtWordNum(nVars);
+ for ( i = 0; i < nVars; i++ )
+ if ( Abc_TtNegVar(t, nVars, i) )
+ Abc_TtFlip( t, nWords, i );
+ else assert( Abc_TtPosVar(t, nVars, i) );
+}
+
+
+/**Function*************************************************************
+
Synopsis [Computes ISOP for 6 variables or less.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-20 18:02:33 +0000