Merge remote-tracking branch 'upstream/master' into yosys-experimental

32 files changed, 4115 insertions, 81 deletions

diff --git a/abcexe.dsp b/abcexe.dsp
index 823af19e..9d5152fc 100644
--- a/abcexe.dsp
+++ b/abcexe.dsp
@@ -88,10 +88,6 @@ LINK32=link.exe
 # PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
 # Begin Source File
 
-SOURCE=.\src\aig\gia\giaSif.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\main\main.c
 # End Source File
 # End Group
diff --git a/abclib.dsp b/abclib.dsp
index d536e0e7..d460427c 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -5191,6 +5191,10 @@ SOURCE=.\src\aig\gia\giaSatoko.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaSatSyn.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaScl.c
 # End Source File
 # Begin Source File
@@ -5295,6 +5299,10 @@ SOURCE=.\src\aig\gia\giaTsim.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaTtopt.cpp
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaUnate.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 488f12cf..942c9eb7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -527,18 +527,22 @@ static inline int          Gia_ObjDiff1( Gia_Obj_t * pObj )                    {
 static inline int          Gia_ObjFaninC0( Gia_Obj_t * pObj )                  { return pObj->fCompl0;        }
 static inline int          Gia_ObjFaninC1( Gia_Obj_t * pObj )                  { return pObj->fCompl1;        }
 static inline int          Gia_ObjFaninC2( Gia_Man_t * p, Gia_Obj_t * pObj )   { return p->pMuxes && Abc_LitIsCompl(p->pMuxes[Gia_ObjId(p, pObj)]);  }
+static inline int          Gia_ObjFaninC( Gia_Obj_t * pObj, int n )            { return n ? Gia_ObjFaninC1(pObj) : Gia_ObjFaninC0(pObj);             }
 static inline Gia_Obj_t *  Gia_ObjFanin0( Gia_Obj_t * pObj )                   { return pObj - pObj->iDiff0;  }
 static inline Gia_Obj_t *  Gia_ObjFanin1( Gia_Obj_t * pObj )                   { return pObj - pObj->iDiff1;  }
 static inline Gia_Obj_t *  Gia_ObjFanin2( Gia_Man_t * p, Gia_Obj_t * pObj )    { return p->pMuxes ? Gia_ManObj(p, Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)])) : NULL;  }
+static inline Gia_Obj_t *  Gia_ObjFanin( Gia_Obj_t * pObj, int n )             { return n ? Gia_ObjFanin1(pObj) : Gia_ObjFanin0(pObj);               }
 static inline Gia_Obj_t *  Gia_ObjChild0( Gia_Obj_t * pObj )                   { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); }
 static inline Gia_Obj_t *  Gia_ObjChild1( Gia_Obj_t * pObj )                   { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); }
 static inline Gia_Obj_t *  Gia_ObjChild2( Gia_Man_t * p, Gia_Obj_t * pObj )    { return Gia_NotCond( Gia_ObjFanin2(p, pObj), Gia_ObjFaninC2(p, pObj) ); }
 static inline int          Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId )      { return ObjId - pObj->iDiff0;    }
 static inline int          Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId )      { return ObjId - pObj->iDiff1;    }
 static inline int          Gia_ObjFaninId2( Gia_Man_t * p, int ObjId )         { return (p->pMuxes && p->pMuxes[ObjId]) ? Abc_Lit2Var(p->pMuxes[ObjId]) : -1; }
+static inline int          Gia_ObjFaninId( Gia_Obj_t * pObj, int ObjId, int n ){ return n ? Gia_ObjFaninId1(pObj, ObjId) : Gia_ObjFaninId0(pObj, ObjId);      }
 static inline int          Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) );              }
 static inline int          Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) );              }
 static inline int          Gia_ObjFaninId2p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)]) : -1; }
+static inline int          Gia_ObjFaninIdp( Gia_Man_t * p, Gia_Obj_t * pObj, int n){ return n ? Gia_ObjFaninId1p(p, pObj) : Gia_ObjFaninId0p(p, pObj);     }
 static inline int          Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
 static inline int          Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
 static inline int          Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId )        { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1;           }
@@ -1544,6 +1548,9 @@ extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName, int fGiaSimple
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
 extern Gia_Man_t *         Gia_ManReadMiniLut( char * pFileName );
 extern void                Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName );
+/*=== giaMinLut.c ===========================================================*/
+extern word *              Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare );
+extern Vec_Int_t *         Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts );
 /*=== giaMuxes.c ===========================================================*/
 extern void                Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
 extern void                Gia_ManPrintMuxStats( Gia_Man_t * p );
@@ -1754,6 +1761,10 @@ extern int                 Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
 extern void                Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose );
 
+/*=== giaTtopt.c ===========================================================*/
+extern Gia_Man_t *         Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds );
+extern Gia_Man_t *         Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity );
+
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
@@ -1763,7 +1774,6 @@ extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
 extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
 
-
 ABC_NAMESPACE_HEADER_END
 
 
diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c
index 7ee795b6..19e2d8fc 100644
--- a/src/aig/gia/giaCut.c
+++ b/src/aig/gia/giaCut.c
@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "misc/util/utilTruth.h"
+#include "misc/vec/vecHsh.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -29,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 #define GIA_MAX_CUTSIZE    8
-#define GIA_MAX_CUTNUM     51
+#define GIA_MAX_CUTNUM     65
 #define GIA_MAX_TT_WORDS   ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1)
 
 #define GIA_CUT_NO_LEAF   0xF
@@ -778,6 +779,218 @@ void Gia_ManExtractTest( Gia_Man_t * pGia )
     Abc_PrintTime( 0, "Creating windows", Abc_Clock() - clk );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Extract a given number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_StoCutPrint( int * pCut )
+{
+    int v; 
+    printf( "{" );
+    for ( v = 1; v <= pCut[0]; v++ )
+        printf( " %d", pCut[v] );
+    printf( " }\n" );
+}
+void Gia_StoPrintCuts( Vec_Int_t * vThis, int iObj, int nCutSize )
+{
+    int i, * pCut;
+    printf( "Cuts of node %d (size = %d):\n", iObj, nCutSize );
+    Sdb_ForEachCut( Vec_IntArray(vThis), pCut, i )
+        if ( !nCutSize || pCut[0] == nCutSize )
+            Gia_StoCutPrint( pCut );
+}
+Vec_Wec_t * Gia_ManFilterCuts( Gia_Man_t * pGia, Vec_Wec_t * vStore, int nCutSize, int nCuts )
+{
+    abctime clkStart = Abc_Clock();
+    Vec_Wec_t * vCutsSel = Vec_WecAlloc( nCuts ); 
+    Vec_Int_t * vLevel, * vCut = Vec_IntAlloc( 10 );
+    Vec_Wec_t * vCuts = Vec_WecAlloc( 1000 ); 
+    Hsh_VecMan_t * p = Hsh_VecManStart( 1000 ); int i, s;
+    Vec_WecForEachLevel( vStore, vLevel, i ) if ( Vec_IntSize(vLevel) )
+    {
+        int v, k, * pCut, Value;
+        Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k )
+        {
+            if ( pCut[0] < 2 )
+                continue;
+
+            for ( v = 1; v <= pCut[0]; v++ )
+                if ( pCut[v] < 9 )
+                    break;
+            if ( v <= pCut[0] )
+                continue;
+
+            Vec_IntClear( vCut );
+            Vec_IntPushArray( vCut, pCut+1, pCut[0] );
+            Value = Hsh_VecManAdd( p, vCut );
+            if ( Value == Vec_WecSize(vCuts) )
+            {
+                Vec_Int_t * vTemp = Vec_WecPushLevel(vCuts);
+                Vec_IntPush( vTemp, 0 );
+                Vec_IntAppend( vTemp, vCut );
+            }
+            Vec_IntAddToEntry( Vec_WecEntry(vCuts, Value), 0, 1 );
+        }
+    }
+    printf( "Collected cuts = %d.\n", Vec_WecSize(vCuts) );
+    for ( s = 3; s <= nCutSize; s++ )
+        Vec_WecForEachLevel( vCuts, vLevel, i )
+            if ( Vec_IntSize(vLevel) - 1 == s )
+            {
+                int * pCut = Vec_IntEntryP(vLevel, 1);
+                int u, v, Value;
+                for ( u = 0; u < s; u++ )
+                {
+                    Vec_IntClear( vCut );
+                    for ( v = 0; v < s; v++ ) if ( v != u )
+                        Vec_IntPush( vCut, pCut[v] );
+                    assert( Vec_IntSize(vCut) == s-1 );
+                    Value = Hsh_VecManAdd( p, vCut );
+                    if ( Value < Vec_WecSize(vCuts) )
+                        Vec_IntAddToEntry( vLevel, 0, Vec_IntEntry(Vec_WecEntry(vCuts, Value), 0) );
+                }
+            }
+    Hsh_VecManStop( p );
+    Vec_IntFree( vCut );
+    // collect 
+    Vec_WecSortByFirstInt( vCuts, 1 );
+    Vec_WecForEachLevelStop( vCuts, vLevel, i, Abc_MinInt(Vec_WecSize(vCuts), nCuts) )
+        Vec_IntAppend( Vec_WecPushLevel(vCutsSel), vLevel );
+    Abc_PrintTime( 0, "Cut filtering time", Abc_Clock() - clkStart );
+    return vCutsSel;
+}
+int Gia_ManCountRefs( Gia_Man_t * pGia, Vec_Int_t * vLevel )
+{
+    int i, iObj, nRefs = 0;
+    Vec_IntForEachEntry( vLevel, iObj, i )
+        nRefs += Gia_ObjRefNumId(pGia, iObj);
+    return nRefs;
+}
+Vec_Wrd_t * Gia_ManGenSims( Gia_Man_t * pGia ) 
+{
+    Vec_Wrd_t * vSims;
+    Vec_WrdFreeP( &pGia->vSimsPi );
+    pGia->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pGia) );
+    vSims  = Gia_ManSimPatSim( pGia );
+    return vSims;
+}
+int Gia_ManFindSatDcs( Gia_Man_t * pGia, Vec_Wrd_t * vSims, Vec_Int_t * vLevel ) 
+{
+    int nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
+    int i, w, iObj, Res = 0, Pres[256] = {0}, nMints = 1 << Vec_IntSize(vLevel);
+    for ( w = 0; w < 64*nWords; w++ )
+    {
+        int iInMint = 0;
+        Vec_IntForEachEntry( vLevel, iObj, i )
+            if ( Abc_TtGetBit( Vec_WrdEntryP(vSims, iObj*nWords), w ) )
+                iInMint |= 1 << i;
+        Pres[iInMint]++;
+    }
+    for ( i = 0; i < nMints; i++ )
+        Res += Pres[i] == 0;
+    return Res;
+}
+
+
+int Gia_ManCollectCutDivs( Gia_Man_t * p, Vec_Int_t * vIns )
+{
+    Gia_Obj_t * pObj; int i, Res = 0; 
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 ); 
+    Vec_IntSort( vIns, 0 );
+
+    Vec_IntPush( vRes, 0 );
+    Vec_IntAppend( vRes, vIns );
+
+    Gia_ManIncrementTravId( p );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vIns, p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
+        {
+            if ( !Gia_ObjIsTravIdPrevious(p, pObj) )
+                Vec_IntPush( vRes, i );
+            Gia_ObjSetTravIdCurrent( p, pObj );
+        }
+//    printf( "Divisors: " );
+//    Vec_IntPrint( vRes );
+    Res = Vec_IntSize(vRes);
+    Vec_IntFree( vRes );
+    return Res;
+}
+
+void Gia_ManConsiderCuts( Gia_Man_t * pGia, Vec_Wec_t * vCuts )
+{
+    Vec_Wrd_t * vSims = Gia_ManGenSims( pGia ); 
+    Vec_Int_t * vLevel; int i;
+    Gia_ManCreateRefs( pGia );
+    Vec_WecForEachLevel( vCuts, vLevel, i )
+    {
+        printf( "Cut %3d  ", i );
+        printf( "Ref = %3d : ", Vec_IntEntry(vLevel, 0) );
+
+        Vec_IntShift( vLevel, 1 );
+        printf( "Ref = %3d : ", Gia_ManCountRefs(pGia, vLevel) );
+        printf( "SDC = %3d : ", Gia_ManFindSatDcs(pGia, vSims, vLevel) );
+        printf( "Div = %3d : ", Gia_ManCollectCutDivs(pGia, vLevel) );
+        Vec_IntPrint( vLevel );
+        Vec_IntShift( vLevel, -1 );
+    }
+    Vec_WrdFree( vSims );
+}
+
+
+Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 )
+{
+    int nCutSize  =  nCutSize0;
+    int nCutNum   =  64;
+    int fCutMin   =  0;
+    int fTruthMin =  0;
+    int fVerbose  =  fVerbose0;
+    Vec_Wec_t * vCutsSel;
+    Gia_Sto_t * p = Gia_StoAlloc( pGia, nCutSize, nCutNum, fCutMin, fTruthMin, fVerbose );
+    Gia_Obj_t * pObj;  int i, iObj;
+    assert( nCutSize <= GIA_MAX_CUTSIZE );
+    assert( nCutNum  <  GIA_MAX_CUTNUM  );
+    // prepare references
+    Gia_ManForEachObj( p->pGia, pObj, iObj )
+        Gia_StoRefObj( p, iObj );
+    // compute cuts
+    Gia_StoComputeCutsConst0( p, 0 );
+    Gia_ManForEachCiId( p->pGia, iObj, i )
+        Gia_StoComputeCutsCi( p, iObj );
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+        Gia_StoComputeCutsNode( p, iObj );
+    if ( p->fVerbose )
+    {
+        printf( "Running cut computation with CutSize = %d  CutNum = %d  CutMin = %s  TruthMin = %s\n", 
+            p->nCutSize, p->nCutNum, p->fCutMin ? "yes":"no", p->fTruthMin ? "yes":"no" );
+        printf( "CutPair = %.0f  ",         p->CutCount[0] );
+        printf( "Merge = %.0f (%.2f %%)  ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
+        printf( "Eval = %.0f (%.2f %%)  ",  p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
+        printf( "Cut = %.0f (%.2f %%)  ",   p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
+        printf( "Cut/Node = %.2f  ",        p->CutCount[3] / Gia_ManAndNum(p->pGia) );
+        printf( "\n" );
+        printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d).  ", 
+            p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
+        Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
+    }
+    vCutsSel = Gia_ManFilterCuts( pGia, p->vCuts, nCutSize0, nCuts0 );
+    Gia_ManConsiderCuts( pGia, vCutsSel );
+    Gia_StoFree( p );
+    return vCutsSel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index cc501562..c9af8a32 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -860,6 +860,27 @@ Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCiNum(p) + Gia_ManCoNum(p) );
+    Gia_ManHashStart( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendBuf( pNew, pObj->Value );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
+    Gia_ManHashStop( pNew );
+    return pNew;
+}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 5c82b260..030eaa60 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1869,7 +1869,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
     Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
     if ( ~pObj->Value )
         return;
-    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) && !Gia_ObjFailed(p,Gia_ObjId(p,pObj))  )
     {
         if ( Gia_ObjIsConst0(pRepr) )
         {
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index ae87277a..8b4e5b12 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1891,7 +1891,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
             if ( !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && 
                  !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize && 
                  !pIfMan->pPars->fEnableCheck75 && !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && 
-                 !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars )
+                 !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars && !pIfMan->pPars->fUseCheck1 && !pIfMan->pPars->fUseCheck2 )
                 If_CutRotatePins( pIfMan, pCutBest );
             // collect leaves of the best cut
             Vec_IntClear( vLeaves );
diff --git a/src/aig/gia/giaResub2.c b/src/aig/gia/giaResub2.c
index 1219526f..10c5a9e0 100644
--- a/src/aig/gia/giaResub2.c
+++ b/src/aig/gia/giaResub2.c
@@ -733,7 +733,7 @@ void Gia_RsbCiWindowTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int  Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n )          { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj);  }
+//static inline int  Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n )          { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj);  }
 
 static inline int  Gia_ObjTravIsTopTwo( Gia_Man_t * p, int iNodeA )            { return (p->pTravIds[iNodeA] >= p->nTravIds - 1);       }
 static inline int  Gia_ObjTravIsSame( Gia_Man_t * p, int iNodeA, int iNodeB )  { return (p->pTravIds[iNodeA] == p->pTravIds[iNodeB]);   }
diff --git a/src/aig/gia/giaSatSyn.c b/src/aig/gia/giaSatSyn.c
new file mode 100644
index 00000000..15829f79
--- /dev/null
+++ b/src/aig/gia/giaSatSyn.c
@@ -0,0 +1,60 @@
+/**CFile****************************************************************
+
+  FileName    [giaSyn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [High-effort synthesis.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSyn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/util/utilTruth.h"
+#include "sat/glucose/AbcGlucose.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int nTimeLimit, int fUseXor, int fFancy, int fVerbose )
+{
+    Gia_Man_t * pNew = NULL;
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 002f6bc2..75a6d653 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -22,6 +22,7 @@
 #include "misc/util/utilTruth.h"
 #include "misc/extra/extra.h"
 //#include <immintrin.h>
+#include "aig/miniaig/miniaig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -2717,13 +2718,89 @@ Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Int_t * Gia_ManProcessBuffs( Gia_Man_t * pHie, Vec_Wrd_t * vSimsH, int nWords, Vec_Mem_t * vStore, Vec_Int_t * vLabels )
+{
+    Vec_Int_t * vPoSigs = Vec_IntAlloc( Gia_ManBufNum(pHie) );
+    Vec_Int_t * vMap;
+    Vec_Wec_t * vNodes = Vec_WecStart( Gia_ManBufNum(pHie) );
+    Gia_Obj_t * pObj; int i, Sig, Value;
+    Gia_ManForEachBuf( pHie, pObj, i )
+    {
+        word * pSim = Vec_WrdEntryP(vSimsH, Gia_ObjId(pHie, pObj)*nWords);
+        int fCompl = pSim[0] & 1;
+        if ( fCompl )
+            Abc_TtNot( pSim, nWords );
+        Vec_IntPush( vPoSigs, Vec_MemHashInsert(vStore, pSim) );
+        if ( fCompl )
+            Abc_TtNot( pSim, nWords );
+    }
+    Vec_IntPrint( vPoSigs );
+    vMap = Vec_IntStartFull( Vec_MemEntryNum(vStore) );
+    Vec_IntForEachEntry( vPoSigs, Sig, i )
+    {
+        assert( Vec_IntEntry(vMap, Sig) == -1 );
+        Vec_IntWriteEntry( vMap, Sig, i );
+    }
+    Vec_IntForEachEntry( vLabels, Sig, i )
+    {
+        if ( Sig < 0 )
+            continue;
+        Value = Vec_IntEntry(vMap, Sig);
+        if ( Value == -1 )
+            continue;
+        assert( Value >= 0 && Value < Gia_ManBufNum(pHie) );
+        Vec_WecPush( vNodes, Value, i );
+    }
+    Vec_WecPrint( vNodes, 0 );
+    Vec_WecFree( vNodes );
+    Vec_IntFree( vMap );
+    Vec_IntFree( vPoSigs );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld )
+{
+    Gia_Obj_t * pObj; int i;
+    Gia_ManSetPhase( pNew );
+    Gia_ManSetPhase( pOld );
+    Gia_ManForEachCo( pNew, pObj, i )
+        if ( pObj->fPhase ^ Gia_ManCo(pOld, i)->fPhase )
+        {
+            printf( "Updating out %d.\n", i );
+            Gia_ObjFlipFaninC0( pObj );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fVerbose )
 {
     abctime clk = Abc_Clock();
     Vec_Wrd_t * vSims  = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords );
     Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat );
     Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie );
-    Gia_Obj_t * pObj; int * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
+    Vec_Int_t * vLabels = Vec_IntStartFull( Gia_ManObjNum(pFlat) );
+    Gia_Obj_t * pObj; int fCompl, Value, * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
     Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
     pFlat->vSimsPi = NULL;
     pHie->vSimsPi = NULL;
@@ -2739,7 +2816,13 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
         word * pSim = Vec_WrdEntryP(vSims0, i*nWords);
         nC0s += Abc_TtIsConst0(pSim, nWords);
         nC1s += Abc_TtIsConst1(pSim, nWords);
-        Vec_MemHashInsert( vStore, pSim );
+        fCompl = pSim[0] & 1;
+        if ( fCompl )
+            Abc_TtNot( pSim, nWords );
+        Value = Vec_MemHashInsert( vStore, pSim );
+        if ( fCompl )
+            Abc_TtNot( pSim, nWords );
+        Vec_IntWriteEntry( vLabels, i, Value );
     }
     nUnique = Vec_MemEntryNum( vStore );
     printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n", 
@@ -2765,10 +2848,12 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
         //if ( Gia_ObjIsBuf(pObj) )
         //    printf( "%d(%d) ", i, nBoundary-1 );
     }
+    Gia_ManProcessBuffs( pHie, vSims1, nWords, vStore, vLabels );
     Vec_MemHashFree( vStore );
     Vec_MemFree( vStore );
     Vec_WrdFree( vSims0 );
     Vec_WrdFree( vSims1 );
+    Vec_IntFree( vLabels );
 
     printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary.  ", 
         nMatched,  100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)), 
@@ -2777,6 +2862,405 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Gia_ManRelTfos( Gia_Man_t * p, Vec_Int_t * vObjs )
+{
+    Gia_Obj_t * pObj; 
+    Vec_Wec_t * vNodes = Vec_WecStart( Vec_IntSize(vObjs)+1 );
+    Vec_Int_t * vSigns = Vec_IntStart( Gia_ManObjNum(p) ); 
+    int n, k, i, iObj, * pSigns = Vec_IntArray(vSigns); 
+    assert( Vec_IntSize(vObjs) < 32 );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        pSigns[iObj] |= 1 << i;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( pSigns[i] == 0 )
+            for ( n = 0; n < 2; n++ )
+                pSigns[i] |= pSigns[Gia_ObjFaninId(pObj, i, n)];
+        if ( pSigns[i] == 0 )
+            continue;
+        Vec_WecPush( vNodes, Vec_IntSize(vObjs), i );
+        for ( k = 0; k < Vec_IntSize(vObjs); k++ )
+            if ( (pSigns[i] >> k) & 1 )
+                Vec_WecPush( vNodes, k, i );
+    }
+    Vec_IntFree( vSigns );
+    return vNodes;
+}
+Vec_Wrd_t * Gia_ManRelDerive( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
+{
+    int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
+    int i, m, iVar, iMint = 0, nMints = 1 << Vec_IntSize(vObjs); 
+    Vec_Wrd_t * vCopy  = Vec_WrdDup(vSims);  Vec_Int_t * vLevel;
+    Vec_Wrd_t * vRel   = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
+    Vec_Wec_t * vNodes = Gia_ManRelTfos( p, vObjs );
+    Vec_WecPrint( vNodes, 0 );
+    Gia_ManForEachAnd( p, pObj, i )
+        assert( pObj->fPhase == 0 );
+    Gia_ManForEachObjVec( vObjs, p, pObj, i )
+        pObj->fPhase = 1;
+    vLevel = Vec_WecEntry( vNodes, Vec_IntSize(vObjs) );
+    Gia_ManForEachObjVec( vLevel, p, pObj, i )
+        if ( pObj->fPhase )
+            Abc_TtClear( Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords), nWords );
+        else
+            Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Gia_ManForEachCo( p, pObj, i )
+        {
+            word * pSimO = Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords);
+            word * pSimF = Vec_WrdEntryP(vCopy, Gia_ObjFaninId0p(p, pObj)*nWords);
+            word * pSimR = Vec_WrdEntryP(vRel, (iMint*Gia_ManCoNum(p) + i)*nWords);
+            Abc_TtXor( pSimR, pSimF, pSimO, nWords, Gia_ObjFaninC0(pObj) );
+        }
+        if ( m == nMints-1 )
+            break;
+        iVar = Abc_TtSuppFindFirst( (m+1) ^ ((m+1) >> 1) ^ (m) ^ ((m) >> 1) );
+        vLevel = Vec_WecEntry( vNodes, iVar );
+        assert( Vec_IntEntry(vLevel, 0) == Vec_IntEntry(vObjs, iVar) );
+        Abc_TtNot( Vec_WrdEntryP(vCopy, Vec_IntEntry(vObjs, iVar)*nWords), nWords );
+        Gia_ManForEachObjVec( vLevel, p, pObj, i )
+            if ( !pObj->fPhase )
+                Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
+        iMint ^= 1 << iVar;
+    }
+    Gia_ManForEachObjVec( vObjs, p, pObj, i )
+        pObj->fPhase = 0;
+    Vec_WrdFree( vCopy );
+    Vec_WecFree( vNodes );
+    return vRel;
+}
+Vec_Wrd_t * Gia_ManRelDerive2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
+{
+    int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
+    int i, Id, m, Index, nMints = 1 << Vec_IntSize(vObjs); 
+    Vec_Wrd_t * vPos, * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Gia_Man_t * pNew = Gia_ManDup( p ); 
+        Gia_ManForEachAnd( pNew, pObj, i )
+        {
+            if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId0(pObj, i))) >= 0 )
+                pObj->iDiff0 = i, pObj->fCompl0 ^= (m >> Index) & 1;
+            if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId1(pObj, i))) >= 0 )
+                pObj->iDiff1 = i, pObj->fCompl1 ^= (m >> Index) & 1;
+        }
+        vPos = Gia_ManSimPatSimOut( pNew, p->vSimsPi, 1 );
+        Gia_ManForEachCoId( p, Id, i )
+            Abc_TtXor( Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p) + i)*nWords), Vec_WrdEntryP(vPos, i*nWords), Vec_WrdEntryP(vSims, Id*nWords), nWords, 0 );
+        Vec_WrdFree( vPos );
+        Gia_ManStop( pNew );
+    }
+    return vRel;
+}
+void Gia_ManRelPrint( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
+{
+    int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
+    printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
+    for ( w = 0; w < 64*nWords; w++ )
+    {
+        Gia_ManForEachCiId( p, Id, i )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+        printf( " " );
+        Vec_IntForEachEntry( vObjs, Id, i )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+        printf( " " );
+        Gia_ManForEachCoId( p, Id, i )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+        printf( " " );
+        for ( m = 0; m < nMints; m++ )
+        {
+            printf( " " );
+            for ( i = 0; i < Vec_IntSize(vObjs); i++ )
+                printf( "%d", (m >> i) & 1 );
+            printf( "=" );
+            Gia_ManForEachCoId( p, Id, i )
+                printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w) );
+        }
+        printf( "\n" );
+    }
+}
+void Gia_ManRelPrint2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
+{
+    int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
+    int nWordsM = Abc_Truth6WordNum(Vec_IntSize(vObjs));
+    Vec_Wrd_t * vRes = Vec_WrdStart( 64*nWords * nWordsM );
+    printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
+    for ( w = 0; w < 64*nWords; w++ )
+    {
+        int iMint = 0;
+        int nValid = 0;
+        Gia_ManForEachCiId( p, Id, i )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+        printf( " " );
+        Vec_IntForEachEntry( vObjs, Id, i )
+        {
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+            if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) )
+                iMint |= 1 << i;
+        }
+        printf( " " );
+        Gia_ManForEachCoId( p, Id, i )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
+        printf( " " );
+        for ( m = 0; m < nMints; m++ )
+        {
+            int Count = 0;
+            Gia_ManForEachCoId( p, Id, i )
+                Count += Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w);
+            printf( "%d", Count == 0 );
+            nValid += Count > 0;
+            if ( Count == 0 )
+                Abc_TtSetBit( Vec_WrdEntryP(vRes, w*nWordsM), m );
+        }
+        printf( " " );
+        for ( m = 0; m < nMints; m++ )
+            printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), m) );
+        printf( " " );
+        assert( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint) );
+        for ( i = 0; i < Vec_IntSize(vObjs); i++ )
+            if ( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint ^ (1 << i)) )
+                printf( "-" );
+            else
+                printf( "%d", (iMint >> i) & 1 );
+        printf( " %d", nMints-nValid );
+        printf( "\n" );
+    }
+    Vec_WrdFree( vRes );
+}
+Vec_Int_t * Gia_ManRelInitObjs()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 10 );
+    /*
+    Vec_IntPush( vRes, 33 );
+    Vec_IntPush( vRes, 52 );
+    Vec_IntPush( vRes, 53 );
+    Vec_IntPush( vRes, 65 );
+    Vec_IntPush( vRes, 79 );
+    Vec_IntPush( vRes, 81 );
+    */
+    /*
+    Vec_IntPush( vRes, 60 );
+    Vec_IntPush( vRes, 61 );
+    Vec_IntPush( vRes, 71 );
+    Vec_IntPush( vRes, 72 );
+    */
+    /*
+    Vec_IntPush( vRes, 65 );
+    Vec_IntPush( vRes, 79 );
+    Vec_IntPush( vRes, 81 );
+    */
+    Vec_IntPush( vRes, 52 );
+    Vec_IntPush( vRes, 54 );
+    Vec_IntPrint( vRes );
+    return vRes;
+}
+void Gia_ManRelDeriveTest2( Gia_Man_t * p )
+{
+    Vec_Int_t * vObjs = Gia_ManRelInitObjs();
+    Vec_Wrd_t * vSims, * vRel, * vRel2; int nWords;
+    Vec_WrdFreeP( &p->vSimsPi );
+    p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+    nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    vSims  = Gia_ManSimPatSim( p );
+    vRel   = Gia_ManRelDerive( p, vObjs, vSims );
+    vRel2  = Gia_ManRelDerive2( p, vObjs, vSims );
+    //assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) );
+    Gia_ManRelPrint2( p, vObjs, vSims, vRel );
+    Vec_WrdFree( vRel2 );
+    Vec_WrdFree( vRel );
+    Vec_WrdFree( vSims );
+    Vec_IntFree( vObjs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManRelInitIns()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 10 );
+    Vec_IntPush( vRes, 12 );
+    Vec_IntPush( vRes, 18 );
+    Vec_IntPush( vRes, 21 );
+    Vec_IntPush( vRes, 34 );
+    Vec_IntPush( vRes, 45 );
+    Vec_IntPush( vRes, 59 );
+    return vRes;
+}
+Vec_Int_t * Gia_ManRelInitOuts()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 10 );
+    Vec_IntPush( vRes, 65 );
+    Vec_IntPush( vRes, 66 );
+    return vRes;
+}
+Vec_Int_t * Gia_ManRelInitMffc( Gia_Man_t * p, Vec_Int_t * vOuts )
+{
+    Gia_Obj_t * pObj; int i;
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Vec_IntSort( vOuts, 0 );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vOuts, p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
+            Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachAndReverse( p, pObj, i )
+        if ( Gia_ObjIsTravIdPrevious(p, pObj) )
+            continue;
+        else if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        {
+            if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
+                Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
+            if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin1(pObj)) )
+                Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin1(pObj) );
+        }
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
+            Vec_IntPush( vRes, i );
+    printf( "MFFC: " );
+    Vec_IntPrint( vRes );
+    return vRes;
+}
+Vec_Int_t * Gia_ManRelInitDivs( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vOuts )
+{
+    Gia_Obj_t * pObj; int i; 
+    Vec_Int_t * vMffc = Gia_ManRelInitMffc( p, vOuts );
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 ); 
+    Vec_IntSort( vIns, 0 );
+
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vMffc, p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    Vec_IntFree( vMffc );
+
+    Vec_IntPush( vRes, 0 );
+    Vec_IntAppend( vRes, vIns );
+
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vIns, p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
+        {
+            if ( !Gia_ObjIsTravIdPrevious(p, pObj) )
+                Vec_IntPush( vRes, i );
+            Gia_ObjSetTravIdCurrent( p, pObj );
+        }
+    printf( "Divisors: " );
+    Vec_IntPrint( vRes );
+    return vRes;
+}
+
+Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts )
+{
+    Vec_Int_t * vRes = Vec_IntStartFull( 1 << Vec_IntSize(vIns) );
+    int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    for ( w = 0; w < 64*nWords; w++ )
+    {
+        int i, iObj, iMint = 0, iMint2 = 0;
+        Vec_IntForEachEntry( vIns, iObj, i )
+            if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
+                iMint |= 1 << i;
+        if ( Vec_IntEntry(vRes, iMint) >= 0 )
+            continue;
+        Vec_IntForEachEntry( vOuts, iObj, i )
+            if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
+                iMint2 |= 1 << i;
+        Vec_IntWriteEntry( vRes, iMint, iMint2 );
+    }
+    return vRes;
+}
+
+void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs )
+{
+    extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose );
+
+    int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1);
+    Vec_Wrd_t * vSimsIn  = Vec_WrdStart( nMints );
+    Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
+    int Entry0 = Vec_IntEntry( vRel, 0 );
+
+    word Value, Phase = 0;
+    int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    Vec_IntForEachEntry( vDivs, iObj, i )
+        if ( Vec_WrdEntry(vSims, iObj*nWords) & 1 )
+            Phase |= 1 << i;
+
+    assert( Entry0 >= 0 );
+    printf( "Entry0 = %d\n", Entry0 );
+    Entry0 ^= 1;
+//    for ( m = 0; m < nMints; m++ )
+    Vec_IntForEachEntry( vRel, Entry, m )
+    {
+        if ( Entry == -1 )
+            continue;
+        Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, iMint), Entry0 ^ Entry );
+
+        Value = 0;
+        Vec_IntForEachEntry( vDivs, iObj, i )
+            if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), m) )
+                Abc_TtSetBit( &Value, i );
+        Vec_WrdEntryP(vSimsOut, iMint)[0] = Value ^ Phase;
+
+        iMint++;
+    }
+    assert( iMint == nMints );
+    printf( "Created %d minterms.\n", iMint );
+    Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 );
+    Vec_WrdFree( vSimsIn );
+    Vec_WrdFree( vSimsOut );
+}
+void Gia_ManRelDeriveTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vIns  = Gia_ManRelInitIns();
+    Vec_Int_t * vOuts = Gia_ManRelInitOuts();
+    Vec_Wrd_t * vSims; Vec_Int_t * vRel, * vDivs; int nWords;
+    Vec_WrdFreeP( &p->vSimsPi );
+    p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+    nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+    vSims  = Gia_ManSimPatSim( p );
+    vRel   = Gia_ManRelDeriveSimple( p, vSims, vIns, vOuts );
+    vDivs  = Gia_ManRelInitDivs( p, vIns, vOuts );
+    //printf( "Neg = %d\n", Vec_IntCountEntry(vRel, -1) );
+
+    Gia_ManRelSolve( p, vSims, vIns, vOuts, vRel, vDivs );
+
+    Vec_IntFree( vDivs );
+    Vec_IntPrint( vRel );
+    Vec_IntFree( vRel );
+    Vec_WrdFree( vSims );
+    Vec_IntFree( vIns );
+    Vec_IntFree( vOuts );
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp
new file mode 100644
index 00000000..a765633f
--- /dev/null
+++ b/src/aig/gia/giaTtopt.cpp
@@ -0,0 +1,1213 @@
+/**CFile****************************************************************
+
+  FileName    [giaTtopt.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Truth-table-based logic synthesis.]
+
+  Author      [Yukio Miyasaka]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaTtopt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifdef _WIN32
+#ifndef __MINGW32__
+#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information
+#endif
+#endif
+
+#include <vector>
+#include <algorithm>
+#include <cassert>
+#include <bitset>
+
+#include "gia.h"
+#include "misc/vec/vecHash.h"
+
+ABC_NAMESPACE_IMPL_START
+
+namespace Ttopt {
+
+class TruthTable {
+public:
+  static const int ww; // word width
+  static const int lww; // log word width
+  typedef std::bitset<64> bsw;
+
+  int nInputs;
+  int nSize;
+  int nTotalSize;
+  int nOutputs;
+  std::vector<word> t;
+
+  std::vector<std::vector<int> > vvIndices;
+  std::vector<std::vector<int> > vvRedundantIndices;
+  std::vector<int> vLevels;
+
+  std::vector<std::vector<word> > savedt;
+  std::vector<std::vector<std::vector<int> > > vvIndicesSaved;
+  std::vector<std::vector<std::vector<int> > > vvRedundantIndicesSaved;
+  std::vector<std::vector<int> > vLevelsSaved;
+
+  static const word ones[];
+  static const word swapmask[];
+
+  TruthTable(int nInputs, int nOutputs): nInputs(nInputs), nOutputs(nOutputs) {
+    srand(0xABC);
+    if(nInputs >= lww) {
+      nSize = 1 << (nInputs - lww);
+      nTotalSize = nSize * nOutputs;
+      t.resize(nTotalSize);
+    } else {
+      nSize = 0;
+      nTotalSize = ((1 << nInputs) * nOutputs + ww - 1) / ww;
+      t.resize(nTotalSize);
+    }
+    vLevels.resize(nInputs);
+    for(int i = 0; i < nInputs; i++) {
+      vLevels[i] = i;
+    }
+  }
+
+  virtual void Save(unsigned i) {
+    if(savedt.size() < i + 1) {
+      savedt.resize(i + 1);
+      vLevelsSaved.resize(i + 1);
+    }
+    savedt[i] = t;
+    vLevelsSaved[i] = vLevels;
+  }
+
+  virtual void Load(unsigned i) {
+    assert(i < savedt.size());
+    t = savedt[i];
+    vLevels = vLevelsSaved[i];
+  }
+
+  virtual void SaveIndices(unsigned i) {
+    if(vvIndicesSaved.size() < i + 1) {
+      vvIndicesSaved.resize(i + 1);
+      vvRedundantIndicesSaved.resize(i + 1);
+    }
+    vvIndicesSaved[i] = vvIndices;
+    vvRedundantIndicesSaved[i] = vvRedundantIndices;
+  }
+
+  virtual void LoadIndices(unsigned i) {
+    vvIndices = vvIndicesSaved[i];
+    vvRedundantIndices = vvRedundantIndicesSaved[i];
+  }
+
+  word GetValue(int index_lev, int lev) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    return (t[index] >> pos) & ones[logwidth];
+  }
+
+  int IsEq(int index1, int index2, int lev, bool fCompl = false) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    bool fEq = true;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        fEq &= (t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i]);
+        fCompl &= (t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i]);
+      }
+    } else {
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      fEq &= !value;
+      fCompl &= !(value ^ ones[logwidth]);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  bool Imply(int index1, int index2, int lev) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        if(t[nScopeSize * index1 + i] & ~t[nScopeSize * index2 + i]) {
+          return false;
+        }
+      }
+      return true;
+    }
+    return !(GetValue(index1, lev) & (GetValue(index2, lev) ^ ones[logwidth]));
+  }
+
+  int BDDNodeCountLevel(int lev) {
+    return vvIndices[lev].size() - vvRedundantIndices[lev].size();
+  }
+
+  int BDDNodeCount() {
+    int count = 1; // const node
+    for(int i = 0; i < nInputs; i++) {
+      count += BDDNodeCountLevel(i);
+    }
+    return count;
+  }
+
+  int BDDFind(int index, int lev) {
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      bool fZero = true;
+      bool fOne = true;
+      for(int i = 0; i < nScopeSize && (fZero || fOne); i++) {
+        word value = t[nScopeSize * index + i];
+        fZero &= !value;
+        fOne &= !(~value);
+      }
+      if(fZero || fOne) {
+        return -2 ^ (int)fOne;
+      }
+      for(unsigned j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        bool fEq = true;
+        bool fCompl = true;
+        for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+          fEq &= (t[nScopeSize * index + i] == t[nScopeSize * index2 + i]);
+          fCompl &= (t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i]);
+        }
+        if(fEq || fCompl) {
+          return (j << 1) ^ (int)fCompl;
+        }
+      }
+    } else {
+      word value = GetValue(index, lev);
+      if(!value) {
+        return -2;
+      }
+      if(!(value ^ ones[logwidth])) {
+        return -1;
+      }
+      for(unsigned j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        word value2 = value ^ GetValue(index2, lev);
+        if(!(value2)) {
+          return j << 1;
+        }
+        if(!(value2 ^ ones[logwidth])) {
+          return (j << 1) ^ 1;
+        }
+      }
+    }
+    return -3;
+  }
+
+  virtual int BDDBuildOne(int index, int lev) {
+    int r = BDDFind(index, lev);
+    if(r >= -2) {
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return (vvIndices[lev].size() - 1) << 1;
+  }
+
+  virtual void BDDBuildStartup() {
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvRedundantIndices.clear();
+    vvRedundantIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      BDDBuildOne(i, 0);
+    }
+  }
+
+  virtual void BDDBuildLevel(int lev) {
+    for(unsigned i = 0; i < vvIndices[lev-1].size(); i++) {
+      int index = vvIndices[lev-1][i];
+      int cof0 = BDDBuildOne(index << 1, lev);
+      int cof1 = BDDBuildOne((index << 1) ^ 1, lev);
+      if(cof0 == cof1) {
+        vvRedundantIndices[lev-1].push_back(index);
+      }
+    }
+  }
+
+  virtual int BDDBuild() {
+    BDDBuildStartup();
+    for(int i = 1; i < nInputs; i++) {
+      BDDBuildLevel(i);
+    }
+    return BDDNodeCount();
+  }
+
+  virtual int BDDRebuild(int lev) {
+    vvIndices[lev].clear();
+    vvIndices[lev+1].clear();
+    for(int i = lev; i < lev + 2; i++) {
+      if(!i) {
+        for(int j = 0; j < nOutputs; j++) {
+          BDDBuildOne(j, 0);
+        }
+      } else {
+        vvRedundantIndices[i-1].clear();
+        BDDBuildLevel(i);
+      }
+    }
+    if(lev < nInputs - 2) {
+      vvRedundantIndices[lev+1].clear();
+      for(unsigned i = 0; i < vvIndices[lev+1].size(); i++) {
+        int index = vvIndices[lev+1][i];
+        if(IsEq(index << 1, (index << 1) ^ 1, lev + 2)) {
+          vvRedundantIndices[lev+1].push_back(index);
+        }
+      }
+    }
+    return BDDNodeCount();
+  }
+
+  virtual void Swap(int lev) {
+    assert(lev < nInputs - 1);
+    std::vector<int>::iterator it0 = std::find(vLevels.begin(), vLevels.end(), lev);
+    std::vector<int>::iterator it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1);
+    std::swap(*it0, *it1);
+    if(nInputs - lev - 1 > lww) {
+      int nScopeSize = 1 << (nInputs - lev - 2 - lww);
+      for(int i = nScopeSize; i < nTotalSize; i += (nScopeSize << 2)) {
+        for(int j = 0; j < nScopeSize; j++) {
+          std::swap(t[i + j], t[i + nScopeSize + j]);
+        }
+      }
+    } else if(nInputs - lev - 1 == lww) {
+      for(int i = 0; i < nTotalSize; i += 2) {
+        t[i+1] ^= t[i] >> (ww / 2);
+        t[i] ^= t[i+1] << (ww / 2);
+        t[i+1] ^= t[i] >> (ww / 2);
+      }
+    } else {
+      for(int i = 0; i < nTotalSize; i++) {
+        int d = nInputs - lev - 2;
+        int shamt = 1 << d;
+        t[i] ^= (t[i] >> shamt) & swapmask[d];
+        t[i] ^= (t[i] & swapmask[d]) << shamt;
+        t[i] ^= (t[i] >> shamt) & swapmask[d];
+      }
+    }
+  }
+
+  void SwapIndex(int &index, int d) {
+    if((index >> d) % 4 == 1) {
+      index += 1 << d;
+    } else if((index >> d) % 4 == 2) {
+      index -= 1 << d;
+    }
+  }
+
+  virtual int BDDSwap(int lev) {
+    Swap(lev);
+    for(int i = lev + 2; i < nInputs; i++) {
+      for(unsigned j = 0; j < vvIndices[i].size(); j++) {
+        SwapIndex(vvIndices[i][j], i - (lev + 2));
+      }
+    }
+    // swapping vvRedundantIndices is unnecessary for node counting
+    return BDDRebuild(lev);
+  }
+
+  int SiftReo() {
+    int best = BDDBuild();
+    Save(0);
+    SaveIndices(0);
+    std::vector<int> vars(nInputs);
+    int i;
+    for(i = 0; i < nInputs; i++) {
+      vars[i] = i;
+    }
+    std::vector<unsigned> vCounts(nInputs);
+    for(i = 0; i < nInputs; i++) {
+      vCounts[i] = BDDNodeCountLevel(vLevels[i]);
+    }
+    for(i = 1; i < nInputs; i++) {
+      int j = i;
+      while(j > 0 && vCounts[vars[j-1]] < vCounts[vars[j]]) {
+        std::swap(vars[j], vars[j-1]);
+        j--;
+      }
+    }
+    bool turn = true;
+    unsigned j;
+    for(j = 0; j < vars.size(); j++) {
+      int var = vars[j];
+      bool updated = false;
+      int lev = vLevels[var];
+      for(int i = lev; i < nInputs - 1; i++) {
+        int count = BDDSwap(i);
+        if(best > count) {
+          best = count;
+          updated = true;
+          Save(turn);
+          SaveIndices(turn);
+        }
+      }
+      if(lev) {
+        Load(!turn);
+        LoadIndices(!turn);
+        for(int i = lev - 1; i >= 0; i--) {
+          int count = BDDSwap(i);
+          if(best > count) {
+            best = count;
+            updated = true;
+            Save(turn);
+            SaveIndices(turn);
+          }
+        }
+      }
+      turn ^= updated;
+      Load(!turn);
+      LoadIndices(!turn);
+    }
+    return best;
+  }
+
+  void Reo(std::vector<int> vLevelsNew) {
+    for(int i = 0; i < nInputs; i++) {
+      int var = std::find(vLevelsNew.begin(), vLevelsNew.end(), i) - vLevelsNew.begin();
+      int lev = vLevels[var];
+      if(lev < i) {
+        for(int j = lev; j < i; j++) {
+          Swap(j);
+        }
+      } else if(lev > i) {
+        for(int j = lev - 1; j >= i; j--) {
+          Swap(j);
+        }
+      }
+    }
+    assert(vLevels == vLevelsNew);
+  }
+
+  int RandomSiftReo(int nRound) {
+    int best = SiftReo();
+    Save(2);
+    for(int i = 0; i < nRound; i++) {
+      std::vector<int> vLevelsNew(nInputs);
+      int j;
+      for(j = 0; j < nInputs; j++) {
+        vLevelsNew[j] = j;
+      }
+      for(j = nInputs - 1; j > 0; j--) {
+        int d = rand() % j;
+        std::swap(vLevelsNew[j], vLevelsNew[d]);
+      }
+      Reo(vLevelsNew);
+      int r = SiftReo();
+      if(best > r) {
+        best = r;
+        Save(2);
+      }
+    }
+    Load(2);
+    return best;
+  }
+
+  int BDDGenerateAigRec(Gia_Man_t *pNew, std::vector<int> const &vInputs, std::vector<std::vector<int> > &vvNodes, int index, int lev) {
+    int r = BDDFind(index, lev);
+    if(r >= 0) {
+      return vvNodes[lev][r >> 1] ^ (r & 1);
+    }
+    if(r >= -2) {
+      return r + 2;
+    }
+    int cof0 = BDDGenerateAigRec(pNew, vInputs, vvNodes, index << 1, lev + 1);
+    int cof1 = BDDGenerateAigRec(pNew, vInputs, vvNodes, (index << 1) ^ 1, lev + 1);
+    if(cof0 == cof1) {
+      return cof0;
+    }
+    int node;
+    if(Imply(index << 1, (index << 1) ^ 1, lev + 1)) {
+      node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev], cof1), cof0);
+    } else if(Imply((index << 1) ^ 1, index << 1, lev + 1)) {
+      node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev] ^ 1, cof0), cof1);
+    } else {
+      node = Gia_ManHashMux(pNew, vInputs[lev], cof1, cof0);
+    }
+    vvIndices[lev].push_back(index);
+    vvNodes[lev].push_back(node);
+    return node;
+  }
+
+  virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) {
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    std::vector<std::vector<int> > vvNodes(nInputs);
+    std::vector<int> vInputs(nInputs);
+    int i;
+    for(i = 0; i < nInputs; i++) {
+      vInputs[vLevels[i]] = Vec_IntEntry(vSupp, nInputs - i - 1) << 1;
+    }
+    for(i = 0; i < nOutputs; i++) {
+      int node = BDDGenerateAigRec(pNew, vInputs, vvNodes, i, 0);
+      Gia_ManAppendCo(pNew, node);
+    }
+  }
+};
+
+const int TruthTable::ww = 64;
+const int TruthTable::lww = 6;
+
+const word TruthTable::ones[7] = {ABC_CONST(0x0000000000000001),
+                                  ABC_CONST(0x0000000000000003),
+                                  ABC_CONST(0x000000000000000f),
+                                  ABC_CONST(0x00000000000000ff),
+                                  ABC_CONST(0x000000000000ffff),
+                                  ABC_CONST(0x00000000ffffffff),
+                                  ABC_CONST(0xffffffffffffffff)};
+  
+const word TruthTable::swapmask[5] = {ABC_CONST(0x2222222222222222),
+                                      ABC_CONST(0x0c0c0c0c0c0c0c0c),
+                                      ABC_CONST(0x00f000f000f000f0),
+                                      ABC_CONST(0x0000ff000000ff00),
+                                      ABC_CONST(0x00000000ffff0000)};
+  
+class TruthTableReo : public TruthTable {
+public:
+  bool fBuilt;
+  std::vector<std::vector<int> > vvChildren;
+  std::vector<std::vector<std::vector<int> > > vvChildrenSaved;
+
+  TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {
+    fBuilt = false;
+  }
+
+  void Save(unsigned i) {
+    if(vLevelsSaved.size() < i + 1) {
+      vLevelsSaved.resize(i + 1);
+    }
+    vLevelsSaved[i] = vLevels;
+  }
+
+  void Load(unsigned i) {
+    assert(i < vLevelsSaved.size());
+    vLevels = vLevelsSaved[i];
+  }
+
+  void SaveIndices(unsigned i) {
+    TruthTable::SaveIndices(i);
+    if(vvChildrenSaved.size() < i + 1) {
+      vvChildrenSaved.resize(i + 1);
+    }
+    vvChildrenSaved[i] = vvChildren;
+  }
+
+  void LoadIndices(unsigned i) {
+    TruthTable::LoadIndices(i);
+    vvChildren = vvChildrenSaved[i];
+  }
+
+  void BDDBuildStartup() {
+    vvChildren.clear();
+    vvChildren.resize(nInputs);
+    TruthTable::BDDBuildStartup();
+  }
+
+  void BDDBuildLevel(int lev) {
+    for(unsigned i = 0; i < vvIndices[lev-1].size(); i++) {
+      int index = vvIndices[lev-1][i];
+      int cof0 = BDDBuildOne(index << 1, lev);
+      int cof1 = BDDBuildOne((index << 1) ^ 1, lev);
+      vvChildren[lev-1].push_back(cof0);
+      vvChildren[lev-1].push_back(cof1);
+      if(cof0 == cof1) {
+        vvRedundantIndices[lev-1].push_back(index);
+      }
+    }
+  }
+
+  int BDDBuild() {
+    if(fBuilt) {
+      return BDDNodeCount();
+    }
+    fBuilt = true;
+    BDDBuildStartup();
+    for(int i = 1; i < nInputs + 1; i++) {
+      BDDBuildLevel(i);
+    }
+    return BDDNodeCount();
+  }
+
+  int BDDRebuildOne(int index, int cof0, int cof1, int lev, Hash_IntMan_t *unique, std::vector<int> &vChildrenLow) {
+    if(cof0 < 0 && cof0 == cof1) {
+      return cof0;
+    }
+    bool fCompl = cof0 & 1;
+    if(fCompl) {
+      cof0 ^= 1;
+      cof1 ^= 1;
+    }
+    int *place = Hash_Int2ManLookup(unique, cof0, cof1);
+    if(*place) {
+      return (Hash_IntObjData2(unique, *place) << 1) ^ (int)fCompl;
+    }
+    vvIndices[lev].push_back(index);
+    Hash_Int2ManInsert(unique, cof0, cof1, vvIndices[lev].size() - 1);
+    vChildrenLow.push_back(cof0);
+    vChildrenLow.push_back(cof1);
+    if(cof0 == cof1) {
+      vvRedundantIndices[lev].push_back(index);
+    }
+    return ((vvIndices[lev].size() - 1) << 1) ^ (int)fCompl;
+  }
+
+  int BDDRebuild(int lev) {
+    vvRedundantIndices[lev].clear();
+    vvRedundantIndices[lev+1].clear();
+    std::vector<int> vChildrenHigh;
+    std::vector<int> vChildrenLow;
+    Hash_IntMan_t *unique = Hash_IntManStart(2 * vvIndices[lev+1].size());
+    vvIndices[lev+1].clear();
+    for(unsigned i = 0; i < vvIndices[lev].size(); i++) {
+      int index = vvIndices[lev][i];
+      int cof0index = vvChildren[lev][i+i] >> 1;
+      int cof1index = vvChildren[lev][i+i+1] >> 1;
+      bool cof0c = vvChildren[lev][i+i] & 1;
+      bool cof1c = vvChildren[lev][i+i+1] & 1;
+      int cof00, cof01, cof10, cof11;
+      if(cof0index < 0) {
+        cof00 = -2 ^ (int)cof0c;
+        cof01 = -2 ^ (int)cof0c;
+      } else {
+        cof00 = vvChildren[lev+1][cof0index+cof0index] ^ (int)cof0c;
+        cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ (int)cof0c;
+      }
+      if(cof1index < 0) {
+        cof10 = -2 ^ (int)cof1c;
+        cof11 = -2 ^ (int)cof1c;
+      } else {
+        cof10 = vvChildren[lev+1][cof1index+cof1index] ^ (int)cof1c;
+        cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ (int)cof1c;
+      }
+      int newcof0 = BDDRebuildOne(index << 1, cof00, cof10, lev + 1, unique, vChildrenLow);
+      int newcof1 = BDDRebuildOne((index << 1) ^ 1, cof01, cof11, lev + 1, unique, vChildrenLow);
+      vChildrenHigh.push_back(newcof0);
+      vChildrenHigh.push_back(newcof1);
+      if(newcof0 == newcof1) {
+        vvRedundantIndices[lev].push_back(index);
+      }
+    }
+    Hash_IntManStop(unique);
+    vvChildren[lev] = vChildrenHigh;
+    vvChildren[lev+1] = vChildrenLow;
+    return BDDNodeCount();
+  }
+
+  void Swap(int lev) {
+    assert(lev < nInputs - 1);
+    std::vector<int>::iterator it0 = std::find(vLevels.begin(), vLevels.end(), lev);
+    std::vector<int>::iterator it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1);
+    std::swap(*it0, *it1);
+    BDDRebuild(lev);
+  }
+
+  int BDDSwap(int lev) {
+    Swap(lev);
+    return BDDNodeCount();
+  }
+
+  virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) {
+    abort();
+  }
+};
+
+class TruthTableRewrite : public TruthTable {
+public:
+  TruthTableRewrite(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {}
+
+  void SetValue(int index_lev, int lev, word value) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    t[index] &= ~(ones[logwidth] << pos);
+    t[index] ^= value << pos;
+  }
+
+  void CopyFunc(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      if(!fCompl) {
+        if(index2 < 0) {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = 0;
+          }
+        } else {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = t[nScopeSize * index2 + i];
+          }
+        }
+      } else {
+        if(index2 < 0) {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = ones[lww];
+          }
+        } else {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = ~t[nScopeSize * index2 + i];
+          }
+        }
+      }
+    } else {
+      word value = 0;
+      if(index2 >= 0) {
+        value = GetValue(index2, lev);
+      }
+      if(fCompl) {
+        value ^= ones[logwidth];
+      }
+      SetValue(index1, lev, value);
+    }
+  }
+
+  void ShiftToMajority(int index, int lev) {
+    assert(index >= 0);
+    int logwidth = nInputs - lev;
+    int count = 0;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        count += bsw(t[nScopeSize * index + i]).count();
+      }
+    } else {
+      count = bsw(GetValue(index, lev)).count();
+    }
+    bool majority = count > (1 << (logwidth - 1));
+    CopyFunc(index, -1, lev, majority);
+  }
+};
+
+class TruthTableCare : public TruthTableRewrite {
+public:
+  std::vector<word> originalt;
+  std::vector<word> caret;
+  std::vector<word> care;
+
+  std::vector<std::vector<std::pair<int, int> > > vvMergedIndices;
+
+  std::vector<std::vector<word> > savedcare;
+  std::vector<std::vector<std::vector<std::pair<int, int> > > > vvMergedIndicesSaved;
+
+  TruthTableCare(int nInputs, int nOutputs): TruthTableRewrite(nInputs, nOutputs) {
+    if(nSize) {
+      care.resize(nSize);
+    } else {
+      care.resize(1);
+    }
+  }
+
+  void Save(unsigned i) {
+    TruthTable::Save(i);
+    if(savedcare.size() < i + 1) {
+      savedcare.resize(i + 1);
+    }
+    savedcare[i] = care;
+  }
+
+  void Load(unsigned i) {
+    TruthTable::Load(i);
+    care = savedcare[i];
+  }
+
+  void SaveIndices(unsigned i) {
+    TruthTable::SaveIndices(i);
+    if(vvMergedIndicesSaved.size() < i + 1) {
+      vvMergedIndicesSaved.resize(i + 1);
+    }
+    vvMergedIndicesSaved[i] = vvMergedIndices;
+  }
+
+  void LoadIndices(unsigned i) {
+    TruthTable::LoadIndices(i);
+    vvMergedIndices = vvMergedIndicesSaved[i];
+  }
+
+  void Swap(int lev) {
+    TruthTable::Swap(lev);
+    if(nInputs - lev - 1 > lww) {
+      int nScopeSize = 1 << (nInputs - lev - 2 - lww);
+      for(int i = nScopeSize; i < nSize; i += (nScopeSize << 2)) {
+        for(int j = 0; j < nScopeSize; j++) {
+          std::swap(care[i + j], care[i + nScopeSize + j]);
+        }
+      }
+    } else if(nInputs - lev - 1 == lww) {
+      for(int i = 0; i < nSize; i += 2) {
+        care[i+1] ^= care[i] >> (ww / 2);
+        care[i] ^= care[i+1] << (ww / 2);
+        care[i+1] ^= care[i] >> (ww / 2);
+      }
+    } else {
+      for(int i = 0; i < nSize || (i == 0 && !nSize); i++) {
+        int d = nInputs - lev - 2;
+        int shamt = 1 << d;
+        care[i] ^= (care[i] >> shamt) & swapmask[d];
+        care[i] ^= (care[i] & swapmask[d]) << shamt;
+        care[i] ^= (care[i] >> shamt) & swapmask[d];
+      }
+    }
+  }
+
+  void RestoreCare() {
+    caret.clear();
+    if(nSize) {
+      for(int i = 0; i < nOutputs; i++) {
+        caret.insert(caret.end(), care.begin(), care.end());
+      }
+    } else {
+      caret.resize(nTotalSize);
+      for(int i = 0; i < nOutputs; i++) {
+        int padding = i * (1 << nInputs);
+        caret[padding / ww] |= care[0] << (padding % ww);
+      }
+    }
+  }
+
+  word GetCare(int index_lev, int lev) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    return (caret[index] >> pos) & ones[logwidth];
+  }
+
+  void CopyFuncMasked(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        word value = t[nScopeSize * index2 + i];
+        if(fCompl) {
+          value = ~value;
+        }
+        word cvalue = caret[nScopeSize * index2 + i];
+        t[nScopeSize * index1 + i] &= ~cvalue;
+        t[nScopeSize * index1 + i] |= cvalue & value;
+      }
+    } else {
+      word one = ones[logwidth];
+      word value1 = GetValue(index1, lev);
+      word value2 = GetValue(index2, lev);
+      if(fCompl) {
+        value2 ^= one;
+      }
+      word cvalue = GetCare(index2, lev);
+      value1 &= cvalue ^ one;
+      value1 |= cvalue & value2;
+      SetValue(index1, lev, value1);
+    }
+  }
+
+  bool IsDC(int index, int lev) {
+    if(nInputs - lev > lww) {
+      int nScopeSize = 1 << (nInputs - lev - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        if(caret[nScopeSize * index + i]) {
+          return false;
+        }
+      }
+    } else if(GetCare(index, lev)) {
+      return false;
+    }
+    return true;
+  }
+
+  int Include(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    bool fEq = true;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        word cvalue = caret[nScopeSize * index2 + i];
+        if(~caret[nScopeSize * index1 + i] & cvalue) {
+          return 0;
+        }
+        word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i];
+        fEq &= !(value & cvalue);
+        fCompl &= !(~value & cvalue);
+      }
+    } else {
+      word cvalue = GetCare(index2, lev);
+      if((GetCare(index1, lev) ^ ones[logwidth]) & cvalue) {
+        return 0;
+      }
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      fEq &= !(value & cvalue);
+      fCompl &= !((value ^ ones[logwidth]) & cvalue);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  int Intersect(int index1, int index2, int lev, bool fCompl, bool fEq = true) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i];
+        word cvalue = caret[nScopeSize * index1 + i] & caret[nScopeSize * index2 + i];
+        fEq &= !(value & cvalue);
+        fCompl &= !(~value & cvalue);
+      }
+    } else {
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      word cvalue = GetCare(index1, lev) & GetCare(index2, lev);
+      fEq &= !(value & cvalue);
+      fCompl &= !((value ^ ones[logwidth]) & cvalue);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  void MergeCare(int index1, int index2, int lev) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        caret[nScopeSize * index1 + i] |= caret[nScopeSize * index2 + i];
+      }
+    } else {
+      word value = GetCare(index2, lev);
+      int index = index1 >> (lww - logwidth);
+      int pos = (index1 % (1 << (lww - logwidth))) << logwidth;
+      caret[index] |= value << pos;
+    }
+  }
+
+  void Merge(int index1, int index2, int lev, bool fCompl) {
+    MergeCare(index1, index2, lev);
+    vvMergedIndices[lev].push_back(std::make_pair((index1 << 1) ^ (int)fCompl, index2));
+  }
+
+  int BDDBuildOne(int index, int lev) {
+    int r = BDDFind(index, lev);
+    if(r >= -2) {
+      if(r >= 0) {
+        Merge(vvIndices[lev][r >> 1], index, lev, r & 1);
+      }
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return (vvIndices[lev].size() - 1) << 1;
+  }
+
+  void CompleteMerge() {
+    for(int i = nInputs - 1; i >= 0; i--) {
+      for(std::vector<std::pair<int, int> >::reverse_iterator it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) {
+        CopyFunc((*it).second, (*it).first >> 1, i, (*it).first & 1);
+      }
+    }
+  }
+
+  void BDDBuildStartup() {
+    RestoreCare();
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvRedundantIndices.clear();
+    vvRedundantIndices.resize(nInputs);
+    vvMergedIndices.clear();
+    vvMergedIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      if(!IsDC(i, 0)) {
+        BDDBuildOne(i, 0);
+      }
+    }
+  }
+
+  virtual void BDDRebuildByMerge(int lev) {
+    for(unsigned i = 0; i < vvMergedIndices[lev].size(); i++) {
+      std::pair<int, int> &p = vvMergedIndices[lev][i];
+      MergeCare(p.first >> 1, p.second, lev);
+    }
+  }
+
+  int BDDRebuild(int lev) {
+    RestoreCare();
+    int i;
+    for(i = lev; i < nInputs; i++) {
+      vvIndices[i].clear();
+      vvMergedIndices[i].clear();
+      if(i) {
+        vvRedundantIndices[i-1].clear();
+      }
+    }
+    for(i = 0; i < lev; i++) {
+      BDDRebuildByMerge(i);
+    }
+    for(i = lev; i < nInputs; i++) {
+      if(!i) {
+        for(int j = 0; j < nOutputs; j++) {
+          if(!IsDC(j, 0)) {
+            BDDBuildOne(j, 0);
+          }
+        }
+      } else {
+        BDDBuildLevel(i);
+      }
+    }
+    return BDDNodeCount();
+  }
+
+  int BDDSwap(int lev) {
+    Swap(lev);
+    return BDDRebuild(lev);
+  }
+
+  void OptimizationStartup() {
+    originalt = t;
+    RestoreCare();
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvMergedIndices.clear();
+    vvMergedIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      if(!IsDC(i, 0)) {
+        BDDBuildOne(i, 0);
+      } else {
+        ShiftToMajority(i, 0);
+      }
+    }
+  }
+
+  virtual void Optimize() {
+    OptimizationStartup();
+    for(int i = 1; i < nInputs; i++) {
+      for(unsigned j = 0; j < vvIndices[i-1].size(); j++) {
+        int index = vvIndices[i-1][j];
+        BDDBuildOne(index << 1, i);
+        BDDBuildOne((index << 1) ^ 1, i);
+      }
+    }
+    CompleteMerge();
+  }
+};
+
+class TruthTableLevelTSM : public TruthTableCare {
+public:
+  TruthTableLevelTSM(int nInputs, int nOutputs): TruthTableCare(nInputs, nOutputs) {}
+
+  int BDDFindTSM(int index, int lev) {
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      bool fZero = true;
+      bool fOne = true;
+      for(int i = 0; i < nScopeSize && (fZero || fOne); i++) {
+        word value = t[nScopeSize * index + i];
+        word cvalue = caret[nScopeSize * index + i];
+        fZero &= !(value & cvalue);
+        fOne &= !(~value & cvalue);
+      }
+      if(fZero || fOne) {
+        return -2 ^ (int)fOne;
+      }
+      for(unsigned j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        bool fEq = true;
+        bool fCompl = true;
+        for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+          word value = t[nScopeSize * index + i] ^ t[nScopeSize * index2 + i];
+          word cvalue = caret[nScopeSize * index + i] & caret[nScopeSize * index2 + i];
+          fEq &= !(value & cvalue);
+          fCompl &= !(~value & cvalue);
+        }
+        if(fEq || fCompl) {
+          return (index2 << 1) ^ (int)!fEq;
+        }
+      }
+    } else {
+      word one = ones[logwidth];
+      word value = GetValue(index, lev);
+      word cvalue = GetCare(index, lev);
+      if(!(value & cvalue)) {
+        return -2;
+      }
+      if(!((value ^ one) & cvalue)) {
+        return -1;
+      }
+      for(unsigned j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        word value2 = value ^ GetValue(index2, lev);
+        word cvalue2 = cvalue & GetCare(index2, lev);
+        if(!(value2 & cvalue2)) {
+          return index2 << 1;
+        }
+        if(!((value2 ^ one) & cvalue2)) {
+          return (index2 << 1) ^ 1;
+        }
+      }
+    }
+    return -3;
+  }
+
+  int BDDBuildOne(int index, int lev) {
+    int r = BDDFindTSM(index, lev);
+    if(r >= -2) {
+      if(r >= 0) {
+        CopyFuncMasked(r >> 1, index, lev, r & 1);
+        Merge(r >> 1, index, lev, r & 1);
+      } else {
+        vvMergedIndices[lev].push_back(std::make_pair(r, index));
+      }
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return index << 1;
+  }
+
+  int BDDBuild() {
+    TruthTable::Save(3);
+    int r = TruthTable::BDDBuild();
+    TruthTable::Load(3);
+    return r;
+  }
+
+  void BDDRebuildByMerge(int lev) {
+    for(unsigned i = 0; i < vvMergedIndices[lev].size(); i++) {
+      std::pair<int, int> &p = vvMergedIndices[lev][i];
+      if(p.first >= 0) {
+        CopyFuncMasked(p.first >> 1, p.second, lev, p.first & 1);
+        MergeCare(p.first >> 1, p.second, lev);
+      }
+    }
+  }
+
+  int BDDRebuild(int lev) {
+    TruthTable::Save(3);
+    int r = TruthTableCare::BDDRebuild(lev);
+    TruthTable::Load(3);
+    return r;
+  }
+};
+
+}
+
+Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vSupp;
+    word v;
+    word * pTruth;
+    int i, g, k, nInputs;
+    Gia_ManLevelNum( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManForEachCi( p, pObj, k )
+        Gia_ManAppendCi( pNew );
+    Gia_ObjComputeTruthTableStart( p, nIns );
+    Gia_ManHashStart( pNew );
+    for ( g = 0; g < Gia_ManCoNum(p); g += nOuts )
+    {
+        vSupp = Gia_ManCollectSuppNew( p, g, nOuts );
+        nInputs = Vec_IntSize( vSupp );
+        Ttopt::TruthTableReo tt( nInputs, nOuts );
+        for ( k = 0; k < nOuts; k++ )
+        {
+            pObj = Gia_ManCo( p, g+k );
+            pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp );
+            if ( nInputs >= 6 )
+                for ( i = 0; i < tt.nSize; i++ )
+                    tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i];
+            else
+            {
+                i = k * (1 << nInputs);
+                v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs];
+                tt.t[i / tt.ww] |= v << (i % tt.ww);
+            }
+        }
+        tt.RandomSiftReo( nRounds );
+        Ttopt::TruthTable tt2( nInputs, nOuts );
+        tt2.t = tt.t;
+        tt2.Reo( tt.vLevels );
+        tt2.BDDGenerateAig( pNew, vSupp );
+        Vec_IntFree( vSupp );
+    }
+    Gia_ObjComputeTruthTableStop( p );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity )
+{
+    int fVerbose = 0;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vSupp;
+    word v;
+    word * pTruth, * pCare;
+    int i, g, k, nInputs;
+    Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileName, fVerbose );
+    Gia_ManLevelNum( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManForEachCi( p, pObj, k )
+        Gia_ManAppendCi( pNew );
+    Gia_ObjComputeTruthTableStart( p, nIns );
+    Gia_ManHashStart( pNew );
+    for ( g = 0; g < Gia_ManCoNum(p); g += nOuts )
+    {
+        vSupp = Gia_ManCollectSuppNew( p, g, nOuts );
+        nInputs = Vec_IntSize( vSupp );
+        Ttopt::TruthTableLevelTSM tt( nInputs, nOuts );
+        for ( k = 0; k < nOuts; k++ )
+        {
+            pObj = Gia_ManCo( p, g+k );
+            pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp );
+            if ( nInputs >= 6 )
+                for ( i = 0; i < tt.nSize; i++ )
+                    tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i];
+            else
+            {
+                i = k * (1 << nInputs);
+                v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs];
+                tt.t[i / tt.ww] |= v << (i % tt.ww);
+            }
+        }
+        i = 1 << Vec_IntSize( vSupp );
+        pCare = Gia_ManCountFraction( p, vSimI, vSupp, nRarity, fVerbose, &i );
+        tt.care[0] = pCare[0];
+        for ( i = 1; i < tt.nSize; i++ )
+            tt.care[i] = pCare[i];
+        ABC_FREE( pCare );
+        tt.RandomSiftReo( nRounds );
+        tt.Optimize();
+        tt.BDDGenerateAig( pNew, vSupp );
+        Vec_IntFree( vSupp );
+    }
+    Gia_ObjComputeTruthTableStop( p );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_WrdFreeP( &vSimI );
+    return pNew;
+}
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index d8130550..dfddc693 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -3130,6 +3130,37 @@ void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Transform flops.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintArray( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i, nSize = Gia_ManObjNum(p);
+    printf( "static int s_ArraySize = %d;\n", nSize );
+    printf( "static int s_ArrayData[%d] = {\n", 2*nSize );
+    printf( "    0, 0," );
+    printf( "\n    " );
+    Gia_ManForEachCi( p, pObj, i )
+        printf( "0, 0,  " );
+    printf( "\n    " );
+    Gia_ManForEachAnd( p, pObj, i )
+        printf( "%d, %d,  ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit1p(p, pObj) );
+    printf( "\n    " );
+    Gia_ManForEachCo( p, pObj, i )
+        printf( "%d, %d,  ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) );
+    printf( "\n" );
+    printf( "};\n" );
+
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 171d8be3..870da208 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -77,6 +77,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaSatLut.c \
     src/aig/gia/giaSatMap.c \
     src/aig/gia/giaSatoko.c \
+    src/aig/gia/giaSatSyn.c \
     src/aig/gia/giaSat3.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaScript.c \
@@ -104,5 +105,6 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaTis.c \
     src/aig/gia/giaTruth.c \
     src/aig/gia/giaTsim.c \
+    src/aig/gia/giaTtopt.cpp \
     src/aig/gia/giaUnate.c \
     src/aig/gia/giaUtil.c
diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h
index 0365b946..9aa41b11 100644
--- a/src/aig/miniaig/miniaig.h
+++ b/src/aig/miniaig/miniaig.h
@@ -144,6 +144,18 @@ static Mini_Aig_t * Mini_AigStart()
     Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
     return p;
 }
+static Mini_Aig_t * Mini_AigStartSupport( int nIns, int nObjsAlloc )
+{
+    Mini_Aig_t * p; int i;
+    assert( 1+nIns < nObjsAlloc );
+    p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
+    p->nCap   = 2*nObjsAlloc;
+    p->nSize  = 2*(1+nIns);
+    p->pArray = MINI_AIG_ALLOC( int, p->nCap );
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = MINI_AIG_NULL;
+    return p;
+}
 static void Mini_AigStop( Mini_Aig_t * p )
 {
     MINI_AIG_FREE( p->pArray );
@@ -170,6 +182,31 @@ static int Mini_AigAndNum( Mini_Aig_t * p )
         nNodes++;
     return nNodes;
 }
+static int Mini_AigXorNum( Mini_Aig_t * p )
+{
+    int i, nNodes = 0;
+    Mini_AigForEachAnd( p, i )
+        nNodes += p->pArray[2*i] > p->pArray[2*i+1];
+    return nNodes;
+}
+static int Mini_AigLevelNum( Mini_Aig_t * p )
+{
+    int i, Level = 0;
+    int * pLevels = MINI_AIG_CALLOC( int, Mini_AigNodeNum(p) );
+    Mini_AigForEachAnd( p, i )
+    {
+        int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
+        int Lel1 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin1(p, i))];
+        pLevels[i] = 1 + (Lel0 > Lel1 ? Lel0 : Lel1);
+    }
+    Mini_AigForEachPo( p, i )
+    {
+        int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
+        Level = Level > Lel0 ? Level : Lel0;
+    }
+    MINI_AIG_FREE( pLevels );
+    return Level;
+}
 static void Mini_AigPrintStats( Mini_Aig_t * p )
 {
     printf( "MiniAIG stats:  PI = %d  PO = %d  FF = %d  AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) );
@@ -648,6 +685,25 @@ int main( int argc, char ** argv )
 }
 */
 
+/*
+#include "aig/miniaig/miniaig.h"
+
+// this procedure creates a MiniAIG for function F = a*b + ~c and writes it into a file "test.aig"
+void Mini_AigTest()
+{
+    Mini_Aig_t * p = Mini_AigStart();    // create empty AIG manager (contains only const0 node)
+    int litApos = Mini_AigCreatePi( p ); // create input A (returns pos lit of A)
+    int litBpos = Mini_AigCreatePi( p ); // create input B (returns pos lit of B)
+    int litCpos = Mini_AigCreatePi( p ); // create input C (returns pos lit of C)
+    int litCneg = Mini_AigLitNot( litCpos ); // neg lit of C
+    int litAnd  = Mini_AigAnd( p, litApos, litBpos ); // lit for a*b
+    int litOr   = Mini_AigOr( p, litAnd, litCneg );   // lit for a*b + ~c
+    Mini_AigCreatePo( p, litOr );                     // create primary output
+    Mini_AigerWrite( "test.aig", p, 1 );              // write the result into a file
+    Mini_AigStop( p );                                // deallocate MiniAIG
+}
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h
index 68c2779c..19373063 100644
--- a/src/aig/miniaig/ndr.h
+++ b/src/aig/miniaig/ndr.h
@@ -506,7 +506,7 @@ static inline void Ndr_WriteVerilogModule( FILE * pFile, void * pDesign, int Mod
         else if ( nArray == 3 && Type == ABC_OPER_ARI_ADD )
             fprintf( pFile, "%s + %s + %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
         else if ( Type == ABC_OPER_BIT_MUX )
-            fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
+            fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[2]], pNames[pArray[1]] );
         else
             fprintf( pFile, "<cannot write operation %s>;\n", Abc_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) );
     }
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 29753210..88a16e7b 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -3267,6 +3267,91 @@ Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp )
     return Abc_NtkStrashToGia( pNtkNew );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int s_ArraySize = 145;
+static int s_ArrayData[290] = {
+    0, 0,
+    0, 0,  0, 0,  0, 0,  0, 0,  0, 0,  0, 0,  0, 0,  0, 0,
+    10, 6,  14, 12,  10, 2,  22, 20,  2, 24,  16, 4,  28, 18,  16, 10,  8, 4,  34, 32,  30, 36,  38, 26,  16, 6,  36, 20,  44, 42,  46, 40,  42, 44,  14, 6,  52, 34,  32, 54,  56, 50,  58, 48,  32, 24,  20, 2,  12, 6,  66, 34,  68, 64,  62, 70,  28, 68,  74, 72,  76, 58,  70, 62,  80, 78,  68, 28,  84, 74,  4, 2,  88, 20,  64, 90,  92, 86,  66, 32,  18, 96,  98, 56,  100, 94,  52, 36,  104, 38,  90, 42,  36, 2,  108, 110,  112, 106,  114, 100,  102, 116,  118, 82,  116, 60,  120, 122,  124, 60,  118, 60,  102, 82,  128, 130,  132, 82,  134, 126,  82, 116,  122, 138,  122, 118,  142, 140,  60, 102,  130, 146,  130, 118,  150, 148,  152, 144,  154, 136,  18, 156,  144, 126,  68, 160,  32, 136,  164, 162,  166, 158,  28, 160,  70, 126,  90, 144,  174, 172,  176, 170,  152, 134,  36, 180,  2, 134,  184, 182,  186, 178,  188, 168,  64, 144,  164, 158,  194, 192,  96, 156,  44, 154,  200, 170,  202, 198,  204, 176,  206, 196,  204, 168,  62, 126,  212, 186,  24, 134,  108, 152,  218, 192,  220, 216,  222, 214,  224, 210,  220, 194,  110, 152,  30, 180,  232, 230,  184, 172,  236, 234,  238, 228,  234, 182,  242, 220,  244, 168,  42, 154,  248, 202,  54, 136,  252, 164,  254, 214,  256, 250,  218, 194,  252, 198,  262, 242,  264, 260,  232, 220,  268, 262,  270, 168,
+    191, 191,  209, 209,  226, 226,  240, 240,  246, 246,  259, 259,  267, 267,  272, 272,
+};
+int Abc_NtkHasConstNode()
+{
+    int i;
+    for ( i = 1; i < s_ArraySize; i++ )
+        if ( s_ArrayData[2*i] || s_ArrayData[2*i+1] )
+            break;
+    for ( ; i < s_ArraySize; i++ )
+        if ( s_ArrayData[2*i] < 2 && s_ArrayData[2*i+1] < 2 )
+            return 1;
+    return 0;
+}
+Abc_Ntk_t * Abc_NtkFromArray()
+{
+    Vec_Ptr_t * vNodes  = Vec_PtrAlloc( s_ArraySize ); int i, nPos = 0; 
+    Abc_Ntk_t * pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    Abc_Obj_t * pObjNew = Abc_NtkHasConstNode() ? Abc_NtkCreateNode(pNtkNew) : NULL; 
+    if ( pObjNew ) pObjNew->pData = Abc_SopCreateConst0((Mem_Flex_t *)pNtkNew->pManFunc);
+    Vec_PtrPush( vNodes, pObjNew );
+    for ( i = 1; i < s_ArraySize; i++ )
+        if ( !s_ArrayData[2*i] && !s_ArrayData[2*i+1] )
+            Vec_PtrPush( vNodes, Abc_NtkCreatePi(pNtkNew) );
+        else
+            break;
+    for ( ; i < s_ArraySize; i++ )
+    {
+        char * pSop = NULL;
+        if ( s_ArrayData[2*i] > s_ArrayData[2*i+1] )
+            pSop = Abc_SopCreateXor( (Mem_Flex_t *)pNtkNew->pManFunc, 2 );
+        else if ( s_ArrayData[2*i] < s_ArrayData[2*i+1] )
+            pSop = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
+        else
+            break;
+        pObjNew = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i]))   );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i+1])) );
+        if ( Abc_LitIsCompl(s_ArrayData[2*i])   )  Abc_SopComplementVar( pSop, 0 );
+        if ( Abc_LitIsCompl(s_ArrayData[2*i+1]) )  Abc_SopComplementVar( pSop, 1 );
+        pObjNew->pData = pSop;
+        Vec_PtrPush( vNodes, pObjNew );
+    }
+    for ( ; i < s_ArraySize; i++ )
+    {
+        char * pSop = NULL;
+        assert( s_ArrayData[2*i] == s_ArrayData[2*i+1] );
+        pObjNew = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i]))   );
+        if ( Abc_LitIsCompl(s_ArrayData[2*i]) )
+            pSop = Abc_SopCreateInv( (Mem_Flex_t *)pNtkNew->pManFunc );
+        else
+            pSop = Abc_SopCreateBuf( (Mem_Flex_t *)pNtkNew->pManFunc );
+        pObjNew->pData = pSop;
+        Vec_PtrPush( vNodes, pObjNew );
+        nPos++;
+    }
+    for ( i = 0; i < nPos; i++ )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), (Abc_Obj_t *)Vec_PtrEntry(vNodes, s_ArraySize-nPos+i) );
+    Vec_PtrFree( vNodes );
+    pNtkNew->pName = Extra_UtilStrsav("test");
+    Abc_NtkAddDummyPiNames( pNtkNew );
+    Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        Abc_Print( 1, "Abc_NtkFromArray(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bb64a3f3..fd677ace 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -499,6 +499,9 @@ static int Abc_CommandAbc9LNetRead           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9LNetSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9LNetEval           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9LNetOpt            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//#ifndef _WIN32
+static int Abc_CommandAbc9Ttopt              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//#endif
 static int Abc_CommandAbc9LNetMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -561,6 +564,7 @@ static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfsd               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9DeepSyn            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SatSyn             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9StochSyn           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1248,6 +1252,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetsim",      Abc_CommandAbc9LNetSim,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lneteval",     Abc_CommandAbc9LNetEval,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetopt",      Abc_CommandAbc9LNetOpt,      0 );
+//#ifndef _WIN32
+    Cmd_CommandAdd( pAbc, "ABC9",         "&ttopt",        Abc_CommandAbc9Ttopt,        0 );
+//#endif
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetmap",      Abc_CommandAbc9LNetMap,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
@@ -1310,6 +1317,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfsd",         Abc_CommandAbc9Mfsd,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&deepsyn",      Abc_CommandAbc9DeepSyn,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&satsyn",       Abc_CommandAbc9SatSyn,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&stochsyn",     Abc_CommandAbc9StochSyn,     0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
@@ -8764,11 +8772,13 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars );
     extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars );
-    int c;
+    extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars );
+    extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars );
+    int c, fKissat = 0, fKissat2 = 0;
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "INTadconugklvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8808,12 +8818,30 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fOnlyAnd ^= 1;
             break;
+        case 'd':
+            pPars->fDynConstr ^= 1;
+            break;
+        case 'c':
+            pPars->fDumpCnf ^= 1;
+            break;
         case 'o':
             pPars->fFewerVars ^= 1;
             break;
+        case 'n':
+            pPars->fOrderNodes ^= 1;
+            break;
+        case 'u':
+            pPars->fUniqFans ^= 1;
+            break;
         case 'g':
             pPars->fGlucose ^= 1;
             break;
+        case 'k':
+            fKissat ^= 1;
+            break;
+        case 'l':
+            fKissat2 ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -8845,21 +8873,31 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
         return 1;
     }
-    if ( pPars->fGlucose )
+    if ( fKissat )
+        Exa_ManExactSynthesis4( pPars );
+    else if ( fKissat2 )
+        Exa_ManExactSynthesis5( pPars );
+    else if ( pPars->fGlucose )
         Exa_ManExactSynthesis( pPars );
     else
         Exa_ManExactSynthesis2( pPars );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" );
+    Abc_Print( -2, "usage: twoexact [-INT <num>] [-adconugklvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of multi-input function using two-input gates\n" );
     Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
     Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
     Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
     Abc_Print( -2, "\t-a       : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
+    Abc_Print( -2, "\t-d       : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
+    Abc_Print( -2, "\t-c       : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" );
     Abc_Print( -2, "\t-o       : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
+    Abc_Print( -2, "\t-n       : toggle ordering internal nodes [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
+    Abc_Print( -2, "\t-u       : toggle using unique fanouts [default = %s]\n", pPars->fUniqFans ? "yes" : "no" );
     Abc_Print( -2, "\t-g       : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
+    Abc_Print( -2, "\t-k       : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" );
+    Abc_Print( -2, "\t-l       : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
     Abc_Print( -2, "\t<hex>    : truth table in hex notation\n" );
@@ -9029,7 +9067,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MINKiaoegvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MINKianegvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9083,7 +9121,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fOnlyAnd ^= 1;
             break;
-        case 'o':
+        case 'n':
             pPars->fOrderNodes ^= 1;
             break;
         case 'e':
@@ -9179,7 +9217,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: allexact [-MIKN <num>] [-iaoevh] <hex>\n" );
+    Abc_Print( -2, "usage: allexact [-MIKN <num>] [-ianevh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of I-input function using N K-input gates\n" );
     Abc_Print( -2, "\t-M <num> : the majority support size (overrides -I and -K) [default = %d]\n", pPars->nMajSupp );
     Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
@@ -9187,7 +9225,7 @@ usage:
     Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
     Abc_Print( -2, "\t-i       : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
     Abc_Print( -2, "\t-a       : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
-    Abc_Print( -2, "\t-o       : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
+    Abc_Print( -2, "\t-n       : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
     Abc_Print( -2, "\t-e       : toggle enumerating all solutions [default = %s]\n", pPars->fEnumSols ? "yes" : "no" );
 //    Abc_Print( -2, "\t-g       : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
@@ -14065,6 +14103,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
     //Mnist_ExperimentWithScaling( nDecMax );
     //Gyx_ProblemSolveTest();
+    {
+        extern Abc_Ntk_t * Abc_NtkFromArray();
+        Abc_Ntk_t * pNtkRes = Abc_NtkFromArray();
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    }
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -32417,13 +32460,14 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     int c, Limit = 2;
     int Multi = 0;
+    int fAddBuffs  = 0;
     int fAddStrash = 0;
-    int fCollapse = 0;
-    int fAddMuxes = 0;
-    int fStrMuxes = 0;
+    int fCollapse  = 0;
+    int fAddMuxes  = 0;
+    int fStrMuxes  = 0;
     int fRehashMap = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LMacmrsh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32449,6 +32493,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Multi <= 0 )
                 goto usage;
             break;
+        case 'b':
+            fAddBuffs ^= 1;
+            break;
         case 'a':
             fAddStrash ^= 1;
             break;
@@ -32475,6 +32522,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
         return 1;
     }
+    if ( fAddBuffs )
+    {
+        extern Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p );
+        pTemp = Gia_ManDupAddBufs( pAbc->pGia );
+        Abc_FrameUpdateGia( pAbc, pTemp );
+        return 0;
+    }
     if ( Multi > 0 )
     {
         extern Gia_Man_t * Gia_ManDupAddPis( Gia_Man_t * p, int nMulti );
@@ -32549,8 +32603,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &st [-LM num] [-acmrsh]\n" );
+    Abc_Print( -2, "usage: &st [-LM num] [-bacmrsh]\n" );
     Abc_Print( -2, "\t         performs structural hashing\n" );
+    Abc_Print( -2, "\t-b     : toggle adding buffers at the inputs and outputs [default = %s]\n", fAddBuffs? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
@@ -39522,7 +39577,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fUse34Spec ^= 1;
             break;
         case 'b':
-            pPars->fUseBat ^= 1;
+            //pPars->fUseBat ^= 1;
+            pPars->fUseCheck1 ^= 1;
             break;
         case 'g':
             pPars->fDelayOpt ^= 1;
@@ -39543,7 +39599,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fEnableCheck75u ^= 1;
             break;
         case 'i':
-            pPars->fUseCofVars ^= 1;
+            //pPars->fUseCofVars ^= 1;
+            pPars->fUseCheck2 ^= 1;
             break;
 //        case 'j':
 //            pPars->fEnableCheck07 ^= 1;
@@ -39656,6 +39713,16 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pFuncCell = If_CutPerformCheck07;
         pPars->fCutMin = 1;
     }
+    if ( pPars->fUseCheck1 || pPars->fUseCheck2 )
+    {
+        if ( pPars->nLutSize > 6 )
+        {
+            Abc_Print( -1, "This feature only works for no more than 6-LUTs.\n" );
+            return 1;
+        }
+        pPars->pFuncCell = pPars->fUseCheck2 ? If_MatchCheck2 : If_MatchCheck1;
+        pPars->fCutMin = 1;
+    }
     if ( pPars->fUseCofVars )
     {
         if ( !(pPars->nLutSize & 1) )
@@ -42176,6 +42243,116 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Ttopt( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    char * pFileName = NULL;
+    int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nIns = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nOuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            Limit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'X':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-X\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( argc > globalUtilOptind + 1 )
+    {
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] );
+            return 0;
+        }
+        fclose( pFile );
+        pFileName = argv[globalUtilOptind];
+    }
+    if ( pFileName )
+        pTemp = Gia_ManTtoptCare( pAbc->pGia, nIns, nOuts, nRounds, pFileName, Limit );
+    else
+        pTemp = Gia_ManTtopt( pAbc->pGia, nIns, nOuts, nRounds );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &ttopt [-IORX num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t           performs specialized AIG optimization\n" );
+    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",                 nIns );
+    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",                  nOuts );
+    Abc_Print( -2, "\t-R num   : patterns are cares starting this value [default = %d]\n", Limit );
+    Abc_Print( -2, "\t-X num   : the number of optimization rounds [default = %d]\n",      nRounds );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",                 fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    Abc_Print( -2, "\t<file>   : file name with simulation information\n");
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Yukio Miyasaka.\n" );
+    Abc_Print( -2, "\t           The paper describing the method: Y. Miyasaka et al. \"Synthesizing\n" );
+    Abc_Print( -2, "\t           a class of practical Boolean functions using truth tables\". Proc. IWLS 2022.\n" );
+    Abc_Print( -2, "\t           https://people.eecs.berkeley.edu/~alanmi/publications/2022/iwls22_reo.pdf\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9LNetMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fTryNew, int fVerbose );
@@ -48333,6 +48510,96 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9SatSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int TimeOut, int fUseXor, int fFancy, int fVerbose );
+    Gia_Man_t * pTemp; int c, nNodes = 0, nOuts = 0, TimeOut = 0, fUseXor = 0, fFancy = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NTafvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodes < 0 )
+                goto usage;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nOuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nOuts < 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOut < 0 )
+                goto usage;
+            break;
+        case 'a':
+            fUseXor ^= 1;
+            break;
+        case 'f':
+            fFancy ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SatSyn(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Gia_ManSyn( pAbc->pGia, nNodes, nOuts, TimeOut, fUseXor, fFancy, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &satsyn [-NOT <num>] [-afvh]\n" );
+    Abc_Print( -2, "\t           performs synthesis\n" );
+    Abc_Print( -2, "\t-N <num> : the number of window nodes [default = %d]\n",                 nNodes  );
+    Abc_Print( -2, "\t-O <num> : the number of window outputs [default = %d]\n",               nOuts  );
+    Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n",    TimeOut );
+    Abc_Print( -2, "\t-a       : toggle using xor-nodes [default = %s]\n",                     fUseXor? "yes": "no" );
+    Abc_Print( -2, "\t-f       : toggle using additional feature [default = %s]\n",            fFancy? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",       fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript );
@@ -50090,6 +50357,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Gia_ManPrintArray( Gia_Man_t * p );
     extern Gia_Man_t * Gia_ManPerformNewResub( Gia_Man_t * p, int nWinCount, int nCutSize, int nProcs, int fVerbose );
     extern void Gia_RsbEnumerateWindows( Gia_Man_t * p, int nInputsMax, int nLevelsMax );
     extern int Gia_ManSumTotalOfSupportSizes( Gia_Man_t * p );
@@ -50154,7 +50422,16 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
         return 1;
     }
-    Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
+    if ( argc == globalUtilOptind + 1 )
+    {
+        extern void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld );
+        Gia_Man_t * pTemp = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 );
+        Gia_ManUpdateCoPhase( pAbc->pGia, pTemp );
+        Gia_ManStop( pTemp );
+        return 0;
+    }
+    //Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
+    Gia_ManPrintArray( pAbc->pGia );
 //    printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
     return 0;
 usage:
diff --git a/src/base/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c
index d401281a..a7615c2d 100644
--- a/src/base/wlc/wlcNdr.c
+++ b/src/base/wlc/wlcNdr.c
@@ -535,10 +535,23 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
   SeeAlso     []
 
 ***********************************************************************/
+void Ndr_DumpNdr( void * pDesign )
+{
+    int i;
+    char ** pNames = ABC_CALLOC( char *, 10000 );
+    for ( i = 0; i < 10000; i++ )
+    {
+        char Buffer[100];
+        sprintf( Buffer, "s%d", i );
+        pNames[i] = Abc_UtilStrsav( Buffer );
+    }
+    Ndr_WriteVerilog( "temp.v", pDesign, pNames, 0 );
+}
 Wlc_Ntk_t * Wlc_ReadNdr( char * pFileName )
 {
     void * pData = Ndr_Read( pFileName );
     Wlc_Ntk_t * pNtk = Wlc_NtkFromNdr( pData );
+    //Ndr_DumpNdr( pData );
     //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
     //Ndr_WriteVerilog( NULL, pData, ppNames, 0 );
     //Ndr_Delete( pData );
diff --git a/src/base/wln/wlnBlast.c b/src/base/wln/wlnBlast.c
index a3ac73c0..887412d6 100644
--- a/src/base/wln/wlnBlast.c
+++ b/src/base/wln/wlnBlast.c
@@ -289,9 +289,17 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
         {
             int fBooth  = 1;
             int fCla    = 0;
-            int fSigned = fSign0 && fSign1;
+            int fSigned = fSign0 && fSign1;   
+            //int i, iObj;
             Vec_IntShrink( vArg0, nSizeArg0 );
             Vec_IntShrink( vArg1, nSizeArg1 );
+
+            //printf( "Adding %d + %d + %d buffers\n", nSizeArg0, nSizeArg1, nRange ); 
+            //Vec_IntForEachEntry( vArg0, iObj, i )
+            //    Vec_IntWriteEntry( vArg0, i, Gia_ManAppendBuf(pNew, iObj) );
+            //Vec_IntForEachEntry( vArg1, iObj, i )
+            //    Vec_IntWriteEntry( vArg1, i, Gia_ManAppendBuf(pNew, iObj) );
+
             if ( Wlc_NtkCountConstBits(Vec_IntArray(vArg0), Vec_IntSize(vArg0)) < Wlc_NtkCountConstBits(Vec_IntArray(vArg1), Vec_IntSize(vArg1)) )
                 ABC_SWAP( Vec_Int_t, *vArg0, *vArg1 )
             if ( fBooth )
@@ -303,6 +311,9 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
             else
                 Vec_IntShrink( vRes, nRange );
             assert( Vec_IntSize(vRes) == nRange );
+
+            //Vec_IntForEachEntry( vRes, iObj, i )
+            //    Vec_IntWriteEntry( vRes, i, Gia_ManAppendBuf(pNew, iObj) );
             return;
         }
         if ( Type == ABC_OPER_ARI_DIV || Type == ABC_OPER_ARI_MOD )
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
index eb96132b..09cbe90f 100644
--- a/src/base/wln/wlnCom.c
+++ b/src/base/wln/wlnCom.c
@@ -92,12 +92,13 @@ void Wln_End( Abc_Frame_t * pAbc )
 ******************************************************************************/
 int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
-    extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose );
+    extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
+    extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
 
     FILE * pFile;
     char * pFileName = NULL;
     char * pTopModule= NULL;
+    char * pDefines  = NULL;
     int fBlast       =    0;
     int fInvert      =    0;
     int fTechMap     =    1;
@@ -105,7 +106,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCollapse    =    0;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TDbismcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -118,6 +119,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTopModule = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pDefines = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'b':
             fBlast ^= 1;
             break;
@@ -164,11 +174,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Gia_Man_t * pNew = NULL;
         if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
         else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
         else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
         else
         {
             printf( "Abc_CommandYosys(): Unknown file extension.\n" );
@@ -180,11 +190,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Rtl_Lib_t * pLib = NULL;
         if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
         else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
         else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
         else
         {
             printf( "Abc_CommandYosys(): Unknown file extension.\n" );
@@ -194,11 +204,12 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%yosys [-T <module>] [-bismcvh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-bismcvh] <file_name>\n" );
     Abc_Print( -2, "\t         reads Verilog or SystemVerilog using Yosys\n" );
     Abc_Print( -2, "\t-T     : specify the top module name (default uses \"-auto-top\"\n" );
+    Abc_Print( -2, "\t-D     : specify defines to be used by Yosys (default \"not used\")\n" );
     Abc_Print( -2, "\t-b     : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
-    Abc_Print( -2, "\t-i     : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
     Abc_Print( -2, "\t-m     : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "yes": "no" );
@@ -330,13 +341,13 @@ usage:
 ******************************************************************************/
 int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose );
+    extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose );
     Gia_Man_t * pNew = NULL;
     Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
     char * pTopModule = NULL;
-    int c, fInv = 0, fVerbose  = 0;
+    int c, fInv = 0, fRev = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Tcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Tcrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -352,6 +363,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fInv ^= 1;
             break;
+        case 'r':
+            fRev ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -366,16 +380,17 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "The design is not entered.\n" );
         return 1;
     }
-    pNew = Rtl_LibCollapse( pLib, pTopModule, fVerbose );
+    pNew = Rtl_LibCollapse( pLib, pTopModule, fRev, fVerbose );
     if ( fInv )
         Gia_ManInvertPos( pNew );
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%collapse [-T <module>] [-cvh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%collapse [-T <module>] [-crvh] <file_name>\n" );
     Abc_Print( -2, "\t         collapse hierarchical design into an AIG\n" );
     Abc_Print( -2, "\t-T     : specify the top module of the design [default = none]\n" );
     Abc_Print( -2, "\t-c     : toggle complementing miter outputs after collapsing [default = %s]\n", fInv? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle bit order reversal in the word-level IO [default = %s]\n", fRev? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index a27d38d2..b45e51f2 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -1736,6 +1736,42 @@ int Rtl_NtkInsertSignalRange( Rtl_Ntk_t * p, int Sig, int * pLits, int nLits )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Int_t * Rtl_NtkRevPermInput( Rtl_Ntk_t * p )
+{
+    Vec_Int_t * vNew = Vec_IntAlloc( 100 ); int b, i, Count = 0;
+    for ( i = 0; i < p->nInputs; i++ )
+    {
+        int Width = Rtl_WireWidth( p, i );
+        for ( b = 0; b < Width; b++ )
+            Vec_IntPush( vNew, Count + Width-1-b );
+        Count += Width;
+    }
+    return vNew;
+}
+Vec_Int_t * Rtl_NtkRevPermOutput( Rtl_Ntk_t * p )
+{
+    Vec_Int_t * vNew = Vec_IntAlloc( 100 );  int b, i, Count = 0;
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        int Width = Rtl_WireWidth( p, p->nInputs + i );
+        for ( b = 0; b < Width; b++ )
+            Vec_IntPush( vNew, Count + Width-1-b );
+        Count += Width;
+    }
+    return vNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Rtl_NtkBlastInputs( Gia_Man_t * pNew, Rtl_Ntk_t * p )
 {
     int b, i;
@@ -2704,6 +2740,41 @@ Gia_Man_t * Rtl_ReduceInverse( Rtl_Lib_t * pLib, Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Gia_Man_t * Gia_ManDupPermIO( Gia_Man_t * p, Vec_Int_t * vPermI, Vec_Int_t * vPermO )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Vec_IntSize(vPermI) == Gia_ManCiNum(p) );
+    assert( Vec_IntSize(vPermO) == Gia_ManCoNum(p) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        Gia_ManCi(p, Vec_IntEntry(vPermI, i))->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        assert( Abc_Lit2Var(pObj->Value) == i );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, Vec_IntEntry(vPermO, i))) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Rtl_LibReturnNtk( Rtl_Lib_t * p, char * pModule )
 {
     int NameId = Wln_ReadFindToken( pModule, p->pManName );
@@ -2715,7 +2786,7 @@ int Rtl_LibReturnNtk( Rtl_Lib_t * p, char * pModule )
     }
     return iNtk;
 }
-Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
+Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose )
 {
     Gia_Man_t * pGia = NULL;
     int NameId = Wln_ReadFindToken( pTopModule, p->pManName );
@@ -2733,6 +2804,16 @@ Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
         Vec_IntPush( vRoots, iNtk );
         Rtl_LibBlast2( p, vRoots, 1 );
         pGia = Gia_ManDup( pTop->pGia );
+        if ( fRev )
+        {
+            Gia_Man_t * pTemp;
+            Vec_Int_t * vPermI = Rtl_NtkRevPermInput( pTop );
+            Vec_Int_t * vPermO = Rtl_NtkRevPermOutput( pTop );
+            pGia = Gia_ManDupPermIO( pTemp = pGia, vPermI, vPermO );
+            Vec_IntFree( vPermI );
+            Vec_IntFree( vPermO );
+            Gia_ManStop( pTemp );
+        }
         //Gia_AigerWrite( pGia, "temp_miter.aig", 0, 0, 0 );
         if ( pTop->pGia->vBarBufs )
             pGia->vBarBufs = Vec_IntDup( pTop->pGia->vBarBufs );
diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c
index 8a8e0a32..391d168c 100644
--- a/src/base/wln/wlnRtl.c
+++ b/src/base/wln/wlnRtl.c
@@ -139,7 +139,7 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
     return 1;
 #endif
 }
-Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose )
+Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
 {
     Rtl_Lib_t * pNtk = NULL;
     char Command[1000];
@@ -147,8 +147,10 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
     int fSVlog = strstr(pFileName, ".sv") != NULL;
     if ( strstr(pFileName, ".rtl") )
         return Rtl_LibReadFile( pFileName, pFileName );
-    sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"", 
-        Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName, 
+    sprintf( Command, "%s -qp \"read_verilog %s %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"", 
+        Wln_GetYosysName(), 
+        pDefines  ? pDefines    : "",
+        fSVlog ? "-sv ":"", pFileName, 
         pTopModule ? "-top "    : "", 
         pTopModule ? pTopModule : "", 
         fCollapse ? "flatten; " : "",
@@ -167,16 +169,17 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
     unlink( pFileTemp );
     return pNtk;
 }
-Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
+Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
 {
     Gia_Man_t * pGia = NULL;
     char Command[1000];
     char * pFileTemp = "_temp_.aig";
     int fRtlil = strstr(pFileName, ".rtl") != NULL;
     int fSVlog = strstr(pFileName, ".sv")  != NULL;
-    sprintf( Command, "%s -qp \"%s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"", 
+    sprintf( Command, "%s -qp \"%s %s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"", 
         Wln_GetYosysName(), 
         fRtlil ? "read_rtlil" : "read_verilog",
+        pDefines  ? pDefines    : "",
         fSVlog ? " -sv ":" ", 
         pFileName, 
         pTopModule ? "-top " : "-auto-top", 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 13fa4108..a72da9b9 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -140,6 +140,8 @@ struct If_Par_t_
     int                fUseCofVars;   // use cofactoring variables
     int                fUseAndVars;   // use bi-decomposition
     int                fUseTtPerm;    // compute truth tables of the cut functions
+    int                fUseCheck1;    // compute truth tables of the cut functions
+    int                fUseCheck2;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fDoAverage;    // optimize average rather than maximum level
     int                fHashMapping;  // perform AIG hashing after mapping
@@ -553,6 +555,8 @@ extern int             If_CluCheckExt( void * p, word * pTruth, int nVars, int n
                            char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 );
 extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, 
                            char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
+extern int             If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
+extern int             If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
 /*=== ifDelay.c =============================================================*/
 extern int             If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, Vec_Int_t * vAig, int * piRes, int nSuppAll, int * pArea );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 079781e0..e3d47f1c 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -767,7 +767,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
          (p->pPars->fUseDsd || p->pPars->pFuncCell2 || p->pPars->fUseBat || 
           p->pPars->pLutStruct || p->pPars->fUserRecLib || p->pPars->fUserSesLib || 
           p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || 
-          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
+          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u || p->pPars->fUseCheck1 || p->pPars->fUseCheck2) )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
         if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )
diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c
index 1f3fea3e..b8851e50 100644
--- a/src/map/if/ifDec07.c
+++ b/src/map/if/ifDec07.c
@@ -1116,6 +1116,36 @@ int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
+{
+    if ( nLeaves < nVars )
+        return 1;
+    assert( nLeaves == nVars );
+    if ( Abc_Tt6Check1( ((word *)pTruth)[0], nLeaves ) )
+        return 1;
+    return 0;
+}
+int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
+{
+    if ( nLeaves < nVars )
+        return 1;
+    assert( nLeaves == nVars );
+    if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
+        return 1;
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index f234d354..b3a4caf6 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -167,7 +167,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     int fFunc0R, fFunc1R;
     int i, k, v, iCutDsd, fChange;
     int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || 
-        p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2;
+        p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2;
     int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0);
     assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
diff --git a/src/map/scl/sclLibUtil.c b/src/map/scl/sclLibUtil.c
index f57669b7..7197310f 100644
--- a/src/map/scl/sclLibUtil.c
+++ b/src/map/scl/sclLibUtil.c
@@ -72,6 +72,8 @@ void Abc_SclHashCells( SC_Lib * p )
     SC_LibForEachCell( p, pCell, i )
     {
         pPlace = Abc_SclHashLookup( p, pCell->pName );
+        if ( *pPlace != -1 && pCell->pName )
+            printf( "There are two standard cells with the same name (%s).\n", pCell->pName );
         assert( *pPlace == -1 );
         *pPlace = i;
     }
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index bc8ac3f0..1a771afa 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1589,7 +1589,31 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
             Supp |= (1 << v), (*pSuppSize)++;
     return Supp;
 }
-
+static inline int Abc_Tt6Check1( word t, int nVars )
+{
+    int n, v, u;
+    for ( n = 0; n < 2; n++ )
+    for ( v = 0; v < nVars; v++ )
+    {
+        word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
+        for ( u = 0; u < nVars; u++ )
+            if ( v != u && !Abc_Tt6HasVar(Cof, u) )
+                return 1;
+    }
+    return 0;
+}
+static inline int Abc_Tt6Check2( word t, int nVars )
+{
+    int n, v;
+    for ( n = 0; n < 2; n++ )
+    for ( v = 0; v < nVars; v++ )
+    {
+        word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
+        if ( Cof == 0 || ~Cof == 0 )
+            return 1;
+    }
+    return 0;
+}
 /**Function*************************************************************
 
   Synopsis    [Checks if there is a var whose both cofs have supp <= nSuppLim.]
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index db0059fd..13923511 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -418,7 +418,6 @@ Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
     Aig_Man_t * pAig;
     Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
     pGia = Gia_ManEquivToChoices( pGia, 3 );
-    Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
     pAig = Gia_ManToAig( pGia, 1 );
     Gia_ManStop( pGia );
     return pAig;
diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c
index be88b9be..60fdbc89 100644
--- a/src/proof/cec/cecClass.c
+++ b/src/proof/cec/cecClass.c
@@ -265,10 +265,13 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
+static int s_Count = 0;
+
+int Cec_ManSimClassRefineOne_rec( Cec_ManSim_t * p, int i )
 {
     unsigned * pSim0, * pSim1;
     int Ent;
+    s_Count++;
     Vec_IntClear( p->vClassOld );
     Vec_IntClear( p->vClassNew );
     Vec_IntPush( p->vClassOld, i );
@@ -290,9 +293,22 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
     Cec_ManSimClassCreate( p->pAig, p->vClassOld );
     Cec_ManSimClassCreate( p->pAig, p->vClassNew );
     if ( Vec_IntSize(p->vClassNew) > 1 )
-        return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
+        return 1 + Cec_ManSimClassRefineOne_rec( p, Vec_IntEntry(p->vClassNew,0) );
     return 1;
 }
+int Cec_ManSimClassRefineOne_( Cec_ManSim_t * p, int i )
+{
+    int Res;
+    s_Count = 0;
+    Res = Cec_ManSimClassRefineOne_rec( p, i );
+    if ( s_Count > 10 )
+    printf( "%d ", s_Count );
+    return Res;
+}
+int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
+{
+    return Cec_ManSimClassRefineOne_rec( p, i );
+}
 
 /**Function*************************************************************
 
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 2c843392..34356359 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -54,10 +54,14 @@ struct Bmc_EsPar_t_
     int        fMajority;
     int        fUseIncr;
     int        fOnlyAnd;
+    int        fDynConstr;
+    int        fDumpCnf;
     int        fGlucose;
     int        fOrderNodes;
     int        fEnumSols;
     int        fFewerVars;
+    int        fQuadrEnc;
+    int        fUniqFans;
     int        RuntimeLim;
     int        fVerbose; 
     char *     pTtStr;
@@ -73,10 +77,14 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
     pPars->fMajority   = 0; 
     pPars->fUseIncr    = 0;
     pPars->fOnlyAnd    = 0; 
+    pPars->fDynConstr  = 0; 
+    pPars->fDumpCnf    = 0; 
     pPars->fGlucose    = 0; 
     pPars->fOrderNodes = 0; 
     pPars->fEnumSols   = 0; 
     pPars->fFewerVars  = 0; 
+    pPars->fQuadrEnc   = 0; 
+    pPars->fUniqFans   = 0; 
     pPars->RuntimeLim  = 0;
     pPars->fVerbose    = 1; 
 }
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index fc77398a..2525f943 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -22,15 +22,23 @@
 #include "misc/extra/extra.h"
 #include "misc/util/utilTruth.h"
 #include "sat/glucose/AbcGlucose.h"
+#include "aig/miniaig/miniaig.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
+#ifdef WIN32
+#include <process.h> 
+#define unlink _unlink
+#else
+#include <unistd.h>
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define MAJ_NOBJS  32 // Const0 + Const1 + nVars + nNodes
+#define MAJ_NOBJS  64 // Const0 + Const1 + nVars + nNodes
 
 typedef struct Maj_Man_t_ Maj_Man_t;
 struct Maj_Man_t_ 
@@ -422,6 +430,8 @@ struct Exa_Man_t_
     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
     Vec_Wec_t *       vOutLits;  // output vars
     bmcg_sat_solver * pSat;      // SAT solver
+    FILE *            pFile;
+    int               nCnfClauses;
 };
 
 static inline word *  Exa_ManTruth( Exa_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
@@ -451,7 +461,7 @@ int Exa_ManMarkup( Exa_Man_t * p )
     int i, k, j;
     assert( p->nObjs <= MAJ_NOBJS );
     // assign functionality
-    p->iVar = 1 + p->nNodes * 3;
+    p->iVar = 1 + 3*p->nNodes;//
     // assign connectivity variables
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
@@ -502,10 +512,26 @@ Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
     if ( pPars->RuntimeLim )
         bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
+    if ( pPars->fDumpCnf )
+    {
+        char Buffer[1000];
+        sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
+        p->pFile = fopen( Buffer, "wb" );
+        fputs( "p cnf                \n", p->pFile );
+    }
     return p;
 }
 void Exa_ManFree( Exa_Man_t * p )
 {
+    if ( p->pFile ) 
+    {
+        char Buffer[1000];
+        sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
+        rewind( p->pFile );
+        fprintf( p->pFile, "p cnf %d %d", bmcg_sat_solver_varnum(p->pSat), p->nCnfClauses );
+        fclose( p->pFile );
+        printf( "CNF was dumped into file \"%s\".\n", Buffer );
+    }
     bmcg_sat_solver_stop( p->pSat );
     Vec_WrdFree( p->vInfo );
     Vec_WecFree( p->vOutLits );
@@ -542,7 +568,7 @@ static inline int Exa_ManEval( Exa_Man_t * p )
     int i, k, iMint; word * pFanins[2];
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
-        int iVarStart = 1 + 3*(i - p->nVars);
+        int iVarStart = 1 + 3*(i - p->nVars);//
         for ( k = 0; k < 2; k++ )
             pFanins[k] = Exa_ManTruth( p, Exa_ManFindFanin(p, i, k) );
         Abc_TtConst0( Exa_ManTruth(p, i), p->nWords );
@@ -596,7 +622,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
     fprintf( pFile, ".outputs F\n" );
     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
     {
-        int iVarStart = 1 + 3*(i - p->nVars);
+        int iVarStart = 1 + 3*(i - p->nVars);//
         int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
         int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
         int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
@@ -634,7 +660,7 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
 //    for ( i = p->nVars + 2; i < p->nObjs; i++ )
     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
     {
-        int iVarStart = 1 + 3*(i - p->nVars);
+        int iVarStart = 1 + 3*(i - p->nVars);//
         int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
         int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
         int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
@@ -666,43 +692,115 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
   SeeAlso     []
 
 ***********************************************************************/
-int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
+static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits )
+{
+    int i;
+    if ( p->pFile )
+    {
+        p->nCnfClauses++;
+        for ( i = 0; i < nLits; i++ )
+            fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( p->pFile, "0\n" );
+    }
+    return bmcg_sat_solver_addclause( p->pSat, pLits, nLits );
+}
+int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded )
 {
     int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
-    // input constraints
+    *pnAdded = 0;
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
-        int iVarStart = 1 + 3*(i - p->nVars);
         for ( k = 0; k < 2; k++ )
         {
             int nLits = 0;
             for ( j = 0; j < p->nObjs; j++ )
-                if ( p->VarMarks[i][k][j] )
+                if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
             assert( nLits > 0 );
             // input uniqueness
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
-                return 0;
             for ( n = 0;   n < nLits; n++ )
             for ( m = n+1; m < nLits; m++ )
             {
+                (*pnAdded)++;
                 pLits2[0] = Abc_LitNot(pLits[n]);
                 pLits2[1] = Abc_LitNot(pLits[m]);
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                     return 0;
             }
             if ( k == 1 )
                 break;
             // symmetry breaking
-            for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
-            for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
+            for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j]   && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
+            for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k+1][j]) )
             {
+                (*pnAdded)++;
                 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
                 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                     return 0;
             }
         }
+    }
+    return 1;
+}
+int Exa_ManSolverSolve( Exa_Man_t * p )
+{
+    int nAdded = 1;
+    while ( nAdded )
+    {
+        int status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+        if ( status != GLUCOSE_SAT )
+            return status;
+        status = Exa_ManAddCnfAdd( p, &nAdded );
+        //printf( "Added %d clauses.\n", nAdded );
+        if ( status != GLUCOSE_SAT )
+            return status;
+    }
+    return GLUCOSE_SAT;
+}
+int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
+{
+    int pLits[MAJ_NOBJS], pLits2[3], i, j, k, n, m;
+    // input constraints
+    for ( i = p->nVars; i < p->nObjs; i++ )
+    {
+        int iVarStart = 1 + 3*(i - p->nVars);//
+        for ( k = 0; k < 2; k++ )
+        {
+            int nLits = 0;
+            for ( j = 0; j < p->nObjs; j++ )
+                if ( p->VarMarks[i][k][j] )
+                    pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
+            assert( nLits > 0 );
+            if ( !Exa_ManAddClause( p, pLits, nLits ) )
+                return 0;
+            // input uniqueness
+            if ( !p->pPars->fDynConstr )
+            {
+                for ( n = 0;   n < nLits; n++ )
+                for ( m = n+1; m < nLits; m++ )
+                {
+                    pLits2[0] = Abc_LitNot(pLits[n]);
+                    pLits2[1] = Abc_LitNot(pLits[m]);
+                    if ( !Exa_ManAddClause( p, pLits2, 2 ) )
+                        return 0;
+                }
+            }
+            if ( k == 1 )
+                break;
+            // symmetry breaking
+            if ( !p->pPars->fDynConstr )
+            {
+                for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
+                for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
+                {
+                    pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
+                    pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
+                    if ( !Exa_ManAddClause( p, pLits2, 2 ) )
+                        return 0;
+                }
+            }
+        }
 #ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
@@ -711,17 +809,34 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
         {
             pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
             pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+            if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                 return 0;
         }
 #endif
+        // unique functions
+        for ( j = p->nVars; j < i; j++ )
+        for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
+        {
+            pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
+            for ( n = 0; n < p->nObjs; n++ ) 
+            for ( m = 0; m < 2; m++ )
+            {
+                if ( p->VarMarks[i][!k][n] && p->VarMarks[j][m][n] )
+                {
+                    pLits2[1] = Abc_Var2Lit( p->VarMarks[i][!k][n], 1 );
+                    pLits2[2] = Abc_Var2Lit( p->VarMarks[j][m][n], 1 );
+                    if ( !Exa_ManAddClause( p, pLits2, 3 ) )
+                        return 0;
+                }
+            }
+        }
         // two input functions
         for ( k = 0; k < 3; k++ )
         {
             pLits[0] = Abc_Var2Lit( iVarStart,   k==1 );
             pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
             pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+            if ( !Exa_ManAddClause( p, pLits, 3 ) )
                 return 0;
         }
         if ( fOnlyAnd )
@@ -729,7 +844,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
             pLits[0] = Abc_Var2Lit( iVarStart,   1 );
             pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
             pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+            if ( !Exa_ManAddClause( p, pLits, 3 ) )
                 return 0;
         }
     }
@@ -738,7 +853,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
     {
         Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
         assert( Vec_IntSize(vArray) > 0 );
-        if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
+        if ( !Exa_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
             return 0;
     }
     return 1;
@@ -754,7 +869,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
         // fanin connectivity
-        int iVarStart = 1 + 3*(i - p->nVars);
+        int iVarStart = 1 + 3*(i - p->nVars);//
         int iBaseSatVarI = p->iVar + 3*(i - p->nVars);
         for ( k = 0; k < 2; k++ )
         {
@@ -770,7 +885,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
                         pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n );
                     else if ( p->VarVals[j] == n )
                         continue;
-                    if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+                    if ( !Exa_ManAddClause( p, pLits, nLits ) )
                         return 0;
                 }
             }
@@ -790,7 +905,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
                 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
                 if ( k > 0 )             pLits[nLits++] = Abc_Var2Lit( iVarStart +  k-1,  n );
                 assert( nLits <= 4 );
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+                if ( !Exa_ManAddClause( p, pLits, nLits ) )
                     return 0;
             }
         }
@@ -815,7 +930,10 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
         abctime clk = Abc_Clock();
         if ( !Exa_ManAddCnf( p, iMint ) )
             break;
-        status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+        if ( pPars->fDynConstr )
+            status = Exa_ManSolverSolve( p );
+        else
+            status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
         if ( pPars->fVerbose )
         {
             printf( "Iter %3d : ", i );
@@ -1141,7 +1259,7 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
         }
 //#ifdef USE_NODE_ORDER
         // node ordering
-        if ( p->pPars->fUseIncr )
+        if ( p->pPars->fOrderNodes )
         {
             for ( j = p->nVars; j < i; j++ )
             for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
@@ -1349,6 +1467,1260 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Exa_ManIsNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut )
+{
+    int i, Count = 0; word Temp;
+    Vec_WrdForEachEntry( vSimsIn, Temp, i )
+        if ( Temp & 1 )
+            Count++;
+    if ( Count )
+        printf( "The data for %d divisors are not normalized.\n", Count );
+    if ( !(Vec_WrdEntry(vSimsOut, 0) & 1) )
+        printf( "The output data is not normalized.\n" );
+//    else if ( Count == 0 )
+//        printf( "The data is fully normalized.\n" );
+}
+static inline void Exa_ManPrintFanin( int nIns, int nDivs, int iNode, int fComp )
+{
+    if ( iNode == 0 )
+        printf( " %s", fComp ? "const1" : "const0" );
+    else if ( iNode > 0 && iNode <= nIns )
+        printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
+    else if ( iNode > nIns && iNode < nDivs )
+        printf( " %s%c", fComp ? "~" : "", 'A'+iNode-nIns-1 );
+    else
+        printf( " %s%d", fComp ? "~" : "", iNode );
+}
+void Exa_ManMiniPrint( Mini_Aig_t * p, int nIns )
+{
+    int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p);
+    printf( "This %d-var function (%d divisors) has %d gates (%d xor) and %d levels:\n", 
+        nIns, nDivs, nNodes, Mini_AigXorNum(p), Mini_AigLevelNum(p) );
+    for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
+    {
+        int Lit0 = Mini_AigNodeFanin0( p, i );
+        printf( "%2d  = ", i );
+        Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
+        printf( "\n" );
+    }
+    for ( i = nDivs + nNodes - 1; i >= nDivs; i-- )
+    {
+        int Lit0 = Mini_AigNodeFanin0( p, i );
+        int Lit1 = Mini_AigNodeFanin1( p, i );
+        printf( "%2d  = ", i );
+        if ( Lit0 < Lit1 )
+        {
+            Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
+            printf( " &" );
+            Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
+        }
+        else
+        {
+            Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
+            printf( " ^" );
+            Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
+        }
+        printf( "\n" );
+    }
+}
+void Exa_ManMiniVerify( Mini_Aig_t * p, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut )
+{
+    extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
+    int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p); 
+    int k, nOuts = Mini_AigPoNum(p), nErrors = 0; word Outs[6] = {0};
+    Vec_Wrd_t * vSimsIn2 = Vec_WrdStart( 64 );
+    assert( nOuts <= 6 );
+    assert( Vec_WrdSize(vSimsIn) <= 64 );
+    assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
+    Vec_WrdFillExtra( vSimsIn, 64, 0 );
+    Extra_BitMatrixTransposeP( vSimsIn, 1, vSimsIn2, 1 );
+    assert( Mini_AigNodeNum(p) <= 64 );
+    for ( i = nDivs; i < nDivs + nNodes; i++ )
+    {
+        int Lit0 = Mini_AigNodeFanin0( p, i );
+        int Lit1 = Mini_AigNodeFanin1( p, i );
+        word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
+        word Sim1 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit1) );
+        Sim0 = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
+        Sim1 = Abc_LitIsCompl(Lit1) ? ~Sim1 : Sim1;
+        Vec_WrdWriteEntry( vSimsIn2, i, Lit0 < Lit1 ? Sim0 & Sim1 : Sim0 ^ Sim1 );
+    }
+    for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
+    {
+        int Lit0 = Mini_AigNodeFanin0( p, i );
+        word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
+        Outs[i - (nDivs + nNodes)] = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
+    }
+    Vec_WrdFree( vSimsIn2 );
+    for ( i = 0; i < Vec_WrdSize(vSimsOut); i++ )
+    {
+        int iOutMint = 0;
+        for ( k = 0; k < nOuts; k++ )
+            if ( (Outs[k] >> i) & 1 )
+                iOutMint |= 1 << k;
+        nErrors += !Abc_TtGetBit(Vec_WrdEntryP(vSimsOut, i), iOutMint);
+    }
+    if ( nErrors == 0 )
+        printf( "Verification successful.  " );
+    else 
+        printf( "Verification failed for %d (out of %d) minterms.\n", nErrors, Vec_WrdSize(vSimsOut) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Exa4_ManParse( char * pFileName )
+{
+    Vec_Int_t * vRes = NULL;
+    char * pToken, pBuffer[1000];
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    while ( fgets( pBuffer, 1000, pFile ) != NULL )
+    {
+        if ( pBuffer[0] == 's' )
+        {
+            if ( strncmp(pBuffer+2, "SAT", 3) )
+                break;
+            assert( vRes == NULL );
+            vRes = Vec_IntAlloc( 100 );
+        }
+        else if ( pBuffer[0] == 'v' )
+        {
+            pToken = strtok( pBuffer+1, " \n\r\t" );
+            while ( pToken )
+            {
+                int Token = atoi(pToken);
+                if ( Token == 0 )
+                    break;
+                Vec_IntSetEntryFull( vRes, Abc_AbsInt(Token), Token > 0 );
+                pToken = strtok( NULL, " \n\r\t" );
+            }
+        }
+        else if ( pBuffer[0] != 'c' )
+            assert( 0 );
+    }
+    fclose( pFile );
+    unlink( pFileName );
+    return vRes;
+}
+Vec_Int_t * Exa4_ManSolve( char * pFileNameIn, char * pFileNameOut, int TimeOut, int fVerbose )
+{
+    int fVerboseSolver = 0;
+    abctime clkTotal = Abc_Clock();
+    Vec_Int_t * vRes = NULL;
+#ifdef _WIN32
+    char * pKissat = "kissat.exe";
+#else
+    char * pKissat = "kissat";
+#endif
+    char Command[1000], * pCommand = (char *)&Command;
+    {
+        FILE * pFile = fopen( pKissat, "rb" );
+        if ( pFile == NULL )
+        {
+            printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
+            return NULL;
+        }
+        fclose( pFile );        
+    }
+    if ( TimeOut )
+        sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+    else
+        sprintf( pCommand, "%s %s %s > %s", pKissat, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+    if ( system( pCommand ) == -1 )
+    {
+        fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand );
+        return 0;
+    }
+    vRes = Exa4_ManParse( pFileNameOut );
+    if ( fVerbose )
+    {
+        if ( vRes )
+            printf( "The problem has a solution. " );
+        else if ( vRes == NULL && TimeOut == 0 )
+            printf( "The problem has no solution. " );
+        else if ( vRes == NULL )
+            printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
+        Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
+    }
+    return vRes;
+}
+
+
+typedef struct Exa4_Man_t_ Exa4_Man_t;
+struct Exa4_Man_t_ 
+{
+    Vec_Wrd_t *       vSimsIn;   // input signatures  (nWords = 1, nIns <= 64)
+    Vec_Wrd_t *       vSimsOut;  // output signatures (nWords = 1, nOuts <= 6)
+    int               fVerbose; 
+    int               nIns;     
+    int               nDivs;     // divisors (const + inputs + tfi + sidedivs)
+    int               nNodes;
+    int               nOuts; 
+    int               nObjs;
+    int               VarMarks[MAJ_NOBJS][2][MAJ_NOBJS];
+    int               nCnfVars; 
+    int               nCnfClauses;
+    FILE *            pFile;
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Exa4_ManMarkup( Exa4_Man_t * p )
+{
+    int i, k, j, nVars[3] = {1 + 5*p->nNodes, 0, 3*p->nNodes*Vec_WrdSize(p->vSimsIn)};
+    assert( p->nObjs <= MAJ_NOBJS );
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+        for ( k = 0; k < 2; k++ )
+            for ( j = 1+!k; j < i-k; j++ )
+                p->VarMarks[i][k][j] = nVars[0] + nVars[1]++;
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+        for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
+            p->VarMarks[i][0][j] = nVars[0] + nVars[1]++;
+    if ( p->fVerbose )
+        printf( "Variables:  Function = %d.  Structure = %d.  Internal = %d.  Total = %d.\n", 
+            nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
+    if ( 0 )
+    {
+        for ( j = 0; j < 2; j++ )
+        {
+            printf( "   : " );
+            for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+            {
+                for ( k = 0; k < 2; k++ )
+                    printf( "%3d ", j ? k : i );
+                printf( " " );
+            }
+            printf( " " );
+            for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+            {
+                printf( "%3d ", j ? 0 : i );
+                printf( " " );
+            }
+            printf( "\n" );
+        }
+        for ( j = 0; j < 5 + p->nNodes*9 + p->nOuts*5; j++ )
+            printf( "-" );
+        printf( "\n" );
+        for ( j = p->nObjs - 2; j >= 0; j-- )
+        {
+            if ( j > 0 && j <= p->nIns )
+                printf( " %c : ", 'a'+j-1 );
+            else
+                printf( "%2d : ", j );
+            for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+            {
+                for ( k = 0; k < 2; k++ )
+                    printf( "%3d ", p->VarMarks[i][k][j] );
+                printf( " " );
+            }
+            printf( " " );
+            for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+            {
+                printf( "%3d ", p->VarMarks[i][0][j] );
+                printf( " " );
+            }
+            printf( "\n" );
+        }
+    }
+    return nVars[0] + nVars[1] + nVars[2];
+}
+Exa4_Man_t * Exa4_ManAlloc( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose )
+{
+    Exa4_Man_t * p = ABC_CALLOC( Exa4_Man_t, 1 );
+    assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
+    p->vSimsIn     = vSimsIn;
+    p->vSimsOut    = vSimsOut;
+    p->fVerbose    = fVerbose;
+    p->nIns        = nIns;  
+    p->nDivs       = nDivs; 
+    p->nNodes      = nNodes;
+    p->nOuts       = nOuts; 
+    p->nObjs       = p->nDivs + p->nNodes + p->nOuts;
+    p->nCnfVars    = Exa4_ManMarkup( p );
+    return p;
+}
+void Exa4_ManFree( Exa4_Man_t * p )
+{
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Exa4_ManAddClause( Exa4_Man_t * p, int * pLits, int nLits )
+{
+    int i, k = 0;
+    for ( i = 0; i < nLits; i++ )
+        if ( pLits[i] == 1 )
+            return 0;
+        else if ( pLits[i] == 0 )
+            continue;
+        else if ( pLits[i] <= 2*p->nCnfVars )
+            pLits[k++] = pLits[i];
+        else assert( 0 );
+    nLits = k;
+    assert( nLits > 0 );
+    if ( p->pFile )
+    {
+        p->nCnfClauses++;
+        for ( i = 0; i < nLits; i++ )
+            fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( p->pFile, "0\n" );
+    }
+    if ( 0 )
+    {
+        for ( i = 0; i < nLits; i++ )
+            fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( stdout, "\n" );
+    }
+    return 1;
+}
+static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Lit2, int Lit3 )
+{
+    int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
+    return Exa4_ManAddClause( p, pLits, 4 );
+}
+int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
+{
+    int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        int iVarStart = 1 + 5*(i - p->nDivs);//
+        for ( k = 0; k < 2; k++ )
+        {
+            nLits = 0;
+            for ( j = 0; j < p->nObjs; j++ )
+                if ( p->VarMarks[i][k][j] )
+                    pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
+            assert( nLits > 0 );
+            Exa4_ManAddClause( p, pLits, nLits );
+            for ( n = 0;   n < nLits; n++ )
+            for ( m = n+1; m < nLits; m++ )
+                Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
+            if ( k == 1 )
+                break;
+            for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
+            for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][1][n] )
+                Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_Var2Lit(p->VarMarks[i][1][n], 1), 0, 0 );
+        }
+        if ( fOrderNodes )
+        for ( j = p->nDivs; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
+            Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][n], 1), Abc_Var2Lit(p->VarMarks[j][0][m], 1), 0, 0 );
+        for ( j = p->nDivs; j < i; j++ )
+        for ( k = 0; k < 2; k++ )        if ( p->VarMarks[i][k][j] )
+        for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][!k][n] )
+        for ( m = 0; m < 2; m++ )        if ( p->VarMarks[j][m][n] )
+            Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(p->VarMarks[i][!k][n], 1), Abc_Var2Lit(p->VarMarks[j][m][n], 1), 0 );
+        if ( fFancy )
+        {
+            nLits = 0;
+            for ( k = 0; k < 5-fOnlyAnd; k++ )
+                pLits[nLits++] = Abc_Var2Lit( iVarStart+k, 0 );
+            Exa4_ManAddClause( p, pLits, nLits );
+            for ( n = 0;   n < nLits; n++ )
+            for ( m = n+1; m < nLits; m++ )
+                Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
+        }
+        else
+        {
+            for ( k = 0; k < 3; k++ )
+                Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0);
+            if ( fOnlyAnd )
+                Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0);
+        }
+    }
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        nLits = 0;
+        for ( k = 0; k < 2; k++ )
+            for ( j = i+1; j < p->nObjs; j++ )
+                if ( p->VarMarks[j][k][i] )
+                    pLits[nLits++] = Abc_Var2Lit( p->VarMarks[j][k][i], 0 );
+        Exa4_ManAddClause( p, pLits, nLits );
+        if ( fUniqFans )
+            for ( n = 0;   n < nLits; n++ )
+            for ( m = n+1; m < nLits; m++ )
+                Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        nLits = 0;
+        for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
+            pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][0][j], 0 );
+        Exa4_ManAddClause( p, pLits, nLits );
+        for ( n = 0;   n < nLits; n++ )
+        for ( m = n+1; m < nLits; m++ )
+            Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
+    }
+    return 1;
+}
+void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
+{
+    int iNodeVar = p->nCnfVars + 3*p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
+    int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
+    int i, k, n, j, VarVals[MAJ_NOBJS];
+    assert( p->nObjs <= MAJ_NOBJS );
+    assert( iMint < Vec_WrdSize(p->vSimsIn) );
+    for ( i = 0; i < p->nDivs; i++ )
+        VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
+    for ( i = 0; i < p->nNodes; i++ )
+        VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
+    for ( i = 0; i < p->nOuts; i++ )
+        VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
+    if ( 0 )
+    {
+        printf( "Adding minterm %d: ", iMint );
+        for ( i = 0; i < p->nObjs; i++ )
+            printf( " %d=%d", i, VarVals[i] );
+        printf( "\n" );
+    }
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        int iVarStart = 1 + 5*(i - p->nDivs);//
+        int iBaseVarI = iNodeVar + 3*(i - p->nDivs);
+        for ( k = 0; k < 2; k++ )
+        for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][k][j] )
+        for ( n = 0; n < 2; n++ )
+            Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
+        if ( fFancy )
+        {
+            //  Clauses for a*b = c
+            //  a + ~c
+            //  b + ~c
+            // ~a + ~b + c
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0,                             Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), 0,                             Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
+
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0,                             Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), 0,                             Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
+
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0,                             Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), 0,                             Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
+            //  Clauses for a+b = c
+            // ~a +  c
+            // ~b +  c
+            //  a +  b + ~c
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0,                             Abc_Var2Lit(iBaseVarI + 2, 0) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), 0,                             Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            //  Clauses for a^b = c
+            // ~a + ~b + ~c
+            // ~a +  b +  c
+            //  a + ~b +  c
+            //  a +  b + ~c
+            if ( !fOnlyAnd )
+            {
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
+            Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
+            }
+        }
+        else
+        {
+            for ( k = 0; k < 4; k++ )
+            for ( n = 0; n < 2; n++ )
+                Exa4_ManAddClause4( p, Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
+        }
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
+        for ( n = 0; n < 2; n++ )
+            Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
+    }
+}
+void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
+{
+    int m;
+    assert( p->pFile == NULL );
+    p->pFile = fopen( pFileName, "wb" );
+    fputs( "p cnf                \n", p->pFile );
+    Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
+    for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
+        Exa4_ManGenMint( p, m, fOnlyAnd, fFancy );
+    rewind( p->pFile );
+    fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses );
+    fclose( p->pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Exa4_ManFindFanin( Exa4_Man_t * p, Vec_Int_t * vValues, int i, int k )
+{
+    int j, Count = 0, iVar = -1;
+    for ( j = 0; j < p->nObjs; j++ )
+        if ( p->VarMarks[i][k][j] && Vec_IntEntry(vValues, p->VarMarks[i][k][j]) )
+        {
+            iVar = j;
+            Count++;
+        }
+    assert( Count == 1 );
+    return iVar;
+}
+static inline void Exa4_ManPrintFanin( Exa4_Man_t * p, int iNode, int fComp )
+{
+    if ( iNode == 0 )
+        printf( " %s", fComp ? "const1" : "const0" );
+    else if ( iNode > 0 && iNode <= p->nIns )
+        printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
+    else if ( iNode > p->nIns && iNode < p->nDivs )
+        printf( " %s%c", fComp ? "~" : "", 'A'+iNode-p->nIns-1 );
+    else
+        printf( " %s%d", fComp ? "~" : "", iNode );
+}
+void Exa4_ManPrintSolution( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
+{
+    int i, k;
+    printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
+        printf( "%2d  = ", i );
+        Exa4_ManPrintFanin( p, iVar, 0 );
+        printf( "\n" );
+    }
+    for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
+    {
+        int iVarStart = 1 + 5*(i - p->nDivs);//
+        if ( fFancy )
+        {
+            int Val1 = Vec_IntEntry(vValues, iVarStart);
+            int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+            int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+            int Val4 = Vec_IntEntry(vValues, iVarStart+3);
+            //int Val5 = Vec_IntEntry(vValues, iVarStart+4);
+            printf( "%2d  = ", i );
+            for ( k = 0; k < 2; k++ )
+            {
+                int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
+                int fComp = k ? Val1 | Val3 : Val2 | Val3;
+                Exa4_ManPrintFanin( p, iNode, fComp );
+                if ( k ) break;
+                printf( " %c", (Val1 || Val2 || Val3) ? '&' : (Val4 ? '|' : '^') );
+            }
+        }
+        else
+        {
+            int Val1 = Vec_IntEntry(vValues, iVarStart);
+            int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+            int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+            printf( "%2d  = ", i );
+            for ( k = 0; k < 2; k++ )
+            {
+                int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
+                int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
+                Exa4_ManPrintFanin( p, iNode, fComp );
+                if ( k ) break;
+                printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
+            }
+        }
+        printf( "\n" );
+    }
+}
+Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
+{
+    int i, k, Compl[MAJ_NOBJS] = {0};
+    Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        int iNodes[2] = {0};
+        int iVarStart = 1 + 5*(i - p->nDivs);//
+        if ( fFancy )
+        {
+            int Val1 = Vec_IntEntry(vValues, iVarStart);
+            int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+            int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+            int Val4 = Vec_IntEntry(vValues, iVarStart+3);
+            int Val5 = Vec_IntEntry(vValues, iVarStart+4);
+            for ( k = 0; k < 2; k++ )
+            {
+                int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
+                int fComp = k ? Val1 | Val3 : Val2 | Val3;
+                iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
+            }
+            if ( Val1 || Val2 || Val3 ) 
+                Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
+            else
+            {
+                if ( Val4 )
+                    Mini_AigOr( pMini, iNodes[0], iNodes[1] );
+                else if ( Val5 )
+                    Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
+                else assert( 0 );
+            }
+        }
+        else
+        {
+            int Val1 = Vec_IntEntry(vValues, iVarStart);
+            int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+            int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+            Compl[i] = Val1 && Val2 && Val3;
+            for ( k = 0; k < 2; k++ )
+            {
+                int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
+                int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
+                iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
+            }
+            if ( Val1 && Val2 ) 
+            {
+                if ( Val3 )
+                    Mini_AigOr( pMini, iNodes[0], iNodes[1] );
+                else
+                    Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
+            }
+            else
+                Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
+        }
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
+        Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
+    }
+    assert( p->nObjs == Mini_AigNodeNum(pMini) );
+    return pMini;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose )
+{
+    Mini_Aig_t * pMini = NULL;
+    abctime clkTotal = Abc_Clock();
+    Vec_Int_t * vValues = NULL;
+    char * pFileNameIn  = "_temp_.cnf";
+    char * pFileNameOut = "_temp_out.cnf";
+    Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
+    Exa_ManIsNormalized( vSimsIn, vSimsOut );
+    Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
+    if ( fVerbose )
+        printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
+    if ( fVerbose )
+        printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
+    vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
+    if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy );
+    //if ( vValues ) Exa4_ManPrintSolution( p, vValues, fFancy );
+    if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
+    if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
+    Vec_IntFreeP( &vValues );
+    Exa4_ManFree( p );
+    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    return pMini;
+}
+void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars )
+{
+    Mini_Aig_t * pMini = NULL;
+    int i, m;
+    Vec_Wrd_t * vSimsIn  = Vec_WrdStart( 8 );
+    Vec_Wrd_t * vSimsOut = Vec_WrdStart( 8 );
+    int Truths[2] = { 0x96, 0xE8 };
+    for ( m = 0; m < 8; m++ )
+    {
+        int iOutMint = 0;
+        for ( i = 0; i < 2; i++ )
+            if ( (Truths[i] >> m) & 1 )
+                iOutMint |= 1 << i;
+        Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), iOutMint );
+        for ( i = 0; i < 3; i++ )
+            if ( (m >> i) & 1 )
+                Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
+    }
+    pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
+    if ( pMini ) Mini_AigStop( pMini );
+    Vec_WrdFree( vSimsIn );
+    Vec_WrdFree( vSimsOut );
+}
+void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars )
+{
+    Mini_Aig_t * pMini = NULL;
+    int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
+    Vec_Wrd_t * vSimsIn  = Vec_WrdStart( nMints );
+    Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
+    word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
+    if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
+    assert( pPars->nVars <= 10 );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
+        for ( i = 0; i < pPars->nVars; i++ )
+            if ( (m >> i) & 1 )
+                Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
+    }
+    assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
+    pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
+    if ( pMini ) Mini_AigStop( pMini );
+    if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
+    Vec_WrdFree( vSimsIn );
+    Vec_WrdFree( vSimsOut );
+}
+
+
+
+typedef struct Exa5_Man_t_ Exa5_Man_t;
+struct Exa5_Man_t_ 
+{
+    Vec_Wrd_t *       vSimsIn;  
+    Vec_Wrd_t *       vSimsOut; 
+    int               fVerbose; 
+    int               nIns;     
+    int               nDivs;   // divisors (const + inputs + tfi + sidedivs)   
+    int               nNodes;   
+    int               nOuts;    
+    int               nObjs;    
+    int               VarMarks[MAJ_NOBJS][MAJ_NOBJS];
+    int               nCnfVars;
+    int               nCnfClauses;
+    FILE *            pFile;
+    Vec_Int_t *       vFans;
+};
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Exa5_ManMarkup( Exa5_Man_t * p )
+{
+    int i, j, k, nVars[3] = {1 + 3*p->nNodes, 0, p->nNodes*Vec_WrdSize(p->vSimsIn)};
+    assert( p->nObjs <= MAJ_NOBJS );
+    Vec_IntFill( p->vFans, 1 + 3*p->nNodes, 0 );
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    for ( j = 2; j < i; j++ )
+    {
+        p->VarMarks[i][j] = nVars[0] + nVars[1];
+        Vec_IntPush( p->vFans, 0 );
+        for ( k = 1; k < j; k++ )
+            Vec_IntPush( p->vFans, (i << 16) | (j << 8) | k );
+        nVars[1] += j;
+    }
+    assert( Vec_IntSize(p->vFans) == nVars[0] + nVars[1] );
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+        for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
+            p->VarMarks[i][j] = nVars[0] + nVars[1]++;
+    if ( p->fVerbose )
+        printf( "Variables:  Function = %d.  Structure = %d.  Internal = %d.  Total = %d.\n", 
+            nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
+    if ( 0 )
+    {
+        {
+            printf( "   : " );
+            for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+            {
+                printf( "%3d ", i );
+                printf( " " );
+            }
+            printf( " " );
+            for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+            {
+                printf( "%3d ", i );
+                printf( " " );
+            }
+            printf( "\n" );
+        }
+        for ( j = 0; j < 5 + p->nNodes*5 + p->nOuts*5; j++ )
+            printf( "-" );
+        printf( "\n" );
+        for ( j = p->nObjs - 2; j >= 0; j-- )
+        {
+            if ( j > 0 && j <= p->nIns )
+                printf( " %c : ", 'a'+j-1 );
+            else
+                printf( "%2d : ", j );
+            for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+            {
+                printf( "%3d ", p->VarMarks[i][j] );
+                printf( " " );
+            }
+            printf( " " );
+            for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+            {
+                printf( "%3d ", p->VarMarks[i][j] );
+                printf( " " );
+            }
+            printf( "\n" );
+        }
+    }
+    return nVars[0] + nVars[1] + nVars[2];
+}
+Exa5_Man_t * Exa5_ManAlloc( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose )
+{
+    Exa5_Man_t * p = ABC_CALLOC( Exa5_Man_t, 1 );
+    assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
+    p->vSimsIn     = vSimsIn;
+    p->vSimsOut    = vSimsOut;
+    p->fVerbose    = fVerbose;
+    p->nIns        = nIns;  
+    p->nDivs       = nDivs;
+    p->nNodes      = nNodes;
+    p->nOuts       = nOuts; 
+    p->nObjs       = p->nDivs + p->nNodes + p->nOuts;
+    p->vFans       = Vec_IntAlloc( 5000 );
+    p->nCnfVars    = Exa5_ManMarkup( p );
+    return p;
+}
+void Exa5_ManFree( Exa5_Man_t * p )
+{
+    Vec_IntFree( p->vFans );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Exa5_ManAddClause( Exa5_Man_t * p, int * pLits, int nLits )
+{
+    int i, k = 0;
+    for ( i = 0; i < nLits; i++ )
+        if ( pLits[i] == 1 )
+            return 0;
+        else if ( pLits[i] == 0 )
+            continue;
+        else if ( pLits[i] <= 2*p->nCnfVars )
+            pLits[k++] = pLits[i];
+        else assert( 0 );
+    nLits = k;
+    assert( nLits > 0 );
+    if ( p->pFile )
+    {
+        p->nCnfClauses++;
+        for ( i = 0; i < nLits; i++ )
+            fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( p->pFile, "0\n" );
+    }
+    if ( 0 )
+    {
+        for ( i = 0; i < nLits; i++ )
+            fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( stdout, "\n" );
+    }
+    return 1;
+}
+static inline int Exa5_ManAddClause4( Exa5_Man_t * p, int Lit0, int Lit1, int Lit2, int Lit3, int Lit4 )
+{
+    int pLits[5] = { Lit0, Lit1, Lit2, Lit3, Lit4 };
+    return Exa5_ManAddClause( p, pLits, 5 );
+}
+static inline void Exa5_ManAddOneHot( Exa5_Man_t * p, int * pLits, int nLits )
+{
+    int n, m;
+    for ( n = 0;   n < nLits; n++ )
+    for ( m = n+1; m < nLits; m++ )
+        Exa5_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0, 0 );
+}
+static inline void Exa5_ManAddGroup( Exa5_Man_t * p, int iVar, int nVars )
+{
+    int i, pLits[MAJ_NOBJS];
+    assert( nVars+1 <= MAJ_NOBJS );
+    pLits[0] = Abc_Var2Lit( iVar, 1 );
+    for ( i = 1; i <= nVars; i++ )
+        pLits[i] = Abc_Var2Lit( iVar+i, 0 );
+    Exa5_ManAddClause( p, pLits, nVars+1 );
+    Exa5_ManAddOneHot( p, pLits+1, nVars );
+    for ( i = 1; i <= nVars; i++ )
+        Exa5_ManAddClause4( p, Abc_LitNot(pLits[0]), Abc_LitNot(pLits[i]), 0, 0, 0 );
+}
+int Exa5_ManGenStart( Exa5_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
+{
+    Vec_Int_t * vArray = Vec_IntAlloc( 100 );
+    int pLits[MAJ_NOBJS], i, j, k, n, m, nLits, iObj;
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        int iVarStart = 1 + 3*(i - p->nDivs);//
+        nLits = 0;
+        for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][j] )
+            Exa5_ManAddGroup( p, p->VarMarks[i][j], j-1 ), pLits[nLits++] = Abc_Var2Lit(p->VarMarks[i][j], 0);
+        Exa5_ManAddClause( p, pLits, nLits );
+        Exa5_ManAddOneHot( p, pLits, nLits );
+        if ( fOrderNodes )
+        for ( j = p->nDivs; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][m] )
+            Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][n], 1), Abc_Var2Lit(p->VarMarks[j][m], 1), 0, 0, 0 );
+        for ( j = p->nDivs; j < i; j++ ) if ( p->VarMarks[i][j] )
+        {
+            // go through all variables of i that point to j and k
+            for ( n = 1; n < j; n++ )
+            {
+                int iVar   = p->VarMarks[i][j] + n; // variable of i pointing to j
+                int iObj   = Vec_IntEntry( p->vFans, iVar );
+                int iNode0 = (iObj >>  0) & 0xFF;
+                int iNode1 = (iObj >>  8) & 0xFF;
+                int iNode2 = (iObj >> 16) & 0xFF;
+                assert( iObj > 0 );
+                assert( iNode1 == j );
+                assert( iNode2 == i );
+                // go through all variables of j and block those that point to k
+                assert( p->VarMarks[j][2]   > 0 );
+                assert( p->VarMarks[j+1][2] > 0 );
+                for ( m = p->VarMarks[j][2]+1; m < p->VarMarks[j+1][2]; m++ )
+                {
+                    int jObj   = Vec_IntEntry( p->vFans, m );
+                    int jNode0 = (jObj >>  0) & 0xFF;
+                    int jNode1 = (jObj >>  8) & 0xFF;
+                    int jNode2 = (jObj >> 16) & 0xFF;
+                    if ( jObj == 0 )
+                        continue;
+                    assert( jNode2 == j );
+                    if ( iNode0 == jNode0 || iNode0 == jNode1 )
+                        Exa5_ManAddClause4( p, Abc_Var2Lit(iVar, 1), Abc_Var2Lit(m, 1), 0, 0, 0 );
+                }
+            }
+        }
+        for ( k = 0; k < 3; k++ )
+            Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0, 0);
+        if ( fOnlyAnd )
+            Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0, 0);
+    }
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        Vec_IntClear( vArray );
+        Vec_IntForEachEntry( p->vFans, iObj, k )
+            if ( iObj && ((iObj & 0xFF) == i || ((iObj >> 8) & 0xFF) == i) )
+                Vec_IntPush( vArray, Abc_Var2Lit(k, 0) );
+        for ( k = p->nDivs + p->nNodes; k < p->nObjs; k++ ) if ( p->VarMarks[k][i] )
+            Vec_IntPush( vArray, Abc_Var2Lit(p->VarMarks[k][i], 0) );
+        Exa5_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+        if ( fUniqFans )
+            Exa5_ManAddOneHot( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+    }
+    Vec_IntFree( vArray );
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        nLits = 0;
+        for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
+            pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j], 0 );
+        Exa5_ManAddClause( p, pLits, nLits );
+        Exa5_ManAddOneHot( p, pLits, nLits );
+    }
+    return 1;
+}
+void Exa5_ManGenMint( Exa5_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
+{
+    int iNodeVar = p->nCnfVars + p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
+    int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
+    int i, k, n, j, VarVals[MAJ_NOBJS], iNodes[3], iVarStart, iObj;
+    assert( p->nObjs <= MAJ_NOBJS );
+    assert( iMint < Vec_WrdSize(p->vSimsIn) );
+    for ( i = 0; i < p->nDivs; i++ )
+        VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
+    for ( i = 0; i < p->nNodes; i++ )
+        VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + i, 0);
+    for ( i = 0; i < p->nOuts; i++ )
+        VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
+    if ( 0 )
+    {
+        printf( "Adding minterm %d: ", iMint );
+        for ( i = 0; i < p->nObjs; i++ )
+            printf( " %d=%d", i, VarVals[i] );
+        printf( "\n" );
+    }
+    Vec_IntForEachEntry( p->vFans, iObj, i )
+    {
+        if ( iObj == 0 ) continue;
+        iNodes[1] = (iObj >>  0) & 0xFF;
+        iNodes[0] = (iObj >>  8) & 0xFF;
+        iNodes[2] = (iObj >> 16) & 0xFF;
+        iVarStart = 1 + 3*(iNodes[2] - p->nDivs);//
+        for ( k = 0; k < 4; k++ )
+        for ( n = 0; n < 2; n++ )
+            Exa5_ManAddClause4( p, Abc_Var2Lit(i, 1), Abc_LitNotCond(VarVals[iNodes[0]], k&1), Abc_LitNotCond(VarVals[iNodes[1]], k>>1), Abc_LitNotCond(VarVals[iNodes[2]], !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
+        for ( n = 0; n < 2; n++ )
+            Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0, 0);
+    }
+}
+void Exa5_ManGenCnf( Exa5_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
+{
+    int m;
+    assert( p->pFile == NULL );
+    p->pFile = fopen( pFileName, "wb" );
+    fputs( "p cnf                \n", p->pFile );
+    Exa5_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
+    for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
+        Exa5_ManGenMint( p, m, fOnlyAnd, fFancy );
+    rewind( p->pFile );
+    fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses );
+    fclose( p->pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Exa5_ManFindFanin( Exa5_Man_t * p, Vec_Int_t * vValues, int i )
+{
+    int j, Count = 0, iVar = -1;
+    for ( j = 0; j < p->nObjs; j++ )
+        if ( p->VarMarks[i][j] && Vec_IntEntry(vValues, p->VarMarks[i][j]) )
+        {
+            iVar = j;
+            Count++;
+        }
+    assert( Count == 1 );
+    return iVar;
+}
+static inline void Exa5_ManPrintFanin( Exa5_Man_t * p, int iNode, int fComp )
+{
+    if ( iNode == 0 )
+        printf( " %s", fComp ? "const1" : "const0" );
+    else if ( iNode > 0 && iNode <= p->nIns )
+        printf( " %s%c", fComp ? "~" : "", 'a'+iNode-1 );
+    else if ( iNode > p->nIns && iNode < p->nDivs )
+        printf( " %s%c", fComp ? "~" : "", 'A'+iNode-p->nIns-1 );
+    else
+        printf( " %s%d", fComp ? "~" : "", iNode );
+}
+void Exa5_ManPrintSolution( Exa5_Man_t * p, Vec_Int_t * vValues, int fFancy )
+{
+    int Fan0[MAJ_NOBJS] = {0};
+    int Fan1[MAJ_NOBJS] = {0};
+    int Count[MAJ_NOBJS] = {0};
+    int i, k, iObj, iNodes[3];
+    printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
+    Vec_IntForEachEntry( p->vFans, iObj, i )
+    {
+        if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
+            continue;
+        iNodes[0] = (iObj >>  0) & 0xFF;
+        iNodes[1] = (iObj >>  8) & 0xFF;
+        iNodes[2] = (iObj >> 16) & 0xFF;
+        assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
+        Fan0[iNodes[2]] = iNodes[0];
+        Fan1[iNodes[2]] = iNodes[1];
+        Count[iNodes[2]]++;
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        int iVar = Exa5_ManFindFanin( p, vValues, i );
+        printf( "%2d  = ", i );
+        Exa5_ManPrintFanin( p, iVar, 0 );
+        printf( "\n" );
+    }
+    for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
+    {
+        int iVarStart = 1 + 3*(i - p->nDivs);//
+        int Val1 = Vec_IntEntry(vValues, iVarStart);
+        int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+        int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+        assert( Count[i] == 1 );
+        printf( "%2d  = ", i );
+        for ( k = 0; k < 2; k++ )
+        {
+            int iNode = k ? Fan1[i] : Fan0[i];
+            int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
+            Exa5_ManPrintFanin( p, iNode, fComp );
+            if ( k ) break;
+            printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
+        }
+        printf( "\n" );
+    }
+}
+Mini_Aig_t * Exa5_ManMiniAig( Exa5_Man_t * p, Vec_Int_t * vValues )
+{
+    Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
+    int Compl[MAJ_NOBJS] = {0};
+    int Fan0[MAJ_NOBJS]  = {0};
+    int Fan1[MAJ_NOBJS]  = {0};
+    int Count[MAJ_NOBJS] = {0};
+    int i, k, iObj, iNodes[3];
+    Vec_IntForEachEntry( p->vFans, iObj, i )
+    {
+        if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
+            continue;
+        iNodes[0] = (iObj >>  0) & 0xFF;
+        iNodes[1] = (iObj >>  8) & 0xFF;
+        iNodes[2] = (iObj >> 16) & 0xFF;
+        assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
+        Fan0[iNodes[2]] = iNodes[0];
+        Fan1[iNodes[2]] = iNodes[1];
+        Count[iNodes[2]]++;
+    }
+    assert( p->nDivs == Mini_AigNodeNum(pMini) );
+    for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
+    {
+        int iNodes[2] = {0};
+        int iVarStart = 1 + 3*(i - p->nDivs);//
+        int Val1 = Vec_IntEntry(vValues, iVarStart);
+        int Val2 = Vec_IntEntry(vValues, iVarStart+1);
+        int Val3 = Vec_IntEntry(vValues, iVarStart+2);
+        assert( Count[i] == 1 );
+        Compl[i] = Val1 && Val2 && Val3;
+        for ( k = 0; k < 2; k++ )
+        {
+            int iNode = k ? Fan1[i] : Fan0[i];
+            int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
+            iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
+        }
+        if ( Val1 && Val2 ) 
+        {
+            if ( Val3 )
+                Mini_AigOr( pMini, iNodes[0], iNodes[1] );
+            else
+                Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
+        }
+        else
+            Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
+    }
+    for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
+    {
+        int iVar = Exa5_ManFindFanin( p, vValues, i );
+        Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
+    }
+    assert( p->nObjs == Mini_AigNodeNum(pMini) );
+    return pMini;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mini_Aig_t * Exa5_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose )
+{
+    abctime clkTotal = Abc_Clock();
+    Mini_Aig_t * pMini  = NULL;
+    Vec_Int_t * vValues = NULL;
+    char * pFileNameIn  = "_temp_.cnf";
+    char * pFileNameOut = "_temp_out.cnf";
+    Exa5_Man_t * p = Exa5_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
+    Exa_ManIsNormalized( vSimsIn, vSimsOut );
+    Exa5_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
+    if ( fVerbose )
+        printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
+    if ( fVerbose )
+        printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
+    vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
+    if ( vValues ) pMini = Exa5_ManMiniAig( p, vValues );
+    //if ( vValues ) Exa5_ManPrintSolution( p, vValues, fFancy );
+    if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
+    if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
+    Vec_IntFreeP( &vValues );
+    Exa5_ManFree( p );
+    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    return pMini;
+}
+void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars )
+{
+    Mini_Aig_t * pMini = NULL;
+    int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
+    Vec_Wrd_t * vSimsIn  = Vec_WrdStart( nMints );
+    Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
+    word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
+    if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
+    assert( pPars->nVars <= 10 );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
+        for ( i = 0; i < pPars->nVars; i++ )
+            if ( (m >> i) & 1 )
+                Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
+    }
+    assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
+    pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
+    if ( pMini ) Mini_AigStop( pMini );
+    if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
+    Vec_WrdFree( vSimsIn );
+    Vec_WrdFree( vSimsOut );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////