summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/cut/cut.h108
-rw-r--r--src/opt/cut/cutInt.h107
-rw-r--r--src/opt/cut/cutList.h115
-rw-r--r--src/opt/cut/cutMan.c174
-rw-r--r--src/opt/cut/cutMerge.c656
-rw-r--r--src/opt/cut/cutNode.c623
-rw-r--r--src/opt/cut/cutSeq.c47
-rw-r--r--src/opt/cut/cutTable.c253
-rw-r--r--src/opt/cut/cutTruth.c322
-rw-r--r--src/opt/cut/module.make6
-rw-r--r--src/opt/fxu/module.make24
-rw-r--r--src/opt/rwr/module.make13
-rw-r--r--src/opt/rwr/rwrCut.c2
13 files changed, 2432 insertions, 18 deletions
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
new file mode 100644
index 00000000..0b4c4535
--- /dev/null
+++ b/src/opt/cut/cut.h
@@ -0,0 +1,108 @@
+/**CFile****************************************************************
+
+ FileName [cut.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUT_H__
+#define __CUT_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_ManStruct_t_ Cut_Man_t;
+typedef struct Cut_CutStruct_t_ Cut_Cut_t;
+typedef struct Cut_ParamsStruct_t_ Cut_Params_t;
+
+struct Cut_ParamsStruct_t_
+{
+ int nVarsMax; // the max cut size ("k" of the k-feasible cuts)
+ int nKeepMax; // the max number of cuts kept at a node
+ int nIdsMax; // the max number of IDs of cut objects
+ int fTruth; // compute truth tables
+ int fHash; // hash cuts to detect unique
+ int fFilter; // filter dominated cuts
+ int fSeq; // compute sequential cuts
+ int fDrop; // drop cuts on the fly
+ int fVerbose; // the verbosiness flag
+};
+
+struct Cut_CutStruct_t_
+{
+ unsigned uTruth : 16; // truth table for 4-input cuts
+ unsigned uPhase : 7; // the phase when mapping into a canonical form
+ unsigned fSimul : 1; // the value of cut's output at 000.. pattern
+ unsigned fCompl : 1; // the cut is complemented
+ unsigned fSeq : 1; // the cut is sequential
+ unsigned nVarsMax : 3; // the max number of vars [4-6]
+ unsigned nLeaves : 3; // the number of leaves [4-6]
+ Cut_Cut_t * pNext; // the next cut in the list
+ void * pData; // the user data
+ int pLeaves[0]; // the array of leaves
+};
+
+static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p ) { if ( p->nVarsMax == 4 ) return (unsigned *)p; return (unsigned *)(p->pLeaves + p->nVarsMax + p->fSeq); }
+static inline unsigned Cut_CutReadPhase( Cut_Cut_t * p ) { return p->uPhase; }
+static inline int Cut_CutReadLeaveNum( Cut_Cut_t * p ) { return p->nLeaves; }
+static inline int * Cut_CutReadLeaves( Cut_Cut_t * p ) { return p->pLeaves; }
+static inline void * Cut_CutReadData( Cut_Cut_t * p ) { return p->pData; }
+
+static inline void * Cut_CutWriteData( Cut_Cut_t * p, void * pData ) { p->pData = pData; }
+static inline void Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth ) {
+ if ( p->nVarsMax == 4 ) { p->uTruth = *puTruth; return; }
+ p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
+ if ( p->nVarsMax == 6 ) p->pLeaves[p->nVarsMax + p->fSeq + 1] = (int)puTruth[1];
+}
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cutMan.c ==========================================================*/
+extern Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams );
+extern void Cut_ManStop( Cut_Man_t * p );
+extern void Cut_ManPrintStats( Cut_Man_t * p );
+extern void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
+/*=== cutNode.c ==========================================================*/
+extern void Cut_NodeSetTriv( Cut_Man_t * p, int Node );
+extern Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
+extern Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
+extern Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node );
+extern void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
+extern void Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
+extern void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node );
+extern void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
new file mode 100644
index 00000000..da54a188
--- /dev/null
+++ b/src/opt/cut/cutInt.h
@@ -0,0 +1,107 @@
+/**CFile****************************************************************
+
+ FileName [cutInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUT_INT_H__
+#define __CUT_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+#include "vec.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_HashTableStruct_t_ Cut_HashTable_t;
+
+struct Cut_ManStruct_t_
+{
+ // user preferences
+ Cut_Params_t * pParams; // computation parameters
+ Vec_Int_t * vFanCounts; // the array of fanout counters
+ // storage for cuts
+ Vec_Ptr_t * vCuts; // cuts by ID
+ Vec_Ptr_t * vCutsNew; // cuts by ID
+ Cut_HashTable_t * tTable; // cuts by their leaves (and root)
+ // memory management
+ Extra_MmFixed_t * pMmCuts;
+ int EntrySize;
+ // temporary variables
+ Cut_Cut_t * pReady;
+ Vec_Ptr_t * vTemp;
+ int fCompl0;
+ int fCompl1;
+ int fSimul;
+ // precomputations
+ unsigned uTruthVars[6][2];
+ unsigned short ** pPerms43;
+ unsigned ** pPerms53;
+ unsigned ** pPerms54;
+ // statistics
+ int nCutsCur;
+ int nCutsAlloc;
+ int nCutsDealloc;
+ int nCutsPeak;
+ int nCutsTriv;
+ int nCutsNode;
+ // runtime
+ int timeMerge;
+ int timeUnion;
+ int timeTruth;
+ int timeFilter;
+ int timeHash;
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cutMerge.c ==========================================================*/
+extern Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+/*=== cutNode.c ==========================================================*/
+extern Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p );
+/*=== cutTable.c ==========================================================*/
+extern Cut_HashTable_t * Cut_TableStart( int Size );
+extern void Cut_TableStop( Cut_HashTable_t * pTable );
+extern int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore );
+extern void Cut_TableClear( Cut_HashTable_t * pTable );
+extern int Cut_TableReadTime( Cut_HashTable_t * pTable );
+/*=== cutTruth.c ==========================================================*/
+extern void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
new file mode 100644
index 00000000..eb008ef9
--- /dev/null
+++ b/src/opt/cut/cutList.h
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+ FileName [cutList.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Implementation of layered listed list of cuts.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutList.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUT_LIST_H__
+#define __CUT_LIST_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_ListStruct_t_ Cut_List_t;
+struct Cut_ListStruct_t_
+{
+ Cut_Cut_t * pHead[7];
+ Cut_Cut_t ** ppTail[7];
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cut_ListStart( Cut_List_t * p )
+{
+ int i;
+ for ( i = 1; i <= 6; i++ )
+ {
+ p->pHead[i] = 0;
+ p->ppTail[i] = &p->pHead[i];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
+{
+ assert( pCut->nLeaves > 0 && pCut->nLeaves < 7 );
+ *p->ppTail[pCut->nLeaves] = pCut;
+ p->ppTail[pCut->nLeaves] = &pCut->pNext;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
+{
+ int i;
+ for ( i = 1; i < 6; i++ )
+ *p->ppTail[i] = p->pHead[i+1];
+ *p->ppTail[6] = NULL;
+ return p->pHead[1];
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
new file mode 100644
index 00000000..a96f8173
--- /dev/null
+++ b/src/opt/cut/cutMan.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+ FileName [cutMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Cut manager.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
+{
+ Cut_Man_t * p;
+ int clk = clock();
+ assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 );
+ p = ALLOC( Cut_Man_t, 1 );
+ memset( p, 0, sizeof(Cut_Man_t) );
+ // set and correct parameters
+ p->pParams = pParams;
+ if ( p->pParams->fSeq )
+ p->pParams->fHash = 1;
+ // space for cuts
+ p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
+ Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+ if ( pParams->fSeq )
+ {
+ p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
+ Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+ }
+ // hash tables
+ if ( pParams->fHash )
+ p->tTable = Cut_TableStart( p->pParams->nKeepMax );
+ // entry size
+ p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
+ if ( pParams->nVarsMax == 5 )
+ p->EntrySize += sizeof(unsigned);
+ else if ( pParams->nVarsMax == 6 )
+ p->EntrySize += 2 * sizeof(unsigned);
+ // memory for cuts
+ p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
+ // precomputations
+// if ( pParams->fTruth && pParams->nVarsMax == 4 )
+// p->pPerms43 = Extra_TruthPerm43();
+// else if ( pParams->fTruth )
+// {
+// p->pPerms53 = Extra_TruthPerm53();
+// p->pPerms54 = Extra_TruthPerm54();
+// }
+ p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA; // 1010 1010 1010 1010 1010 1010 1010 1010
+ p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC; // 1010 1010 1010 1010 1010 1010 1010 1010
+ p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0; // 1111 0000 1111 0000 1111 0000 1111 0000
+ p->uTruthVars[3][1] = p->uTruthVars[3][0] = 0xFF00FF00; // 1111 1111 0000 0000 1111 1111 0000 0000
+ p->uTruthVars[4][1] = p->uTruthVars[4][0] = 0xFFFF0000; // 1111 1111 1111 1111 0000 0000 0000 0000
+ p->uTruthVars[5][0] = 0x00000000;
+ p->uTruthVars[5][1] = 0xFFFFFFFF;
+ p->vTemp = Vec_PtrAlloc( 100 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the cut manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_ManStop( Cut_Man_t * p )
+{
+ Cut_Cut_t * pCut;
+ int i;
+ Vec_PtrForEachEntry( p->vCuts, pCut, i )
+ {
+ if ( pCut != NULL )
+ {
+ int k = 0;
+ }
+ }
+
+ if ( p->vCutsNew ) Vec_PtrFree( p->vCutsNew );
+ if ( p->vCuts ) Vec_PtrFree( p->vCuts );
+ if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
+ if ( p->pPerms43 ) free( p->pPerms43 );
+ if ( p->pPerms53 ) free( p->pPerms53 );
+ if ( p->pPerms54 ) free( p->pPerms54 );
+ if ( p->vTemp ) Vec_PtrFree( p->vTemp );
+ if ( p->tTable ) Cut_TableStop( p->tTable );
+ Extra_MmFixedStop( p->pMmCuts, 0 );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_ManPrintStats( Cut_Man_t * p )
+{
+ printf( "Cut computation statistics:\n" );
+ printf( "Current cuts = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv );
+ printf( "Peak cuts = %8d.\n", p->nCutsPeak );
+ printf( "Total allocated = %8d.\n", p->nCutsAlloc );
+ printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
+ printf( "The cut size = %3d bytes.\n", p->EntrySize );
+ printf( "Peak memory = %.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
+ PRT( "Merge ", p->timeMerge );
+ PRT( "Union ", p->timeUnion );
+ PRT( "Hash ", Cut_TableReadTime(p->tTable) );
+ PRT( "Filter", p->timeFilter );
+ PRT( "Truth ", p->timeTruth );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
+{
+ p->vFanCounts = vFanCounts;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c
new file mode 100644
index 00000000..ba1afce4
--- /dev/null
+++ b/src/opt/cut/cutMerge.c
@@ -0,0 +1,656 @@
+/**CFile****************************************************************
+
+ FileName [cutMerge.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Procedure to merge two cuts.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description [This procedure works.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
+ Cut_Cut_t * pRes;
+ int * pRow;
+ int nLeaves0, nLeaves1, Limit;
+ int i, k, Count, nNodes;
+
+ assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+ // the case of the largest cut sizes
+ Limit = p->pParams->nVarsMax;
+ nLeaves0 = pCut0->nLeaves;
+ nLeaves1 = pCut1->nLeaves;
+ if ( nLeaves0 == Limit && nLeaves1 == Limit )
+ {
+ for ( i = 0; i < nLeaves0; i++ )
+ if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+ return NULL;
+ pRes = Cut_CutAlloc( p );
+ for ( i = 0; i < nLeaves0; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = nLeaves0;
+ return pRes;
+ }
+ // the case when one of the cuts is the largest
+ if ( nLeaves0 == Limit )
+ {
+ for ( i = 0; i < nLeaves1; i++ )
+ {
+ for ( k = nLeaves0 - 1; k >= 0; k-- )
+ if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+ break;
+ if ( k == -1 ) // did not find
+ return NULL;
+ }
+ pRes = Cut_CutAlloc( p );
+ for ( i = 0; i < nLeaves0; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = nLeaves0;
+ return pRes;
+ }
+ // other cases
+ nNodes = nLeaves0;
+ for ( i = 0; i < nLeaves1; i++ )
+ {
+ for ( k = nLeaves0 - 1; k >= 0; k-- )
+ {
+ if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
+ continue;
+ if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
+ {
+ pRow = M[k+1];
+ if ( pRow[0] == 0 )
+ pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+ else if ( pRow[1] == 0 )
+ pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+ else if ( pRow[2] == 0 )
+ pRow[2] = pCut1->pLeaves[i];
+ else
+ assert( 0 );
+ if ( ++nNodes > Limit )
+ {
+ for ( i = 0; i <= nLeaves0; i++ )
+ M[i][0] = 0;
+ return NULL;
+ }
+ }
+ break;
+ }
+ if ( k == -1 )
+ {
+ pRow = M[0];
+ if ( pRow[0] == 0 )
+ pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+ else if ( pRow[1] == 0 )
+ pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+ else if ( pRow[2] == 0 )
+ pRow[2] = pCut1->pLeaves[i];
+ else
+ assert( 0 );
+ if ( ++nNodes > Limit )
+ {
+ for ( i = 0; i <= nLeaves0; i++ )
+ M[i][0] = 0;
+ return NULL;
+ }
+ continue;
+ }
+ }
+
+ pRes = Cut_CutAlloc( p );
+ for ( Count = 0, i = 0; i <= nLeaves0; i++ )
+ {
+ if ( i > 0 )
+ pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
+ pRow = M[i];
+ if ( pRow[0] )
+ {
+ pRes->pLeaves[Count++] = pRow[0];
+ if ( pRow[1] )
+ {
+ pRes->pLeaves[Count++] = pRow[1];
+ if ( pRow[2] )
+ pRes->pLeaves[Count++] = pRow[2];
+ }
+ pRow[0] = 0;
+ }
+ }
+ assert( Count == nNodes );
+ pRes->nLeaves = nNodes;
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ Cut_Cut_t * pRes;
+ int * pLeaves;
+ int Limit, nLeaves0, nLeaves1;
+ int i, k, c;
+
+ assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+ // consider two cuts
+ nLeaves0 = pCut0->nLeaves;
+ nLeaves1 = pCut1->nLeaves;
+
+ // the case of the largest cut sizes
+ Limit = p->pParams->nVarsMax;
+ if ( nLeaves0 == Limit && nLeaves1 == Limit )
+ {
+ for ( i = 0; i < nLeaves0; i++ )
+ if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+ return NULL;
+ pRes = Cut_CutAlloc( p );
+ for ( i = 0; i < nLeaves0; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = pCut0->nLeaves;
+ return pRes;
+ }
+ // the case when one of the cuts is the largest
+ if ( nLeaves0 == Limit )
+ {
+ for ( i = 0; i < nLeaves1; i++ )
+ {
+ for ( k = nLeaves0 - 1; k >= 0; k-- )
+ if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+ break;
+ if ( k == -1 ) // did not find
+ return NULL;
+ }
+ pRes = Cut_CutAlloc( p );
+ for ( i = 0; i < nLeaves0; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = pCut0->nLeaves;
+ return pRes;
+ }
+
+ // prepare the cut
+ if ( p->pReady == NULL )
+ p->pReady = Cut_CutAlloc( p );
+ pLeaves = p->pReady->pLeaves;
+
+ // compare two cuts with different numbers
+ i = k = 0;
+ for ( c = 0; c < Limit; c++ )
+ {
+ if ( k == nLeaves1 )
+ {
+ if ( i == nLeaves0 )
+ {
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+ pLeaves[c] = pCut0->pLeaves[i++];
+ continue;
+ }
+ if ( i == nLeaves0 )
+ {
+ if ( k == nLeaves1 )
+ {
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+ pLeaves[c] = pCut1->pLeaves[k++];
+ continue;
+ }
+ if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+ {
+ pLeaves[c] = pCut0->pLeaves[i++];
+ continue;
+ }
+ if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+ {
+ pLeaves[c] = pCut1->pLeaves[k++];
+ continue;
+ }
+ pLeaves[c] = pCut0->pLeaves[i++];
+ k++;
+ }
+ if ( i < nLeaves0 || k < nLeaves1 )
+ return NULL;
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo3( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ Cut_Cut_t * pRes;
+ int * pLeaves;
+ int Limit, nLeaves0, nLeaves1;
+ int i, k, c;
+
+ assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+ // prepare the cut
+ if ( p->pReady == NULL )
+ p->pReady = Cut_CutAlloc( p );
+ pLeaves = p->pReady->pLeaves;
+
+ // consider two cuts
+ Limit = p->pParams->nVarsMax;
+ nLeaves0 = pCut0->nLeaves;
+ nLeaves1 = pCut1->nLeaves;
+ if ( nLeaves0 == Limit )
+ { // the case when one of the cuts is the largest
+ if ( nLeaves1 == Limit )
+ { // the case when both cuts are the largest
+ for ( i = 0; i < nLeaves0; i++ )
+ {
+ pLeaves[i] = pCut0->pLeaves[i];
+ if ( pLeaves[i] != pCut1->pLeaves[i] )
+ return NULL;
+ }
+ }
+ else
+ {
+ for ( i = k = 0; i < nLeaves0; i++ )
+ {
+ pLeaves[i] = pCut0->pLeaves[i];
+ if ( k == (int)nLeaves1 )
+ continue;
+ if ( pLeaves[i] < pCut1->pLeaves[k] )
+ continue;
+ if ( pLeaves[i] == pCut1->pLeaves[k++] )
+ continue;
+ return NULL;
+ }
+ if ( k < nLeaves1 )
+ return NULL;
+ }
+ p->pReady->nLeaves = nLeaves0;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+
+ // compare two cuts with different numbers
+ i = k = 0;
+ for ( c = 0; c < Limit; c++ )
+ {
+ if ( k == nLeaves1 )
+ {
+ if ( i == nLeaves0 )
+ {
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+ pLeaves[c] = pCut0->pLeaves[i++];
+ continue;
+ }
+ if ( i == nLeaves0 )
+ {
+ if ( k == nLeaves1 )
+ {
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+ pLeaves[c] = pCut1->pLeaves[k++];
+ continue;
+ }
+ if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+ {
+ pLeaves[c] = pCut0->pLeaves[i++];
+ continue;
+ }
+ if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+ {
+ pLeaves[c] = pCut1->pLeaves[k++];
+ continue;
+ }
+ pLeaves[c] = pCut0->pLeaves[i++];
+ k++;
+ }
+ if ( i < nLeaves0 || k < nLeaves1 )
+ return NULL;
+ p->pReady->nLeaves = c;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo4( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ Cut_Cut_t * pRes;
+ int * pLeaves;
+ int i, k, min, NodeTemp, Limit, nTotal;
+
+ assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+ // prepare the cut
+ if ( p->pReady == NULL )
+ p->pReady = Cut_CutAlloc( p );
+ pLeaves = p->pReady->pLeaves;
+
+ // consider two cuts
+ Limit = p->pParams->nVarsMax;
+ if ( pCut0->nLeaves == (unsigned)Limit )
+ { // the case when one of the cuts is the largest
+ if ( pCut1->nLeaves == (unsigned)Limit )
+ { // the case when both cuts are the largest
+ for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+ {
+ pLeaves[i] = pCut0->pLeaves[i];
+ if ( pLeaves[i] != pCut1->pLeaves[i] )
+ return NULL;
+ }
+ }
+ else
+ {
+ for ( i = k = 0; i < (int)pCut0->nLeaves; i++ )
+ {
+ pLeaves[i] = pCut0->pLeaves[i];
+ if ( k == (int)pCut1->nLeaves )
+ continue;
+ if ( pLeaves[i] < pCut1->pLeaves[k] )
+ continue;
+ if ( pLeaves[i] == pCut1->pLeaves[k++] )
+ continue;
+ return NULL;
+ }
+ if ( k < (int)pCut1->nLeaves )
+ return NULL;
+ }
+ p->pReady->nLeaves = pCut0->nLeaves;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+ }
+
+ // count the number of unique entries in pCut1
+ nTotal = pCut0->nLeaves;
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ // try to find this entry among the leaves of pCut0
+ for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+ if ( pCut1->pLeaves[i] == pCut0->pLeaves[k] )
+ break;
+ if ( k < (int)pCut0->nLeaves ) // found
+ continue;
+ // we found a new entry to add
+ if ( nTotal == Limit )
+ return NULL;
+ pLeaves[nTotal++] = pCut1->pLeaves[i];
+ }
+ // we know that the feasible cut exists
+
+ // add the starting entries
+ for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+ pLeaves[k] = pCut0->pLeaves[k];
+
+ // selection-sort the entries
+ for ( i = 0; i < nTotal - 1; i++ )
+ {
+ min = i;
+ for ( k = i+1; k < nTotal; k++ )
+ if ( pLeaves[k] < pLeaves[min] )
+ min = k;
+ NodeTemp = pLeaves[i];
+ pLeaves[i] = pLeaves[min];
+ pLeaves[min] = NodeTemp;
+ }
+ p->pReady->nLeaves = nTotal;
+ pRes = p->pReady; p->pReady = NULL;
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description [This procedure works.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
+ Cut_Cut_t * pRes;
+ int * pRow;
+ unsigned uSign0, uSign1;
+ int i, k, nNodes, Count;
+ unsigned Limit = p->pParams->nVarsMax;
+
+ assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+ // the case of the largest cut sizes
+ if ( pCut0->nLeaves == Limit && pCut1->nLeaves == Limit )
+ {
+ for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+ if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+ return NULL;
+ pRes = Cut_CutAlloc( p );
+ for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = pCut0->nLeaves;
+ return pRes;
+ }
+ // the case when one of the cuts is the largest
+ if ( pCut0->nLeaves == Limit )
+ {
+ if ( !p->pParams->fTruth )
+ {
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+ if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+ break;
+ if ( k == -1 ) // did not find
+ return NULL;
+ }
+ pRes = Cut_CutAlloc( p );
+ }
+ else
+ {
+ uSign1 = 0;
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+ if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+ {
+ uSign1 |= (1 << i);
+ break;
+ }
+ if ( k == -1 ) // did not find
+ return NULL;
+ }
+ pRes = Cut_CutAlloc( p );
+ pRes->uTruth = (uSign1 << 8);
+ }
+ for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+ pRes->pLeaves[i] = pCut0->pLeaves[i];
+ pRes->nLeaves = pCut0->nLeaves;
+ return pRes;
+ }
+ // other cases
+ nNodes = pCut0->nLeaves;
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+ {
+ if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
+ continue;
+ if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
+ {
+ pRow = M[k+1];
+ if ( pRow[0] == 0 )
+ pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+ else if ( pRow[1] == 0 )
+ pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+ else if ( pRow[2] == 0 )
+ pRow[2] = pCut1->pLeaves[i];
+ else
+ assert( 0 );
+ if ( ++nNodes > (int)Limit )
+ {
+ for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
+ M[i][0] = 0;
+ return NULL;
+ }
+ }
+ break;
+ }
+ if ( k == -1 )
+ {
+ pRow = M[0];
+ if ( pRow[0] == 0 )
+ pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+ else if ( pRow[1] == 0 )
+ pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+ else if ( pRow[2] == 0 )
+ pRow[2] = pCut1->pLeaves[i];
+ else
+ assert( 0 );
+ if ( ++nNodes > (int)Limit )
+ {
+ for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
+ M[i][0] = 0;
+ return NULL;
+ }
+ continue;
+ }
+ }
+
+ pRes = Cut_CutAlloc( p );
+ if ( !p->pParams->fTruth )
+ {
+ for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
+ {
+ if ( i > 0 )
+ pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
+ pRow = M[i];
+ if ( pRow[0] )
+ {
+ pRes->pLeaves[Count++] = pRow[0];
+ if ( pRow[1] )
+ {
+ pRes->pLeaves[Count++] = pRow[1];
+ if ( pRow[2] )
+ pRes->pLeaves[Count++] = pRow[2];
+ }
+ pRow[0] = 0;
+ }
+ }
+ assert( Count == nNodes );
+ pRes->nLeaves = nNodes;
+/*
+ // make sure that the cut is correct
+ {
+ for ( i = 1; i < (int)pRes->nLeaves; i++ )
+ if ( pRes->pLeaves[i-1] >= pRes->pLeaves[i] )
+ {
+ int v = 0;
+ }
+ }
+*/
+ return pRes;
+ }
+
+ uSign0 = uSign1 = 0;
+ for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
+ {
+ if ( i > 0 )
+ {
+ uSign0 |= (1 << Count);
+ pRes->pLeaves[Count++] = pCut1->pLeaves[i-1];
+ }
+ pRow = M[i];
+ if ( pRow[0] )
+ {
+ uSign1 |= (1 << Count);
+ pRes->pLeaves[Count++] = pRow[0];
+ if ( pRow[1] )
+ {
+ uSign1 |= (1 << Count);
+ pRes->pLeaves[Count++] = pRow[1];
+ if ( pRow[2] )
+ {
+ uSign1 |= (1 << Count);
+ pRes->pLeaves[Count++] = pRow[2];
+ }
+ }
+ pRow[0] = 0;
+ }
+ }
+ assert( Count == nNodes );
+ pRes->nLeaves = nNodes;
+ pRes->uTruth = (uSign1 << 8) | uSign0;
+ return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
new file mode 100644
index 00000000..6ce3b983
--- /dev/null
+++ b/src/opt/cut/cutNode.c
@@ -0,0 +1,623 @@
+/**CFile****************************************************************
+
+ FileName [cutNode.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Procedures to compute cuts for a node.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+#include "cutList.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node );
+static inline void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
+static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList );
+
+static void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+static void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
+
+// iterator through all the cuts of the list
+#define Cut_ListForEachCut( pList, pCut ) \
+ for ( pCut = pList; \
+ pCut; \
+ pCut = pCut->pNext )
+#define Cut_ListForEachCutStop( pList, pCut, pStop ) \
+ for ( pCut = pList; \
+ pCut != pStop; \
+ pCut = pCut->pNext )
+#define Cut_ListForEachCutSafe( pList, pCut, pCut2 ) \
+ for ( pCut = pList, \
+ pCut2 = pCut? pCut->pNext: NULL; \
+ pCut; \
+ pCut = pCut2, \
+ pCut2 = pCut? pCut->pNext: NULL )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns the pointer to the linked list of cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+{
+ return Vec_PtrEntry( p->vCuts, Node );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the pointer to the linked list of cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+ Vec_PtrWriteEntry( p->vCuts, Node, pList );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the trivial cut for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
+{
+ assert( Cut_NodeReadCuts(p, Node) == NULL );
+ Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the cuts at the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
+{
+ Cut_Cut_t * pList, * pCut, * pCut2;
+ pList = Cut_NodeReadCuts( p, Node );
+ if ( pList == NULL )
+ return;
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ Cut_NodeWriteCuts( p, Node, NULL );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
+{
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts by merging cuts at two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
+{
+ Cut_List_t SuperList;
+ Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
+ int i, Limit = p->pParams->nVarsMax;
+ int clk = clock();
+ assert( p->pParams->nVarsMax <= 6 );
+ // start the new list
+ Cut_ListStart( &SuperList );
+ // get the cut lists of children
+ pList0 = Cut_NodeReadCuts( p, Node0 );
+ pList1 = Cut_NodeReadCuts( p, Node1 );
+ assert( pList0 && pList1 );
+ // get the simultation bit of the node
+ p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
+ // set temporary variables
+ p->fCompl0 = fCompl0;
+ p->fCompl1 = fCompl1;
+ // find the point in the list where the max-var cuts begin
+ Cut_ListForEachCut( pList0, pStop0 )
+ if ( pStop0->nLeaves == (unsigned)Limit )
+ break;
+ Cut_ListForEachCut( pList1, pStop1 )
+ if ( pStop1->nLeaves == (unsigned)Limit )
+ break;
+ // start with the elementary cut
+ pTemp0 = Cut_CutCreateTriv( p, Node );
+ Cut_ListAdd( &SuperList, pTemp0 );
+ p->nCutsNode = 1;
+ // small by small
+ Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
+ Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
+ if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+ goto finish;
+ // all by large
+ Cut_ListForEachCut( pList0, pTemp0 )
+ Cut_ListForEachCut( pStop1, pTemp1 )
+ if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+ goto finish;
+ // all by large
+ Cut_ListForEachCut( pList1, pTemp1 )
+ Cut_ListForEachCut( pStop0, pTemp0 )
+ if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+ goto finish;
+ // large by large
+ Cut_ListForEachCut( pStop0, pTemp0 )
+ Cut_ListForEachCut( pStop1, pTemp1 )
+ {
+ assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit );
+ for ( i = 0; i < Limit; i++ )
+ if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
+ break;
+ if ( i < Limit )
+ continue;
+ if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+ goto finish;
+ }
+finish :
+ // set the list at the node
+ assert( Cut_NodeReadCuts(p, Node) == NULL );
+ pList0 = Cut_ListFinish( &SuperList );
+ Cut_NodeWriteCuts( p, Node, pList0 );
+ // clear the hash table
+ if ( p->pParams->fHash && !p->pParams->fSeq )
+ Cut_TableClear( p->tTable );
+ // consider dropping the fanins cuts
+ if ( p->pParams->fDrop )
+ {
+ Cut_NodeTryDroppingCuts( p, Node0 );
+ Cut_NodeTryDroppingCuts( p, Node1 );
+ }
+p->timeMerge += clock() - clk;
+ // filter the cuts
+clk = clock();
+ if ( p->pParams->fFilter )
+ Cut_CutFilter( p, pList0 );
+p->timeFilter += clock() - clk;
+ return pList0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Processes two cuts.]
+
+ Description [Returns 1 if the limit has been reached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
+{
+ Cut_Cut_t * pCut;
+ // merge the cuts
+ if ( pCut0->nLeaves >= pCut1->nLeaves )
+ pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
+ else
+ pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
+ if ( pCut == NULL )
+ return 0;
+ assert( pCut->nLeaves > 1 );
+ // add the root if sequential
+ if ( p->pParams->fSeq )
+ pCut->pLeaves[pCut->nLeaves] = Root;
+ // check the lookup table
+ if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
+ {
+ Cut_CutRecycle( p, pCut );
+ return 0;
+ }
+ // compute the truth table
+ if ( p->pParams->fTruth )
+ Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+ // add to the list
+ Cut_ListAdd( pSuperList, pCut );
+ // return status (0 if okay; 1 if exceeded the limit)
+ return ++p->nCutsNode == p->pParams->nKeepMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts by unioning cuts at a choice node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
+{
+ Cut_List_t SuperList;
+ Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
+ int i, k, Node, Root, Limit = p->pParams->nVarsMax;
+ int clk = clock();
+
+ assert( p->pParams->nVarsMax <= 6 );
+
+ // start the new list
+ Cut_ListStart( &SuperList );
+
+ // remember the root node to save the resulting cuts
+ Root = Vec_IntEntry( vNodes, 0 );
+ p->nCutsNode = 1;
+
+ // collect small cuts first
+ Vec_PtrClear( p->vTemp );
+ Vec_IntForEachEntry( vNodes, Node, i )
+ {
+ // get the cuts of this node
+ pList = Cut_NodeReadCuts( p, Node );
+ Cut_NodeWriteCuts( p, Node, NULL );
+ assert( pList );
+ // remember the starting point
+ pListStart = pList->pNext;
+ // save or recycle the elementary cut
+ if ( i == 0 )
+ Cut_ListAdd( &SuperList, pList ), pTop = pList;
+ else
+ Cut_CutRecycle( p, pList );
+ // save all the cuts that are smaller than the limit
+ Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+ {
+ if ( pCut->nLeaves == (unsigned)Limit )
+ {
+ Vec_PtrPush( p->vTemp, pCut );
+ break;
+ }
+ // check hash tables
+ if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
+ {
+ Cut_CutRecycle( p, pCut );
+ continue;
+ }
+ // set the complemented bit by comparing the first cut with the current cut
+ pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+ // add to the list
+ Cut_ListAdd( &SuperList, pCut );
+ if ( ++p->nCutsNode == p->pParams->nKeepMax )
+ {
+ // recycle the rest of the cuts of this node
+ Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ // recycle all cuts of other nodes
+ Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
+ Cut_NodeFreeCuts( p, Node );
+ // recycle the saved cuts of other nodes
+ Vec_PtrForEachEntry( p->vTemp, pList, k )
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ goto finish;
+ }
+ }
+ }
+ // collect larger cuts next
+ Vec_PtrForEachEntry( p->vTemp, pList, i )
+ {
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ {
+ if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
+ {
+ Cut_CutRecycle( p, pCut );
+ continue;
+ }
+ // set the complemented bit
+ pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+ // add to the list
+ Cut_ListAdd( &SuperList, pCut );
+ if ( ++p->nCutsNode == p->pParams->nKeepMax )
+ {
+ // recycle the rest of the cuts
+ Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ // recycle the saved cuts of other nodes
+ Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ goto finish;
+ }
+ }
+ }
+finish :
+ // set the cuts at the node
+ assert( Cut_NodeReadCuts(p, Root) == NULL );
+ pList = Cut_ListFinish( &SuperList );
+ Cut_NodeWriteCuts( p, Root, pList );
+ // clear the hash table
+ if ( p->pParams->fHash && !p->pParams->fSeq )
+ Cut_TableClear( p->tTable );
+p->timeUnion += clock() - clk;
+ // filter the cuts
+clk = clock();
+ if ( p->pParams->fFilter )
+ Cut_CutFilter( p, pList );
+p->timeFilter += clock() - clk;
+ return pList;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
+{
+ Cut_Cut_t * pCut;
+ // cut allocation
+ pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+ memset( pCut, 0, sizeof(Cut_Cut_t) );
+ pCut->nVarsMax = p->pParams->nVarsMax;
+ pCut->fSeq = p->pParams->fSeq;
+ pCut->fSimul = p->fSimul;
+ // statistics
+ p->nCutsAlloc++;
+ p->nCutsCur++;
+ if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
+ p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+{
+ Cut_Cut_t * pCut;
+ pCut = Cut_CutAlloc( p );
+ pCut->nLeaves = 1;
+ pCut->pLeaves[0] = Node;
+ if ( p->pParams->fTruth )
+ Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+ p->nCutsTriv++;
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+ p->nCutsDealloc++;
+ p->nCutsCur--;
+ if ( pCut->nLeaves == 1 )
+ p->nCutsTriv--;
+ Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Consider dropping cuts if they are useless by now.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
+{
+ int nFanouts;
+ assert( p->vFanCounts );
+ nFanouts = Vec_IntEntry( p->vFanCounts, Node );
+ assert( nFanouts > 0 );
+ if ( --nFanouts == 0 )
+ Cut_NodeFreeCuts( p, Node );
+ Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CutPrint( Cut_Cut_t * pCut )
+{
+ int i;
+ assert( pCut->nLeaves > 1 );
+ printf( "%d : {", pCut->nLeaves );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ printf( " %d", pCut->pLeaves[i] );
+ printf( " }" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Consider dropping cuts if they are useless by now.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ printf( "\n" );
+ printf( "%d : %5d %5d %5d %5d %5d\n",
+ pCut0->nLeaves,
+ pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1,
+ pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1,
+ pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1,
+ pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1,
+ pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
+ );
+ printf( "%d : %5d %5d %5d %5d %5d\n",
+ pCut1->nLeaves,
+ pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1,
+ pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1,
+ pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1,
+ pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1,
+ pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
+ );
+ if ( pCut == NULL )
+ printf( "Cannot merge\n" );
+ else
+ printf( "%d : %5d %5d %5d %5d %5d\n",
+ pCut->nLeaves,
+ pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1,
+ pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1,
+ pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1,
+ pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1,
+ pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
+ );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Filter the cuts using dominance.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
+{
+ Cut_Cut_t * pListR, ** ppListR = &pListR;
+ Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
+ int i, k;
+ // save the first cut
+ *ppListR = pList, ppListR = &pList->pNext;
+ // try to filter out other cuts
+ pPrev = pList;
+ Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
+ {
+ assert( pCut->nLeaves > 1 );
+ // go through all the previous cuts up to pCut
+ Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
+ {
+ if ( pDom->nLeaves >= pCut->nLeaves )
+ continue;
+ // check if every node in pDom is contained in pCut
+ for ( i = 0; i < (int)pDom->nLeaves; i++ )
+ {
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+ break;
+ if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+ break;
+ }
+ if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut
+ break;
+ }
+ if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
+ {
+ // make sure cuts are connected after removing
+ pPrev->pNext = pCut->pNext;
+/*
+ // report
+ printf( "Recycling cut: " );
+ Cut_CutPrint( pCut );
+ printf( "\n" );
+ printf( "As contained in: " );
+ Cut_CutPrint( pDom );
+ printf( "\n" );
+*/
+ // recycle the cut
+ Cut_CutRecycle( p, pCut );
+ }
+ else // pDom is NOT contained in pCut - save pCut
+ {
+ *ppListR = pCut, ppListR = &pCut->pNext;
+ pPrev = pCut;
+ }
+ }
+ *ppListR = NULL;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
new file mode 100644
index 00000000..869bd7b3
--- /dev/null
+++ b/src/opt/cut/cutSeq.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [cutSeq.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Sequential cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutTable.c b/src/opt/cut/cutTable.c
new file mode 100644
index 00000000..5dfaca7b
--- /dev/null
+++ b/src/opt/cut/cutTable.c
@@ -0,0 +1,253 @@
+/**CFile****************************************************************
+
+ FileName [cutTable.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Hashing cuts to prevent duplication.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct Cut_HashTableStruct_t_
+{
+ int nBins;
+ Cut_Cut_t ** pBins;
+ int nEntries;
+ int * pPlaces;
+ int nPlaces;
+ int timeLookup;
+};
+
+// iterator through all the cuts of the list
+#define Cut_TableListForEachCut( pList, pCut ) \
+ for ( pCut = pList; \
+ pCut; \
+ pCut = pCut->pData )
+#define Cut_TableListForEachCutSafe( pList, pCut, pCut2 ) \
+ for ( pCut = pList, \
+ pCut2 = pCut? pCut->pData: NULL; \
+ pCut; \
+ pCut = pCut2, \
+ pCut2 = pCut? pCut->pData: NULL )
+
+// primes used to compute the hash key
+static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };
+
+// hashing function
+static inline unsigned Cut_HashKey( Cut_Cut_t * pCut )
+{
+ unsigned i, uRes = pCut->nLeaves * s_HashPrimes[9];
+ for ( i = 0; i < pCut->nLeaves + pCut->fSeq; i++ )
+ uRes += s_HashPrimes[i] * pCut->pLeaves[i];
+ return uRes;
+}
+
+// hashing function
+static inline int Cut_CompareTwo( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
+{
+ unsigned i;
+ if ( pCut1->nLeaves != pCut2->nLeaves )
+ return 1;
+ for ( i = 0; i < pCut1->nLeaves; i++ )
+ if ( pCut1->pLeaves[i] != pCut2->pLeaves[i] )
+ return 1;
+ return 0;
+}
+
+static void Cut_TableResize( Cut_HashTable_t * pTable );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_HashTable_t * Cut_TableStart( int Size )
+{
+ Cut_HashTable_t * pTable;
+ pTable = ALLOC( Cut_HashTable_t, 1 );
+ memset( pTable, 0, sizeof(Cut_HashTable_t) );
+ // allocate the table
+ pTable->nBins = Cudd_PrimeCopy( Size );
+ pTable->pBins = ALLOC( Cut_Cut_t *, pTable->nBins );
+ memset( pTable->pBins, 0, sizeof(Cut_Cut_t *) * pTable->nBins );
+ pTable->pPlaces = ALLOC( int, pTable->nBins );
+ return pTable;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TableStop( Cut_HashTable_t * pTable )
+{
+ FREE( pTable->pPlaces );
+ free( pTable->pBins );
+ free( pTable );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check the existence of a cut in the lookup table]
+
+ Description [Returns 1 if the entry is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore )
+{
+ Cut_Cut_t * pEnt;
+ unsigned Key;
+ int clk = clock();
+
+ Key = Cut_HashKey(pCut) % pTable->nBins;
+ Cut_TableListForEachCut( pTable->pBins[Key], pEnt )
+ {
+ if ( !Cut_CompareTwo( pEnt, pCut ) )
+ {
+pTable->timeLookup += clock() - clk;
+ return 1;
+ }
+ }
+ if ( pTable->nEntries > 2 * pTable->nBins )
+ {
+ Cut_TableResize( pTable );
+ Key = Cut_HashKey(pCut) % pTable->nBins;
+ }
+ // remember the place
+ if ( fStore && pTable->pBins[Key] == NULL )
+ pTable->pPlaces[ pTable->nPlaces++ ] = Key;
+ // add the cut to the table
+ pCut->pData = pTable->pBins[Key];
+ pTable->pBins[Key] = pCut;
+ pTable->nEntries++;
+pTable->timeLookup += clock() - clk;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Stops the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TableClear( Cut_HashTable_t * pTable )
+{
+ int i;
+ assert( pTable->nPlaces <= pTable->nBins );
+ for ( i = 0; i < pTable->nPlaces; i++ )
+ {
+ assert( pTable->pBins[ pTable->pPlaces[i] ] );
+ pTable->pBins[ pTable->pPlaces[i] ] = NULL;
+ }
+ pTable->nPlaces = 0;
+ pTable->nEntries = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TableResize( Cut_HashTable_t * pTable )
+{
+ Cut_Cut_t ** pBinsNew;
+ Cut_Cut_t * pEnt, * pEnt2;
+ int nBinsNew, Counter, i, clk;
+ unsigned Key;
+
+clk = clock();
+ // get the new table size
+ nBinsNew = Cudd_PrimeCopy( 3 * pTable->nBins );
+ // allocate a new array
+ pBinsNew = ALLOC( Cut_Cut_t *, nBinsNew );
+ memset( pBinsNew, 0, sizeof(Cut_Cut_t *) * nBinsNew );
+ // rehash the entries from the old table
+ Counter = 0;
+ for ( i = 0; i < pTable->nBins; i++ )
+ Cut_TableListForEachCutSafe( pTable->pBins[i], pEnt, pEnt2 )
+ {
+ Key = Cut_HashKey(pEnt) % nBinsNew;
+ pEnt->pData = pBinsNew[Key];
+ pBinsNew[Key] = pEnt;
+ Counter++;
+ }
+ assert( Counter == pTable->nEntries );
+// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
+// PRT( "Time", clock() - clk );
+ // replace the table and the parameters
+ free( pTable->pBins );
+ pTable->pBins = pBinsNew;
+ pTable->nBins = nBinsNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_TableReadTime( Cut_HashTable_t * pTable )
+{
+ if ( pTable == NULL )
+ return 0;
+ return pTable->timeLookup;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
new file mode 100644
index 00000000..efacd456
--- /dev/null
+++ b/src/opt/cut/cutTruth.c
@@ -0,0 +1,322 @@
+/**CFile****************************************************************
+
+ FileName [cutTruth.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [K-feasible cut computation package.]
+
+ Synopsis [Incremental truth table computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+static void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+static void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ 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 [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+int clk = clock();
+ if ( pCut->nVarsMax == 4 )
+ Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
+ else if ( pCut->nVarsMax == 5 )
+ Cut_TruthCompute5( p, pCut, pCut0, pCut1 );
+ else // if ( pCut->nVarsMax == 6 )
+ Cut_TruthCompute6( p, pCut, pCut0, pCut1 );
+p->timeTruth += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ unsigned * puTruthCut0, * puTruthCut1;
+ unsigned uTruth0, uTruth1, uPhase;
+
+ puTruthCut0 = Cut_CutReadTruth(pCut0);
+ puTruthCut1 = Cut_CutReadTruth(pCut1);
+
+ uPhase = Cut_TruthPhase( pCut, pCut0 );
+ uTruth0 = Extra_TruthPerm4One( *puTruthCut0, uPhase );
+ uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
+
+ uPhase = Cut_TruthPhase( pCut, pCut1 );
+ uTruth1 = Extra_TruthPerm4One( *puTruthCut1, uPhase );
+ uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
+
+ uTruth1 = uTruth0 & uTruth1;
+ if ( pCut->fCompl )
+ uTruth1 = ~uTruth1;
+ if ( pCut->nVarsMax == 4 )
+ uTruth1 &= 0xFFFF;
+ Cut_CutWriteTruth( pCut, &uTruth1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ unsigned * puTruthCut0, * puTruthCut1;
+ unsigned uTruth0, uTruth1, uPhase;
+
+ puTruthCut0 = Cut_CutReadTruth(pCut0);
+ puTruthCut1 = Cut_CutReadTruth(pCut1);
+
+ uPhase = Cut_TruthPhase( pCut, pCut0 );
+ uTruth0 = Extra_TruthPerm5One( *puTruthCut0, uPhase );
+ uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
+
+ uPhase = Cut_TruthPhase( pCut, pCut1 );
+ uTruth1 = Extra_TruthPerm5One( *puTruthCut1, uPhase );
+ uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
+
+ uTruth1 = uTruth0 & uTruth1;
+ if ( pCut->fCompl )
+ uTruth1 = ~uTruth1;
+ Cut_CutWriteTruth( pCut, &uTruth1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ unsigned * puTruthCut0, * puTruthCut1;
+ unsigned uTruth0[2], uTruth1[2], uPhase;
+
+ puTruthCut0 = Cut_CutReadTruth(pCut0);
+ puTruthCut1 = Cut_CutReadTruth(pCut1);
+
+ uPhase = Cut_TruthPhase( pCut, pCut0 );
+ Extra_TruthPerm6One( puTruthCut0, uPhase, uTruth0 );
+ uTruth0[0] = p->fCompl0? ~uTruth0[0]: uTruth0[0];
+ uTruth0[1] = p->fCompl0? ~uTruth0[1]: uTruth0[1];
+
+ uPhase = Cut_TruthPhase( pCut, pCut1 );
+ Extra_TruthPerm6One( puTruthCut1, uPhase, uTruth1 );
+ uTruth1[0] = p->fCompl1? ~uTruth1[0]: uTruth1[0];
+ uTruth1[1] = p->fCompl1? ~uTruth1[1]: uTruth1[1];
+
+ uTruth1[0] = uTruth0[0] & uTruth1[0];
+ uTruth1[1] = uTruth0[1] & uTruth1[1];
+ if ( pCut->fCompl )
+ {
+ uTruth1[0] = ~uTruth0[0];
+ uTruth1[1] = ~uTruth0[1];
+ }
+ Cut_CutWriteTruth( pCut, uTruth1 );
+}
+
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+ unsigned uTruth0, uTruth1, uPhase;
+ int clk = clock();
+
+ assert( pCut->nVarsMax < 6 );
+
+ // assign the truth table
+ if ( pCut0->nLeaves == pCut->nLeaves )
+ uTruth0 = *Cut_CutReadTruth(pCut0);
+ else
+ {
+ assert( pCut0->nLeaves < pCut->nLeaves );
+ uPhase = Cut_TruthPhase( pCut, pCut0 );
+ if ( pCut->nVarsMax == 4 )
+ {
+ assert( pCut0->nLeaves < 4 );
+ assert( uPhase < 16 );
+ uTruth0 = p->pPerms43[pCut0->uTruth & 0xFF][uPhase];
+ }
+ else
+ {
+ assert( pCut->nVarsMax == 5 );
+ assert( pCut0->nLeaves < 5 );
+ assert( uPhase < 32 );
+ if ( pCut0->nLeaves == 4 )
+ {
+// Count4++;
+/*
+ if ( uPhase == 31-16 ) // 01111
+ uTruth0 = pCut0->uTruth;
+ else if ( uPhase == 31-8 ) // 10111
+ uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][0];
+ else if ( uPhase == 31-4 ) // 11011
+ uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][1];
+ else if ( uPhase == 31-2 ) // 11101
+ uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][2];
+ else if ( uPhase == 31-1 ) // 11110
+ uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][3];
+ else
+ assert( 0 );
+*/
+ uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
+ }
+ else
+ {
+// Count5++;
+// uTruth0 = p->pPerms53[pCut0->uTruth & 0xFF][uPhase];
+ uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
+ }
+ }
+ }
+ uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
+
+ // assign the truth table
+ if ( pCut1->nLeaves == pCut->nLeaves )
+ uTruth0 = *Cut_CutReadTruth(pCut1);
+ else
+ {
+ assert( pCut1->nLeaves < pCut->nLeaves );
+ uPhase = Cut_TruthPhase( pCut, pCut1 );
+ if ( pCut->nVarsMax == 4 )
+ {
+ assert( pCut1->nLeaves < 4 );
+ assert( uPhase < 16 );
+ uTruth1 = p->pPerms43[pCut1->uTruth & 0xFF][uPhase];
+ }
+ else
+ {
+ assert( pCut->nVarsMax == 5 );
+ assert( pCut1->nLeaves < 5 );
+ assert( uPhase < 32 );
+ if ( pCut1->nLeaves == 4 )
+ {
+// Count4++;
+/*
+ if ( uPhase == 31-16 ) // 01111
+ uTruth1 = pCut1->uTruth;
+ else if ( uPhase == 31-8 ) // 10111
+ uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][0];
+ else if ( uPhase == 31-4 ) // 11011
+ uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][1];
+ else if ( uPhase == 31-2 ) // 11101
+ uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][2];
+ else if ( uPhase == 31-1 ) // 11110
+ uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][3];
+ else
+ assert( 0 );
+*/
+ uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
+ }
+ else
+ {
+// Count5++;
+// uTruth1 = p->pPerms53[pCut1->uTruth & 0xFF][uPhase];
+ uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
+ }
+ }
+ }
+ uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
+ uTruth1 = uTruth0 & uTruth1;
+ if ( pCut->fCompl )
+ uTruth1 = ~uTruth1;
+ if ( pCut->nVarsMax == 4 )
+ uTruth1 &= 0xFFFF;
+ Cut_CutWriteTruth( pCut, &uTruth1 );
+p->timeTruth += clock() - clk;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make
new file mode 100644
index 00000000..1175b3f2
--- /dev/null
+++ b/src/opt/cut/module.make
@@ -0,0 +1,6 @@
+SRC += src/opt/cut/cutMan.c \
+ src/opt/cut/cutMerge.c \
+ src/opt/cut/cutNode.c \
+ src/opt/cut/cutSeq.c \
+ src/opt/cut/cutTable.c \
+ src/opt/cut/cutTruth.c
diff --git a/src/opt/fxu/module.make b/src/opt/fxu/module.make
index 331712d1..dd8acd40 100644
--- a/src/opt/fxu/module.make
+++ b/src/opt/fxu/module.make
@@ -1,12 +1,12 @@
-SRC += fxu.c \
- fxuCreate.c \
- fxuHeapD.c \
- fxuHeapS.c \
- fxuList.c \
- fxuMatrix.c \
- fxuPair.c \
- fxuPrint.c \
- fxuReduce.c \
- fxuSelect.c \
- fxuSingle.c \
- fxuUpdate.c
+SRC += src/opt/fxu/fxu.c \
+ src/opt/fxu/fxuCreate.c \
+ src/opt/fxu/fxuHeapD.c \
+ src/opt/fxu/fxuHeapS.c \
+ src/opt/fxu/fxuList.c \
+ src/opt/fxu/fxuMatrix.c \
+ src/opt/fxu/fxuPair.c \
+ src/opt/fxu/fxuPrint.c \
+ src/opt/fxu/fxuReduce.c \
+ src/opt/fxu/fxuSelect.c \
+ src/opt/fxu/fxuSingle.c \
+ src/opt/fxu/fxuUpdate.c
diff --git a/src/opt/rwr/module.make b/src/opt/rwr/module.make
index e97eb33e..fc72630f 100644
--- a/src/opt/rwr/module.make
+++ b/src/opt/rwr/module.make
@@ -1,6 +1,7 @@
-SRC += rwrCut.c \
- rwrEva.c \
- rwrExp.c \
- rwrLib.c \
- rwrMan.c \
- rwrUtil.c
+SRC += src/opt/rwr/rwrCut.c \
+ src/opt/rwr/rwrEva.c \
+ src/opt/rwr/rwrExp.c \
+ src/opt/rwr/rwrLib.c \
+ src/opt/rwr/rwrMan.c \
+ src/opt/rwr/rwrPrint.c \
+ src/opt/rwr/rwrUtil.c
diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c
index 209d6ee6..be512963 100644
--- a/src/opt/rwr/rwrCut.c
+++ b/src/opt/rwr/rwrCut.c
@@ -245,6 +245,8 @@ Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode )
}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 16:37:31 +0000