Improvements to Boolean matching.

8 files changed, 563 insertions, 88 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b99c1049..db15c678 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15309,7 +15309,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fEnableCheck07 ^= 1;
             break;
         case 'i':
-            pPars->fEnableCheck08 ^= 1;
+            pPars->fUseCofVars ^= 1;
             break;
         case 'k':
             pPars->fUseDsdTune ^= 1;
@@ -15376,7 +15376,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;
     }
 
-    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 )
+    if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 )
     {
         Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
         return 1;
@@ -15391,14 +15391,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pFuncCell = If_CutPerformCheck07;
         pPars->fCutMin = 1;
     }
-    if ( pPars->fEnableCheck08 )
+    if ( pPars->fUseCofVars )
     {
-        if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 )
+        if ( !(pPars->nLutSize & 1) )
         {
-            Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" );
+            Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" );
             return 1;
         }
-        pPars->pFuncCell = If_CutPerformCheck08;
         pPars->fCutMin = 1;
     }
     if ( pPars->fUseDsdTune )
@@ -15610,7 +15609,7 @@ usage:
     Abc_Print( -2, "\t-y       : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
-    Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
+    Abc_Print( -2, "\t-i       : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
     Abc_Print( -2, "\t-n       : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
@@ -30984,7 +30983,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojikfuztncvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojfuikztncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31159,18 +31158,18 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'j':
             pPars->fEnableCheck07 ^= 1;
             break;
-        case 'i':
-            pPars->fEnableCheck08 ^= 1;
-            break;
-        case 'k':
-            pPars->fUseDsdTune ^= 1;
-            break;
         case 'f':
             pPars->fEnableCheck75 ^= 1;
             break;
         case 'u':
             pPars->fEnableCheck75u ^= 1;
             break;
+        case 'i':
+            pPars->fUseCofVars ^= 1;
+            break;
+        case 'k':
+            pPars->fUseDsdTune ^= 1;
+            break;
         case 'z':
             pPars->fDeriveLuts ^= 1;
             break;
@@ -31247,7 +31246,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;
     }
 
-    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
+    if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
     {
         Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
         return 1;
@@ -31262,14 +31261,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pFuncCell = If_CutPerformCheck07;
         pPars->fCutMin = 1;
     }
-    if ( pPars->fEnableCheck08 )
+    if ( pPars->fUseCofVars )
     {
-        if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 )
+        if ( !(pPars->nLutSize & 1) )
         {
-            Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" );
+            Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" );
             return 1;
         }
-        pPars->pFuncCell = If_CutPerformCheck08;
         pPars->fCutMin = 1;
     }
     if ( pPars->fUseDsdTune )
@@ -31439,7 +31437,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojikfuztncvh]\n" );
+    Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojfuikztncvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -31467,9 +31465,9 @@ usage:
     Abc_Print( -2, "\t-y       : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
-    Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
     Abc_Print( -2, "\t-f       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" );
     Abc_Print( -2, "\t-u       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
+    Abc_Print( -2, "\t-i       : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
@@ -32255,7 +32253,7 @@ usage:
     Abc_Print( -2, "\t-L num   : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit );
     Abc_Print( -2, "\t-E num   : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
-    Abc_Print( -2, "\t-M num   : LUT size for the cofactoring (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux );
+    Abc_Print( -2, "\t-M num   : LUT size when cofactoring is performed (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux );
 //    Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
     Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index f6849337..a0180563 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -131,6 +131,7 @@ struct If_Par_t_
     int                fEnableCheck75u;// enable additional checking
     int                fUseDsd;       // compute DSD of the cut functions
     int                fUseDsdTune;   // use matching based on precomputed manager
+    int                fUseCofVars;   // use cofactoring variables
     int                fUseTtPerm;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fDoAverage;    // optimize average rather than maximum level
@@ -242,6 +243,7 @@ struct If_Man_t_
     Vec_Wec_t *        vTtIsops[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD
     Vec_Int_t *        vTtDsds[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into DSD
     Vec_Str_t *        vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations
+    Vec_Str_t *        vTtVars[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into selected vars
     Hash_IntMan_t *    vPairHash;     // hashing pairs of truth tables
     Vec_Int_t *        vPairRes;      // resulting truth table
     Vec_Str_t *        vPairPerms;    // resulting permutation
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index d13d6a49..7b9ad3c1 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -754,7 +754,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
     if ( !pCut->fUseless && 
          (p->pPars->fUseDsd || p->pPars->fUseBat || 
           p->pPars->pLutStruct || p->pPars->fUserRecLib || 
-          p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || 
+          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || 
           p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || 
           p->pPars->fEnableCheck75u) )
     {
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 5525678b..51607066 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -2410,7 +2410,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
     pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
     If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( (i & 0xFF) == 0 )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
         nVars = If_DsdObjSuppSize(pObj);
         if ( nVars <= LutSize )
             continue;
@@ -2574,7 +2575,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
                 }
                 for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ )
                 {
-                    if ( (k & 0x3FF) == 0 )
+                    if ( (k & 0xFF) == 0 )
                         Extra_ProgressBarUpdate( pProgress, k, NULL );
                     pObj  = If_DsdVecObj( &p->vObjs, k );
                     nVars = If_DsdObjSuppSize(pObj);
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 0d66814b..472a1b1e 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -125,6 +125,17 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
         p->vPairRes = Vec_IntAlloc( 1000 );
         Vec_IntPush( p->vPairRes, -1 );
     }
+    if ( pPars->fUseCofVars )
+    {
+        for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
+        {
+            p->vTtVars[v] = Vec_StrAlloc( 1000 );
+            Vec_StrPush( p->vTtVars[v], 0 );
+            Vec_StrPush( p->vTtVars[v], 0 );
+        }
+        for ( v = 0; v < 6; v++ )
+            p->vTtVars[v]  = p->vTtVars[6];
+    }
     if ( pPars->fUseBat )
     {
 //        abctime clk = Abc_Clock();
@@ -209,8 +220,8 @@ void If_ManStop( If_Man_t * p )
     {
         for ( i = 0; i <= 16; i++ )
             if ( p->nCutsUseless[i] )
-                Abc_Print( 1, "Useless cuts %2d  = %9d  (out of %9d)  (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
-        Abc_Print( 1, "Useless cuts all = %9d  (out of %9d)  (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
+                Abc_Print( 1, "Useless cuts %2d  = %9d  (out of %9d)  (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/Abc_MaxInt(p->nCutsCount[i],1) );
+        Abc_Print( 1, "Useless cuts all = %9d  (out of %9d)  (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/Abc_MaxInt(p->nCutsCountAll,1) );
     }
 //    if ( p->pPars->fVerbose && p->nCuts5 )
 //        Abc_Print( 1, "Statistics about 5-cuts: Total = %d  Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
@@ -235,6 +246,8 @@ void If_ManStop( If_Man_t * p )
         Vec_IntFreeP( &p->vTtDsds[i] );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_StrFreeP( &p->vTtPerms[i] );
+    for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
+        Vec_StrFreeP( &p->vTtVars[i] );
     Vec_IntFreeP( &p->vCutData );
     Vec_IntFreeP( &p->vPairRes );
     Vec_StrFreeP( &p->vPairPerms );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 18b1eed2..ae8897e2 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -270,6 +270,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 p->nCutsCountAll++;
                 p->nCutsCount[pCut->nLeaves]++;
             }
+            else if ( p->pPars->fUseCofVars )
+            {
+                extern int Abc_TtCheckCondDepTest( word * pTruth, int nVars, int nSuppLim );
+                int iCofVar = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
+                if ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) || Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId) == (char)-1 )
+                {
+                    while ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) )
+                        Vec_StrPush( p->vTtVars[pCut->nLeaves], (char)-1 );
+                    iCofVar = Abc_TtCheckCondDep( If_CutTruthWR(p, pCut), pCut->nLeaves, p->pPars->nLutSize / 2 );
+                    Vec_StrWriteEntry( p->vTtVars[pCut->nLeaves], truthId, (char)iCofVar );
+                }
+                iCofVar = Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId);
+                assert( iCofVar >= 0 && iCofVar <= (int)pCut->nLeaves );
+                pCut->fUseless = (int)(iCofVar == (int)pCut->nLeaves && pCut->nLeaves > 0);
+                p->nCutsUselessAll += pCut->fUseless;
+                p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
+                p->nCutsCountAll++;
+                p->nCutsCount[pCut->nLeaves]++;
+            }
         }
         
         // compute the application-specific cost and depth
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 7b3adfec..24260c2a 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -37,14 +37,14 @@ ABC_NAMESPACE_IMPL_START
 
 // network types
 typedef enum { 
-    IF_DSD_NONE = 0,               // 0:  unknown
-    IF_DSD_CONST0,                 // 1:  constant
-    IF_DSD_VAR,                    // 2:  variable
-    IF_DSD_AND,                    // 3:  AND
-    IF_DSD_XOR,                    // 4:  XOR
-    IF_DSD_MUX,                    // 5:  MUX
-    IF_DSD_PRIME                   // 6:  PRIME
-} If_DsdType_t;
+    IFN_DSD_NONE = 0,               // 0:  unknown
+    IFN_DSD_CONST0,                 // 1:  constant
+    IFN_DSD_VAR,                    // 2:  variable
+    IFN_DSD_AND,                    // 3:  AND
+    IFN_DSD_XOR,                    // 4:  XOR
+    IFN_DSD_MUX,                    // 5:  MUX
+    IFN_DSD_PRIME                   // 6:  PRIME
+} Ifn_DsdType_t;
 
 // object types
 static char * Ifn_Symbs[16] = { 
@@ -124,7 +124,7 @@ int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
     p->nPars  = p->nObjs;
     for ( i = p->nInps; i < p->nObjs; i++ )
     {
-        if ( p->Nodes[i].Type != IF_DSD_PRIME )
+        if ( p->Nodes[i].Type != IFN_DSD_PRIME )
             continue;
         p->Nodes[i].iFirst = p->nPars;
         p->nPars += (1 << p->Nodes[i].nFanins);
@@ -162,7 +162,7 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
 {
     int i, LutSize = 0;
     for ( i = p->nInps; i < p->nObjs; i++ )
-        if ( p->Nodes[i].Type == IF_DSD_PRIME )
+        if ( p->Nodes[i].Type == IFN_DSD_PRIME )
             LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
     return LutSize;
 }
@@ -182,9 +182,150 @@ int Ifn_NtkInputNum( Ifn_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Ifn_ErrorMessage( const char * format, ...  )
+{
+    char * pMessage;
+    va_list args;
+    va_start( args, format );
+    pMessage = vnsprintf( format, args );
+    va_end( args );
+    printf( "%s", pMessage );
+    ABC_FREE( pMessage );
+    return 0;
+}
+int Inf_ManOpenSymb( char * pStr )
+{
+    if ( pStr[0] == '(' )
+        return 3;
+    if ( pStr[0] == '[' )
+        return 4;
+    if ( pStr[0] == '<' )
+        return 5;
+    if ( pStr[0] == '{' )
+        return 6;
+    return 0;
+}
 int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
 {
-    int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1;
+    int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1, RetValue = 1;
+    for ( i = 0; pStr[i]; i++ )
+    {
+        if ( Inf_ManOpenSymb(pStr+i) )
+            nNodes++;
+        if ( pStr[i] == ';' || 
+             pStr[i] == '(' || pStr[i] == ')' || 
+             pStr[i] == '[' || pStr[i] == ']' || 
+             pStr[i] == '<' || pStr[i] == '>' || 
+             pStr[i] == '{' || pStr[i] == '}' )
+            continue;
+        if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
+            continue;
+        if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
+        {
+            MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') );
+            Marks[pStr[i] - 'a'] = 1;
+            continue;
+        }
+        return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
+    }
+    for ( i = 0; i <= MaxVar; i++ )
+        if ( Marks[i] == 0 )
+            return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
+    *pnInps = MaxVar + 1;
+    *pnObjs = MaxVar + 1 + nNodes;
+    return 1;
+}
+static inline char * Ifn_NtkParseFindClosingParanthesis( char * pStr, char Open, char Close )
+{
+    int Counter = 0;
+    assert( *pStr == Open );
+    for ( ; *pStr; pStr++ )
+    {
+        if ( *pStr == Open )
+            Counter++;
+        if ( *pStr == Close )
+            Counter--;
+        if ( Counter == 0 )
+            return pStr;
+    }
+    return NULL;
+}
+int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode )
+{
+    Ifn_Obj_t * pObj;
+    int nFanins = 0, pFanins[IFN_INS];
+    int Type = Inf_ManOpenSymb( pStr );
+    char * pLim = Ifn_NtkParseFindClosingParanthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
+    *ppFinal = NULL;
+    if ( pLim == NULL )
+        return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
+    while ( pStr < pLim )
+    {
+        assert( nFanins < IFN_INS );
+        if ( pStr[0] >= 'a' && pStr[0] <= 'z' )
+            pFanins[nFanins++] = pStr[0] - 'a', pStr++; 
+        else if ( Inf_ManOpenSymb(pStr) )
+        {
+            if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) )
+                return 0;
+            pFanins[nFanins++] = *piNode - 1;
+        }
+        else
+            return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
+    }
+    assert( pStr == pLim );
+    pObj = p->Nodes + (*piNode)++;
+    pObj->Type = Type;
+    assert( pObj->nFanins == 0 );
+    pObj->nFanins = nFanins;
+    memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins );
+    *ppFinal = pLim + 1;
+    if ( Type == IFN_DSD_MUX && nFanins != 3 )
+        return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" );
+    return 1;
+}
+int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
+{
+    char * pFinal; int iNode;
+    if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
+        return 0;
+    if ( p->nInps > IFN_INS )
+        return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
+    assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
+    if ( !Inf_ManOpenSymb(pStr) )
+        return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" );
+    iNode = p->nInps;
+    if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) )
+        return 0;
+    if ( pFinal[0] && pFinal[0] != ';' )
+        return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" );
+    if ( iNode != p->nObjs )
+        return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ifn_ManStrType2( char * pStr )
+{
+    int i;
+    for ( i = 0; pStr[i]; i++ )
+        if ( pStr[i] == '=' )
+            return 1;
+    return 0;
+}
+int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs )
+{
+    int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
     for ( i = 0; pStr[i]; i++ )
     {
         if ( pStr[i] == '=' || pStr[i] == ';' || 
@@ -201,11 +342,8 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
                 Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
             continue;
         }
-        printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
-        RetValue = 0;
+        return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
     }
-    if ( !RetValue )
-        return 0;
     for ( i = 0; pStr[i]; i++ )
     {
         if ( pStr[i] == '=' || pStr[i] == ';' || 
@@ -222,43 +360,27 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
                 Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
             continue;
         }
-        printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
-        RetValue = 0;
+        return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
     }
-    if ( !RetValue )
-        return 0;
     MaxVar++;
     MaxDef++;
     for ( i = 0; i < MaxDef; i++ )
         if ( Marks[i] == 0 )
-            printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0;
+            return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
     for ( i = 0; i < MaxVar; i++ )
         if ( Marks[i] == 2 )
-            printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
+            return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i );
     for ( i = MaxVar; i < MaxDef; i++ )
         if ( Marks[i] == 1 )
-            printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
-    if ( !RetValue )
-        return 0;
+            return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i );
     *pnInps = MaxVar;
     *pnObjs = MaxDef;
     return 1;
 }
-int Ifn_ErrorMessage( const char * format, ...  )
-{
-    char * pMessage;
-    va_list args;
-    va_start( args, format );
-    pMessage = vnsprintf( format, args );
-    va_end( args );
-    printf( "%s", pMessage );
-    ABC_FREE( pMessage );
-    return 0;
-}
-int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
+int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
 {
     int i, k, n, f, nFans, iFan;
-    if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
+    if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) )
         return 0;
     if ( p->nInps > IFN_INS )
         return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
@@ -270,25 +392,25 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
             if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
                 break;
         if ( pStr[k] == 0 )
-            return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i );
+            return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i );
         if ( pStr[k+2] == '(' )
-            p->Nodes[i].Type = IF_DSD_AND, Next = ')';
+            p->Nodes[i].Type = IFN_DSD_AND, Next = ')';
         else if ( pStr[k+2] == '[' )
-            p->Nodes[i].Type = IF_DSD_XOR, Next = ']';
+            p->Nodes[i].Type = IFN_DSD_XOR, Next = ']';
         else if ( pStr[k+2] == '<' )
-            p->Nodes[i].Type = IF_DSD_MUX, Next = '>';
+            p->Nodes[i].Type = IFN_DSD_MUX, Next = '>';
         else if ( pStr[k+2] == '{' )
-            p->Nodes[i].Type = IF_DSD_PRIME, Next = '}';
+            p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
         else 
-            return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
+            return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
         for ( n = k + 3; pStr[n]; n++ )
             if ( pStr[n] == Next )
                 break;
         if ( pStr[n] == 0 )
-            return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
+            return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
         nFans = n - k - 3;
         if ( nFans < 1 || nFans > 8 )
-            return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
+            return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
         for ( f = 0; f < nFans; f++ )
         {
             iFan = pStr[k + 3 + f] - 'a';
@@ -298,8 +420,11 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
         }
         p->Nodes[i].nFanins = nFans;
     }
-    // truth tables
-    Abc_TtElemInit2( p->pTtElems, p->nInps );
+    return 1;
+}
+void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p )
+{
+    int i, k;
     // parse constraints
     p->nConstr = 0;
     for ( i = 0; i < p->nInps; i++ )
@@ -311,17 +436,265 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
             }
 //    if ( p->nConstr )
 //        printf( "Total constraints = %d\n", p->nConstr );
-    return 1;
 }
+
 Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
 {
     Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
-    if ( Ifn_NtkParseInt( pStr, p ) )
-        return p;
-    ABC_FREE( p );
-    return NULL;
+    if ( Ifn_ManStrType2(pStr) )
+    {
+        if ( !Ifn_NtkParseInt2( pStr, p ) )
+        {
+            ABC_FREE( p );
+            return NULL;
+        }
+    }
+    else
+    {
+        if ( !Ifn_NtkParseInt( pStr, p ) )
+        {
+            ABC_FREE( p );
+            return NULL;
+        }
+    }
+    Ifn_NtkParseConstraints( pStr, p );
+    Abc_TtElemInit2( p->pTtElems, p->nInps );
+    printf( "Finished parsing: " ); Ifn_NtkPrint(p);
+    return p;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derive AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni );
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "model" );
+    Gia_ManHashStart( pNew );
+    for ( i = 0; i < p->nInps; i++ )
+        pVarMap[i] = Gia_ManAppendCi(pNew);
+    for ( i = p->nObjs; i < p->nParsVIni; i++ )
+        pVarMap[i] = Gia_ManAppendCi(pNew);
+    for ( i = p->nInps; i < p->nObjs; i++ )
+    {
+        int Type = p->Nodes[i].Type;
+        int nFans = p->Nodes[i].nFanins;
+        int * pFans = p->Nodes[i].Fanins;
+        int iFanin = p->Nodes[i].iFirst;
+        if ( Type == IFN_DSD_AND )
+        {
+            iLit = 1;
+            for ( k = 0; k < nFans; k++ )
+                iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
+            pVarMap[i] = iLit;
+        }
+        else if ( Type == IFN_DSD_XOR )
+        {
+            iLit = 0;
+            for ( k = 0; k < nFans; k++ )
+                iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
+            pVarMap[i] = iLit;
+        }
+        else if ( Type == IFN_DSD_MUX )
+        {
+            assert( nFans == 3 );
+            pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
+        }
+        else if ( Type == IFN_DSD_PRIME )
+        {
+            int n, Step, pVarsData[256];
+            int nMints = (1 << nFans);
+            assert( nFans >= 1 && nFans <= 8 );
+            for ( k = 0; k < nMints; k++ )
+                pVarsData[k] = pVarMap[iFanin + k];
+            for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
+                for ( n = 0; n < nMints; n += Step << 1 )
+                    pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] );
+            assert( Step == nMints );
+            pVarMap[i] = pVarsData[0];
+        }
+        else assert( 0 );
+    }
+    Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] );
+    ABC_FREE( pVarMap );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) );
+    assert( Gia_ManPoNum(pNew) == 1 );
+    return pNew;
+}
+// compute cofactors w.r.t. the first nIns variables
+Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp; 
+    Gia_Obj_t * pObj;
+    int i, m, nMints = nIns;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        if ( i >= nIns )
+            pObj->Value = Gia_ManAppendCi( pNew );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Gia_ManForEachCi( p, pObj, i )
+            if ( i < nIns )
+                pObj->Value = ((m >> i) & 1);
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachPo( p, pObj, i )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
+{
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    pAig->nRegs = 0;
+    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
+    Aig_ManStop( pAig );
+    return pCnf;
+}
+sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
+{
+    sat_solver * pSat;
+    Gia_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    int i;    
+    pCnf = Cnf_DeriveGiaRemapped( p );
+    // start the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    // add timeframe clauses
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
+    // inputs/outputs
+    *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
+    Gia_ManForEachCi( p, pObj, i )
+        Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
+    *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
+    Cnf_DataFree( pCnf );
+    return pSat;
+}
+sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
+{
+    Gia_Man_t * p1, * p2;
+    sat_solver * pSat = NULL;
+    *pvPiVars = *pvPoVars = NULL;
+    p1 = Ifn_ManStrFindModel( p );
+//    Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
+    p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
+    Gia_ManStop( p1 );
+//    Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
+    pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
+    Gia_ManStop( p2 );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        printf( "%c", 'a' + pPerms[i] );
+    printf( "\n" );
+}
+int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits )
+{
+    int v, Value, m, mNew, nMints = (1 << nVars);
+    assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) );
+    assert( nVars <= nVarsAll );
+    // remap minterms
+    Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
+    for ( m = 0; m < nMints; m++ )
+    {
+        mNew = 0;
+        for ( v = 0; v < nVarsAll; v++ )
+        {
+            assert( pPerm[v] < nVars );
+            if ( ((m >> pPerm[v]) & 1) )
+                mNew |= (1 << v);
+        }
+        assert( Vec_IntEntry(vLits, mNew) == -1 );
+        Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
+    }
+    // find assumptions
+    v = 0;
+    Vec_IntForEachEntry( vLits, Value, m )
+        if ( Value >= 0 )
+            Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
+    Vec_IntShrink( vLits, v );
+    // run SAT solver
+    Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+    return (int)(Value == l_True);
+}
+void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
+{
+    int i, iVar;
+    Vec_IntClear( vValues );
+    Vec_IntForEachEntry( vPiVars, iVar, i )
+        Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
+}
+int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, Vec_Int_t * vValues )
+{
+    // extract permutation
+    int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
+    for ( i = 0; i < Vec_IntSize(vPiVars); i++ )
+    {
+        pPerm[i] = Abc_TtGetHex( &Perm, i );
+        assert( pPerm[i] < nVars );
+    }
+    // perform SAT check 
+    RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, Vec_IntSize(vPiVars), vValues );
+    Vec_IntClear( vValues );
+    if ( RetValue == 0 )
+        return 0;
+    Ifn_ManSatDeriveOne( pSat, vPiVars, vValues );
+    return 1;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Derive truth table given the configulation values.]
@@ -353,24 +726,24 @@ word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
         int nFans = p->Nodes[i].nFanins;
         int * pFans = p->Nodes[i].Fanins;
         word * pTruth = Ifn_ObjTruth( p, i );
-        if ( p->Nodes[i].Type == IF_DSD_AND )
+        if ( p->Nodes[i].Type == IFN_DSD_AND )
         {
             Abc_TtFill( pTruth, p->nWords );
             for ( f = 0; f < nFans; f++ )
                 Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
         }
-        else if ( p->Nodes[i].Type == IF_DSD_XOR )
+        else if ( p->Nodes[i].Type == IFN_DSD_XOR )
         {
             Abc_TtClear( pTruth, p->nWords );
             for ( f = 0; f < nFans; f++ )
                 Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
         }
-        else if ( p->Nodes[i].Type == IF_DSD_MUX )
+        else if ( p->Nodes[i].Type == IFN_DSD_MUX )
         {
             assert( nFans == 3 );
             Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
         }
-        else if ( p->Nodes[i].Type == IF_DSD_PRIME )
+        else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
         {
             int nValues = (1 << nFans);
             word * pTemp = Ifn_ObjTruth(p, p->nObjs);
@@ -573,7 +946,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
     {
         int nFans = p->Nodes[i].nFanins;
         int * pFans = p->Nodes[i].Fanins;
-        if ( p->Nodes[i].Type == IF_DSD_AND )
+        if ( p->Nodes[i].Type == IFN_DSD_AND )
         {
             nLits = 0;
             pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
@@ -590,7 +963,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
             if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
                 return 0;
         }
-        else if ( p->Nodes[i].Type == IF_DSD_XOR )
+        else if ( p->Nodes[i].Type == IFN_DSD_XOR )
         {
             int m, nMints = (1 << (nFans+1));
             for ( m = 0; m < nMints; m++ )
@@ -609,7 +982,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
                     return 0;
             }
         }
-        else if ( p->Nodes[i].Type == IF_DSD_MUX )
+        else if ( p->Nodes[i].Type == IFN_DSD_MUX )
         {
             pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
             pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
@@ -635,7 +1008,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
             if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
                 return 0;
         }
-        else if ( p->Nodes[i].Type == IF_DSD_PRIME )
+        else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
         {
             int nValues = (1 << nFans);
             int iParStart = p->Nodes[i].iFirst;
@@ -704,7 +1077,7 @@ void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
     for ( v = p->nObjs; v < p->nPars; v++ )
     {
         for ( i = p->nInps; i < p->nObjs; i++ )
-            if ( p->Nodes[i].Type == IF_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
+            if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
                 break;
         if ( i < p->nObjs )
             printf( " " );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 98883748..fbabdbe8 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1011,6 +1011,75 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
     return Supp;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks if there is a var whose both cofs have supp <= nSuppLim.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim )
+{
+    int v, d, nWords = Abc_TtWordNum(nVars);
+    if ( nVars <= nSuppLim + 1 )
+        return 0;
+    for ( v = 0; v < nVars; v++ )
+    {
+        int nDep0 = 0, nDep1 = 0;
+        for ( d = 0; d < nVars; d++ )
+        {
+            if ( v == d )
+                continue;
+            if ( v < d )
+            {
+                nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 );
+                nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 );
+            }
+            else // if ( v > d )
+            {
+                nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 );
+                nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 );
+            }
+            if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
+                break;
+        }
+        if ( d == nVars )
+            return v;
+    }
+    return nVars;
+}
+static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
+{
+    int nVarsMax = 12;
+    word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
+    int v, d, nWords = Abc_TtWordNum(nVars);
+    assert( nVars <= nVarsMax );
+    if ( nVars <= nSuppLim + 1 )
+        return 0;
+    for ( v = 0; v < nVars; v++ )
+    {
+        int nDep0 = 0, nDep1 = 0;
+        Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
+        Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
+        for ( d = 0; d < nVars; d++ )
+        {
+            if ( v == d )
+                continue;
+            nDep0 += Abc_TtHasVar( Cof0, nVars, d );
+            nDep1 += Abc_TtHasVar( Cof1, nVars, d );
+            if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
+                break;
+        }
+        if ( d == nVars )
+            return v;
+    }
+    return nVars;
+}
+
 
 /**Function*************************************************************