Updates to exact synthesis commands.

4 files changed, 226 insertions, 38 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3467008a..2259d3ff 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8299,7 +8299,7 @@ int Abc_CommandLutExact( 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, "INKaogvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "INKiaogvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8336,6 +8336,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLutSize < 0 )
                 goto usage;
             break;
+        case 'i':
+            pPars->fUseIncr ^= 1;
+            break;
         case 'a':
             pPars->fOnlyAnd ^= 1;
             break;
@@ -8388,11 +8391,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: lutexact [-INK <num>] [-aogvh] <hex>\n" );
+    Abc_Print( -2, "usage: lutexact [-INK <num>] [-iaogvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of I-input function using N K-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 K-input nodes [default = %d]\n", pPars->nNodes );
     Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
+    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 additional optimizations [default = %s]\n", pPars->fFewerVars ? "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" );
@@ -8420,7 +8424,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, "MINKaoegvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MINKiaoegvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8468,6 +8472,9 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLutSize < 0 )
                 goto usage;
             break;
+        case 'i':
+            pPars->fUseIncr ^= 1;
+            break;
         case 'a':
             pPars->fOnlyAnd ^= 1;
             break;
@@ -8499,6 +8506,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nVars = pPars->nMajSupp;
         pPars->nLutSize = 3;
         pPars->fMajority = 1;
+        pPars->fUseIncr = 1;
         if ( pPars->nNodes == 0 )
         {
             if ( pPars->nMajSupp == 5 )
@@ -8549,16 +8557,30 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
         return 1;
     }
+    if ( !pPars->fUseIncr )
+    {
+        if ( pPars->fMajority )
+        {
+            Abc_Print( -1, "Cannot synthesize majority in the non-incremental mode (use \'-i\').\n" );
+            return 1;
+        }
+        if ( pPars->nLutSize > 3 )
+        {
+            Abc_Print( -1, "Cannot synthesize LUT4 and larger in non-incremental mode (use \'-i\').\n" );
+            return 1;
+        }
+    }
     Zyx_ManExactSynthesis( pPars );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: allexact [-MIKN <num>] [-aoevh] <hex>\n" );
+    Abc_Print( -2, "usage: allexact [-MIKN <num>] [-iaoevh] <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 );
     Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
     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-e       : toggle enumerating all solutions [default = %s]\n", pPars->fEnumSols ? "yes" : "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 752bab5b..1d5180f3 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -52,6 +52,7 @@ struct Bmc_EsPar_t_
     int        nLutSize;
     int        nMajSupp;
     int        fMajority;
+    int        fUseIncr;
     int        fOnlyAnd;
     int        fGlucose;
     int        fOrderNodes;
@@ -69,6 +70,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
     pPars->nLutSize    = 2; 
     pPars->nMajSupp    = 0;
     pPars->fMajority   = 0; 
+    pPars->fUseIncr    = 0;
     pPars->fOnlyAnd    = 0; 
     pPars->fGlucose    = 0; 
     pPars->fOrderNodes = 0; 
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 92ff06ee..efa8d857 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -799,14 +799,41 @@ struct Exa3_Man_t_
     int               iVar;      // the next available SAT variable
     word *            pTruth;    // truth table
     Vec_Wrd_t *       vInfo;     // nVars + nNodes + 1
+    Vec_Bit_t *       vUsed2;    // bit masks
+    Vec_Bit_t *       vUsed3;    // bit masks
     int               VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
     Vec_Wec_t *       vOutLits;  // output vars
     bmcg_sat_solver * pSat;      // SAT solver
+    int               nUsed[2];
 };
 
 static inline word *  Exa3_ManTruth( Exa3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
 
+static inline int     Exa3_ManIsUsed2( Exa3_Man_t * p, int m, int n, int i, int j )
+{
+    int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j;
+    p->nUsed[0]++;
+    assert( i < n && j < n && i < j );
+    if ( Vec_BitEntry(p->vUsed2, Pos) )
+        return 1;
+    p->nUsed[1]++;
+    Vec_BitWriteEntry( p->vUsed2, Pos, 1 );
+    return 0;
+}
+
+static inline int     Exa3_ManIsUsed3( Exa3_Man_t * p, int m, int n, int i, int j, int k )
+{
+    int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k;
+    p->nUsed[0]++;
+    assert( i < n && j < n && k < n && i < j && j < k );
+    if ( Vec_BitEntry(p->vUsed3, Pos) )
+        return 1;
+    p->nUsed[1]++;
+    Vec_BitWriteEntry( p->vUsed3, Pos, 1 );
+    return 0;
+}
+
 
 /**Function*************************************************************
 
@@ -882,6 +909,10 @@ static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     p->vOutLits   = Vec_WecStart( p->nObjs );
     p->iVar       = Exa3_ManMarkup( p );
     p->vInfo      = Exa3_ManTruthTables( p );
+    if ( p->pPars->nLutSize == 2 )
+    p->vUsed2     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
+    else if ( p->pPars->nLutSize == 3 )
+    p->vUsed3     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
     p->pSat       = bmcg_sat_solver_start();
     bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
     return p;
@@ -890,6 +921,8 @@ static void Exa3_ManFree( Exa3_Man_t * p )
 {
     bmcg_sat_solver_stop( p->pSat );
     Vec_WrdFree( p->vInfo );
+    Vec_BitFreeP( &p->vUsed2 );
+    Vec_BitFreeP( &p->vUsed3 );
     Vec_WecFree( p->vOutLits );
     ABC_FREE( p );
 }
@@ -1041,18 +1074,21 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
-#ifdef USE_NODE_ORDER
+//#ifdef USE_NODE_ORDER
         // node ordering
-        for ( j = p->nVars; 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] )
+        if ( p->pPars->fUseIncr )
         {
-            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 ) )
-                return 0;
+            for ( j = p->nVars; 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] )
+            {
+                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 ) )
+                    return 0;
+            }
         }
-#endif
+//#endif
         if ( p->nLutSize != 2 )
             continue;
         // two-input functions
@@ -1123,7 +1159,7 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint )
                 continue;
             for ( k = 0; k <= p->LutMask; k++ )
             {
-                int pLits[8], nLits = 0;
+                int pLits[16], nLits = 0;
                 if ( k == 0 && n == 1 )
                     continue;
                 //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1)  );
@@ -1142,6 +1178,69 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint )
     p->iVar += (p->nLutSize+1)*p->nNodes;
     return 1;
 }
+
+static int Exa3_ManAddCnf2( Exa3_Man_t * p, int iMint )
+{
+    int iBaseSatVar = p->iVar + p->nNodes*iMint;
+    // save minterm values
+    int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
+    for ( i = 0; i < p->nVars; i++ )
+        p->VarVals[i] = (iMint >> i) & 1;
+    //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
+    for ( i = p->nVars; i < p->nObjs; i++ )
+    {
+//        int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
+        int iVarStart = 1 + p->LutMask*(i - p->nVars);
+        // collect fanin variables
+        int pFanins[16];
+        for ( j = 0; j < p->nLutSize; j++ )
+            pFanins[j] = Exa3_ManFindFanin(p, i, j);
+        // check cache
+        if ( p->pPars->nLutSize == 2 && Exa3_ManIsUsed2(p, iMint, i, pFanins[1], pFanins[0]) )
+            continue;
+        if ( p->pPars->nLutSize == 3 && Exa3_ManIsUsed3(p, iMint, i, pFanins[2], pFanins[1], pFanins[0]) )
+            continue;
+        // node functionality
+        for ( n = 0; n < 2; n++ )
+        {
+            if ( i == p->nObjs - 1 && n == Value )
+                continue;
+            for ( k = 0; k <= p->LutMask; k++ )
+            {
+                int pLits[16], nLits = 0;
+                if ( k == 0 && n == 1 )
+                    continue;
+                for ( j = 0; j < p->nLutSize; j++ )
+                {
+//                    pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, (k >> j) & 1 );
+                    pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j][pFanins[j]], 1 );
+                    if ( pFanins[j] >= p->nVars )
+                        pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + pFanins[j] - p->nVars, (k >> j) & 1 );
+                    else if ( p->VarVals[pFanins[j]] != ((k >> j) & 1) )
+                        break;
+                }
+                if ( j < p->nLutSize )
+                    continue;
+//                if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, !n );
+                if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + i - p->nVars, !n );
+                if ( k > 0 )             pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1,             n );
+                assert( nLits <= 2*p->nLutSize+2 );
+                if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+                    return 0;
+            }
+        }
+    }
+    return 1;
+}
+void Exa3_ManPrint( Exa3_Man_t * p, int i, int iMint, abctime clk )
+{
+    printf( "Iter%6d : ", i );
+    Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
+    printf( "  Var =%5d  ", bmcg_sat_solver_varnum(p->pSat) );
+    printf( "Cla =%6d  ", bmcg_sat_solver_clausenum(p->pSat) );
+    printf( "Conf =%9d  ", bmcg_sat_solver_conflictnum(p->pSat) );
+    Abc_PrintTime( 1, "Time", clk );
+}
 void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
 {
     int i, status, iMint = 1;
@@ -1155,30 +1254,31 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
     assert( status );
     printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
+    if ( pPars->fUseIncr ) 
+    {
+        bmcg_sat_solver_set_nvars( p->pSat, p->iVar + p->nNodes*(1 << p->nVars) );
+        status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+        assert( status == GLUCOSE_SAT );
+    }
     for ( i = 0; iMint != -1; i++ )
     {
         abctime clk = Abc_Clock();
-        if ( !Exa3_ManAddCnf( p, iMint ) )
+        if ( pPars->fUseIncr ? !Exa3_ManAddCnf2( p, iMint ) : !Exa3_ManAddCnf( p, iMint ) )
             break;
         status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
-        if ( pPars->fVerbose )
-        {
-            printf( "Iter %3d : ", i );
-            Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
-            printf( "  Var =%5d  ", p->iVar );
-            printf( "Cla =%6d  ", bmcg_sat_solver_clausenum(p->pSat) );
-            printf( "Conf =%9d  ", bmcg_sat_solver_conflictnum(p->pSat) );
-            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-        }
+        if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
+            Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
         if ( status == GLUCOSE_UNSAT )
-        {
-            printf( "The problem has no solution.\n" );
             break;
-        }
         iMint = Exa3_ManEval( p );
     }
+    if ( pPars->fVerbose )
+        Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
     if ( iMint == -1 )
         Exa3_ManPrintSolution( p, fCompl );
+    else
+        printf( "The problem has no solution.\n" );
+    printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
     Exa3_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
 }
diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c
index f4949af5..2a3bca07 100644
--- a/src/sat/bmc/bmcMaj3.c
+++ b/src/sat/bmc/bmcMaj3.c
@@ -575,9 +575,11 @@ struct Zyx_Man_t_
 
 static inline word *  Zyx_ManTruth( Zyx_Man_t * p, int v )        { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
 
-static inline int     Zyx_FuncVar( Zyx_Man_t * p, int i, int m )  { return (p->LutMask + 1) * (i - p->pPars->nVars) + m;        }
-static inline int     Zyx_TopoVar( Zyx_Man_t * p, int i, int f )  { return p->TopoBase + p->nObjs * (i - p->pPars->nVars) + f;  }
-static inline int     Zyx_MintVar( Zyx_Man_t * p, int m, int i )  { return p->MintBase + p->nObjs * m + i;                      }
+static inline int     Zyx_FuncVar( Zyx_Man_t * p, int i, int m )  { return (p->LutMask + 1) * (i - p->pPars->nVars) + m;         }
+static inline int     Zyx_TopoVar( Zyx_Man_t * p, int i, int f )  { return p->TopoBase + p->nObjs * (i - p->pPars->nVars) + f;   }
+static inline int     Zyx_MintVar( Zyx_Man_t * p, int m, int i )  { return p->MintBase + p->nObjs * m + i;                       }
+
+//static inline int     Zyx_MintVar2( Zyx_Man_t * p, int m, int i, int f ) { assert(i >= p->pPars->nVars); return p->MintBase + m * p->pPars->nNodes * (p->pPars->nLutSize + 1) + (i - p->pPars->nVars) * (p->pPars->nLutSize + 1) + f; }
 
 static inline int     Zyx_ManIsUsed2( Zyx_Man_t * p, int m, int n, int i, int j )
 {
@@ -801,12 +803,15 @@ Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     p->vVarValues = Vec_IntStartFull( p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
     p->vMidMints  = Vec_IntAlloc( 1 << p->pPars->nVars );
     p->vInfo      = Zyx_ManTruthTables( p, pTruth );
-    if ( p->pPars->nLutSize == 2 || p->pPars->fMajority )
-    p->vUsed2     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
-    else if ( p->pPars->nLutSize == 3 )
-    p->vUsed3     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
     p->vPairs     = Zyx_ManCreateSymVarPairs( p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : pTruth, p->pPars->nVars );
     p->pSat       = bmcg_sat_solver_start();
+    if ( pPars->fUseIncr )
+    {
+        if ( p->pPars->nLutSize == 2 || p->pPars->fMajority )
+            p->vUsed2     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
+        else if ( p->pPars->nLutSize == 3 )
+            p->vUsed3     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
+    }
     bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
     Zyx_ManSetupVars( p );
     Zyx_ManAddCnfStart( p );
@@ -995,9 +1000,8 @@ int Zyx_ManAddCnfBlockSolution( Zyx_Man_t * p )
     Vec_IntFree( vLits );
     return 1;
 }
-int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
+int Zyx_ManAddCnfLazyFunc2( Zyx_Man_t * p, int iMint )
 {
-    int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}};
     int i, k, n, j, s;
     assert( !p->pPars->fMajority || p->pPars->nLutSize == 3 );
     //printf( "Adding functionality clauses for minterm %d.\n", iMint );
@@ -1008,6 +1012,7 @@ int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
         assert( nFanins == p->pPars->nLutSize );
         if ( p->pPars->fMajority )
         {
+            int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}};
             for ( k = 0; k < 3; k++ )
             {
                 if ( Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][Sets[k][0]], p->pFanins[i][Sets[k][1]]) )
@@ -1051,6 +1056,65 @@ int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
     return 1;
 }
 
+int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
+{
+    int i, k, n, j, s, t, u;
+    //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
+    assert( !p->pPars->fMajority && p->pPars->nLutSize < 4 );
+    p->Counts[iMint]++;
+    if ( p->pPars->nLutSize == 2 )
+    {
+        for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+        for ( s = 0;               s < i;        s++ )
+        for ( t = s+1;             t < i;        t++ )
+        {
+            p->pFanins[i][0] = s;
+            p->pFanins[i][1] = t;
+            for ( k = 0; k <= p->LutMask; k++ )
+            for ( n = 0; n < 2; n++ )
+            {
+                p->nLits[0] = 0;
+                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
+                for ( j = 0; j < p->pPars->nLutSize; j++ )
+                {
+                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
+                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
+                }
+                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
+                if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+                    return 0;
+            }
+        }
+    }
+    else if ( p->pPars->nLutSize == 3 )
+    {
+        for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+        for ( s = 0;               s < i;        s++ )
+        for ( t = s+1;             t < i;        t++ )
+        for ( u = t+1;             u < i;        u++ )
+        {
+            p->pFanins[i][0] = s;
+            p->pFanins[i][1] = t;
+            p->pFanins[i][2] = u;
+            for ( k = 0; k <= p->LutMask; k++ )
+            for ( n = 0; n < 2; n++ )
+            {
+                p->nLits[0] = 0;
+                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
+                for ( j = 0; j < p->pPars->nLutSize; j++ )
+                {
+                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
+                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
+                }
+                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
+                if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+                    return 0;
+            }
+        }
+    }
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1251,14 +1315,14 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
             else
                 break;
         }
-        if ( !Zyx_ManAddCnfLazyFunc(p, iMint) )
+        if ( pPars->fUseIncr ? !Zyx_ManAddCnfLazyFunc2(p, iMint) : !Zyx_ManAddCnfLazyFunc(p, iMint) )
         {
             printf( "Became UNSAT after adding constraints for minterm %d\n", iMint );
             status = GLUCOSE_UNSAT;
             break;
         }
         status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
-        if ( pPars->fVerbose && Iter % 100 == 0 )
+        if ( pPars->fVerbose && (!pPars->fUseIncr || Iter % 100 == 0) )
         {
             Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clk );
             clk = Abc_Clock();