From 0145b0ca724ba866480a3edcc1292cdf04117d6f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 16 Oct 2015 18:34:06 -0700 Subject: Moving BDD-based threshold function detection to the BDD part of the code. --- src/base/abci/abc.c | 3 +- src/bdd/extrab/extraBddThresh.c | 693 +++++++++++++++++++++++++++++++++++++++ src/bdd/extrab/module.make | 1 + src/map/if/if.h | 1 + src/map/if/ifDsd.c | 8 + src/misc/extra/extraUtilThresh.c | 693 --------------------------------------- src/misc/extra/module.make | 1 - 7 files changed, 705 insertions(+), 695 deletions(-) create mode 100644 src/bdd/extrab/extraBddThresh.c delete mode 100644 src/misc/extra/extraUtilThresh.c (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 187fcf89..d6a9b1cc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -16941,7 +16941,6 @@ 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 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, fThreshHeuristic = 0, fVerbose = 0; Extra_UtilGetoptReset(); @@ -17009,8 +17008,10 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv ) If_DsdManCleanMarks( pDsd, fVerbose ); if ( fInvMarks ) If_DsdManInvertMarks( pDsd, fVerbose ); +#ifdef ABC_USE_CUDD else Id_DsdManTuneThresh( pDsd, fUnate, fThresh, fThreshHeuristic, fVerbose ); +#endif return 0; usage: diff --git a/src/bdd/extrab/extraBddThresh.c b/src/bdd/extrab/extraBddThresh.c new file mode 100644 index 00000000..511fc24b --- /dev/null +++ b/src/bdd/extrab/extraBddThresh.c @@ -0,0 +1,693 @@ +/**CFile**************************************************************** + + FileName [extraBddThresh.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [Dealing with threshold functions.] + + Author [Augusto Neutzling, Jody Matos, and Alan Mishchenko (UC Berkeley).] + + Affiliation [Federal University of Rio Grande do Sul, Brazil] + + Date [Ver. 1.0. Started - October 7, 2014.] + + Revision [$Id: extraBddThresh.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" + +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); + //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_ThreshSortByChowInverted(word * t, int nVars, int * pChow) { + int i, nWords = Abc_TtWordNum(nVars); + //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]) + continue; + ABC_SWAP(int, pChow[i], pChow[i + 1]); + Abc_TtSwapAdjacent(t, nWords, i); + fChange = 1; + } + if (!fChange) + return; + } +} +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) + Cost += pW[i]; + return Cost; +} +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; +// 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; +} +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)) + 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 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.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +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[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)); +// 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"); +} +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 + diff --git a/src/bdd/extrab/module.make b/src/bdd/extrab/module.make index 38cdddb6..8369315c 100644 --- a/src/bdd/extrab/module.make +++ b/src/bdd/extrab/module.make @@ -4,5 +4,6 @@ SRC += src/bdd/extrab/extraBddAuto.c \ src/bdd/extrab/extraBddKmap.c \ src/bdd/extrab/extraBddMisc.c \ src/bdd/extrab/extraBddSymm.c \ + src/misc/extra/extraBddThresh.c \ src/bdd/extrab/extraBddTime.c \ src/bdd/extrab/extraBddUnate.c diff --git a/src/map/if/if.h b/src/map/if/if.h index 214eda88..55f28fab 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -576,6 +576,7 @@ extern char * If_DsdManGetCellStr( If_DsdMan_t * p ); extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose ); extern int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig ); extern int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm ); +extern void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fThreshHeuristic, int fVerbose ); /*=== ifLib.c =============================================================*/ extern If_LibLut_t * If_LibLutRead( char * FileName ); extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 5d9077c3..f70f2177 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -26,6 +26,10 @@ #include "aig/gia/gia.h" #include "bool/kit/kit.h" +#ifdef ABC_USE_CUDD +#include "bdd/extrab/extraBdd.h" +#endif + #ifdef ABC_USE_PTHREADS #ifdef _WIN32 @@ -2761,6 +2765,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, SeeAlso [] ***********************************************************************/ +#ifdef ABC_USE_CUDD + 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 ); @@ -2821,6 +2827,8 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fThreshH If_DsdManPrintDistrib( p ); } +#endif // ABC_USE_CUDD are used + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/extraUtilThresh.c b/src/misc/extra/extraUtilThresh.c deleted file mode 100644 index 6633381c..00000000 --- a/src/misc/extra/extraUtilThresh.c +++ /dev/null @@ -1,693 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraUtilThresh.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [extra] - - Synopsis [Dealing with threshold functions.] - - Author [Augusto Neutzling, Jody Matos, and Alan Mishchenko (UC Berkeley).] - - Affiliation [Federal University of Rio Grande do Sul, Brazil] - - 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" - -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); - //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_ThreshSortByChowInverted(word * t, int nVars, int * pChow) { - int i, nWords = Abc_TtWordNum(nVars); - //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]) - continue; - ABC_SWAP(int, pChow[i], pChow[i + 1]); - Abc_TtSwapAdjacent(t, nWords, i); - fChange = 1; - } - if (!fChange) - return; - } -} -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) - Cost += pW[i]; - return Cost; -} -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; -// 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; -} -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)) - 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 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.] - - Description [] - - SideEffects [] - - SeeAlso [] - - ***********************************************************************/ -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[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)); -// 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"); -} -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 - diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 5c1276e3..e9bd782e 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -10,6 +10,5 @@ SRC += src/misc/extra/extraUtilBitMatrix.c \ src/misc/extra/extraUtilProgress.c \ src/misc/extra/extraUtilReader.c \ src/misc/extra/extraUtilSupp.c \ - src/misc/extra/extraUtilThresh.c \ src/misc/extra/extraUtilTruth.c \ src/misc/extra/extraUtilUtil.c -- cgit v1.2.3