Version abc60407

10 files changed, 1163 insertions, 70 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 0a1cd41a..c2142c4f 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -59,8 +59,10 @@ struct Cut_ParamsStruct_t_
     int                fFilter;           // filter dominated cuts
     int                fSeq;              // compute sequential cuts
     int                fDrop;             // drop cuts on the fly
-    int                fMulti;            // compute factor-cuts
+    int                fDag;              // compute only DAG cuts
+    int                fTree;             // compute only tree cuts
     int                fRecord;           // record the cut computation flow
+    int                fFancy;            // perform fancy computations
     int                fVerbose;          // the verbosiness flag
 };
 
@@ -117,8 +119,9 @@ extern void             Cut_ManPrintStats( Cut_Man_t * p );
 extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
+extern void             Cut_ManIncrementDagNodes( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); 
+extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
 extern Cut_Cut_t *      Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
 /*=== cutSeq.c ==========================================================*/
@@ -135,7 +138,13 @@ extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
 extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
 extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 /*=== cutTruth.c ==========================================================*/
-extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
+extern void             Cut_TruthNCanonicize( Cut_Cut_t * pCut );
+/*=== cutPre22.c ==========================================================*/
+extern void             Cut_CellPrecompute();
+extern void             Cut_CellLoad();
+extern int              Cut_CellIsRunning();
+extern void             Cut_CellDumpToFile();
+extern int              Cut_CellTruthLookup( unsigned * pTruth, int nVars );
 
 #ifdef __cplusplus
 }
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 375d2213..c6246ad7 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -65,13 +65,13 @@ struct Cut_ManStruct_t_
     Cut_Cut_t *        pStore1[2];
     Cut_Cut_t *        pCompareOld;
     Cut_Cut_t *        pCompareNew;
+    unsigned *         puTemp[4];
     // record of the cut computation
     Vec_Int_t *        vNodeCuts;        // the number of cuts for each node
     Vec_Int_t *        vNodeStarts;      // the number of the starting cut of each node
     Vec_Int_t *        vCutPairs;        // the pairs of parent cuts for each cut
     // statistics
     int                nCutsCur;
-    int                nCutsMulti;
     int                nCutsAlloc;
     int                nCutsDealloc;
     int                nCutsPeak;
@@ -79,8 +79,8 @@ struct Cut_ManStruct_t_
     int                nCutsFilter;
     int                nCutsLimit;
     int                nNodes;
-    int                nNodesMulti;
-    int                nNodesMulti0;
+    int                nNodesDag;
+    int                nNodesNoCuts;
     // runtime
     int                timeMerge;
     int                timeUnion;
@@ -130,7 +130,7 @@ extern void                Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut
 /*=== cutMerge.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
 /*=== cutNode.c ==========================================================*/
-extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv ); 
+extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv, int TreeCode ); 
 extern int                 Cut_CutListVerify( Cut_Cut_t * pList );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
@@ -139,7 +139,8 @@ extern int                 Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t
 extern void                Cut_TableClear( Cut_HashTable_t * pTable );
 extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
-extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern void                Cut_TruthComputeOld( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern void                Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
 #endif
 
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 8269da06..0cd01bc9 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -61,22 +61,30 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
         Vec_PtrFill( p->vCutsOld, pParams->nIdsMax, NULL );
         p->vCutsTemp = Vec_PtrAlloc( pParams->nCutSet );
         Vec_PtrFill( p->vCutsTemp, pParams->nCutSet, NULL );
+        if ( pParams->fTruth && pParams->nVarsMax > 5 )
+        {
+            pParams->fTruth = 0;
+            printf( "Skipping computation of truth tables for sequential cuts with more than 5 inputs.\n" );
+        }
     }
-    assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
     p->EntrySize = sizeof(Cut_Cut_t) + pParams->nVarsMax * sizeof(int);
     if ( pParams->fTruth )
     {
-        if ( pParams->nVarsMax > 8 )
+        if ( pParams->nVarsMax > 14 )
         {
             pParams->fTruth = 0;
-            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+            printf( "Skipping computation of truth table for more than %d inputs.\n", 14 );
         }
         else
         {
             p->nTruthWords = Cut_TruthWords( pParams->nVarsMax );
             p->EntrySize += p->nTruthWords * sizeof(unsigned);
         }
+        p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+        p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
+        p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
+        p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
     }
     // enable cut computation recording
     if ( pParams->fRecord )
@@ -120,6 +128,7 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
     if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+    if ( p->puTemp[0] )   free( p->puTemp[0] );
 
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
@@ -153,15 +162,10 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
-    if ( p->pParams->fMulti )
-    {
-    printf( "Factor-cut computation statistics:\n" );
     printf( "Total nodes       = %8d.\n", p->nNodes );
-    printf( "Factor nodes      = %8d.\n", p->nNodesMulti );
-    printf( "Factor nodes 0    = %8d.\n", p->nNodesMulti0 );
-    printf( "Factor cuts       = %8d.\n", p->nCutsMulti );
-    printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsMulti))/(p->nNodesMulti-p->nNodesMulti0) );
-    }
+    printf( "DAG nodes         = %8d.\n", p->nNodesDag );
+    printf( "Tree nodes        = %8d.\n", p->nNodes - p->nNodesDag );
+    printf( "Nodes w/o cuts    = %8d.\n", p->nNodesNoCuts );
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
@@ -229,6 +233,22 @@ int Cut_ManReadVarsMax( Cut_Man_t * p )
     return p->pParams->nVarsMax;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManIncrementDagNodes( Cut_Man_t * p )
+{
+    p->nNodesDag++;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index cace83bd..b651dac9 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -277,7 +277,7 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
     }
     // compute the truth table
     if ( p->pParams->fTruth )
-        Cut_TruthCompute( pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
+        Cut_TruthCompute( p, pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
     // add to the list
     Cut_ListAdd( pSuperList, pCut );
     // return status (0 if okay; 1 if exceeded the limit)
@@ -295,7 +295,7 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv )
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode )
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pCut;
@@ -312,7 +312,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     // compute the cuts
 clk = clock();
     Cut_ListStart( pSuper );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv, TreeCode );
     pList = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
     // verify the result of cut computation
@@ -351,9 +351,9 @@ p->timeMerge += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv )
+void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv, int TreeCode )
 {
-    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1;
+    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1, * pStore0, * pStore1;
     int i, nCutsOld, Limit;
     // start with the elementary cut
     if ( fTriv ) 
@@ -375,6 +375,19 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // set temporary variables
     p->fCompl0 = fCompl0;
     p->fCompl1 = fCompl1;
+    // if tree cuts are computed, make sure only the unit cuts propagate over the DAG nodes
+    if ( TreeCode & 1 )
+    {
+        assert( pList0->nLeaves == 1 );
+        pStore0 = pList0->pNext;
+        pList0->pNext = NULL;
+    }
+    if ( TreeCode & 2 )
+    {
+        assert( pList1->nLeaves == 1 );
+        pStore1 = pList1->pNext;
+        pList1->pNext = NULL;
+    }
     // find the point in the list where the max-var cuts begin
     Cut_ListForEachCut( pList0, pStop0 )
         if ( pStop0->nLeaves == (unsigned)Limit )
@@ -386,8 +399,10 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
+    {
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
+    }
     // small by large
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
@@ -395,7 +410,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     }
     // small by large
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -404,7 +419,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
@@ -419,15 +434,15 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( i < Limit )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     } 
-    if ( fTriv ) 
-    {
-        p->nCutsMulti += p->nCutsCur - nCutsOld;         
-        p->nNodesMulti++;
-        if ( p->nCutsCur == nCutsOld )
-            p->nNodesMulti0++;
-    }
+    if ( p->nNodeCuts == 0 )
+        p->nNodesNoCuts++;
+Quits:
+    if ( TreeCode & 1 )
+        pList0->pNext = pStore0;
+    if ( TreeCode & 2 )
+        pList1->pNext = pStore1;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index cad0069a..8e1ad3da 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -366,7 +366,7 @@ Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int No
         ppTail = &pCut->pNext;
         // compute the truth table
         if ( p->pParams->fTruth )
-            Cut_TruthCompute( pCut, pCut0, pCut1, fCompl0, fCompl1 );
+            Cut_TruthComputeOld( pCut, pCut0, pCut1, fCompl0, fCompl1 );
     }
     *ppTail = NULL;
 
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
new file mode 100644
index 00000000..dd52b694
--- /dev/null
+++ b/src/opt/cut/cutPre22.c
@@ -0,0 +1,983 @@
+/**CFile****************************************************************
+
+  FileName    [cutPre22.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Precomputes truth tables for the 2x2 macro cell.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutPre22.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define CUT_CELL_MVAR  9
+
+typedef struct Cut_Cell_t_ Cut_Cell_t;
+typedef struct Cut_CMan_t_ Cut_CMan_t;
+
+struct Cut_Cell_t_
+{
+    Cut_Cell_t *       pNext;                        // pointer to the next cell in the table
+    Cut_Cell_t *       pNextVar;                     // pointer to the next cell of this support size
+    Cut_Cell_t *       pParent;                      // pointer to the cell used to derive this one
+    int                nUsed;                        // the number of times the cell is used
+    char               Box[4];                       // functions in the boxes
+    unsigned           nVars          :  4;          // the number of variables
+    unsigned           CrossBar0      :  4;          // the variable set equal
+    unsigned           CrossBar1      :  4;          // the variable set equal
+    unsigned           CrossBarPhase  :  2;          // the phase of the cross bar (0, 1, or 2)
+    unsigned           CanonPhase     : 18;          // the canonical phase
+    char               CanonPerm[CUT_CELL_MVAR+3];   // semicanonical permutation
+    short              Store[2*CUT_CELL_MVAR];       // minterm counts in the cofactors
+    unsigned           uTruth[1<<(CUT_CELL_MVAR-5)]; // the current truth table
+};
+
+struct Cut_CMan_t_
+{
+    // storage for canonical cells
+    Extra_MmFixed_t *  pMem;
+    st_table *         tTable;
+    Cut_Cell_t *       pSameVar[CUT_CELL_MVAR+1];
+    // elementary truth tables
+    unsigned           uInputs[CUT_CELL_MVAR][1<<(CUT_CELL_MVAR-5)];
+    // temporary truth tables
+    unsigned           uTemp1[22][1<<(CUT_CELL_MVAR-5)];
+    unsigned           uTemp2[22][1<<(CUT_CELL_MVAR-5)];
+    unsigned           uTemp3[22][1<<(CUT_CELL_MVAR-5)];
+    unsigned           uFinal[1<<(CUT_CELL_MVAR-5)];
+    unsigned           puAux[1<<(CUT_CELL_MVAR-5)];
+    // statistical variables
+    int                nTotal;
+    int                nGood;
+    int                nVarCounts[CUT_CELL_MVAR+1];
+    int                nSymGroups[CUT_CELL_MVAR+1];
+    int                nSymGroupsE[CUT_CELL_MVAR+1];
+    int                timeCanon;
+    int                timeSupp;
+    int                timeTable;
+    int                nCellFound;
+    int                nCellNotFound;
+};
+
+// NP-classes of functions of 3 variables (22)
+static char * s_NP3[22] = {
+    " 0\n",                          // 00    const 0            // 0 vars 
+    " 1\n",                          // 01    const 1            // 0 vars  
+    "1 1\n",                         // 02    a                  // 1 vars  
+    "11 1\n",                        // 03    ab                 // 2 vars  
+    "11 0\n",                        // 04    (ab)'              // 2 vars  
+    "10 1\n01 1\n",                  // 05    a<+>b              // 2 vars  
+    "111 1\n",                       // 06 0s abc                // 3 vars  
+    "111 0\n",                       // 07    (abc)'             // 
+    "11- 1\n1-1 1\n",                // 08 1p a(b+c)             // 
+    "11- 0\n1-1 0\n",                // 09    (a(b+c))'          // 
+    "111 1\n100 1\n010 1\n001 1\n",  // 10 2s a<+>b<+>c          // 
+    "10- 0\n1-0 0\n011 0\n",         // 11 3p a<+>bc             // 
+    "101 1\n110 1\n",                // 12 4p a(b<+>c)           // 
+    "101 0\n110 0\n",                // 13    (a(b<+>c))'        // 
+    "11- 1\n1-1 1\n-11 1\n",         // 14 5s ab+bc+ac           // 
+    "111 1\n000 1\n",                // 15 6s abc+a'b'c'         // 
+    "111 0\n000 0\n",                // 16    (abc+a'b'c')'      // 
+    "11- 1\n-11 1\n0-1 1\n",         // 17 7  ab+bc+a'c          // 
+    "011 1\n101 1\n110 1\n",         // 18 8s a'bc+ab'c+abc'     // 
+    "011 0\n101 0\n110 0\n",         // 19    (a'bc+ab'c+abc')'  // 
+    "100 1\n-11 1\n",                // 20 9p ab'c'+bc           // 
+    "100 0\n-11 0\n"                 // 21    (ab'c'+bc)'        // 
+};
+
+// NP-classes of functions of 3 variables (22)
+static char * s_NP3Names[22] = {
+    "   const 0            ",
+    "   const 1            ",
+    "   a                  ",
+    "   ab                 ",
+    "   (ab)'              ",
+    "   a<+>b              ",
+    "0s abc                ",
+    "   (abc)'             ",
+    "1p a(b+c)             ",
+    "   (a(b+c))'          ",
+    "2s a<+>b<+>c          ",
+    "3p a<+>bc             ",
+    "4p a(b<+>c)           ",
+    "   (a(b<+>c))'        ",
+    "5s ab+bc+ac           ",
+    "6s abc+a'b'c'         ",
+    "   (abc+a'b'c')'      ",
+    "7  ab+bc+a'c          ",
+    "8s a'bc+ab'c+abc'     ",
+    "   (a'bc+ab'c+abc')'  ",
+    "9p ab'c'+bc           ",
+    "   (ab'c'+bc)'        "
+};
+
+// the number of variables in each function
+static int s_NP3VarNums[22] = { 0, 0, 1, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };
+
+// NPN classes of functions of exactly 3 inputs (10)
+static int s_NPNe3[10] = { 6, 8, 10, 11, 12, 14, 15, 17, 18, 20 };
+
+// NPN classes of functions of exactly 3 inputs that are symmetric (5)
+static int s_NPNe3s[10] = { 6, 10, 14, 15, 18 };
+
+// NPN classes of functions of exactly 3 inputs (4)
+static int s_NPNe3p[10] = { 8, 11, 12, 20 };
+
+static Cut_CMan_t * Cut_CManStart();
+static void Cut_CManStop( Cut_CMan_t * p );
+static void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type );
+static void Cut_CellCanonicize( Cut_CMan_t * p, Cut_Cell_t * pCell );
+static int  Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell );
+static void Cut_CellSuppMin( Cut_Cell_t * pCell );
+static void Cut_CellCrossBar( Cut_Cell_t * pCell );
+
+
+static Cut_CMan_t * s_pCMan = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the precomputation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellLoad()
+{
+    FILE * pFile;
+    char * pFileName = "cells22_daomap_iwls.txt";
+    char pString[1000];
+    Cut_CMan_t * p;
+    Cut_Cell_t * pCell;
+    int Length; //, i;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", pFileName );
+        return;
+    }
+   // start the manager
+    p = Cut_CManStart();
+    // load truth tables
+    while ( fgets(pString, 1000, pFile) )
+    {
+        Length = strlen(pString);
+        pString[Length--] = 0;
+        if ( Length == 0 )
+            continue;
+        // derive the cell
+        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+        memset( pCell, 0, sizeof(Cut_Cell_t) );
+        pCell->nVars = Extra_Base2Log(Length*4);
+        pCell->nUsed = 1;
+//        Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
+        Extra_ReadHexadecimal( pCell->uTruth, pString, pCell->nVars );
+        Cut_CellSuppMin( pCell );
+/*
+        // set the elementary permutation
+        for ( i = 0; i < (int)pCell->nVars; i++ )
+            pCell->CanonPerm[i] = i;
+        // canonicize
+        pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+*/
+        // add to the table
+        p->nTotal++;
+        if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
+            p->nGood++;
+    }
+    printf( "Read %d cells from file \"%s\". Added %d cells to the table.\n", p->nTotal, pFileName, p->nGood );
+    fclose( pFile );
+//    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Precomputes truth tables for the 2x2 macro cell.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellPrecompute()
+{
+    Cut_CMan_t * p;
+    Cut_Cell_t * pCell, * pTemp;
+    int i1, i2, i3, i, j, k, c, clk = clock(), clk2 = clock();
+
+    p = Cut_CManStart();
+
+    // precompute truth tables
+    for ( i = 0; i < 22; i++ )
+        Cut_CellTruthElem( p->uInputs[0], p->uInputs[1], p->uInputs[2], p->uTemp1[i], 9, i );
+    for ( i = 0; i < 22; i++ )
+        Cut_CellTruthElem( p->uInputs[3], p->uInputs[4], p->uInputs[5], p->uTemp2[i], 9, i );
+    for ( i = 0; i < 22; i++ )
+        Cut_CellTruthElem( p->uInputs[6], p->uInputs[7], p->uInputs[8], p->uTemp3[i], 9, i );
+/*
+        if ( k == 8 && ((i1 == 6 && i2 == 14 && i3 == 20) || (i1 == 20 && i2 == 6 && i3 == 14)) )
+        {
+            Extra_PrintBinary( stdout, &pCell->CanonPhase, pCell->nVars+1 ); printf( " : " );
+            for ( i = 0; i < pCell->nVars; i++ )
+                printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+            Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars );
+            printf( "\n" );
+        }
+*/
+/*
+    // go through symmetric roots
+    for ( k = 0; k < 5; k++ )
+    for ( i1 =  0; i1 < 22; i1++ )
+    for ( i2 = i1; i2 < 22; i2++ )
+    for ( i3 = i2; i3 < 22; i3++ )
+    {
+        // derive the cell
+        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+        memset( pCell, 0, sizeof(Cut_Cell_t) );
+        pCell->nVars  = 9;
+        pCell->Box[0] = s_NPNe3s[k];
+        pCell->Box[1] = i1;
+        pCell->Box[2] = i2;
+        pCell->Box[3] = i3;
+        // fill in the truth table
+        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3s[k] );
+        // canonicize
+        Cut_CellCanonicize( pCell );
+
+        // add to the table
+        p->nTotal++;
+        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+        else
+            p->nGood++;
+    }
+
+    // go through partially symmetric roots
+    for ( k = 0; k < 4; k++ )
+    for ( i1 = 0;  i1 < 22; i1++ )
+    for ( i2 = 0;  i2 < 22; i2++ )
+    for ( i3 = i2; i3 < 22; i3++ )
+    {
+        // derive the cell
+        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+        memset( pCell, 0, sizeof(Cut_Cell_t) );
+        pCell->nVars  = 9;
+        pCell->Box[0] = s_NPNe3p[k];
+        pCell->Box[1] = i1;
+        pCell->Box[2] = i2;
+        pCell->Box[3] = i3;
+        // fill in the truth table
+        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3p[k] );
+        // canonicize
+        Cut_CellCanonicize( pCell );
+
+        // add to the table
+        p->nTotal++;
+        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+        else
+            p->nGood++;
+    }
+
+    // go through non-symmetric functions
+    for ( i1 = 0; i1 < 22; i1++ )
+    for ( i2 = 0; i2 < 22; i2++ )
+    for ( i3 = 0; i3 < 22; i3++ )
+    {
+        // derive the cell
+        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+        memset( pCell, 0, sizeof(Cut_Cell_t) );
+        pCell->nVars  = 9;
+        pCell->Box[0] = 17;
+        pCell->Box[1] = i1;
+        pCell->Box[2] = i2;
+        pCell->Box[3] = i3;
+        // fill in the truth table
+        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, 17 );
+        // canonicize
+        Cut_CellCanonicize( pCell );
+
+        // add to the table
+        p->nTotal++;
+        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+        else
+            p->nGood++;
+    }
+*/
+
+    // go through non-symmetric functions
+    for ( k = 0; k < 10; k++ )
+    for ( i1 = 0; i1 < 22; i1++ )
+    for ( i2 = 0; i2 < 22; i2++ )
+    for ( i3 = 0; i3 < 22; i3++ )
+    {
+        // derive the cell
+        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+        memset( pCell, 0, sizeof(Cut_Cell_t) );
+        pCell->nVars  = 9;
+        pCell->Box[0] = s_NPNe3[k];
+        pCell->Box[1] = i1;
+        pCell->Box[2] = i2;
+        pCell->Box[3] = i3;
+        // set the elementary permutation
+        for ( i = 0; i < (int)pCell->nVars; i++ )
+            pCell->CanonPerm[i] = i;
+        // fill in the truth table
+        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3[k] );
+        // minimize the support
+        Cut_CellSuppMin( pCell );
+
+        // canonicize
+        pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+
+        // add to the table
+        p->nTotal++;
+        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+        else
+        {
+            p->nGood++;
+            p->nVarCounts[pCell->nVars]++;
+
+            if ( pCell->nVars )
+            for ( i = 0; i < (int)pCell->nVars-1; i++ )
+            {
+                if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
+                    continue;
+                // i and i+1 can be symmetric
+                // find the end of this group
+                for ( j = i+1; j < (int)pCell->nVars; j++ )
+                    if ( pCell->Store[2*i] != pCell->Store[2*j] ) 
+                        break;
+
+                if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
+                    p->nSymGroupsE[j-i]++;
+                else
+                    p->nSymGroups[j-i]++;
+                i = j - 1;
+            }
+/*
+            if ( pCell->nVars == 3 )
+            {
+                Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
+                for ( i = 0; i < (int)pCell->nVars; i++ )
+                    printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+                printf( "\n" );
+            }
+*/
+        }
+    }
+
+    printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
+    PRT( "Time", clock() - clk );
+    printf( "Cells:  " );
+    for ( i = 0; i <= 9; i++ )
+        printf( "%d=%d ", i, p->nVarCounts[i] );
+    printf( "\nDiffs:  " );
+    for ( i = 0; i <= 9; i++ )
+        printf( "%d=%d ", i, p->nSymGroups[i] );
+    printf( "\nEquals: " );
+    for ( i = 0; i <= 9; i++ )
+        printf( "%d=%d ", i, p->nSymGroupsE[i] );
+    printf( "\n" );
+
+    // continue adding new cells using support
+    for ( k = CUT_CELL_MVAR; k > 3; k-- )
+    {
+        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+        for ( i1 = 0; i1 < k; i1++ )
+        for ( i2 = i1+1; i2 < k; i2++ )
+        for ( c = 0; c < 3; c++ )
+        {
+            // derive the cell
+            pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+            memset( pCell, 0, sizeof(Cut_Cell_t) );
+            pCell->nVars   = pTemp->nVars;
+            pCell->pParent = pTemp;
+            // set the elementary permutation
+            for ( i = 0; i < (int)pCell->nVars; i++ )
+                pCell->CanonPerm[i] = i;
+            // fill in the truth table
+            Extra_TruthCopy( pCell->uTruth, pTemp->uTruth, pTemp->nVars );
+            // create the cross-bar
+            pCell->CrossBar0 = i1;
+            pCell->CrossBar1 = i2;
+            pCell->CrossBarPhase = c;
+            Cut_CellCrossBar( pCell );
+            // minimize the support
+//clk2 = clock();
+            Cut_CellSuppMin( pCell );
+//p->timeSupp += clock() - clk2;
+            // canonicize
+//clk2 = clock();
+            pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+//p->timeCanon += clock() - clk2;
+
+            // add to the table
+//clk2 = clock();
+            p->nTotal++;
+            if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+                Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+            else
+            {
+                p->nGood++;
+                p->nVarCounts[pCell->nVars]++;
+
+                for ( i = 0; i < (int)pCell->nVars-1; i++ )
+                {
+                    if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
+                        continue;
+                    // i and i+1 can be symmetric
+                    // find the end of this group
+                    for ( j = i+1; j < (int)pCell->nVars; j++ )
+                        if ( pCell->Store[2*i] != pCell->Store[2*j] ) 
+                            break;
+
+                    if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
+                        p->nSymGroupsE[j-i]++;
+                    else
+                        p->nSymGroups[j-i]++;
+                    i = j - 1;
+                }
+/*
+                if ( pCell->nVars == 3 )
+                {
+                    Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
+                    for ( i = 0; i < (int)pCell->nVars; i++ )
+                        printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+                    printf( "\n" );
+                }
+*/
+            }
+//p->timeTable += clock() - clk2;
+        }
+
+        printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
+        PRT( "Time", clock() - clk );
+        printf( "Cells:  " );
+        for ( i = 0; i <= 9; i++ )
+            printf( "%d=%d ", i, p->nVarCounts[i] );
+        printf( "\nDiffs:  " );
+        for ( i = 0; i <= 9; i++ )
+            printf( "%d=%d ", i, p->nSymGroups[i] );
+        printf( "\nEquals: " );
+        for ( i = 0; i <= 9; i++ )
+            printf( "%d=%d ", i, p->nSymGroupsE[i] );
+        printf( "\n" );
+    }
+//    printf( "\n" );
+    PRT( "Supp ", p->timeSupp );
+    PRT( "Canon", p->timeCanon );
+    PRT( "Table", p->timeTable );
+//    Cut_CManStop( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check the table.]
+
+  Description [Returns 1 if such a truth table already exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell )
+{
+    Cut_Cell_t ** pSlot, * pTemp;
+    unsigned Hash;
+    Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum( pCell->nVars ) );
+    if ( !st_find_or_add( p->tTable, (char *)Hash, (char ***)&pSlot ) )
+        *pSlot = NULL;
+    for ( pTemp = *pSlot; pTemp; pTemp = pTemp->pNext )
+    {
+        if ( pTemp->nVars != pCell->nVars )
+            continue;
+        if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
+            return 1;
+    }
+    // the entry is new
+    pCell->pNext = *pSlot;
+    *pSlot = pCell;
+    // add it to the variable support list
+    pCell->pNextVar = p->pSameVar[pCell->nVars];
+    p->pSameVar[pCell->nVars] = pCell;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellSuppMin( Cut_Cell_t * pCell )
+{
+    static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
+    unsigned * pIn, * pOut, * pTemp;
+    int i, k, Counter, Temp;
+
+    // go backward through the support variables and remove redundant
+    for ( k = pCell->nVars - 1; k >= 0; k-- )
+        if ( !Extra_TruthVarInSupport(pCell->uTruth, pCell->nVars, k) )
+        {
+            // shift all the variables above this one
+            Counter = 0;
+            pIn = pCell->uTruth; pOut = uTemp;
+            for ( i = k; i < (int)pCell->nVars - 1; i++ )
+            {
+                Extra_TruthSwapAdjacentVars( pOut, pIn, pCell->nVars, i );
+                pTemp = pIn; pIn = pOut; pOut = pTemp;
+                // swap the support vars
+                Temp = pCell->CanonPerm[i]; 
+                pCell->CanonPerm[i] = pCell->CanonPerm[i+1];
+                pCell->CanonPerm[i+1] = Temp;
+                Counter++;
+            }
+            // return the function back into its place
+            if ( Counter & 1 )
+                Extra_TruthCopy( pOut, pIn, pCell->nVars );
+            // remove one variable
+            pCell->nVars--;
+//            Extra_PrintBinary( stdout, pCell->uTruth, (1<<pCell->nVars) ); printf( "\n" );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellCrossBar( Cut_Cell_t * pCell )
+{
+    static unsigned uTemp0[1<<(CUT_CELL_MVAR-5)];
+    static unsigned uTemp1[1<<(CUT_CELL_MVAR-5)];
+    Extra_TruthCopy( uTemp0, pCell->uTruth, pCell->nVars );
+    Extra_TruthCopy( uTemp1, pCell->uTruth, pCell->nVars );
+    if ( pCell->CanonPhase == 0 )
+    {
+        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
+        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
+    }
+    else if ( pCell->CanonPhase == 1 )
+    {
+        Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
+        Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
+    }
+    else if ( pCell->CanonPhase == 2 )
+    {
+        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar1 );
+        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
+        Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
+    }
+    else assert( 0 );
+    Extra_TruthCombine( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type )
+{
+    int nWords = Extra_TruthWordNum( nVars );
+    int i;
+
+    assert( Type < 22 );
+    switch ( Type )
+    {
+    // " 0\n",                         // 00   const 0
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = 0;
+        return;
+    // " 1\n",                         // 01   const 1
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = 0xFFFFFFFF;
+        return;
+    // "1 1\n",                        // 02   a
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i];
+        return;
+    // "11 1\n",                       // 03   ab
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] & InB[i];
+        return;
+    // "11 0\n",                       // 04   (ab)'
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~(InA[i] & InB[i]);
+        return;
+    // "10 1\n01 1\n",                 // 05   a<+>b
+    case 5:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] ^ InB[i];
+        return;
+    // "111 1\n",                      // 06 + abc
+    case 6:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] & InB[i] & InC[i];
+        return;
+    // "111 0\n",                      // 07   (abc)'
+    case 7:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~(InA[i] & InB[i] & InC[i]);
+        return;
+    // "11- 1\n1-1 1\n",               // 08 + a(b+c)
+    case 8:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] & (InB[i] | InC[i]);
+        return;
+    // "11- 0\n1-1 0\n",               // 09   (a(b+c))'
+    case 9:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~(InA[i] & (InB[i] | InC[i]));
+        return;
+    // "111 1\n100 1\n010 1\n001 1\n", // 10 + a<+>b<+>c
+    case 10:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] ^ InB[i] ^ InC[i];
+        return;
+    // "10- 0\n1-0 0\n011 0\n",        // 11 + a<+>bc
+    case 11:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] ^ (InB[i] & InC[i]);
+        return;
+    // "101 1\n110 1\n",               // 12 + a(b<+>c)
+    case 12:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = InA[i] & (InB[i] ^ InC[i]);
+        return;
+    // "101 0\n110 0\n",               // 13   (a(b<+>c))'
+    case 13:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~(InA[i] & (InB[i] ^ InC[i]));
+        return;
+    // "11- 1\n1-1 1\n-11 1\n",        // 14 + ab+bc+ac
+    case 14:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (InA[i] & InC[i]);
+        return;
+    // "111 1\n000 1\n",               // 15 + abc+a'b'c'
+    case 15:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]);
+        return;
+    // "111 0\n000 0\n",               // 16   (abc+a'b'c')'
+    case 16:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~((InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]));
+        return;
+    // "11- 1\n-11 1\n0-1 1\n",        // 17 + ab+bc+a'c
+    case 17:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (~InA[i] & InC[i]);
+        return;
+    // "011 1\n101 1\n110 1\n",        // 18 + a'bc+ab'c+abc'
+    case 18:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]);
+        return;
+    // "011 0\n101 0\n110 0\n",        // 19   (a'bc+ab'c+abc')'
+    case 19:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~((~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]));
+        return;
+    // "100 1\n-11 1\n",               // 20 + ab'c'+bc
+    case 20:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]);
+        return;
+    // "100 0\n-11 0\n"                // 21   (ab'c'+bc)'
+    case 21:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = ~((InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]));
+        return;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Start the precomputation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_CMan_t * Cut_CManStart()
+{
+    Cut_CMan_t * p;
+    int i, k;
+    // start the manager
+    assert( sizeof(unsigned) == 4 );
+    p = ALLOC( Cut_CMan_t, 1 );
+    memset( p, 0, sizeof(Cut_CMan_t) );
+    // start the table and the memory manager
+    p->tTable = st_init_table(st_ptrcmp,st_ptrhash);
+    p->pMem = Extra_MmFixedStart( sizeof(Cut_Cell_t) );
+    // set elementary truth tables
+    for ( k = 0; k < CUT_CELL_MVAR; k++ )
+        for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
+            if ( i & (1 << k) )
+                p->uInputs[k][i/32] |= (1 << (i%32));
+    s_pCMan = p;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CManStop( Cut_CMan_t * p )
+{
+    st_free_table( p->tTable );
+    Extra_MmFixedStop( p->pMem, 0 );
+    free( p );
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CellIsRunning()
+{
+    return s_pCMan != NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CellDumpToFile()
+{
+    FILE * pFile;
+    Cut_CMan_t * p = s_pCMan;
+    Cut_Cell_t * pTemp;
+    char * pFileName = "celllib22.txt";
+    int NumUsed[10][5] = {{0}};
+    int BoxUsed[22][5] = {{0}};
+    int i, k, Counter;
+    int clk = clock();
+
+    if ( p == NULL )
+    {
+        printf( "Cut_CellDumpToFile: Cell manager is not defined.\n" );
+        return;
+    }
+
+    // count the number of cells used
+    for ( k = CUT_CELL_MVAR; k >= 0; k-- )
+    {
+        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+        {
+            if ( pTemp->nUsed == 0 )
+                NumUsed[k][0]++;
+            else if ( pTemp->nUsed < 10 )
+                NumUsed[k][1]++;
+            else if ( pTemp->nUsed < 100 )
+                NumUsed[k][2]++;
+            else if ( pTemp->nUsed < 1000 )
+                NumUsed[k][3]++;
+            else 
+                NumUsed[k][4]++;
+
+            for ( i = 0; i < 4; i++ )
+                if ( pTemp->nUsed == 0 )
+                    BoxUsed[ pTemp->Box[i] ][0]++;
+                else if ( pTemp->nUsed < 10 )
+                    BoxUsed[ pTemp->Box[i] ][1]++;
+                else if ( pTemp->nUsed < 100 )
+                    BoxUsed[ pTemp->Box[i] ][2]++;
+                else if ( pTemp->nUsed < 1000 )
+                    BoxUsed[ pTemp->Box[i] ][3]++;
+                else 
+                    BoxUsed[ pTemp->Box[i] ][4]++;
+        }
+    }
+
+    printf( "Functions found = %10d.  Functions not found = %10d.\n", p->nCellFound, p->nCellNotFound );
+    for ( k = 0; k <= CUT_CELL_MVAR; k++ )
+    {
+        printf( "%3d  : ", k );
+        for ( i = 0; i < 5; i++ ) 
+            printf( "%8d ", NumUsed[k][i] );
+        printf( "\n" );
+    }
+    printf( "Box usage:\n" );
+    for ( k = 0; k < 22; k++ )
+    {
+        printf( "%3d  : ", k );
+        for ( i = 0; i < 5; i++ ) 
+            printf( "%8d ", BoxUsed[k][i] );
+        printf( "  %s", s_NP3Names[k] );
+        printf( "\n" );
+    }
+
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cut_CellDumpToFile: Cannout open output file.\n" );
+        return;
+    }
+
+    Counter = 0;
+    for ( k = 0; k <= CUT_CELL_MVAR; k++ )
+    {
+        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+            if ( pTemp->nUsed > 0 )
+            {
+                Extra_PrintHexadecimal( pFile, pTemp->uTruth, (k <= 5? 5 : k) );
+                fprintf( pFile, "\n" );
+                Counter++;
+            }
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+
+    printf( "Library composed of %d functions is written into file \"%s\".  ", Counter, pFileName );
+
+    PRT( "Time", clock() - clk );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Looks up if the given function exists in the hash table.]
+
+  Description [If the function exists, returns 1, meaning that it can be
+  implemented using two levels of 3-input LUTs. If the function does not 
+  exist, return 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CellTruthLookup( unsigned * pTruth, int nVars )
+{
+    Cut_CMan_t * p = s_pCMan;
+    Cut_Cell_t * pTemp;
+    Cut_Cell_t Cell, * pCell = &Cell;
+    unsigned Hash;
+    int i;
+
+    // cell manager is not defined
+    if ( p == NULL )
+    {
+        printf( "Cut_CellTruthLookup: Cell manager is not defined.\n" );
+        return 0;
+    }
+
+    // canonicize
+    memset( pCell, 0, sizeof(Cut_Cell_t) );
+    pCell->nVars = nVars;
+    Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
+    Cut_CellSuppMin( pCell );
+    // set the elementary permutation
+    for ( i = 0; i < (int)pCell->nVars; i++ )
+        pCell->CanonPerm[i] = i;
+    // canonicize
+    pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+
+
+    // check if the cell exists
+    Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum(pCell->nVars) );
+    if ( st_lookup( p->tTable, (char *)Hash, (char **)&pTemp ) )
+    {
+        for ( ; pTemp; pTemp = pTemp->pNext )
+        {
+            if ( pTemp->nVars != pCell->nVars )
+                continue;
+            if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
+            {
+                pTemp->nUsed++;
+                p->nCellFound++;
+                return 1;
+            }
+        }
+    }
+    p->nCellNotFound++;
+    return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index 4b8738a2..d36f94f7 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -109,9 +109,9 @@ void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int
     // merge the old and the new
 clk = clock();
     Cut_ListStart( pSuper );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0 );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0 );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0, 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0, 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv, 0 );
     pListNew = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
 
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index b65e5eff..54b3aac0 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -20,17 +20,27 @@
 
 #include "cutInt.h"
 
+/* 
+    Truth tables computed in this package are represented as bit-strings
+    stored in the cut data structure. Cuts of any number of inputs have 
+    the truth table with 2^k bits, where k is the max number of cut inputs.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern int nTotal = 0;
+extern int nGood  = 0;
+extern int nEqual = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs truth table computation.]
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
 
   Description []
                
@@ -60,6 +70,48 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
 
   Synopsis    [Performs truth table computation.]
 
+  Description [This procedure cannot be used while recording oracle
+  because it will overwrite Num0 and Num1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthNCanonicize( Cut_Cut_t * pCut )
+{
+    unsigned uTruth;
+    unsigned * uCanon2;
+    char * pPhases2;
+    assert( pCut->nVarsMax < 6 );
+
+    // get the direct truth table
+    uTruth = *Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon0 = uCanon2[0];
+    pCut->Num0    = pPhases2[0];
+
+    // get the complemented truth table
+    uTruth = ~*Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon1 = uCanon2[0];
+    pCut->Num1    = pPhases2[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
   Description []
                
   SideEffects []
@@ -67,7 +119,7 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
+void Cut_TruthComputeOld( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
     static unsigned uTruth0[8], uTruth1[8];
     int nTruthWords = Cut_TruthWords( pCut->nVarsMax );
@@ -111,43 +163,55 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i
 
   Synopsis    [Performs truth table computation.]
 
-  Description [This procedure cannot be used while recording oracle
-  because it will overwrite Num0 and Num1.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCanonicize( Cut_Cut_t * pCut )
+void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
-    unsigned uTruth;
-    unsigned * uCanon2;
-    char * pPhases2;
-    assert( pCut->nVarsMax < 6 );
-
-    // get the direct truth table
-    uTruth = *Cut_CutReadTruth(pCut);
-
-    // compute the direct truth table
-    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
-//    uCanon[0] = uCanon2[0];
-//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
-//    uPhases[0] = pPhases2[0];
-    pCut->uCanon0 = uCanon2[0];
-    pCut->Num0    = pPhases2[0];
+    // permute the first table
+    if ( fCompl0 ) 
+        Extra_TruthNot( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
+    else
+        Extra_TruthCopy( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
+    Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut0) );
+    // permute the second table
+    if ( fCompl1 ) 
+        Extra_TruthNot( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
+    else
+        Extra_TruthCopy( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
+    Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut1) );
+    // produce the resulting table
+    if ( pCut->fCompl )
+        Extra_TruthNand( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+    else
+        Extra_TruthAnd( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+    // quit if no fancy computation is needed
+    if ( !p->pParams->fFancy )
+        return;
+
+    // count the total number of truth tables computed
+    nTotal++;
+
+    // MAPPING INTO ALTERA 6-2 LOGIC BLOCKS
+    // call this procedure to find the minimum number of common variables in the cofactors
+    // if this number is less or equal than 3, the cut can be implemented using the 6-2 logic block
+//    if ( Extra_TruthMinCofSuppOverlap( Cut_CutReadTruth(pCut), pCut->nVarsMax, NULL ) <= 3 )
+//        nGood++;
+
+    // MAPPING INTO ACTEL 2x2 CELLS
+    // call this procedure to see if a semi-canonical form can be found in the lookup table 
+    // (if it exists, then a two-level 3-input LUT implementation of the cut exists)
+    // Before this procedure is called, cell manager should be defined by calling
+    // Cut_CellLoad (make sure file "cells22_daomap_iwls.txt" is available in the working dir)
+    if ( Cut_CellIsRunning() && pCut->nVarsMax <= 9 )
+        nGood += Cut_CellTruthLookup( Cut_CutReadTruth(pCut), pCut->nVarsMax );
+}
 
-    // get the complemented truth table
-    uTruth = ~*Cut_CutReadTruth(pCut);
 
-    // compute the direct truth table
-    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
-//    uCanon[0] = uCanon2[0];
-//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
-//    uPhases[0] = pPhases2[0];
-    pCut->uCanon1 = uCanon2[0];
-    pCut->Num1    = pPhases2[0];
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make
index af2d8fc1..132e730b 100644
--- a/src/opt/cut/module.make
+++ b/src/opt/cut/module.make
@@ -4,5 +4,6 @@ SRC +=  src/opt/cut/cutApi.c \
         src/opt/cut/cutMerge.c \
         src/opt/cut/cutNode.c \
         src/opt/cut/cutOracle.c \
+        src/opt/cut/cutPre22.c \
         src/opt/cut/cutSeq.c \
         src/opt/cut/cutTruth.c 
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index b83a524f..55132a75 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
     // get the node's cuts
 clk = clock();
-    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0 );
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
 p->timeCut += clock() - clk;