Version abc60419

abc.dsp

@@ -502,7 +502,11 @@ SOURCE=.\src\base\io\ioWritePla.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\base\io\ioWriteVerilog.c
+SOURCE=.\src\base\io\ioWriteVer.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteVerAux.c
 # End Source File
 # End Group
 # Begin Group "main"
@@ -1302,6 +1306,10 @@ SOURCE=.\src\opt\cut\cutCut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\cut\cutExpand.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\cut\cutInt.h
 # End Source File
 # Begin Source File

src/base/abc/abcAig.c

@@ -743,6 +743,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool
     if ( fUpdateLevel )
     {
         Abc_AigUpdateLevel_int( pMan );
+        if ( pMan->pNtkAig->vLevelsR ) 
             Abc_AigUpdateLevelR_int( pMan );
     }
 }
@@ -819,10 +820,13 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
             pFanout->fMarkA = 1;
             Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
             // schedule the updated fanout for updating reverse level
+            if ( pMan->pNtkAig->vLevelsR ) 
+            {
                 assert( pFanout->fMarkB == 0 );
                 pFanout->fMarkB = 1;
                 Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
             }
+        }
 
         // the fanout has changed, update EXOR status of its fanouts
         Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )

src/base/abc/abcObj.c

@@ -235,7 +235,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
-        assert( Abc_NtkPoNum(pObj->pNtk) == 1 );
+        assert( Abc_NtkPoNum(pObj->pNtk) > 0 );
         Vec_PtrRemove( pObj->pNtk->vCos, pObj );
         pObj->pNtk->nPos--;
         // add the name to the table

src/base/abci/abc.c

@@ -69,6 +69,7 @@ static int Abc_CommandRr           ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDemiter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrPos        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -178,6 +179,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
@@ -2866,8 +2868,8 @@ int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: rr [-W NM] [-fvh]\n" );
-    fprintf( pErr, "\t         performs redundancy removal in the current network\n" );
-    fprintf( pErr, "\t-W NM  : window size as the number of TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels );
+    fprintf( pErr, "\t         removes combinational redundancies in the current network\n" );
+    fprintf( pErr, "\t-W NM  : window size: TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels );
     fprintf( pErr, "\t-f     : toggle RR w.r.t. fanouts [default = %s]\n", fUseFanouts? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -3027,10 +3029,10 @@ usage:
 int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
     int fComb;
     int c;
-    extern Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkDemiter( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3062,17 +3064,16 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->fExor )
+    if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
     {
         fprintf( pErr, "The miter's PO is not an EXOR.\n" );
         return 1;
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDemiter( pNtk );
-    if ( pNtkRes == NULL )
+    if ( !Abc_NtkDemiter( pNtk ) )
     {
-        fprintf( pErr, "Miter computation has failed.\n" );
+        fprintf( pErr, "Demitering has failed.\n" );
         return 1;
     }
     // replace the current network
@@ -3098,6 +3099,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    int fComb;
+    int c;
+    extern int Abc_NtkOrPos( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fComb ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "The network is not strashed.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+    {
+        fprintf( pErr, "The network already has one PO.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The miter has latches. ORing is not performed.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkOrPos( pNtk ) )
+    {
+        fprintf( pErr, "ORing the POs has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+//    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: orpos [-h]\n" );
+    fprintf( pErr, "\t        creates single-output miter by ORing the POs of the current network\n" );
+//    fprintf( pErr, "\t-c    : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4540,15 +4614,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cut_CellDumpToFile();
 //    else
 //        Cut_CellPrecompute();
-//        Cut_CellLoad();
-
+        Cut_CellLoad();
+/*
         {
             Abc_Ntk_t * pNtkRes;
             extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
             pNtkRes = Abc_NtkTopmost( pNtk, nLevels );
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
-
+*/
     return 0;
 
 usage:

src/base/abci/abcFraig.c

@@ -704,6 +704,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Fraig_Params_t Params;
     Abc_Ntk_t * pStore, * pFraig;
     int nWords1, nWords2, nWordsMin;
+    int clk = clock();
 
     // get the stored network
     pStore = Abc_FrameReadNtkStore();
@@ -740,6 +741,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 //    Fraig_ManReportChoices( p );
     // transform it into FRAIG
     pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
+PRT( "Total fraiging time", clock() - clk );
     if ( pFraig == NULL )
         return NULL;
     Abc_NtkDelete( pStore );

src/base/abci/abcMiter.c

@@ -957,7 +957,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the timeframes of the network.]
+  Synopsis    [Splits the miter into two logic cones combined by an EXOR]
 
   Description []
 
@@ -966,7 +966,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
+int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNodeC, * pNodeA, * pNodeB, * pNode;
     Abc_Obj_t * pPoNew;
@@ -975,22 +975,33 @@ Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
-    assert( Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->fExor );
+    if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
+    {
+        printf( "The root of the miter is not an EXOR gate.\n" );
+        return 0;
+    }
     pNodeC = Abc_NodeRecognizeMux( Abc_ObjFanin0(Abc_NtkPo(pNtk,0)), &pNodeA, &pNodeB );
     assert( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) );
+    if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk,0)) )
+    {
+        pNodeA = Abc_ObjNot(pNodeA);
+        pNodeB = Abc_ObjNot(pNodeB);
+    }
 
+    // add the PO corresponding to control input
     pPoNew = Abc_NtkCreatePo( pNtk );
     Abc_ObjAddFanin( pPoNew, pNodeC );
     Abc_NtkLogicStoreName( pPoNew, "addOut1" );
 
+    // add the PO corresponding to other input
     pPoNew = Abc_NtkCreatePo( pNtk );
-    Abc_ObjAddFanin( pPoNew, Abc_ObjRegular(pNodeA) );
+    Abc_ObjAddFanin( pPoNew, pNodeB );
     Abc_NtkLogicStoreName( pPoNew, "addOut2" );
 
     // mark the nodes in the first cone
-    pNodeA = Abc_ObjRegular(pNodeA);
+    pNodeB = Abc_ObjRegular(pNodeB);
     vNodes1 = Abc_NtkDfsNodes( pNtk, &pNodeC, 1 );
-    vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeA, 1 );
+    vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeB, 1 );
 
     Vec_PtrForEachEntry( vNodes1, pNode, i )
         pNode->fMarkA = 1;
@@ -1003,9 +1014,45 @@ Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
     printf( "First cone = %6d.  Second cone = %6d.  Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
     Vec_PtrFree( vNodes1 );
     Vec_PtrFree( vNodes2 );
+    return 1;
+}
+
+/**Function*************************************************************
 
+  Synopsis    [ORs the outputs.]
 
-    return pNtk;
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkOrPos( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pMiter;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    // OR the POs
+    pMiter = Abc_ObjNot( Abc_NtkConst1(pNtk) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+    // remove the POs and their names
+    for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- )
+        Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) );
+    assert( Abc_NtkPoNum(pNtk) == 0 );
+    // create the new PO
+    pNode = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pNode, pMiter );
+    Abc_NtkLogicStoreName( pNode, "miter" );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkOrPos: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcPrint.c

@@ -70,10 +70,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
             fprintf( pFile, " (choice = %d)", Num );
         if ( Num = Abc_NtkGetExorNum(pNtk) )
             fprintf( pFile, " (exor = %d)", Num );
-        if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
-            fprintf( pFile, " (mux = %d)", Num2-Num );
-        if ( Num2 )
-            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
+//        if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
+//            fprintf( pFile, " (mux = %d)", Num2-Num );
+//        if ( Num2 )
+//            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
     }
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
@@ -110,11 +110,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         FILE * pTable;
         pTable = fopen( "stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
-        fprintf( pTable, "%4d ", Abc_NtkPiNum(pNtk) );
-        fprintf( pTable, "%4d ", Abc_NtkPoNum(pNtk) );
-//        fprintf( pTable, "%4d ", Abc_NtkLatchNum(pNtk) );
-        fprintf( pTable, "%6d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%6d ", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }

src/base/cmd/cmd.c

@@ -168,6 +168,14 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
     pAbc->TimeTotal += pAbc->TimeCommand;
     fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
         (float)pAbc->TimeCommand / CLOCKS_PER_SEC, (float)pAbc->TimeTotal / CLOCKS_PER_SEC );
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "runtimes.txt", "a+" );
+        fprintf( pTable, "%4.2f\n", (float)pAbc->TimeCommand / CLOCKS_PER_SEC );
+        fclose( pTable );
+    }
+*/
     pAbc->TimeCommand = 0;
     return 0;
 

src/base/io/ioReadBlif.c

@@ -212,6 +212,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
         pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
+    else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
+    {
+        printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
+            Extra_FileReaderGetLineNumber(p->pReader, 0), p->vTokens->pArray[0] );
+        return NULL;
+    }
 
     // read the inputs/outputs
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );

src/base/io/module.make

@@ -17,4 +17,5 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioWriteGml.c \
     src/base/io/ioWriteList.c \
     src/base/io/ioWritePla.c \
-    src/base/io/ioWriteVerilog.c
+    src/base/io/ioWriteVer.c \
+    src/base/io/ioWriteVerAux.c

src/opt/cut/cutExpand.c

+/**CFile****************************************************************
+
+  FileName    [cutExpand.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Computes the truth table of the cut after expansion.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutExpand.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define CUT_CELL_MVAR  9
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the composition of cuts.]
+
+  Description [Inputs are: 
+  - a factor cut (truth table is stored inside)
+  - a node in the factor cut
+  - a tree cut to be substituted (truth table is stored inside)
+  - the resulting cut (truth table will be filled in).
+  Note that all cuts, including the resulting one, should be already 
+  computed and the nodes should be stored in the ascending order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthCompose( Cut_Cut_t * pCutF, int Node, Cut_Cut_t * pCutT, Cut_Cut_t * pCutRes )
+{
+    static unsigned uCof0[1<<(CUT_CELL_MVAR-5)];
+    static unsigned uCof1[1<<(CUT_CELL_MVAR-5)];
+    static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
+    unsigned * pIn, * pOut, * pTemp;
+    unsigned uPhase;
+    int NodeIndex, i, k;
+
+    // sanity checks
+    assert( pCutF->nVarsMax == pCutT->nVarsMax );
+    assert( pCutF->nVarsMax == pCutRes->nVarsMax );
+    assert( pCutF->nVarsMax <= CUT_CELL_MVAR );
+    // the factor cut (pCutF) should have its nodes sorted in the ascending order
+    assert( pCutF->nLeaves <= pCutF->nVarsMax );
+    for ( i = 0; i < (int)pCutF->nLeaves - 1; i++ )
+        assert( pCutF->pLeaves[i] < pCutF->pLeaves[i+1] );
+    // the tree cut (pCutT) should have its nodes sorted in the ascending order
+    assert( pCutT->nLeaves <= pCutT->nVarsMax );
+    for ( i = 0; i < (int)pCutT->nLeaves - 1; i++ )
+        assert( pCutT->pLeaves[i] < pCutT->pLeaves[i+1] );
+    // the resulting cut (pCutRes) should have its nodes sorted in the ascending order
+    assert( pCutRes->nLeaves <= pCutRes->nVarsMax );
+    for ( i = 0; i < (int)pCutRes->nLeaves - 1; i++ )
+        assert( pCutRes->pLeaves[i] < pCutRes->pLeaves[i+1] );
+    // make sure that every node in pCutF (except Node) appears in pCutRes
+    for ( i = 0; i < (int)pCutF->nLeaves; i++ )
+    {
+        if ( pCutF->pLeaves[i] == Node )
+            continue;
+        for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
+            if ( pCutF->pLeaves[i] == pCutRes->pLeaves[k] )
+                break;
+        assert( k < (int)pCutRes->nLeaves ); // node i from pCutF is not found in pCutRes!!!
+    }
+    // make sure that every node in pCutT appears in pCutRes
+    for ( i = 0; i < (int)pCutT->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
+            if ( pCutT->pLeaves[i] == pCutRes->pLeaves[k] )
+                break;
+        assert( k < (int)pCutRes->nLeaves ); // node i from pCutT is not found in pCutRes!!!
+    }
+
+
+    // find the index of the given node in the factor cut
+    NodeIndex = -1;
+    for ( NodeIndex = 0; NodeIndex < (int)pCutF->nLeaves; NodeIndex++ )
+        if ( pCutF->pLeaves[NodeIndex] == Node )
+            break;
+    assert( NodeIndex >= 0 );  // Node should be in pCutF
+
+    // copy the truth table
+    Extra_TruthCopy( uTemp, Cut_CutReadTruth(pCutF), pCutF->nLeaves );
+
+    // bubble-move the NodeIndex variable to be the last one (the most significant one)
+    pIn = uTemp; pOut = uCof0; // uCof0 is used for temporary storage here
+    for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
+    {
+        Extra_TruthSwapAdjacentVars( pOut, pIn, pCutF->nLeaves, i );
+        pTemp = pIn; pIn = pOut; pOut = pTemp;
+    }
+    if ( (pCutF->nLeaves - 1 - NodeIndex) & 1 )
+        Extra_TruthCopy( pOut, pIn, pCutF->nLeaves );
+    // the result of stretching is in uTemp
+
+    // cofactor the factor cut with respect to the node
+    Extra_TruthCopy( uCof0, uTemp, pCutF->nLeaves );
+    Extra_TruthCofactor0( uCof0, pCutF->nLeaves, pCutF->nLeaves-1 );
+    Extra_TruthCopy( uCof1, uTemp, pCutF->nLeaves );
+    Extra_TruthCofactor1( uCof1, pCutF->nLeaves, pCutF->nLeaves-1 );
+
+    // temporarily shrink the factor cut's variables by removing Node 
+    for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
+        pCutF->pLeaves[i] = pCutF->pLeaves[i+1];
+    pCutF->nLeaves--;
+
+    // spread out the cofactors' truth tables to the same var order as the resulting cut
+    uPhase = Cut_TruthPhase(pCutRes, pCutF);
+    assert( Extra_WordCountOnes(uPhase) == (int)pCutF->nLeaves );
+    Extra_TruthStretch( uTemp, uCof0, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
+    Extra_TruthCopy( uCof0, uTemp, pCutF->nVarsMax );
+    Extra_TruthStretch( uTemp, uCof1, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
+    Extra_TruthCopy( uCof1, uTemp, pCutF->nVarsMax );
+
+    // spread out the tree cut's truth table to the same var order as the resulting cut
+    uPhase = Cut_TruthPhase(pCutRes, pCutT); 
+    assert( Extra_WordCountOnes(uPhase) == (int)pCutT->nLeaves );
+    Extra_TruthStretch( uTemp, Cut_CutReadTruth(pCutT), pCutT->nLeaves, pCutT->nVarsMax, uPhase );
+
+    // create the resulting truth table
+    pTemp = Cut_CutReadTruth(pCutRes);
+    for ( i = Extra_TruthWordNum(pCutRes->nLeaves)-1; i >= 0; i-- )
+        pTemp[i] = (uCof0[i] & ~uTemp[i]) | (uCof1[i] & uTemp[i]);
+
+    // undo the removal of the node from the cut
+    for ( i = (int)pCutF->nLeaves - 1; i >= NodeIndex; --i )
+        pCutF->pLeaves[i+1] = pCutF->pLeaves[i];
+    pCutF->pLeaves[NodeIndex] = Node;
+    pCutF->nLeaves++;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/cut/cutPre22.c

@@ -203,6 +203,11 @@ void Cut_CellLoad()
 */
         // add to the table
         p->nTotal++;
+
+//        Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars ); printf( "\n" );
+//        if ( p->nTotal == 500 )
+//            break;
+
         if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
             p->nGood++;
     }