Adding new mapping feature.

4 files changed, 56 insertions, 18 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index d77ac536..6a47a52b 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -133,6 +133,7 @@ struct If_Par_t_
     int                fUseDsd;       // compute DSD of the cut functions
     int                fUseDsdTune;   // use matching based on precomputed manager
     int                fUseCofVars;   // use cofactoring variables
+    int                fUseAndVars;   // use bi-decomposition
     int                fUseTtPerm;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fDoAverage;    // optimize average rather than maximum level
@@ -245,6 +246,7 @@ struct If_Man_t_
     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
+    Vec_Int_t *        vTtDecs[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into decomposition pattern
     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 7b9ad3c1..adf00740 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -754,9 +754,8 @@ 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->fUseCofVars || 
-          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || 
-          p->pPars->fEnableCheck75u) )
+          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || 
+          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
         if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 472a1b1e..80d1f429 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -136,6 +136,17 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
         for ( v = 0; v < 6; v++ )
             p->vTtVars[v]  = p->vTtVars[6];
     }
+    if ( pPars->fUseAndVars )
+    {
+        for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
+        {
+            p->vTtDecs[v] = Vec_IntAlloc( 1000 );
+            Vec_IntPush( p->vTtDecs[v], 0 );
+            Vec_IntPush( p->vTtDecs[v], 0 );
+        }
+        for ( v = 0; v < 6; v++ )
+            p->vTtDecs[v]  = p->vTtDecs[6];
+    }
     if ( pPars->fUseBat )
     {
 //        abctime clk = Abc_Clock();
@@ -248,6 +259,8 @@ void If_ManStop( If_Man_t * p )
         Vec_StrFreeP( &p->vTtPerms[i] );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_StrFreeP( &p->vTtVars[i] );
+    for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
+        Vec_IntFreeP( &p->vTtDecs[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 e192c90e..32e3ce15 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -99,7 +99,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_Cut_t * pCut0R, * pCut1R;
     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->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->pLutStruct != NULL;
+    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->pLutStruct != NULL;
     assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
 
@@ -270,23 +270,47 @@ 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 )
+            else 
             {
-                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 )
+                if ( p->pPars->fUseAndVars )
                 {
-                    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 );
+                    int iDecMask = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
+                    if ( truthId >= Vec_IntSize(p->vTtDecs[pCut->nLeaves]) || Vec_IntEntry(p->vTtDecs[pCut->nLeaves], truthId) == -1 )
+                    {
+                        while ( truthId >= Vec_IntSize(p->vTtDecs[pCut->nLeaves]) )
+                            Vec_IntPush( p->vTtDecs[pCut->nLeaves], -1 );
+                        if ( (int)pCut->nLeaves > p->pPars->nLutSize / 2 )
+                            iDecMask = Abc_TtProcessBiDec( If_CutTruthW(p, pCut), (int)pCut->nLeaves, p->pPars->nLutSize / 2 );
+                        else
+                            iDecMask = 0;
+                        Vec_IntWriteEntry( p->vTtDecs[pCut->nLeaves], truthId, iDecMask );
+                    }
+                    iDecMask = Vec_IntEntry(p->vTtDecs[pCut->nLeaves], truthId);
+                    assert( iDecMask >= 0 );
+                    pCut->fUseless = (int)(iDecMask == 0 && (int)pCut->nLeaves > p->pPars->nLutSize / 2);
+                    p->nCutsUselessAll += pCut->fUseless;
+                    p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
+                    p->nCutsCountAll++;
+                    p->nCutsCount[pCut->nLeaves]++;
+                }
+                if ( p->pPars->fUseCofVars && (!p->pPars->fUseAndVars || pCut->fUseless) )
+                {
+                    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]++;
                 }
-                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]++;
             }
         }