Threshold logic checking code by Augusto Neutzling and Jody Matos.

1 files changed, 591 insertions, 231 deletions

diff --git a/src/misc/extra/extraUtilThresh.c b/src/misc/extra/extraUtilThresh.c
index 478e025c..6633381c 100644
--- a/src/misc/extra/extraUtilThresh.c
+++ b/src/misc/extra/extraUtilThresh.c
@@ -1,27 +1,31 @@
 /**CFile****************************************************************
 
-  FileName    [extraUtilThresh.c]
+ FileName    [extraUtilThresh.c]
 
-  SystemName  [ABC: Logic synthesis and verification system.]
+ SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [extra]
+ PackageName [extra]
 
-  Synopsis    [Dealing with threshold functions.]
+ Synopsis    [Dealing with threshold functions.]
 
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
+ Author      [Augusto Neutzling, Jody Matos, and Alan Mishchenko (UC Berkeley).]
 
-  Date        [Ver. 1.0. Started - October 7, 2014.]
+ Affiliation [Federal University of Rio Grande do Sul, Brazil]
 
-  Revision    [$Id: extraUtilThresh.c,v 1.0 2014/10/07 00:00:00 alanmi Exp $]
+ Date        [Ver. 1.0. Started - October 7, 2014.]
 
-***********************************************************************/
+ Revision    [$Id: extraUtilThresh.c,v 1.0 2014/10/07 00:00:00 alanmi Exp $]
+
+ ***********************************************************************/
 
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
+#include "base/main/main.h"
+#include "misc/extra/extra.h"
+#include "bdd/cudd/cudd.h"
+#include "bool/kit/kit.h"
 
 #include "misc/vec/vec.h"
 #include "misc/util/utilTruth.h"
@@ -38,296 +42,652 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Checks thresholdness of the function.]
+ Synopsis    [Checks thresholdness of the function.]
+
+ Description []
 
-  Description []
-               
-  SideEffects []
+ SideEffects []
 
-  SeeAlso     []
+ SeeAlso     []
 
-***********************************************************************/
-void Extra_ThreshPrintChow( int Chow0, int * pChow, int nVars )
-{
+ ***********************************************************************/
+void Extra_ThreshPrintChow(int Chow0, int * pChow, int nVars) {
     int i;
-    for ( i = 0; i < nVars; i++ )
-        printf( "%d ", pChow[i] );
-    printf( "  %d\n", Chow0 );
+    for (i = 0; i < nVars; i++)
+        printf("%d ", pChow[i]);
+    printf("  %d\n", Chow0);
 }
-int Extra_ThreshComputeChow( word * t, int nVars, int * pChow )
-{
+int Extra_ThreshComputeChow(word * t, int nVars, int * pChow) {
     int i, k, Chow0 = 0, nMints = (1 << nVars);
-    memset( pChow, 0, sizeof(int) * nVars );
+    memset(pChow, 0, sizeof(int) * nVars);
     // compute Chow coefs
-    for ( i = 0; i < nMints; i++ )
-        if ( Abc_TtGetBit(t, i) )
-            for ( Chow0++, k = 0; k < nVars; k++ )
-                if ( (i >> k) & 1 )
+    for (i = 0; i < nMints; i++)
+        if (Abc_TtGetBit(t, i))
+            for (Chow0++, k = 0; k < nVars; k++)
+                if ((i >> k) & 1)
                     pChow[k]++;
     // compute modified Chow coefs
-    for ( k = 0; k < nVars; k++ )
+    for (k = 0; k < nVars; k++)
         pChow[k] = 2 * pChow[k] - Chow0;
-    return Chow0 - (1 << (nVars-1));
+    return Chow0 - (1 << (nVars - 1));
+}
+void Extra_ThreshSortByChow(word * t, int nVars, int * pChow) {
+    int i, nWords = Abc_TtWordNum(nVars);
+    //sort the variables by Chow in ascending order
+    while (1) {
+        int fChange = 0;
+        for (i = 0; i < nVars - 1; i++) {
+            if (pChow[i] >= pChow[i + 1])
+                continue;
+            ABC_SWAP(int, pChow[i], pChow[i + 1]);
+            Abc_TtSwapAdjacent(t, nWords, i);
+            fChange = 1;
+        }
+        if (!fChange)
+            return;
+    }
 }
-void Extra_ThreshSortByChow( word * t, int nVars, int * pChow )
-{
+void Extra_ThreshSortByChowInverted(word * t, int nVars, int * pChow) {
     int i, nWords = Abc_TtWordNum(nVars);
-    while ( 1 )
-    {
+    //sort the variables by Chow in descending order
+    while (1) {
         int fChange = 0;
-        for ( i = 0; i < nVars - 1; i++ )
-        {
-            if ( pChow[i] >= pChow[i+1] )
+        for (i = 0; i < nVars - 1; i++) {
+            if (pChow[i] <= pChow[i + 1])
                 continue;
-            ABC_SWAP( int, pChow[i], pChow[i+1] );
-            Abc_TtSwapAdjacent( t, nWords, i );
+            ABC_SWAP(int, pChow[i], pChow[i + 1]);
+            Abc_TtSwapAdjacent(t, nWords, i);
             fChange = 1;
         }
-        if ( !fChange )
+        if (!fChange)
             return;
     }
 }
-static inline int Extra_ThreshWeightedSum( int * pW, int nVars, int m )
-{
+int Extra_ThreshInitializeChow(int nVars, int * pChow) {
+    int i = 0, Aux[16], nChows = 0;
+    //group the variables which have the same Chow
+    for (i = 0; i < nVars; i++) {
+        if (i == 0 || (pChow[i] == pChow[i - 1]))
+            Aux[i] = nChows;
+        else {
+            nChows++;
+            Aux[i] = nChows;
+        }
+    }
+    for (i = 0; i < nVars; i++)
+        pChow[i] = Aux[i];
+    nChows++;
+    return nChows;
+
+}
+static inline int Extra_ThreshWeightedSum(int * pW, int nVars, int m) {
     int i, Cost = 0;
-    for ( i = 0; i < nVars; i++ )
-        if ( (m >> i) & 1 )
+    for (i = 0; i < nVars; i++)
+        if ((m >> i) & 1)
             Cost += pW[i];
     return Cost;
 }
-int Extra_ThreshSelectWeights3( word * t, int nVars, int * pW )
-{
+static inline int Extra_ThreshCubeWeightedSum1(int * pWofChow, int * pChow,
+        char * pIsop, int nVars, int j) {
+    int k, Cost = 0;
+    for (k = j; k < j + nVars; k++)
+        if (pIsop[k] == '1')
+            Cost += pWofChow[pChow[k - j]];
+    return Cost;
+}
+static inline int Extra_ThreshCubeWeightedSum2(int * pWofChow, int * pChow,
+        char * pIsop, int nVars, int j) {
+    int k, Cost = 0;
+    for (k = j; k < j + nVars; k++)
+        if (pIsop[k] == '-')
+            Cost += pWofChow[pChow[k - j]];
+    return Cost;
+}
+
+static inline int Extra_ThreshCubeWeightedSum3(int * pWofChow, int nChows,
+        unsigned long ** pGreaters, int j) {
+    int i, Cost = 0;
+    for (i = 0; i < nChows; i++)
+        Cost += pWofChow[i] * pGreaters[j][i];
+    return Cost;
+}
+static inline int Extra_ThreshCubeWeightedSum4(int * pWofChow, int nChows,
+        unsigned long ** pSmallers, int j) {
+    int i, Cost = 0;
+    for (i = 0; i < nChows; i++)
+        Cost += pWofChow[i] * pSmallers[j][i];
+    return Cost;
+}
+int Extra_ThreshSelectWeights3(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars);
-    assert( nVars == 3 );
-    for ( pW[2] = 1;     pW[2] <= nVars; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= nVars; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= nVars; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
+    assert(nVars == 3);
+    for (pW[2] = 1; pW[2] <= nVars; pW[2]++)
+        for (pW[1] = pW[2]; pW[1] <= nVars; pW[1]++)
+            for (pW[0] = pW[1]; pW[0] <= nVars; pW[0]++) {
+                Lmin = 10000;
+                Lmax = 0;
+                for (m = 0; m < nMints; m++) {
+                    if (Abc_TtGetBit(t, m))
+                        Lmin = Abc_MinInt(Lmin,
+                                Extra_ThreshWeightedSum(pW, nVars, m));
+                    else
+                        Lmax = Abc_MaxInt(Lmax,
+                                Extra_ThreshWeightedSum(pW, nVars, m));
+                    if (Lmax >= Lmin)
+                        break;
 //            printf( "%c%d ", Abc_TtGetBit(t, m) ? '+' : '-', Extra_ThreshWeightedSum(pW, nVars, m) );
-        }
+                }
 //        printf( "  -%d +%d\n", Lmax, Lmin );
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+                if (m < nMints)
+                    continue;
+                assert(Lmax < Lmin);
+                return Lmin;
+            }
     return 0;
 }
-int Extra_ThreshSelectWeights4( word * t, int nVars, int * pW )
-{
+int Extra_ThreshSelectWeights4(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars);
-    assert( nVars == 4 );
-    for ( pW[3] = 1;     pW[3] <= nVars; pW[3]++ )
-    for ( pW[2] = pW[3]; pW[2] <= nVars; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= nVars; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= nVars; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
-        }
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+    assert(nVars == 4);
+    for (pW[3] = 1; pW[3] <= nVars; pW[3]++)
+        for (pW[2] = pW[3]; pW[2] <= nVars; pW[2]++)
+            for (pW[1] = pW[2]; pW[1] <= nVars; pW[1]++)
+                for (pW[0] = pW[1]; pW[0] <= nVars; pW[0]++) {
+                    Lmin = 10000;
+                    Lmax = 0;
+                    for (m = 0; m < nMints; m++) {
+                        if (Abc_TtGetBit(t, m))
+                            Lmin = Abc_MinInt(Lmin,
+                                    Extra_ThreshWeightedSum(pW, nVars, m));
+                        else
+                            Lmax = Abc_MaxInt(Lmax,
+                                    Extra_ThreshWeightedSum(pW, nVars, m));
+                        if (Lmax >= Lmin)
+                            break;
+                    }
+                    if (m < nMints)
+                        continue;
+                    assert(Lmax < Lmin);
+                    return Lmin;
+                }
     return 0;
 }
-int Extra_ThreshSelectWeights5( word * t, int nVars, int * pW )
-{
+int Extra_ThreshSelectWeights5(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 0;
-    assert( nVars == 5 );
-    for ( pW[4] = 1;     pW[4] <= Limit; pW[4]++ )
-    for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
-    for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
-        }
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+    assert(nVars == 5);
+    for (pW[4] = 1; pW[4] <= Limit; pW[4]++)
+        for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
+            for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
+                for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
+                    for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
+                        Lmin = 10000;
+                        Lmax = 0;
+                        for (m = 0; m < nMints; m++) {
+                            if (Abc_TtGetBit(t, m))
+                                Lmin = Abc_MinInt(Lmin,
+                                        Extra_ThreshWeightedSum(pW, nVars, m));
+                            else
+                                Lmax = Abc_MaxInt(Lmax,
+                                        Extra_ThreshWeightedSum(pW, nVars, m));
+                            if (Lmax >= Lmin)
+                                break;
+                        }
+                        if (m < nMints)
+                            continue;
+                        assert(Lmax < Lmin);
+                        return Lmin;
+                    }
     return 0;
 }
-int Extra_ThreshSelectWeights6( word * t, int nVars, int * pW )
-{
+int Extra_ThreshSelectWeights6(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 3;
-    assert( nVars == 6 );
-    for ( pW[5] = 1;     pW[5] <= Limit; pW[5]++ )
-    for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
-    for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
-    for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
-        }
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+    assert(nVars == 6);
+    for (pW[5] = 1; pW[5] <= Limit; pW[5]++)
+        for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
+            for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
+                for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
+                    for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
+                        for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
+                            Lmin = 10000;
+                            Lmax = 0;
+                            for (m = 0; m < nMints; m++) {
+                                if (Abc_TtGetBit(t, m))
+                                    Lmin = Abc_MinInt(Lmin,
+                                            Extra_ThreshWeightedSum(pW, nVars,
+                                                    m));
+                                else
+                                    Lmax = Abc_MaxInt(Lmax,
+                                            Extra_ThreshWeightedSum(pW, nVars,
+                                                    m));
+                                if (Lmax >= Lmin)
+                                    break;
+                            }
+                            if (m < nMints)
+                                continue;
+                            assert(Lmax < Lmin);
+                            return Lmin;
+                        }
     return 0;
 }
-int Extra_ThreshSelectWeights7( word * t, int nVars, int * pW )
-{
+int Extra_ThreshSelectWeights7(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 6;
-    assert( nVars == 7 );
-    for ( pW[6] = 1;     pW[6] <= Limit; pW[6]++ )
-    for ( pW[5] = pW[6]; pW[5] <= Limit; pW[5]++ )
-    for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
-    for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
-    for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
-        }
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+    assert(nVars == 7);
+    for (pW[6] = 1; pW[6] <= Limit; pW[6]++)
+        for (pW[5] = pW[6]; pW[5] <= Limit; pW[5]++)
+            for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
+                for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
+                    for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
+                        for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
+                            for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
+                                Lmin = 10000;
+                                Lmax = 0;
+                                for (m = 0; m < nMints; m++) {
+                                    if (Abc_TtGetBit(t, m))
+                                        Lmin = Abc_MinInt(Lmin,
+                                                Extra_ThreshWeightedSum(pW,
+                                                        nVars, m));
+                                    else
+                                        Lmax = Abc_MaxInt(Lmax,
+                                                Extra_ThreshWeightedSum(pW,
+                                                        nVars, m));
+                                    if (Lmax >= Lmin)
+                                        break;
+                                }
+                                if (m < nMints)
+                                    continue;
+                                assert(Lmax < Lmin);
+                                return Lmin;
+                            }
     return 0;
 }
-int Extra_ThreshSelectWeights8( word * t, int nVars, int * pW )
-{
+int Extra_ThreshSelectWeights8(word * t, int nVars, int * pW) {
     int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 1; // <<-- incomplete detection to save runtime!
-    assert( nVars == 8 );
-    for ( pW[7] = 1;     pW[7] <= Limit; pW[7]++ )
-    for ( pW[6] = pW[7]; pW[6] <= Limit; pW[6]++ )
-    for ( pW[5] = pW[6]; pW[5] <= Limit; pW[5]++ )
-    for ( pW[4] = pW[5]; pW[4] <= Limit; pW[4]++ )
-    for ( pW[3] = pW[4]; pW[3] <= Limit; pW[3]++ )
-    for ( pW[2] = pW[3]; pW[2] <= Limit; pW[2]++ )
-    for ( pW[1] = pW[2]; pW[1] <= Limit; pW[1]++ )
-    for ( pW[0] = pW[1]; pW[0] <= Limit; pW[0]++ )
-    {
-        Lmin = 10000; Lmax = 0;
-        for ( m = 0; m < nMints; m++ )
-        {
-            if ( Abc_TtGetBit(t, m) )
-                Lmin = Abc_MinInt( Lmin, Extra_ThreshWeightedSum(pW, nVars, m) );
-            else
-                Lmax = Abc_MaxInt( Lmax, Extra_ThreshWeightedSum(pW, nVars, m) );
-            if ( Lmax >= Lmin )
-                break;
-        }
-        if ( m < nMints )
-            continue;
-        assert( Lmax < Lmin );
-        return Lmin;
-    }
+    assert(nVars == 8);
+    for (pW[7] = 1; pW[7] <= Limit; pW[7]++)
+        for (pW[6] = pW[7]; pW[6] <= Limit; pW[6]++)
+            for (pW[5] = pW[6]; pW[5] <= Limit; pW[5]++)
+                for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
+                    for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
+                        for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
+                            for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
+                                for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
+                                    Lmin = 10000;
+                                    Lmax = 0;
+                                    for (m = 0; m < nMints; m++) {
+                                        if (Abc_TtGetBit(t, m))
+                                            Lmin = Abc_MinInt(Lmin,
+                                                    Extra_ThreshWeightedSum(pW,
+                                                            nVars, m));
+                                        else
+                                            Lmax = Abc_MaxInt(Lmax,
+                                                    Extra_ThreshWeightedSum(pW,
+                                                            nVars, m));
+                                        if (Lmax >= Lmin)
+                                            break;
+                                    }
+                                    if (m < nMints)
+                                        continue;
+                                    assert(Lmax < Lmin);
+                                    return Lmin;
+                                }
     return 0;
 }
-int Extra_ThreshSelectWeights( word * t, int nVars, int * pW )
-{
-    if ( nVars <= 2 )
+int Extra_ThreshSelectWeights(word * t, int nVars, int * pW) {
+    if (nVars <= 2)
         return (t[0] & 0xF) != 6 && (t[0] & 0xF) != 9;
-    if ( nVars == 3 )
-        return Extra_ThreshSelectWeights3( t, nVars, pW );
-    if ( nVars == 4 )
-        return Extra_ThreshSelectWeights4( t, nVars, pW );
-    if ( nVars == 5 )
-        return Extra_ThreshSelectWeights5( t, nVars, pW );
-    if ( nVars == 6 )
-        return Extra_ThreshSelectWeights6( t, nVars, pW );
-    if ( nVars == 7 )
-        return Extra_ThreshSelectWeights7( t, nVars, pW );
-    if ( nVars == 8 )
-        return Extra_ThreshSelectWeights8( t, nVars, pW );
+    if (nVars == 3)
+        return Extra_ThreshSelectWeights3(t, nVars, pW);
+    if (nVars == 4)
+        return Extra_ThreshSelectWeights4(t, nVars, pW);
+    if (nVars == 5)
+        return Extra_ThreshSelectWeights5(t, nVars, pW);
+    if (nVars == 6)
+        return Extra_ThreshSelectWeights6(t, nVars, pW);
+    if (nVars == 7)
+        return Extra_ThreshSelectWeights7(t, nVars, pW);
+    if (nVars == 8)
+        return Extra_ThreshSelectWeights8(t, nVars, pW);
     return 0;
 }
-int Extra_ThreshCheck( word * t, int nVars, int * pW )
-{
+void Extra_ThreshIncrementWeights(int nChows, int * pWofChow, int i) {
+    int k;
+    for (k = i; k < nChows; k++) {
+        pWofChow[k]++;
+    }
+}
+void Extra_ThreshDecrementWeights(int nChows, int * pWofChow, int i) {
+    int k;
+    for (k = i; k < nChows; k++) {
+        pWofChow[k]--;
+    }
+}
+void Extra_ThreshPrintInequalities(unsigned long ** pGreaters,
+        unsigned long ** pSmallers, int nChows, int nInequalities) {
+    int i = 0, k = 0;
+    for (k = 0; k < nInequalities; k++) {
+        printf("\n Inequality [%d] = ", k);
+        for (i = 0; i < nChows; i++) {
+            printf("%ld ", pGreaters[k][i]);
+        }
+        printf(" > ");
+
+        for (i = 0; i < nChows; i++) {
+            printf("%ld ", pSmallers[k][i]);
+        }
+    }
+}
+void Extra_ThreshCreateInequalities(char * pIsop, char * pIsopFneg, int nVars,
+        int * pWofChow, int * pChow, int nChows, int nInequalities,
+        unsigned long ** pGreaters, unsigned long ** pSmallers) {
+    int i = 0, j = 0, k = 0, m = 0;
+
+    int nCubesIsop = strlen(pIsop) / (nVars + 3);
+    int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
+
+    for (k = 0; k < nCubesIsop * nCubesIsopFneg; k++)
+        for (i = 0; i < nChows; i++) {
+            pGreaters[k][i] = 0;
+            pSmallers[k][i] = 0;
+        }
+    m = 0;
+    for (i = 0; i < (int)strlen(pIsop); i += (nVars + 3))
+        for (j = 0; j < nCubesIsopFneg; j++) {
+            for (k = 0; k < nVars; k++)
+                if (pIsop[i + k] == '1')
+                    pGreaters[m][pChow[k]] = pGreaters[m][(pChow[k])] + 1;
+
+            m++;
+        }
+    m = 0;
+    for (i = 0; i < nCubesIsop; i++)
+        for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3)) {
+            for (k = 0; k < nVars; k++)
+                if (pIsopFneg[j + k] == '-')
+                    pSmallers[m][pChow[k]] = pSmallers[m][pChow[k]] + 1;
+            m++;
+        }
+//        Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
+//        printf( "\nInequalities was Created \n");
+}
+
+void Extra_ThreshSimplifyInequalities(int nInequalities, int nChows,
+        unsigned long ** pGreaters, unsigned long ** pSmallers) {
+    int i = 0, k = 0;
+
+    for (k = 0; k < nInequalities; k++) {
+        for (i = 0; i < nChows; i++) {
+            if ((pGreaters[k][i]) == (pSmallers[k][i])) {
+                pGreaters[k][i] = 0;
+                pSmallers[k][i] = 0;
+            } else if ((pGreaters[k][i]) > (pSmallers[k][i])) {
+                pGreaters[k][i] = pGreaters[k][i] - pSmallers[k][i];
+                pSmallers[k][i] = 0;
+            } else {
+                pSmallers[k][i] = pSmallers[k][i] - pGreaters[k][i];
+                ;
+                pGreaters[k][i] = 0;
+            }
+        }
+    }
+//        Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
+//        printf( "\nInequalities was Siplified \n");
+}
+int Extra_ThreshAssignWeights(word * t, char * pIsop, char * pIsopFneg,
+        int nVars, int * pW, int * pChow, int nChows, int Wmin) {
+
+    int i = 0, j = 0, Lmin = 1000, Lmax = 0, Limit = nVars * 2, delta = 0,
+            deltaOld = -1000, fIncremented = 0;
+    //******************************
+    int * pWofChow = ABC_ALLOC( int, nChows );
+    int nCubesIsop = strlen(pIsop) / (nVars + 3);
+    int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
+    int nInequalities = nCubesIsop * nCubesIsopFneg;
+    unsigned long **pGreaters;
+    unsigned long **pSmallers;
+
+    pGreaters = malloc(nCubesIsop * nCubesIsopFneg * sizeof *pGreaters);
+    for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+        pGreaters[i] = malloc(nChows * sizeof *pGreaters[i]);
+    }
+    pSmallers = malloc(nCubesIsop * nCubesIsopFneg * sizeof *pSmallers);
+    for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+        pSmallers[i] = malloc(nChows * sizeof *pSmallers[i]);
+    }
+
+    //******************************
+    Extra_ThreshCreateInequalities(pIsop, pIsopFneg, nVars, pWofChow, pChow,
+            nChows, nInequalities, pGreaters, pSmallers);
+    Extra_ThreshSimplifyInequalities(nInequalities, nChows, pGreaters,
+            pSmallers);
+
+    //initializes the weights
+    pWofChow[0] = Wmin;
+    for (i = 1; i < nChows; i++) {
+        pWofChow[i] = pWofChow[i - 1] + 1;
+    }
+    i = 0;
+
+    //assign the weights respecting the inequalities
+    while (i < nChows && pWofChow[nChows - 1] <= Limit) {
+        Lmin = 1000;
+        Lmax = 0;
+
+        while (j < nInequalities) {
+            if (pGreaters[j][i] != 0) {
+                Lmin = Extra_ThreshCubeWeightedSum3(pWofChow, nChows, pGreaters,
+                        j);
+                Lmax = Extra_ThreshCubeWeightedSum4(pWofChow, nChows, pSmallers,
+                        j);
+                delta = Lmin - Lmax;
+
+                if (delta > 0) {
+                    if (fIncremented == 1) {
+                        j = 0;
+                        fIncremented = 0;
+                        deltaOld = -1000;
+                    } else
+                        j++;
+                    continue;
+                }
+                if (delta > deltaOld) {
+                    Extra_ThreshIncrementWeights(nChows, pWofChow, i);
+                    deltaOld = delta;
+                    fIncremented = 1;
+                } else if (fIncremented == 1) {
+                    Extra_ThreshDecrementWeights(nChows, pWofChow, i);
+                    j++;
+                    deltaOld = -1000;
+                    fIncremented = 0;
+                    continue;
+                } else
+                    j++;
+            } else
+                j++;
+
+        }
+        i++;
+        j = 0;
+    }
+
+    //******************************
+    for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+        free(pGreaters[i]);
+    }
+    free(pGreaters);
+    for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
+        free(pSmallers[i]);
+    }
+    free(pSmallers);
+    //******************************
+
+    i = 0;
+    Lmin = 1000;
+    Lmax = 0;
+
+    //check the assigned weights in the original system
+    for (j = 0; j < (int)strlen(pIsop); j += (nVars + 3))
+        Lmin = Abc_MinInt(Lmin,
+                Extra_ThreshCubeWeightedSum1(pWofChow, pChow, pIsop, nVars, j));
+    for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3))
+        Lmax = Abc_MaxInt(Lmax,
+                Extra_ThreshCubeWeightedSum2(pWofChow, pChow, pIsopFneg, nVars,
+                        j));
+
+    for (i = 0; i < nVars; i++) {
+        pW[i] = pWofChow[pChow[i]];
+    }
+
+    ABC_FREE( pWofChow );
+    if (Lmin > Lmax)
+        return Lmin;
+    else
+        return 0;
+}
+void Extra_ThreshPrintWeights(int T, int * pW, int nVars) {
+    int i;
+
+    if (T == 0)
+        fprintf( stdout, "\nHeuristic method: is not TLF\n\n");
+    else {
+        fprintf( stdout, "\nHeuristic method: Weights and threshold value:\n");
+        for (i = 0; i < nVars; i++)
+            printf("%d ", pW[i]);
+        printf("  %d\n", T);
+    }
+}
+/**Function*************************************************************
+
+
+ Synopsis    [Checks thresholdness of the function.]
+
+ Description []
+
+ SideEffects []
+
+
+ SeeAlso     []
+
+ ***********************************************************************/
+int Extra_ThreshCheck(word * t, int nVars, int * pW) {
     int Chow0, Chow[16];
-    if ( !Abc_TtIsUnate(t, nVars) )
+    if (!Abc_TtIsUnate(t, nVars))
         return 0;
-    Abc_TtMakePosUnate( t, nVars );
-    Chow0 = Extra_ThreshComputeChow( t, nVars, Chow );
-    Extra_ThreshSortByChow( t, nVars, Chow );
-    return Extra_ThreshSelectWeights( t, nVars, pW );
+    Abc_TtMakePosUnate(t, nVars);
+    Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
+    Extra_ThreshSortByChow(t, nVars, Chow);
+    return Extra_ThreshSelectWeights(t, nVars, pW);
+}
+/**Function*************************************************************
+
+
+ Synopsis    [Checks thresholdness of the function by using a heuristic method.]
+
+ Description []
+
+ SideEffects []
+
+
+ SeeAlso     []
+
+ ***********************************************************************/
+int Extra_ThreshHeuristic(word * t, int nVars, int * pW) {
+
+    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+    int Chow0, Chow[16], nChows, i, T = 0;
+    DdManager * dd;
+    Vec_Str_t * vCube;
+    DdNode * ddNode, * ddNodeFneg;
+    char * pIsop, * pIsopFneg;
+    if (nVars <= 1)
+        return 1;
+    if (!Abc_TtIsUnate(t, nVars))
+        return 0;
+    Abc_TtMakePosUnate(t, nVars);
+    Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
+    Extra_ThreshSortByChowInverted(t, nVars, Chow);
+    nChows = Extra_ThreshInitializeChow(nVars, Chow);
+
+    dd = (DdManager *) Abc_FrameReadManDd();
+    vCube = Vec_StrAlloc(nVars);
+    for (i = 0; i < nVars; i++)
+        Cudd_bddIthVar(dd, i);
+    ddNode = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
+    Cudd_Ref(ddNode);
+    pIsop = Abc_ConvertBddToSop( NULL, dd, ddNode, ddNode, nVars, 1,
+            vCube, 1);
+
+    Abc_TtNot(t, Abc_TruthWordNum(nVars));
+    ddNodeFneg = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
+    Cudd_Ref(ddNodeFneg);
+
+    pIsopFneg = Abc_ConvertBddToSop( NULL, dd, ddNodeFneg, ddNodeFneg,
+            nVars, 1, vCube, 1);
+
+    Cudd_RecursiveDeref(dd, ddNode);
+    Cudd_RecursiveDeref(dd, ddNodeFneg);
+
+    T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow, nChows,
+            1);
+
+    for (i = 2; (i < 4) && (T == 0) && (nVars >= 6); i++)
+        T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow,
+                nChows, i);
+
+    free(pIsop);
+    free(pIsopFneg);
+    Vec_StrFree(vCube);
+
+    return T;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks unateness of a function.]
+ Synopsis    [Checks unateness of a function.]
+
+ Description []
 
-  Description []
-               
-  SideEffects []
+ SideEffects []
 
-  SeeAlso     []
+ SeeAlso     []
 
-***********************************************************************/
-void Extra_ThreshCheckTest()
-{
-    int nVars = 5;
+ ***********************************************************************/
+void Extra_ThreshCheckTest() {
+    int nVars = 6;
     int T, Chow0, Chow[16], Weights[16];
 //    word t =  s_Truths6[0] & s_Truths6[1] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4];
 //    word t =  (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]);
-    word t =  (s_Truths6[2] & s_Truths6[1]) | (s_Truths6[2] & s_Truths6[0] & s_Truths6[3]) | (s_Truths6[2] & s_Truths6[0] & ~s_Truths6[4]);
+//    word t = (s_Truths6[2] & s_Truths6[1])
+//            | (s_Truths6[2] & s_Truths6[0] & s_Truths6[3])
+//            | (s_Truths6[2] & s_Truths6[0] & ~s_Truths6[4]);
+    word t = (s_Truths6[0] & s_Truths6[1] & s_Truths6[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
 //    word t =  (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]);
 //    word t =  (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]) | 
 //        (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[5]);
     int i;
-    assert( nVars <= 8 );
-    for ( i = 0; i < nVars; i++ )
-        printf( "%d %d %d\n", i, Abc_TtPosVar(&t, nVars, i), Abc_TtNegVar(&t, nVars, i) );
+    assert(nVars <= 8);
+    for (i = 0; i < nVars; i++)
+        printf("%d %d %d\n", i, Abc_TtPosVar(&t, nVars, i),
+                Abc_TtNegVar(&t, nVars, i));
 //    word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
-    Chow0 = Extra_ThreshComputeChow( &t, nVars, Chow );
-    if ( (T = Extra_ThreshCheck(&t, nVars, Weights)) )
-        Extra_ThreshPrintChow( T, Weights, nVars );
+    Chow0 = Extra_ThreshComputeChow(&t, nVars, Chow);
+    if ((T = Extra_ThreshCheck(&t, nVars, Weights)))
+        Extra_ThreshPrintChow(T, Weights, nVars);
     else
-        printf( "No threshold\n" );
+        printf("No threshold\n");
 }
+void Extra_ThreshHeuristicTest() {
+    int nVars = 6;
+    int T, Weights[16];
 
+    //    word t = 19983902376700760000;
+    word t = (s_Truths6[0] & s_Truths6[1] & s_Truths6[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
+    word * pT = &t;
+    T = Extra_ThreshHeuristic(pT, nVars, Weights);
+    Extra_ThreshPrintWeights(T, Weights, nVars);
+
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
 ABC_NAMESPACE_IMPL_END