Improvements to LMS code.

src/aig/gia/gia.h

@@ -890,10 +890,10 @@ extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
 /*=== giaTruth.c ===========================================================*/
 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 unsigned *          Gia_ObjComputeTruthTable( 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 );
-extern unsigned *          Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves );
+extern word *              Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves );
 /*=== giaTsim.c ============================================================*/
 extern Gia_Man_t *         Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
 /*=== giaUtil.c ===========================================================*/
@@ -932,6 +932,7 @@ extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManPrint( Gia_Man_t * p );
+extern void                Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern void                Gia_ManMarkFanoutDrivers( Gia_Man_t * p );

src/aig/gia/giaTruth.c

@@ -141,7 +141,7 @@ int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
+word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     Gia_Obj_t * pTemp, * pRoot;
     word * pTruth, * pTruthL, * pTruth0, * pTruth1;
@@ -205,7 +205,7 @@ unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
         pTruth = Gla_ObjTruthNode( p, pRoot );
     else
         pTruth = NULL;
-    return (unsigned *)Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) );
+    return Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) );
 }
 
 /**Function*************************************************************
@@ -227,7 +227,7 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
     int i;
     Gia_ManForEachPo( p, pObj, i )
     {
-        pTruth = Gia_ObjComputeTruthTable( p, pObj );
+        pTruth = (unsigned *)Gia_ObjComputeTruthTable( p, pObj );
 //        Extra_PrintHex( stdout, pTruth, Gia_ManPiNum(p) ); printf( "\n" );
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
@@ -316,7 +316,7 @@ void Gia_ObjComputeTruthTableStop( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
+word * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
 {
     Gia_Obj_t * pTemp;
     word * pTruth, * pTruthL, * pTruth0, * pTruth1;
@@ -358,7 +358,7 @@ unsigned * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_In
         assert( pTemp->fMark0 == 1 );
         pTemp->fMark0 = 0; 
     }
-    return (unsigned *)Gla_ObjTruthNode( p, pRoot );
+    return Gla_ObjTruthNode( p, pRoot );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaUtil.c

@@ -1109,6 +1109,22 @@ void Gia_ManPrint( Gia_Man_t * p )
     Gia_ManForEachObj( p, pObj, i )
         Gia_ObjPrint( p, pObj );
 }
+void Gia_ManPrintCo_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
+        Gia_ManPrintCo_rec( p, Gia_ObjFanin1(pObj) );
+    }
+    Gia_ObjPrint( p, pObj );
+}
+void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsCo(pObj) );
+    printf( "TFI cone of CO number %d:\n", Gia_ObjCioId(pObj) );
+    Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
+    Gia_ObjPrint( p, pObj );
+}
 
 /**Function*************************************************************
 

src/base/abci/abcRec2.c

@@ -1107,7 +1107,7 @@ void Abc_NtkRecStart2( Gia_Man_t * pGia, int nVars, int nCuts, int fTrim )
 clk = clock();
 //     Gia_ManForEachPo( pGia, pObj, i )
 //     {
-//         pTruthSrc = Gia_ObjComputeTruthTable(pGia, pObj);
+//         pTruthSrc = (unsigned *)Gia_ObjComputeTruthTable(pGia, pObj);
 // //        pTruthDst = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
 // //        Kit_TruthCopy(pTruthDst, pTruthSrc, p->nVars);
 //         Rec_MemSetEntry( p, Gia_ObjCioId(pObj), pTruthSrc );
@@ -1125,7 +1125,7 @@ timeInsert = clock();
         assert(pFanin->fMark1 == 0);
         pFanin->fMark1 = 1;
 //        pTruth = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
-        pTruth = Gia_ObjComputeTruthTable(pGia, pObj);
+        pTruth = (unsigned *)Gia_ObjComputeTruthTable(pGia, pObj);
 
         //pTruth = Rec_MemReadEntry( p, Gia_ObjCioId(pObj) );
         // add the resulting truth table to the hash table 
@@ -1569,7 +1569,7 @@ timeBuild = clock();
     }
     //assert(pObj);
     pObj = Gia_ManObj(pAig, Abc_Lit2Var(iRecObj));
-    pTruth = Gia_ObjComputeTruthTable(pAig, pObj);
+    pTruth = (unsigned *)Gia_ObjComputeTruthTable(pAig, pObj);
 s_pMan->timeBuild += clock() - timeBuild;
     
     if ( Kit_TruthSupport(pTruth, nInputs) != Kit_BitMask(nLeaves) )
@@ -2349,7 +2349,7 @@ void Abc_NtkRecAddFromLib2( Gia_Man_t * pGia2, Gia_Obj_t * pRoot, int nVars )
         Gia_ObjSetCopyF(pGia2, 0, pAbcObj, Gia_ObjId(pGia,pObj));
     }
     assert(pObj);
-    pTruth = Gia_ObjComputeTruthTable(pGia, pObj);
+    pTruth = (unsigned *)Gia_ObjComputeTruthTable(pGia, pObj);
     //pTruth = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, Gia_ObjId(pGia, pObj) );
     assert ( Kit_TruthSupport(pTruth, nInputs) == Kit_BitMask(nLeaves) );
     // compare the truth tables

src/base/abci/abcRec3.c

@@ -28,6 +28,8 @@
 
 ABC_NAMESPACE_IMPL_START
 
+#define LMS_VAR_MAX    16  // LMS_VAR_MAX >= 6
+#define LMS_MAX_WORD  (1<<(LMS_VAR_MAX-6))
 //#define LMS_USE_OLD_FORM
 
 ////////////////////////////////////////////////////////////////////////
@@ -38,10 +40,9 @@ ABC_NAMESPACE_IMPL_START
     This LMS manager can be used in two modes:
         - library constuction
         - AIG level minimization
-
+    To switch from library construction to AIG level minimization
-    It is not OK to switch from library construction to AIG level minimization
+    LSM manager should be restarted by dumping GIA (rec_dump3 <file>.aig) 
-    without restarting LSM manager.  To restart the LSM manager, GIA has to be written out 
+    and starting LMS manager again (rec_start3 <file>.aig).
-    (rec_dump3 <file>.aig) and LMS manager started again (rec_start3 <file>.aig).
 */
 
 typedef struct Lms_Man_t_ Lms_Man_t;
@@ -67,8 +68,8 @@ struct Lms_Man_t_
     Vec_Ptr_t *       vLabelsP;     // temporary storage for HOP node labels
     Vec_Int_t *       vLabels;      // temporary storage for AIG node labels
     Vec_Str_t *       vSupps;       // used temporarily by TT dumping
-    word              pTemp1[1024]; // copy of the truth table
+    word              pTemp1[LMS_MAX_WORD]; // copy of the truth table
-    word              pTemp2[1024]; // copy of the truth table
+    word              pTemp2[LMS_MAX_WORD]; // copy of the truth table
     // statistics 
     int               nTried;
     int               nFilterSize;
@@ -96,146 +97,6 @@ static Lms_Man_t * s_pMan3 = NULL;
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lms_Man_t * Lms_ManStart( Gia_Man_t * pGia, int nVars, int nCuts, int fFuncOnly, int fVerbose )
-{
-    Lms_Man_t * p;
-    clock_t clk, clk2 = clock();
-    // if GIA is given, use the number of variables from GIA
-    nVars = pGia ? Gia_ManCiNum(pGia) : nVars;
-    assert( nVars >= 6 && nVars <= 16 );
-    // allocate manager
-    p = ABC_CALLOC( Lms_Man_t, 1 );
-    // parameters
-    p->nVars = nVars;
-    p->nCuts = nCuts;
-    p->nWords = Abc_Truth6WordNum( nVars );
-    p->fFuncOnly = fFuncOnly;
-    // internal data for library construction
-    p->vTtMem = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
-    Vec_MemHashAlloc( p->vTtMem, 10000 );
-    if ( fFuncOnly )
-        return p;    
-    p->vTruthIds = Vec_IntAlloc( 10000 );
-    if ( pGia == NULL )
-    {
-        int i;
-        p->pGia = Gia_ManStart( 10000 );
-        p->pGia->pName = Abc_UtilStrsav( "record" );
-        for ( i = 0; i < nVars; i++ )
-            Gia_ManAppendCi( p->pGia );
-    }
-    else
-    {
-        Gia_Obj_t * pObj;
-        unsigned * pTruth;
-        int i, Index, Prev = -1;
-        p->pGia = pGia;
-        // populate the manager with subgraphs present in GIA
-        p->nAdded = Gia_ManCoNum( p->pGia );
-        Gia_ManForEachCo( p->pGia, pObj, i )
-        {
-            clk = clock();
-            pTruth = Gia_ObjComputeTruthTable( p->pGia, pObj );
-            p->timeTruth += clock() - clk;
-            clk = clock();
-            Index = Vec_MemHashInsert( p->vTtMem, (word *)pTruth );
-            p->timeInsert += clock() - clk;
-            assert( Index == Prev || Index == Prev + 1 ); // GIA subgraphs should be ordered
-            Vec_IntPush( p->vTruthIds, Index );
-            Prev = Index;
-        }
-    }
-    // temporaries
-    p->vNodes    = Vec_PtrAlloc( 1000 );
-    p->vLabelsP  = Vec_PtrAlloc( 1000 );
-    p->vLabels   = Vec_IntAlloc( 1000 );
-p->timeTotal += clock() - clk2;
-    return p;    
-}
-void Lms_ManStop( Lms_Man_t * p )
-{
-    // temporaries
-    Vec_IntFreeP( &p->vLabels );
-    Vec_PtrFreeP( &p->vLabelsP );
-    Vec_PtrFreeP( &p->vNodes );
-    // internal data for AIG level minimization
-    Vec_IntFreeP( &p->vTruthPo );
-    Vec_WrdFreeP( &p->vDelays );
-    Vec_StrFreeP( &p->vAreas );
-    Vec_IntFreeP( &p->vFreqs );
-    // internal data for library construction
-    Vec_IntFreeP( &p->vTruthIds );
-    Vec_MemHashFree( p->vTtMem );
-    Vec_MemFree( p->vTtMem );
-    Gia_ManStop( p->pGia );
-    ABC_FREE( p );
-}
-void Lms_ManPrint( Lms_Man_t * p )
-{
-//    Gia_ManPrintStats( p->pGia, 0, 0 );
-    printf( "Library with %d vars has %d classes and %d AIG subgraphs with %d AND nodes.\n", 
-        p->nVars, Vec_MemEntryNum(p->vTtMem), p->nAdded, p->pGia ? Gia_ManAndNum(p->pGia) : 0 );
-
-    p->nAddedFuncs = Vec_MemEntryNum(p->vTtMem);
-    printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,         !p->nTried? 0 : 100.0*p->nTried/p->nTried );
-    printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,    !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
-    printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund,  !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
-    printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume,  !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
-    printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,   !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
-    printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,   !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
-    printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,    !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
-    printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,         !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
-    printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,    !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
-    if ( p->nHoleInTheWall )
-    printf( "Cuts whose logic structure has a hole       = %10d. (%6.2f %%)\n", p->nHoleInTheWall, !p->nTried? 0 : 100.0*p->nHoleInTheWall/p->nTried );
-
-    p->timeOther = p->timeTotal - p->timeTruth - p->timeCanon - p->timeBuild - p->timeCheck - p->timeInsert;
-    ABC_PRTP( "Runtime: Truth ", p->timeTruth,  p->timeTotal );
-    ABC_PRTP( "Runtime: Canon ", p->timeCanon,  p->timeTotal );
-    ABC_PRTP( "Runtime: Build ", p->timeBuild,  p->timeTotal );
-    ABC_PRTP( "Runtime: Check ", p->timeCheck,  p->timeTotal );
-    ABC_PRTP( "Runtime: Insert", p->timeInsert, p->timeTotal );
-    ABC_PRTP( "Runtime: Other ", p->timeOther,  p->timeTotal );
-    ABC_PRTP( "Runtime: TOTAL ", p->timeTotal,  p->timeTotal );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose )
-{
-    assert( s_pMan3 == NULL );
-    s_pMan3 = Lms_ManStart( p, nVars, nCuts, fFuncOnly, fVerbose );
-}
-
-void Abc_NtkRecStop3()
-{
-    assert( s_pMan3 != NULL );
-    Lms_ManStop( s_pMan3 );
-    s_pMan3 = NULL;
-}
-
-
 /**Function*************************************************************
 
   Synopsis    [Compute delay/area profiles of POs.]
@@ -247,9 +108,9 @@ void Abc_NtkRecStop3()
   SeeAlso     []
 
 ***********************************************************************/
-static inline int  Lms_DelayGet( word D, int v )           { assert(v >= 0 && v < 16); return (int)((D >> (v << 2)) & 0xF);                    }
+static inline int  Lms_DelayGet( word D, int v )           { assert(v >= 0 && v < LMS_VAR_MAX); return (int)((D >> (v << 2)) & 0xF);                             }
-static inline void Lms_DelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < 16); assert(d >= 0 && d < 16); *pD |= ((word)d << (v << 2)); }
+static inline void Lms_DelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < LMS_VAR_MAX); assert(d >= 0 && d < LMS_VAR_MAX); *pD |= ((word)d << (v << 2)); }
-static inline word Lms_DelayInit( int v )                  { assert(v >= 0 && v < 16); return (word)1 << (v << 2);                             }
+static inline word Lms_DelayInit( int v )                  { assert(v >= 0 && v < LMS_VAR_MAX); return (word)1 << (v << 2);                                      }
 static inline word Lms_DelayMax( word D1, word D2, int nVars )
 {
     int v, Max;
@@ -349,6 +210,50 @@ Vec_Str_t * Lms_GiaAreas( Gia_Man_t * p )
         Vec_StrPush( vAreas, (char)(Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) ? Lms_ObjArea(Gia_ObjFanin0(pObj)) : 0) );
     return vAreas;
 }
+Vec_Str_t * Lms_GiaSuppSizes( Gia_Man_t * p )
+{
+    Vec_Str_t * vResult;
+    Vec_Str_t * vSupps;
+    Gia_Obj_t * pObj;
+    int i;
+    vSupps = Vec_StrAlloc( Gia_ManObjNum(p) );
+    Vec_StrPush( vSupps, 0 );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            Vec_StrPush( vSupps, (char)Abc_MaxInt( Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)), Vec_StrEntry(vSupps, Gia_ObjFaninId1(pObj, i)) ) );
+        else if ( Gia_ObjIsCo(pObj) )
+            Vec_StrPush( vSupps, Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)) );
+        else if ( Gia_ObjIsCi(pObj) )
+            Vec_StrPush( vSupps, (char)(Gia_ObjCioId(pObj)+1) );
+        else assert( 0 );
+    }
+    assert( Vec_StrSize(vSupps) == Gia_ManObjNum(p) );
+    vResult = Vec_StrAlloc( Gia_ManCoNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_StrPush( vResult, Vec_StrEntry(vSupps, Gia_ObjId(p, pObj)) );
+    Vec_StrFree( vSupps );
+    return vResult;
+}
+void Lms_GiaProfilesPrint( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Vec_Wrd_t * vDelays;
+    Vec_Str_t * vAreas;
+    vDelays = Lms_GiaDelays( p );
+    vAreas = Lms_GiaAreas( p );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        printf( "%6d : ", i );
+        printf( "A = %2d  ", Vec_StrEntry(vAreas, i) );
+        Lms_DelayPrint( Vec_WrdEntry(vDelays, i), Gia_ManPiNum(p) );
+//        Lms_GiaPrintSubgraph( p, pObj );
+//        printf( "\n" );
+    }
+    Vec_WrdFree( vDelays );
+    Vec_StrFree( vAreas );
+}
 
 /**Function*************************************************************
 
@@ -386,7 +291,7 @@ void Lms_GiaPrintSubgraph( Gia_Man_t * p, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Prints delay/area profiles of the GIA subgraphs.]
+  Synopsis    []
 
   Description []
                
@@ -395,65 +300,156 @@ void Lms_GiaPrintSubgraph( Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Lms_GiaProfilesPrint( Gia_Man_t * p )
+Lms_Man_t * Lms_ManStart( Gia_Man_t * pGia, int nVars, int nCuts, int fFuncOnly, int fVerbose )
+{
+    Lms_Man_t * p;
+    clock_t clk, clk2 = clock();
+    // if GIA is given, use the number of variables from GIA
+    nVars = pGia ? Gia_ManCiNum(pGia) : nVars;
+    assert( nVars >= 6 && nVars <= LMS_VAR_MAX );
+    // allocate manager
+    p = ABC_CALLOC( Lms_Man_t, 1 );
+    // parameters
+    p->nVars = nVars;
+    p->nCuts = nCuts;
+    p->nWords = Abc_Truth6WordNum( nVars );
+    p->fFuncOnly = fFuncOnly;
+    // internal data for library construction
+    p->vTtMem = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
+    Vec_MemHashAlloc( p->vTtMem, 10000 );
+    if ( fFuncOnly )
+        return p;    
+    p->vTruthIds = Vec_IntAlloc( 10000 );
+    if ( pGia == NULL )
+    {
+        int i;
+        p->pGia = Gia_ManStart( 10000 );
+        p->pGia->pName = Abc_UtilStrsav( "record" );
+        for ( i = 0; i < nVars; i++ )
+            Gia_ManAppendCi( p->pGia );
+    }
+    else
     {
         Gia_Obj_t * pObj;
-    int i;
+        word * pTruth;
-    Vec_Wrd_t * vDelays;
+        int i, Index, Prev = -1;
-    Vec_Str_t * vAreas;
+        p->pGia = pGia;
-    vDelays = Lms_GiaDelays( p );
+        // populate the manager with subgraphs present in GIA
-    vAreas = Lms_GiaAreas( p );
+        p->nAdded = Gia_ManCoNum( p->pGia );
-
+        Gia_ManForEachCo( p->pGia, pObj, i )
-    Gia_ManForEachPo( p, pObj, i )
         {
-        printf( "%6d : ", i );
+            clk = clock();
-        printf( "A = %2d  ", Vec_StrEntry(vAreas, i) );
+            pTruth = Gia_ObjComputeTruthTable( p->pGia, pObj );
-        Lms_DelayPrint( Vec_WrdEntry(vDelays, i), Gia_ManPiNum(p) );
+            p->timeTruth += clock() - clk;
-//        Lms_GiaPrintSubgraph( p, pObj );
+            clk = clock();
-//        printf( "\n" );
+            Index = Vec_MemHashInsert( p->vTtMem, pTruth );
+            p->timeInsert += clock() - clk;
+            assert( Index == Prev || Index == Prev + 1 ); // GIA subgraphs should be ordered
+            Vec_IntPush( p->vTruthIds, Index );
+            Prev = Index;
         }
-
-    Vec_WrdFree( vDelays );
-    Vec_StrFree( vAreas );
     }
-
+    // temporaries
-/**Function*************************************************************
+    p->vNodes    = Vec_PtrAlloc( 1000 );
-
+    p->vLabelsP  = Vec_PtrAlloc( 1000 );
-  Synopsis    [Compute support sizes for each CO.]
+    p->vLabels   = Vec_IntAlloc( 1000 );
-
+p->timeTotal += clock() - clk2;
-  Description []
+    return p;    
-               
+}
-  SideEffects []
+void Lms_ManStop( Lms_Man_t * p )
-
+{
-  SeeAlso     []
+    // temporaries
-
+    Vec_IntFreeP( &p->vLabels );
-***********************************************************************/
+    Vec_PtrFreeP( &p->vLabelsP );
-Vec_Str_t * Gia_ManSuppSizes( Gia_Man_t * p )
+    Vec_PtrFreeP( &p->vNodes );
+    // internal data for AIG level minimization
+    Vec_IntFreeP( &p->vTruthPo );
+    Vec_WrdFreeP( &p->vDelays );
+    Vec_StrFreeP( &p->vAreas );
+    Vec_IntFreeP( &p->vFreqs );
+    // internal data for library construction
+    Vec_IntFreeP( &p->vTruthIds );
+    Vec_MemHashFree( p->vTtMem );
+    Vec_MemFree( p->vTtMem );
+    Gia_ManStop( p->pGia );
+    ABC_FREE( p );
+}
+void Lms_ManPrepare( Lms_Man_t * p )
+{
+    // compute the first PO for each semi-canonical form
+    int i, Entry;
+    assert( !p->fLibConstr );
+    assert( p->vTruthPo == NULL );
+    p->vTruthPo = Vec_IntStartFull( Vec_MemEntryNum(p->vTtMem)+1 );
+    assert( Vec_IntFindMin(p->vTruthIds) >= 0 );
+    assert( Vec_IntFindMax(p->vTruthIds) < Vec_MemEntryNum(p->vTtMem) );
+    Vec_IntForEachEntry( p->vTruthIds, Entry, i )
+        if ( Vec_IntEntry(p->vTruthPo, Entry) == -1 )
+            Vec_IntWriteEntry( p->vTruthPo, Entry, i );
+    Vec_IntWriteEntry( p->vTruthPo, Vec_MemEntryNum(p->vTtMem), Gia_ManCoNum(p->pGia) );
+    // compute delay/area and init frequency
+    assert( p->vDelays == NULL );
+    assert( p->vAreas == NULL );
+    assert( p->vFreqs == NULL );
+    p->vDelays = Lms_GiaDelays( p->pGia );
+    p->vAreas  = Lms_GiaAreas( p->pGia );
+    p->vFreqs  = Vec_IntStart( Gia_ManCoNum(p->pGia) );
+}
+void Lms_ManPrintFuncStats( Lms_Man_t * p )
 {
-    Vec_Str_t * vResult;
     Vec_Str_t * vSupps;
-    Gia_Obj_t * pObj;
+    int Counters[LMS_VAR_MAX+1] = {0}, CountersS[LMS_VAR_MAX+1] = {0};
-    int i;
+    int i, Entry, Next;
-    vSupps = Vec_StrAlloc( Gia_ManObjNum(p) );
+    if ( p->pGia == NULL )
-    Vec_StrPush( vSupps, 0 );
+        return;
-    Gia_ManForEachObj1( p, pObj, i )
+    if ( p->fLibConstr )
+        return;
+    if ( p->vTruthPo == NULL )
+        Lms_ManPrepare( p );
+    vSupps = Lms_GiaSuppSizes( p->pGia );
+    Vec_IntForEachEntry( p->vTruthPo, Entry, i )
     {
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( i == Vec_IntSize(p->vTruthPo) - 1 )
-            Vec_StrPush( vSupps, (char)Abc_MaxInt( Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)), Vec_StrEntry(vSupps, Gia_ObjFaninId1(pObj, i)) ) );
+            break;
-        else if ( Gia_ObjIsCo(pObj) )
+        Next = Vec_IntEntry( p->vTruthPo, i+1 );
-            Vec_StrPush( vSupps, Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)) );
+        Counters[Vec_StrEntry(vSupps, Entry)]++;
-        else if ( Gia_ObjIsCi(pObj) )
+        CountersS[Vec_StrEntry(vSupps, Entry)] += Next - Entry;
-            Vec_StrPush( vSupps, (char)(Gia_ObjCioId(pObj)+1) );
-        else assert( 0 );
     }
-    assert( Vec_StrSize(vSupps) == Gia_ManObjNum(p) );
+    for ( i = 0; i <= LMS_VAR_MAX; i++ )
-    vResult = Vec_StrAlloc( Gia_ManCoNum(p) );
+        if ( Counters[i] )
-    Gia_ManForEachCo( p, pObj, i )
+            printf( "Inputs = %2d.  Funcs = %8d.  Subgrs = %8d.  Ratio = %6.2f.\n", i, Counters[i], CountersS[i], 1.0*CountersS[i]/Counters[i] );
-        Vec_StrPush( vResult, Vec_StrEntry(vSupps, Gia_ObjId(p, pObj)) );
     Vec_StrFree( vSupps );
-    return vResult;
 }
+void Lms_ManPrint( Lms_Man_t * p )
+{
+//    Gia_ManPrintStats( p->pGia, 0, 0 );
+    printf( "Library with %d vars has %d classes and %d AIG subgraphs with %d AND nodes.\n", 
+        p->nVars, Vec_MemEntryNum(p->vTtMem), p->nAdded, p->pGia ? Gia_ManAndNum(p->pGia) : 0 );
 
+    Lms_ManPrintFuncStats( p );
+
+    p->nAddedFuncs = Vec_MemEntryNum(p->vTtMem);
+    printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,         !p->nTried? 0 : 100.0*p->nTried/p->nTried );
+    printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,    !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
+    printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund,  !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
+    printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume,  !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
+    printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,   !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
+    printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,   !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
+    printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,    !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
+    printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,         !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
+    printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,    !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
+    if ( p->nHoleInTheWall )
+    printf( "Cuts whose logic structure has a hole       = %10d. (%6.2f %%)\n", p->nHoleInTheWall, !p->nTried? 0 : 100.0*p->nHoleInTheWall/p->nTried );
+
+    p->timeOther = p->timeTotal - p->timeTruth - p->timeCanon - p->timeBuild - p->timeCheck - p->timeInsert;
+    ABC_PRTP( "Runtime: Truth ", p->timeTruth,  p->timeTotal );
+    ABC_PRTP( "Runtime: Canon ", p->timeCanon,  p->timeTotal );
+    ABC_PRTP( "Runtime: Build ", p->timeBuild,  p->timeTotal );
+    ABC_PRTP( "Runtime: Check ", p->timeCheck,  p->timeTotal );
+    ABC_PRTP( "Runtime: Insert", p->timeInsert, p->timeTotal );
+    ABC_PRTP( "Runtime: Other ", p->timeOther,  p->timeTotal );
+    ABC_PRTP( "Runtime: TOTAL ", p->timeTotal,  p->timeTotal );
+}
 
 /**Function*************************************************************
 
@@ -472,9 +468,9 @@ void Abc_NtkRecLibMerge3( Gia_Man_t * pLib )
     Lms_Man_t * p = s_pMan3;
     Gia_Man_t * pGia = p->pGia;
     Vec_Str_t * vSupps;
-    char pCanonPerm[16];
+    char pCanonPerm[LMS_VAR_MAX];
     unsigned uCanonPhase;
-    unsigned * pTruth;
+    word * pTruth;
     int i, k, Index, iFanin0, iFanin1, nLeaves;
     Gia_Obj_t * pObjPo, * pDriver, * pTemp = NULL;
     clock_t clk, clk2 = clock();
@@ -491,12 +487,13 @@ void Abc_NtkRecLibMerge3( Gia_Man_t * pLib )
         Gia_ManHashStart( pGia );
 
     // add AIG subgraphs
-    vSupps = Gia_ManSuppSizes( pLib );
+    vSupps = Lms_GiaSuppSizes( pLib );
     Gia_ManForEachCo( pLib, pObjPo, k )
     {
         // get support size
         nLeaves = Vec_StrEntry(vSupps, k);
         assert( nLeaves > 1 );
+
         // compute the truth table
 clk = clock();
         pTruth = Gia_ObjComputeTruthTable( pLib, Gia_ObjFanin0(pObjPo) );
@@ -512,6 +509,8 @@ clk = clock();
         Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
 p->timeCanon += clock() - clk;
         // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
+        if ( nLeaves == 2 && Abc_TtSupportSize(pTruth, 2) != 2 )
+            continue;
 
 clk = clock();
         // map cut leaves into elementary variables of GIA
@@ -549,7 +548,7 @@ p->timeCheck += clock() - clk;
         if ( memcmp( p->pTemp1, pTruth, p->nWords * sizeof(word) ) != 0 )
         {
     
-            Kit_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
+            Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
             Kit_DsdPrintFromTruth( (unsigned *)p->pTemp1, nLeaves ); printf( "\n" );
             printf( "Truth table verification has failed.\n" );
     
@@ -590,7 +589,7 @@ p->timeTotal += clock() - clk2;
 int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
 {
     Lms_Man_t * p = s_pMan3;
-    char pCanonPerm[16];
+    char pCanonPerm[LMS_VAR_MAX];
     unsigned uCanonPhase;
     int i, Index, iFanin0, iFanin1, fHole;
     int nLeaves = If_CutLeaveNum(pCut);
@@ -598,13 +597,13 @@ int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     Gia_Man_t * pGia = p->pGia;
     Gia_Obj_t * pDriver;
     If_Obj_t * pIfObj = NULL;
-    unsigned * pTruth;
+    word * pTruth;
     clock_t clk;
     p->nTried++;
 
     // skip small cuts
     assert( p->nVars == (int)pCut->nLimit );
-    if ( nLeaves < 2 )
+    if ( nLeaves < 2 || (nLeaves == 2 && Abc_TtSupportSize(If_CutTruthW(pCut), 2) != 2) )
     {
         p->nFilterSize++;
         return 1;
@@ -871,32 +870,15 @@ p->timeCanon += clock() - clk;
 int If_CutDelayRecCost3( If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pObj )
 {
     Lms_Man_t * p = s_pMan3;
-    char pCanonPerm[16];
+    char pCanonPerm[LMS_VAR_MAX];
     unsigned uCanonPhase;
     // make sure the cut functions match the library
     assert( p->nVars == (int)pCut->nLimit );
     // if this assertion fires, it means that LMS manager was used for library construction
     // in this case, GIA has to be written out and the manager restarted as described above
     assert( !p->fLibConstr );
-    if ( p->vTruthPo == NULL ) // the first time AIG level minimization is called
+    if ( p->vTruthPo == NULL )
-    {
+        Lms_ManPrepare( p );
-        // compute the first PO for each semi-canonical form
-        int i, Entry;
-        p->vTruthPo = Vec_IntStartFull( Vec_MemEntryNum(p->vTtMem)+1 );
-        assert( Vec_IntFindMin(p->vTruthIds) >= 0 );
-        assert( Vec_IntFindMax(p->vTruthIds) < Vec_MemEntryNum(p->vTtMem) );
-        Vec_IntForEachEntry( p->vTruthIds, Entry, i )
-            if ( Vec_IntEntry(p->vTruthPo, Entry) == -1 )
-                Vec_IntWriteEntry( p->vTruthPo, Entry, i );
-        Vec_IntWriteEntry( p->vTruthPo, Vec_MemEntryNum(p->vTtMem), Gia_ManCoNum(p->pGia) );
-        // compute delay/area and init frequency
-        assert( p->vDelays == NULL );
-        assert( p->vAreas == NULL );
-        assert( p->vFreqs == NULL );
-        p->vDelays = Lms_GiaDelays( p->pGia );
-        p->vAreas  = Lms_GiaAreas( p->pGia );
-        p->vFreqs  = Vec_IntStart( Gia_ManCoNum(p->pGia) );
-    }
     // return the delay of the best structure
     return If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, NULL );
 }
@@ -915,7 +897,7 @@ int If_CutDelayRecCost3( If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pObj )
 Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj )
 {
     Lms_Man_t * p = s_pMan3;
-    char pCanonPerm[16];
+    char pCanonPerm[LMS_VAR_MAX];
     unsigned uCanonPhase;
     Hop_Obj_t * pFan0, * pFan1, * pHopObj;
     Gia_Man_t * pGia = p->pGia;
@@ -991,7 +973,7 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
 int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
 {
     Lms_Man_t * p = s_pMan3;
-    char pCanonPerm[16];
+    char pCanonPerm[LMS_VAR_MAX];
     unsigned uCanonPhase;
     int iFan0, iFan1, iGiaObj;
     Gia_Man_t * pGia = p->pGia;
@@ -1274,22 +1256,10 @@ void Abc_NtkRecDumpTt3( char * pFileName, int fBinary )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRecPs3(int fPrintLib)
+int Abc_NtkRecInputNum3()
 {
-    Lms_ManPrint( s_pMan3 );
+    return Gia_ManCiNum(s_pMan3->pGia);
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_NtkRecIsRunning3()
 {
     return s_pMan3 != NULL;
@@ -1303,11 +1273,24 @@ Gia_Man_t * Abc_NtkRecGetGia3()
     printf( "After normalizing:  Library has %d classes and %d AIG subgraphs with %d AND nodes.\n", 
         Vec_MemEntryNum(s_pMan3->vTtMem), Gia_ManPoNum(s_pMan3->pGia), Gia_ManAndNum(s_pMan3->pGia) );
     Abc_PrintTime( 1, "Normalization runtime", clock() - clk );
+    s_pMan3->fLibConstr = 0;
     return s_pMan3->pGia;
 }
-int Abc_NtkRecInputNum3()
+void Abc_NtkRecPs3(int fPrintLib)
 {
-    return Gia_ManCiNum(s_pMan3->pGia);
+    Lms_ManPrint( s_pMan3 );
+}
+void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose )
+{
+    assert( s_pMan3 == NULL );
+    s_pMan3 = Lms_ManStart( p, nVars, nCuts, fFuncOnly, fVerbose );
+}
+
+void Abc_NtkRecStop3()
+{
+    assert( s_pMan3 != NULL );
+    Lms_ManStop( s_pMan3 );
+    s_pMan3 = NULL;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/io/io.c

@@ -2738,7 +2738,7 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
     Gia_Obj_t * pObj;
     char * pFileName;
     FILE * pFile;
-    unsigned * pTruth;
+    word * pTruth;
     int nBytes;
     int fReverse = 0;
     int fBinary = 0;
@@ -2794,7 +2794,7 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
         if ( fBinary )
             fwrite( pTruth, nBytes, 1, pFile );
         else
-            Extra_PrintHex( pFile, pTruth, Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
+            Extra_PrintHex( pFile, (unsigned *)pTruth, Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
     }
     fclose( pFile );
     return 0;

src/proof/abs/absRpm.c

@@ -665,7 +665,7 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
             nSize0 = Abs_GiaSortNodes( p, vSupp );
             assert( nSize0 > 0 && nSize0 <= nCutMax );
             // check if truth table has const cofs
-            pTruth = (word *)Gia_ObjComputeTruthTableCut( p, pObj, vSupp );
+            pTruth = Gia_ObjComputeTruthTableCut( p, pObj, vSupp );
             fHasConst = !Abs_GiaCheckTruth( pTruth, Vec_IntSize(vSupp), nSize0 );
             if ( fVeryVerbose )
             {