Moving BDD-based threshold function detection to the BDD part of the code.

2 files changed, 0 insertions, 694 deletions

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 <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"
-
-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