Version abc60812

28 files changed, 1169 insertions, 215 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bb8f5658..f3dbe357 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -93,6 +93,7 @@ static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -210,6 +211,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -5088,6 +5090,75 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fUpdateLevel, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUpdateLevel = 1;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "zvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyHaig( pNtk, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: haig [-vh]\n" );
+    fprintf( pErr, "\t         prints HAIG stats after one round of sequential rewriting\n" );
+//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 380b3f8b..7d5ed6ec 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -179,6 +179,36 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan;
+    pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
+    if ( pMan == NULL )
+        return NULL;
+
+    Ivy_ManHaigStart( pMan );
+    Ivy_ManRewriteSeq( pMan, 0, fVerbose );
+    Ivy_ManHaigPrintStats( pMan );
+    Ivy_ManHaigStop( pMan );
+
+//    pNtkAig = Abc_NtkIvyAfterHaig( pNtk, pMan, 1 );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs )
 {
     extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
@@ -276,10 +306,10 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 {
-    Abc_Ntk_t * pNtkAig;
+//    Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;//, * pTemp;
     int fCleanup = 1;
-    int nNodes;
+//    int nNodes;
     int nLatches = Abc_NtkLatchNum(pNtk);
     int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 );
 
@@ -329,6 +359,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 //    Ivy_ManStop( pTemp );
 
 //    Ivy_ManTestCutsAll( pMan );
+//    Ivy_ManTestCutsTravAll( pMan );
 
 //    Ivy_ManPrintStats( pMan );
 
@@ -344,7 +375,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 //    Ivy_ManRequiredLevels( pMan );
 
 //    Pla_ManFastLutMap( pMan, 8 );
-//    Ivy_ManStop( pMan );
+    Ivy_ManStop( pMan );
     return NULL;
 
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 33f432f4..6cbab1a6 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -148,7 +148,6 @@ Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
 void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 {
     ProgressBar * pProgress;
-    DdManager * dd = pNtk->pManFunc;
     Abc_Obj_t * pNode, * pNodeNew;
     Vec_Ptr_t * vNodes;
     int i;
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 5c4a0675..a1011a36 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -111,7 +111,6 @@ Abc_Frame_t * Abc_FrameAllocate()
     // set the starting step
     p->nSteps = 1;
     p->fBatchMode = 0;
-    p->fProgress = 1;
     // initialize decomposition manager
     define_cube_size(20);
     set_espresso_flags();
@@ -176,7 +175,7 @@ void Abc_FrameRestart( Abc_Frame_t * p )
 ***********************************************************************/
 bool Abc_FrameShowProgress( Abc_Frame_t * p )
 {
-    return p->fProgress;
+    return Abc_FrameIsFlagEnabled( "progressbar" );
 }
 
 
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 109e91c8..d2bca1ab 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -55,7 +55,6 @@ struct Abc_Frame_t_
     int             nSteps;      // the counter of different network processed
     int             fAutoexac;   // marks the autoexec mode
     int                fBatchMode;     // are we invoked in batch mode?
-    int             fProgress;   // shows progress bars
     // output streams
     FILE *          Out;
     FILE *          Err;
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
index 45667768..9be29f87 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -27,6 +27,8 @@ extern "C" {
 #include <stdlib.h>
 #include "extra.h"
 
+//#pragma warning( disable : 4514 )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     MACRO DEFINITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -91,9 +93,9 @@ struct _reo_plane
 struct _reo_hash
 {
     int         Sign;            // signature of the current cache operation
-    unsigned    Arg1;            // the first argument
-    unsigned    Arg2;            // the second argument
-    unsigned    Arg3;            // the second argument
+    reo_unit *  Arg1;            // the first argument
+    reo_unit *  Arg2;            // the second argument
+    reo_unit *  Arg3;            // the third argument
 };
 
 struct _reo_man
diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c
index b38575f0..84a0bc19 100644
--- a/src/bdd/reo/reoProfile.c
+++ b/src/bdd/reo/reoProfile.c
@@ -330,7 +330,7 @@ void reoProfileWidthPrint( reo_man * p )
              WidthMax = p->pPlanes[i].statsWidth;
         TotalWidth += p->pPlanes[i].statsWidth;
     }
-    assert( p->nWidthCur = TotalWidth );
+    assert( p->nWidthCur == TotalWidth );
     printf( "WIDTH:  " );
     printf( "Maximum = %5d.  ", WidthMax );
     printf( "Total = %7d.  ", p->nWidthCur );
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c
index cb730d8e..4afa650c 100644
--- a/src/bdd/reo/reoSwap.c
+++ b/src/bdd/reo/reoSwap.c
@@ -271,9 +271,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                    HKey = (HKey+1) % p->nTableSize );
             assert( p->HTable[HKey].Sign != p->Signature );
             p->HTable[HKey].Sign = p->Signature;
-            p->HTable[HKey].Arg1 = (unsigned)pUnitE;
-            p->HTable[HKey].Arg2 = (unsigned)pUnitT;
-            p->HTable[HKey].Arg3 = (unsigned)pUnit;
+            p->HTable[HKey].Arg1 = pUnitE;
+            p->HTable[HKey].Arg2 = pUnitT;
+            p->HTable[HKey].Arg3 = pUnit;
 
             nNodesUpMovedDown++;
 
@@ -512,10 +512,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T )
+            if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane20 = (reo_unit *)p->HTable[HKey].Arg3;
+                pNewPlane20 = p->HTable[HKey].Arg3;
                 assert( pNewPlane20->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -549,9 +549,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = (unsigned)pNew1E;
-                p->HTable[HKey].Arg2 = (unsigned)pNew1T;
-                p->HTable[HKey].Arg3 = (unsigned)pNewPlane20;
+                p->HTable[HKey].Arg1 = pNew1E;
+                p->HTable[HKey].Arg2 = pNew1T;
+                p->HTable[HKey].Arg3 = pNewPlane20;
 
                 nNodesUnrefAdded++;
                         
@@ -637,10 +637,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T )
+            if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane21 = (reo_unit *)p->HTable[HKey].Arg3;
+                pNewPlane21 = p->HTable[HKey].Arg3;
                 assert( pNewPlane21->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -675,9 +675,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = (unsigned)pNew2E;
-                p->HTable[HKey].Arg2 = (unsigned)pNew2T;
-                p->HTable[HKey].Arg3 = (unsigned)pNewPlane21;
+                p->HTable[HKey].Arg1 = pNew2E;
+                p->HTable[HKey].Arg2 = pNew2T;
+                p->HTable[HKey].Arg3 = pNewPlane21;
 
                 nNodesUnrefAdded++;
 
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 752cd3d7..65d31d01 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -51,9 +51,9 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     {
         // search cache - use linear probing
         for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (unsigned)F )
+            if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
             {
-                pUnit = (reo_unit*) p->HTable[HKey].Arg2;  
+                pUnit = p->HTable[HKey].Arg2;  
                 assert( pUnit );
                 // increment the edge counter
                 pUnit->n++;
@@ -93,8 +93,8 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
         // might have been used. Make sure that its signature is different.
         for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
         p->HTable[HKey].Sign = p->Signature;
-        p->HTable[HKey].Arg1 = (unsigned)F;
-        p->HTable[HKey].Arg2 = (unsigned)pUnit;
+        p->HTable[HKey].Arg1 = (reo_unit *)F;
+        p->HTable[HKey].Arg2 = pUnit;
     }
 
     // increment the counter of nodes
@@ -126,7 +126,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
     if ( pUnit->n != 1 )
     {
         for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (unsigned)pUnit )
+            if ( p->HTable[HKey].Arg1 == pUnit )
             {
                 bRes = (DdNode*) p->HTable[HKey].Arg2;  
                 assert( bRes );
@@ -179,8 +179,8 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
          // might have been used. Make sure that its signature is different.
          for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
          p->HTable[HKey].Sign = p->Signature;
-         p->HTable[HKey].Arg1 = (unsigned)pUnit;
-         p->HTable[HKey].Arg2 = (unsigned)bRes;  
+         p->HTable[HKey].Arg1 = pUnit;
+         p->HTable[HKey].Arg2 = (reo_unit *)bRes;  
 
          // add the DD to the referenced DD list in order to be able to store it in cache
          p->pRefNodes[p->nRefNodes++] = bRes;  Cudd_Ref( bRes ); 
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index bdbc3d89..8b20daae 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -341,7 +341,7 @@ extern int         Extra_MmStepReadMemUsage( Extra_MmStep_t * p );
 
 /*=== extraUtilMisc.c ========================================================*/
 
-/* finds the smallest integer larger of equal than the logarithm. */
+/* finds the smallest integer larger or equal than the logarithm */
 extern int         Extra_Base2Log( unsigned Num );
 extern int         Extra_Base2LogDouble( double Num );
 extern int         Extra_Base10Log( unsigned Num );
@@ -400,7 +400,15 @@ static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char
 
 /*=== extraUtilTruth.c ================================================================*/
 
-static inline int Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int   Extra_Float2Int( float Val )     { return *((int *)&Val);               }
+static inline float Extra_Int2Float( int Num )       { return *((float *)&Num);             }
+static inline int   Extra_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
+static inline int   Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+
+static inline void  Extra_TruthSetBit( unsigned * p, int Bit )   { p[Bit>>5] |= (1<<(Bit & 31));               }
+static inline void  Extra_TruthXorBit( unsigned * p, int Bit )   { p[Bit>>5] ^= (1<<(Bit & 31));               }
+static inline int   Extra_TruthHasBit( unsigned * p, int Bit )   { return (p[Bit>>5] & (1<<(Bit & 31))) > 0;   }
+
 static inline int Extra_WordCountOnes( unsigned uWord )
 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -409,6 +417,13 @@ static inline int Extra_WordCountOnes( unsigned uWord )
     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
     return  (uWord & 0x0000FFFF) + (uWord>>16);
 }
+static inline int Extra_TruthCountOnes( unsigned * pIn, int nVars )
+{
+    int w, Counter = 0;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        Counter += Extra_WordCountOnes(pIn[w]);
+    return Counter;
+}
 static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
 {
     int w;
@@ -504,18 +519,26 @@ extern void     Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
 extern void     Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void     Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int      Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
-extern int      Extra_TruthCountOnes( unsigned * pTruth, int nVars );
 extern void     Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
 extern unsigned Extra_TruthHash( unsigned * pIn, int nWords );
 extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
 
 /*=== extraUtilUtil.c ================================================================*/
 
+#ifndef ALLOC
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#endif
+
+#ifndef FREE
 #define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#endif
+
+#ifndef REALLOC
 #define REALLOC(type, obj, num)    \
         ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
          ((type *) malloc(sizeof(type) * (num))))
+#endif
+
 
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();
diff --git a/src/misc/extra/extraUtil.h b/src/misc/extra/extraUtil.h
deleted file mode 100644
index d3f432c2..00000000
--- a/src/misc/extra/extraUtil.h
+++ /dev/null
@@ -1,60 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [extraUtil.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [extra]
-
-  Synopsis    [Various reusable software utilities.]
-
-  Description []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: extraUtil.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __EXTRA_UTIL_H__
-#define __EXTRA_UTIL_H__
-
-/*---------------------------------------------------------------------------*/
-/* Nested includes                                                           */
-/*---------------------------------------------------------------------------*/
-
-#include <string.h>
-#include <time.h>
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-/*===========================================================================*/
-/*     Various Utilities                                                     */
-/*===========================================================================*/
-
-
-/**AutomaticEnd***************************************************************/
-
-#endif /* __EXTRA_UTIL_H__ */
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index 6b10813c..ab476f6f 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -782,26 +782,6 @@ void Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar )
 
 /**Function*************************************************************
 
-  Synopsis    [Changes phase of the function w.r.t. one variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Extra_TruthCountOnes( unsigned * pTruth, int nVars )
-{
-    int nWords = Extra_TruthWordNum( nVars );
-    int i, Counter = 0;
-    for ( i = 0; i < nWords; i++ )
-        Counter += Extra_WordCountOnes( pTruth[i] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes minimum overlap in supports of cofactors.]
 
   Description []
diff --git a/src/opt/cut/cut60720.zip b/src/opt/cut/cut60720.zip
deleted file mode 100644
index 86ad6726..00000000
--- a/src/opt/cut/cut60720.zip
+++ /dev/null
diff --git a/src/opt/cut/cut60721.zip b/src/opt/cut/cut60721.zip
deleted file mode 100644
index d55ccfd0..00000000
--- a/src/opt/cut/cut60721.zip
+++ /dev/null
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 02b7605c..e56c58f3 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -88,13 +88,13 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
         printf( "The current network does not have SOPs to perform extraction.\n" );
         return NULL;
     }
-
+/*
     if ( nPairsStore > 10000000 )
     {
         printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
         return NULL;
     }
-
+*/
     // start the matrix
     p = Fxu_MatrixAllocate();
     // create the column labels 
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index a36c795b..2409284e 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -110,14 +110,17 @@ struct Ivy_Man_t_
     int              nTravIds;       // the traversal ID
     int              nLevelMax;      // the maximum level
     Vec_Int_t *      vRequired;      // required times
-//    Vec_Ptr_t *      vFanouts;       // representation of the fanouts
     int              fFanout;        // fanout is allocated
     void *           pData;          // the temporary data
     void *           pCopy;          // the temporary data
+    Ivy_Man_t *      pHaig;          // history AIG if present
     // memory management
     Vec_Ptr_t *      vChunks;        // allocated memory pieces
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
     Ivy_Obj_t *      pListFree;      // the list of free nodes 
+    // timing statistics
+    int              time1;
+    int              time2;
 };
 
 
@@ -197,51 +200,54 @@ static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->nO
 static inline int          Ivy_ManHashObjNum( Ivy_Man_t * p )     { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH];     }
 static inline int          Ivy_ManGetCost( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }
 
-static inline Ivy_Type_t   Ivy_ObjType( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type;               }
-static inline Ivy_Init_t   Ivy_ObjInit( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Init;               }
-static inline int          Ivy_ObjIsConst1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Id == 0;            }
-static inline int          Ivy_ObjIsGhost( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->Id < 0;             }
-static inline int          Ivy_ObjIsNone( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_NONE;   }
-static inline int          Ivy_ObjIsPi( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI;     }
-static inline int          Ivy_ObjIsPo( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO;     }
-static inline int          Ivy_ObjIsCi( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
-static inline int          Ivy_ObjIsCo( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
-static inline int          Ivy_ObjIsAssert( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ASSERT; }
-static inline int          Ivy_ObjIsLatch( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LATCH;  }
-static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND;    }
-static inline int          Ivy_ObjIsExor( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR;   }
-static inline int          Ivy_ObjIsBuf( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF;    }
-static inline int          Ivy_ObjIsNode( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
-static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
-static inline int          Ivy_ObjIsHash( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
-static inline int          Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
-
-static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA;  }
-static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1;     }
-static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0;     }
+static inline Ivy_Type_t   Ivy_ObjType( Ivy_Obj_t * pObj )        { return pObj->Type;               }
+static inline Ivy_Init_t   Ivy_ObjInit( Ivy_Obj_t * pObj )        { return pObj->Init;               }
+static inline int          Ivy_ObjIsConst1( Ivy_Obj_t * pObj )    { return pObj->Id == 0;            }
+static inline int          Ivy_ObjIsGhost( Ivy_Obj_t * pObj )     { return pObj->Id < 0;             }
+static inline int          Ivy_ObjIsNone( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_NONE;   }
+static inline int          Ivy_ObjIsPi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI;     }
+static inline int          Ivy_ObjIsPo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO;     }
+static inline int          Ivy_ObjIsCi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsCo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsAssert( Ivy_Obj_t * pObj )    { return pObj->Type == IVY_ASSERT; }
+static inline int          Ivy_ObjIsLatch( Ivy_Obj_t * pObj )     { return pObj->Type == IVY_LATCH;  }
+static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_AND;    }
+static inline int          Ivy_ObjIsExor( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_EXOR;   }
+static inline int          Ivy_ObjIsBuf( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_BUF;    }
+static inline int          Ivy_ObjIsNode( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
+static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
+static inline int          Ivy_ObjIsHash( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj )  { return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
+
+static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { return pObj->fMarkA;  }
+static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { pObj->fMarkA = 1;     }
+static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { pObj->fMarkA = 0;     }
  
-static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId;                                              }
-static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds;                          }
-static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds - 1;                      }
-static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds);     }
-static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds - 1); }
-
-static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { assert( !Ivy_IsComplement(pObj) ); return pObj->Id;                               }
-static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase;                           }
-static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->fExFan;                           }
-static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs;                            }
-static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++;                                 }
-static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
-static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
-static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
-static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin0);        }
-static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin1);        }
-static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin0);             }
-static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin1);             }
-static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0;                          }
-static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1;                          }
-static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Level;                            }
-static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
+static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId )                { pObj->TravId = TravId;                               }
+static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                          }
+static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { pObj->TravId = p->nTravIds - 1;                      }
+static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { return (int )((int)pObj->TravId == p->nTravIds);     }
+static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { return (int )((int)pObj->TravId == p->nTravIds - 1); }
+
+static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { return pObj->Id;                               }
+static inline int          Ivy_ObjTravId( Ivy_Obj_t * pObj )      { return pObj->TravId;                           }
+static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { return pObj->fPhase;                           }
+static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { return pObj->fExFan;                           }
+static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { return pObj->nRefs;                            }
+static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { pObj->nRefs++;                                 }
+static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
+static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
+static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
+static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin0);        }
+static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin1);        }
+static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin0);             }
+static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin1);             }
+static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { return pObj->pFanin0;                          }
+static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { return pObj->pFanin1;                          }
+static inline Ivy_Obj_t *  Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL;  }
+static inline Ivy_Obj_t *  Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }
+static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { return pObj->Level;                            }
+static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
 static inline void         Ivy_ObjClean( Ivy_Obj_t * pObj )       
 { 
     int IdSaved = pObj->Id; 
@@ -415,10 +421,19 @@ extern void            Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_
 extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+/*=== ivyHaig.c ==========================================================*/
+extern void            Ivy_ManHaigStart( Ivy_Man_t * p );
+extern void            Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
+extern void            Ivy_ManHaigStop( Ivy_Man_t * p );
+extern void            Ivy_ManHaigPrintStats( Ivy_Man_t * p );
+extern void            Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
+extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
 /*=== ivyIsop.c ==========================================================*/
 extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
+extern Ivy_Man_t *     Ivy_ManDup( Ivy_Man_t * p );
 extern void            Ivy_ManStop( Ivy_Man_t * p );
 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
 extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
index 0303485a..3e8bd6d2 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -59,6 +59,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
     Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
     Ivy_ManForEachPi( p, pObj, i )
         pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
+    // if HAIG is defined, trasfer the pointers to the PIs/latches
+//    if ( p->pHaig )
+//        Ivy_ManHaigTrasfer( p, pNew );
     // balance the AIG
     vStore = Vec_VecAlloc( 50 );
     Ivy_ManForEachPo( p, pObj, i )
@@ -327,10 +330,18 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, i
     // get the two last nodes
     pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
     pObj2 = Vec_PtrEntry( vSuper, RightBound     );
+    if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 )
+        return;
     // find the first node that can be shared
     for ( i = RightBound; i >= LeftBound; i-- )
     {
         pObj3 = Vec_PtrEntry( vSuper, i );
+        if ( Ivy_Regular(pObj3) == p->pConst1 )
+        {
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+            return;
+        }
         pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
         if ( Ivy_TableLookup( p, pGhost ) )
         {
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 65ba4aac..d918c96c 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -889,7 +889,6 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
 {
     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
-    Ivy_Man_t * pMan = p;
     Ivy_Obj_t * pLeaf;
     int i, k, iLeaf0, iLeaf1;
 
diff --git a/src/temp/ivy/ivyCutTrav.c b/src/temp/ivy/ivyCutTrav.c
new file mode 100644
index 00000000..ea57c9f5
--- /dev/null
+++ b/src/temp/ivy/ivyCutTrav.c
@@ -0,0 +1,473 @@
+/**CFile****************************************************************
+
+  FileName    [ivyCutTrav.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyCutTrav.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId );
+static void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront );
+static void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, int nLeaves, int nWords, Vec_Int_t * vStore );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves, int nNodeLimit, 
+                                      Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront, Vec_Int_t * vStore, Vec_Vec_t * vBitCuts )
+{
+    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
+    Vec_Ptr_t * vCuts, * vCuts0, * vCuts1;
+    unsigned * pBitCut;
+    Ivy_Obj_t * pLeaf;
+    Ivy_Cut_t * pCut;
+    int i, k, nWords, nNodes;
+
+    assert( nLeaves <= IVY_CUT_INPUT );
+
+    // find the given number of nodes in the TFI
+    Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront );
+    nNodes = Vec_PtrSize(vNodes);
+//    assert( nNodes <= nNodeLimit );
+
+    // make sure vBitCuts has enough room
+    Vec_VecExpand( vBitCuts, nNodes-1 );
+    Vec_VecClear( vBitCuts );
+
+    // prepare the memory manager
+    Vec_IntClear( vStore );
+    Vec_IntGrow( vStore, 64000 );
+
+    // set elementary cuts for the leaves
+    nWords = Extra_BitWordNum( nNodes );
+    Vec_PtrForEachEntry( vFront, pLeaf, i )
+    {
+        assert( Ivy_ObjTravId(pLeaf) < nNodes );
+        // get the new bitcut
+        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
+        // set it as the cut of this leaf
+        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
+    }
+
+    // compute the cuts for each node
+    Vec_PtrForEachEntry( vNodes, pLeaf, i )
+    {
+        // skip the leaves
+        vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) );
+        if ( Vec_PtrSize(vCuts) > 0 )
+            continue;
+        // add elementary cut
+        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
+        // set it as the cut of this leaf
+        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
+        // get the fanin cuts
+        vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) );
+        vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) );
+        assert( Vec_PtrSize(vCuts0) > 0 );
+        assert( Vec_PtrSize(vCuts1) > 0 );
+        // merge the cuts
+        Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore );
+    }
+
+    // start the structure
+    pCutStore->nCuts = 0;
+    pCutStore->nCutsMax = IVY_CUT_LIMIT;
+    // collect the cuts of the root node
+    vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) );
+    Vec_PtrForEachEntry( vCuts, pBitCut, i )
+    {
+        pCut = pCutStore->pCuts + pCutStore->nCuts++;
+        pCut->nSize = 0;
+        pCut->nSizeMax = nLeaves;
+        pCut->uHash = 0;
+        for ( k = 0; k < nNodes; k++ )
+            if ( Extra_TruthHasBit(pBitCut, k) )
+                pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( Vec_PtrEntry(vNodes, k) );
+        assert( pCut->nSize <= nLeaves );
+        if ( pCutStore->nCuts == pCutStore->nCutsMax )
+            break;
+    }
+
+    // clean the travIds
+    Vec_PtrForEachEntry( vNodes, pLeaf, i )
+        pLeaf->TravId = 0;
+    return pCutStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates elementary bit-cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId )
+{
+    unsigned * pBitCut;
+    pBitCut = Vec_IntFetch( vStore, nWords );
+    memset( pBitCut, 0, 4 * nWords );
+    Extra_TruthSetBit( pBitCut, NodeId );
+    return pBitCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the node by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CompareNodesByLevel( Ivy_Obj_t ** ppObj1, Ivy_Obj_t ** ppObj2 )
+{
+    Ivy_Obj_t * pObj1 = *ppObj1;
+    Ivy_Obj_t * pObj2 = *ppObj2;
+    if ( pObj1->Level < pObj2->Level )
+        return -1;
+    if ( pObj1->Level > pObj2->Level )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark all nodes up to the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolumeTrav1_rec( Ivy_Obj_t * pObj, int Depth )
+{
+    if ( Ivy_ObjIsCi(pObj) || Depth == 0 )
+        return;
+    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 );
+    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 );
+    pObj->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the marked nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolumeTrav2_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( !pObj->fMarkA )
+        return;
+    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
+{
+    Ivy_Obj_t * pTemp, * pFanin;
+    int i, nNodes;
+    // mark nodes up to the given depth
+    Ivy_NodeComputeVolumeTrav1_rec( pObj, 6 );
+    // collect the marked nodes
+    Vec_PtrClear( vFront );
+    Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront );
+    // find the fanins that are not marked
+    Vec_PtrClear( vNodes );
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+    {
+        pFanin = Ivy_ObjFanin0(pTemp);
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+        }
+        pFanin = Ivy_ObjFanin1(pTemp);
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+        }
+    }
+    // remember the number of nodes in the frontier
+    nNodes = Vec_PtrSize( vNodes );
+    // add the remaining nodes
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+        Vec_PtrPush( vNodes, pTemp );
+    // unmark the nodes
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+    {
+        pTemp->fMarkA = 0;
+        pTemp->TravId = i;
+    }
+    // collect the frontier nodes
+    Vec_PtrClear( vFront );
+    Vec_PtrForEachEntryStop( vNodes, pTemp, i, nNodes )
+        Vec_PtrPush( vFront, pTemp );
+//    printf( "%d ", Vec_PtrSize(vNodes) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolume2( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
+{
+    Ivy_Obj_t * pLeaf, * pPivot, * pFanin;
+    int LevelMax, i;
+    assert( Ivy_ObjIsNode(pObj) );
+    // clear arrays
+    Vec_PtrClear( vNodes );
+    Vec_PtrClear( vFront );
+    // add the root
+    pObj->fMarkA = 1;
+    Vec_PtrPush( vNodes, pObj );
+    Vec_PtrPush( vFront, pObj );
+    // expand node with maximum level
+    LevelMax = pObj->Level;
+    do {
+        // get the node to expand
+        pPivot = NULL;
+        Vec_PtrForEachEntryReverse( vFront, pLeaf, i )
+        {
+            if ( (int)pLeaf->Level == LevelMax )
+            {
+                pPivot = pLeaf;
+                break;
+            }
+        }
+        // decrease level if we did not find the node
+        if ( pPivot == NULL )
+        {
+            if ( --LevelMax == 0 )
+                break;
+            continue;
+        }
+        // the node to expand is found
+        // remove it from frontier
+        Vec_PtrRemove( vFront, pPivot );
+        // add fanins
+        pFanin = Ivy_ObjFanin0(pPivot); 
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+            Vec_PtrPush( vFront, pFanin );
+        }
+        pFanin = Ivy_ObjFanin1(pPivot); 
+        if ( pFanin && !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+            Vec_PtrPush( vFront, pFanin );
+        }
+        // quit if we collected enough nodes
+    } while ( Vec_PtrSize(vNodes) < nNodeLimit );
+
+    // sort nodes by level
+    Vec_PtrSort( vNodes, Ivy_CompareNodesByLevel );
+    // make sure the nodes are ordered in the increasing number of levels
+    pFanin = Vec_PtrEntry( vNodes, 0 );
+    pPivot = Vec_PtrEntryLast( vNodes );
+    assert( pFanin->Level <= pPivot->Level );
+
+    // clean the marks and remember node numbers in the TravId
+    Vec_PtrForEachEntry( vNodes, pFanin, i )
+    {
+        pFanin->fMarkA = 0;
+        pFanin->TravId = i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Extra_TruthOrWords( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nWords )
+{
+    int w;
+    for ( w = nWords-1; w >= 0; w-- )
+        pOut[w] = pIn0[w] | pIn1[w];
+}
+static inline int Extra_TruthIsImplyWords( unsigned * pIn1, unsigned * pIn2, int nWords )
+{
+    int w;
+    for ( w = nWords-1; w >= 0; w-- )
+        if ( pIn1[w] & ~pIn2[w] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two sets of bit-cuts at a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, 
+                           int nLeaves, int nWords, Vec_Int_t * vStore )
+{
+    unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest;
+    int i, k, c, w, Counter;
+    // iterate through the cut pairs
+    Vec_PtrForEachEntry( vCuts0, pBitCut0, i )
+    Vec_PtrForEachEntry( vCuts1, pBitCut1, k )
+    {
+        // skip infeasible cuts
+        Counter = 0;
+        for ( w = 0; w < nWords; w++ )
+        {
+            Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] );
+            if ( Counter > nLeaves )
+                break;
+        }
+        if ( Counter > nLeaves )
+            continue;
+        // the new cut is feasible - create it
+        pBitCutTest = Vec_IntFetch( vStore, nWords );
+        Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords );
+        // filter contained cuts; try to find containing cut
+        w = 0;
+        Vec_PtrForEachEntry( vCuts, pBitCut, c )
+        {
+            if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) )
+                break;
+            if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) )
+                continue;
+            Vec_PtrWriteEntry( vCuts, w++, pBitCut );
+        }
+        if ( c != Vec_PtrSize(vCuts) )
+            continue;
+        Vec_PtrShrink( vCuts, w );
+        // add the cut
+        Vec_PtrPush( vCuts, pBitCutTest );
+    }
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Compute the set of all cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
+{
+    Ivy_Store_t * pStore;
+    Ivy_Obj_t * pObj;
+    Vec_Ptr_t * vNodes, * vFront;
+    Vec_Int_t * vStore;
+    Vec_Vec_t * vBitCuts;
+    int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
+    int clk = clock();
+
+    vNodes = Vec_PtrAlloc( 100 );
+    vFront = Vec_PtrAlloc( 100 );
+    vStore = Vec_IntAlloc( 100 );
+    vBitCuts = Vec_VecAlloc( 100 );
+
+    nNodeTotal = nNodeOver = 0;
+    nCutsTotal = -Ivy_ManNodeNum(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts );
+        nCutsCut    = pStore->nCuts;
+        nCutsTotal += nCutsCut;
+        nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
+        nNodeTotal++;
+    }
+    printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
+        nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
+    PRT( "Time", clock() - clk );
+
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vFront );
+    Vec_IntFree( vStore );
+    Vec_VecFree( vBitCuts );
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 7246ec25..314bed8d 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -119,7 +119,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
-    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
+//    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
     *pvLatches = vLatches;
     return vNodes;
 }
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
new file mode 100644
index 00000000..7ce71a60
--- /dev/null
+++ b/src/temp/ivy/ivyHaig.c
@@ -0,0 +1,348 @@
+/**CFile****************************************************************
+
+  FileName    [ivyHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [HAIG management procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyHaig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    HAIGing rules in working AIG:
+    - The node points to the representative of its class
+    - The pointer can be complemented if they have different polarity
+
+    Choice node rules in HAIG:
+    - Equivalent nodes are linked into a ring
+    - Exactly one node in the ring has fanouts (this node is called representative)
+    - Pointer going from a node to the next node in the ring is complemented 
+      if the first node is complemented, compared to the representative node
+    - The representative node always has non-complemented pointer to the next node
+    - New nodes are inserted into the ring before the representative node
+*/
+
+// returns the representative node of the given HAIG node
+static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pTemp;
+    assert( !Ivy_IsComplement(pObj) );
+    // if the node has no equivalent or has fanout, it is representative
+    if ( pObj->pEquiv == NULL || Ivy_ObjRefs(pObj) > 0 )
+        return pObj;
+    // the node belongs to a class and is not a representative
+    // complemented edge (pObj->pEquiv) tells if it is complemented w.r.t. the repr
+    for ( pTemp = Ivy_Regular(pObj->pEquiv); pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+        if ( Ivy_ObjRefs(pTemp) > 0 )
+            break;
+    // return the representative node
+    assert( pTemp != pObj );
+    return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
+}
+
+// counts the number of nodes in the equivalence class
+static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pTemp;
+    int Counter;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjRefs(pObj) > 0 );
+    if ( pObj->pEquiv == NULL )
+        return 1;
+    Counter = 1;
+    assert( !Ivy_IsComplement(pObj->pEquiv) );
+    for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+        Counter++;
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts HAIG for the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigStart( Ivy_Man_t * p )
+{
+    assert( p->pHaig == NULL );
+    p->pHaig = Ivy_ManDup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the HAIG to the newly created manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    assert( p->pHaig != NULL );
+    Ivy_ManConst1(pNew)->pEquiv = Ivy_ManConst1(p)->pEquiv;
+    Ivy_ManForEachPi( pNew, pObj, i )
+        pObj->pEquiv = Ivy_ManPi( p, i )->pEquiv;
+    pNew->pHaig = p->pHaig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops HAIG for the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigStop( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    assert( p->pHaig != NULL );
+    Ivy_ManStop( p->pHaig );
+    p->pHaig = NULL;
+    // remove dangling pointers to the HAIG objects
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->pEquiv = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
+{
+    assert( p->pHaig != NULL );
+    assert( !Ivy_IsComplement(pObj) );
+    if ( Ivy_ObjType(pObj) == IVY_BUF )
+        pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
+    else if ( Ivy_ObjType(pObj) == IVY_LATCH )
+        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+    else if ( Ivy_ObjType(pObj) == IVY_AND )
+        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    else assert( 0 );
+    // make sure the node points to the representative
+    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the pair of equivalent nodes in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew )
+{
+    Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
+    Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
+    int fCompl;
+    assert( p->pHaig != NULL );
+    // get pointers to the classes
+    pObjOldHaig = pObjOld->pEquiv;
+    pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
+    // get regular pointers
+    pObjOldHaigR = Ivy_Regular(pObjOldHaig);
+    pObjNewHaigR = Ivy_Regular(pObjNewHaig);
+    // check if there is phase difference between them
+    fCompl = (Ivy_IsComplement(pObjOldHaig) != Ivy_IsComplement(pObjNewHaig));
+    // if the class is the same, nothing to do
+    if ( pObjOldHaigR == pObjNewHaigR )
+        return;
+    // combine classes
+    // assume the second node does not belong to a class
+    assert( pObjNewHaigR->pEquiv == NULL );
+    // add this node to the class of pObjOldHaig
+    if ( pObjOldHaigR->pEquiv == NULL )
+        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
+    else
+        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
+    pObjOldHaigR->pEquiv = pObjNewHaigR;
+    // update the class of the new node
+    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of choices and choice nodes in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
+{
+    Ivy_Obj_t * pObj;
+    int nChoices, nChoiceNodes, Counter, i;
+    assert( p->pHaig != NULL );
+    nChoices = nChoiceNodes = 0;
+    Ivy_ManForEachObj( p->pHaig, pObj, i )
+    {
+        if ( Ivy_ObjIsTerm(pObj) || i == 0 )
+            continue;
+        if ( Ivy_ObjRefs(pObj) == 0 )
+        {
+            assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
+            continue;
+        }
+        Counter = Ivy_HaigObjCountClass( pObj );
+        nChoiceNodes += (int)(Counter > 1);
+        nChoices += Counter - 1;
+    }
+    *pnChoices = nChoices;
+    return nChoiceNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
+{
+    int nChoices, nChoiceNodes;
+    assert( p->pHaig != NULL );
+    printf( "Original : " );
+    Ivy_ManPrintStats( p );
+    printf( "HAIG     : " );
+    Ivy_ManPrintStats( p->pHaig );
+
+    // print choice node stats
+    nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
+    printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); 
+    Ivy_ManHaigSimulate( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Applies the simulation rules.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1 )
+{
+    assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
+    if ( In0 == IVY_INIT_DC || In1 == IVY_INIT_DC )
+        return IVY_INIT_DC;
+    if ( In0 == IVY_INIT_1 && In1 == IVY_INIT_1 )
+        return IVY_INIT_1;
+    return IVY_INIT_0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulate HAIG using modified 3-valued simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigSimulate( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Obj_t * pObj;
+    Ivy_Init_t In0, In1;
+    int i, k, Counter;
+    assert( p->pHaig != NULL );
+    p = p->pHaig;
+    // collect latches and nodes in the DFS order
+    vNodes = Ivy_ManDfsSeq( p, &vLatches );
+    // set the PI values
+    Ivy_ManConst1(p)->Init = IVY_INIT_0;
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->Init = IVY_INIT_0;
+    // set the latch values
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        pObj->Init = IVY_INIT_DC;
+    // perform several rounds of simulation
+    for ( k = 0; k < 5; k++ )
+    {
+        // count the number of non-determinate values
+        Counter = 0;
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            Counter += ( pObj->Init == IVY_INIT_DC );
+        printf( "Iter %d : Non-determinate = %d\n", k, Counter );               
+        // simulate the internal nodes
+        Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        {
+            In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
+            In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
+            pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
+        }
+        // simulate the latches
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            pObj->Level = Ivy_ObjFanin0(pObj)->Init;
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            pObj->Init = pObj->Level, pObj->Level = 0;
+    }
+    // free arrays
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLatches );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 9839567f..e3b8a5b8 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -70,6 +70,62 @@ Ivy_Man_t * Ivy_ManStart()
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Man_t * pNew;
+    Ivy_Obj_t * pObj;
+    int i;
+    // collect latches and nodes in the DFS order
+    vNodes = Ivy_ManDfsSeq( p, &vLatches );
+    // create the new manager
+    pNew = Ivy_ManStart();
+    // create the PIs
+    Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+    // create the fake PIs for latches
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+    // duplicate internal nodes
+    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    // add the POs
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) );
+    // transform additional PI nodes into latches and connect them
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+    {
+        assert( !Ivy_ObjFaninC0(pObj) );
+        pObj->pEquiv->Type = IVY_LATCH;
+        pObj->pEquiv->Init = pObj->Init;
+        Ivy_ObjConnect( pNew, pObj->pEquiv, Ivy_ObjChild0Equiv(pObj), NULL );
+    }
+    // shrink the arrays
+    Vec_PtrShrink( pNew->vPis, Ivy_ManPiNum(p) );
+    // update the counters of different objects
+    pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
+    pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
+    // free arrays
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLatches );
+    // check the resulting network
+    if ( !Ivy_ManCheck(pNew) )
+        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -81,6 +137,8 @@ Ivy_Man_t * Ivy_ManStart()
 ***********************************************************************/
 void Ivy_ManStop( Ivy_Man_t * p )
 {
+    if ( p->time1 ) { PRT( "Update lev  ", p->time1 ); }
+    if ( p->time2 ) { PRT( "Update levR ", p->time2 ); }
 //    Ivy_TableProfile( p );
 //    if ( p->vFanouts )  Ivy_ManStopFanout( p );
     if ( p->vChunks )   Ivy_ManStopMemory( p );
diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c
index 6ca33541..09c73c49 100644
--- a/src/temp/ivy/ivyMem.c
+++ b/src/temp/ivy/ivyMem.c
@@ -89,7 +89,7 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
     int i, nBytes;
     assert( sizeof(Ivy_Obj_t) <= 64 );
     assert( p->pListFree == NULL );
-    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
+//    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
     // allocate new memory page
     nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
     pMemory = ALLOC( char, nBytes );
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index f098332d..a7970156 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -294,45 +294,6 @@ int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals,
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Constructs the well-balanced tree of gates.]
-
-  Description [Disregards levels and possible logic sharing.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
-{
-    Ivy_Obj_t * pObj1, * pObj2;
-    if ( nObjs == 1 )
-        return ppObjs[0];
-    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
-    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
-    return Ivy_Oper( p, pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
-    assert( Type == IVY_AND || Type == IVY_EXOR );
-    assert( nArgs > 0 );
-    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 3122c8c8..e8924b5b 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -79,7 +79,6 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     assert( Ivy_TableLookup(p, pGhost) == NULL );
     // get memory for the new object
     pObj = Ivy_ManFetchMemory( p );
-//printf( "Reusing %p.\n", pObj );
     assert( Ivy_ObjIsNone(pObj) );
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
@@ -115,6 +114,9 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Ivy_ObjType(pObj)]++;
     p->nCreated++;
+    // if HAIG is defined, create a corresponding node
+    if ( p->pHaig )
+        Ivy_ManHaigCreateObj( p, pObj );
     return pObj;
 }
 
@@ -258,7 +260,6 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
         // free the node
         Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
         Ivy_ManRecycleMemory( p, pObj );
-//printf( "Recycling after delete %p.\n", pObj );
     }
     else
     {
@@ -312,7 +313,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
 ***********************************************************************/
 void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel )
 {
-    int nRefsOld;
+    int nRefsOld;//, clk;
     // the object to be replaced cannot be complemented
     assert( !Ivy_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
@@ -321,12 +322,16 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
     // the object cannot be the same
     assert( pObjOld != Ivy_Regular(pObjNew) );
+    // if HAIG is defined, create the choice node
+    if ( p->pHaig )
+        Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
     // if the new object is complemented or already used, add the buffer
     if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
         pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
     assert( !Ivy_IsComplement(pObjNew) );
     if ( fUpdateLevel )
     {
+//clk = clock();
         // if the new node's arrival time is different, recursively update arrival time of the fanouts
         if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
         {
@@ -334,7 +339,9 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
             pObjOld->Level = pObjNew->Level;
             Ivy_ObjUpdateLevel_rec( p, pObjOld );
         }
+//p->time1 += clock() - clk;
         // if the new node's required time has changed, recursively update required time of the fanins
+//clk = clock();
         if ( p->vRequired )
         {
             int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
@@ -344,6 +351,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
                 Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
             }
         }
+//p->time2 += clock() - clk;
     }
     // delete the old object
     if ( fDeleteOld )
@@ -375,7 +383,6 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     // recycle the object that was taken over by pObjOld
     Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
     Ivy_ManRecycleMemory( p, pObjNew );
-//printf( "Recycling after patch %p.\n", pObjNew );
     // if the new node is the buffer propagate it
     if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
         Vec_PtrPush( p->vBufs, pObjOld );
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
index af216e45..8115ce4f 100644
--- a/src/temp/ivy/ivyOper.c
+++ b/src/temp/ivy/ivyOper.c
@@ -210,6 +210,45 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t *
 
 /**Function*************************************************************
 
+  Synopsis    [Constructs the well-balanced tree of gates.]
+
+  Description [Disregards levels and possible logic sharing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
+    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+    return Ivy_Oper( p, pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Implements the miter.]
 
   Description []
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 7cf55b69..11660e42 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -80,10 +80,6 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
         // stop if all nodes have been tried once
         if ( i > nNodes )
             break;
-        if ( i == 8648 )
-        {
-            int x = 0;
-        }
         // for each cut, try to resynthesize it
         nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
         if ( nGain > 0 || nGain == 0 && fUseZeroCost )
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index 91994ca6..ca84ded1 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -446,7 +446,7 @@ static inline int Abc_NodePlayerCost( int nFanins )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost )
+static inline int Abc_NtkPlayerCostOneLevel( int nCost, int RankCost )
 {
     return (nCost / RankCost) + ((nCost % RankCost) > 0);
 }
@@ -466,7 +466,8 @@ int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
 {
     Abc_Obj_t * pObj;
     int * pLevelCosts, * pLevelCostsR;
-    int nFanins, nLevels, LevelR, Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR, i; 
+    int Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR;
+    int nFanins, nLevels, LevelR, i; 
     // compute the reverse levels
     Abc_NtkStartReverseLevels( pNtk );
     // compute the costs for each level
@@ -491,17 +492,19 @@ int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
     {
         CostTotal    += pLevelCosts[i];
         CostTotalR   += pLevelCostsR[i];
-        nRanksTotal  += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
-        nRanksTotalR += Abc_NtkPlayerCostOne( pLevelCostsR[i], RankCost );
+        nRanksTotal  += Abc_NtkPlayerCostOneLevel( pLevelCosts[i], RankCost );
+        nRanksTotalR += Abc_NtkPlayerCostOneLevel( pLevelCostsR[i], RankCost );
     }
     assert( CostTotal == CostTotalR );
     // print out statistics
     if ( fVerbose )
     {
         for ( i = 1; i <= nLevels; i++ )
+        {
             printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i, 
             pLevelCosts[i], ((double)pLevelCosts[i])/RankCost, 
             pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost );
+        }
         printf( "TOTAL    : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n", 
             CostTotal, nRanksTotal, nRanksTotalR, nLevels );
     }