From 19a4bb930edcfc7910388bb08fd86482b9dd35e7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Sep 2015 15:24:25 -0700 Subject: Threshold logic checking code by Augusto Neutzling and Jody Matos. --- src/misc/extra/extraUtilThresh.c | 822 ++++++++++++++++++++++++++++----------- 1 file changed, 591 insertions(+), 231 deletions(-) (limited to 'src/misc/extra') 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 #include #include #include +#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 -- cgit v1.2.3