Detection of threshold functions.

4 files changed, 434 insertions, 53 deletions

diff --git a/src/misc/extra/extraUtilThresh.c b/src/misc/extra/extraUtilThresh.c
new file mode 100644
index 00000000..88752b7d
--- /dev/null
+++ b/src/misc/extra/extraUtilThresh.c
@@ -0,0 +1,333 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilThresh.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Dealing with threshold functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  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 "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);
+    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;
+    }
+}
+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;
+}
+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;
+}
+int Extra_ThreshCheck( word * t, int nVars, int * pW )
+{
+    int Chow[16], Chow0, nMints = (1 << 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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks unateness of a function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_ThreshCheckTest()
+{
+    int nVars = 5;
+    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[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" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 1503cec1..87ba8559 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -18,5 +18,6 @@ SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraUtilProgress.c \
     src/misc/extra/extraUtilReader.c \
     src/misc/extra/extraUtilSupp.c \
+    src/misc/extra/extraUtilTrash.c \
     src/misc/extra/extraUtilTruth.c \
     src/misc/extra/extraUtilUtil.c
diff --git a/src/misc/util/utilIsop.c b/src/misc/util/utilIsop.c
index f42dcabe..a62fc84d 100644
--- a/src/misc/util/utilIsop.c
+++ b/src/misc/util/utilIsop.c
@@ -95,47 +95,6 @@ static inline void Abc_IsopAddLits( int * pCover, int nCost0, int nCost1, int Va
     for ( c = 0; c < nCost1; c++ )
         pCover[nCost0+c] |= (1 << Abc_Var2Lit(Var,1));
 }
-int Abc_Isop6Cover2( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
-{
-    word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
-    int Var, nCost0, nCost1, nCost2;
-    assert( nVars <= 6 );
-    assert( (uOn & ~uOnDc) == 0 );
-    if ( uOn == 0 )
-    {
-        pRes[0] = 0;
-        return 0;
-    }
-    if ( uOnDc == ~(word)0 )
-    {
-        pRes[0] = ~(word)0;
-        if ( pCover ) pCover[0] = 0;
-        return (1 << 16);
-    }
-    assert( nVars > 0 );
-    // find the topmost var
-    for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
-             break;
-    assert( Var >= 0 );
-    // cofactor
-    uOn0   = Abc_Tt6Cofactor0( uOn,   Var );
-    uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
-    uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
-    uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
-    // solve for cofactors
-    nCost0 = Abc_Isop6Cover2( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_Isop6Cover2( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
-    nCost2 = Abc_Isop6Cover2( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
-    // derive the final truth table
-    *pRes = uRes2 | (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
-    assert( (uOn & ~*pRes) == 0 && (*pRes & ~uOnDc) == 0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, Var );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
-}
 int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
 {
     word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
@@ -164,13 +123,10 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
     uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
     uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
     uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
-//R0 = bsop(L0&~(U1 | (L1 &  ~U0)),U0,new_varbs)
     // solve for cofactors
-//    nCost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
-    nCost0 = Abc_Isop6Cover( uOn0 & ~(uOnDc1 | (uOn1 & ~uOnDc0)), uOnDc0, &uRes0, Var, nCostLim, pCover );
+    nCost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
     if ( nCost0 >= nCostLim ) return nCostLim;
-//    nCost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    nCost1 = Abc_Isop6Cover( uOn1 & ~(uOnDc0 | (uOn0 & ~uOnDc1)), uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
+    nCost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
     if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
     nCost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
     if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
@@ -180,7 +136,6 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
     Abc_IsopAddLits( pCover, nCost0, nCost1, Var );
     return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
 }
-
 int Abc_Isop7Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
 {
     word uOn0, uOn1, uOn2, uOnDc2, uRes0, uRes1, uRes2;
@@ -622,13 +577,11 @@ int Abc_Isop( word * pFunc, int nVars, int Type, int nCubeLim, Vec_Int_t * vCove
 ***********************************************************************/
 int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
 {
-    int fVerbose = 1;
+    int Cost, fVerbose = 0;
     word pRes[1024];
-    int Cost;
 //    if ( fVerbose )
 //    Dau_DsdPrintFromTruth( pFunc, nVars ), printf( "         " );
 
-
     Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
     vCover->nSize = Cost >> 16;
     assert( vCover->nSize <= vCover->nCap );
@@ -646,7 +599,7 @@ int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
     printf( "%5d(%5d) ", Cost >> 16, Cost & 0xFFFF );
     Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
 
-/*
+
     Cost = Abc_EsopCheck( pFunc, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
     vCover->nSize = Cost >> 16;
     assert( vCover->nSize <= vCover->nCap );
@@ -663,12 +616,11 @@ int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
     if ( fVerbose )
     printf( "%5d(%5d)  ", Cost >> 16, Cost & 0xFFFF );
     Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
-*/
+
 
     if ( fVerbose )
     printf( "\n" );
 //Kit_TruthIsopPrintCover( vCover, nVars, 0 );
-
     return 1; 
 }
 
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 1416034d..0b52b3f4 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1597,6 +1597,101 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks unateness of a function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_Tt6PosVar( word t, int iVar )
+{
+    return ((t >> (1<<iVar)) & t & s_Truths6Neg[iVar]) == (t & s_Truths6Neg[iVar]);
+}
+static inline int Abc_Tt6NegVar( word t, int iVar )
+{
+    return ((t << (1<<iVar)) & t & s_Truths6[iVar]) == (t & s_Truths6[iVar]);
+}
+static inline int Abc_TtPosVar( word * t, int nVars, int iVar )
+{
+    assert( iVar < nVars );
+    if ( nVars <= 6 )
+        return Abc_Tt6PosVar( t[0], iVar );
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        int nWords = Abc_TtWordNum( nVars );
+        for ( i = 0; i < nWords; i++ )
+            if ( ((t[i] >> Shift) & t[i] & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + Abc_TtWordNum( nVars );
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != (t[i] & t[Step+i]) )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtNegVar( word * t, int nVars, int iVar )
+{
+    assert( iVar < nVars );
+    if ( nVars <= 6 )
+        return Abc_Tt6NegVar( t[0], iVar );
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        int nWords = Abc_TtWordNum( nVars );
+        for ( i = 0; i < nWords; i++ )
+            if ( ((t[i] << Shift) & t[i] & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + Abc_TtWordNum( nVars );
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( (t[i] & t[Step+i]) != t[Step+i] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtIsUnate( word * t, int nVars )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        if ( !Abc_TtNegVar(t, nVars, i) && !Abc_TtPosVar(t, nVars, i) )
+            return 0;
+    return 1;
+}
+static inline int Abc_TtIsPosUnate( word * t, int nVars )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        if ( !Abc_TtPosVar(t, nVars, i) )
+            return 0;
+    return 1;
+}
+static inline void Abc_TtMakePosUnate( word * t, int nVars )
+{
+    int i, nWords = Abc_TtWordNum(nVars);
+    for ( i = 0; i < nVars; i++ )
+        if ( Abc_TtNegVar(t, nVars, i) )
+            Abc_TtFlip( t, nWords, i );
+        else assert( Abc_TtPosVar(t, nVars, i) );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes ISOP for 6 variables or less.]
 
   Description []