Version abc90215

14 files changed, 2142 insertions, 1813 deletions

diff --git a/src/aig/cec/cec.c b/src/aig/cec/cec.c
new file mode 100644
index 00000000..a017f831
--- /dev/null
+++ b/src/aig/cec/cec.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [cec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index fb0bb830..fa7c5dbc 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -21,10 +21,6 @@
 #ifndef __CEC_H__
 #define __CEC_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,8 +44,8 @@ struct Cec_ParSat_t_
     int              nBTLimit;      // conflict limit at a node
     int              nSatVarMax;    // the max number of SAT variables
     int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              fPolarFlip;    // flops polarity of variables
     int              fFirstStop;    // stop on the first sat output
-    int              fPolarFlip;    // uses polarity adjustment
     int              fVerbose;      // verbose stats
 };
 
@@ -55,8 +55,15 @@ struct Cec_ParCsw_t_
 {
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
-    int              nBTlimit;      // conflict limit at a node
+    int              nItersMax;     // the maximum number of iterations of SAT sweeping
+    int              nBTLimit;      // conflict limit at a node
+    int              nSatVarMax;    // the max number of SAT variables
+    int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              nLevelMax;     // restriction on the level nodes to be swept
+    int              nDepthMax;     // the depth in terms of steps of speculative reduction
     int              fRewriting;    // enables AIG rewriting
+    int              fFirstStop;    // stop on the first sat output
+    int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
 
@@ -86,7 +93,8 @@ struct Cec_ParCec_t_
 extern void          Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
 extern void          Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
-extern int           Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p );
+extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars );
+extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cec/cecAig.c b/src/aig/cec/cecAig.c
deleted file mode 100644
index 2a6f5683..00000000
--- a/src/aig/cec/cecAig.c
+++ /dev/null
@@ -1,151 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecAig.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinatinoal equivalence checking.]
-
-  Synopsis    [AIG manipulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives combinational miter of the two AIGs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Cec_DeriveMiter_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
-    if ( pObj->pData )
-        return pObj->pData;
-    Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );
-    if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
-    Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) );
-    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    Aig_Regular(pObj->pData)->pHaig = pObj->pHaig;
-    return pObj->pData;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives combinational miter of the two AIGs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
-{
-    Bar_Progress_t * pProgress = NULL;
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj0, * pObj1, * pObjNew;
-    int i;
-    assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
-    assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManNodeNum(p0) + Aig_ManNodeNum(p1) );
-    pNew->pName = Aig_UtilStrsav( p0->pName );
-    // create the PIs
-    Aig_ManCleanData( p0 );
-    Aig_ManCleanData( p1 );
-    Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p0, pObj0, i )
-    {
-        pObjNew = Aig_ObjCreatePi( pNew );
-        pObj0->pData = pObjNew;
-        Aig_ManPi(p1, i)->pData = pObjNew;
-    }
-    // add logic for the POs
-    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p0) );
-    Aig_ManForEachPo( p0, pObj0, i )
-    {
-        Bar_ProgressUpdate( pProgress, i, "Miter..." );
-        pObj1 = Aig_ManPo( p1, i );
-        Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj0) );        
-        Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj1) );  
-        pObjNew = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild0Copy(pObj1) );
-        Aig_ObjCreatePo( pNew, pObjNew );
-    }
-    Bar_ProgressStop( pProgress );
-    Aig_ManCleanup( pNew );
-    Aig_ManSetRegNum( pNew, 0 );
-    // check the resulting network
-//    if ( !Aig_ManCheck(pNew) )
-//        printf( "Cec_DeriveMiter(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates AIG in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Cec_Duplicate( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManNodeNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
-    // add logic for the POs
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );        
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-    }
-    Aig_ManCleanup( pNew );
-    Aig_ManSetRegNum( pNew, 0 );
-    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-    // check the resulting network
-//    if ( !Aig_ManCheck(pNew) )
-//        printf( "Cec_DeriveMiter(): The check has failed.\n" );
-    return pNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index f3f6bf11..65fa2e9b 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -24,12 +24,69 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int        Cec_ObjRepr( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iRepr;               }
+static inline void       Cec_ObjSetRepr( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iRepr = Num;                }
+
+static inline int        Cec_ObjProved( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iProved;             }
+static inline void       Cec_ObjSetProved( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iProved = 1;                }
+
+static inline int        Cec_ObjFailed( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iFailed;             }
+static inline void       Cec_ObjSetFailed( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iFailed = 1;                }
+
+static inline int        Cec_ObjNext( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iNext;               }
+static inline void       Cec_ObjSetNext( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iNext = Num;                }
+
+static inline unsigned   Cec_ObjSim( Cec_ManCsw_t * p, int Id )                { return p->pObjs[Id].SimNum;              }
+static inline unsigned * Cec_ObjSimP1( Cec_ManCsw_t * p, int Id )              { return &p->pObjs[Id].SimNum;             }
+static inline unsigned * Cec_ObjSimP( Cec_ManCsw_t * p, int Id )               { return p->pMems + Cec_ObjSim(p, Id) + 1; }
+static inline void       Cec_ObjSetSim( Cec_ManCsw_t * p, int Id, unsigned n ) { p->pObjs[Id].SimNum = n;                 }
+
+static inline int        Cec_ObjIsConst( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) == 0;                           }
+static inline int        Cec_ObjIsHead( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) > 0;  }
+static inline int        Cec_ObjIsNone( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) == 0; }
+static inline int        Cec_ObjIsTail( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) > 0 && Cec_ObjNext(p, Id) == 0; }
+static inline int        Cec_ObjIsClass( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) > 0 || Cec_ObjNext(p, Id) > 0;  }
+
+#define Cec_ManForEachObj( p, i )                              \
+    for ( i = 0; i < Gia_ManObjNum(p->pAig); i++ )
+#define Cec_ManForEachObj1( p, i )                             \
+    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
+#define Cec_ManForEachClass( p, i )                            \
+    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) if ( !Cec_ObjIsHead(p, i) ) {} else
+#define Cec_ClassForEachObj( p, i, iObj )                      \
+    for ( assert(Cec_ObjIsHead(p, i)), iObj = i; iObj; iObj = Cec_ObjNext(p, iObj) )
+#define Cec_ClassForEachObj1( p, i, iObj )                     \
+    for ( assert(Cec_ObjIsHead(p, i)), iObj = Cec_ObjNext(p, i); iObj; iObj = Cec_ObjNext(p, iObj) )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the set of representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
+{
+    int i, * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
+    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
+        if ( Cec_ObjProved(p, i) )
+        {
+            assert( Cec_ObjRepr(p, i) >= 0 );
+            pReprs[i] = Cec_ObjRepr(p, i);
+        }
+    return pReprs;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,42 +96,50 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p )
+Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p )
 {
-    Aig_Man_t * pAig;
-    Aig_Obj_t ** pCopy;
-    Aig_Obj_t * pMiter, * pRes0, * pRes1, * pRepr;
-    int i;
-    pCopy = ALLOC( Aig_Obj_t *, p->nObjs );
-    pCopy[0] = NULL;
-    pAig = Aig_ManStart( p->nNodes );
-    for ( i = 1; i < p->nObjs; i++ )
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int iRes0, iRes1, iRepr, iNode;
+    int i, fCompl, * piCopies;
+    Vec_IntClear( p->vXorNodes );
+    Gia_ManLevelNum( p->pAig );
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
+    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+    Gia_ManHashAlloc( pNew );
+    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
+    piCopies[0] = 0;
+    Gia_ManForEachObj1( p->pAig, pObj, i )
     {
-        if ( p->pFans0[i] == 0 ) // pi always has zero first fanin
+        if ( Gia_ObjIsCi(pObj) ) 
         {
-            pCopy[i] = Aig_ObjCreatePi( pAig );
+            piCopies[i] = Gia_ManAppendCi( pNew );
             continue;
         }
-        if ( p->pFans1[i] == 0 ) // po always has non-zero 1st fanin and zero 2nd fanin
+        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
+        if ( Gia_ObjIsCo(pObj) ) 
+        {
+            Gia_ManAppendCo( pNew, iRes0 );
             continue;
-        pRes0 = pCopy[ Cec_Lit2Var(p->pFans0[i]) ];
-        pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->pFans0[i]) );
-        pRes1 = pCopy[ Cec_Lit2Var(p->pFans1[i]) ];
-        pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->pFans1[i]) );
-        pCopy[i] = Aig_And( pAig, pRes0, pRes1 );
-        if ( p->pReprs[i] < 0 )
+        }
+        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
+        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
             continue;
-        assert( p->pReprs[i] < i );
-        pRepr = p->pReprs[i]? pCopy[ p->pReprs[i] ] : Aig_ManConst1(pAig);
-        if ( Aig_Regular(pCopy[i]) == Aig_Regular(pRepr) )
+        assert( Cec_ObjRepr(p, i) < i );
+        iRepr = piCopies[Cec_ObjRepr(p, i)];
+        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
             continue;
-        pMiter = Aig_Exor( pAig, pCopy[i], pRepr );
-        Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
+        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
+        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
     }
-    free( pCopy );
-    Aig_ManSetRegNum( pAig, 0 );
-    Aig_ManCleanup( pAig );
-    return pAig;
+    ABC_FREE( piCopies );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -88,16 +153,70 @@ Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Caig_ManCountOne( Caig_Man_t * p, int i )
+Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p )
 {
-    int Ent, nLits = 0;
-    assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 );
-    for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] )
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int iRes0, iRes1, iRepr, iNode, iMiter;
+    int i, fCompl, * piCopies, * pDepths;
+    Vec_IntClear( p->vXorNodes );
+//    Gia_ManLevelNum( p->pAig );
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
+    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+    Gia_ManHashAlloc( pNew );
+    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
+    pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+    piCopies[0] = 0;
+    Gia_ManForEachObj1( p->pAig, pObj, i )
     {
-        assert( p->pReprs[Ent] == i );
-        nLits++;
+        if ( Gia_ObjIsCi(pObj) ) 
+        {
+            piCopies[i] = Gia_ManAppendCi( pNew );
+            continue;
+        }
+        if ( Gia_ObjIsCo(pObj) ) 
+            continue;
+        if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
+             piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
+             continue;
+        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
+        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
+        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+        pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
+        if ( Cec_ObjRepr(p, i) < 0 || Cec_ObjFailed(p, i) )
+            continue;
+        assert( Cec_ObjRepr(p, i) < i );
+        iRepr = piCopies[Cec_ObjRepr(p, i)];
+        if ( iRepr == -1 )
+            continue;
+        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
+            continue;
+        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
+        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
+        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
+        if ( Cec_ObjProved(p, i) )
+            continue;
+//        if ( p->pPars->nLevelMax && 
+//            (Gia_ObjLevel(p->pAig, pObj)  > p->pPars->nLevelMax || 
+//             Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
+//            continue;
+        // produce speculative miter
+        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
+        Gia_ManAppendCo( pNew, iMiter );
+        Vec_IntPush( p->vXorNodes, Cec_ObjRepr(p, i) );
+        Vec_IntPush( p->vXorNodes, i );
+        // add to the depth of this node
+        pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Cec_ObjRepr(p, i)] );
+        if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
+            piCopies[i] = -1;
     }
-    return 1 + nLits;
+    ABC_FREE( piCopies );
+    ABC_FREE( pDepths );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -109,15 +228,52 @@ int Caig_ManCountOne( Caig_Man_t * p, int i )
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
-int Caig_ManCountLiterals( Caig_Man_t * p )
+Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p )
 {
-    int i, nLits = 0;
-    for ( i = 1; i < p->nObjs; i++ )
-        if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
-            nLits += Caig_ManCountOne(p, i) - 1;
-    return nLits;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int iRes0, iRes1, iRepr, iNode, iMiter;
+    int i, fCompl, * piCopies;
+    Vec_IntClear( p->vXorNodes );
+    Gia_ManLevelNum( p->pAig );
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
+    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+    Gia_ManHashAlloc( pNew );
+    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
+    piCopies[0] = 0;
+    Gia_ManForEachObj1( p->pAig, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) ) 
+        {
+            piCopies[i] = Gia_ManAppendCi( pNew );
+            continue;
+        }
+        if ( Gia_ObjIsCo(pObj) ) 
+            continue;
+        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
+        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
+        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
+            continue;
+        assert( Cec_ObjRepr(p, i) < i );
+        iRepr = piCopies[Cec_ObjRepr(p, i)];
+        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
+            continue;
+        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
+        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
+        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
+        // add speculative miter
+        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
+        Gia_ManAppendCo( pNew, iMiter );
+    }
+    ABC_FREE( piCopies );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -131,13 +287,15 @@ int Caig_ManCountLiterals( Caig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter )
+int Cec_ManCswCountOne( Cec_ManCsw_t * p, int i )
 {
-    int Ent;
-    printf( "Class %4d :  Num = %2d  {", Counter, Caig_ManCountOne(p, i) );
-    for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
-        printf(" %d", Ent );
-    printf( " }\n" );
+    int Ent, nLits = 1;
+    Cec_ClassForEachObj1( p, i, Ent )
+    {
+        assert( Cec_ObjRepr(p, Ent) == i );
+        nLits++;
+    }
+    return nLits;
 }
 
 /**Function*************************************************************
@@ -151,25 +309,12 @@ void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose )
+int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p )
 {
-    int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
-    for ( i = 1; i < p->nObjs; i++ )
-    {
-        if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
-            Counter++;
-        if ( p->pReprs[i] == 0 )
-            Counter1++;
-        if ( p->pReprs[i] < 0 && p->pNexts[i] == 0 )
-            CounterX++;
-    }
-    nLits = Caig_ManCountLiterals( p );
-    printf( "Class = %6d. Const1 = %6d. Other = %6d. Lits = %7d. Total = %7d.\n", 
-        Counter, Counter1, CounterX, nLits, nLits+Counter1 );
-    if ( fVerbose )
-    for ( i = 1; i < p->nObjs; i++ )
-        if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
-            Caig_ManPrintOne( p, i, ++Counter );
+    int i, nLits = 0;
+    Cec_ManForEachObj( p, i )
+        nLits += (Cec_ObjRepr(p, i) >= 0);
+    return nLits;
 }
 
 /**Function*************************************************************
@@ -183,12 +328,13 @@ void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i )
+void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
 {
     int Ent;
-    Vec_PtrClear( p->vSims );
-    for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
-        Vec_PtrPush( p->vSims, p->pSims + Ent );
+    printf( "Class %4d :  Num = %2d  {", Counter, Cec_ManCswCountOne(p, i) );
+    Cec_ClassForEachObj( p, i, Ent )
+        printf(" %d", Ent );
+    printf( " }\n" );
 }
 
 /**Function*************************************************************
@@ -202,15 +348,26 @@ void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i )
+void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
 {
-    unsigned * pSim;
-    int Ent;
-    Vec_PtrClear( p->vSims );
-    for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
+    int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
+    Cec_ManForEachObj1( p, i )
+    {
+        if ( Cec_ObjIsHead(p, i) )
+            Counter++;
+        else if ( Cec_ObjIsConst(p, i) )
+            Counter1++;
+        else if ( Cec_ObjIsNone(p, i) )
+            CounterX++;
+    }
+    nLits = Cec_ManCswCountLitsAll( p );
+    printf( "Class =%7d. Const =%7d. Unsed =%7d. Lits =%8d. All =%8d. Mem = %5.2f Mb\n", 
+        Counter, Counter1, CounterX, nLits-Counter1, nLits, 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20) );
+    if ( fVerbose )
     {
-        pSim = Caig_ManSimDeref( p, Ent );
-        Vec_PtrPush( p->vSims, pSim + 1 );
+        Counter = 0;
+        Cec_ManForEachClass( p, i )
+            Cec_ManCswPrintOne( p, i, ++Counter );
     }
 }
 
@@ -225,7 +382,7 @@ void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords )
+int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords )
 {
     int w;
     if ( (p0[0] & 1) == (p1[0] & 1) )
@@ -255,7 +412,7 @@ int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-int Caig_ManCompareConst( unsigned * p, int nWords )
+int Cec_ManCswCompareConst( unsigned * p, int nWords )
 {
     int w;
     if ( p[0] & 1 )
@@ -285,26 +442,26 @@ int Caig_ManCompareConst( unsigned * p, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass )
+void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
 {
-    int * pNext, Repr, Ent, i;
+    int Repr = -1, EntPrev = -1, Ent, i;
     assert( Vec_IntSize(vClass) > 0 );
     Vec_IntForEachEntry( vClass, Ent, i )
     {
         if ( i == 0 )
         {
             Repr = Ent;
-            p->pReprs[Ent] = -1;
-            pNext = p->pNexts + Ent;
+            Cec_ObjSetRepr( p, Ent, -1 );
+            EntPrev = Ent;
         }
         else
         {
-            p->pReprs[Ent] = Repr;
-            *pNext = Ent;
-            pNext = p->pNexts + Ent;
+            Cec_ObjSetRepr( p, Ent, Repr );
+            Cec_ObjSetNext( p, EntPrev, Ent );
+            EntPrev = Ent;
         }
     }
-    *pNext = 0;
+    Cec_ObjSetNext( p, EntPrev, 0 );
 }
 
 /**Function*************************************************************
@@ -318,32 +475,28 @@ void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims )
+int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
 {
     unsigned * pSim0, * pSim1;
-    int Ent, c = 0, d = 0;
+    int Ent;
     Vec_IntClear( p->vClassOld );
     Vec_IntClear( p->vClassNew );
-    pSim0 = Vec_PtrEntry( vSims, c++ );
     Vec_IntPush( p->vClassOld, i );
-    for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] )
+    pSim0 = fFirst? Cec_ObjSimP1(p, i) : Cec_ObjSimP(p, i);
+    Cec_ClassForEachObj1( p, i, Ent )
     {
-        pSim1 = Vec_PtrEntry( vSims, c++ );
-        if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) )
+        pSim1 = fFirst? Cec_ObjSimP1(p, Ent) : Cec_ObjSimP(p, Ent);
+        if ( Cec_ManCswCompareEqual( pSim0, pSim1, p->nWords ) )
             Vec_IntPush( p->vClassOld, Ent );
         else
-        {
             Vec_IntPush( p->vClassNew, Ent );
-            Vec_PtrWriteEntry( vSims, d++, pSim1 );
-        }
     }
-    Vec_PtrShrink( vSims, d );
-    if ( Vec_IntSize(p->vClassNew) == 0 )
+    if ( Vec_IntSize( p->vClassNew ) == 0 )
         return 0;
-    Caig_ManClassCreate( p, p->vClassOld );
-    Caig_ManClassCreate( p, p->vClassNew );
+    Cec_ManCswClassCreate( p, p->vClassOld );
+    Cec_ManCswClassCreate( p, p->vClassNew );
     if ( Vec_IntSize(p->vClassNew) > 1 )
-        return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims );
+        return 1 + Cec_ManCswClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), fFirst );
     return 1;
 }
 
@@ -358,7 +511,7 @@ int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims )
   SeeAlso     []
 
 ***********************************************************************/
-int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
+int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
 {
     static int s_Primes[16] = { 
         1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
@@ -386,49 +539,51 @@ int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManClassesCreate( Caig_Man_t * p )
+void Cec_ManCswClassesCreate( Cec_ManCsw_t * p )
 {
     int * pTable, nTableSize, i, Key;
-    nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 );
-    pTable = CALLOC( int, nTableSize );
-    p->pReprs = ALLOC( int, p->nObjs );
-    p->pNexts = CALLOC( int, p->nObjs );
-    for ( i = 1; i < p->nObjs; i++ )
+    p->nWords = 1;
+    nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p->pAig) / 10 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    Cec_ObjSetRepr( p, 0, -1 );
+    Cec_ManForEachObj1( p, i )
     {
-        if ( Caig_ManCompareConst( p->pSims + i, 1 ) )
+        if ( Gia_ObjIsCo(Gia_ManObj(p->pAig, i)) ) 
+        {
+            Cec_ObjSetRepr( p, i, -1 );
+            continue;
+        }
+        if ( Cec_ManCswCompareConst( Cec_ObjSimP1(p, i), p->nWords ) )
         {
-            p->pReprs[i] = 0;
+            Cec_ObjSetRepr( p, i, 0 );
             continue;
         }
-        Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize );
+        Key = Cec_ManCswHashKey( Cec_ObjSimP1(p, i), p->nWords, nTableSize );
         if ( pTable[Key] == 0 )
-            p->pReprs[i] = -1;
+            Cec_ObjSetRepr( p, i, -1 );
         else
         {
-            p->pNexts[ pTable[Key] ] = i;
-            p->pReprs[i] = p->pReprs[ pTable[Key] ];
-            if ( p->pReprs[i] == -1 )
-                p->pReprs[i] = pTable[Key];
+            Cec_ObjSetNext( p, pTable[Key], i );
+            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
+            if ( Cec_ObjRepr(p, i) == -1 )
+                Cec_ObjSetRepr( p, i, pTable[Key] );
         }
         pTable[Key] = i;
     }
-    FREE( pTable );
-Caig_ManPrintClasses( p, 0 );
+    ABC_FREE( pTable );
+    if ( p->pPars->fVeryVerbose )
+    Cec_ManCswPrintClasses( p, 0 );
     // refine classes
-    p->vSims     = Vec_PtrAlloc( 100 );
-    p->vClassOld = Vec_IntAlloc( 100 );
-    p->vClassNew = Vec_IntAlloc( 100 );
-    for ( i = 1; i < p->nObjs; i++ )
-        if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
-        {
-            Caig_ManCollectSimsSimple( p, i );
-            Caig_ManClassRefineOne( p, i, p->vSims );
-        }
+    Cec_ManForEachClass( p, i )
+        Cec_ManCswClassRefineOne( p, i, 1 );
     // clean memory
-    memset( p->pSims, 0, sizeof(unsigned) * p->nObjs );
-Caig_ManPrintClasses( p, 0 );
+    Cec_ManForEachObj( p, i )
+        Cec_ObjSetSim( p, i, 0 );
+    if ( p->pPars->fVeryVerbose )
+    Cec_ManCswPrintClasses( p, 0 );
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -440,27 +595,87 @@ Caig_ManPrintClasses( p, 0 );
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManSimulateSimple( Caig_Man_t * p )
+void Cec_ManCswSimulateSimple( Cec_ManCsw_t * p )
 {
+    Gia_Obj_t * pObj;
     unsigned Res0, Res1;
     int i;
-    for ( i = 1; i < p->nObjs; i++ )
+    Gia_ManForEachCi( p->pAig, pObj, i )
+        Cec_ObjSetSim( p, i, Aig_ManRandom(0) );
+    Gia_ManForEachAnd( p->pAig, pObj, i )
+    {
+        Res0 = Cec_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
+        Res1 = Cec_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
+        Cec_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
+                             (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
+{
+    unsigned * pPlace, Ent;
+    pPlace = &p->MemFree;
+    for ( Ent = p->nMems * (p->nWords + 1); 
+          Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; 
+          Ent += p->nWords + 1 )
+    {
+        *pPlace = Ent;
+        pPlace = p->pMems + Ent;
+    }
+    *pPlace = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
+{
+    unsigned * pSim;
+    assert( p->pObjs[i].SimNum == 0 );
+    if ( p->MemFree == 0 )
     {
-        if ( p->pFans0[i] == 0 ) // pi
+        if ( p->nWordsAlloc == 0 )
         {
-            p->pSims[i] = Aig_ManRandom( 0 );
-            continue;
+            assert( p->pMems == NULL );
+            p->nWordsAlloc = (1<<17); // -> 1Mb
+            p->nMems = 1;
         }
-        Res0 = p->pSims[Cec_Lit2Var(p->pFans0[i])];
-        Res1 = p->pSims[Cec_Lit2Var(p->pFans1[i])];
-        p->pSims[i] = (Cec_LitIsCompl(p->pFans0[i]) ? ~Res0: Res0) &
-                      (Cec_LitIsCompl(p->pFans1[i]) ? ~Res1: Res1);
+        p->nWordsAlloc *= 2;
+        p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
+        Cec_ManCswSimMemRelink( p );
     }
+    p->pObjs[i].SimNum = p->MemFree;
+    pSim = p->pMems + p->MemFree;
+    p->MemFree = pSim[0];
+    pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
+    p->nMems++;
+    if ( p->nMemsMax < p->nMems )
+        p->nMemsMax = p->nMems;
+    return pSim;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Dereference simulaton info.]
 
   Description []
                
@@ -469,10 +684,19 @@ void Caig_ManSimulateSimple( Caig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManProcessClass( Caig_Man_t * p, int i )
+unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
 {
-    Caig_ManCollectSimsNormal( p, i );
-    Caig_ManClassRefineOne( p, i, p->vSims );
+    unsigned * pSim;
+    assert( p->pObjs[i].SimNum > 0 );
+    pSim = p->pMems + p->pObjs[i].SimNum;
+    if ( --pSim[0] == 0 )
+    {
+        pSim[0] = p->MemFree;
+        p->MemFree = p->pObjs[i].SimNum;
+        p->pObjs[i].SimNum = 0;
+        p->nMems--;
+    }
+    return pSim;
 }
 
 /**Function*************************************************************
@@ -486,51 +710,179 @@ void Caig_ManProcessClass( Caig_Man_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined )
+void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
 {
-    Vec_Int_t * vClasses;
-    int * pTable, nTableSize, i, Key, iNode;
     unsigned * pSim;
+    int * pTable, nTableSize, i, k, Key;
     if ( Vec_IntSize(vRefined) == 0 )
         return;
     nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
-    pTable = CALLOC( int, nTableSize );
-    vClasses = Vec_IntAlloc( 100 );
-    Vec_IntForEachEntry( vRefined, iNode, i )
+    pTable = ABC_CALLOC( int, nTableSize );
+    Vec_IntForEachEntry( vRefined, i, k )
     {
-        pSim = Caig_ManSimRead( p, iNode );
-        assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) );
-        Key = Caig_ManHashKey( pSim + 1, p->nWords, nTableSize );
+        if ( i == 7720 )
+        {
+            int s = 0;
+        }
+        pSim = Cec_ObjSimP( p, i );
+        assert( !Cec_ManCswCompareConst( pSim, p->nWords ) );
+        Key = Cec_ManCswHashKey( pSim, p->nWords, nTableSize );
         if ( pTable[Key] == 0 )
         {
-            assert( p->pReprs[iNode] == 0 );
-            assert( p->pNexts[iNode] == 0 );
-            p->pReprs[iNode] = -1;
-            Vec_IntPush( vClasses, iNode );
+            assert( Cec_ObjRepr(p, i) == 0 );
+            assert( Cec_ObjNext(p, i) == 0 );
+            Cec_ObjSetRepr( p, i, -1 );
         }
         else
         {
-            p->pNexts[ pTable[Key] ] = iNode;
-            p->pReprs[iNode] = p->pReprs[ pTable[Key] ];
-            if ( p->pReprs[iNode] == -1 )
-                p->pReprs[iNode] = pTable[Key];
-            assert( p->pReprs[iNode] > 0 );
+            Cec_ObjSetNext( p, pTable[Key], i );
+            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
+            if ( Cec_ObjRepr(p, i) == -1 )
+                Cec_ObjSetRepr( p, i, pTable[Key] );
+            assert( Cec_ObjRepr(p, i) > 0 );
         }
-        pTable[Key] = iNode;
+        pTable[Key] = i;
     }
-    FREE( pTable );
-    // refine classes
-    Vec_IntForEachEntry( vClasses, iNode, i )
+    Vec_IntForEachEntry( vRefined, i, k )
     {
-        if ( p->pNexts[iNode] == 0 )
+        if ( Cec_ObjIsHead( p, i ) )
+            Cec_ManCswClassRefineOne( p, i, 0 );
+    }
+    Vec_IntForEachEntry( vRefined, i, k )
+        Cec_ManCswSimDeref( p, i );
+    ABC_FREE( pTable );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one round.]
+
+  Description [Returns the number of PO entry if failed; 0 otherwise.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, int iSeries, int fRandomize )
+{
+    static int nCountRand = 0;
+    Gia_Obj_t * pObj;
+    unsigned * pRes0, * pRes1, * pRes;
+    int i, k, w, Ent, iCiId = 0, iCoId = 0;
+    p->nMemsMax = 0;
+    Vec_IntClear( p->vRefinedC );
+    if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
+    {
+        pRes = Cec_ManCswSimRef( p, 0 );
+        for ( w = 1; w <= p->nWords; w++ )
+            pRes[w] = 0;
+    }
+    Gia_ManForEachObj1( p->pAig, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) ) 
+        {
+            if ( Gia_ObjValue(pObj) == 0 )
+            {
+                iCiId++;
+                continue;
+            }
+            pRes = Cec_ManCswSimRef( p, i );
+            if ( vInfoCis ) 
+            {
+                pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
+                for ( w = 1; w <= p->nWords; w++ )
+                {
+                    pRes[w] = pRes0[iSeries*p->nWords+w-1];
+                    if ( fRandomize )
+                        pRes[w] ^= (1 << (nCountRand++ & 0x1f));
+                }
+            }
+            else
+            {
+                for ( w = 1; w <= p->nWords; w++ )
+                    pRes[w] = Aig_ManRandom( 0 );
+            }
+            // make sure the first pattern is always zero
+            pRes[1] ^= (pRes[1] & 1);
+            goto references;
+        }
+        if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
         {
-            Caig_ManSimDeref( p, iNode );
+            pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+            if ( vInfoCos )
+            {
+                pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
+                if ( Gia_ObjFaninC0(pObj) )
+                    for ( w = 1; w <= p->nWords; w++ )
+                        pRes[w-1] = ~pRes0[w];
+                else 
+                    for ( w = 1; w <= p->nWords; w++ )
+                        pRes[w-1] = pRes0[w];
+            }
             continue;
         }
-        Caig_ManCollectSimsNormal( p, iNode );
-        Caig_ManClassRefineOne( p, iNode, p->vSims );
+        assert( Gia_ObjValue(pObj) );
+        pRes  = Cec_ManCswSimRef( p, i );
+        pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+        pRes1 = Cec_ManCswSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+        if ( Gia_ObjFaninC0(pObj) )
+        {
+            if ( Gia_ObjFaninC1(pObj) )
+                for ( w = 1; w <= p->nWords; w++ )
+                    pRes[w] = ~(pRes0[w] | pRes1[w]);
+            else
+                for ( w = 1; w <= p->nWords; w++ )
+                    pRes[w] = ~pRes0[w] & pRes1[w];
+        }
+        else
+        {
+            if ( Gia_ObjFaninC1(pObj) )
+                for ( w = 1; w <= p->nWords; w++ )
+                    pRes[w] = pRes0[w] & ~pRes1[w];
+            else
+                for ( w = 1; w <= p->nWords; w++ )
+                    pRes[w] = pRes0[w] & pRes1[w];
+        }
+references:
+        // if this node is candidate constant, collect it
+        if ( Cec_ObjIsConst(p, i) && !Cec_ManCswCompareConst(pRes + 1, p->nWords) )
+        {
+            pRes[0]++;
+            Vec_IntPush( p->vRefinedC, i );
+        }
+        // if the node belongs to a class, save it
+        if ( Cec_ObjIsClass(p, i) )
+            pRes[0]++;
+        // if this is the last node of the class, process it
+        if ( Cec_ObjIsTail(p, i) )
+        {
+            Vec_IntClear( p->vClassTemp );
+            Cec_ClassForEachObj( p, Cec_ObjRepr(p, i), Ent )
+                Vec_IntPush( p->vClassTemp, Ent );
+            Cec_ManCswClassRefineOne( p, Cec_ObjRepr(p, i), 0 );
+            Vec_IntForEachEntry( p->vClassTemp, Ent, k )
+                Cec_ManCswSimDeref( p, Ent );
+        }
     }
-    Vec_IntFree( vClasses );
+    if ( Vec_IntSize(p->vRefinedC) > 0 )
+        Cec_ManCswProcessRefined( p, p->vRefinedC );
+    assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
+    assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
+    assert( p->nMems == 1 );
+    if ( p->pPars->fVeryVerbose )
+        Cec_ManCswPrintClasses( p, 0 );
+/*
+    if ( p->nMems > 1 )
+    {
+        for ( i = 1; i < p->nObjs; i++ )
+        if ( p->pSims[i] )
+        {
+            int x = 0;
+        }
+    }
+*/
 }
 
 /**Function*************************************************************
@@ -544,24 +896,153 @@ void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined )
   SeeAlso     []
 
 ***********************************************************************/
-Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters )
+int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
 {
-    Caig_Man_t * p;
     int i;
-    Aig_ManRandom( 1 );
-    p = Caig_ManCreate( pAig );
-    p->nWords = 1;
-    Caig_ManSimulateSimple( p );
-    Caig_ManClassesCreate( p );
-    p->nWords = nWords;
-    for ( i = 0; i < nIters; i++ )
+    Gia_ManSetRefs( p->pAig );
+    Cec_ManCswSimulateSimple( p );
+    Cec_ManCswClassesCreate( p );
+    for ( i = 0; i < p->pPars->nRounds; i++ )
+    {
+        p->nWords = i + 1;
+        Cec_ManCswSimMemRelink( p );
+        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
+    }
+    p->nWords = p->pPars->nWords;
+    Cec_ManCswSimMemRelink( p );
+    for ( i = 0; i < p->pPars->nRounds; i++ )
+        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
+{
+    int Result;
+    if ( pObj->fMark0 )
+        return 1;
+    if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
+        return 0;
+    Result = (Cec_ManCswClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
+              Cec_ManCswClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
+    return pObj->fMark0 = Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
+{
+    Vec_Ptr_t * vInfo;
+    Gia_Obj_t * pObj, * pObjOld, * pReprOld;
+    int i, k, iRepr, iNode;
+    vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), p->pPars->nWords );
+    if ( vInfo != NULL )
     {
-    Caig_ManSimulateRound( p, 0 );
-Caig_ManPrintClasses( p, 0 );
+        for ( i = 0; i < pPat->nSeries; i++ )
+            Cec_ManCswSimulateRound( p, vInfo, NULL, i, 0 );
+        Vec_PtrFree( vInfo );
     }
-    return p;
+    assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
+    // mark the transitive fanout of failed nodes
+    if ( p->pPars->nDepthMax != 1 )
+    {
+        Gia_ManCleanMark0( p->pAig );
+        Gia_ManCleanMark1( p->pAig );
+        Gia_ManForEachCo( pNew, pObj, k )
+        {
+            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
+                continue;
+//            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
+            Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
+        }
+        // mark the nodes reachable through the failed nodes
+        Gia_ManForEachAnd( p->pAig, pObjOld, k )
+            pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
+        // unmark the disproved nodes
+        Gia_ManForEachCo( pNew, pObj, k )
+        {
+            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
+                continue; 
+            pObjOld = Gia_ManObj(p->pAig, iNode);
+            assert( pObjOld->fMark0 == 1 );
+            if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
+                pObjOld->fMark1 = 1;
+        }
+        // clean marks
+        Gia_ManForEachAnd( p->pAig, pObjOld, k )
+            if ( pObjOld->fMark1 )
+            {
+                pObjOld->fMark0 = 0;
+                pObjOld->fMark1 = 0;
+            }
+    }
+    // set the results
+    Gia_ManForEachCo( pNew, pObj, k )
+    {
+        iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+        iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+        pReprOld = Gia_ManObj(p->pAig, iRepr);
+        pObjOld = Gia_ManObj(p->pAig, iNode);
+        if ( pObj->fMark1 )
+        { // proved
+            assert( pObj->fMark0 == 0 );
+            assert( !Cec_ObjProved(p, iNode) );
+            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
+//            if ( pObjOld->fMark0 == 0 )
+            {
+                assert( iRepr == Cec_ObjRepr(p, iNode) );
+                Cec_ObjSetProved( p, iNode );
+                p->nAllProved++;
+            }
+        }
+        else if ( pObj->fMark0 )
+        { // disproved
+            assert( pObj->fMark1 == 0 );
+            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
+//            if ( pObjOld->fMark0 == 0 )
+            {
+                if ( iRepr == Cec_ObjRepr(p, iNode) )
+                    printf( "Cec_ManCswClassesUpdate(): Error! Node is not refined!\n" );
+                p->nAllDisproved++;
+            }
+        }
+        else
+        { // failed
+            assert( pObj->fMark0 == 0 );
+            assert( pObj->fMark1 == 0 );
+            assert( !Cec_ObjFailed(p, iNode) );
+            assert( !Cec_ObjProved(p, iNode) );
+            Cec_ObjSetFailed( p, iNode );
+            p->nAllFailed++;
+        }
+    } 
+    return 0;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecCnf.c b/src/aig/cec/cecCnf.c
deleted file mode 100644
index 8b8c011d..00000000
--- a/src/aig/cec/cecCnf.c
+++ /dev/null
@@ -1,328 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecCnf.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinatinoal equivalence checking.]
-
-  Synopsis    [CNF computation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Addes clauses to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_AddClausesMux( Cec_ManSat_t * p, Aig_Obj_t * pNode )
-{
-    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
-    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
-
-    assert( !Aig_IsComplement( pNode ) );
-    assert( Aig_ObjIsMuxType( pNode ) );
-    // get nodes (I = if, T = then, E = else)
-    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
-    // get the variable numbers
-    VarF = Cec_ObjSatNum(p,pNode);
-    VarI = Cec_ObjSatNum(p,pNodeI);
-    VarT = Cec_ObjSatNum(p,Aig_Regular(pNodeT));
-    VarE = Cec_ObjSatNum(p,Aig_Regular(pNodeE));
-    // get the complementation flags
-    fCompT = Aig_IsComplement(pNodeT);
-    fCompE = Aig_IsComplement(pNodeE);
-
-    // f = ITE(i, t, e)
-
-    // i' + t' + f
-    // i' + t  + f'
-    // i  + e' + f
-    // i  + e  + f'
-
-    // create four clauses
-    pLits[0] = toLitCond(VarI, 1);
-    pLits[1] = toLitCond(VarT, 1^fCompT);
-    pLits[2] = toLitCond(VarF, 0);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 1);
-    pLits[1] = toLitCond(VarT, 0^fCompT);
-    pLits[2] = toLitCond(VarF, 1);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 0);
-    pLits[1] = toLitCond(VarE, 1^fCompE);
-    pLits[2] = toLitCond(VarF, 0);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 0);
-    pLits[1] = toLitCond(VarE, 0^fCompE);
-    pLits[2] = toLitCond(VarF, 1);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-
-    // two additional clauses
-    // t' & e' -> f'
-    // t  & e  -> f 
-
-    // t  + e   + f'
-    // t' + e'  + f 
-
-    if ( VarT == VarE )
-    {
-//        assert( fCompT == !fCompE );
-        return;
-    }
-
-    pLits[0] = toLitCond(VarT, 0^fCompT);
-    pLits[1] = toLitCond(VarE, 0^fCompE);
-    pLits[2] = toLitCond(VarF, 1);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarT, 1^fCompT);
-    pLits[1] = toLitCond(VarE, 1^fCompE);
-    pLits[2] = toLitCond(VarF, 0);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
-        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
-        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Addes clauses to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_AddClausesSuper( Cec_ManSat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
-{
-    Aig_Obj_t * pFanin;
-    int * pLits, nLits, RetValue, i;
-    assert( !Aig_IsComplement(pNode) );
-    assert( Aig_ObjIsNode( pNode ) );
-    // create storage for literals
-    nLits = Vec_PtrSize(vSuper) + 1;
-    pLits = ALLOC( int, nLits );
-    // suppose AND-gate is A & B = C
-    // add !A => !C   or   A + !C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        pLits[0] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
-        pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1);
-        if ( p->pPars->fPolarFlip )
-        {
-            if ( Aig_Regular(pFanin)->fPhase )  pLits[0] = lit_neg( pLits[0] );
-            if ( pNode->fPhase )                pLits[1] = lit_neg( pLits[1] );
-        }
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-    }
-    // add A & B => C   or   !A + !B + C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        pLits[i] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
-        if ( p->pPars->fPolarFlip )
-        {
-            if ( Aig_Regular(pFanin)->fPhase )  pLits[i] = lit_neg( pLits[i] );
-        }
-    }
-    pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0);
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNode->fPhase )  pLits[nLits-1] = lit_neg( pLits[nLits-1] );
-    }
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
-    assert( RetValue );
-    free( pLits );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
-{
-    // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || 
-         (!fFirst && Aig_ObjRefs(pObj) > 1) || 
-         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
-    {
-        Vec_PtrPushUnique( vSuper, pObj );
-        return;
-    }
-    // go through the branches
-    Cec_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
-    Cec_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
-{
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
-    Vec_PtrClear( vSuper );
-    Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the solver clause database.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Cec_ObjSatNum(p,pObj) )
-        return;
-    assert( Cec_ObjSatNum(p,pObj) == 0 );
-    if ( Aig_ObjIsConst1(pObj) )
-        return;
-    Vec_PtrPush( p->vUsedNodes, pObj );
-    Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
-    if ( Aig_ObjIsNode(pObj) )
-        Vec_PtrPush( vFrontier, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the solver clause database.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj )
-{ 
-    Vec_Ptr_t * vFrontier;
-    Aig_Obj_t * pNode, * pFanin;
-    int i, k, fUseMuxes = 1;
-    // quit if CNF is ready
-    if ( Cec_ObjSatNum(p,pObj) )
-        return;
-    // start the frontier
-    vFrontier = Vec_PtrAlloc( 100 );
-    Cec_ObjAddToFrontier( p, pObj, vFrontier );
-    // explore nodes in the frontier
-    Vec_PtrForEachEntry( vFrontier, pNode, i )
-    {
-        // create the supergate
-        assert( Cec_ObjSatNum(p,pNode) );
-        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
-        {
-            Vec_PtrClear( p->vFanins );
-            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
-            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
-            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
-                Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
-            Cec_AddClausesMux( p, pNode );
-        }
-        else
-        {
-            Cec_CollectSuper( pNode, fUseMuxes, p->vFanins );
-            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
-                Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
-            Cec_AddClausesSuper( p, pNode, p->vFanins );
-        }
-        assert( Vec_PtrSize(p->vFanins) > 1 );
-    }
-    Vec_PtrFree( vFrontier );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 86287a96..ab8fd5cf 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -37,20 +37,20 @@
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSat_t) );
-    p->nBTLimit       =   100;  // conflict limit at a node
-    p->nSatVarMax     =  2000;  // the max number of SAT variables
-    p->nCallsRecycle  =    10;  // calls to perform before recycling SAT solver
-    p->fFirstStop     =     0;  // stop on the first sat output
-    p->fPolarFlip     =     0;  // uses polarity adjustment
-    p->fVerbose       =     0;  // verbose stats
-}
-
-/**Function*************************************************************
+    p->nBTLimit       =      10;  // conflict limit at a node
+    p->nSatVarMax     =    2000;  // the max number of SAT variables
+    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    p->fPolarFlip     =       1;  // flops polarity of variables
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVerbose       =       1;  // verbose stats
+}  
+  
+/**Function************  *************************************************
 
   Synopsis    [This procedure sets default parameters.]
 
@@ -64,12 +64,19 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
 {
     memset( p, 0, sizeof(Cec_ParCsw_t) );
-    p->nWords         =    15;  // the number of simulation words
-    p->nRounds        =    10;  // the number of simulation rounds
-    p->nBTlimit       =    10;  // conflict limit at a node
-    p->fRewriting     =     0;  // enables AIG rewriting
-    p->fVerbose       =     1;  // verbose stats
-}
+    p->nWords         =      20;  // the number of simulation words
+    p->nRounds        =      20;  // the number of simulation rounds
+    p->nItersMax      =      20;  // the maximum number of iterations of SAT sweeping
+    p->nBTLimit       =   10000;  // conflict limit at a node
+    p->nSatVarMax     =    2000;  // the max number of SAT variables
+    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
+    p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
+    p->fRewriting     =       0;  // enables AIG rewriting
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+} 
 
 /**Function*************************************************************
 
@@ -85,20 +92,19 @@ void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
 void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
 {
     memset( p, 0, sizeof(Cec_ParCec_t) );
-    p->nIters         =     5;  // iterations of SAT solving/sweeping
-    p->nBTLimitBeg    =     2;  // starting backtrack limit
-    p->nBTlimitMulti  =     8;  // multiple of backtrack limiter
-    p->fUseSmartCnf   =     0;  // use smart CNF computation
-    p->fRewriting     =     0;  // enables AIG rewriting
-    p->fSatSweeping   =     0;  // enables SAT sweeping
-    p->fFirstStop     =     0;  // stop on the first sat output
-    p->fVerbose       =     1;  // verbose stats
-}
-
+    p->nIters         =       1;  // iterations of SAT solving/sweeping
+    p->nBTLimitBeg    =       2;  // starting backtrack limit
+    p->nBTlimitMulti  =       8;  // multiple of backtrack limiter
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fRewriting     =       0;  // enables AIG rewriting
+    p->fSatSweeping   =       0;  // enables SAT sweeping
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVerbose       =       1;  // verbose stats
+}  
 
 /**Function*************************************************************
 
-  Synopsis    [Performs equivalence checking.]
+  Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
                
@@ -107,39 +113,21 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit )
+Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 {
-    Cec_MtrStatus_t Status;
-    Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw;
-    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Caig_Man_t * pCaig;
-    Aig_Man_t * pSRAig;
-    int clk;
-
-    Cec_ManCswSetDefaultParams( pParsCsw );
-    pParsCsw->nBTlimit = nBTLimit;
-    pCaig = Caig_ManClassesPrepare( pAig, pParsCsw->nWords, pParsCsw->nRounds );
-
-    pSRAig = Caig_ManSpecReduce( pCaig );
-    Aig_ManPrintStats( pSRAig );
-
-    Cec_ManSatSetDefaultParams( pParsSat );
-    pParsSat->fFirstStop = 0;
-    pParsSat->nBTLimit = pParsCsw->nBTlimit;
-clk = clock();
-    Status = Cec_SatSolveOutputs( pSRAig, pParsSat );
-    Cec_MiterStatusPrint( Status, "SRM   ", clock() - clk );
-
-    Aig_ManStop( pSRAig );
-
-    Caig_ManDelete( pCaig );
-
-    return 1;
+    Gia_Man_t * pNew;
+    Cec_ManPat_t * pPat;
+    pPat = Cec_ManPatStart();
+    Cec_ManSatSolve( pPat, pAig, pPars );
+    pNew = Gia_ManDupDfsSkip( pAig );
+    Cec_ManPatStop( pPat );
+    return pNew;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Performs equivalence checking.]
+  Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
                
@@ -148,82 +136,94 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars )
+Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars )
 {
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Cec_MtrStatus_t Status;
-    Aig_Man_t * pMiter;
-    int i, clk = clock();
-    if ( pPars->fVerbose )
-    {
-        Status = Cec_MiterStatusTrivial( pAig0 );
-        Status.nNodes += pAig1? Aig_ManNodeNum( pAig1 ) : 0;
-        Cec_MiterStatusPrint( Status, "Init  ", 0 );
-    }
-    // create combinational miter
-    if ( pAig1 == NULL )
+    Gia_Man_t * pNew;
+    Cec_ManCsw_t * p;
+    Cec_ManPat_t * pPat;
+    int i, RetValue, clk, clk2, clkTotal = clock();
+    Aig_ManRandom( 1 );
+    Gia_ManSetPhase( pAig );
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
+    p = Cec_ManCswStart( pAig, pPars );
+clk = clock();
+    RetValue = Cec_ManCswClassesPrepare( p );
+p->timeSim += clock() - clk;
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVeryVerbose;
+    pPat = Cec_ManPatStart();
+    pPat->fVerbose = pPars->fVeryVerbose;
+    for ( i = 1; i <= pPars->nItersMax; i++ )
     {
-        Status = Cec_MiterStatus( pAig0 );
-        if ( Status.nSat > 0 && pPars->fFirstStop )
+        clk2 = clock();
+        pNew = Cec_ManCswSpecReduction( p ); 
+        if ( pPars->fVeryVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "Output %d is trivially SAT.\n", Status.iOut );
-            return 0;
+            Gia_ManPrintStats( p->pAig );
+            Gia_ManPrintStats( pNew );
         }
-        if ( Status.nUndec == 0 )
+        if ( Gia_ManCoNum(pNew) == 0 )
         {
-            if ( pPars->fVerbose )
-            printf( "The miter has no undecided outputs.\n" );
-            return 1;
+            Gia_ManStop( pNew );
+            break;
         }
-        pMiter = Cec_Duplicate( pAig0 );
-    }
-    else
-    {
-        pMiter = Cec_DeriveMiter( pAig0, pAig1 );
-        Status = Cec_MiterStatus( pMiter );
-        if ( Status.nSat > 0 && pPars->fFirstStop )
+clk = clock();
+        Cec_ManSatSolve( pPat, pNew, pParsSat ); 
+p->timeSat += clock() - clk;
+clk = clock();
+        Cec_ManCswClassesUpdate( p, pPat, pNew );
+p->timeSim += clock() - clk;
+        Gia_ManStop( pNew );
+        pNew = Cec_ManCswDupWithClasses( p );
+        Gia_WriteAiger( pNew, "gia_temp_new.aig", 0, 1 );
+        if ( p->pPars->fVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "Output %d is trivially SAT.\n", Status.iOut );
-            Aig_ManStop( pMiter );
-            return 0;
+            printf( "%3d : P =%7d. D =%7d. F =%6d. Lit =%8d. And =%8d. ", 
+                i, p->nAllProved, p->nAllDisproved, p->nAllFailed,  
+                Cec_ManCswCountLitsAll(p), Gia_ManAndNum(pNew) );
+            ABC_PRT( "Time", clock() - clk2 );
         }
-        if ( Status.nUndec == 0 )
+        if ( p->pPars->fVeryVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "The problem is solved by structrual hashing.\n" );
-            Aig_ManStop( pMiter );
-            return 1;
+            ABC_PRTP( "Sim ", p->timeSim, clock() - clkTotal );
+            ABC_PRTP( "Sat ", p->timeSat, clock() - clkTotal );
+            ABC_PRT( "Time", clock() - clkTotal );
+            printf( "****** Intermedate result %3d ******\n", i );
+            Gia_ManPrintStats( p->pAig );
+            Gia_ManPrintStats( pNew );
+            printf("The result is written into file \"%s\".\n", "gia_temp.aig" );
+            printf( "************************************\n" );
         }
-    }
-    if ( pPars->fVerbose )
-        Cec_MiterStatusPrint( Status, "Strash", clock() - clk );
-    // start parameter structures
-    Cec_ManSatSetDefaultParams( pParsSat );
-    pParsSat->fFirstStop = pPars->fFirstStop;
-    pParsSat->nBTLimit = pPars->nBTLimitBeg;
-    for ( i = 0; i < pPars->nIters; i++ )
-    {
-        // try SAT solving
-        clk = clock();
-        pParsSat->nBTLimit *= pPars->nBTlimitMulti;
-        Status = Cec_SatSolveOutputs( pMiter, pParsSat );
-        if ( pPars->fVerbose )
-            Cec_MiterStatusPrint( Status, "SAT   ", clock() - clk );
-        if ( Status.nSat && pParsSat->fFirstStop )
-            break;
-        if ( Status.nUndec == 0 )
+        if ( Gia_ManAndNum(pNew) == 0 )
+        {
+            Gia_ManStop( pNew );
             break;
+        }
+        Gia_ManStop( pNew );
+    }
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
 
-        // try rewriting
-
-        // try SAT sweeping
-        Cec_Sweep( pMiter, 10 );
-        i = i;
+    // verify the result
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Verifying the result:\n" );
+        pNew = Cec_ManCswSpecReductionProved( p );
+        pParsSat->nBTLimit = 1000000;
+        pParsSat->fVerbose = 1;
+        Cec_ManSatSolve( NULL, pNew, pParsSat ); 
+        Gia_ManStop( pNew );
     }
-    Aig_ManStop( pMiter );
-    return 1;
+
+    // create the resulting miter
+    pAig->pReprs = Cec_ManCswDeriveReprs( p );
+    pNew = Gia_ManDupDfsClasses( pAig );
+    Cec_ManCswStop( p );
+    Cec_ManPatStop( pPat );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 93221f83..309f4292 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -21,34 +21,60 @@
 #ifndef __CEC_INT_H__
 #define __CEC_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "aig.h"
 #include "satSolver.h"
 #include "bar.h"
+#include "gia.h"
 #include "cec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// simulation pattern manager
+typedef struct Cec_ManPat_t_ Cec_ManPat_t;
+struct Cec_ManPat_t_
+{
+    Vec_Int_t *      vPattern1;      // pattern in terms of primary inputs
+    Vec_Int_t *      vPattern2;      // pattern in terms of primary inputs
+    Vec_Str_t *      vStorage;       // storage for compressed patterns
+    int              iStart;         // position in the array where recent patterns begin
+    int              nPats;          // total number of recent patterns
+    int              nPatsAll;       // total number of all patterns
+    int              nPatLits;       // total number of literals in recent patterns
+    int              nPatLitsAll;    // total number of literals in all patterns
+    int              nPatLitsMin;    // total number of literals in minimized recent patterns
+    int              nPatLitsMinAll; // total number of literals in minimized all patterns
+    int              nSeries;        // simulation series
+    int              fVerbose;       // verbose stats
+    // runtime statistics
+    int              timeFind;       // detecting the pattern  
+    int              timeShrink;     // minimizing the pattern
+    int              timeVerify;     // verifying the result of minimisation
+    int              timeSort;       // sorting literals 
+    int              timePack;       // packing into sim info structures 
+    int              timeTotal;      // total runtime  
+};
+
+// SAT solving manager
 typedef struct Cec_ManSat_t_ Cec_ManSat_t;
 struct Cec_ManSat_t_
 {
     // parameters
     Cec_ParSat_t *   pPars;          
     // AIGs used in the package
-    Aig_Man_t *      pAig;           // the AIG whose outputs are considered
+    Gia_Man_t *      pAig;           // the AIG whose outputs are considered
     Vec_Int_t *      vStatus;        // status for each output
     // SAT solving
     sat_solver *     pSat;           // recyclable SAT solver
@@ -62,6 +88,11 @@ struct Cec_ManSat_t_
     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;
+    int              nConfSat;
+    int              nConfUndec;
     // runtime stats
     int              timeSatUnsat;   // unsat
     int              timeSatSat;     // sat
@@ -69,144 +100,82 @@ struct Cec_ManSat_t_
     int              timeTotal;      // total runtime
 };
 
-typedef struct Cec_ManCla_t_ Cec_ManCla_t;
-
-typedef struct Cec_ManCsw_t_ Cec_ManCsw_t;
-struct Cec_ManCsw_t_
+// combinational sweeping object
+typedef struct Cec_ObjCsw_t_ Cec_ObjCsw_t;
+struct Cec_ObjCsw_t_
 {
-    // parameters
-    Cec_ParCsw_t *   pPars;          
-    // AIGs used in the package
-    Aig_Man_t *      pAig;           // the AIG for SAT sweeping
-    Aig_Man_t *      pFraig;         // the AIG after SAT sweeping
-    // equivalence classes
-    Cec_ManCla_t *   ppClasses;      // equivalence classes of nodes
-    // choice node statistics
-    int              nLits;          // the number of lits in the cand equiv classes
-    int              nReprs;         // the number of proved equivalent pairs
-    int              nEquivs;        // the number of final equivalences
-    int              nChoices;       // the number of final choice nodes
-};
-
-typedef struct Cec_ManCec_t_ Cec_ManCec_t;
-struct Cec_ManCec_t_
-{
-    // parameters
-    Cec_ParCec_t *   pPars;          
-    // AIGs used in the package
-    Aig_Man_t *      pAig;           // the miter for equivalence checking
-    // mapping of PI/PO nodes
-
-    // counter-example
-    int *            pCex;           // counter-example
-    int              iOutput;        // the output for this counter-example
-
-    // statistics
-
-};
-
-typedef struct Cec_MtrStatus_t_ Cec_MtrStatus_t;
-struct Cec_MtrStatus_t_
-{
-    int         nInputs;  // the total number of inputs
-    int         nNodes;   // the total number of nodes
-    int         nOutputs; // the total number of outputs
-    int         nUnsat;   // the number of UNSAT outputs
-    int         nSat;     // the number of SAT outputs
-    int         nUndec;   // the number of undecided outputs
-    int         iOut;     // the satisfied output
+    int              iRepr;          // representative node
+    unsigned         iNext   : 30;   // next node in the class
+    unsigned         iProved :  1;   // this node is proved
+    unsigned         iFailed :  1;   // this node is failed
+    unsigned         SimNum;         // simulation info number
 };
 
 // combinational simulation manager
-typedef struct Caig_Man_t_ Caig_Man_t;
-struct Caig_Man_t_
+typedef struct Cec_ManCsw_t_ Cec_ManCsw_t;
+struct Cec_ManCsw_t_
 {
     // parameters
-    Aig_Man_t *     pAig;         // the AIG to be used for simulation
-    int             nWords;       // the number of words to simulate
-    // AIG representation
-    int             nPis;         // the number of primary inputs
-    int             nPos;         // the number of primary outputs
-    int             nNodes;       // the number of internal nodes
-    int             nObjs;        // nPis + nNodes + nPos + 1
-    int *           pFans0;       // fanin0 for all objects
-    int *           pFans1;       // fanin1 for all objects
-    // simulation info
-    unsigned short* pRefs;        // reference counter for each node
-    unsigned *      pSims;        // simlulation information for each node
+    Gia_Man_t *      pAig;           // the AIG to be used for simulation
+    Cec_ParCsw_t *   pPars;          // SAT sweeping parameters 
+    int              nWords;         // the number of simulation words
+    // equivalence classes
+    Cec_ObjCsw_t *   pObjs;          // objects used for SAT sweeping
     // recycable memory
-    unsigned *      pMems;        // allocated simulaton memory
-    int             nWordsAlloc;  // the number of allocated entries
-    int             nMems;        // the number of used entries  
-    int             nMemsMax;     // the max number of used entries 
-    int             MemFree;      // next free entry
-    // equivalence class representation
-    int *           pReprs;       // representatives of each node
-    int *           pNexts;       // nexts for each node
+    unsigned *       pMems;          // allocated simulaton memory
+    int              nWordsAlloc;    // the number of allocated entries
+    int              nMems;          // the number of used entries  
+    int              nMemsMax;       // the max number of used entries 
+    int              MemFree;        // next free entry
     // temporaries
-    Vec_Ptr_t *     vSims;        // pointers to sim info
-    Vec_Int_t *     vClassOld;    // old class numbers
-    Vec_Int_t *     vClassNew;    // new class numbers
+    Vec_Int_t *      vClassOld;      // old class numbers
+    Vec_Int_t *      vClassNew;      // new class numbers
+    Vec_Int_t *      vClassTemp;     // temporary storage
+    Vec_Int_t *      vRefinedC;      // refined const reprs
+    // simulation patterns
+    Vec_Int_t *      vXorNodes;      // nodes used in speculative reduction
+    int              nAllProved;     // total number of proved nodes
+    int              nAllDisproved;  // total number of disproved nodes
+    int              nAllFailed;     // total number of failed nodes
+    // runtime stats
+    int              timeSim;        // unsat
+    int              timeSat;        // sat
+    int              timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int  Cec_Var2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
-static inline int  Cec_Lit2Var( int Lit )              { return Lit >> 1;           }
-static inline int  Cec_LitIsCompl( int Lit )           { return Lit & 1;            }
-static inline int  Cec_LitNot( int Lit )               { return Lit ^ 1;            }
-static inline int  Cec_LitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
-static inline int  Cec_LitRegular( int Lit )           { return Lit & ~01;          }
-
-static inline int  Cec_ObjSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
-static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
-
-static inline Aig_Obj_t * Cec_ObjFraig( Aig_Obj_t * pObj )                       { return pObj->pData;  }
-static inline void        Cec_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
-static inline int  Cec_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
-{
-    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
-}
-static inline void Cec_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
-{
-    assert( !Cec_ObjIsConst1Cand( pAig, pObj ) );
-    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== cecAig.c ==========================================================*/
-extern Aig_Man_t *     Cec_Duplicate( Aig_Man_t * p );
-extern Aig_Man_t *     Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 );
-/*=== cecClass.c ==========================================================*/
-extern Aig_Man_t *     Caig_ManSpecReduce( Caig_Man_t * p );
-extern int             Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords );
-extern int             Caig_ManCompareConst( unsigned * p, int nWords );
-extern void            Caig_ManProcessClass( Caig_Man_t * p, int i );
-extern void            Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined );
-extern Caig_Man_t *    Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters );
-/*=== cecCnf.c ==========================================================*/
-extern void            Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj );
-/*=== cecSat.c ==========================================================*/
-extern Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars );
-/*=== cecSim.c ==========================================================*/
-extern Caig_Man_t *    Caig_ManCreate( Aig_Man_t * pAig );
-extern void            Caig_ManDelete( Caig_Man_t * p );
-extern unsigned *      Caig_ManSimRead( Caig_Man_t * p, int i );
-extern unsigned *      Caig_ManSimRef( Caig_Man_t * p, int i );
-extern unsigned *      Caig_ManSimDeref( Caig_Man_t * p, int i );
-extern int             Caig_ManSimulateRound( Caig_Man_t * p, int fMiter );
-extern int             Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
-/*=== cecStatus.c ==========================================================*/
-extern int             Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p );
-extern Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p );
-extern void            Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time );
+/*=== cecCore.c ============================================================*/
+/*=== cecClass.c ============================================================*/
+extern int                  Cec_ManCswCountLitsAll( Cec_ManCsw_t * p );
+extern int *                Cec_ManCswDeriveReprs( Cec_ManCsw_t * p );
+extern Gia_Man_t *          Cec_ManCswSpecReduction( Cec_ManCsw_t * p );
+extern Gia_Man_t *          Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p );
+extern Gia_Man_t *          Cec_ManCswDupWithClasses( Cec_ManCsw_t * p );
+extern int                  Cec_ManCswClassesPrepare( Cec_ManCsw_t * p );
+extern int                  Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
+/*=== cecMan.c ============================================================*/
+extern Cec_ManCsw_t *       Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t *  pPars );  
+extern void                 Cec_ManCswStop( Cec_ManCsw_t * p );
+extern Cec_ManPat_t *       Cec_ManPatStart();
+extern void                 Cec_ManPatPrintStats( Cec_ManPat_t * p );
+extern void                 Cec_ManPatStop( Cec_ManPat_t * p );
+extern Cec_ManSat_t *       Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void                 Cec_ManSatPrintStats( Cec_ManSat_t * p );
+extern void                 Cec_ManSatStop( Cec_ManSat_t * p );
+/*=== cecPat.c ============================================================*/
+extern void                 Cec_ManPatSavePattern( Cec_ManPat_t *  pPat, Cec_ManSat_t *  p, Gia_Obj_t * pObj );
+extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWords );
+/*=== cecSolve.c ============================================================*/
+extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
+extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+/*=== cecUtil.c ============================================================*/
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 86415c53..b8ee75b2 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Creates AIG.]
 
   Description []
                
@@ -39,10 +39,26 @@
   SeeAlso     []
 
 ***********************************************************************/
+Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t *  pPars )  
+{ 
+    Cec_ManCsw_t * p;
+    p = ABC_ALLOC( Cec_ManCsw_t, 1 );
+    memset( p, 0, sizeof(Cec_ManCsw_t) );
+    p->pAig  = pAig;
+    p->pPars = pPars;
+    p->pObjs = ABC_CALLOC( Cec_ObjCsw_t, Gia_ManObjNum(pAig) );
+    // temporaries
+    p->vClassOld  = Vec_IntAlloc( 1000 );
+    p->vClassNew  = Vec_IntAlloc( 1000 );
+    p->vClassTemp = Vec_IntAlloc( 1000 );
+    p->vRefinedC  = Vec_IntAlloc( 10000 );
+    p->vXorNodes  = Vec_IntAlloc( 1000 );
+    return p;
+}
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Deletes AIG.]
 
   Description []
                
@@ -51,6 +67,161 @@
   SeeAlso     []
 
 ***********************************************************************/
+void Cec_ManCswStop( Cec_ManCsw_t * p )  
+{
+    Vec_IntFree( p->vXorNodes );
+    Vec_IntFree( p->vClassOld );
+    Vec_IntFree( p->vClassNew );
+    Vec_IntFree( p->vClassTemp );
+    Vec_IntFree( p->vRefinedC );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cec_ManPat_t * Cec_ManPatStart()  
+{ 
+    Cec_ManPat_t * p;
+    p = ABC_CALLOC( Cec_ManPat_t, 1 );
+    p->vStorage  = Vec_StrAlloc( 1<<20 );
+    p->vPattern1 = Vec_IntAlloc( 1000 );
+    p->vPattern2 = Vec_IntAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatPrintStats( Cec_ManPat_t * p )  
+{ 
+    printf( "Latest: P = %8d.  L = %10d.  Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", 
+        p->nPats, p->nPatLits, p->nPatLitsMin, 1.0 * p->nPatLitsMin/p->nPats, 
+        1.0*(Vec_StrSize(p->vStorage)-p->iStart)/(1<<20) );
+    printf( "Total:  P = %8d.  L = %10d.  Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", 
+        p->nPatsAll, p->nPatLitsAll, p->nPatLitsMinAll, 1.0 * p->nPatLitsMinAll/p->nPatsAll, 
+        1.0*Vec_StrSize(p->vStorage)/(1<<20) );
+    ABC_PRTP( "Finding  ", p->timeFind,   p->timeTotal );
+    ABC_PRTP( "Shrinking", p->timeShrink, p->timeTotal );
+    ABC_PRTP( "Verifying", p->timeVerify, p->timeTotal );
+    ABC_PRTP( "Sorting  ", p->timeSort,   p->timeTotal );
+    ABC_PRTP( "Packing  ", p->timePack,   p->timeTotal );
+    ABC_PRT( "TOTAL    ",  p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatStop( Cec_ManPat_t * p )  
+{
+    Vec_StrFree( p->vStorage );
+    Vec_IntFree( p->vPattern1 );
+    Vec_IntFree( p->vPattern2 );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+{
+    Cec_ManSat_t * p;
+    // create interpolation manager
+    p = ABC_ALLOC( Cec_ManSat_t, 1 );
+    memset( p, 0, sizeof(Cec_ManSat_t) );
+    p->pPars        = pPars;
+    p->pAig         = pAig;
+    // SAT solving
+    p->nSatVars     = 1;
+    p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
+    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
+    p->vFanins      = Vec_PtrAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatPrintStats( Cec_ManSat_t * p )
+{
+    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "Conf = %5d  ", p->pPars->nBTLimit );
+    printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
+    printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatStop( Cec_ManSat_t * p )
+{
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    Vec_PtrFree( p->vUsedNodes );
+    Vec_PtrFree( p->vFanins );
+    ABC_FREE( p->pSatVars );
+    ABC_FREE( p );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
new file mode 100644
index 00000000..1af4f333
--- /dev/null
+++ b/src/aig/cec/cecPat.c
@@ -0,0 +1,493 @@
+/**CFile****************************************************************
+
+  FileName    [cec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cec_ManPatStoreNum( Cec_ManPat_t * p, int Num )
+{
+    unsigned x = (unsigned)Num;
+    assert( Num >= 0 );
+    while ( x & ~0x7f )
+    {
+        Vec_StrPush( p->vStorage, (char)((x & 0x7f) | 0x80) );
+        x >>= 7;
+    }
+    Vec_StrPush( p->vStorage, (char)x );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cec_ManPatRestoreNum( Cec_ManPat_t * p )
+{
+    int ch, i, x = 0;
+    for ( i = 0; (ch = Vec_StrEntry(p->vStorage, p->iStart++)) & 0x80; i++ )
+        x |= (ch & 0x7f) << (7 * i);
+    return x | (ch << (7 * i));
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cec_ManPatStore( Cec_ManPat_t * p, Vec_Int_t * vPat )
+{
+    int i, Number, NumberPrev;
+    assert( Vec_IntSize(vPat) > 0 );
+    Cec_ManPatStoreNum( p, Vec_IntSize(vPat) );
+    NumberPrev = Vec_IntEntry( vPat, 0 );
+    Cec_ManPatStoreNum( p, NumberPrev );
+    Vec_IntForEachEntryStart( vPat, Number, i, 1 )
+    {
+        assert( NumberPrev < Number );
+        Cec_ManPatStoreNum( p, Number - NumberPrev );
+        NumberPrev = Number;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cec_ManPatRestore( Cec_ManPat_t * p, Vec_Int_t * vPat )
+{
+    int i, Size, Number;
+    Vec_IntClear( vPat );
+    Size = Cec_ManPatRestoreNum( p );
+    Number = Cec_ManPatRestoreNum( p );
+    Vec_IntPush( vPat, Number );
+    for ( i = 1; i < Size; i++ )
+    {
+        Number += Cec_ManPatRestoreNum( p );
+        Vec_IntPush( vPat, Number );
+    }
+    assert( Vec_IntSize(vPat) == Size );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManPatComputePattern_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Counter = 0;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pObj->fMark1 = Cec_ObjSatVarValue( pSat, pObj );
+        return 1;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin0(pObj) );
+    Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin1(pObj) );
+    pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
+                   (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatComputePattern1_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vPat, Gia_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( pObj->fMark1 == 1 )
+    {
+        Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
+        Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
+    }
+    else
+    {
+        assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
+                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
+        if ( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 )
+            Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
+        else
+            Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatComputePattern2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vPat, Gia_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( pObj->fMark1 == 1 )
+    {
+        Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
+        Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
+    }
+    else
+    {
+        assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
+                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
+        if ( (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 )
+            Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
+        else
+            Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManPatComputePattern3_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Value0, Value1, Value;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return (pObj->fMark1 << 1) | pObj->fMark0;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pObj->fMark0 = 1;
+        pObj->fMark1 = 1;
+        return GIA_UND;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Value0 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
+    Value1 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin1(pObj) );
+    Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
+    pObj->fMark0 =  (Value & 1);
+    pObj->fMark1 = ((Value >> 1) & 1);
+    return Value;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
+{
+    Gia_Obj_t * pTemp;
+    int i, Value;
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vPat, Value, i )
+    {
+        pTemp = Gia_ManCi( p, Gia_Lit2Var(Value) );
+//        assert( Gia_LitIsCompl(Value) != (int)pTemp->fMark1 );
+        if ( pTemp->fMark1 )
+        {
+            pTemp->fMark0 = 0;
+            pTemp->fMark1 = 1;
+        }
+        else
+        {
+            pTemp->fMark0 = 1;
+            pTemp->fMark1 = 0;
+        }
+        Gia_ObjSetTravIdCurrent( p, pTemp );
+    }
+    Value = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
+    Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) );
+    if ( Value != GIA_ONE )
+        printf( "Cec_ManPatVerifyPattern(): Verification failed.\n" );
+    assert( Value == GIA_ONE );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatComputePattern4_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    pObj->fMark0 = 0;
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
+    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsCo(pObj) );
+    Gia_ManIncrementTravId( p );
+    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t *  p, Gia_Obj_t * pObj )
+{
+    Vec_Int_t * vPat;
+    int nPatLits, clk, clkTotal = clock();
+    assert( Gia_ObjIsCo(pObj) );
+    pMan->nPats++;
+    pMan->nPatsAll++;
+    // compute values in the cone of influence
+clk = clock();
+    Gia_ManIncrementTravId( p->pAig );
+    nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
+    assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
+    pMan->nPatLits += nPatLits;
+    pMan->nPatLitsAll += nPatLits;
+pMan->timeFind += clock() - clk;
+    // compute sensitizing path
+clk = clock();
+    Vec_IntClear( pMan->vPattern1 );
+    Gia_ManIncrementTravId( p->pAig );
+    Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
+    // compute sensitizing path
+    Vec_IntClear( pMan->vPattern2 );
+    Gia_ManIncrementTravId( p->pAig );
+    Cec_ManPatComputePattern2_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern2 );
+    // compare patterns
+    vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
+    pMan->nPatLitsMin += Vec_IntSize(vPat);
+    pMan->nPatLitsMinAll += Vec_IntSize(vPat);
+pMan->timeShrink += clock() - clk;
+    // verify pattern using ternary simulation
+clk = clock();
+    Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
+pMan->timeVerify += clock() - clk;
+    // sort pattern
+clk = clock();
+    Vec_IntSort( vPat, 0 );
+pMan->timeSort += clock() - clk;
+    // save pattern
+    Cec_ManPatStore( pMan, vPat );
+    pMan->timeTotal += clock() - clkTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+*************************************`**********************************/
+int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
+{
+    unsigned * pInfo, * pPres;
+    int i;
+    for ( i = 0; i < nLits; i++ )
+    {
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        if ( Aig_InfoHasBit( pPres, iBit ) && 
+             Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+             return 0;
+    }
+    for ( i = 0; i < nLits; i++ )
+    {
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        Aig_InfoSetBit( pPres, iBit );
+        if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+            Aig_InfoXorBit( pInfo, iBit );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWordsInit )
+{
+    Vec_Int_t * vPat = pMan->vPattern1;
+    Vec_Ptr_t * vInfo, * vPres;
+    int k, kMax = -1, nPatterns = 0;
+    int iStartOld = pMan->iStart;
+    int nWords = nWordsInit;
+    int nBits = 32 * nWords;
+    int clk = clock();
+    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Aig_ManRandomInfo( vInfo, 0, nWords );
+    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Vec_PtrCleanSimInfo( vPres, 0, nWords );
+    while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
+    {
+        nPatterns++;
+        Cec_ManPatRestore( pMan, vPat );
+        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
+            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+        kMax = AIG_MAX( kMax, k );
+        if ( k == nBits-1 )
+        {
+            Vec_PtrReallocSimInfo( vInfo );
+            Aig_ManRandomInfo( vInfo, nWords, 2*nWords );
+            Vec_PtrReallocSimInfo( vPres );
+            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
+            nWords *= 2;
+            nBits *= 2;
+        }
+    }
+    Vec_PtrFree( vPres );
+    pMan->nSeries = Vec_PtrReadWordsSimInfo(vInfo) / nWordsInit;
+    pMan->timePack += clock() - clk;
+    pMan->timeTotal += clock() - clk;
+    pMan->iStart = iStartOld;
+    if ( pMan->fVerbose )
+    {
+        printf( "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", 
+            nPatterns, kMax, nWordsInit*32, pMan->nSeries );
+        ABC_PRT( "Time", clock() - clk );
+        Cec_ManPatPrintStats( pMan );
+    }
+    return vInfo;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecSat.c b/src/aig/cec/cecSat.c
deleted file mode 100644
index 9cf13ebc..00000000
--- a/src/aig/cec/cecSat.c
+++ /dev/null
@@ -1,250 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinatinoal equivalence checking.]
-
-  Synopsis    [SAT solver calls.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cec_ManSat_t * Cec_ManCreate( Aig_Man_t * pAig, Cec_ParSat_t * pPars )
-{
-    Cec_ManSat_t * p;
-    // create interpolation manager
-    p = ALLOC( Cec_ManSat_t, 1 );
-    memset( p, 0, sizeof(Cec_ManSat_t) );
-    p->pPars        = pPars;
-    p->pAig         = pAig;
-    // SAT solving
-    p->nSatVars     = 1;
-    p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(pAig) );
-    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
-    p->vFanins      = Vec_PtrAlloc( 100 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManStop( Cec_ManSat_t * p )
-{
-    if ( p->pSat )
-        sat_solver_delete( p->pSat );
-    Vec_PtrFree( p->vUsedNodes );
-    Vec_PtrFree( p->vFanins );
-    FREE( p->pSatVars );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recycles the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
-{
-    int Lit;
-    if ( p->pSat )
-    {
-        Aig_Obj_t * pObj;
-        int i;
-        Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
-            Cec_ObjSetSatNum( p, pObj, 0 );
-        Vec_PtrClear( p->vUsedNodes );
-//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
-        sat_solver_delete( p->pSat );
-    }
-    p->pSat = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 1000 );
-    // var 0 is not used
-    // var 1 is reserved for const1 node - add the clause
-    p->nSatVars = 1;
-//    p->nSatVars = 0;
-    Lit = toLit( p->nSatVars );
-    if ( p->pPars->fPolarFlip )
-        Lit = lit_neg( Lit );
-    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    Cec_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
-
-    p->nRecycles++;
-    p->nCallsSince = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs equivalence test for the two nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManSatCheckNode( Cec_ManSat_t * p, Aig_Obj_t * pNode )
-{
-    int nBTLimit = p->pPars->nBTLimit;
-    int Lit, RetValue, status, clk;
-
-    // sanity checks
-    assert( !Aig_IsComplement(pNode) );
-
-    p->nCallsSince++;  // experiment with this!!!
-    
-    // check if SAT solver needs recycling
-    if ( p->pSat == NULL || 
-        (p->pPars->nSatVarMax && 
-         p->nSatVars > p->pPars->nSatVarMax && 
-         p->nCallsSince > p->pPars->nCallsRecycle) )
-        Cec_ManSatSolverRecycle( p );
-
-    // if the nodes do not have SAT variables, allocate them
-    Cec_CnfNodeAddToSolver( p, pNode );
-
-    // propage unit clauses
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-    Lit = toLitCond( Cec_ObjSatNum(p,pNode), pNode->fPhase );
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( pNode->fPhase )  Lit = lit_neg( Lit );
-    }
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
-    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-    if ( RetValue == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        Lit = lit_neg( Lit );
-        RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-        assert( RetValue );
-        p->timeSatUnsat++;
-        return 1;
-    }
-    else if ( RetValue == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        p->timeSatSat++;
-        return 0;
-    }
-    else // if ( RetValue == l_Undef )
-    {
-p->timeSatUndec += clock() - clk;
-        p->timeSatUndec++;
-        return -1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars )
-{
-    Bar_Progress_t * pProgress = NULL;
-    Cec_MtrStatus_t Status;
-    Cec_ManSat_t * p;
-    Aig_Obj_t * pObj;
-    int i, status;
-    Status = Cec_MiterStatus( pAig );
-    p = Cec_ManCreate( pAig, pPars );
-    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(pAig) );
-    Aig_ManForEachPo( pAig, pObj, i )
-    {
-        Bar_ProgressUpdate( pProgress, i, "SAT..." );
-        if ( Cec_OutputStatus(pAig, pObj) )
-            continue;
-        status = Cec_ManSatCheckNode( p, Aig_ObjFanin0(pObj) );
-        if ( status == 1 )
-        {
-            Status.nUndec--, Status.nUnsat++;
-            Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst0(pAig) );
-        }
-        if ( status == 0 )
-        {
-            Status.nUndec--, Status.nSat++;
-            Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst1(pAig) );
-        }
-        if ( status == -1 )
-            continue;
-        // save the pattern (if it is first)
-        if ( Status.iOut == -1 )
-        {
-        }
-        // quit if at least one of them is solved
-        if ( status == 0 && pPars->fFirstStop )
-            break;
-    }
-    Aig_ManCleanup( pAig );
-    Bar_ProgressStop( pProgress );
-    printf( "    Confs = %8d.  Recycles = %6d.\n", p->pPars->nBTLimit, p->nRecycles );
-    Cec_ManStop( p );
-    return Status;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c
deleted file mode 100644
index 8a5f3cd5..00000000
--- a/src/aig/cec/cecSim.c
+++ /dev/null
@@ -1,459 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecSim.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinatinoal equivalence checking.]
-
-  Synopsis    [AIG simulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Count PIs with fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Caig_ManCountRelevantPis( Aig_Man_t * pAig )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    Aig_ManForEachPi( pAig, pObj, i )
-        if ( Aig_ObjRefs(pObj) )
-            Counter++;
-        else 
-            pObj->iData = -1;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count PIs with fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Caig_ManCountRelevantPos( Aig_Man_t * pAig )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    Aig_ManForEachPo( pAig, pObj, i )
-        if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
-            Counter++;
-        else 
-            pObj->iData = -1;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the PO corresponding to the PO driver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Caig_ManFindPo( Aig_Man_t * pAig, int iNode )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManForEachPo( pAig, pObj, i )
-        if ( pObj->iData == iNode )
-            return i;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates fast simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Caig_ManCreate_rec( Caig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int iFan0, iFan1;
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsConst1(pObj) );
-    if ( pObj->iData )
-        return pObj->iData;
-    if ( Aig_ObjIsNode(pObj) )
-    {
-        iFan0 = Caig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
-        iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
-        iFan1 = Caig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
-        iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
-    }
-    else if ( Aig_ObjIsPo(pObj) )
-    {
-        iFan0 = Caig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
-        iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
-        iFan1 = 0;
-    }
-    else
-        iFan0 = iFan1 = 0;
-    assert( Aig_ObjRefs(pObj) < (1<<16) );
-    p->pFans0[p->nObjs] = iFan0;
-    p->pFans1[p->nObjs] = iFan1;
-    p->pRefs[p->nObjs]  = (unsigned short)Aig_ObjRefs(pObj);
-    return pObj->iData = p->nObjs++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates fast simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig )
-{
-    Caig_Man_t * p;
-    Aig_Obj_t * pObj;
-    int i, nObjs;
-    Aig_ManCleanData( pAig );
-    p = (Caig_Man_t *)ALLOC( Caig_Man_t, 1 );
-    memset( p, 0, sizeof(Caig_Man_t) );
-    p->pAig = pAig;
-    p->nPis = Caig_ManCountRelevantPis(pAig);
-    p->nPos = Caig_ManCountRelevantPos(pAig);
-    p->nNodes = Aig_ManNodeNum(pAig);
-    nObjs = p->nPis + p->nPos + p->nNodes + 1;
-    p->pFans0 = ALLOC( int, nObjs );
-    p->pFans1 = ALLOC( int, nObjs );
-    p->pRefs = ALLOC( unsigned short, nObjs );
-    p->pSims = CALLOC( unsigned, nObjs );
-    // add objects
-    p->nObjs = 1;
-    Aig_ManForEachPo( pAig, pObj, i )
-        if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
-            Caig_ManCreate_rec( p, pObj );
-    assert( p->nObjs == nObjs );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates fast simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Caig_ManDelete( Caig_Man_t * p )
-{
-    if ( p->vSims )     Vec_PtrFree( p->vSims );
-    if ( p->vClassOld ) Vec_IntFree( p->vClassOld );
-    if ( p->vClassNew ) Vec_IntFree( p->vClassNew );
-    FREE( p->pFans0 );
-    FREE( p->pFans1 );
-    FREE( p->pRefs );
-    FREE( p->pSims );
-    FREE( p->pMems );
-    FREE( p->pReprs );
-    FREE( p->pNexts );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [References simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Caig_ManSimRead( Caig_Man_t * p, int i )
-{
-    assert( i && p->pSims[i] > 0 );
-    return p->pMems + p->pSims[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [References simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Caig_ManSimRef( Caig_Man_t * p, int i )
-{
-    unsigned * pSim;
-    assert( i );
-    assert( p->pSims[i] == 0 );
-    if ( p->MemFree == 0 )
-    {
-        int * pPlace, Ent;
-        if ( p->nWordsAlloc == 0 )
-        {
-            assert( p->pMems == NULL );
-            p->nWordsAlloc = (1<<17); // -> 1Mb
-            p->nMems = 1;
-        }
-        p->nWordsAlloc *= 2;
-        p->pMems = REALLOC( unsigned, p->pMems, p->nWordsAlloc );
-        pPlace = &p->MemFree;
-        for ( Ent = p->nMems * (p->nWords + 1); 
-              Ent + p->nWords + 1 < p->nWordsAlloc; 
-              Ent += p->nWords + 1 )
-        {
-            *pPlace = Ent;
-            pPlace = p->pMems + Ent;
-        }
-        *pPlace = 0;
-    }
-    p->pSims[i] = p->MemFree;
-    pSim = p->pMems + p->MemFree;
-    p->MemFree = pSim[0];
-    pSim[0] = p->pRefs[i];
-    p->nMems++;
-    if ( p->nMemsMax < p->nMems )
-        p->nMemsMax = p->nMems;
-    return pSim;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dereference simulaton info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i )
-{
-    unsigned * pSim;
-    assert( i );
-    assert( p->pSims[i] > 0 );
-    pSim = p->pMems + p->pSims[i];
-    if ( --pSim[0] == 0 )
-    {
-        pSim[0] = p->MemFree;
-        p->MemFree = p->pSims[i];
-        p->pSims[i] = 0;
-        p->nMems--;
-    }
-    return pSim;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one round.]
-
-  Description [Returns the number of PO entry if failed; 0 otherwise.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Caig_ManSimulateRound( Caig_Man_t * p, int fMiter )
-{
-    Vec_Int_t * vRefined = NULL;
-    unsigned * pRes0, * pRes1, * pRes;
-    int i, w, iFan0, iFan1;
-    if ( p->pReprs )
-        vRefined = Vec_IntAlloc( 1000 );
-    for ( i = 1; i < p->nObjs; i++ )
-    {
-        if ( p->pFans0[i] == 0 ) // pi always has zero first fanin
-        {
-            pRes = Caig_ManSimRef( p, i );
-            for ( w = 1; w <= p->nWords; w++ )
-                pRes[w] = Aig_ManRandom( 0 );
-            goto references;
-        }
-        if ( p->pFans1[i] == 0 ) // po always has non-zero 1st fanin and zero 2nd fanin
-        {
-            if ( fMiter )
-            {
-                unsigned Const = Cec_LitIsCompl(p->pFans0[i])? ~0 : 0;
-                pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
-                for ( w = 1; w <= p->nWords; w++ )
-                    if ( pRes0[w] != Const )
-                        return i;
-            }
-            continue;
-        }
-        pRes = Caig_ManSimRef( p, i );
-        iFan0 = p->pFans0[i];
-        iFan1 = p->pFans1[i];
-        pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
-        pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) );
-        if ( Cec_LitIsCompl(iFan0) && Cec_LitIsCompl(iFan1) )
-            for ( w = 1; w <= p->nWords; w++ )
-                pRes[w] = ~(pRes0[w] | pRes1[w]);
-        else if ( Cec_LitIsCompl(iFan0) && !Cec_LitIsCompl(iFan1) )
-            for ( w = 1; w <= p->nWords; w++ )
-                pRes[w] = ~pRes0[w] & pRes1[w];
-        else if ( !Cec_LitIsCompl(iFan0) && Cec_LitIsCompl(iFan1) )
-            for ( w = 1; w <= p->nWords; w++ )
-                pRes[w] = pRes0[w] & ~pRes1[w];
-        else if ( !Cec_LitIsCompl(iFan0) && !Cec_LitIsCompl(iFan1) )
-            for ( w = 1; w <= p->nWords; w++ )
-                pRes[w] = pRes0[w] & pRes1[w];
-references:
-        if ( p->pReprs == NULL )
-            continue;
-        // if this node is candidate constant, collect it
-        if ( p->pReprs[i] == 0 && !Caig_ManCompareConst(pRes + 1, p->nWords) )
-        {
-            pRes[0]++;
-            Vec_IntPush( vRefined, i );
-        }
-        // if the node belongs to a class, save it
-        if ( p->pReprs[i] > 0 || p->pNexts[i] > 0 )
-            pRes[0]++;
-        // if this is the last node of the class, process it
-        if ( p->pReprs[i] > 0 && p->pNexts[i] == 0 )
-            Caig_ManProcessClass( p, p->pReprs[i] );
-    }
-    if ( p->pReprs )
-        Caig_ManProcessRefined( p, vRefined );
-    if ( p->pReprs )
-        Vec_IntFree( vRefined );
-    assert( p->nMems == 1 );
-/*
-    if ( p->nMems > 1 )
-    {
-        for ( i = 1; i < p->nObjs; i++ )
-        if ( p->pSims[i] )
-        {
-            int x = 0;
-        }
-    }
-*/
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the bug is detected, 0 otherwise.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose )
-{
-    Caig_Man_t * p;
-    Cec_MtrStatus_t Status;
-    int i, RetValue = 0, clk, clkTotal = clock();
-/*
-    p = Caig_ManClassesPrepare( pAig, nWords, nIters );
-//    if ( fVerbose )
-    printf( "Maxcut = %6d.  AIG mem = %8.3f Mb.  Sim mem = %8.3f Mb.\n", 
-        p->nMemsMax, 
-        1.0*(p->nObjs * 14)/(1<<20), 
-        1.0*(p->nMemsMax * (nWords+1))/(1<<20) );
-    Caig_ManDelete( p );
-    return 0;
-*/
-    Status = Cec_MiterStatus( pAig );
-    if ( Status.nSat > 0 )
-    {
-        printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
-        return 1;
-    }
-    if ( Status.nUndec == 0 )
-    {
-        printf( "Miter is trivially unsatisfiable.\n" );
-        return 0;
-    }
-    Aig_ManRandom( 1 );
-    p = Caig_ManCreate( pAig );
-    p->nWords = nWords;
-    for ( i = 0; i < nIters; i++ )
-    {
-        clk = clock();
-        RetValue = Caig_ManSimulateRound( p, fMiter );
-        if ( fVerbose )
-        {
-            printf( "Iter %3d out of %3d and timeout %3d sec. ", i+1, nIters, TimeLimit );
-            printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC);
-        }
-        if ( RetValue > 0 )
-        {
-            int iOut = Caig_ManFindPo(p->pAig, RetValue);
-            if ( fVerbose )
-            printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
-            break;
-        }
-        if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
-        {
-            printf( "No bug detected after %d rounds with time limit %d seconds.\n", i+1, TimeLimit );
-            break;
-        }
-    }
-    if ( fVerbose )
-    printf( "Maxcut = %6d.  AIG mem = %8.3f Mb.  Sim mem = %8.3f Mb.\n", 
-        p->nMemsMax, 
-        1.0*(p->nObjs * 14)/(1<<20), 
-        1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
-    Caig_ManDelete( p );
-    return RetValue > 0;
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
new file mode 100644
index 00000000..0ec7df45
--- /dev/null
+++ b/src/aig/cec/cecSolve.c
@@ -0,0 +1,537 @@
+/**CFile****************************************************************
+
+  FileName    [cecSolve.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Performs one round of SAT solving.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSolve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Cec_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj )             { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; }
+static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj, int Num ) { p->pSatVars[Gia_ObjId(p->pAig,pObj)] = Num;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value of the SAT variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj )             
+{ 
+    return sat_solver_var_value( p->pSat, Cec_ObjSatNum(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_AddClausesMux( Cec_ManSat_t * p, Gia_Obj_t * pNode )
+{
+    Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+    assert( !Gia_IsComplement( pNode ) );
+    assert( Gia_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the variable numbers
+    VarF = Cec_ObjSatNum(p,pNode);
+    VarI = Cec_ObjSatNum(p,pNodeI);
+    VarT = Cec_ObjSatNum(p,Gia_Regular(pNodeT));
+    VarE = Cec_ObjSatNum(p,Gia_Regular(pNodeE));
+    // get the complementation flags
+    fCompT = Gia_IsComplement(pNodeT);
+    fCompE = Gia_IsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 1^fCompT);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 0^fCompT);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = toLitCond(VarT, 0^fCompT);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarT, 1^fCompT);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+    Gia_Obj_t * pFanin;
+    int * pLits, nLits, RetValue, i;
+    assert( !Gia_IsComplement(pNode) );
+    assert( Gia_ObjIsAnd( pNode ) );
+    // create storage for literals
+    nLits = Vec_PtrSize(vSuper) + 1;
+    pLits = ABC_ALLOC( int, nLits );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
+        pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1);
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Gia_Regular(pFanin)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNode->fPhase )                pLits[1] = lit_neg( pLits[1] );
+        }
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[i] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Gia_Regular(pFanin)->fPhase )  pLits[i] = lit_neg( pLits[i] );
+        }
+    }
+    pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNode->fPhase )  pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+    assert( RetValue );
+    ABC_FREE( pLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || 
+         (!fFirst && Gia_ObjValue(pObj) > 1) || 
+         (fUseMuxes && Gia_ObjIsMuxType(pObj)) )
+    {
+        Vec_PtrPushUnique( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    Cec_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Cec_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
+{
+    assert( !Gia_IsComplement(pObj) );
+    assert( !Gia_ObjIsCi(pObj) );
+    Vec_PtrClear( vSuper );
+    Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Gia_IsComplement(pObj) );
+    if ( Cec_ObjSatNum(p,pObj) )
+        return;
+    assert( Cec_ObjSatNum(p,pObj) == 0 );
+    if ( Gia_ObjIsConst0(pObj) )
+        return;
+    Vec_PtrPush( p->vUsedNodes, pObj );
+    Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
+    if ( Gia_ObjIsAnd(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{ 
+    Vec_Ptr_t * vFrontier;
+    Gia_Obj_t * pNode, * pFanin;
+    int i, k, fUseMuxes = 1;
+    // quit if CNF is ready
+    if ( Cec_ObjSatNum(p,pObj) )
+        return;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_PtrPush( p->vUsedNodes, pObj );
+        Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
+        sat_solver_setnvars( p->pSat, p->nSatVars );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    Cec_ObjAddToFrontier( p, pObj, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( Cec_ObjSatNum(p,pNode) );
+        if ( fUseMuxes && Gia_ObjIsMuxType(pNode) )
+        {
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+                Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+            Cec_AddClausesMux( p, pNode );
+        }
+        else
+        {
+            Cec_CollectSuper( pNode, fUseMuxes, p->vFanins );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+                Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+            Cec_AddClausesSuper( p, pNode, p->vFanins );
+        }
+        assert( Vec_PtrSize(p->vFanins) > 1 );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
+{
+    int Lit;
+    if ( p->pSat )
+    {
+        Gia_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+            Cec_ObjSetSatNum( p, pObj, 0 );
+        Vec_PtrClear( p->vUsedNodes );
+//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
+        sat_solver_delete( p->pSat );
+    }
+    p->pSat = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 1000 );
+    // var 0 is not used
+    // var 1 is reserved for const0 node - add the clause
+    p->nSatVars = 1;
+//    p->nSatVars = 0;
+    Lit = toLitCond( p->nSatVars, 1 );
+    if ( p->pPars->fPolarFlip )
+        Lit = lit_neg( Lit );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ );
+
+    p->nRecycles++;
+    p->nCallsSince = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+    int nBTLimit = p->pPars->nBTLimit;
+    int Lit, RetValue, status, clk, nConflicts;
+
+    p->nCallsSince++;  // experiment with this!!!
+    p->nSatTotal++;
+    
+    // check if SAT solver needs recycling
+    if ( p->pSat == NULL || 
+        (p->pPars->nSatVarMax && 
+         p->nSatVars > p->pPars->nSatVarMax && 
+         p->nCallsSince > p->pPars->nCallsRecycle) )
+        Cec_ManSatSolverRecycle( p );
+
+    // if the nodes do not have SAT variables, allocate them
+    Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) );
+
+    // propage unit clauses
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    Lit = toLitCond( Cec_ObjSatNum(p,Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Gia_ObjFanin0(pObj)->fPhase )  Lit = lit_neg( Lit );
+    }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+    nConflicts = p->pSat->stats.conflicts;
+    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        Lit = lit_neg( Lit );
+        RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+        assert( RetValue );
+        p->nSatUnsat++;
+        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
+        return 1;
+    }
+    else if ( RetValue == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatSat++;
+        p->nConfSat += p->pSat->stats.conflicts - nConflicts;
+        return 0;
+    }
+    else // if ( RetValue == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatUndec++;
+        p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
+        return -1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of solving for the POs of the AIG.]
+
+  Description [Labels the nodes that have been proved (pObj->fMark1) 
+  and returns the set of satisfying assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Cec_ManSat_t * p;
+    Gia_Obj_t * pObj;
+    int i, status, clk = clock();
+    // reset the manager
+    if ( pPat )
+    {
+        pPat->iStart = Vec_StrSize(pPat->vStorage);
+        pPat->nPats = 0;
+        pPat->nPatLits = 0;
+        pPat->nPatLitsMin = 0;
+    }
+    Gia_ManSetPhase( pAig );
+    Gia_ManResetTravId( pAig );
+    p = Cec_ManSatCreate( pAig, pPars );
+    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            pObj->fMark0 = 0;
+            pObj->fMark1 = 1;
+            continue;
+        }
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
+        status = Cec_ManSatCheckNode( p, pObj );
+        pObj->fMark0 = (status == 0);
+        pObj->fMark1 = (status == 1);
+/*
+        if ( status == -1 )
+        {
+            Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
+            Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 );
+            Gia_ManStop( pTemp );
+            printf( "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
+        }
+*/
+        if ( status != 0 )
+            continue;
+        // save the pattern
+        if ( pPat )
+            Cec_ManPatSavePattern( pPat, p, pObj );
+        // quit if one of them is solved
+        if ( pPars->fFirstStop )
+            break;
+    }
+    p->timeTotal = clock() - clk;
+    Bar_ProgressStop( pProgress );
+    if ( pPars->fVerbose )
+        Cec_ManSatPrintStats( p );
+    Cec_ManSatStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecStatus.c b/src/aig/cec/cecStatus.c
deleted file mode 100644
index 79d6ec66..00000000
--- a/src/aig/cec/cecStatus.c
+++ /dev/null
@@ -1,187 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecStatus.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinatinoal equivalence checking.]
-
-  Synopsis    [Miter status.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecStatus.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the output is known.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pChild;
-    assert( Aig_ObjIsPo(pObj) );
-    pChild = Aig_ObjChild0(pObj);
-    // check if the output is constant 0
-    if ( pChild == Aig_ManConst0(p) )
-        return 1;
-    // check if the output is constant 1
-    if ( pChild == Aig_ManConst1(p) )
-        return 1;
-    // check if the output is a primary input
-    if ( Aig_ObjIsPi(Aig_Regular(pChild)) )
-        return 1;
-    // check if the output is 1 for the 0000 pattern
-    if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns number of used inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_CountInputs( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    Aig_ManForEachPi( p, pObj, i )
-        Counter += (int)(pObj->nRefs > 0);
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p )
-{
-    Cec_MtrStatus_t Status;
-    Aig_Obj_t * pObj, * pChild;
-    int i;
-    assert( p->nRegs == 0 );
-    memset( &Status, 0, sizeof(Cec_MtrStatus_t) );
-    Status.iOut = -1;
-    Status.nInputs  = Cec_CountInputs( p );
-    Status.nNodes   = Aig_ManNodeNum( p );
-    Status.nOutputs = Aig_ManPoNum(p);
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        pChild = Aig_ObjChild0(pObj);
-        // check if the output is constant 0
-        if ( pChild == Aig_ManConst0(p) )
-            Status.nUnsat++;
-        // check if the output is constant 1
-        else if ( pChild == Aig_ManConst1(p) )
-        {
-            Status.nSat++;
-            if ( Status.iOut == -1 )
-                Status.iOut = i;
-        }
-        // check if the output is a primary input
-        else if ( Aig_ObjIsPi(Aig_Regular(pChild)) )
-        {
-            Status.nSat++;
-            if ( Status.iOut == -1 )
-                Status.iOut = i;
-        }
-    // check if the output is 1 for the 0000 pattern
-        else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
-        {
-            Status.nSat++;
-            if ( Status.iOut == -1 )
-                Status.iOut = i;
-        }
-        else
-            Status.nUndec++;
-    }
-    return Status;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p )
-{
-    Cec_MtrStatus_t Status;
-    memset( &Status, 0, sizeof(Cec_MtrStatus_t) );
-    Status.iOut = -1;
-    Status.nInputs  = Aig_ManPiNum(p);
-    Status.nNodes   = Aig_ManNodeNum( p );
-    Status.nOutputs = Aig_ManPoNum(p);
-    Status.nUndec   = Aig_ManPoNum(p);
-    return Status;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time )
-{
-    printf( "%s:", pString );
-    printf( "  I =%6d", S.nInputs );
-    printf( "  N =%7d", S.nNodes );
-    printf( "  " );
-    printf( "  ? =%6d", S.nUndec );
-    printf( "  U =%6d", S.nUnsat );
-    printf( "  S =%6d", S.nSat );
-    printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC));
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index 29f8c859..f8e2602a 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -1,8 +1,5 @@
-SRC +=    src/aig/cec/cecAig.c \
-    src/aig/cec/cecClass.c \
-    src/aig/cec/cecCnf.c \
+SRC +=    src/aig/cec/cecClass.c \
     src/aig/cec/cecCore.c \
     src/aig/cec/cecMan.c \
-    src/aig/cec/cecSat.c \
-    src/aig/cec/cecSim.c \
-    src/aig/cec/cecStatus.c
+    src/aig/cec/cecPat.c \
+    src/aig/cec/cecSolve.c