Various changes.

6 files changed, 1211 insertions, 1 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 42eb71d5..51b4b2e3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -216,6 +216,7 @@ struct Gia_Man_t_
     Vec_Wrd_t *    vSimsPo;
     Vec_Int_t *    vClassOld;
     Vec_Int_t *    vClassNew;
+    Vec_Int_t *    vPats;
     // incremental simulation
     int            fIncrSim;
     int            iNextPi;
@@ -1275,6 +1276,11 @@ extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose );
 extern Gia_Man_t *         Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
+/*=== giaDecs.c ============================================================*/
+extern int                 Gia_ResubVarNum( Vec_Int_t * vResub );
+extern word                Gia_ResubToTruth6( Vec_Int_t * vResub );
+extern int                 Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose );
+extern Vec_Int_t *         Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type );
 /*=== giaDfs.c ============================================================*/
 extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
 extern void                Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes );
diff --git a/src/aig/gia/giaDecs.c b/src/aig/gia/giaDecs.c
new file mode 100644
index 00000000..343891d5
--- /dev/null
+++ b/src/aig/gia/giaDecs.c
@@ -0,0 +1,350 @@
+/**CFile****************************************************************
+
+  FileName    [giaDecs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Calling various decomposition engines.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaDecs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/gia/gia.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
+#include "bool/bdc/bdc.h"
+#include "bool/kit/kit.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
+extern Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc, int Depth );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ResubVarNum( Vec_Int_t * vResub )
+{
+    if ( Vec_IntSize(vResub) == 1 )
+        return Vec_IntEntryLast(vResub) >= 2;
+    return Vec_IntEntryLast(vResub)/2 - Vec_IntSize(vResub)/2 - 1;
+}
+word Gia_ResubToTruth6_rec( Vec_Int_t * vResub, int iNode, int nVars )
+{
+    assert( iNode >= 0 && nVars <= 6 );
+    if ( iNode < nVars )
+        return s_Truths6[iNode];
+    else
+    {
+        int iLit0 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 0) );
+        int iLit1 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 1) );
+        word Res0 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit0)-2, nVars );
+        word Res1 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit1)-2, nVars );
+        Res0 = Abc_LitIsCompl(iLit0) ? ~Res0 : Res0;
+        Res1 = Abc_LitIsCompl(iLit1) ? ~Res1 : Res1;
+        return iLit0 > iLit1 ? Res0 ^ Res1 : Res0 & Res1;
+    }
+}
+word Gia_ResubToTruth6( Vec_Int_t * vResub )
+{
+    word Res;
+    int iRoot = Vec_IntEntryLast(vResub);
+    if ( iRoot < 2 )
+        return iRoot ? ~(word)0 : 0;
+    assert( iRoot != 2 && iRoot != 3 );
+    Res = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iRoot)-2, Gia_ResubVarNum(vResub) );
+    return Abc_LitIsCompl(iRoot) ? ~Res : Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Gia_ManDeriveTruths( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords )
+{
+    int nTtWords = Abc_Truth6WordNum(Vec_IntSize(vSet));
+    int nFuncs = Vec_WrdSize(vIsfs) / 2 / nWords;
+    Vec_Wrd_t * vRes = Vec_WrdStart( 2 * nFuncs * nTtWords );
+    Vec_Wrd_t * vIn = Vec_WrdStart( 64*nWords ), * vOut;
+    int i, f, m, iObj; word Func;
+    assert( Vec_IntSize(vSet) <= 64 );
+    Vec_IntForEachEntry( vSet, iObj, i )
+        Abc_TtCopy( Vec_WrdEntryP(vIn, i*nWords), Vec_WrdEntryP(vSims, Vec_IntEntry(vCands, iObj)*nWords), nWords, 0 );
+    vOut = Vec_WrdStart( Vec_WrdSize(vIn) );
+    Extra_BitMatrixTransposeP( vIn, nWords, vOut, 1 );
+    for ( f = 0; f < nFuncs; f++ )
+    {
+        word * pIsf[2]   = { Vec_WrdEntryP(vIsfs, (2*f+0)*nWords), 
+                             Vec_WrdEntryP(vIsfs, (2*f+1)*nWords) };
+        word * pTruth[2] = { Vec_WrdEntryP(vRes, (2*f+0)*nTtWords), 
+                             Vec_WrdEntryP(vRes, (2*f+1)*nTtWords) };
+        for ( m = 0; m < 64*nWords; m++ )
+        {
+            int iMint = (int)Vec_WrdEntry(vOut, m);
+            int Value0 = Abc_TtGetBit( pIsf[0], m );
+            int Value1 = Abc_TtGetBit( pIsf[1], m );
+            if ( !Value0 && !Value1 )
+                continue;
+            if ( Value0 && Value1 )
+                printf( "Internal error: Onset and Offset overlap.\n" );
+            assert( !Value0 || !Value1 );
+            Abc_TtSetBit( pTruth[Value1], iMint );
+        }
+        if ( Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) )
+            printf( "Verification for function %d failed for %d minterm pairs.\n", f,
+                Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) );
+    }
+    if ( Vec_IntSize(vSet) < 6 )
+        Vec_WrdForEachEntry( vRes, Func, i )
+            Vec_WrdWriteEntry( vRes, i, Abc_Tt6Stretch(Func, Vec_IntSize(vSet)) );
+    Vec_WrdFree( vIn );
+    Vec_WrdFree( vOut );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCountResub( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
+{
+    Vec_Int_t * vResub; int nNodes;
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords;
+    Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars );
+    Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars );
+    assert( Vec_WrdSize(vElems) == nTtWords * nVars );
+    assert( nFuncs == 1 );
+    Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) );
+    Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) );
+    for ( v = 0; v < nVars; v++ )
+        Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) );
+    vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, fVerbose, NULL, 0 );
+    Vec_PtrFree( vDivs );
+    Vec_WrdFree( vElems );
+    nNodes = Vec_IntSize(vResub) ? Vec_IntSize(vResub)/2 : 999;
+    Vec_IntFree( vResub );
+    return nNodes;
+}
+Vec_Int_t * Gia_ManDeriveResub( Vec_Wrd_t * vTruths, int nVars )
+{
+    Vec_Int_t * vResub;  
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords;
+    Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars );
+    Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars );
+    assert( Vec_WrdSize(vElems) == nTtWords * nVars );
+    assert( nFuncs == 1 );
+    Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) );
+    Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) );
+    for ( v = 0; v < nVars; v++ )
+        Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) );
+    vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, 0, NULL, 0 );
+    Vec_PtrFree( vDivs );
+    Vec_WrdFree( vElems );
+    return vResub;
+}
+
+int Gia_ManCountBidec( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
+{
+    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords );
+    nNodes = Bdc_ManBidecNodeNum( pTruth[1], pTruth[0], nVars, fVerbose );
+    Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords );
+    return nNodes;
+}
+Vec_Int_t * Gia_ManDeriveBidec( Vec_Wrd_t * vTruths, int nVars )
+{
+    Vec_Int_t * vRes = NULL;
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords );
+    vRes = Bdc_ManBidecResub( pTruth[1], pTruth[0], nVars );
+    Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords );
+    return vRes;
+}
+
+int Gia_ManCountIsop( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
+{
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    int nNodes = Kit_IsopNodeNum( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL );
+    return nNodes;
+}
+Vec_Int_t * Gia_ManDeriveIsop( Vec_Wrd_t * vTruths, int nVars )
+{
+    Vec_Int_t * vRes = NULL;
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    vRes = Kit_IsopResub( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL );
+    return vRes;
+}
+
+int Gia_ManCountBdd( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
+{
+    extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose );
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    Gia_Man_t * pGia; int nNodes;
+
+    Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords );
+    Abc_TtNot( pTruth[0], nTtWords );
+    pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 );
+    Abc_TtNot( pTruth[0], nTtWords );
+    Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords );
+
+    nNodes = Gia_ManAndNum(pGia);
+    Gia_ManStop( pGia );
+    return nNodes;
+}
+Vec_Int_t * Gia_ManDeriveBdd( Vec_Wrd_t * vTruths, int nVars )
+{
+    extern Vec_Int_t * Gia_ManToGates( Gia_Man_t * p );
+    Vec_Int_t * vRes = NULL;
+    extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose );
+    int nTtWords = Abc_Truth6WordNum(nVars);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    Gia_Man_t * pGia;
+
+    Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords );
+    Abc_TtNot( pTruth[0], nTtWords );
+    pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 );
+    Abc_TtNot( pTruth[0], nTtWords );
+    Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords );
+
+    vRes = Gia_ManToGates( pGia );
+    Gia_ManStop( pGia );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose )
+{
+    Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords );
+    int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    int nNodesResub = Gia_ManCountResub( vTruths, nVars, 0 );
+    int nNodesBidec = nVars > 2 ? Gia_ManCountBidec( vTruths, nVars, 0 ) : 999;
+    int nNodesIsop  = nVars > 2 ? Gia_ManCountIsop( vTruths, nVars, 0 ) : 999;
+    int nNodesBdd   = nVars > 2 ? Gia_ManCountBdd( vTruths, nVars, 0 ) : 999;
+    int nNodesMin   = Abc_MinInt( Abc_MinInt(nNodesResub, nNodesBidec), Abc_MinInt(nNodesIsop, nNodesBdd) );
+    if ( fVerbose )
+    {
+        printf( "Size = %2d  ", nVars );
+        printf( "Resub =%3d  ", nNodesResub );
+        printf( "Bidec =%3d  ", nNodesBidec );
+        printf( "Isop =%3d  ",  nNodesIsop );
+        printf( "Bdd =%3d  ",   nNodesBdd );
+        Abc_TtIsfPrint( pTruth[0], pTruth[1], nTtWords ); 
+        if ( nVars <= 6 )
+        {
+            printf( "  " );
+            Extra_PrintHex( stdout, (unsigned*)pTruth[0], nVars );
+            printf( "  " );
+            Extra_PrintHex( stdout, (unsigned*)pTruth[1], nVars );
+        }
+        printf( "\n" );
+    }
+    Vec_WrdFree( vTruths );
+    if ( nNodesMin > 500 )
+        return -1;
+    if ( nNodesMin == nNodesResub )
+        return (nNodesMin << 2) | 0;
+    if ( nNodesMin == nNodesBidec )
+        return (nNodesMin << 2) | 1;
+    if ( nNodesMin == nNodesIsop )
+        return (nNodesMin << 2) | 2;
+    if ( nNodesMin == nNodesBdd )
+        return (nNodesMin << 2) | 3;
+    return -1;
+}
+Vec_Int_t * Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type )
+{
+    Vec_Int_t * vRes = NULL;
+    Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords );
+    int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet);
+    word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), 
+                         Vec_WrdEntryP(vTruths, 1*nTtWords) };
+    if ( Type == 0 )
+        vRes = Gia_ManDeriveResub( vTruths, nVars );
+    else if ( Type == 1 )
+        vRes = Gia_ManDeriveBidec( vTruths, nVars );
+    else if ( Type == 2 )
+        vRes = Gia_ManDeriveIsop( vTruths, nVars );
+    else if ( Type == 3 )
+        vRes = Gia_ManDeriveBdd( vTruths, nVars );
+    if ( vRes && Gia_ResubVarNum(vRes) <= 6 )
+    {
+        word Func = Gia_ResubToTruth6( vRes );
+        assert( !(Func &  pTruth[0][0]) );
+        assert( !(pTruth[1][0] & ~Func) );   
+    }
+    Vec_WrdFree( vTruths );
+    return vRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 772dc31a..464835e4 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -94,6 +94,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vStore );
     Vec_IntFreeP( &p->vClassNew );
     Vec_IntFreeP( &p->vClassOld );
+    Vec_IntFreeP( &p->vPats );
     Vec_WrdFreeP( &p->vSims );
     Vec_WrdFreeP( &p->vSimsT );
     Vec_WrdFreeP( &p->vSimsPi );
diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index a5017b7d..33fd5276 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -651,6 +651,37 @@ Gia_Man_t * Gia_ManConstructFromGates2( Vec_Wec_t * vFuncs, Vec_Wec_t * vDivs, i
         Vec_IntFree( vSupp );
     return pNew;
 }
+Vec_Int_t * Gia_ManToGates( Gia_Man_t * p )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 2*Gia_ManAndNum(p) + 1 );
+    Gia_Obj_t * pRoot = Gia_ManCo( p, 0 );
+    int iRoot = Gia_ObjFaninId0p(p, pRoot) - 1;
+    int nVars = Gia_ManCiNum(p);
+    assert( Gia_ManCoNum(p) == 1 );
+    if ( iRoot == -1 )
+        Vec_IntPush( vRes, Gia_ObjFaninC0(pRoot) );
+    else if ( iRoot < nVars )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) );
+    else
+    {
+        Gia_Obj_t * pObj, * pLast = NULL; int i;
+        Gia_ManForEachCi( p, pObj, i )
+            assert( Gia_ObjId(p, pObj) == i+1 );
+        Gia_ManForEachAnd( p, pObj, i )
+        {
+            int iLit0 = Abc_Var2Lit( Gia_ObjFaninId0(pObj, i) - 1, Gia_ObjFaninC0(pObj) );
+            int iLit1 = Abc_Var2Lit( Gia_ObjFaninId1(pObj, i) - 1, Gia_ObjFaninC1(pObj) );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+            pLast = pObj;
+        }
+        assert( pLast == Gia_ObjFanin0(pRoot) );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) );
+    }
+    assert( Vec_IntSize(vRes) == 2*Gia_ManAndNum(p) + 1 );
+    return vRes;
+}
 
 /**Function*************************************************************
 
@@ -1378,7 +1409,10 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth )
             if ( iResLit >= 0 ) 
             {
                 int iNode = nVars + Vec_IntSize(p->vGates)/2;
-                Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) );
+                if ( iDiv < iResLit )
+                    Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) );
+                else
+                    Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_LitNot(iDiv) );
                 return Abc_Var2Lit( iNode, fUseOr );
             }
         }
diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c
new file mode 100644
index 00000000..f95d815d
--- /dev/null
+++ b/src/aig/gia/giaSupps.c
@@ -0,0 +1,817 @@
+/**CFile****************************************************************
+
+  FileName    [giaSupp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Support computation manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/gia/gia.h"
+#include "base/main/mainInt.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
+#include "misc/vec/vecHsh.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Supp_Man_t_ Supp_Man_t;
+struct Supp_Man_t_
+{
+    // user data
+    int         nIters;     // optimization rounds
+    int         nRounds;    // optimization rounds
+    int         nWords;     // the number of simulation words
+    int         nDivWords;  // the number of divisor words
+    Vec_Wrd_t * vIsfs;      // functions to synthesize
+    Vec_Int_t * vCands;     // candidate divisors
+    Vec_Int_t * vWeights;   // divisor weights (optional)
+    Vec_Wrd_t * vSims;      // simulation values
+    Vec_Wrd_t * vSimsC;     // simulation values
+    Gia_Man_t * pGia;       // used for object names
+    // computed data
+    Vec_Wrd_t * vDivs[2];   // simulation values
+    Vec_Wrd_t * vPats[2];   // simulation values
+    Vec_Ptr_t * vMatrix;    // simulation values
+    Vec_Wrd_t * vMask;      // simulation values
+    Vec_Wrd_t * vRowTemp;   // simulation values
+    Vec_Int_t * vCosts;     // candidate costs
+    Hsh_VecMan_t * pHash;   // subsets considered
+    Vec_Wrd_t * vSFuncs;    // ISF storage
+    Vec_Int_t * vSStarts;   // subset function starts
+    Vec_Int_t * vSCount;    // subset function count
+    Vec_Int_t * vSPairs;    // subset pair count
+    Vec_Int_t * vTemp;      // temporary
+    Vec_Int_t * vTempSets;  // temporary
+    Vec_Int_t * vTempPairs; // temporary
+    Vec_Wec_t * vSolutions; // solutions for each node count
+};
+
+extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Supp_ManFuncInit( Vec_Wrd_t * vFuncs, int nWords )
+{
+    int i, k = 0, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2;
+    assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) );
+    for ( i = 0; i < nFuncs; i++ )
+    {
+        word * pFunc0 = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords);
+        word * pFunc1 = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords);
+        if ( Abc_TtIsConst0(pFunc0, nWords) || Abc_TtIsConst0(pFunc1, nWords) )
+            continue;
+        if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), pFunc0, nWords, 0 );
+        if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), pFunc1, nWords, 0 );
+        k++;
+    }
+    Vec_WrdShrink( vFuncs, 2*k*nWords );
+    return k;
+}
+int Supp_ManCostInit( Vec_Wrd_t * vFuncs, int nWords )
+{
+    int Res = 0, i, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2;
+    assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) );
+    for ( i = 0; i < nFuncs; i++ )
+    {
+        word * pFunc0 = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords);
+        word * pFunc1 = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords);
+        Res += Abc_TtCountOnesVec(pFunc0, nWords) * Abc_TtCountOnesVec(pFunc1, nWords);
+    }
+    assert( nFuncs < 128 );
+    assert( Res < (1 << 24) );
+    return (nFuncs << 24) | Res;
+}
+void Supp_ManInit( Supp_Man_t * p )
+{
+    int Value, nFuncs, iSet = Hsh_VecManAdd( p->pHash, p->vTemp ); // empty set
+    assert( iSet == 0 );
+    Vec_IntPush( p->vSStarts, Vec_WrdSize(p->vSFuncs) );
+    Vec_WrdAppend( p->vSFuncs, p->vIsfs );
+    nFuncs = Supp_ManFuncInit( p->vSFuncs, p->nWords );
+    assert( Vec_WrdSize(p->vSFuncs) == 2 * nFuncs * p->nWords );
+    Value = Supp_ManCostInit(p->vSFuncs, p->nWords);
+    Vec_IntPush( p->vSCount, Value >> 24 );
+    Vec_IntPush( p->vSPairs, Value & 0xFFFFFF );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Supp_DeriveLines( Supp_Man_t * p )
+{
+    int n, i, iObj, nWords = p->nWords;
+    int nDivWords = Abc_Bit6WordNum( Vec_IntSize(p->vCands) );
+    for ( n = 0; n < 2; n++ )
+    {
+        p->vDivs[n] = Vec_WrdStart( 64*nWords*nDivWords );
+        p->vPats[n] = Vec_WrdStart( 64*nWords*nDivWords );
+        if ( p->vSimsC )
+            Vec_IntForEachEntry( p->vCands, iObj, i )
+                Abc_TtAndSharp( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSimsC, iObj*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n );
+        else
+            Vec_IntForEachEntry( p->vCands, iObj, i )
+                Abc_TtCopy( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n );
+        Extra_BitMatrixTransposeP( p->vDivs[n], nWords, p->vPats[n], nDivWords );
+    }
+    return nDivWords;
+}
+Supp_Man_t * Supp_ManCreate( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vWeights, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC, int nWords, Gia_Man_t * pGia, int nIters, int nRounds )
+{
+    Supp_Man_t * p = ABC_CALLOC( Supp_Man_t, 1 );
+    p->nIters     = nIters;
+    p->nRounds    = nRounds;
+    p->nWords     = nWords;
+    p->vIsfs      = vIsfs;
+    p->vCands     = vCands;
+    p->vWeights   = vWeights;
+    p->vSims      = vSims;
+    p->vSimsC     = vSimsC;
+    p->pGia       = pGia;
+    // computed data
+    p->nDivWords  = Supp_DeriveLines( p );
+    p->vMatrix    = Vec_PtrAlloc( 100 );
+    p->vMask      = Vec_WrdAlloc( 100 );
+    p->vRowTemp   = Vec_WrdStart( 64*p->nDivWords );
+    p->vCosts     = Vec_IntStart( Vec_IntSize(p->vCands) );
+    p->pHash      = Hsh_VecManStart( 1000 );
+    p->vSFuncs    = Vec_WrdAlloc( 1000 );
+    p->vSStarts   = Vec_IntAlloc( 1000 );
+    p->vSCount    = Vec_IntAlloc( 1000 );
+    p->vSPairs    = Vec_IntAlloc( 1000 );
+    p->vSolutions = Vec_WecStart( 16 );
+    p->vTemp      = Vec_IntAlloc( 10 );
+    p->vTempSets  = Vec_IntAlloc( 10 );
+    p->vTempPairs = Vec_IntAlloc( 10 );
+    Supp_ManInit( p );
+    return p;
+}
+void Supp_ManCleanMatrix( Supp_Man_t * p )
+{
+    Vec_Wrd_t * vTemp; int i;
+    Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, i )
+        Vec_WrdFreeP( &vTemp );
+    Vec_PtrClear( p->vMatrix );
+}
+void Supp_ManDelete( Supp_Man_t * p )
+{
+    Supp_ManCleanMatrix( p );
+    Vec_WrdFreeP( &p->vDivs[0] );
+    Vec_WrdFreeP( &p->vDivs[1] );
+    Vec_WrdFreeP( &p->vPats[0] );
+    Vec_WrdFreeP( &p->vPats[1] );
+    Vec_PtrFreeP( &p->vMatrix );
+    Vec_WrdFreeP( &p->vMask );
+    Vec_WrdFreeP( &p->vRowTemp );
+    Vec_IntFreeP( &p->vCosts );
+    Hsh_VecManStop( p->pHash );
+    Vec_WrdFreeP( &p->vSFuncs );
+    Vec_IntFreeP( &p->vSStarts );
+    Vec_IntFreeP( &p->vSCount );
+    Vec_IntFreeP( &p->vSPairs );
+    Vec_WecFreeP( &p->vSolutions );
+    Vec_IntFreeP( &p->vTemp );
+    Vec_IntFreeP( &p->vTempSets );
+    Vec_IntFreeP( &p->vTempPairs );
+    ABC_FREE( p );
+}
+int Supp_ManMemory( Supp_Man_t * p )
+{
+    int nMem = sizeof(Supp_Man_t);
+    nMem += 2*(int)Vec_WrdMemory( p->vDivs[0] );
+    nMem += 2*(int)Vec_WrdMemory( p->vPats[0] );
+    nMem += (Vec_PtrSize(p->vMatrix)+1)*(int)Vec_WrdMemory( p->vRowTemp );
+    nMem += (int)Vec_WrdMemory( p->vMask );
+    nMem += (int)Vec_IntMemory( p->vCosts );
+    nMem += (int)Hsh_VecManMemory( p->pHash );
+    nMem += (int)Vec_WrdMemory( p->vSFuncs );
+    nMem += (int)Vec_IntMemory( p->vSStarts );
+    nMem += (int)Vec_IntMemory( p->vSCount );
+    nMem += (int)Vec_IntMemory( p->vSPairs );
+    nMem += (int)Vec_WecMemory( p->vSolutions );
+    nMem += (int)Vec_IntMemory( p->vTemp );
+    nMem += (int)Vec_IntMemory( p->vTempSets );
+    nMem += (int)Vec_IntMemory( p->vTempPairs );
+    return nMem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Supp_ArrayWeight( Vec_Int_t * vRes, Vec_Int_t * vWeights )
+{
+    int i, iObj, Cost = 0;
+    if ( !vWeights )
+        return Vec_IntSize(vRes);
+    Vec_IntForEachEntry( vRes, iObj, i )
+        Cost += Vec_IntEntry(vWeights, iObj);
+    return Cost;
+}
+int Supp_SetWeight( Supp_Man_t * p, int iSet )
+{
+    return Supp_ArrayWeight( Hsh_VecReadEntry(p->pHash, iSet), p->vWeights );
+}
+int Supp_SetSize( Supp_Man_t * p, int iSet )
+{
+    return Vec_IntSize( Hsh_VecReadEntry(p->pHash, iSet) );
+}
+int Supp_SetFuncNum( Supp_Man_t * p, int iSet )
+{
+    return Vec_IntEntry(p->vSCount, iSet);
+}
+int Supp_SetPairNum( Supp_Man_t * p, int iSet )
+{
+    return Vec_IntEntry(p->vSPairs, iSet);
+}
+void Supp_SetConvert( Vec_Int_t * vSet, Vec_Int_t * vCands )
+{
+    int i, iObj;
+    Vec_IntForEachEntry( vSet, iObj, i )
+        Vec_IntWriteEntry( vSet, i, Vec_IntEntry(vCands, iObj) );
+}
+void Supp_PrintNodes( Gia_Man_t * pGia, Vec_Int_t * vObjs, int Skip, int Limit )
+{
+    int i, iObj;
+    //printf( "Considering %d targets: ", Vec_IntSize(vObjs) );
+    Vec_IntForEachEntryStart( vObjs, iObj, i, Skip )
+    {
+        if ( iObj < 0 )
+            continue;
+        printf( "(%d)", iObj );
+        if ( pGia && pGia->vWeights && Vec_IntEntry(pGia->vWeights, iObj) > 0 )
+            printf( "(%d)", Vec_IntEntry(pGia->vWeights, iObj) );
+        if ( pGia )
+            printf( " %s  ", Gia_ObjName(pGia, iObj)+2 );
+        else
+            printf( " n%d  ", iObj );
+        if ( i >= Limit )
+        {
+            printf( "...  " );
+            break;
+        }
+    }
+    printf( "Cost = %d", Supp_ArrayWeight(vObjs, pGia ? pGia->vWeights : NULL) );
+    printf( "\n" );
+}
+void Supp_PrintOne( Supp_Man_t * p, int iSet )
+{
+    Vec_Int_t * vSet = Hsh_VecReadEntry(p->pHash, iSet);
+    printf( "Set %5d :  ", iSet );
+    printf( "Funcs %2d  ", Supp_SetFuncNum(p, iSet) );
+    printf( "Pairs %4d  ", Supp_SetPairNum(p, iSet) );
+    printf( "Start %8d  ", Vec_IntEntry(p->vSStarts, iSet) );
+    printf( "Weight %4d  ", Supp_ArrayWeight(vSet, p->vWeights) );
+    Vec_IntClearAppend( p->vTemp, vSet );
+    Supp_SetConvert( p->vTemp, p->vCands );
+    Supp_PrintNodes( p->pGia, p->vTemp, 0, 6 );
+}
+int Supp_ManRefine1( Supp_Man_t * p, int iSet, int iObj )
+{
+    word * pSet = Vec_WrdEntryP( p->vSims, Vec_IntEntry(p->vCands, iObj)*p->nWords );
+    word * pIsf; int nFuncs  = Vec_IntEntry(p->vSCount, iSet);
+    int i, n, f, w, nFuncsNew = 0, Mark = Vec_WrdSize(p->vSFuncs), Res = 0;
+    if ( Vec_WrdSize(p->vSFuncs) + 4*nFuncs*p->nWords > Vec_WrdCap(p->vSFuncs) )
+        Vec_WrdGrow( p->vSFuncs, 2*Vec_WrdCap(p->vSFuncs) );
+    pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) );
+    for ( i = 0; i < nFuncs; i++ )
+    {
+        word * pFunc[2] = { pIsf + (2*i+0)*p->nWords, pIsf + (2*i+1)*p->nWords };
+        for ( f = 0; f < 2; f++ )
+        {
+            int nOnes[2], Start = Vec_WrdSize(p->vSFuncs);
+            for ( n = 0; n < 2; n++ )
+            {
+                word * pLimit = Vec_WrdLimit(p->vSFuncs);
+                if ( f )
+                    for ( w = 0; w < p->nWords; w++ )
+                        Vec_WrdPush( p->vSFuncs, pFunc[n][w] & pSet[w] );
+                else
+                    for ( w = 0; w < p->nWords; w++ )
+                        Vec_WrdPush( p->vSFuncs, pFunc[n][w] & ~pSet[w] );
+                nOnes[n] = Abc_TtCountOnesVec( pLimit, p->nWords );
+            }
+            if ( nOnes[0] && nOnes[1] )
+                Res += nOnes[0] * nOnes[1];
+            else
+                Vec_WrdShrink( p->vSFuncs, Start );
+        }
+    }
+    assert( Res < (1 << 24) );
+    nFuncsNew = (Vec_WrdSize(p->vSFuncs) - Mark)/2/p->nWords;
+    assert( nFuncsNew < 128 );
+    assert( nFuncsNew >= 0 && nFuncsNew <= 2*nFuncs );
+    return (nFuncsNew << 24) | Res;
+}
+void Supp_ManRefine( Supp_Man_t * p, int iSet, int iObj, int * pnFuncs, int * pnPairs )
+{
+    word * pDivs0 = Vec_WrdEntryP( p->vDivs[0], iObj*p->nWords );
+    word * pDivs1 = Vec_WrdEntryP( p->vDivs[1], iObj*p->nWords );
+    word * pIsf; int nFuncs = Supp_SetFuncNum(p, iSet); 
+    int i, f, w, nFuncsNew = 0, Mark = Vec_WrdSize(p->vSFuncs), Res = 0;
+    if ( Vec_WrdSize(p->vSFuncs) + 6*nFuncs*p->nWords > Vec_WrdCap(p->vSFuncs) )
+        Vec_WrdGrow( p->vSFuncs, 2*Vec_WrdCap(p->vSFuncs) );
+    if ( Vec_WrdSize(p->vSFuncs) == Vec_IntEntry(p->vSStarts, iSet) )
+        pIsf = Vec_WrdLimit( p->vSFuncs );
+    else
+        pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) );
+    for ( i = 0; i < nFuncs; i++ )
+    {
+        word * pFunc[2] = { pIsf + (2*i+0)*p->nWords, pIsf + (2*i+1)*p->nWords };
+        for ( f = 0; f < 3; f++ )
+        {
+            int nOnes[2], Start = Vec_WrdSize(p->vSFuncs);
+            word * pLimit[2] = { Vec_WrdLimit(p->vSFuncs), Vec_WrdLimit(p->vSFuncs) + p->nWords };
+            if ( f == 0 )
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[0][w] &  pDivs0[w] );
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[1][w] & ~pDivs1[w] );
+            }
+            else if ( f == 1 )
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[0][w] &  pDivs1[w] );
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[1][w] & ~pDivs0[w] );
+            }
+            else
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[0][w] & ~pDivs0[w] & ~pDivs1[w] );
+                for ( w = 0; w < p->nWords; w++ )
+                    Vec_WrdPush( p->vSFuncs, pFunc[1][w] );
+            }
+            nOnes[0] = Abc_TtCountOnesVec( pLimit[0], p->nWords );
+            nOnes[1] = Abc_TtCountOnesVec( pLimit[1], p->nWords );
+            if ( nOnes[0] && nOnes[1] )
+                Res += nOnes[0] * nOnes[1];
+            else
+                Vec_WrdShrink( p->vSFuncs, Start );
+        }
+    }
+    assert( Res < (1 << 24) );
+    nFuncsNew = (Vec_WrdSize(p->vSFuncs) - Mark)/2/p->nWords;
+    *pnFuncs = nFuncsNew;
+    *pnPairs = Res;
+}
+int Supp_ManSubsetAdd( Supp_Man_t * p, int iSet, int iObj, int fVerbose )
+{
+    int iSetNew, nEntries = Hsh_VecSize( p->pHash );
+    Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet );
+    Vec_IntClear( p->vTemp );
+    Vec_IntAppend( p->vTemp, vSet );
+    Vec_IntPushOrder( p->vTemp, iObj );
+    assert( Vec_IntIsOrdered(p->vTemp, 0) );
+    iSetNew = Hsh_VecManAdd( p->pHash, p->vTemp );
+    if ( iSetNew == nEntries ) // new entry
+    {
+        int nFuncs, nPairs;
+        Vec_IntPush( p->vSStarts, Vec_WrdSize(p->vSFuncs) );
+        Supp_ManRefine( p, iSet, iObj, &nFuncs, &nPairs );
+        Vec_IntPush( p->vSCount, nFuncs );
+        Vec_IntPush( p->vSPairs, nPairs );
+        assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSStarts) );
+        assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSCount) );
+        assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSPairs) );
+        if ( Supp_SetFuncNum(p, iSetNew) == 0 && Supp_SetSize(p, iSetNew) < Vec_WecSize(p->vSolutions) )
+            Vec_WecPush( p->vSolutions, Supp_SetSize(p, iSetNew), iSetNew );
+        if ( fVerbose )
+            Supp_PrintOne( p, iSetNew );
+    }
+    return iSetNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Supp_ComputePair1( Supp_Man_t * p, int iSet )
+{
+    int Random = 0xFFFFFF & Abc_Random(0);
+    int nFuncs = Vec_IntEntry(p->vSCount, iSet);
+    int iFunc = Random % nFuncs; 
+    word * pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) );
+    word * pFunc[2] = { pIsf + (2*iFunc+0)*p->nWords, pIsf + (2*iFunc+1)*p->nWords };
+    int iBit0 = ((Random >> 16) & 1) ? Abc_TtFindFirstBit2(pFunc[0], p->nWords) : Abc_TtFindLastBit2(pFunc[0], p->nWords);
+    int iBit1 = ((Random >> 17) & 1) ? Abc_TtFindFirstBit2(pFunc[1], p->nWords) : Abc_TtFindLastBit2(pFunc[1], p->nWords);
+    if ( 1 )
+    {
+        Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet ); int i, iObj;
+        Vec_IntForEachEntry( vSet, iObj, i )
+        {
+            word * pSet = Vec_WrdEntryP( p->vSims, Vec_IntEntry(p->vCands, iObj)*p->nWords );
+            assert( Abc_TtGetBit(pSet, iBit0) == Abc_TtGetBit(pSet, iBit1) );
+        }
+    }
+    return (iBit0 << 16) | iBit1;
+}
+int Supp_ComputePair( Supp_Man_t * p, int iSet )
+{
+    int Random = 0xFFFFFF & Abc_Random(0);
+    int nFuncs = Vec_IntEntry(p->vSCount, iSet);
+    int iFunc = Random % nFuncs; 
+    word * pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) );
+    word * pFunc[2] = { pIsf + (2*iFunc+0)*p->nWords, pIsf + (2*iFunc+1)*p->nWords };
+    int iBit0 = ((Random >> 16) & 1) ? Abc_TtFindFirstBit2(pFunc[0], p->nWords) : Abc_TtFindLastBit2(pFunc[0], p->nWords);
+    int iBit1 = ((Random >> 17) & 1) ? Abc_TtFindFirstBit2(pFunc[1], p->nWords) : Abc_TtFindLastBit2(pFunc[1], p->nWords);
+    if ( 1 )
+    {
+        Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet ); int i, iObj;
+        Vec_IntForEachEntry( vSet, iObj, i )
+        {
+            word * pSet0 = Vec_WrdEntryP( p->vDivs[0], iObj*p->nWords );
+            word * pSet1 = Vec_WrdEntryP( p->vDivs[1], iObj*p->nWords );
+            int Value00 = Abc_TtGetBit(pSet0, iBit0);
+            int Value01 = Abc_TtGetBit(pSet0, iBit1);
+            int Value10 = Abc_TtGetBit(pSet1, iBit0);
+            int Value11 = Abc_TtGetBit(pSet1, iBit1);
+            assert( !Value00 || !Value11 );
+            assert( !Value01 || !Value10 );
+        }
+    }
+    return (iBit0 << 16) | iBit1;
+}
+Vec_Int_t * Supp_Compute64Pairs( Supp_Man_t * p, Vec_Int_t * vSets )
+{
+    int i;
+    Vec_IntClear( p->vTempPairs );
+    for ( i = 0; i < 64; i++ )
+    {
+        int Rand = 0xFFFFFF & Abc_Random(0);
+        int iSet = Vec_IntEntry( vSets, Rand % Vec_IntSize(vSets) );
+        Vec_IntPush( p->vTempPairs, Supp_ComputePair(p, iSet) );
+    }
+    return p->vTempPairs;
+}
+void Supp_ManFillBlock( Supp_Man_t * p, Vec_Int_t * vPairs, Vec_Wrd_t * vRes )
+{
+    int i, Pair;
+    assert( Vec_IntSize(vPairs) == 64 );
+    Vec_IntForEachEntry( vPairs, Pair, i )
+    {
+        int iBit0 = Pair >> 16, iBit1 = Pair & 0xFFFF; 
+        word * pPat00 = Vec_WrdEntryP(p->vPats[0], iBit0*p->nDivWords);
+        word * pPat01 = Vec_WrdEntryP(p->vPats[0], iBit1*p->nDivWords);
+        word * pPat10 = Vec_WrdEntryP(p->vPats[1], iBit0*p->nDivWords);
+        word * pPat11 = Vec_WrdEntryP(p->vPats[1], iBit1*p->nDivWords);
+        word * pPat   = Vec_WrdEntryP(p->vRowTemp, i*p->nDivWords);
+        Abc_TtAnd( pPat, pPat00, pPat11, p->nDivWords, 0 );
+        Abc_TtOrAnd( pPat, pPat01, pPat10, p->nDivWords );
+    }
+    Extra_BitMatrixTransposeP( p->vRowTemp, p->nDivWords, vRes, 1 );
+}
+void Supp_ManAddPatterns( Supp_Man_t * p, Vec_Int_t * vSets )
+{
+    Vec_Int_t * vPairs = Supp_Compute64Pairs( p, vSets );
+    Vec_Wrd_t * vRow = Vec_WrdStart( 64*p->nDivWords );
+    Supp_ManFillBlock( p, vPairs, vRow );
+    Vec_PtrPush( p->vMatrix, vRow );
+}
+Vec_Int_t * Supp_ManCollectOnes( word * pSim, int nWords )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 ); int i;
+    for ( i = 0; i < 64*nWords; i++ )
+        if ( Abc_TtGetBit(pSim, i) )
+            Vec_IntPush( vRes, i );
+    return vRes;
+}
+Vec_Int_t * Supp_Compute64PairsFunc( Supp_Man_t * p, Vec_Int_t * vBits0, Vec_Int_t * vBits1 )
+{
+    int i;
+    Vec_IntClear( p->vTempPairs );
+    for ( i = 0; i < 64; i++ )
+    {
+        int Random = 0xFFFFFF & Abc_Random(0);
+        int iBit0 = Vec_IntEntry( vBits0, (Random & 0xFFF) % Vec_IntSize(vBits0) );
+        int iBit1 = Vec_IntEntry( vBits1, (Random >>   12) % Vec_IntSize(vBits1) );
+        Vec_IntPush( p->vTempPairs, (iBit0 << 16) | iBit1 );
+    }
+    return p->vTempPairs;
+}
+void Supp_ManAddPatternsFunc( Supp_Man_t * p, int nBatches )
+{
+    int b;
+    Vec_Int_t * vBits0 = Supp_ManCollectOnes( Vec_WrdEntryP(p->vSFuncs, 0*p->nWords), p->nWords );
+    Vec_Int_t * vBits1 = Supp_ManCollectOnes( Vec_WrdEntryP(p->vSFuncs, 1*p->nWords), p->nWords );
+    for ( b = 0; b < nBatches; b++ )
+    {
+        Vec_Int_t * vPairs = Supp_Compute64PairsFunc( p, vBits0, vBits1 );
+        Vec_Wrd_t * vRow = Vec_WrdStart( 64*p->nDivWords );
+        Supp_ManFillBlock( p, vPairs, vRow );
+        Vec_PtrPush( p->vMatrix, vRow );
+    }
+    Vec_IntFree( vBits0 );
+    Vec_IntFree( vBits1 );
+}
+int Supp_FindNextDiv( Supp_Man_t * p, int Pair )
+{
+    int iDiv, iBit0 = Pair >> 16, iBit1 = Pair & 0xFFFF; 
+    word * pPat00 = Vec_WrdEntryP(p->vPats[0], iBit0*p->nDivWords);
+    word * pPat01 = Vec_WrdEntryP(p->vPats[0], iBit1*p->nDivWords);
+    word * pPat10 = Vec_WrdEntryP(p->vPats[1], iBit0*p->nDivWords);
+    word * pPat11 = Vec_WrdEntryP(p->vPats[1], iBit1*p->nDivWords);
+    int iDiv1 = Abc_TtFindFirstAndBit2( pPat00, pPat11, p->nDivWords );
+    int iDiv2 = Abc_TtFindFirstAndBit2( pPat01, pPat10, p->nDivWords );
+    iDiv1 = iDiv1 == -1 ? ABC_INFINITY : iDiv1;
+    iDiv2 = iDiv2 == -1 ? ABC_INFINITY : iDiv2;
+    iDiv = Abc_MinInt( iDiv1, iDiv2 );
+    assert( iDiv >= 0 && iDiv < Vec_IntSize(p->vCands) );
+    return iDiv;
+}
+int Supp_ManRandomSolution( Supp_Man_t * p, int iSet, int fVerbose )
+{
+    Vec_IntClear( p->vTempSets );
+    while ( Supp_SetFuncNum(p, iSet) > 0 )
+    {
+        int Pair = Supp_ComputePair( p, iSet );
+        int iDiv = Supp_FindNextDiv( p, Pair );
+        iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose );
+        if ( Supp_SetFuncNum(p, iSet) > 0 )
+            Vec_IntPush( p->vTempSets, iSet );
+    }
+    if ( Vec_IntSize(p->vTempSets) < 2 )
+        return iSet;
+    Supp_ManAddPatterns( p, p->vTempSets );
+    return iSet;
+}
+int Supp_ManSubsetRemove( Supp_Man_t * p, int iSet, int iPos )
+{
+    int i, iSetNew = 0, nSize = Supp_SetSize(p, iSet);
+    for ( i = 0; i < nSize; i++ )
+        if ( i != iPos && Supp_SetFuncNum(p, iSetNew) > 0 )
+            iSetNew = Supp_ManSubsetAdd( p, iSetNew, Vec_IntEntry(Hsh_VecReadEntry(p->pHash, iSet), i), 0 );
+    return iSetNew;
+}
+int Supp_ManMinimize( Supp_Man_t * p, int iSet0, int r, int fVerbose )
+{
+    int i, nSize = Supp_SetSize(p, iSet0);
+    Vec_Int_t * vPerm = Vec_IntStartNatural( Supp_SetSize(p, iSet0) );
+    Vec_IntRandomizeOrder( vPerm );
+    Vec_IntClear( p->vTempSets );
+    if ( fVerbose )
+    printf( "Removing items from %d:\n", iSet0 );
+    // make sure we first try to remove items with higher weight
+    for ( i = 0; i < nSize; i++ )
+    {
+        int Index = Vec_IntEntry( vPerm, i );
+        int iSet = Supp_ManSubsetRemove( p, iSet0, Index );
+        if ( fVerbose )
+        printf( "Item %2d : ", Index ); 
+        if ( fVerbose )
+        Supp_PrintOne( p, iSet );
+        if ( Supp_SetFuncNum(p, iSet) == 0 )
+        {
+            Vec_IntFree( vPerm );
+            return Supp_ManMinimize( p, iSet, r, fVerbose );
+        }
+        Vec_IntPush( p->vTempSets, iSet );
+    }
+    Supp_ManAddPatterns( p, p->vTempSets );
+    Vec_IntFree( vPerm );
+    return iSet0;
+}
+int Supp_ManFindNextObj( Supp_Man_t * p, int fVerbose )
+{
+    Vec_Wrd_t * vTemp; int r, k, iDiv;
+    word Sim, * pMask = Vec_WrdArray(p->vMask);
+    assert( Vec_WrdSize(p->vMask) == Vec_PtrSize(p->vMatrix) );
+    Vec_IntFill( p->vCosts, Vec_IntSize(p->vCosts), 0 );
+    Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, r )
+        Vec_WrdForEachEntryStop( vTemp, Sim, k, Vec_IntSize(p->vCosts) )
+            Vec_IntAddToEntry( p->vCosts, k, Abc_TtCountOnes(Sim & pMask[r]) );
+    iDiv = Vec_IntArgMax( p->vCosts );
+    if ( fVerbose )
+    printf( "Choosing divisor %d with weight %d.\n", iDiv, Vec_IntEntry(p->vCosts, iDiv) );
+    Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, r )
+        pMask[r] &= ~Vec_WrdEntry( vTemp, iDiv );
+    return iDiv;
+}
+int Supp_ManReconstruct( Supp_Man_t * p, int fVerbose )
+{
+    int iSet = 0;
+    Vec_WrdFill( p->vMask, Vec_PtrSize(p->vMatrix), ~(word)0 );
+    if ( fVerbose )
+    printf( "\nBuilding a new set:\n" );
+    while ( Supp_SetPairNum(p, iSet) )
+    {
+        int iDiv = Supp_ManFindNextObj( p, fVerbose );
+        iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose );
+        if ( Abc_TtIsConst0(Vec_WrdArray(p->vMask), Vec_WrdSize(p->vMask)) )
+            break;
+    }
+    if ( fVerbose )
+    printf( "Adding random part:\n" );
+    return Supp_ManRandomSolution( p, iSet, fVerbose );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVerbose, Vec_Int_t ** pvDivs )
+{
+    Vec_Int_t * vLevel, * vRes = NULL; 
+    int i, k, iSet, nFuncs = 0, Count = 0;
+    int iSolBest = -1, Cost, CostBest = ABC_INFINITY;
+    Vec_WecForEachLevel( vSols, vLevel, i )
+    {
+        Count += Vec_IntSize(vLevel) > 0;
+        Vec_IntForEachEntry( vLevel, iSet, k )
+        {
+            if ( fVerbose )
+                printf( "%3d : ", nFuncs++ );
+            Cost = Gia_ManEvalSolutionOne( p->pGia, p->vSims, p->vIsfs, p->vCands, Hsh_VecReadEntry(p->pHash, iSet), p->nWords, fVerbose );
+            if ( Cost == -1 )
+                continue;
+            if ( CostBest > Cost )
+            {
+                CostBest = Cost;
+                iSolBest = iSet;
+            }
+            if ( nFuncs > 5 )
+                break;
+        }
+        if ( Count == 2 || k < Vec_IntSize(vLevel) )
+            break;
+    }
+    if ( iSolBest > 0 && (CostBest >> 2) < 50 )
+    {
+        Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSolBest ); int i, iObj;
+        vRes = Gia_ManDeriveSolutionOne( p->pGia, p->vSims, p->vIsfs, p->vCands, vSet, p->nWords, CostBest & 3 );
+        assert( !vRes || Vec_IntSize(vRes) == 2*(CostBest >> 2)+1 );
+        if ( vRes && pvDivs )
+        {
+            Vec_IntClear( *pvDivs );
+            Vec_IntPushTwo( *pvDivs, -1, -1 );
+            Vec_IntForEachEntry( vSet, iObj, i )
+                Vec_IntPush( *pvDivs, Vec_IntEntry(p->vCands, iObj) );
+        }
+    }
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Supp_FindGivenOne( Supp_Man_t * p )
+{
+    int i, iObj, iSet = 0;
+    Vec_Int_t * vSet = Vec_IntStart( 2 );
+    //extern void Patch_GenerateSet11( Gia_Man_t * p, Vec_Int_t * vDivs, Vec_Int_t * vCands );
+    //Patch_GenerateSet11( p->pGia, vSet, p->vCands );
+    Vec_IntDrop( vSet, 0 );
+    Vec_IntDrop( vSet, 0 );
+    Vec_IntForEachEntry( vSet, iObj, i )
+        iSet = Supp_ManSubsetAdd( p, iSet, iObj, 1 );
+    Vec_IntFree( vSet );
+    return iSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vWeights, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC, int nWords, Gia_Man_t * pGia, Vec_Int_t ** pvDivs, int nIters, int nRounds, int fVerbose )
+{
+    int fVeryVerbose = 0;
+    int i, r, iSet, iBest = -1;
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vRes = NULL; 
+    Supp_Man_t * p = Supp_ManCreate( vIsfs, vCands, vWeights, vSims, vSimsC, nWords, pGia, nIters, nRounds );
+    if ( Supp_SetFuncNum(p, 0) == 0 )
+    {
+        Supp_ManDelete( p );
+        Vec_IntClear( *pvDivs );
+        Vec_IntPushTwo( *pvDivs, -1, -1 );
+        vRes = Vec_IntAlloc( 1 );
+        Vec_IntPush( vRes, Abc_TtIsConst0(Vec_WrdArray(vIsfs), nWords) );
+        return vRes;
+    }
+    if ( fVerbose )
+    printf( "\nUsing %d divisors with %d words. Problem has %d functions and %d minterm pairs.\n", 
+        Vec_IntSize(p->vCands), p->nWords, Supp_SetFuncNum(p, 0), Supp_SetPairNum(p, 0) );
+    //iBest = Supp_FindGivenOne( p );
+    if ( iBest == -1 )
+    for ( i = 0; i < p->nIters; i++ )
+    {
+        Supp_ManAddPatternsFunc( p, i );
+        iSet = Supp_ManRandomSolution( p, 0, fVeryVerbose );
+        for ( r = 0; r < p->nRounds; r++ )
+        {
+            if ( fVeryVerbose )
+            printf( "\n\nITER %d   ROUND %d\n", i, r );
+            iSet = Supp_ManMinimize( p, iSet, r, fVeryVerbose );
+            if ( iBest == -1 || Supp_SetWeight(p, iBest) > Supp_SetWeight(p, iSet) )
+            //if ( Supp_SetSize(p, iBest) > Supp_SetSize(p, iSet) )
+            {
+                if ( fVeryVerbose )
+                printf( "\nThe best solution found:\n" );
+                if ( fVeryVerbose )
+                Supp_PrintOne( p, iSet );
+                iBest = iSet;
+            }
+            iSet = Supp_ManReconstruct( p, fVeryVerbose );
+        }
+        if ( fVeryVerbose )
+        printf( "Matrix size %d.\n", Vec_PtrSize(p->vMatrix) );
+        Supp_ManCleanMatrix( p );
+    }
+    if ( fVerbose )
+    {
+        printf( "Explored %d divisor sets. Found %d solutions. Memory usage %.2f MB.  ", 
+            Hsh_VecSize(p->pHash), Vec_WecSizeSize(p->vSolutions), 1.0*Supp_ManMemory(p)/(1<<20) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        printf( "The best solution:  " );
+        if ( iBest == -1 )
+            printf( "No solution.\n" );
+        else
+            Supp_PrintOne( p, iBest );
+    }
+    vRes = Supp_ManFindBestSolution( p, p->vSolutions, fVerbose, pvDivs );
+    Supp_ManDelete( p );
+//    if ( vRes && Vec_IntSize(vRes) == 0 )
+//        Vec_IntFreeP( &vRes );
+    return vRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 35ed4ab0..0786ce44 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -16,6 +16,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaCSat2.c \
     src/aig/gia/giaCTas.c \
     src/aig/gia/giaCut.c \
+    src/aig/gia/giaDecs.c \
     src/aig/gia/giaDeep.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
@@ -89,6 +90,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaStr.c \
     src/aig/gia/giaSupMin.c \
     src/aig/gia/giaSupp.c \
+    src/aig/gia/giaSupps.c \
     src/aig/gia/giaSweep.c \
     src/aig/gia/giaSweeper.c \
     src/aig/gia/giaSwitch.c \