summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c23
-rw-r--r--src/map/if/ifDsd.c9
-rw-r--r--src/misc/extra/extraUtilThresh.c822
3 files changed, 612 insertions, 242 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e1dd7bb4..f9af09e9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16724,11 +16724,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 );
+ extern void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fThreshHeuristic, int fVerbose );
If_DsdMan_t * pDsd = (If_DsdMan_t *)Abc_FrameReadManDsd();
- int c, nLimit = 0, nLutSize = -1, fCleanOccur = 0, fCleanMarks = 0, fInvMarks = 0, fUnate = 0, fThresh = 0, fVerbose = 0;
+ int c, nLimit = 0, nLutSize = -1, fCleanOccur = 0, fCleanMarks = 0, fInvMarks = 0, fUnate = 0, fThresh = 0, fThreshHeuristic = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "LKomiutvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LKomiutsvh" ) ) != EOF )
{
switch ( c )
{
@@ -16765,6 +16765,9 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
fThresh ^= 1;
break;
+ case 's':
+ fThreshHeuristic ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -16789,14 +16792,11 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
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 );
+ Id_DsdManTuneThresh( pDsd, fUnate, fThresh, fThreshHeuristic, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: dsd_filter [-LK num] [-omiutvh]\n" );
+ Abc_Print( -2, "usage: dsd_filter [-LK num] [-omiutsvh]\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 );
@@ -16805,8 +16805,15 @@ usage:
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-s : toggles marking threshold functions heuristically [default = %s]\n", fThreshHeuristic?"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");
+ Abc_Print( -2, "\t \n" );
+ Abc_Print( -2, "\t Option \"dsd_filter -s\" was contributed by Augusto Neutzling and Jody Matos from\n" );
+ Abc_Print( -2, "\t Federal University of Rio Grande do Sul, Brazil. The paper describing the method:\n" );
+ Abc_Print( -2, "\t A. Neutzling, J. M. Matos, A. Mishchenko, R. Ribas, and A. Reis,\n" );
+ Abc_Print( -2, "\t \"Threshold logic synthesis based on cut pruning\". Proc. ICCAD 2015.\n" );
+// Abc_Print( -2, "\t http://www.eecs.berkeley.edu/~alanmi/publications/2015/iccad15_thresh.pdf\n" );
return 1;
}
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index cdc34b2a..e05e9a6f 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -2761,9 +2761,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
SeeAlso []
***********************************************************************/
-void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose )
+void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fThreshHeuristic, int fVerbose )
{
extern int Extra_ThreshCheck( word * t, int nVars, int * pW );
+ extern int Extra_ThreshHeuristic( word * t, int nVars, int * pW );
int fVeryVerbose = 0;
int pW[16];
ProgressBar * pProgress = NULL;
@@ -2771,7 +2772,7 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
word * pTruth, Perm;
int i, nVars, Value;
abctime clk = Abc_Clock();
- assert( fUnate != fThresh );
+ assert( fUnate != fThresh || fUnate != fThreshHeuristic );
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
@@ -2799,7 +2800,9 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
Value = Abc_TtIsUnate( pTruth, nVars );
else if ( fThresh )
Value = Extra_ThreshCheck( pTruth, nVars, pW );
- else
+ else if ( fThreshHeuristic )
+ Value = Extra_ThreshHeuristic( pTruth, nVars, pW );
+ else
Value = 0;
Perm = 0;
if ( fVeryVerbose )
diff --git a/src/misc/extra/extraUtilThresh.c b/src/misc/extra/extraUtilThresh.c
index 478e025c..6633381c 100644
--- a/src/misc/extra/extraUtilThresh.c
+++ b/src/misc/extra/extraUtilThresh.c
@@ -1,27 +1,31 @@
/**CFile****************************************************************
- FileName [extraUtilThresh.c]
+ FileName [extraUtilThresh.c]
- SystemName [ABC: Logic synthesis and verification system.]
+ SystemName [ABC: Logic synthesis and verification system.]
- PackageName [extra]
+ PackageName [extra]
- Synopsis [Dealing with threshold functions.]
+ Synopsis [Dealing with threshold functions.]
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
+ Author [Augusto Neutzling, Jody Matos, and Alan Mishchenko (UC Berkeley).]
- Date [Ver. 1.0. Started - October 7, 2014.]
+ Affiliation [Federal University of Rio Grande do Sul, Brazil]
- Revision [$Id: extraUtilThresh.c,v 1.0 2014/10/07 00:00:00 alanmi Exp $]
+ 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 "base/main/main.h"
+#include "misc/extra/extra.h"
+#include "bdd/cudd/cudd.h"
+#include "bool/kit/kit.h"
#include "misc/vec/vec.h"
#include "misc/util/utilTruth.h"
@@ -38,296 +42,652 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
- Synopsis [Checks thresholdness of the function.]
+ Synopsis [Checks thresholdness of the function.]
+
+ Description []
- Description []
-
- SideEffects []
+ SideEffects []
- SeeAlso []
+ SeeAlso []
-***********************************************************************/
-void Extra_ThreshPrintChow( int Chow0, int * pChow, int nVars )
-{
+ ***********************************************************************/
+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 );
+ for (i = 0; i < nVars; i++)
+ printf("%d ", pChow[i]);
+ printf(" %d\n", Chow0);
}
-int Extra_ThreshComputeChow( word * t, int nVars, int * pChow )
-{
+int Extra_ThreshComputeChow(word * t, int nVars, int * pChow) {
int i, k, Chow0 = 0, nMints = (1 << nVars);
- memset( pChow, 0, sizeof(int) * 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 )
+ 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++ )
+ for (k = 0; k < nVars; k++)
pChow[k] = 2 * pChow[k] - Chow0;
- return Chow0 - (1 << (nVars-1));
+ return Chow0 - (1 << (nVars - 1));
+}
+void Extra_ThreshSortByChow(word * t, int nVars, int * pChow) {
+ int i, nWords = Abc_TtWordNum(nVars);
+ //sort the variables by Chow in ascending order
+ 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;
+ }
}
-void Extra_ThreshSortByChow( word * t, int nVars, int * pChow )
-{
+void Extra_ThreshSortByChowInverted(word * t, int nVars, int * pChow) {
int i, nWords = Abc_TtWordNum(nVars);
- while ( 1 )
- {
+ //sort the variables by Chow in descending order
+ while (1) {
int fChange = 0;
- for ( i = 0; i < nVars - 1; i++ )
- {
- if ( pChow[i] >= pChow[i+1] )
+ 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 );
+ ABC_SWAP(int, pChow[i], pChow[i + 1]);
+ Abc_TtSwapAdjacent(t, nWords, i);
fChange = 1;
}
- if ( !fChange )
+ if (!fChange)
return;
}
}
-static inline int Extra_ThreshWeightedSum( int * pW, int nVars, int m )
-{
+int Extra_ThreshInitializeChow(int nVars, int * pChow) {
+ int i = 0, Aux[16], nChows = 0;
+ //group the variables which have the same Chow
+ for (i = 0; i < nVars; i++) {
+ if (i == 0 || (pChow[i] == pChow[i - 1]))
+ Aux[i] = nChows;
+ else {
+ nChows++;
+ Aux[i] = nChows;
+ }
+ }
+ for (i = 0; i < nVars; i++)
+ pChow[i] = Aux[i];
+ nChows++;
+ return nChows;
+
+}
+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 )
+ for (i = 0; i < nVars; i++)
+ if ((m >> i) & 1)
Cost += pW[i];
return Cost;
}
-int Extra_ThreshSelectWeights3( word * t, int nVars, int * pW )
-{
+static inline int Extra_ThreshCubeWeightedSum1(int * pWofChow, int * pChow,
+ char * pIsop, int nVars, int j) {
+ int k, Cost = 0;
+ for (k = j; k < j + nVars; k++)
+ if (pIsop[k] == '1')
+ Cost += pWofChow[pChow[k - j]];
+ return Cost;
+}
+static inline int Extra_ThreshCubeWeightedSum2(int * pWofChow, int * pChow,
+ char * pIsop, int nVars, int j) {
+ int k, Cost = 0;
+ for (k = j; k < j + nVars; k++)
+ if (pIsop[k] == '-')
+ Cost += pWofChow[pChow[k - j]];
+ return Cost;
+}
+
+static inline int Extra_ThreshCubeWeightedSum3(int * pWofChow, int nChows,
+ unsigned long ** pGreaters, int j) {
+ int i, Cost = 0;
+ for (i = 0; i < nChows; i++)
+ Cost += pWofChow[i] * pGreaters[j][i];
+ return Cost;
+}
+static inline int Extra_ThreshCubeWeightedSum4(int * pWofChow, int nChows,
+ unsigned long ** pSmallers, int j) {
+ int i, Cost = 0;
+ for (i = 0; i < nChows; i++)
+ Cost += pWofChow[i] * pSmallers[j][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;
+ 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;
- }
+ if (m < nMints)
+ continue;
+ assert(Lmax < Lmin);
+ return Lmin;
+ }
return 0;
}
-int Extra_ThreshSelectWeights4( word * t, int nVars, int * pW )
-{
+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;
- }
+ 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 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;
- }
+ 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 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;
- }
+ 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 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;
- }
+ 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 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;
- }
+ 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 )
+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 );
+ 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 )
-{
+void Extra_ThreshIncrementWeights(int nChows, int * pWofChow, int i) {
+ int k;
+ for (k = i; k < nChows; k++) {
+ pWofChow[k]++;
+ }
+}
+void Extra_ThreshDecrementWeights(int nChows, int * pWofChow, int i) {
+ int k;
+ for (k = i; k < nChows; k++) {
+ pWofChow[k]--;
+ }
+}
+void Extra_ThreshPrintInequalities(unsigned long ** pGreaters,
+ unsigned long ** pSmallers, int nChows, int nInequalities) {
+ int i = 0, k = 0;
+ for (k = 0; k < nInequalities; k++) {
+ printf("\n Inequality [%d] = ", k);
+ for (i = 0; i < nChows; i++) {
+ printf("%ld ", pGreaters[k][i]);
+ }
+ printf(" > ");
+
+ for (i = 0; i < nChows; i++) {
+ printf("%ld ", pSmallers[k][i]);
+ }
+ }
+}
+void Extra_ThreshCreateInequalities(char * pIsop, char * pIsopFneg, int nVars,
+ int * pWofChow, int * pChow, int nChows, int nInequalities,
+ unsigned long ** pGreaters, unsigned long ** pSmallers) {
+ int i = 0, j = 0, k = 0, m = 0;
+
+ int nCubesIsop = strlen(pIsop) / (nVars + 3);
+ int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
+
+ for (k = 0; k < nCubesIsop * nCubesIsopFneg; k++)
+ for (i = 0; i < nChows; i++) {
+ pGreaters[k][i] = 0;
+ pSmallers[k][i] = 0;
+ }
+ m = 0;
+ for (i = 0; i < (int)strlen(pIsop); i += (nVars + 3))
+ for (j = 0; j < nCubesIsopFneg; j++) {
+ for (k = 0; k < nVars; k++)
+ if (pIsop[i + k] == '1')
+ pGreaters[m][pChow[k]] = pGreaters[m][(pChow[k])] + 1;
+
+ m++;
+ }
+ m = 0;
+ for (i = 0; i < nCubesIsop; i++)
+ for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3)) {
+ for (k = 0; k < nVars; k++)
+ if (pIsopFneg[j + k] == '-')
+ pSmallers[m][pChow[k]] = pSmallers[m][pChow[k]] + 1;
+ m++;
+ }
+// Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
+// printf( "\nInequalities was Created \n");
+}
+
+void Extra_ThreshSimplifyInequalities(int nInequalities, int nChows,
+ unsigned long ** pGreaters, unsigned long ** pSmallers) {
+ int i = 0, k = 0;
+
+ for (k = 0; k < nInequalities; k++) {
+ for (i = 0; i < nChows; i++) {
+ if ((pGreaters[k][i]) == (pSmallers[k][i])) {
+ pGreaters[k][i] = 0;
+ pSmallers[k][i] = 0;
+ } else if ((pGreaters[k][i]) > (pSmallers[k][i])) {
+ pGreaters[k][i] = pGreaters[k][i] - pSmallers[k][i];
+ pSmallers[k][i] = 0;
+ } else {
+ pSmallers[k][i] = pSmallers[k][i] - pGreaters[k][i];
+ ;
+ pGreaters[k][i] = 0;
+ }
+ }
+ }
+// Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
+// printf( "\nInequalities was Siplified \n");
+}
+int Extra_ThreshAssignWeights(word * t, char * pIsop, char * pIsopFneg,
+ int nVars, int * pW, int * pChow, int nChows, int Wmin) {
+
+ int i = 0, j = 0, Lmin = 1000, Lmax = 0, Limit = nVars * 2, delta = 0,
+ deltaOld = -1000, fIncremented = 0;
+ //******************************
+ int * pWofChow = ABC_ALLOC( int, nChows );
+ int nCubesIsop = strlen(pIsop) / (nVars + 3);
+ int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
+ int nInequalities = nCubesIsop * nCubesIsopFneg;
+ unsigned long **pGreaters;
+ unsigned long **pSmallers;
+
+ pGreaters = malloc(nCubesIsop * nCubesIsopFneg * sizeof *pGreaters);
+ for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+ pGreaters[i] = malloc(nChows * sizeof *pGreaters[i]);
+ }
+ pSmallers = malloc(nCubesIsop * nCubesIsopFneg * sizeof *pSmallers);
+ for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+ pSmallers[i] = malloc(nChows * sizeof *pSmallers[i]);
+ }
+
+ //******************************
+ Extra_ThreshCreateInequalities(pIsop, pIsopFneg, nVars, pWofChow, pChow,
+ nChows, nInequalities, pGreaters, pSmallers);
+ Extra_ThreshSimplifyInequalities(nInequalities, nChows, pGreaters,
+ pSmallers);
+
+ //initializes the weights
+ pWofChow[0] = Wmin;
+ for (i = 1; i < nChows; i++) {
+ pWofChow[i] = pWofChow[i - 1] + 1;
+ }
+ i = 0;
+
+ //assign the weights respecting the inequalities
+ while (i < nChows && pWofChow[nChows - 1] <= Limit) {
+ Lmin = 1000;
+ Lmax = 0;
+
+ while (j < nInequalities) {
+ if (pGreaters[j][i] != 0) {
+ Lmin = Extra_ThreshCubeWeightedSum3(pWofChow, nChows, pGreaters,
+ j);
+ Lmax = Extra_ThreshCubeWeightedSum4(pWofChow, nChows, pSmallers,
+ j);
+ delta = Lmin - Lmax;
+
+ if (delta > 0) {
+ if (fIncremented == 1) {
+ j = 0;
+ fIncremented = 0;
+ deltaOld = -1000;
+ } else
+ j++;
+ continue;
+ }
+ if (delta > deltaOld) {
+ Extra_ThreshIncrementWeights(nChows, pWofChow, i);
+ deltaOld = delta;
+ fIncremented = 1;
+ } else if (fIncremented == 1) {
+ Extra_ThreshDecrementWeights(nChows, pWofChow, i);
+ j++;
+ deltaOld = -1000;
+ fIncremented = 0;
+ continue;
+ } else
+ j++;
+ } else
+ j++;
+
+ }
+ i++;
+ j = 0;
+ }
+
+ //******************************
+ for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+ free(pGreaters[i]);
+ }
+ free(pGreaters);
+ for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+ free(pSmallers[i]);
+ }
+ free(pSmallers);
+ //******************************
+
+ i = 0;
+ Lmin = 1000;
+ Lmax = 0;
+
+ //check the assigned weights in the original system
+ for (j = 0; j < (int)strlen(pIsop); j += (nVars + 3))
+ Lmin = Abc_MinInt(Lmin,
+ Extra_ThreshCubeWeightedSum1(pWofChow, pChow, pIsop, nVars, j));
+ for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3))
+ Lmax = Abc_MaxInt(Lmax,
+ Extra_ThreshCubeWeightedSum2(pWofChow, pChow, pIsopFneg, nVars,
+ j));
+
+ for (i = 0; i < nVars; i++) {
+ pW[i] = pWofChow[pChow[i]];
+ }
+
+ ABC_FREE( pWofChow );
+ if (Lmin > Lmax)
+ return Lmin;
+ else
+ return 0;
+}
+void Extra_ThreshPrintWeights(int T, int * pW, int nVars) {
+ int i;
+
+ if (T == 0)
+ fprintf( stdout, "\nHeuristic method: is not TLF\n\n");
+ else {
+ fprintf( stdout, "\nHeuristic method: Weights and threshold value:\n");
+ for (i = 0; i < nVars; i++)
+ printf("%d ", pW[i]);
+ printf(" %d\n", T);
+ }
+}
+/**Function*************************************************************
+
+
+ Synopsis [Checks thresholdness of the function.]
+
+ Description []
+
+ SideEffects []
+
+
+ SeeAlso []
+
+ ***********************************************************************/
+int Extra_ThreshCheck(word * t, int nVars, int * pW) {
int Chow0, Chow[16];
- if ( !Abc_TtIsUnate(t, 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 );
+ Abc_TtMakePosUnate(t, nVars);
+ Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
+ Extra_ThreshSortByChow(t, nVars, Chow);
+ return Extra_ThreshSelectWeights(t, nVars, pW);
+}
+/**Function*************************************************************
+
+
+ Synopsis [Checks thresholdness of the function by using a heuristic method.]
+
+ Description []
+
+ SideEffects []
+
+
+ SeeAlso []
+
+ ***********************************************************************/
+int Extra_ThreshHeuristic(word * t, int nVars, int * pW) {
+
+ extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+ int Chow0, Chow[16], nChows, i, T = 0;
+ DdManager * dd;
+ Vec_Str_t * vCube;
+ DdNode * ddNode, * ddNodeFneg;
+ char * pIsop, * pIsopFneg;
+ if (nVars <= 1)
+ return 1;
+ if (!Abc_TtIsUnate(t, nVars))
+ return 0;
+ Abc_TtMakePosUnate(t, nVars);
+ Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
+ Extra_ThreshSortByChowInverted(t, nVars, Chow);
+ nChows = Extra_ThreshInitializeChow(nVars, Chow);
+
+ dd = (DdManager *) Abc_FrameReadManDd();
+ vCube = Vec_StrAlloc(nVars);
+ for (i = 0; i < nVars; i++)
+ Cudd_bddIthVar(dd, i);
+ ddNode = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
+ Cudd_Ref(ddNode);
+ pIsop = Abc_ConvertBddToSop( NULL, dd, ddNode, ddNode, nVars, 1,
+ vCube, 1);
+
+ Abc_TtNot(t, Abc_TruthWordNum(nVars));
+ ddNodeFneg = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
+ Cudd_Ref(ddNodeFneg);
+
+ pIsopFneg = Abc_ConvertBddToSop( NULL, dd, ddNodeFneg, ddNodeFneg,
+ nVars, 1, vCube, 1);
+
+ Cudd_RecursiveDeref(dd, ddNode);
+ Cudd_RecursiveDeref(dd, ddNodeFneg);
+
+ T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow, nChows,
+ 1);
+
+ for (i = 2; (i < 4) && (T == 0) && (nVars >= 6); i++)
+ T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow,
+ nChows, i);
+
+ free(pIsop);
+ free(pIsopFneg);
+ Vec_StrFree(vCube);
+
+ return T;
}
/**Function*************************************************************
- Synopsis [Checks unateness of a function.]
+ Synopsis [Checks unateness of a function.]
+
+ Description []
- Description []
-
- SideEffects []
+ SideEffects []
- SeeAlso []
+ SeeAlso []
-***********************************************************************/
-void Extra_ThreshCheckTest()
-{
- int nVars = 5;
+ ***********************************************************************/
+void Extra_ThreshCheckTest() {
+ int nVars = 6;
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[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[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
// 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) );
+ 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 );
+ Chow0 = Extra_ThreshComputeChow(&t, nVars, Chow);
+ if ((T = Extra_ThreshCheck(&t, nVars, Weights)))
+ Extra_ThreshPrintChow(T, Weights, nVars);
else
- printf( "No threshold\n" );
+ printf("No threshold\n");
}
+void Extra_ThreshHeuristicTest() {
+ int nVars = 6;
+ int T, Weights[16];
+ // word t = 19983902376700760000;
+ word t = (s_Truths6[0] & s_Truths6[1] & s_Truths6[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
+ word * pT = &t;
+ T = Extra_ThreshHeuristic(pT, nVars, Weights);
+ Extra_ThreshPrintWeights(T, Weights, nVars);
+
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:31:26 +0000