Version abc90329

16 files changed, 875 insertions, 1576 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 28d610e9..87c85516 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -52,6 +52,15 @@ struct Gia_Rpr_t_
     unsigned       fColorB :  1;  // marks cone of B
 };
 
+typedef struct Gia_Plc_t_ Gia_Plc_t;
+struct Gia_Plc_t_
+{
+    unsigned       fFixed  :  1;  // the placement of this object is fixed
+    unsigned       xCoord  : 15;  // x-ooordinate of the placement
+    unsigned       fUndef  :  1;  // the placement of this object is not assigned
+    unsigned       yCoord  : 15;  // y-ooordinate of the placement
+};
+
 typedef struct Gia_Obj_t_ Gia_Obj_t;
 struct Gia_Obj_t_
 {
@@ -117,6 +126,8 @@ struct Gia_Man_t_
     Gia_Cex_t *    pCexComb;      // combinational counter-example
     int *          pCopies;       // intermediate copies
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
+    unsigned char* pSwitching;    // switching activity for each object
+    Gia_Plc_t *    pPlacement;    // placement of the objects
 };
 
 
@@ -247,7 +258,7 @@ static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t *
 static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
 
 static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) );  }
-static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, pObj), Gia_IsComplement(pObj) );              }
+static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
 static inline int          Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit )      { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) );        }
 
 static inline int          Gia_ObjValue( Gia_Obj_t * pObj )                    { return pObj->Value;                                        }
@@ -375,8 +386,10 @@ static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p
 static inline int         Gia_ObjIsConst( Gia_Man_t * p, int Id )            { return Gia_ObjRepr(p, Id) == 0;                                   }
 static inline int         Gia_ObjIsHead( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsNone( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
-static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;          }
-static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;           }
+static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;                  }
+static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;                   }
+static inline int         Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k )  { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0;  }
+static inline int         Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k);                     }
 
 #define Gia_ManForEachConst( p, i )                            \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
@@ -419,6 +432,8 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ )
+#define Gia_ManForEachCoReverse( p, pObj, i )                           \
+    for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- )
 #define Gia_ManForEachCoDriver( p, pObj, i )                            \
     for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ObjFanin0(Gia_ManCo(p, i))); i++ )
 #define Gia_ManForEachPi( p, pObj, i )                                  \
@@ -443,7 +458,9 @@ extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
 /*=== giaAiger.c ===========================================================*/
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
+extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 /*=== giaCsat.c ============================================================*/
+extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
@@ -455,6 +472,10 @@ extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
 /*=== giaDup.c ============================================================*/
+extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
+
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupSelf( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
@@ -508,19 +529,22 @@ extern int                 Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
 extern int                 Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
 extern int                 Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
 extern Gia_Man_t *         Gia_ManRehash( Gia_Man_t * p );
+extern void                Gia_ManHashProfile( Gia_Man_t * p );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
  /*=== giaMan.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManStart( int nObjsMax ); 
 extern void                Gia_ManStop( Gia_Man_t * p );  
-extern void                Gia_ManPrintStats( Gia_Man_t * p ); 
+extern void                Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); 
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 /*=== giaMap.c ===========================================================*/
 extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+/*=== giaPat.c ===========================================================*/
+extern void                Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
 /*=== giaRetime.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose );
 /*=== giaSat.c ============================================================*/
@@ -535,6 +559,9 @@ extern Gia_Man_t *         Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int
 extern int *               Gia_SortFloats( float * pArray, int * pPerm, int nSize );
 /*=== giaSim.c ============================================================*/
 extern int                 Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
+/*=== giaSwitch.c ============================================================*/
+extern float               Gia_ManEvaluateSwitching( Gia_Man_t * p );
+extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
 /*=== giaTsim.c ============================================================*/
 extern Gia_Man_t *         Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
 /*=== giaUtil.c ===========================================================*/
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index da1a8c9f..adc58e6c 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -194,6 +194,25 @@ int Gia_ReadInt( unsigned char * pPos )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads decoded value.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev )
+{
+    int Item = Gia_ReadAigerDecode( ppPos );
+    if ( Item & 1 )
+        return iPrev + (Item >> 1);
+    return iPrev - (Item >> 1);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read equivalence classes from the string.]
 
   Description []
@@ -238,7 +257,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads decoded value.]
+  Synopsis    [Read flop classes from the string.]
 
   Description []
   
@@ -247,12 +266,13 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev )
+void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize )
 {
-    int Item = Gia_ReadAigerDecode( ppPos );
-    if ( Item & 1 )
-        return iPrev + (Item >> 1);
-    return iPrev - (Item >> 1);
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc/4 == nSize );
+    assert( Vec_IntSize(vClasses) == nSize );
+    memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize );
+    *ppPos += 4 * nSize;
 }
 
 /**Function*************************************************************
@@ -290,6 +310,50 @@ int * Gia_ReadMapping( unsigned char ** ppPos, int nSize )
 
 /**Function*************************************************************
 
+  Synopsis    [Read switching from the string.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize )
+{
+    unsigned char * pSwitching;
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc == nSize );
+    pSwitching = ABC_ALLOC( unsigned char, nSize );
+    memcpy( pSwitching, *ppPos, nSize );
+    *ppPos += nSize;
+    return pSwitching;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read placement from the string.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize )
+{
+    Gia_Plc_t * pPlacement;
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc/4 == nSize );
+    pPlacement = ABC_ALLOC( Gia_Plc_t, nSize );
+    memcpy( pPlacement, *ppPos, 4*nSize );
+    *ppPos += 4 * nSize;
+    return pPlacement;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the AIG in the binary AIGER format.]
 
   Description []
@@ -455,6 +519,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
             pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
             pNew->pNexts = Gia_ManDeriveNexts( pNew );
         }
+        if ( *pCur == 'f' )
+        {
+            pCur++;
+            // read flop classes
+            pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
+            Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) );
+        }
         if ( *pCur == 'm' )
         {
             pCur++;
@@ -465,6 +536,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
         {
             pCur++;
             // read placement
+            pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) );
+        }
+        if ( *pCur == 's' )
+        {
+            pCur++;
+            // read switching activity
+            pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) );
         }
         if ( *pCur == 'n' )
         {
@@ -762,7 +840,10 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
 
     // create normalized AIG
     if ( !Gia_ManIsNormalized(pInit) )
+    {
+        printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
         p = Gia_ManDupNormalized( pInit );
+    }
     else
         p = pInit;
 
@@ -831,6 +912,15 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         fwrite( pEquivs, 1, nEquivSize, pFile );
         ABC_FREE( pEquivs );
     }
+    // write flop classes
+    if ( p->vFlopClasses )
+    {
+        char Buffer[10];
+        int nSize = 4*Gia_ManRegNum(p);
+        fprintf( pFile, "f" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile );
+    }
     // write mapping
     if ( p->pMapping )
     {
@@ -841,6 +931,26 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         ABC_FREE( pMaps );
     }
     // write placement
+    if ( p->pPlacement )
+    {
+        char Buffer[10];
+        int nSize = 4*Gia_ManObjNum(p);
+        Gia_WriteInt( Buffer, nSize );
+        fprintf( pFile, "p" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( p->pPlacement, 1, nSize, pFile );
+    }
+    // write flop classes
+    if ( p->pSwitching )
+    {
+        char Buffer[10];
+        int nSize = Gia_ManObjNum(p);
+        Gia_WriteInt( Buffer, nSize );
+        fprintf( pFile, "s" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( p->pSwitching, 1, nSize, pFile );
+    }
+    // write name
     if ( p->pName )
         fprintf( pFile, "n%s%c", p->pName, '\0' );
     fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
@@ -850,6 +960,24 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Gia_ManStop( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits )
+{
+    char Buffer[100];
+    sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
+    Gia_WriteAiger( p, Buffer, 0, 0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat.c
index 1e7cc949..5fa9f40f 100644
--- a/src/aig/gia/giaCSat2.c
+++ b/src/aig/gia/giaCSat.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [giaCSat2.c]
+  FileName    [giaCSat.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: giaCSat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -48,10 +48,10 @@ struct Cbs_Que_t_
 {
     int           iHead;        // beginning of the queue
     int           iTail;        // end of the queue
-    int           nSize;        // allocated size
+   int           nSize;        // allocated size
     Gia_Obj_t **  pData;        // nodes stored in the queue
 };
-
+ 
 typedef struct Cbs_Man_t_ Cbs_Man_t;
 struct Cbs_Man_t_
 {
@@ -60,6 +60,20 @@ struct Cbs_Man_t_
     Cbs_Que_t     pProp;        // propagation queue
     Cbs_Que_t     pJust;        // justification queue
     Vec_Int_t *   vModel;       // satisfying assignment
+    // SAT calls statistics
+    int           nSatUnsat;    // the number of proofs
+    int           nSatSat;      // the number of failure
+    int           nSatUndec;    // the number of timeouts
+    int           nSatTotal;    // the number of calls
+    // conflicts
+    int           nConfUnsat;   // conflicts in unsat problems
+    int           nConfSat;     // conflicts in sat problems
+    int           nConfUndec;   // conflicts in undec problems
+    // runtime stats
+    int           timeSatUnsat; // unsat
+    int           timeSatSat;   // sat
+    int           timeSatUndec; // undecided
+    int           timeTotal;    // total runtime
 };
 
 static inline int   Cbs_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -196,7 +210,8 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
     p->pProp.iHead = 0;
     Cbs_QueForEachEntry( p->pProp, pVar, i )
         if ( Gia_ObjIsCi(pVar) )
-            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
 } 
 
 /**Function*************************************************************
@@ -714,7 +729,7 @@ void Cbs_ManSolveTest( Gia_Man_t * pGia )
             CountUndec++;
         else 
         {
-            int iLit, k;
+//            int iLit, k;
             vCex = Cbs_ReadModel( p );
 
 //        printf( "complemented = %d.  ", Gia_ObjFaninC0(pRoot) );
@@ -738,6 +753,132 @@ void Cbs_ManSolveTest( Gia_Man_t * pGia )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cbs_ManSatPrintStats( Cbs_Man_t * p )
+{
+    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "Conf = %5d  ", p->Pars.nBTLimit );
+    printf( "JustMax = %5d  ", p->Pars.nJustLimit );
+    printf( "\n" );
+    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
+    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
+    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+    ABC_PRT( "Total time", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus )
+{
+    extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+    Cbs_Man_t * p; 
+    Vec_Int_t * vCex, * vVisit, * vCexStore;
+    Vec_Str_t * vStatus;
+    Gia_Obj_t * pRoot; 
+    int i, status, clk, clkTotal = clock();
+    assert( Gia_ManRegNum(pAig) == 0 );
+    // prepare AIG
+    Gia_ManCreateRefs( pAig );
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
+    // create logic network
+    p = Cbs_ManAlloc();
+    p->Pars.nBTLimit = nConfs;
+    p->pAig   = pAig;
+    // create resulting data-structures
+    vStatus   = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+    vCexStore = Vec_IntAlloc( 10000 );
+    vVisit    = Vec_IntAlloc( 100 );
+    vCex      = Cbs_ReadModel( p );
+    // solve for each output
+    Gia_ManForEachCo( pAig, pRoot, i )
+    {
+        Vec_IntClear( vCex );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+        {
+            if ( Gia_ObjFaninC0(pRoot) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
+            continue;
+        }
+        clk = clock();
+        p->Pars.fUseHighest = 1;
+        p->Pars.fUseLowest  = 0;
+        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+        if ( status == -1 )
+        {
+            p->Pars.fUseHighest = 0;
+            p->Pars.fUseLowest  = 1;
+            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+        }
+        Vec_StrPush( vStatus, (char)status );
+        if ( status == -1 )
+        {
+            p->nSatUndec++;
+            p->nConfUndec += p->Pars.nBTThis;
+            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+            p->timeSatUndec += clock() - clk;
+            continue;
+        }
+        if ( status == 1 )
+        {
+            p->nSatUnsat++;
+            p->nConfUnsat += p->Pars.nBTThis;
+            p->timeSatUnsat += clock() - clk;
+            continue;
+        }
+        p->nSatSat++;
+        p->nConfUnsat += p->Pars.nBTThis;
+//        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+        Cec_ManSatAddToStore( vCexStore, vCex, i );
+        p->timeSatSat += clock() - clk;
+    }
+    Vec_IntFree( vVisit );
+    p->nSatTotal = Gia_ManPoNum(pAig);
+    p->timeTotal = clock() - clkTotal;
+//    Cbs_ManSatPrintStats( p );
+    Cbs_ManStop( p );
+    *pvStatus = vStatus;
+//    printf( "Total number of cex literals = %d. (Ave = %d)\n", 
+//         Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, 
+//        (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
+    return vCexStore;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaCSat0.c b/src/aig/gia/giaCSat0.c
deleted file mode 100644
index a0d567a2..00000000
--- a/src/aig/gia/giaCSat0.c
+++ /dev/null
@@ -1,328 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [giaCsat0.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Circuit-based SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaCsat0.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int          Sat_ObjXValue( Gia_Obj_t * pObj )          { return (pObj->fMark1 << 1) | pObj->fMark0; }
-static inline void         Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); }
-
-static inline int          Sat_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->Value > 0;                    }
-static inline void         Sat_VarAssign( Gia_Obj_t * pVar, int i )   { assert(!pVar->Value); pVar->Value = i;     }
-static inline void         Sat_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->Value);  pVar->Value = 0;     }
-static inline int          Sat_VarValue( Gia_Obj_t * pVar )           { assert(pVar->Value);  return pVar->fMark0; }
-static inline void         Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->Value);  pVar->fMark0 = v;    }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the cone and initialized them to x.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
-{
-    if ( Sat_ObjXValue(pObj) == GIA_UND )
-        return;
-    assert( pObj->Value == 0 );
-    if ( Gia_ObjIsAnd(pObj) )
-    {
-        Gia_SatCollectCone_rec( p, Gia_ObjFanin0(pObj), vVisit );
-        Gia_SatCollectCone_rec( p, Gia_ObjFanin1(pObj), vVisit );
-    }
-    assert( Sat_ObjXValue(pObj) == 0 );
-    Sat_ObjSetXValue( pObj, GIA_UND );
-    Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the cone and initialized them to x.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatCollectCone( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
-{
-    assert( !Gia_IsComplement(pObj) );
-    assert( !Gia_ObjIsConst0(pObj) );
-    assert( Sat_ObjXValue(pObj) == 0 );
-    Vec_IntClear( vVisit );
-    Gia_SatCollectCone_rec( p, pObj, vVisit );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit )
-{
-    Gia_Obj_t * pObj;
-    int i, Entry, Value, Value0, Value1;
-    assert( Gia_ObjIsCo(pRoot) );
-    assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) );
-    // collect nodes and initialized them to x
-    Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
-    // set binary values to nodes in the counter-example
-    Vec_IntForEachEntry( vCex, Entry, i )
-    {
-        pObj = Gia_NotCond( Gia_ManObj( p, Gia_Lit2Var(Entry) ), Gia_LitIsCompl(Entry) );
-        Sat_ObjSetXValue( Gia_Regular(pObj), Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE );
-        assert( Sat_ObjXValue(Gia_Regular(pObj)) == (Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE) );
-    }
-    // simulate
-    Gia_ManForEachObjVec( vVisit, p, pObj, i )
-    {
-        if ( Gia_ObjIsCi(pObj) )
-            continue;
-        assert( Gia_ObjIsAnd(pObj) );
-        Value0 = Sat_ObjXValue( Gia_ObjFanin0(pObj) );
-        Value1 = Sat_ObjXValue( Gia_ObjFanin1(pObj) );
-        Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
-        Sat_ObjSetXValue( pObj, Value );
-    }
-    Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) );
-    if ( Value != GIA_ONE )
-        printf( "Gia_SatVerifyPattern(): Verification FAILED.\n" );
-//    else
-//        printf( "Gia_SatVerifyPattern(): Verification succeeded.\n" );
-//    assert( Value == GIA_ONE );
-    // clean the nodes
-    Gia_ManForEachObjVec( vVisit, p, pObj, i )
-        Sat_ObjSetXValue( pObj, 0 );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Undoes the assignment since the given value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatUndo_rec( Gia_Obj_t * pObj, unsigned Value, Vec_Int_t * vCex )
-{
-    if ( pObj->Value < Value )
-        return;
-    pObj->Value = 0;
-    if ( Gia_ObjIsCi(pObj) )
-    {
-        if ( vCex ) Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pObj), !pObj->fPhase) );
-        return;
-    }
-    Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, vCex );
-    Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, vCex );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates assignments.]
-
-  Description [Returns 1 if UNSAT, 0 if SAT.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_SatProp_rec( Gia_Obj_t * pObj, unsigned Phase, unsigned * pValue, int * pnConfs )
-{
-    int Value = *pValue;
-    if ( pObj->Value )
-        return pObj->fPhase != Phase;
-    if ( Gia_ObjIsCi(pObj) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = Phase;
-        return 0;
-    }
-    if ( Phase ) // output of AND should be 1
-    {
-        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-            return 1;
-        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-        {
-            Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, NULL );
-            return 1;
-        }
-/*
-        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-            return 1;
-        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-        {
-            Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, NULL );
-            return 1;
-        }
-*/
-        pObj->Value = Value;
-        pObj->fPhase = 1;
-        return 0; 
-    }
-    // output of AND should be 0
-
-    (*pValue)++;
-    if ( !Gia_SatProp_rec( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = 0;
-        return 0;
-    }
-    if ( !*pnConfs )
-        return 1;
-
-    (*pValue)++;
-    if ( !Gia_SatProp_rec( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = 0;
-        return 0;
-    }
-    if ( !*pnConfs )
-        return 1;
-    // cannot be satisfied
-    (*pnConfs)--;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure to solve SAT for the node.]
-
-  Description [Returns 1 if UNSAT, 0 if SAT, and -1 if undecided.]
-               
-  SideEffects [Precondition: pObj->Value should be 0.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_SatSolve( Gia_Obj_t * pObj, unsigned Phase, int nConfsMax, Vec_Int_t * vCex )
-{
-    int Value = 1;
-    int nConfs = nConfsMax? nConfsMax : (1<<30);
-    assert( !Gia_IsComplement(pObj) );
-    assert( !Gia_ObjIsConst0(pObj) );
-    assert( pObj->Value == 0 );
-    if ( Gia_SatProp_rec( pObj, Phase, &Value, &nConfs ) )
-    {
-//        if ( nConfs )
-//            printf( "UNSAT after %d conflicts\n", nConfsMax - nConfs );
-//        else
-//            printf( "UNDEC after %d conflicts\n", nConfsMax );
-        return nConfs? 1 : -1;
-    }
-    Vec_IntClear( vCex );
-    Gia_SatUndo_rec( pObj, 1, vCex );
-//    printf( "SAT after %d conflicts\n", nConfsMax - nConfs );
-    return 0;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure to test the new SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatSolveTest( Gia_Man_t * p )
-{
-    int nConfsMax = 1000;
-    int CountUnsat, CountSat, CountUndec;
-    Vec_Int_t * vCex;
-    Vec_Int_t * vVisit;
-    Gia_Obj_t * pRoot; 
-    int i, RetValue, clk = clock();
-    // prepare AIG
-    Gia_ManCleanValue( p );
-    Gia_ManCleanMark0( p );
-    Gia_ManCleanMark1( p );
-    vCex   = Vec_IntAlloc( 100 );
-    vVisit = Vec_IntAlloc( 100 );
-    // solve for each output
-    CountUnsat = CountSat = CountUndec = 0;
-    Gia_ManForEachCo( p, pRoot, i )
-    {
-        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
-            continue;
-//printf( "Output %6d : ", i );
-        RetValue = Gia_SatSolve( Gia_ObjFanin0(pRoot), !Gia_ObjFaninC0(pRoot), nConfsMax, vCex );
-        if ( RetValue == 1 )
-            CountUnsat++;
-        else if ( RetValue == -1 )
-            CountUndec++;
-        else 
-        {
-//            Gia_Obj_t * pTemp;
-//            int k;
-            assert( RetValue == 0 );
-            CountSat++;
-/*
-            Vec_IntForEachEntry( vCex, pTemp, k )
-//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
-                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
-            printf( "\n" );
-*/
-//            Gia_SatVerifyPattern( p, pRoot, vCex, vVisit );
-        }
-//        Gia_ManCheckMark0( p );
-//        Gia_ManCheckMark1( p );
-    }
-    Vec_IntFree( vCex );
-    Vec_IntFree( vVisit );
-    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
-    ABC_PRT( "Time", clock() - clk );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/gia/giaCSat1.c b/src/aig/gia/giaCSat1.c
deleted file mode 100644
index 12b7071f..00000000
--- a/src/aig/gia/giaCSat1.c
+++ /dev/null
@@ -1,602 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [giaCsat1.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Circuit-based SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaCsat1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-
-typedef struct Css_Fan_t_ Css_Fan_t;
-struct Css_Fan_t_
-{
-    unsigned       iFan     : 31;    // ID of the fanin/fanout
-    unsigned       fCompl   :  1;    // complemented attribute
-};
-
-typedef struct Css_Obj_t_ Css_Obj_t;
-struct Css_Obj_t_
-{
-    unsigned       fCi      :  1;    // terminal node CI
-    unsigned       fCo      :  1;    // terminal node CO
-    unsigned       fAssign  :  1;    // assigned variable
-    unsigned       fValue   :  1;    // variable value
-    unsigned       fPhase   :  1;    // value under 000 pattern
-    unsigned       nFanins  :  5;    // the number of fanins
-    unsigned       nFanouts : 22;    // total number of fanouts
-    unsigned       hHandle;          // application specific data
-    union {
-    unsigned       iFanouts;         // application specific data
-    int            TravId;           // ID of the node
-    };
-    Css_Fan_t      Fanios[0];        // the array of fanins/fanouts
-};
-
-typedef struct Css_Man_t_ Css_Man_t;
-struct Css_Man_t_
-{
-    Gia_Man_t *    pGia;             // the original AIG manager
-    Vec_Int_t *    vCis;             // the vector of CIs (PIs + LOs)
-    Vec_Int_t *    vCos;             // the vector of COs (POs + LIs)
-    int            nObjs;            // the number of objects
-    int            nNodes;           // the number of nodes
-    int *          pObjData;         // the logic network defined for the AIG
-    int            nObjData;         // the size of array to store the logic network
-    int *          pLevels;          // the linked lists of levels
-    int            nLevels;          // the max number of logic levels
-    int            nTravIds;         // traversal ID to mark the cones
-    Vec_Int_t *    vTrail;           // sequence of assignments
-    int            nConfsMax;         // max number of conflicts
-};
-
-static inline unsigned    Gia_ObjHandle( Gia_Obj_t * pObj )                           { return pObj->Value;                                 } 
-
-static inline int         Css_ObjIsCi( Css_Obj_t * pObj )                             { return pObj->fCi;                                   } 
-static inline int         Css_ObjIsCo( Css_Obj_t * pObj )                             { return pObj->fCo;                                   } 
-static inline int         Css_ObjIsNode( Css_Obj_t * pObj )                           { return!pObj->fCi &&!pObj->fCo && pObj->nFanins > 0; } 
-static inline int         Css_ObjIsConst0( Css_Obj_t * pObj )                         { return!pObj->fCi &&!pObj->fCo && pObj->nFanins == 0;} 
-
-static inline int         Css_ObjFaninNum( Css_Obj_t * pObj )                         { return pObj->nFanins;                               } 
-static inline int         Css_ObjFanoutNum( Css_Obj_t * pObj )                        { return pObj->nFanouts;                              } 
-static inline int         Css_ObjSize( Css_Obj_t * pObj )                             { return sizeof(Css_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts;  } 
-static inline int         Css_ObjId( Css_Obj_t * pObj )                               { assert( 0 ); return -1;                             } 
-
-static inline Css_Obj_t * Css_ManObj( Css_Man_t * p, unsigned iHandle )               { return (Css_Obj_t *)(p->pObjData + iHandle);        } 
-static inline Css_Obj_t * Css_ObjFanin( Css_Obj_t * pObj, int i )                     { return (Css_Obj_t *)(((int *)pObj) - pObj->Fanios[i].iFan);               } 
-static inline Css_Obj_t * Css_ObjFanout( Css_Obj_t * pObj, int i )                    { return (Css_Obj_t *)(((int *)pObj) + pObj->Fanios[pObj->nFanins+i].iFan); } 
-static inline int         Css_ObjFaninC( Css_Obj_t * pObj, int i )                    { return pObj->Fanios[i].fCompl;                      } 
-static inline int         Css_ObjFanoutC( Css_Obj_t * pObj, int i )                   { return pObj->Fanios[pObj->nFanins+i].fCompl;        } 
-
-static inline int         Css_ManObjNum( Css_Man_t * p )                              { return p->nObjs;                                    } 
-static inline int         Css_ManNodeNum( Css_Man_t * p )                             { return p->nNodes;                                   } 
- 
-static inline void        Css_ManIncrementTravId( Css_Man_t * p )                     { p->nTravIds++;                                      }
-static inline void        Css_ObjSetTravId( Css_Obj_t * pObj, int TravId )            { pObj->TravId = TravId;                              }
-static inline void        Css_ObjSetTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )  { pObj->TravId = p->nTravIds;                         }
-static inline void        Css_ObjSetTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1;                     }
-static inline int         Css_ObjIsTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )   { return ((int)pObj->TravId == p->nTravIds);          }
-static inline int         Css_ObjIsTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj )  { return ((int)pObj->TravId == p->nTravIds - 1);      }
-
-static inline int   Css_VarIsAssigned( Css_Obj_t * pVar )      { return pVar->fAssign;                        }
-static inline void  Css_VarAssign( Css_Obj_t * pVar )          { assert(!pVar->fAssign); pVar->fAssign = 1;   }
-static inline void  Css_VarUnassign( Css_Obj_t * pVar )        { assert(pVar->fAssign);  pVar->fAssign = 0;   }
-static inline int   Css_VarValue( Css_Obj_t * pVar )           { assert(pVar->fAssign);  return pVar->fValue; }
-static inline void  Css_VarSetValue( Css_Obj_t * pVar, int v ) { assert(pVar->fAssign);  pVar->fValue = v;    }
-
-#define Css_ManForEachObj( p, pObj, i )               \
-    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) )
-#define Css_ManForEachObjVecStart( vVec, p, pObj, i, iStart )            \
-    for ( i = iStart; (i < Vec_IntSize(vVec)) && (pObj = Css_ManObj(p,Vec_IntEntry(vVec,i))); i++ )
-#define Css_ManForEachNode( p, pObj, i )              \
-    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) ) if ( Css_ObjIsTerm(pObj) ) {} else
-#define Css_ObjForEachFanin( pObj, pNext, i )         \
-    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)); i++ )
-#define Css_ObjForEachFanout( pObj, pNext, i )        \
-    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)); i++ )
-#define Css_ObjForEachFaninLit( pObj, pNext, fCompl, i )         \
-    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)) && ((fCompl = Css_ObjFaninC(pObj,i)),1); i++ )
-#define Css_ObjForEachFanoutLit( pObj, pNext, fCompl, i )        \
-    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)) && ((fCompl = Css_ObjFanoutC(pObj,i)),1); i++ )
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates logic network isomorphic to the given AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Css_Man_t * Css_ManCreateLogicSimple( Gia_Man_t * pGia )
-{
-    Css_Man_t * p;
-    Css_Obj_t * pObjLog, * pFanLog;
-    Gia_Obj_t * pObj;
-    int i, iHandle = 0;
-    p = ABC_CALLOC( Css_Man_t, 1 );
-    p->pGia = pGia;
-    p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
-    p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
-    p->nObjData = (sizeof(Css_Obj_t) / 4) * Gia_ManObjNum(pGia) + 4 * Gia_ManAndNum(pGia) + 2 * Gia_ManCoNum(pGia);
-    p->pObjData = ABC_CALLOC( int, p->nObjData );
-    ABC_FREE( pGia->pRefs );
-    Gia_ManCreateRefs( pGia );
-    Gia_ManForEachObj( pGia, pObj, i )
-    {
-        pObj->Value = iHandle;
-        pObjLog = Css_ManObj( p, iHandle );
-        pObjLog->nFanins  = 0;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
-        pObjLog->hHandle  = iHandle;
-        pObjLog->iFanouts = 0;
-        if ( Gia_ObjIsAnd(pObj) )
-        {
-            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
-                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
-                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
-
-            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin1(pObj)) ); 
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
-                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
-                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC1(pObj);
-
-            p->nNodes++;
-        }
-        else if ( Gia_ObjIsCo(pObj) )
-        {
-            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
-                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
-            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
-                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
-
-            pObjLog->fCo = 1;
-            Vec_IntPush( p->vCos, iHandle );
-        }
-        else if ( Gia_ObjIsCi(pObj) )
-        {
-            pObjLog->fCi = 1;
-            Vec_IntPush( p->vCis, iHandle );
-        }
-        iHandle += Css_ObjSize( pObjLog );
-        p->nObjs++;
-    }
-    assert( iHandle == p->nObjData );
-    Gia_ManForEachObj( pGia, pObj, i )
-    {
-        pObjLog = Css_ManObj( p, Gia_ObjHandle(pObj) );
-        assert( pObjLog->nFanouts == pObjLog->iFanouts );
-        pObjLog->TravId = 0;
-    }
-    p->nTravIds = 1;
-    p->vTrail = Vec_IntAlloc( 100 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates logic network isomorphic to the given AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Css_ManStop( Css_Man_t * p )
-{
-    Vec_IntFree( p->vTrail );
-    Vec_IntFree( p->vCis );
-    Vec_IntFree( p->vCos );
-    ABC_FREE( p->pObjData );
-    ABC_FREE( p->pLevels );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates implications for the net.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Css_ManImplyNet_rec( Css_Man_t * p, Css_Obj_t * pVar, unsigned Value )
-{
-    static inline Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar );
-    Css_Obj_t * pNext;
-    int i;
-    if ( !Css_ObjIsTravIdCurrent(p, pVar) )
-        return 0;
-    // assign the variable
-    assert( !Css_VarIsAssigned(pVar) );
-    Css_VarAssign( pVar );
-    Css_VarSetValue( pVar, Value );
-    Vec_IntPush( p->vTrail, pVar->hHandle );
-    // propagate fanouts, then fanins
-    Css_ObjForEachFanout( pVar, pNext, i )
-        if ( Css_ManImplyNode_rec( p, pNext ) )
-            return 1;
-    Css_ObjForEachFanin( pVar, pNext, i )
-        if ( Css_ManImplyNode_rec( p, pNext ) )
-            return 1;
-    return 0;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Propagates implications for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar )
-{
-    Css_Obj_t * pFan0, * pFan1;
-    if ( Css_ObjIsCi(pVar) )
-        return 0;
-    pFan0 = Css_ObjFanin(pVar, 0);
-    pFan1 = Css_ObjFanin(pVar, 1);
-    if ( !Css_VarIsAssigned(pVar) )
-    {
-        if ( Css_VarIsAssigned(pFan0) )
-        {
-            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> propagate
-                return Css_ManImplyNet_rec(p, pVar, 0);
-            // assigned positive
-            if ( Css_VarIsAssigned(pFan1) )
-            {
-                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
-                    return Css_ManImplyNet_rec(p, pVar, 0);
-                // asigned positive -> propagate
-                return Css_ManImplyNet_rec(p, pVar, 1);
-            }
-            return 0;
-        }
-        if ( Css_VarIsAssigned(pFan1) )
-        {
-            if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
-                return Css_ManImplyNet_rec(p, pVar, 0);
-            return 0;
-        }
-        assert( 0 );
-        return 0;
-    }
-    if ( Css_VarValue(pVar) ) // positive
-    {
-        if ( Css_VarIsAssigned(pFan0) )
-        {
-            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> conflict
-                return 1;
-            // check second var
-            if ( Css_VarIsAssigned(pFan1) )
-            {
-                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
-                    return 1;
-                // positive + positive -> nothing to do
-                return 0;
-            }
-        }
-        else
-        {
-            // pFan0 unassigned -> enqueue first var
-//            Css_ManEnqueue( p, pFan0, !Css_ObjFaninC(pVar,0) );
-            if ( Css_ManImplyNet_rec( p, pFan0, !Css_ObjFaninC(pVar,0) ) )
-                return 1;
-            // check second var
-            if ( Css_VarIsAssigned(pFan1) )
-            {
-                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
-                    return 1;
-                // positive + positive -> nothing to do
-                return 0;
-            }
-        }
-        // unassigned -> enqueue second var
-//        Css_ManEnqueue( p, pFan1, !Css_ObjFaninC(pVar,1) );
-        return Css_ManImplyNet_rec( p, pFan1, !Css_ObjFaninC(pVar,1) );
-    }
-    else // negative
-    {
-        if ( Css_VarIsAssigned(pFan0) )
-        {
-            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> nothing to do
-                return 0;
-            if ( Css_VarIsAssigned(pFan1) )
-            {
-                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
-                    return 0;
-                // positive + positive -> conflict
-                return 1;
-            }
-            // positive + unassigned -> enqueue second var
-//            Css_ManEnqueue( p, pFan1, Css_ObjFaninC(pVar,1) );
-            return Css_ManImplyNet_rec( p, pFan1, Css_ObjFaninC(pVar,1) );
-        }
-        else
-        {
-            if ( Css_VarIsAssigned(pFan1) )
-            {
-                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
-                    return 0;
-                // unassigned + positive -> enqueue first var
-//                Css_ManEnqueue( p, pFan0, Css_ObjFaninC(pVar,0) );
-                return Css_ManImplyNet_rec( p, pFan0, Css_ObjFaninC(pVar,0) );
-            }
-        }
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Css_ManCancelUntil( Css_Man_t * p, int iBound, Vec_Int_t * vCex )
-{
-    Css_Obj_t * pVar;
-    int i;
-    Css_ManForEachObjVecStart( p->vTrail, p, pVar, i, iBound )
-    {
-        if ( vCex )  
-            Vec_IntPush( vCex, Gia_Var2Lit(Css_ObjId(pVar), !pVar->fValue) );
-        Css_VarUnassign( pVar );
-    }
-    Vec_IntShrink( p->vTrail, iBound );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Justifies assignments.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Css_ManJustify( Css_Man_t * p, int iBegin )
-{
-    Css_Obj_t * pVar, * pFan0, * pFan1;
-    int iState, iThis;
-    if ( p->nConfsMax == 0 )
-        return 1;
-    // get the next variable to justify
-    Css_ManForEachObjVecStart( p->vTrail, p, pVar, iThis, iBegin )
-    {
-        assert( Css_VarIsAssigned(pVar) );
-        if ( Css_VarValue(pVar) || Css_ObjIsCi(pVar) )
-            continue;
-        pFan0 = Css_ObjFanin(pVar,0);
-        pFan1 = Css_ObjFanin(pVar,0);
-        if ( !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) )
-            break;
-    }
-    if ( iThis == Vec_IntSize(p->vTrail) ) // could not find
-        return 0;
-    // found variable to justify
-    assert( !Css_VarValue(pVar) && !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) );
-    // remember the state of the stack
-    iState = Vec_IntSize( p->vTrail );
-    // try to justify by setting first fanin to 0
-    if ( !Css_ManImplyNet_rec(p, pFan0, 0) && !Css_ManJustify(p, iThis) )
-        return 0;
-    Css_ManCancelUntil( p, iState, NULL );
-    if ( p->nConfsMax == 0 )
-        return 1;
-    // try to justify by setting second fanin to 0
-    if ( !Css_ManImplyNet_rec(p, pFan1, 0) && !Css_ManJustify(p, iThis) )
-        return 0;
-    Css_ManCancelUntil( p, iState, NULL );
-    if ( p->nConfsMax == 0 )
-        return 1;
-    p->nConfsMax--;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marsk logic cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Css_ManMarkCone_rec( Css_Man_t * p, Css_Obj_t * pVar )
-{
-    if ( Css_ObjIsTravIdCurrent(p, pVar) )
-        return;
-    Css_ObjSetTravIdCurrent(p, pVar);
-    assert( !Css_VarIsAssigned(pVar) );
-    if ( Css_ObjIsCi(pVar) )
-        return;
-    else
-    {
-        Css_Obj_t * pNext;
-        int i;
-        Css_ObjForEachFanin( pVar, pNext, i )
-            Css_ManMarkCone_rec( p, pNext );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs one call to the SAT solver.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Css_ManPrepare( Css_Man_t * p, int * pLits, int nLits )
-{
-    Css_Obj_t * pVar;
-    int i;
-    // mark the cone
-    Css_ManIncrementTravId( p );
-    for ( i = 0; i < nLits; i++ )
-    {
-        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
-        Css_ManMarkCone_rec( p, pVar );
-    }
-    // assign literals
-    Vec_IntClear( p->vTrail );
-    for ( i = 0; i < nLits; i++ )
-    {
-        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
-        if ( Css_ManImplyNet_rec( p, pVar, !Gia_LitIsCompl(pLits[i]) ) )
-        {
-            Css_ManCancelUntil( p, 0, NULL );
-            return 1;
-        }
-    }
-    return 0;
-}
- 
-
-/**Function*************************************************************
-
-  Synopsis    [Runs one call to the SAT solver.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Css_ManSolve( Css_Man_t * p, int * pLits, int nLits, int nConfsMax, Vec_Int_t * vCex )
-{
-    // propagate the assignments
-    if ( Css_ManPrepare( p, pLits, nLits ) )
-        return 1;
-    // justify the assignments
-    p->nConfsMax = nConfsMax;
-    if ( Css_ManJustify( p, 0 ) )
-        return p->nConfsMax? 1 : -1;
-    // derive model and return the solver to the initial state
-    Vec_IntClear( vCex );
-    Css_ManCancelUntil( p, 0, vCex );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure to test the new SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatSolveTest2( Gia_Man_t * pGia )
-{
-    extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
-    int nConfsMax = 1000;
-    int CountUnsat, CountSat, CountUndec;
-    Css_Man_t * p; 
-    Vec_Int_t * vCex;
-    Vec_Int_t * vVisit;
-    Gia_Obj_t * pRoot; 
-    int i, RetValue, iLit, clk = clock();
-    // create logic network
-    p = Css_ManCreateLogicSimple( pGia );
-    // prepare AIG
-    Gia_ManCleanValue( pGia );
-    Gia_ManCleanMark0( pGia );
-    Gia_ManCleanMark1( pGia );
-    vCex   = Vec_IntAlloc( 100 );
-    vVisit = Vec_IntAlloc( 100 );
-    // solve for each output
-    CountUnsat = CountSat = CountUndec = 0;
-    Gia_ManForEachCo( pGia, pRoot, i )
-    {
-        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
-            continue;
-//printf( "Output %6d : ", i );
-        iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
-        RetValue = Css_ManSolve( p, &iLit, 1, nConfsMax, vCex );
-        if ( RetValue == 1 )
-            CountUnsat++;
-        else if ( RetValue == -1 )
-            CountUndec++;
-        else 
-        {
-//            Gia_Obj_t * pTemp;
-//            int k;
-            assert( RetValue == 0 );
-            CountSat++;
-/*
-            Vec_PtrForEachEntry( vCex, pTemp, k )
-//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
-                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
-            printf( "\n" );
-*/
-            Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
-        }
-//        Gia_ManCheckMark0( p );
-//        Gia_ManCheckMark1( p );
-    }
-    Css_ManStop( p );
-    Vec_IntFree( vCex );
-    Vec_IntFree( vVisit );
-    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
-    ABC_PRT( "Time", clock() - clk );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/gia/giaCSatA.c b/src/aig/gia/giaCSatA.c
deleted file mode 100644
index 12f6895a..00000000
--- a/src/aig/gia/giaCSatA.c
+++ /dev/null
@@ -1,103 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [giaSolver.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Circuit-based SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sat_Cla_t_ Sat_Cla_t;
-struct Sat_Cla_t_
-{
-    unsigned       hWatch0;          // watched list for 0 literal
-    unsigned       hWatch1;          // watched list for 1 literal
-    int            Activity;         // activity of the clause
-    int            nLits;            // the number of literals
-    int            pLits[0];         // the array of literals  
-};
-
-typedef struct Sat_Fan_t_ Sat_Fan_t;
-struct Sat_Fan_t_
-{
-    unsigned       iFan      : 31;   // ID of the fanin/fanout
-    unsigned       fCompl    :  1;   // complemented attribute
-};
-
-typedef struct Sat_Obj_t_ Sat_Obj_t;
-struct Sat_Obj_t_
-{
-    unsigned       hHandle;          // node handle
-    unsigned       fAssign   :  1;   // terminal node (CI/CO)
-    unsigned       fValue    :  1;   // value under 000 pattern
-    unsigned       fMark0    :  1;   // first user-controlled mark
-    unsigned       fMark1    :  1;   // second user-controlled mark
-    unsigned       nFanouuts : 28;   // the number of fanouts
-    unsigned       nFanins   :  8;   // the number of fanins
-    unsigned       Level     : 24;   // logic level
-    unsigned       hNext;            // next one on this level 
-    unsigned       hWatch0;          // watched list for 0 literal
-    unsigned       hWatch1;          // watched list for 1 literal
-    unsigned       hReason;          // reason for this variable
-    unsigned       Depth;            // decision depth
-    Sat_Fan_t      Fanios[0];        // the array of fanins/fanouts
-};
-
-typedef struct Sat_Man_t_ Sat_Man_t;
-struct Sat_Man_t_
-{
-    Gia_Man_t *    pGia;             // the original AIG manager
-    // circuit
-    Vec_Int_t      vCis;             // the vector of CIs (PIs + LOs)
-    Vec_Int_t      vObjs;            // the vector of objects
-    // learned clauses         
-    Vec_Int_t      vClauses;         // the vector of clauses
-    // solver data
-    Vec_Int_t      vTrail;           // variable queue               
-    Vec_Int_t      vTrailLim;        // pointer into the trail               
-    int            iHead;            // variable queue 
-    int            iTail;            // variable queue
-    int            iRootLevel;       // first decision
-    // levelized order
-    int            iLevelTop;        // the largest unassigned level 
-    Vec_Int_t      vLevels;          // the linked lists of levels
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/gia/giaCSatB.c b/src/aig/gia/giaCSatB.c
deleted file mode 100644
index e1f68c6f..00000000
--- a/src/aig/gia/giaCSatB.c
+++ /dev/null
@@ -1,490 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [giaSolver.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Circuit-based SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sat_Man_t_ Sat_Man_t;
-struct Sat_Man_t_
-{
-    Gia_Man_t *    pGia;             // the original AIG manager
-    Vec_Int_t *    vModel;           // satisfying PI assignment
-    int            nConfs;           // cur number of conflicts
-    int            nConfsMax;        // max number of conflicts
-    int            iHead;            // variable queue 
-    int            iTail;            // variable queue
-    int            iJust;            // head of justification
-    int            nTrail;           // variable queue size
-    int            pTrail[0];        // variable queue data
-};
-
-static inline int          Sat_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
-static inline void         Sat_VarAssign( Gia_Obj_t * pVar )          { assert(!pVar->fMark0); pVar->fMark0 = 1;    }
-static inline void         Sat_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->fMark0);  pVar->fMark0 = 0;    }
-static inline int          Sat_VarValue( Gia_Obj_t * pVar )           { assert(pVar->fMark0);  return pVar->fMark1; }
-static inline void         Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0);  pVar->fMark1 = v;    }
-
-extern void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat );
-extern void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sat_Man_t * Sat_ManCreate( Gia_Man_t * pGia )
-{
-    Sat_Man_t * p;
-    p = (Sat_Man_t *)ABC_ALLOC( char, sizeof(Sat_Man_t) + sizeof(int)*Gia_ManObjNum(pGia) );
-    memset( p, 0, sizeof(Sat_Man_t) );
-    p->pGia   = pGia;
-    p->nTrail = Gia_ManObjNum(pGia);
-    p->vModel = Vec_IntAlloc( 1000 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_ManDelete( Sat_Man_t * p )
-{
-    Vec_IntFree( p->vModel );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sat_ManCancelUntil( Sat_Man_t * p, int iBound )
-{
-    Gia_Obj_t * pVar;
-    int i;
-    for ( i = p->iTail-1; i >= iBound; i-- )
-    {
-        pVar = Gia_ManObj( p->pGia, p->pTrail[i] );
-        Sat_VarUnassign( pVar );
-    }
-    p->iTail = p->iTail = iBound;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sat_ManDeriveModel( Sat_Man_t * p )
-{
-    Gia_Obj_t * pVar;
-    int i;
-    Vec_IntClear( p->vModel );
-    for ( i = 0; i < p->iTail; i++ )
-    {
-        pVar = Gia_ManObj( p->pGia, p->pTrail[i] );
-        if ( Gia_ObjIsCi(pVar) )
-            Vec_IntPush( p->vModel, Gia_ObjCioId(pVar) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sat_ManEnqueue( Sat_Man_t * p, Gia_Obj_t * pVar, int Value )
-{
-    assert( p->iTail < p->nTrail );
-    Sat_VarAssign( pVar );
-    Sat_VarSetValue( pVar, Value );
-    p->pTrail[p->iTail++] = Gia_ObjId(p->pGia, pVar);
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sat_ManAssume( Sat_Man_t * p, Gia_Obj_t * pVar, int Value )
-{
-    assert( p->iHead == p->iTail );
-    Sat_ManEnqueue( p, pVar, Value );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates one assignment.]
-
-  Description [Returns 1 if there is no conflict, 0 otherwise.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sat_ManPropagateOne( Sat_Man_t * p, int iPos )
-{
-    Gia_Obj_t * pVar, * pFan0, * pFan1;
-    pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] );
-    if ( Gia_ObjIsCi(pVar) )
-        return 1;
-    pFan0 = Gia_ObjFanin0(pVar);
-    pFan1 = Gia_ObjFanin1(pVar);
-    if ( Sat_VarValue(pVar) ) // positive
-    {
-        if ( Sat_VarIsAssigned(pFan0) )
-        {
-            if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> conflict
-                return 0;
-            // check second var
-            if ( Sat_VarIsAssigned(pFan1) )
-            {
-                if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict
-                    return 0;
-                // positive + positive -> nothing to do
-                return 1;
-            }
-        }
-        else
-        {
-            // pFan0 unassigned -> enqueue first var
-            Sat_ManEnqueue( p, pFan0, !Gia_ObjFaninC0(pVar) );
-            // check second var
-            if ( Sat_VarIsAssigned(pFan1) )
-            {
-                if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict
-                    return 0;
-                // positive + positive -> nothing to do
-                return 1;
-            }
-        }
-        // unassigned -> enqueue second var
-        Sat_ManEnqueue( p, pFan1, !Gia_ObjFaninC1(pVar) );
-    }
-    else // negative
-    {
-        if ( Sat_VarIsAssigned(pFan0) )
-        {
-            if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> nothing to do
-                return 1;
-            if ( Sat_VarIsAssigned(pFan1) )
-            {
-                if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do
-                    return 1;
-                // positive + positive -> conflict
-                return 0;
-            }
-            // positive + unassigned -> enqueue second var
-            Sat_ManEnqueue( p, pFan1, Gia_ObjFaninC1(pVar) );
-        }
-        else
-        {
-            if ( Sat_VarIsAssigned(pFan1) )
-            {
-                if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do
-                    return 1;
-                // unassigned + positive -> enqueue first var
-                Sat_ManEnqueue( p, pFan0, Gia_ObjFaninC0(pVar) );
-            }
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates assignments.]
-
-  Description [Returns 1 if there is no conflict.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sat_ManPropagate( Sat_Man_t * p )
-{
-    assert( p->iHead <= p->iTail );
-    for ( ; p->iHead < p->iTail; p->iHead++ )
-        if ( !Sat_ManPropagateOne( p, p->pTrail[p->iHead] ) )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates one assignment.]
-
-  Description [Returns 1 if justified, 0 if conflict, -1 if needs justification.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sat_ManJustifyNextOne( Sat_Man_t * p, int iPos )
-{
-    Gia_Obj_t * pVar, * pFan0, * pFan1;
-    pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] );
-    if ( Gia_ObjIsCi(pVar) )
-        return 1;
-    pFan0 = Gia_ObjFanin0(pVar);
-    pFan1 = Gia_ObjFanin1(pVar);
-    if ( Sat_VarValue(pVar) ) // positive
-        return 1;
-    // nevative
-    if ( Sat_VarIsAssigned(pFan0) )
-    {
-        if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> already justified
-            return 1;
-        // positive
-        if ( Sat_VarIsAssigned(pFan1) )
-        {
-            if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified
-                return 1;
-            // positive -> conflict
-            return 0;
-        }
-        // unasigned -> propagate
-        Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) );
-        return Sat_ManPropagate(p);
-    }
-    if ( Sat_VarIsAssigned(pFan1) )
-    {
-        if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified
-            return 1;
-        // positive
-        assert( !Sat_VarIsAssigned(pFan0) );
-        // unasigned -> propagate
-        Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) );
-        return Sat_ManPropagate(p);
-    }
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Justifies assignments.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sat_ManJustify( Sat_Man_t * p )
-{
-    Gia_Obj_t * pVar, * pFan0, * pFan1;
-    int RetValue, iState, iJustState;
-    if ( p->nConfs && p->nConfs >= p->nConfsMax )
-        return -1;
-    // get the next variable to justify
-    assert( p->iJust <= p->iTail );
-    iJustState = p->iJust;
-    for ( ; p->iJust < p->iTail; p->iJust++ )
-    {
-        RetValue = Sat_ManJustifyNextOne( p, p->pTrail[p->iJust] );
-        if ( RetValue == 0 )
-            return 1;
-        if ( RetValue == -1 )
-            break;
-    }
-    if ( p->iJust == p->iTail ) // could not find
-        return 0;
-    // found variable to justify
-    pVar = Gia_ManObj( p->pGia, p->pTrail[p->iJust] );
-    pFan0 = Gia_ObjFanin0(pVar);
-    pFan1 = Gia_ObjFanin1(pVar);
-    assert( !Sat_VarValue(pVar) && !Sat_VarIsAssigned(pFan0) && !Sat_VarIsAssigned(pFan1) );
-    // remember the state of the stack
-    iState = p->iHead;
-    // try to justify by setting first fanin to 0
-    Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) );
-    if ( Sat_ManPropagate(p) ) 
-    {
-        RetValue = Sat_ManJustify(p);
-        if ( RetValue != 1 )
-            return RetValue;
-    }
-    Sat_ManCancelUntil( p, iState );
-    // try to justify by setting second fanin to 0
-    Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) );
-    if ( Sat_ManPropagate(p) ) 
-    {
-        RetValue = Sat_ManJustify(p);
-        if ( RetValue != 1 )
-            return RetValue;
-    }
-    Sat_ManCancelUntil( p, iState );
-    p->iJust = iJustState;
-    p->nConfs++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs one call to the SAT solver.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sat_ManPrepare( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax )
-{
-    Gia_Obj_t * pVar;
-    int i;
-    // double check that vars are unassigned
-    Gia_ManForEachObj( p->pGia, pVar, i )
-        assert( !Sat_VarIsAssigned(pVar) );
-    // prepare
-    p->iHead = p->iTail = p->iJust = 0;
-    p->nConfsMax = nConfsMax;
-    // assign literals
-    for ( i = 0; i < nLits; i++ )
-    {
-        pVar = Gia_ManObj( p->pGia, Gia_Lit2Var(pLits[i]) );
-        if ( Sat_VarIsAssigned(pVar) ) // assigned
-        {
-            if ( Sat_VarValue(pVar) != Gia_LitIsCompl(pLits[i]) ) // compatible assignment
-                continue;
-        }
-        else // unassigned
-        {
-            Sat_ManAssume( p, pVar, !Gia_LitIsCompl(pLits[i]) );
-            if ( Sat_ManPropagate(p) ) 
-                continue;
-        }
-        // conflict
-        Sat_ManCancelUntil( p, 0 );
-        return 1;
-    }
-    assert( p->iHead == p->iTail );
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Runs one call to the SAT solver.]
-
-  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sat_ManSolve( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax )
-{
-    int RetValue;
-    // propagate the assignments
-    if ( Sat_ManPrepare( p, pLits, nLits, nConfsMax ) )
-        return 1;
-    // justify the assignments
-    RetValue = Sat_ManJustify( p );
-    if ( RetValue == 0 ) // SAT
-        Sat_ManDeriveModel( p );
-    // return the solver to the initial state
-    Sat_ManCancelUntil( p, 0 );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Testing the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax )
-{
-    Sat_Man_t * p;
-    int RetValue, iLit;
-    assert( Gia_ObjIsCo(pObj) );
-    p = Sat_ManCreate( pGia );
-    iLit = Gia_LitNot( Gia_ObjFaninLit0p(pGia, pObj) );
-    RetValue = Sat_ManSolve( p, &iLit, 1, nConfsMax );
-    if ( RetValue == 0 )
-    {
-        Cec_ManPatVerifyPattern( pGia, pObj, p->vModel );
-        Cec_ManPatCleanMark0( pGia, pObj );
-    }
-    Sat_ManDelete( p );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index c5efa839..b256100c 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -859,7 +859,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
     if ( fVerbose )
     { 
         printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) );
-        Gia_ManPrintStats( p );
+        Gia_ManPrintStats( p, 0 );
     }
     if ( Vec_IntSize( vSigs ) > 200 )
     {
@@ -885,7 +885,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
         if ( fVerbose )
             printf( "Cofactored variable %d.\n", iVar );
         if ( fVerbose )
-            Gia_ManPrintStats( pAig );
+            Gia_ManPrintStats( pAig, 0 );
     }
     Vec_IntFree( vSigsNew );
     return pAig;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 0c536dab..2510f572 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -30,6 +30,226 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Removes pointers to the unmarked nodes..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr, iPrev;
+    if ( p->pReprs == NULL )
+        return;
+    assert( pNew->pReprs == NULL && pNew->pNexts == NULL );
+    // start representatives
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
+    for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = iPrev = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+        {
+            Gia_ObjSetRepr( pNew, iNode, iRepr );
+            assert( iPrev < iNode );
+            iPrev = iNode;
+        }
+    }
+    Vec_IntFree( vClass );
+    pNew->pNexts = Gia_ManDeriveNexts( pNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps combinational inputs when objects are DFS ordered.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapCis( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Vec_IntSize(p->vCis) == Vec_IntSize(pNew->vCis) );
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        assert( Gia_ObjCioId(pObj) == i );
+        pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
+        assert( !Gia_IsComplement(pObjNew) );
+        Vec_IntWriteEntry( pNew->vCis, i, Gia_ObjId(pNew, pObjNew) );
+        Gia_ObjSetCioId( pObjNew, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps combinational outputs when objects are DFS ordered.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapCos( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Vec_IntSize(p->vCos) == Vec_IntSize(pNew->vCos) );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        assert( Gia_ObjCioId(pObj) == i );
+        pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
+        assert( !Gia_IsComplement(pObjNew) );
+        Vec_IntWriteEntry( pNew->vCos, i, Gia_ObjId(pNew, pObjNew) );
+        Gia_ObjSetCioId( pObjNew, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManDupOrderDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManForEachCi( p, pObj, i )
+        if ( !~pObj->Value )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    Gia_ManDupRemapCis( pNew, p );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCoReverse( p, pObj, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManForEachCi( p, pObj, i )
+        if ( !~pObj->Value )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    Gia_ManDupRemapCis( pNew, p );
+    Gia_ManDupRemapCos( pNew, p );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting first PIs, then nodes, then POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    assert( Gia_ManIsNormalized(pNew) );
+    return pNew;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG without any changes.]
 
   Description []
@@ -296,7 +516,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     if ( pNew->pHTable )
         return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-}
+} 
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 6c2f00df..fa172f70 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -36,6 +36,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define GIA_PLACE_SIZE 0x7fff 
+// objects will be placed in box [0, GIA_PLACE_SIZE] x [0, GIA_PLACE_SIZE]
 
 typedef float  Emb_Dat_t;
 
@@ -247,6 +249,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
         Emb_ObjAddFanin( Emb_ManObj(p,Gia_ObjValue(pObjRo)), Emb_ManObj(p,Gia_ObjValue(pObjRi)) );
     assert( nNodes  == Emb_ManNodeNum(p) );
     assert( hHandle == p->nObjData );
+    assert( p->nObjs == Gia_ManObjNum(pGia) );
     if ( hHandle != p->nObjData )
         printf( "Emb_ManStartSimple(): Fatal error in internal representation.\n" );
     // make sure the fanin/fanout counters are correct
@@ -1407,7 +1410,7 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
 
 /**Function*************************************************************
 
-  Synopsis    [Projects into square of size [0;0xffff] x [0;0xffff].]
+  Synopsis    [Projects into square of size [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE].]
 
   Description []
                
@@ -1432,7 +1435,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
         Min0 = ABC_MIN( Min0, pY0[k] );
         Max0 = ABC_MAX( Max0, pY0[k] );
     }
-    Str0 = 1.0*0xffff/(Max0 - Min0);
+    Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0);
     // update the coordinates
     for ( k = 0; k < p->nObjs; k++ )
         pY0[k] = (pY0[k] != 0.0) ? ((pY0[k] - Min0) * Str0) : 0.0;
@@ -1446,7 +1449,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
         Min1 = ABC_MIN( Min1, pY1[k] );
         Max1 = ABC_MAX( Max1, pY1[k] );
     }
-    Str1 = 1.0*0xffff/(Max1 - Min1);
+    Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1);
     // update the coordinates
     for ( k = 0; k < p->nObjs; k++ )
         pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0;
@@ -1455,12 +1458,12 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
     pPerm0 = Gia_SortFloats( pY0, NULL, p->nObjs );
     pPerm1 = Gia_SortFloats( pY1, NULL, p->nObjs );
 
-    // average solutions and project them into square [0;0xffff] x [0;0xffff]
+    // average solutions and project them into square [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE]
     p->pPlacement = ABC_ALLOC( unsigned short, 2 * p->nObjs );
     for ( k = 0; k < p->nObjs; k++ )
     {
-        p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
-        p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+        p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
+        p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
     }
     ABC_FREE( pPerm0 );
     ABC_FREE( pPerm1 );
@@ -1568,8 +1571,8 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
         pPermY = Gia_SortFloats( pVertY, NULL, p->nObjs );
         for ( k = 0; k < p->nObjs; k++ )
         {
-            p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
-            p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+            p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
+            p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
         }
         ABC_FREE( pPermX );
         ABC_FREE( pPermY );
@@ -1783,7 +1786,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
 void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars )
 {
     Emb_Man_t * p;
-    int clk, clkSetup;
+    int i, clk, clkSetup;
 //   Gia_ManTestDistance( pGia );
 
     // transform AIG into internal data-structure
@@ -1843,6 +1846,17 @@ if ( pPars->fVerbose )
 ABC_PRT( "Image dump", clock() - clk );
     }
 
+    // transfer placement
+    if ( Gia_ManObjNum(pGia) == p->nObjs )
+    {
+        // assuming normalized ordering of the AIG
+        pGia->pPlacement = ABC_CALLOC( Gia_Plc_t, p->nObjs );
+        for ( i = 0; i < p->nObjs; i++ ) 
+        {
+            pGia->pPlacement[i].xCoord = p->pPlacement[2*i+0];
+            pGia->pPlacement[i].yCoord = p->pPlacement[2*i+1];
+        }
+    }
     Emb_ManStop( p );
 }
 
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index b87c77e5..79345fd0 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -226,6 +226,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
+        printf( "Const0 = " );
+        Gia_ManForEachConst( p, i )
+            printf( "%d ", i );
+        printf( "\n" );
         Counter = 0;
         Gia_ManForEachClass( p, i )
             Gia_ManEquivPrintOne( p, i, ++Counter );
@@ -275,15 +279,15 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
 void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     Gia_Obj_t * pRepr;
-    if ( ~pObj->Value )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
     if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
     {
         Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
         pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
     Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
     Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -303,18 +307,25 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
 Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew;
-    Gia_Obj_t * pObj, * pRepr;
+    Gia_Obj_t * pObj;
     int i;
+    if ( !p->pReprs )
+    {
+        printf( "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
+        return NULL;
+    }
     if ( fDualOut && (Gia_ManPoNum(p) & 1) )
     {
         printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     Gia_ManSetPhase( p );
     if ( fDualOut )
         Gia_ManEquivSetColors( p, fVerbose );
@@ -323,11 +334,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-    {
         pObj->Value = Gia_ManAppendCi(pNew);
-        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-    }
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
@@ -662,11 +669,13 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
         printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
@@ -786,11 +795,13 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     vXorLits = Vec_IntAlloc( 1000 );
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 8bc38ed9..a7cae8fe 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
 void Gia_ManHashAlloc( Gia_Man_t * p )  
 {
     assert( p->pHTable == NULL );
-    p->nHTable = Aig_PrimeCudd( p->nObjsAlloc / 3 );
+    p->nHTable = Aig_PrimeCudd( p->nObjsAlloc );
     p->pHTable = ABC_CALLOC( int, p->nHTable );
 }
 
@@ -174,6 +174,34 @@ void Gia_ManHashResize( Gia_Man_t * p )
     ABC_FREE( pHTableOld );
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Gia_ManHashProfile( Gia_Man_t * p )
+{
+    Gia_Obj_t * pEntry;
+    int i, Counter;
+    printf( "Table size = %d. Entries = %d.\n", p->nHTable, Gia_ManAndNum(p) );
+    for ( i = 0; i < p->nHTable; i++ )
+    {
+        Counter = 0;
+        for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL); 
+              pEntry; 
+              pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) )
+            Counter++;
+        if ( Counter ) 
+            printf( "%d ", Counter );
+    }
+    printf( "\n" );
+}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 4439453d..dba90507 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -70,6 +70,8 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pPlacement );
+    ABC_FREE( p->pSwitching );
     ABC_FREE( p->pCexComb );
     ABC_FREE( p->pIso );
     ABC_FREE( p->pMapping );
@@ -128,17 +130,48 @@ void Gia_ManPrintClasses( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintStats( Gia_Man_t * p )
+void Gia_ManPrintPlacement( Gia_Man_t * p )
+{
+    int i, nFixed = 0, nUndef = 0;
+    if ( p->pPlacement == NULL )
+        return;
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        nFixed += p->pPlacement[i].fFixed;
+        nUndef += p->pPlacement[i].fUndef;
+    }
+    printf( "Placement:  Objects = %8d.  Fixed = %8d.  Undef = %8d.\n", Gia_ManObjNum(p), nFixed, nUndef );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 {
     if ( p->pName )
         printf( "%8s : ", p->pName );
-    printf( "i/o =%7d/%7d  ", Gia_ManPiNum(p), Gia_ManPoNum(p) );
+    printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
     if ( Gia_ManRegNum(p) )
-        printf( "ff =%7d  ", Gia_ManRegNum(p) );
-    printf( "and =%8d  ", Gia_ManAndNum(p) );
-    printf( "lev =%5d  ", Gia_ManLevelNum(p) );
-    printf( "cut =%5d  ", Gia_ManCrossCut(p) );
-    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+        printf( "  ff =%7d", Gia_ManRegNum(p) );
+    printf( "  and =%8d", Gia_ManAndNum(p) );
+    printf( "  lev =%5d", Gia_ManLevelNum(p) );
+    printf( "  cut =%5d", Gia_ManCrossCut(p) );
+    printf( "  mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+    if ( fSwitch )
+    {
+        if ( p->pSwitching )
+            printf( "  power =%7.2f", Gia_ManEvaluateSwitching(p) );
+        else
+            printf( "  power =%7.2f", Gia_ManComputeSwitching(p, 48, 16, 0) );
+    }
 //    printf( "obj =%5d  ", Gia_ManObjNum(p) );
     printf( "\n" );
 
@@ -147,6 +180,8 @@ void Gia_ManPrintStats( Gia_Man_t * p )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
     if ( p->pMapping )
         Gia_ManPrintMappingStats( p );
+    if ( p->pPlacement )
+        Gia_ManPrintPlacement( p );
     // print register classes
 //    Gia_ManPrintClasses( p );
 }
diff --git a/src/aig/gia/giaPat.c b/src/aig/gia/giaPat.c
new file mode 100644
index 00000000..7968932c
--- /dev/null
+++ b/src/aig/gia/giaPat.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+  FileName    [gia.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int   Sat_ObjXValue( Gia_Obj_t * pObj )          { return (pObj->fMark1 << 1) | pObj->fMark0;             }
+static inline void  Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone and initialized them to x.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
+{
+    if ( Sat_ObjXValue(pObj) == GIA_UND )
+        return;
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_SatCollectCone_rec( p, Gia_ObjFanin0(pObj), vVisit );
+        Gia_SatCollectCone_rec( p, Gia_ObjFanin1(pObj), vVisit );
+    }
+    assert( Sat_ObjXValue(pObj) == 0 );
+    Sat_ObjSetXValue( pObj, GIA_UND );
+    Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone and initialized them to x.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatCollectCone( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
+{
+    assert( !Gia_IsComplement(pObj) );
+    assert( !Gia_ObjIsConst0(pObj) );
+    assert( Sat_ObjXValue(pObj) == 0 );
+    Vec_IntClear( vVisit );
+    Gia_SatCollectCone_rec( p, pObj, vVisit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the counter-examples asserts the output.]
+
+  Description [Assumes that fMark0 and fMark1 are clean. Leaves them clean.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit )
+{
+    Gia_Obj_t * pObj;
+    int i, Entry, Value, Value0, Value1;
+    assert( Gia_ObjIsCo(pRoot) );
+    assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) );
+    // collect nodes and initialized them to x
+    Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
+    // set binary values to nodes in the counter-example
+    Vec_IntForEachEntry( vCex, Entry, i )
+//        Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
+        Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
+    // simulate
+    Gia_ManForEachObjVec( vVisit, p, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) )
+            continue;
+        assert( Gia_ObjIsAnd(pObj) );
+        Value0 = Sat_ObjXValue( Gia_ObjFanin0(pObj) );
+        Value1 = Sat_ObjXValue( Gia_ObjFanin1(pObj) );
+        Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
+        Sat_ObjSetXValue( pObj, Value );
+    }
+    Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) );
+    if ( Value != GIA_ONE )
+        printf( "Gia_SatVerifyPattern(): Verification FAILED.\n" );
+//    else
+//        printf( "Gia_SatVerifyPattern(): Verification succeeded.\n" );
+//    assert( Value == GIA_ONE );
+    // clean the nodes
+    Gia_ManForEachObjVec( vVisit, p, pObj, i )
+        Sat_ObjSetXValue( pObj, 0 );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 71aefec3..713f224b 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -73,13 +73,13 @@ static inline unsigned * Gia_SwiDataCo( Gia_ManSwi_t * p, int i )  { return p->p
 void Gia_ManSetDefaultParamsSwi( Gia_ParSwi_t * p )
 {
     memset( p, 0, sizeof(Gia_ParSwi_t) );
-    p->nWords        =   1;  // the number of machine words of simulatation data 
+    p->nWords        =  10;  // the number of machine words of simulatation data 
     p->nIters        =  48;  // the number of all timeframes to simulate
     p->nPref         =  16;  // the number of first timeframes to skip when computing switching
     p->nRandPiFactor =   2;  // primary input transition probability (-1=3/8; 0=1/2; 1=1/4; 2=1/8, etc)
     p->fProbOne      =   0;  // compute probability of signal being one (if 0, compute probability of switching)
     p->fProbTrans    =   1;  // compute signal transition probability (if 0, compute transition probability using probability of being one)
-    p->fVerbose      =   1;  // enables verbose output
+    p->fVerbose      =   0;  // enables verbose output
 }
 
 /**Function*************************************************************
@@ -483,12 +483,14 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount )
         else if ( Gia_ObjIsCo(pObj) )
         {
             assert( Gia_ObjValue(pObj) == GIA_NONE );
-            Gia_ManSwiSimulateCo( p, iCos++, pObj );
+//            Gia_ManSwiSimulateCo( p, iCos++, pObj );
+            Gia_ManSwiSimulateCo( p, Gia_ObjCioId(pObj), pObj );
         }
         else // if ( Gia_ObjIsCi(pObj) )
         {
             assert( Gia_ObjValue(pObj) < p->pAig->nFront );
-            Gia_ManSwiSimulateCi( p, pObj, iCis++ );
+//            Gia_ManSwiSimulateCi( p, pObj, iCis++ );
+            Gia_ManSwiSimulateCi( p, pObj, Gia_ObjCioId(pObj) );
         }
         if ( fCount && !Gia_ObjIsCo(pObj) )
         {
@@ -498,8 +500,8 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount )
                 p->pData1[i] += Gia_ManSwiSimInfoCountOnes( p, Gia_ObjValue(pObj) );
         }
     }
-    assert( Gia_ManCiNum(p->pAig) == iCis );
-    assert( Gia_ManCoNum(p->pAig) == iCos );
+//    assert( Gia_ManCiNum(p->pAig) == iCis );
+//    assert( Gia_ManCoNum(p->pAig) == iCos );
 }
 
 /**Function*************************************************************
@@ -633,12 +635,10 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
     // set the default parameters
     Gia_ManSetDefaultParamsSwi( pPars ); 
     // override some of the defaults
-    pPars->nWords   = 10;       // set number machine words to simulate
     pPars->nIters   = nFrames;  // set number of total timeframes
     if ( Abc_FrameReadFlag("seqsimframes") )
         pPars->nIters = atoi( Abc_FrameReadFlag("seqsimframes") );
     pPars->nPref    = nPref;    // set number of first timeframes to skip  
-    pPars->fVerbose = 0;        // disable verbose output
     // decide what should be computed
     if ( fProbOne )
     {
@@ -666,7 +666,94 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
     return vResult;
 }
 
-  ////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    [Computes probability of switching (or of being 1).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_ManEvaluateSwitching( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    float SwitchTotal = 0.0;
+    int i;
+    assert( p->pSwitching );
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachObj( p, pObj, i )
+        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
+    return SwitchTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes probability of switching (or of being 1).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+    Gia_Man_t * pDfs;
+    Gia_Obj_t * pObj, * pObjDfs;
+    Vec_Int_t * vSwitching;
+    float * pSwitching, Switch, SwitchTotal = 0.0, SwitchTotal2 = 0.0;
+    int i;
+    Gia_ParSwi_t Pars, * pPars = &Pars;
+    ABC_FREE( p->pSwitching );
+    // set the default parameters
+    Gia_ManSetDefaultParamsSwi( pPars ); 
+    // override some of the defaults
+    pPars->nIters   = nFrames;  // set number of total timeframes
+    pPars->nPref    = nPref;    // set number of first timeframes to skip  
+    // decide what should be computed
+    if ( fProbOne )
+    {
+        // if the user asked to compute propability of 1, we do not need transition information
+        pPars->fProbOne   = 1;  // enable computing probabiblity of being one
+        pPars->fProbTrans = 0;  // disable computing transition probability 
+    }
+    else
+    {
+        // if the user asked for transition propabability, we do not need to compute probability of 1
+        pPars->fProbOne   = 0;  // disable computing probabiblity of being one
+        pPars->fProbTrans = 1;  // enable computing transition probability 
+    }
+    // derives the DFS ordered AIG
+    Gia_ManCreateRefs( p );
+//    pDfs = Gia_ManDupOrderDfs( p );
+    pDfs = Gia_ManDup( p );
+    assert( Gia_ManObjNum(pDfs) == Gia_ManObjNum(p) );
+    // perform the computation of switching activity
+    vSwitching = Gia_ManSwiSimulate( pDfs, pPars );
+    // transfer the computed result to the original AIG
+    p->pSwitching = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) );
+    pSwitching = (float *)vSwitching->pArray;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObjDfs = Gia_ObjFromLit( pDfs, pObj->Value );
+        Switch = pSwitching[ Gia_ObjId(pDfs, pObjDfs) ];
+        p->pSwitching[i] = (char)((Switch >= 1.0) ? 255 : (int)((0.002 + Switch) * 255)); // 0.00196 = (1/255)/2
+        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
+//        SwitchTotal2 += Gia_ObjRefs(p, pObj) * Switch;
+//        printf( "%d = %.2f\n", i, Gia_ObjRefs(p, pObj) * Switch );
+    }
+//    printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal );
+    Vec_IntFree( vSwitching );
+    Gia_ManStop( pDfs );
+    return SwitchTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index d5ff628a..055d7580 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
     src/aig/gia/giaCof.c \
+    src/aig/gia/giaCSat.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
     src/aig/gia/giaEmbed.c \
@@ -15,6 +16,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMap.c \
+    src/aig/gia/giaPat.c \
     src/aig/gia/giaRetime.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaSim.c \