New logic sharing extraction.

6 files changed, 475 insertions, 55 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a5ce3f65..02104958 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -174,7 +174,7 @@ struct Gia_Man_t_
     // truth table computation for small functions
     int            nTtVars;       // truth table variables
     int            nTtWords;      // truth table words
-    Vec_Str_t *    vTtNums;       // object numbers
+    Vec_Int_t *    vTtNums;       // object numbers
     Vec_Int_t *    vTtNodes;      // internal nodes
     Vec_Ptr_t *    vTtInputs;     // truth tables for constant and primary inputs
     Vec_Wrd_t *    vTtMemory;     // truth tables for internal nodes
@@ -454,8 +454,8 @@ static inline void         Gia_ObjSetXorLevel( Gia_Man_t * p, Gia_Obj_t * pObj )
 static inline void         Gia_ObjSetMuxLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsMux(p,pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt( Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))), Gia_ObjLevel(p,Gia_ObjFanin2(p,pObj))) ); }
 static inline void         Gia_ObjSetGateLevel( Gia_Man_t * p, Gia_Obj_t * pObj ){ if ( Gia_ObjIsMux(p,pObj) ) Gia_ObjSetMuxLevel(p, pObj); else if ( Gia_ObjIsXor(pObj) ) Gia_ObjSetXorLevel(p, pObj); else if ( Gia_ObjIsAnd(pObj) ) Gia_ObjSetAndLevel(p, pObj); }
 
-static inline int          Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj )       { return (int)(unsigned char)Vec_StrGetEntry(p->vTtNums, Gia_ObjId(p,pObj));                  }
-static inline void         Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 && n < 254 ); Vec_StrSetEntry(p->vTtNums, Gia_ObjId(p,pObj), (char)n);   }
+static inline int          Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj )           { return Vec_IntGetEntry(p->vTtNums, Gia_ObjId(p,pObj));               }
+static inline void         Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 ); Vec_IntSetEntry(p->vTtNums, Gia_ObjId(p,pObj), n); }
 
 static inline int          Gia_ObjRefNumId( Gia_Man_t * p, int Id )            { return p->pRefs[Id];                              }
 static inline int          Gia_ObjRefIncId( Gia_Man_t * p, int Id )            { return p->pRefs[Id]++;                            }
@@ -931,7 +931,7 @@ extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_I
 extern void                Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName );
 /*=== giaBalance.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
-extern Gia_Man_t *         Gia_ManMultiExtract( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@@ -1193,7 +1193,7 @@ extern Gia_Man_t *         Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig
 /*=== giaTruth.c ===========================================================*/
 extern word                Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp );
 extern word                Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
-extern int                 Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern void                Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern word *              Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax );
 extern void                Gia_ObjComputeTruthTableStop( Gia_Man_t * p );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 8fbf63aa..afe22952 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -896,7 +896,7 @@ Gia_Man_t * Dam_ManMultiExtractInt( Gia_Man_t * pGia, int nNewNodesMax, int fVer
     Dam_ManFree( p );
     return pNew;
 }
-Gia_Man_t * Gia_ManMultiExtract( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew, * pNew1, * pNew2;
     if ( fVerbose )     Gia_ManPrintStats( p, NULL );
diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c
new file mode 100644
index 00000000..9a73ecf0
--- /dev/null
+++ b/src/aig/gia/giaFx.c
@@ -0,0 +1,442 @@
+/**CFile****************************************************************
+
+  FileName    [giaFx.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Interface to fast_extract package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaFx.c,v 1.00 2013/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "bool/kit/kit.h"
+#include "misc/vec/vecWec.h"
+#include "bool/dec/dec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create GIA for SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManGraphToAig( Gia_Man_t * p, Dec_Graph_t * pGraph )
+{
+    Dec_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
+    int i, iAnd0, iAnd1;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Abc_LitNotCond( 1, Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Abc_LitNotCond( Dec_GraphVar(pGraph)->iFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        iAnd0 = Abc_LitNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->iFunc, pNode->eEdge0.fCompl ); 
+        iAnd1 = Abc_LitNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->iFunc, pNode->eEdge1.fCompl ); 
+        pNode->iFunc = Gia_ManHashAnd( p, iAnd0, iAnd1 );
+    }
+    // complement the result if necessary
+    return Abc_LitNotCond( pNode->iFunc, Dec_GraphIsComplement(pGraph) );
+}
+int Gia_ManSopToAig( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves )
+{
+    int i, iAnd, iSum, Value, nFanins;
+    char * pCube;
+    // get the number of variables
+    nFanins = Kit_PlaGetVarNum(pSop);
+    // go through the cubes of the node's SOP
+    iSum = 0;
+    Kit_PlaForEachCube( pSop, nFanins, pCube )
+    {
+        // create the AND of literals
+        iAnd = 1;
+        Kit_PlaCubeForEachVar( pCube, Value, i )
+        {
+            assert( Vec_IntEntry(vLeaves, i) >= 0 );
+            if ( Value == '1' )
+                iAnd = Gia_ManHashAnd( p, iAnd, Vec_IntEntry(vLeaves, i) );
+            else if ( Value == '0' )
+                iAnd = Gia_ManHashAnd( p, iAnd, Abc_LitNot(Vec_IntEntry(vLeaves, i)) );
+            else assert( Value == '-' );
+        }
+        // add to the sum of cubes
+        iSum = Gia_ManHashOr( p, iSum, iAnd );
+    }
+    // decide whether to complement the result
+    if ( Kit_PlaIsComplement(pSop) )
+        iSum = Abc_LitNot(iSum);
+    return iSum;
+}
+int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves )
+{
+    if ( Kit_PlaGetVarNum(pSop) == 0 )
+        return Abc_LitNotCond( 1, Kit_PlaIsConst0(pSop) );
+    assert( Kit_PlaGetVarNum(pSop) == Vec_IntSize(vLeaves) );
+    if ( Kit_PlaGetVarNum(pSop) > 2 && Kit_PlaGetCubeNum(pSop) > 1 )
+    {
+        Dec_Graph_t * pFForm;
+        Dec_Node_t * pFFNode;
+        int i, Lit;
+        pFForm = Dec_Factor( pSop );
+        // assign fanins
+        Dec_GraphForEachLeaf( pFForm, pFFNode, i )
+        {
+            assert( Vec_IntEntry(vLeaves, i) >= 0 );
+            pFFNode->iFunc = Vec_IntEntry(vLeaves, i);
+        }
+        // perform strashing
+        Lit = Gia_ManGraphToAig( p, pFForm );
+        Dec_GraphFree( pFForm );
+        return Lit;
+    }
+    return Gia_ManSopToAig( p, pSop, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing truth tables for the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Gia_ManComputeTruths( Gia_Man_t * p, int nCutSize, int nLutNum )
+{
+    Vec_Wrd_t * vTruths;
+    Vec_Int_t vLeaves;
+    word * pTruth;
+    int i, k, nWords;
+    nWords = Abc_Truth6WordNum( nCutSize );
+    vTruths = Vec_WrdAlloc( nWords * nLutNum );
+    Gia_ObjComputeTruthTableStart( p, nCutSize );
+    Gia_ManForEachLut( p, i )
+    {
+        // collect and sort fanins
+        vLeaves.nCap = vLeaves.nSize = Gia_ObjLutSize( p, i );
+        vLeaves.pArray = Gia_ObjLutFanins( p, i );
+        assert( Vec_IntCheckUniqueSmall(&vLeaves) );
+        Vec_IntSelectSort( Vec_IntArray(&vLeaves), Vec_IntSize(&vLeaves) );
+        // compute truth table
+        pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, i), &vLeaves );
+        for ( k = 0; k < nWords; k++ )
+            Vec_WrdPush( vTruths, pTruth[k] );
+//        Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
+    }
+    Gia_ObjComputeTruthTableStop( p );
+    assert( Vec_WrdCap(vTruths) == 16 || Vec_WrdSize(vTruths) == Vec_WrdCap(vTruths) );
+    return vTruths;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts information about the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManAssignNumbers( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManFillValue( p );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Counter++;
+    Gia_ManForEachLut( p, i )
+        Gia_ManObj(p, i)->Value = Counter++;
+    return Counter;
+}
+Vec_Wec_t * Gia_ManFxRetrieve( Gia_Man_t * p, Vec_Str_t ** pvCompl )
+{
+    Vec_Wec_t * vCubes;
+    Vec_Wrd_t * vTruths;
+    Vec_Int_t * vCube, * vCover;
+    int nItems, nCutSize, nWords;
+    int i, c, v, Lit, Cube, Counter = 0;
+    abctime clk = Abc_Clock();
+    nItems = Gia_ManAssignNumbers( p );
+    // compute truth tables
+    nCutSize = Gia_ManLutSizeMax( p );
+    nWords = Abc_Truth6WordNum( nCutSize );
+    vTruths = Gia_ManComputeTruths( p, Abc_MaxInt(6, nCutSize), nItems - Gia_ManCiNum(p) );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    // collect cubes
+    vCubes = Vec_WecAlloc( 1000 );
+    *pvCompl = Vec_StrStart( nItems );
+    Gia_ManForEachLut( p, i )
+    {
+        Gia_Obj_t * pObj = Gia_ManObj( p, i );
+        int nVars = Gia_ObjLutSize( p, i );
+        int * pVars = Gia_ObjLutFanins( p, i );
+        word * pTruth = Vec_WrdEntryP( vTruths, Counter++ * nWords );
+        int Status = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 1 );
+        if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
+        {
+            Vec_StrWriteEntry( *pvCompl, pObj->Value, (char)(Vec_IntSize(vCover) == 0) );
+            vCube = Vec_WecPushLevel( vCubes );
+            Vec_IntPush( vCube, pObj->Value );
+            continue;
+        }
+        Vec_StrWriteEntry( *pvCompl, pObj->Value, (char)Status );
+        Vec_IntForEachEntry( vCover, Cube, c )
+        {
+            vCube = Vec_WecPushLevel( vCubes );
+            Vec_IntPush( vCube, pObj->Value );
+            for ( v = 0; v < nVars; v++ )
+            {
+                Lit = 3 & (Cube >> (v << 1));
+                if ( Lit == 1 )
+                    Vec_IntPush( vCube, Abc_Var2Lit(Gia_ManObj(p, pVars[v])->Value, 1) );
+                else if ( Lit == 2 )
+                    Vec_IntPush( vCube, Abc_Var2Lit(Gia_ManObj(p, pVars[v])->Value, 0) );
+                else if ( Lit != 0 )
+                    assert( 0 );
+            }
+            Vec_IntSelectSort( Vec_IntArray(vCube) + 1, Vec_IntSize(vCube) - 1 );
+        }        
+    }
+    assert( Counter * nWords == Vec_WrdSize(vTruths) );
+    Vec_WrdFree( vTruths );
+    Vec_IntFree( vCover );
+    Abc_PrintTime( 1, "Setup time", Abc_Clock() - clk );
+    return vCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates GIA after factoring the resulting SOPs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFxTopoOrder_rec( Vec_Wec_t * vCubes, Vec_Int_t * vFirst, Vec_Int_t * vCount, Vec_Int_t * vVisit, Vec_Int_t * vOrder, int iObj )
+{
+    int c, v, Lit;
+    int iFirst = Vec_IntEntry( vFirst, iObj );
+    int nCubes = Vec_IntEntry( vCount, iObj ); 
+    assert( !Vec_IntEntry( vVisit, iObj ) );
+    Vec_IntWriteEntry( vVisit, iObj, 1 );
+    for ( c = 0; c < nCubes; c++ )
+    {
+        Vec_Int_t * vCube = Vec_WecEntry( vCubes, iFirst + c );
+        assert( Vec_IntEntry(vCube, 0) == iObj );
+        Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+            if ( !Vec_IntEntry( vVisit, Abc_Lit2Var(Lit) ) )
+                Gia_ManFxTopoOrder_rec( vCubes, vFirst, vCount, vVisit, vOrder, Abc_Lit2Var(Lit) );
+    }
+    Vec_IntPush( vOrder, iObj );
+}
+Vec_Int_t * Gia_ManFxTopoOrder( Vec_Wec_t * vCubes, int nInputs, int nStart, Vec_Int_t ** pvFirst, Vec_Int_t ** pvCount )
+{
+    Vec_Int_t * vOrder, * vFirst, * vCount, * vVisit, * vCube;
+    int i, iFanin, nNodeMax = -1;
+    // find the largest index
+    Vec_WecForEachLevel( vCubes, vCube, i )
+        nNodeMax = Abc_MaxInt( nNodeMax, Vec_IntEntry(vCube, 0) );
+    nNodeMax++;
+    // quit if there is no new nodes
+    if ( nNodeMax == nStart )
+    {
+        printf( "The network is unchanged by fast extract.\n" );
+        return NULL;
+    }
+    // find first cube and how many cubes
+    vFirst = Vec_IntStart( nNodeMax );
+    vCount = Vec_IntStart( nNodeMax );
+    Vec_WecForEachLevel( vCubes, vCube, i )
+    {
+        iFanin = Vec_IntEntry( vCube, 0 );
+        assert( iFanin >= nInputs );
+        if ( Vec_IntEntry(vCount, iFanin) == 0 )
+            Vec_IntWriteEntry( vFirst, iFanin, i );
+        Vec_IntAddToEntry( vCount, iFanin, 1 );
+    }
+    // put all of them in a topo order
+    vOrder = Vec_IntStart( nInputs );
+    vVisit = Vec_IntStart( nNodeMax );
+    for ( i = 0; i < nInputs; i++ )
+        Vec_IntWriteEntry( vVisit, i, 1 );
+    for ( i = nInputs; i < nNodeMax; i++ )
+        if ( !Vec_IntEntry( vVisit, i ) )
+            Gia_ManFxTopoOrder_rec( vCubes, vFirst, vCount, vVisit, vOrder, i );
+    assert( Vec_IntSize(vOrder) == nNodeMax );
+    Vec_IntFree( vVisit );
+    // return topological order of new nodes
+    *pvFirst = vFirst;
+    *pvCount = vCount;
+    return vOrder;
+}
+Gia_Man_t * Gia_ManFxInsert( Gia_Man_t * p, Vec_Wec_t * vCubes, Vec_Str_t * vCompls )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj; Vec_Str_t * vSop;
+    Vec_Int_t * vOrder, * vFirst, * vCount, * vFanins;
+    Vec_Int_t * vCopies, * vCube, * vMap;
+    int k, c, v, Lit, Var, iItem;
+    abctime clk = Abc_Clock();
+    // prepare the cubes
+    vOrder = Gia_ManFxTopoOrder( vCubes, Gia_ManCiNum(p), Vec_StrSize(vCompls), &vFirst, &vCount );
+    if ( vOrder == NULL )
+        return Gia_ManDup( p );
+    assert( Vec_IntSize(vOrder) > Vec_StrSize(vCompls) );
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashStart( pNew );
+    // create primary inputs
+    vMap = Vec_IntStartFull( Vec_IntSize(vOrder) );
+    vCopies = Vec_IntAlloc( Vec_IntSize(vOrder) );
+    Gia_ManForEachCi( p, pObj, k )
+        Vec_IntPush( vCopies, Gia_ManAppendCi(pNew) );
+    Vec_IntFillExtra( vCopies, Vec_IntSize(vOrder), -1 );
+    // add AIG nodes in the topological order
+    vSop = Vec_StrAlloc( 1000 );
+    vFanins = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntryStart( vOrder, iItem, k, Gia_ManCiNum(p) )
+    {
+        int iFirst = Vec_IntEntry( vFirst, iItem );
+        int nCubes = Vec_IntEntry( vCount, iItem );
+        // collect fanins
+        Vec_IntClear( vFanins );
+        for ( c = 0; c < nCubes; c++ )
+        {
+            vCube = Vec_WecEntry( vCubes, iFirst + c );
+            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+                if ( Vec_IntEntry(vMap, Abc_Lit2Var(Lit)) == -1 )
+                {
+                    Vec_IntWriteEntry( vMap, Abc_Lit2Var(Lit), Vec_IntSize(vFanins) );
+                    Vec_IntPush( vFanins, Abc_Lit2Var(Lit) );
+                }
+        }
+        // create SOPs
+        Vec_StrClear( vSop );
+        for ( c = 0; c < nCubes; c++ )
+        {
+            for ( v = 0; v < Vec_IntSize(vFanins); v++ )
+                Vec_StrPush( vSop, '-' );
+            vCube = Vec_WecEntry( vCubes, iFirst + c );
+            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+            {
+                Lit = Abc_Lit2LitV( Vec_IntArray(vMap), Lit );
+                assert( Lit >= 0 && Abc_Lit2Var(Lit) < Vec_IntSize(vFanins) );
+                Vec_StrWriteEntry( vSop, Vec_StrSize(vSop) - Vec_IntSize(vFanins) + Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)? '0' : '1') );
+            }
+            Vec_StrPush( vSop, ' ' );
+            Vec_StrPush( vSop, '1' );
+            Vec_StrPush( vSop, '\n' );
+        }
+        Vec_StrPush( vSop, '\0' );
+        // collect fanins
+        Vec_IntForEachEntry( vFanins, Var, v )
+        {
+            Vec_IntWriteEntry( vMap, Var, -1 );
+            Vec_IntWriteEntry( vFanins, v, Vec_IntEntry(vCopies, Var) );
+        }
+        // derive new AIG
+        Lit = Gia_ManFactorNode( pNew, Vec_StrArray(vSop), vFanins );
+        Lit = Abc_LitNotCond( Lit, (iItem < Vec_StrSize(vCompls)) && (Vec_StrEntry(vCompls, iItem) > 0) );
+        // remeber this literal
+        assert( Vec_IntEntry(vCopies, iItem) == -1 );
+        Vec_IntWriteEntry( vCopies, iItem, Lit );
+    }
+    Gia_ManHashStop( pNew );
+    // create primary outputs
+    Gia_ManForEachCo( p, pObj, k )
+    {
+        Lit = Gia_ObjFaninId0p(p, pObj) ? Vec_IntEntry(vCopies, Gia_ObjFanin0(pObj)->Value) : 0;
+        Gia_ManAppendCo( pNew, Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObj) ) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // cleanup
+    Vec_IntFree( vOrder );
+    Vec_IntFree( vFirst );
+    Vec_IntFree( vCount );
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vCopies );
+    Vec_IntFree( vMap );
+    Vec_StrFree( vSop );
+    // remove dangling nodes
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Abc_PrintTime( 1, "Setdn time", Abc_Clock() - clk );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs classical fast_extract on logic functions.]
+
+  Description []
+               
+  SideEffects [Sorts the fanins of each cut in the increasing order.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose )
+{
+    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose );
+    Gia_Man_t * pNew = NULL;
+    Vec_Wec_t * vCubes;
+    Vec_Str_t * vCompl;
+    abctime clk;
+    assert( Gia_ManHasMapping(p) );   
+    // collect information
+    vCubes = Gia_ManFxRetrieve( p, &vCompl );
+    // call the fast extract procedure
+    clk = Abc_Clock();
+    Fx_FastExtract( vCubes, Vec_StrSize(vCompl), nNewNodesMax, LitCountMax, fVerbose, fVeryVerbose );
+    Abc_PrintTime( 1, "Fx runtime", Abc_Clock() - clk );
+    // insert information
+    pNew = Gia_ManFxInsert( p, vCubes, vCompl );
+    // cleanup
+    Vec_WecFree( vCubes );
+    Vec_StrFree( vCompl );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 5df2faa5..e57fe27d 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -95,7 +95,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vDoms );
     Vec_IntFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vTruths );
-    Vec_StrFreeP( &p->vTtNums );
+    Vec_IntFreeP( &p->vTtNums );
     Vec_IntFreeP( &p->vTtNodes );
     Vec_WrdFreeP( &p->vTtMemory );
     Vec_PtrFreeP( &p->vTtInputs );
diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
index 0ba2f244..043e4c5f 100644
--- a/src/aig/gia/giaTruth.c
+++ b/src/aig/gia/giaTruth.c
@@ -38,8 +38,8 @@ static word s_Truth6[6] = {
 
 static inline word * Gla_ObjTruthElem( Gia_Man_t * p, int i )            { return (word *)Vec_PtrEntry( p->vTtInputs, i );                                           }
 static inline word * Gla_ObjTruthNode( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjNum(p, pObj);                    }
-static inline word * Gla_ObjTruthFree1( Gia_Man_t * p )                  { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * 254;                                    }
-static inline word * Gla_ObjTruthFree2( Gia_Man_t * p )                  { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * 255;                                    }
+static inline word * Gla_ObjTruthFree1( Gia_Man_t * p )                  { return Vec_WrdArray(p->vTtMemory) + Vec_WrdSize(p->vTtMemory) - p->nTtWords * 1;          }
+static inline word * Gla_ObjTruthFree2( Gia_Man_t * p )                  { return Vec_WrdArray(p->vTtMemory) + Vec_WrdSize(p->vTtMemory) - p->nTtWords * 2;          }
 static inline word * Gla_ObjTruthConst0( Gia_Man_t * p, word * pDst )                   { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = 0; return pDst;                      }
 static inline word * Gla_ObjTruthDup( Gia_Man_t * p, word * pDst, word * pSrc, int c )  { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = c ? ~pSrc[w] : pSrc[w]; return pDst; }
 
@@ -143,28 +143,22 @@ word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSu
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( !Gia_ObjIsAnd(pObj) )
-        return 0;
+        return;
     if ( pObj->fMark0 )
-        return 0;
+        return;
     pObj->fMark0 = 1;
     Gia_ObjCollectInternal_rec( p, Gia_ObjFanin0(pObj) );
     Gia_ObjCollectInternal_rec( p, Gia_ObjFanin1(pObj) );
-    if ( Vec_IntSize(p->vTtNodes) > 253 )
-        return 1;
     Gia_ObjSetNum( p, pObj, Vec_IntSize(p->vTtNodes) );
     Vec_IntPush( p->vTtNodes, Gia_ObjId(p, pObj) );
-    return 0;
 }
-int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
-    int RetValue;
     Vec_IntClear( p->vTtNodes );
-    RetValue = Gia_ObjCollectInternal_rec( p, pObj );
-    assert( Vec_IntSize(p->vTtNodes) < 254 );
-    return RetValue;
+    Gia_ObjCollectInternal_rec( p, pObj );
 }
 
 /**Function*************************************************************
@@ -188,7 +182,7 @@ word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
     {
         p->nTtVars   = Gia_ManPiNum( p );
         p->nTtWords  = (p->nTtVars <= 6 ? 1 : (1 << (p->nTtVars - 6)));
-        p->vTtNums   = Vec_StrAlloc( Gia_ManObjNum(p) + 1000 );
+        p->vTtNums   = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
         p->vTtNodes  = Vec_IntAlloc( 256 );
         p->vTtInputs = Vec_PtrAllocTruthTables( p->nTtVars );
         p->vTtMemory = Vec_WrdStart( p->nTtWords * 256 );
@@ -201,13 +195,10 @@ word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
     }
     // collect internal nodes
     pRoot = Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj;
-    if ( Gia_ObjCollectInternal( p, pRoot ) )
-    {
-        Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
-            pTemp->fMark0 = 0;
-        return NULL;
-    }
+    Gia_ObjCollectInternal( p, pRoot );
     // compute the truth table for internal nodes
+    if ( Vec_WrdSize(p->vTtMemory) < p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2) )
+        Vec_WrdFillExtra( p->vTtMemory, p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2), 0 );
     Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
     {
         pTemp->fMark0 = 0; // unmark nodes marked by Gia_ObjCollectInternal()
@@ -283,21 +274,18 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ObjCollectInternalCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ObjCollectInternalCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( pObj->fMark0 )
-        return 0;
-    assert( Gia_ObjIsAnd(pObj) );
-    if ( Gia_ObjCollectInternalCut_rec( p, Gia_ObjFanin0(pObj) ) )
-        return 1;
-    if ( Gia_ObjCollectInternalCut_rec( p, Gia_ObjFanin1(pObj) ) )
-        return 1;
+        return;
     pObj->fMark0 = 1;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ObjCollectInternalCut_rec( p, Gia_ObjFanin0(pObj) );
+    Gia_ObjCollectInternalCut_rec( p, Gia_ObjFanin1(pObj) );
     Gia_ObjSetNum( p, pObj, Vec_IntSize(p->vTtNodes) );
     Vec_IntPush( p->vTtNodes, Gia_ObjId(p, pObj) );
-    return (Vec_IntSize(p->vTtNodes) >= 254);
 }
-int Gia_ObjCollectInternalCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
+void Gia_ObjCollectInternalCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
 {
     Gia_Obj_t * pObj;
     int i;
@@ -311,7 +299,7 @@ int Gia_ObjCollectInternalCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLe
     }
     assert( pRoot->fMark0 == 0 ); // the root cannot be one of the leaves
     Vec_IntClear( p->vTtNodes );
-    return Gia_ObjCollectInternalCut_rec( p, pRoot );
+    Gia_ObjCollectInternalCut_rec( p, pRoot );
 }
 
 /**Function*************************************************************
@@ -329,17 +317,17 @@ void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax )
 {
     assert( p->vTtMemory == NULL );
     p->nTtVars   = nVarsMax;
-    p->nTtWords  = (p->nTtVars <= 6 ? 1 : (1 << (p->nTtVars - 6)));
-    p->vTtNums   = Vec_StrAlloc( Gia_ManObjNum(p) + 1000 );
+    p->nTtWords  = Abc_Truth6WordNum( p->nTtVars );
+    p->vTtNums   = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
     p->vTtNodes  = Vec_IntAlloc( 256 );
     p->vTtInputs = Vec_PtrAllocTruthTables( p->nTtVars );
-    p->vTtMemory = Vec_WrdStart( p->nTtWords * 256 );
+    p->vTtMemory = Vec_WrdStart( p->nTtWords * 64 );
 }
 void Gia_ObjComputeTruthTableStop( Gia_Man_t * p )
 {
     p->nTtVars   = 0;
     p->nTtWords  = 0;
-    Vec_StrFreeP( &p->vTtNums );
+    Vec_IntFreeP( &p->vTtNums );
     Vec_IntFreeP( &p->vTtNodes );
     Vec_PtrFreeP( &p->vTtInputs );
     Vec_WrdFreeP( &p->vTtMemory );
@@ -364,21 +352,10 @@ word * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t
     assert( p->vTtMemory != NULL );
     assert( Vec_IntSize(vLeaves) <= p->nTtVars );
     // collect internal nodes
-    if ( Gia_ObjCollectInternalCut( p, pRoot, vLeaves ) )
-    {
-        // unmark nodes makred by Gia_ObjCollectInternal()
-        Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
-            pTemp->fMark0 = 0; 
-        // unmark leaves marked by Gia_ObjCollectInternal()
-        Gia_ManForEachObjVec( vLeaves, p, pTemp, i )
-        {
-            assert( pTemp->fMark0 == 1 );
-            pTemp->fMark0 = 0; 
-        }
-        return NULL;
-    }
+    Gia_ObjCollectInternalCut( p, pRoot, vLeaves );
     // compute the truth table for internal nodes
-    assert( Vec_IntSize(p->vTtNodes) < 254 );
+    if ( Vec_WrdSize(p->vTtMemory) < p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2) )
+        Vec_WrdFillExtra( p->vTtMemory, p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2), 0 );
     Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
     {
         pTemp->fMark0 = 0; // unmark nodes marked by Gia_ObjCollectInternal()
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 1bac1d4b..cf12b835 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -21,6 +21,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaForce.c \
     src/aig/gia/giaFrames.c \
     src/aig/gia/giaFront.c \
+    src/aig/gia/giaFx.c \
     src/aig/gia/giaGlitch.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaIf.c \