Version abc90215

13 files changed, 3442 insertions, 0 deletions

diff --git a/src/aig/cec2/cec.h b/src/aig/cec2/cec.h
new file mode 100644
index 00000000..3586b535
--- /dev/null
+++ b/src/aig/cec2/cec.h
@@ -0,0 +1,104 @@
+/**CFile****************************************************************
+
+  FileName    [cec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CEC_H__
+#define __CEC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// dynamic SAT parameters
+typedef struct Cec_ParSat_t_ Cec_ParSat_t;
+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              fFirstStop;    // stop on the first sat output
+    int              fPolarFlip;    // uses polarity adjustment
+    int              fVerbose;      // verbose stats
+};
+
+// combinational SAT sweeping parameters
+typedef struct Cec_ParCsw_t_ Cec_ParCsw_t;
+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              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              fRewriting;    // enables AIG rewriting
+    int              fFirstStop;    // stop on the first sat output
+    int              fVerbose;      // verbose stats
+};
+
+// combinational equivalence checking parameters
+typedef struct Cec_ParCec_t_ Cec_ParCec_t;
+struct Cec_ParCec_t_
+{
+    int              nIters;        // iterations of SAT solving/sweeping
+    int              nBTLimitBeg;   // starting backtrack limit
+    int              nBTlimitMulti; // multiple of backtrack limit
+    int              fUseSmartCnf;  // use smart CNF computation
+    int              fRewriting;    // enables AIG rewriting
+    int              fSatSweeping;  // enables SAT sweeping
+    int              fFirstStop;    // stop on the first sat output
+    int              fVerbose;      // verbose stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cecCore.c ==========================================================*/
+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 );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cec2/cecAig.c b/src/aig/cec2/cecAig.c
new file mode 100644
index 00000000..c322ead8
--- /dev/null
+++ b/src/aig/cec2/cecAig.c
@@ -0,0 +1,168 @@
+/**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;
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        pObj->pData = Aig_ObjCreatePi( pNew );
+        if ( pObj->pHaig )
+        {
+            assert( pObj->pHaig->pData == NULL );
+            pObj->pHaig->pData = pObj->pData;
+        }
+        return pObj->pData;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );
+    Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    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 )
+    {
+        pObj1 = Aig_ManPi( p1, i );
+        pObj0->pHaig = pObj1;
+        pObj1->pHaig = pObj0;
+        if ( Aig_ObjRefs(pObj0) || Aig_ObjRefs(pObj1) )
+            continue;
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObj0->pData = pObjNew;
+        pObj1->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_ManSetRegNum( pNew, 0 );
+    assert( Aig_ManHasNoGaps(pNew) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_Duplicate( Aig_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // make sure the AIG does not have choices and dangling nodes
+    Aig_ManForEachNode( p, pObj, i )
+        assert( Aig_ObjRefs(pObj) > 0 );
+    // 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->pHaig = NULL;
+        if ( Aig_ObjRefs(pObj) == 0 )
+            pObj->pData = Aig_ObjCreatePi( pNew );
+    }
+    // add logic for the POs
+    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        Bar_ProgressUpdate( pProgress, i, "Miter..." );
+        Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );        
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Bar_ProgressStop( pProgress );
+    Aig_ManSetRegNum( pNew, 0 );
+    assert( Aig_ManHasNoGaps(pNew) );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/cecClass.c b/src/aig/cec2/cecClass.c
new file mode 100644
index 00000000..24e40281
--- /dev/null
+++ b/src/aig/cec2/cecClass.c
@@ -0,0 +1,571 @@
+/**CFile****************************************************************
+
+  FileName    [cecClass.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Equivalence class representation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels )
+{
+    Aig_Man_t * pAig;
+    Aig_Obj_t ** pCopy;
+    Aig_Obj_t * pRes0, * pRes1, * pRepr, * pNode;
+    Aig_Obj_t * pMiter;
+    int i;
+    pAig = Aig_ManStart( p->nNodes );
+    pCopy = ABC_ALLOC( Aig_Obj_t *, p->nObjs );
+    pCopy[0] = Aig_ManConst1(pAig);
+    for ( i = 1; i < p->nObjs; i++ )
+    {
+        if ( p->pFans0[i] == -1 ) // pi always has zero first fanin
+        {
+            pCopy[i] = Aig_ObjCreatePi( pAig );
+            continue;
+        }
+        if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
+            continue;
+        pRes0 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans0[i])], Cec_LitIsCompl(p->pFans0[i]) );
+        pRes1 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans1[i])], Cec_LitIsCompl(p->pFans1[i]) );
+        pNode = pCopy[i] = Aig_And( pAig, pRes0, pRes1 );
+        if ( p->pReprs[i] < 0 )
+            continue;
+        assert( p->pReprs[i] < i );
+        pRepr = pCopy[p->pReprs[i]];
+        if ( Aig_Regular(pNode) == Aig_Regular(pRepr) )
+            continue;
+        pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) );
+        if ( nLevels && ((int)Aig_Regular(pRepr)->Level > nLevels || (int)Aig_Regular(pNode)->Level > nLevels) )
+            continue;
+        pMiter = Aig_Exor( pAig, pNode, pRepr );
+        Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+//        Aig_ObjCreatePo( pAig, Aig_Regular(pRepr) );
+//        Aig_ObjCreatePo( pAig, Aig_Regular(pCopy[i]) );
+    }
+    ABC_FREE( pCopy );
+    Aig_ManSetRegNum( pAig, 0 );
+    Aig_ManCleanup( pAig );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManCountOne( Caig_Man_t * p, int i )
+{
+    int Ent, nLits = 0;
+    assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 );
+    for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] )
+    {
+        assert( p->pReprs[Ent] == i );
+        nLits++;
+    }
+    return 1 + nLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManCountLiterals( Caig_Man_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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter )
+{
+    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" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose )
+{
+    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. Const = %6d. Unsed = %6d. Lits = %7d. All = %7d. Mem = %5.2f Mb\n", 
+        Counter, Counter1, CounterX, nLits, nLits+Counter1, 1.0*p->nMemsMax/(1<<20) );
+    if ( fVerbose )
+    for ( i = 1; i < p->nObjs; i++ )
+        if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
+            Caig_ManPrintOne( p, i, ++Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i )
+{
+    int Ent;
+    Vec_PtrClear( p->vSims );
+    for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
+        Vec_PtrPush( p->vSims, p->pSims + Ent );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i )
+{
+    unsigned * pSim;
+    int Ent;
+    Vec_PtrClear( p->vSims );
+    for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
+    {
+        pSim = Caig_ManSimDeref( p, Ent );
+        Vec_PtrPush( p->vSims, pSim + 1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords )
+{
+    int w;
+    if ( (p0[0] & 1) == (p1[0] & 1) )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != p1[w] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != ~p1[w] )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManCompareConst( unsigned * p, int nWords )
+{
+    int w;
+    if ( p[0] & 1 )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != ~0 )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != 0 )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass )
+{
+    int * pNext, Repr, 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;
+        }
+        else
+        {
+            p->pReprs[Ent] = Repr;
+            *pNext = Ent;
+            pNext = p->pNexts + Ent;
+        }
+    }
+    *pNext = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims )
+{
+    unsigned * pSim0, * pSim1;
+    int Ent, c = 0, d = 0;
+    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] )
+    {
+        pSim1 = Vec_PtrEntry( vSims, c++ );
+        if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) )
+            Vec_IntPush( p->vClassOld, Ent );
+        else
+        {
+            Vec_IntPush( p->vClassNew, Ent );
+            Vec_PtrWriteEntry( vSims, d++, pSim1 );
+        }
+    }
+//if ( Vec_PtrSize(vSims) > 100 )
+//printf( "%d -> %d %d \n", Vec_PtrSize(vSims), Vec_IntSize(p->vClassOld), Vec_IntSize(p->vClassNew) );
+    Vec_PtrShrink( vSims, d );
+    if ( Vec_IntSize(p->vClassNew) == 0 )
+        return 0;
+    Caig_ManClassCreate( p, p->vClassOld );
+    Caig_ManClassCreate( p, p->vClassNew );
+    if ( Vec_IntSize(p->vClassNew) > 1 )
+        return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
+{
+    static int s_Primes[16] = { 
+        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
+        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+    unsigned uHash = 0;
+    int i;
+    if ( pSim[0] & 1 )
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
+    else
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= pSim[i] * s_Primes[i & 0xf];
+    return (int)(uHash % nTableSize);
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManClassesCreate( Caig_Man_t * p )
+{
+    int * pTable, nTableSize, i, Key;
+    nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    p->pReprs = ABC_ALLOC( int, p->nObjs );
+    p->pNexts = ABC_CALLOC( int, p->nObjs );
+    for ( i = 1; i < p->nObjs; i++ )
+    {
+        if ( p->pFans0[i] > 0 && p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
+            continue;
+        if ( Caig_ManCompareConst( p->pSims + i, 1 ) )
+        {
+            p->pReprs[i] = 0;
+            continue;
+        }
+        Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize );
+        if ( pTable[Key] == 0 )
+            p->pReprs[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];
+        }
+        pTable[Key] = i;
+    }
+    ABC_FREE( pTable );
+Caig_ManPrintClasses( p, 0 );
+    // refine classes
+    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 );
+        }
+    // clean memory
+    memset( p->pSims, 0, sizeof(unsigned) * p->nObjs );
+Caig_ManPrintClasses( p, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManSimulateSimple( Caig_Man_t * p )
+{
+    unsigned Res0, Res1;
+    int i;
+    for ( i = 1; i < p->nObjs; i++ )
+    {
+        if ( p->pFans0[i] == -1 ) // pi
+        {
+            p->pSims[i] = Aig_ManRandom( 0 );
+            continue;
+        }
+        if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
+            continue;
+        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);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined )
+{
+    Vec_Int_t * vClasses;
+    int * pTable, nTableSize, i, Key, iNode;
+    unsigned * pSim;
+    if ( Vec_IntSize(vRefined) == 0 )
+        return;
+    nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    vClasses = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vRefined, iNode, i )
+    {
+        pSim = Caig_ManSimRead( p, iNode );
+        assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) );
+        Key = Caig_ManHashKey( pSim + 1, 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 );
+        }
+        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 );
+        }
+        pTable[Key] = iNode;
+    }
+    ABC_FREE( pTable );
+    // refine classes
+    Vec_IntForEachEntry( vClasses, iNode, i )
+    {
+        if ( p->pNexts[iNode] == 0 )
+        {
+            Caig_ManSimDeref( p, iNode );
+            continue;
+        }
+        Caig_ManCollectSimsNormal( p, iNode );
+        Caig_ManClassRefineOne( p, iNode, p->vSims );
+    }
+    Vec_IntFree( vClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters )
+{
+    Vec_Ptr_t * vInfo;
+    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++ )
+    {
+        p->nWords = i + 1;
+        Caig_ManSimMemRelink( p );
+        p->nMemsMax = 0;
+
+        vInfo = Vec_PtrAllocSimInfo( p->nPis, p->nWords );
+        Aig_ManRandomInfo( vInfo, 0, p->nWords );
+        Caig_ManSimulateRound( p, vInfo, NULL );
+        Vec_PtrFree( vInfo );
+Caig_ManPrintClasses( p, 0 );
+    }
+
+    p->nWords = nWords;
+    Caig_ManSimMemRelink( p );
+    p->nMemsMax = 0;
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/cecCnf.c b/src/aig/cec2/cecCnf.c
new file mode 100644
index 00000000..706b15e0
--- /dev/null
+++ b/src/aig/cec2/cecCnf.c
@@ -0,0 +1,328 @@
+/**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 = 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,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 );
+    ABC_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/cec2/cecCore.c b/src/aig/cec2/cecCore.c
new file mode 100644
index 00000000..540a3951
--- /dev/null
+++ b/src/aig/cec2/cecCore.c
@@ -0,0 +1,245 @@
+/**CFile****************************************************************
+
+  FileName    [cecCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParSat_t) );
+    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->fFirstStop     =     0;  // stop on the first sat output
+    p->fPolarFlip     =     0;  // uses polarity adjustment
+    p->fVerbose       =     0;  // verbose stats
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParCsw_t) );
+    p->nWords         =    10;  // the number of simulation words
+    p->nRounds        =    10;  // the number of simulation rounds
+    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->nLevelMax      =    50;  // restriction on the level of nodes to be swept
+    p->fRewriting     =     0;  // enables AIG rewriting
+    p->fFirstStop     =     0;  // stop on the first sat output
+    p->fVerbose       =     1;  // verbose stats
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParCec_t) );
+    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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit )
+{
+    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+//    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, 20 );
+    Aig_ManPrintStats( pSRAig );
+    Ioa_WriteAiger( pSRAig, "temp_srm.aig", 0, 1 );
+
+/*
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars )
+{
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw;
+    Cec_MtrStatus_t Status;
+    Caig_Man_t * pCaig;
+    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 )
+    {
+        Status = Cec_MiterStatus( pAig0 );
+        if ( Status.nSat > 0 && pPars->fFirstStop )
+        {
+            if ( pPars->fVerbose )
+            printf( "Output %d is trivially SAT.\n", Status.iOut );
+            return 0;
+        }
+        if ( Status.nUndec == 0 )
+        {
+            if ( pPars->fVerbose )
+            printf( "The miter has no undecided outputs.\n" );
+            return 1;
+        }
+        pMiter = Cec_Duplicate( pAig0 );
+    }
+    else
+    {
+        pMiter = Cec_DeriveMiter( pAig0, pAig1 );
+        Status = Cec_MiterStatus( pMiter );
+        if ( Status.nSat > 0 && pPars->fFirstStop )
+        {
+            if ( pPars->fVerbose )
+            printf( "Output %d is trivially SAT.\n", Status.iOut );
+            Aig_ManStop( pMiter );
+            return 0;
+        }
+        if ( Status.nUndec == 0 )
+        {
+            if ( pPars->fVerbose )
+            printf( "The problem is solved by structrual hashing.\n" );
+            Aig_ManStop( pMiter );
+            return 1;
+        }
+    }
+    if ( pPars->fVerbose )
+        Cec_MiterStatusPrint( Status, "Strash", clock() - clk );
+    // start parameter structures
+//    Cec_ManSatSetDefaultParams( pParsSat );
+//    pParsSat->fFirstStop = pPars->fFirstStop;
+//    pParsSat->nBTLimit   = pPars->nBTLimitBeg;
+/*
+        // 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 )
+            break;
+*/
+
+    Cec_ManCswSetDefaultParams( pParsCsw );
+    pCaig = Caig_ManClassesPrepare( pMiter, pParsCsw->nWords, pParsCsw->nRounds );
+    for ( i = 0; i < pPars->nIters; i++ )
+    {
+        Cec_ManSatSweepInt( pCaig, pParsCsw );
+        i = i;
+    }
+    Caig_ManDelete( pCaig );
+    Aig_ManStop( pMiter );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/cecInt.h b/src/aig/cec2/cecInt.h
new file mode 100644
index 00000000..ef43e44c
--- /dev/null
+++ b/src/aig/cec2/cecInt.h
@@ -0,0 +1,208 @@
+/**CFile****************************************************************
+
+  FileName    [cecInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CEC_INT_H__
+#define __CEC_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "satSolver.h"
+#include "bar.h"
+#include "cec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+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
+    Vec_Int_t *      vStatus;        // status for each output
+    // SAT solving
+    sat_solver *     pSat;           // recyclable SAT solver
+    int              nSatVars;       // the counter of SAT variables
+    int *            pSatVars;       // mapping of each node into its SAT var
+    Vec_Ptr_t *      vUsedNodes;     // nodes whose SAT vars are assigned
+    int              nRecycles;      // the number of times SAT solver was recycled
+    int              nCallsSince;    // the number of calls since the last recycle
+    Vec_Ptr_t *      vFanins;        // fanins of the CNF node
+    // SAT calls statistics
+    int              nSatUnsat;      // the number of proofs
+    int              nSatSat;        // the number of failure
+    int              nSatUndec;      // the number of timeouts
+    // runtime stats
+    int              timeSatUnsat;   // unsat
+    int              timeSatSat;     // sat
+    int              timeSatUndec;   // undecided
+    int              timeTotal;      // total runtime
+};
+
+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
+};
+
+// combinational simulation manager
+typedef struct Caig_Man_t_ Caig_Man_t;
+struct Caig_Man_t_
+{
+    // parameters
+    Aig_Man_t *     pAig;         // the AIG to be used for simulation
+    int             nWords;       // the number of simulation words
+    // 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
+    int *           pRefs;        // reference counter for each node
+    unsigned *      pSims;        // simlulation information for each node
+    // 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 ABC_FREE entry
+    // equivalence class representation
+    int *           pReprs;       // representatives of each node
+    int *           pNexts;       // nexts for each node
+    // 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 *     vRefinedC;    // refined const reprs
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      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, int nLevels );
+extern int             Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords );
+extern int             Caig_ManCompareConst( unsigned * p, int nWords );
+extern void            Caig_ManCollectSimsNormal( Caig_Man_t * p, int i );
+extern int             Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims );
+extern void            Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined );
+extern void            Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose );
+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 void            Caig_ManSimMemRelink( 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 void            Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
+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 );
+/*=== cecSweep.c ==========================================================*/
+extern void            Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars );
+extern Aig_Man_t *     Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cec2/cecMan.c b/src/aig/cec2/cecMan.c
new file mode 100644
index 00000000..86415c53
--- /dev/null
+++ b/src/aig/cec2/cecMan.c
@@ -0,0 +1,59 @@
+/**CFile****************************************************************
+
+  FileName    [cecMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Manager pcocures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/cecSat.c b/src/aig/cec2/cecSat.c
new file mode 100644
index 00000000..a999dd97
--- /dev/null
+++ b/src/aig/cec2/cecSat.c
@@ -0,0 +1,250 @@
+/**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 = 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, 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 );
+    ABC_FREE( p->pSatVars );
+    ABC_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, 
+        (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->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/cec2/cecSat2.c b/src/aig/cec2/cecSat2.c
new file mode 100644
index 00000000..4f009b25
--- /dev/null
+++ b/src/aig/cec2/cecSat2.c
@@ -0,0 +1,284 @@
+/**CFile****************************************************************
+
+  FileName    [cecSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinational equivalence checking.]
+
+  Synopsis    [Backend calling the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: cecSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "cnf.h"
+#include "../../sat/lsat/solver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p )
+{
+    solver * pSat;
+    int i, status;
+    pSat = solver_new();
+    for ( i = 0; i < p->nVars; i++ )
+        solver_newVar( pSat );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        if ( !solver_addClause( pSat, p->pClauses[i+1]-p->pClauses[i], p->pClauses[i] ) )
+        {
+            solver_delete( pSat );
+            return NULL;
+        }
+    }
+    status = solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        solver_delete( pSat );
+        return NULL;
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf )
+{
+/*
+    sat_solver * pSat = p;
+    Aig_Obj_t * pObj;
+    int i, Lit;
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+    {
+        Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
+            return 0;
+    }
+*/
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf )
+{
+    Aig_Obj_t * pObj;
+    int i, * pLits;
+    pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        pLits[i] = solver_mkLit_args( pCnf->pVarNums[pObj->Id], 0 );
+    if ( !solver_addClause( pSat, Aig_ManPoNum(pCnf->pMan), pLits ) )
+    {
+        free( pLits );
+        return 0;
+    }
+    free( pLits );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverPrintStatsNew( FILE * pFile, solver * pSat )
+{
+//    printf( "starts        : %8d\n", solver_num_assigns(pSat) );
+    printf( "vars          : %8d\n", solver_num_vars(pSat) );
+    printf( "clauses       : %8d\n", solver_num_clauses(pSat) );
+    printf( "conflicts     : %8d\n", solver_num_learnts(pSat) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ALLOC( int, nVars+1 );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < solver_num_vars(pSat) );
+        pModel[i] = (int)(solver_modelValue_Var( pSat, pVars[i] ) == solver_l_True);
+    }
+    return pModel;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_RunSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+{
+    solver * pSat;
+    Cnf_Dat_t * pCnf;
+    int status, RetValue, clk = clock();
+    Vec_Int_t * vCiIds;
+
+    assert( Aig_ManRegNum(pMan) == 0 );
+    pMan->pData = NULL;
+
+    // derive CNF
+    pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+//    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+
+    // convert into SAT solver
+    pSat = Cnf_WriteIntoSolverNew( pCnf );
+    if ( pSat == NULL )
+    {
+        Cnf_DataFree( pCnf );
+        return 1;
+    }
+
+
+    if ( fAndOuts )
+    {
+        assert( 0 );
+        // assert each output independently
+        if ( !Cnf_DataWriteAndClausesNew( pSat, pCnf ) )
+        {
+            solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+    }
+    else
+    {
+        // add the OR clause for the outputs
+        if ( !Cnf_DataWriteOrClauseNew( pSat, pCnf ) )
+        {
+            solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+    }
+    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+    Cnf_DataFree( pCnf );
+
+
+//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+
+    // simplify the problem
+    clk = clock();
+    status = solver_simplify(pSat);
+//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+    if ( status == 0 )
+    {
+        Vec_IntFree( vCiIds );
+        solver_delete( pSat );
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return 1;
+    }
+
+    // solve the miter
+    clk = clock();
+    if ( fVerbose )
+        solver_set_verbosity( pSat, 1 );
+    status = solver_solve( pSat, 0, NULL );
+    if ( status == solver_l_Undef )
+    {
+//        printf( "The problem timed out.\n" );
+        RetValue = -1;
+    }
+    else if ( status == solver_l_True )
+    {
+//        printf( "The problem is SATISFIABLE.\n" );
+        RetValue = 0;
+    }
+    else if ( status == solver_l_False )
+    {
+//        printf( "The problem is UNSATISFIABLE.\n" );
+        RetValue = 1;
+    }
+    else
+        assert( 0 );
+//    PRT( "SAT sat_solver time", clock() - clk );
+//    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
+ 
+    // if the problem is SAT, get the counterexample
+    if ( status == solver_l_True )
+    {
+        pMan->pData = Sat_SolverGetModelNew( pSat, vCiIds->pArray, vCiIds->nSize );
+    }
+    // free the sat_solver
+    if ( fVerbose )
+        Sat_SolverPrintStatsNew( stdout, pSat );
+//sat_solver_store_write( pSat, "trace.cnf" );
+//sat_solver_store_free( pSat );
+    solver_delete( pSat );
+    Vec_IntFree( vCiIds );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cec2/cecSim.c b/src/aig/cec2/cecSim.c
new file mode 100644
index 00000000..4fedbddc
--- /dev/null
+++ b/src/aig/cec2/cecSim.c
@@ -0,0 +1,447 @@
+/**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    [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;
+    assert( Aig_ManHasNoGaps(pAig) );
+    Aig_ManCleanData( pAig );
+    p = (Caig_Man_t *)ABC_ALLOC( Caig_Man_t, 1 );
+    memset( p, 0, sizeof(Caig_Man_t) );
+    p->pAig = pAig;
+    p->nPis = Aig_ManPiNum(pAig);
+    p->nPos = Aig_ManPoNum(pAig);
+    p->nNodes = Aig_ManNodeNum(pAig);
+    p->nObjs  = p->nPis + p->nPos + p->nNodes + 1;
+    p->pFans0 = ABC_ALLOC( int, p->nObjs );
+    p->pFans1 = ABC_ALLOC( int, p->nObjs );
+    p->pRefs  = ABC_ALLOC( int, p->nObjs );
+    p->pSims  = ABC_CALLOC( unsigned, p->nObjs );
+    // add objects
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        p->pRefs[i] = Aig_ObjRefs(pObj);
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+            p->pFans1[i] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+            p->pFans1[i] = -1;
+        }
+        else 
+        {
+            assert( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) );
+            p->pFans0[i] = -1;
+            p->pFans1[i] = -1;
+        }
+    }
+    // temporaries
+    p->vClassOld = Vec_IntAlloc( 1000 );
+    p->vClassNew = Vec_IntAlloc( 1000 );
+    p->vRefinedC = Vec_IntAlloc( 10000 );
+    p->vSims     = Vec_PtrAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fast simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManDelete( Caig_Man_t * p )
+{
+    Vec_IntFree( p->vClassOld );
+    Vec_IntFree( p->vClassNew );
+    Vec_IntFree( p->vRefinedC );
+    Vec_PtrFree( p->vSims );
+    ABC_FREE( p->pFans0 );
+    ABC_FREE( p->pFans1 );
+    ABC_FREE( p->pRefs );
+    ABC_FREE( p->pSims );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pReprs );
+    ABC_FREE( p->pNexts );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Caig_ManSimMemRelink( Caig_Man_t * p )
+{
+    int * pPlace, Ent;
+    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;
+}
+
+/**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( p->pSims[i] == 0 );
+    if ( p->MemFree == 0 )
+    {
+        if ( p->nWordsAlloc == 0 )
+        {
+            assert( p->pMems == NULL );
+            p->nWordsAlloc = (1<<17); // -> 1Mb
+            p->nMems = 1;
+        }
+        p->nWordsAlloc *= 2;
+        p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
+        Caig_ManSimMemRelink( p );
+    }
+    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( 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     []
+
+***********************************************************************/
+void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
+{
+    unsigned * pRes0, * pRes1, * pRes;
+    int i, w, iCiId = 0, iCoId = 0;
+    int nWords = Vec_PtrReadWordsSimInfo( vInfoCis );
+    assert( vInfoCos == NULL || nWords == Vec_PtrReadWordsSimInfo(vInfoCos) );
+    Vec_IntClear( p->vRefinedC );
+    if ( p->pRefs[0] )
+    {
+        pRes = Caig_ManSimRef( p, 0 );
+        for ( w = 1; w <= nWords; w++ )
+            pRes[w] = ~0;
+    }
+    for ( i = 1; i < p->nObjs; i++ )
+    {
+        if ( p->pFans0[i] == -1 ) // ci always has zero first fanin
+        {
+            if ( p->pRefs[i] == 0 )
+            {
+                iCiId++;
+                continue;
+            }
+            pRes = Caig_ManSimRef( p, i );
+            pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
+            for ( w = 1; w <= nWords; w++ )
+                pRes[w] = pRes0[w-1];
+            goto references;
+        }
+        if ( p->pFans1[i] == -1 ) // co always has non-zero 1st fanin and zero 2nd fanin
+        {
+            pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
+            if ( vInfoCos )
+            {
+                pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
+                if ( Cec_LitIsCompl(p->pFans0[i]) )
+                    for ( w = 1; w <= nWords; w++ )
+                        pRes[w-1] = ~pRes0[w];
+                else 
+                    for ( w = 1; w <= nWords; w++ )
+                        pRes[w-1] = pRes0[w];
+            }
+            continue;
+        }
+        assert( p->pRefs[i] );
+        pRes  = Caig_ManSimRef( p, i );
+        pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
+        pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) );
+        if ( Cec_LitIsCompl(p->pFans0[i]) )
+        {
+            if ( Cec_LitIsCompl(p->pFans1[i]) )
+                for ( w = 1; w <= nWords; w++ )
+                    pRes[w] = ~(pRes0[w] | pRes1[w]);
+            else
+                for ( w = 1; w <= nWords; w++ )
+                    pRes[w] = ~pRes0[w] & pRes1[w];
+        }
+        else
+        {
+            if ( Cec_LitIsCompl(p->pFans1[i]) )
+                for ( w = 1; w <= nWords; w++ )
+                    pRes[w] = pRes0[w] & ~pRes1[w];
+            else
+                for ( w = 1; w <= 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, nWords) )
+        {
+            pRes[0]++;
+            Vec_IntPush( p->vRefinedC, 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_ManCollectSimsNormal( p, p->pReprs[i] );
+            Caig_ManClassRefineOne( p, p->pReprs[i], p->vSims );
+        }
+    }
+    if ( Vec_IntSize(p->vRefinedC) > 0 )
+        Caig_ManProcessRefined( p, p->vRefinedC );
+    assert( iCiId == p->nPis );
+    assert( vInfoCos == NULL || iCoId == p->nPos );
+    assert( p->nMems == 1 );
+/*
+    if ( p->nMems > 1 )
+    {
+        for ( i = 1; i < p->nObjs; i++ )
+        if ( p->pSims[i] )
+        {
+            int x = 0;
+        }
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of PO that failed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManFindPo( Vec_Ptr_t * vInfo, int nWords )
+{
+    unsigned * pInfo;
+    int i, w;
+    Vec_PtrForEachEntry( vInfo, pInfo, i )
+        for ( w = 0; w < nWords; w++ )
+            if ( pInfo[w] != 0 )
+                return i;
+    return -1;
+}
+
+/**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;
+    Vec_Ptr_t * vInfoCis, * vInfoCos = NULL;
+    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;
+*/
+    if ( fMiter )
+    {
+        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;
+    if ( fMiter )
+        vInfoCos = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords );
+    for ( i = 0; i < nIters; i++ )
+    {
+        clk = clock();
+        vInfoCis = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords );
+        Aig_ManRandomInfo( vInfoCis, 0, nWords );
+        Caig_ManSimulateRound( p, vInfoCis, vInfoCos );
+        Vec_PtrFree( vInfoCis );
+        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 ( fMiter )
+        {
+            int iOut = Cec_ManFindPo( vInfoCos, nWords );
+            if ( iOut >= 0 )
+            {
+                if ( fVerbose )
+                printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
+                RetValue = 1;
+                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 );
+    if ( vInfoCos )
+        Vec_PtrFree( vInfoCos );
+    return RetValue > 0;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/cecStatus.c b/src/aig/cec2/cecStatus.c
new file mode 100644
index 00000000..79d6ec66
--- /dev/null
+++ b/src/aig/cec2/cecStatus.c
@@ -0,0 +1,187 @@
+/**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/cec2/cecSweep.c b/src/aig/cec2/cecSweep.c
new file mode 100644
index 00000000..d7d85b02
--- /dev/null
+++ b/src/aig/cec2/cecSweep.c
@@ -0,0 +1,582 @@
+/**CFile****************************************************************
+
+  FileName    [cecSweep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Pattern accumulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cec_ManCsw_t_ Cec_ManCsw_t;
+struct Cec_ManCsw_t_
+{
+    // parameters
+    Cec_ParCsw_t *  pPars;        // parameters   
+    Caig_Man_t *    p;            // AIG and simulation manager
+    // mapping into copy
+    Aig_Obj_t **    pCopy;        // the copy of nodes   
+    Vec_Int_t *     vCopies;      // the nodes copied in the last round
+    char *          pProved;      // tells if the given node is proved
+    char *          pProvedNow;   // tells if the given node is proved
+    int *           pLevel;       // level of the nodes
+    // collected patterns
+    Vec_Ptr_t *     vInfo;        // simulation info accumulated
+    Vec_Ptr_t *     vPres;        // simulation presence accumulated
+    Vec_Ptr_t *     vInfoAll;     // vector of vectors of simulation info
+    // temporaries
+    Vec_Int_t *     vPiNums;      // primary input numbers
+    Vec_Int_t *     vPoNums;      // primary output numbers
+    Vec_Int_t *     vPat;         // one counter-example
+    Vec_Ptr_t *     vSupp;        // support of one node
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds pattern to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSavePattern( Cec_ManCsw_t * p, Vec_Int_t * vPat )
+{
+    unsigned * pInfo, * pPres;
+    int nPatsAlloc, iLit, i, c;
+    assert( p->p->nWords == Vec_PtrReadWordsSimInfo(p->vInfo) );
+    // find next empty place
+    nPatsAlloc = 32 * p->p->nWords;
+    for ( c = 0; c < nPatsAlloc; c++ )
+    {
+        Vec_IntForEachEntry( vPat, iLit, i )
+        {
+            pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) );
+            if ( Aig_InfoHasBit( pPres, c ) )
+                break;
+        }
+        if ( i == Vec_IntSize(vPat) )
+            break;
+    }
+    // increase the size if needed
+    if ( c == nPatsAlloc )
+    {
+        p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->p->nWords );
+        Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords );
+        Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords );
+        Vec_PtrPush( p->vInfoAll, p->vInfo );
+        c = 0;
+    }
+    // save the pattern
+    Vec_IntForEachEntry( vPat, iLit, i )
+    {
+        pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) );
+        pInfo = Vec_PtrEntry( p->vInfo, Cec_Lit2Var(iLit) );
+        Aig_InfoSetBit( pPres, c );
+        if ( !Cec_LitIsCompl(iLit) )
+            Aig_InfoSetBit( pInfo, c );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Cec_ManCswCreatePartition_rec( Aig_Man_t * pAig, Cec_ManCsw_t * p, int i )
+{
+    Aig_Obj_t * pRes0, * pRes1;
+    if ( p->pCopy[i] )
+        return p->pCopy[i];
+    Vec_IntPush( p->vCopies, i );
+    if ( p->p->pFans0[i] == -1 ) // pi
+    {
+        Vec_IntPush( p->vPiNums, Aig_ObjPioNum( Aig_ManObj(p->p->pAig, i) ) );
+        return p->pCopy[i] = Aig_ObjCreatePi( pAig );
+    }
+    assert( p->p->pFans0[i] && p->p->pFans1[i] );
+    pRes0 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans0[i]) );
+    pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->p->pFans0[i]) );
+    pRes1 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans1[i]) );
+    pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->p->pFans1[i]) );
+    return p->pCopy[i] = Aig_And( pAig, pRes0, pRes1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates dynamic partition.]
+
+  Description [PIs point to node IDs. POs point to node IDs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_ManCswCreatePartition( Cec_ManCsw_t * p, int * piStart, int nMitersMin, int nNodesMin, int nLevelMax )
+{
+    Caig_Man_t * pMan = p->p;
+    Aig_Man_t * pAig;
+    Aig_Obj_t * pRepr, * pNode, * pMiter, * pTerm;
+    int i, iNode, Counter = 0;
+    assert( p->pCopy && p->vCopies );
+    // clear previous marks
+    Vec_IntForEachEntry( p->vCopies, iNode, i )
+        p->pCopy[iNode] = NULL;
+    Vec_IntClear( p->vCopies );
+    // iterate through nodes starting from the given one
+    pAig = Aig_ManStart( nNodesMin );
+    p->pCopy[0] = Aig_ManConst1(pAig);
+    Vec_IntPush( p->vCopies, 0 );
+    for ( i = *piStart; i < pMan->nObjs; i++ )
+    {
+        if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin
+            continue;
+        if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
+            continue;
+        if ( pMan->pReprs[i] < 0 )
+            continue;
+        if ( p->pPars->nLevelMax && (p->pLevel[i] > p->pPars->nLevelMax || p->pLevel[pMan->pReprs[i]] > p->pPars->nLevelMax) )
+            continue;
+        // create cones
+        pRepr = Cec_ManCswCreatePartition_rec( pAig, p, pMan->pReprs[i] );
+        pNode = Cec_ManCswCreatePartition_rec( pAig, p, i );
+        // skip if they are the same
+        if ( Aig_Regular(pRepr) == Aig_Regular(pNode) )
+        {
+            p->pProvedNow[i] = 1;
+            continue;
+        }
+        // perform speculative reduction
+        assert( p->pCopy[i] == pNode );
+        p->pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) );
+        if ( p->pProved[i] )
+        {
+            p->pProvedNow[i] = 1;
+            continue;
+        }
+        pMiter = Aig_Exor( pAig, pRepr, pNode );
+        pTerm = Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+        Vec_IntPush( p->vPoNums, i );
+        if ( ++Counter > nMitersMin && Aig_ManObjNum(pAig) > nNodesMin )
+            break;
+    }
+    *piStart = i + 1;
+    Aig_ManSetRegNum( pAig, 0 );
+    Aig_ManCleanup( pAig );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatDerivePattern( Cec_ManCsw_t * p, Aig_Man_t * pAig, Aig_Obj_t * pRoot, Cnf_Dat_t * pCnf, sat_solver * pSat )
+{
+    Aig_Obj_t * pObj;
+    int i, Value, iVar;
+    assert( Aig_ObjIsPo(pRoot) );
+    Aig_SupportNodes( pAig, &pRoot, 1, p->vSupp );
+    Vec_IntClear( p->vPat );
+    Vec_PtrForEachEntry( p->vSupp, pObj, i )
+    {
+        assert( Aig_ObjIsPi(pObj) );
+        Value = sat_solver_var_value( pSat, pCnf->pVarNums[pObj->Id] );
+        iVar = Vec_IntEntry( p->vPiNums, Aig_ObjPioNum(pObj) );
+        assert( iVar >= 0 && iVar < p->p->nPis );
+        Vec_IntPush( p->vPat, Cec_Var2Lit( iVar, !Value ) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCreateLevel( Cec_ManCsw_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( p->pLevel == NULL );
+    p->pLevel = ABC_ALLOC( int, p->p->nObjs );
+    Aig_ManForEachObj( p->p->pAig, pObj, i )
+        p->pLevel[i] = Aig_ObjLevel(pObj);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cec_ManCsw_t * Cec_ManCswCreate( Caig_Man_t * pMan, Cec_ParCsw_t * pPars )
+{
+    Cec_ManCsw_t * p;
+    // create interpolation manager
+    p = ABC_ALLOC( Cec_ManCsw_t, 1 );
+    memset( p, 0, sizeof(Cec_ManCsw_t) );
+    p->pPars      = pPars;
+    p->p          = pMan;
+    // internal storage
+    p->vCopies    = Vec_IntAlloc( 10000 );
+    p->pCopy      = ABC_CALLOC( Aig_Obj_t *, pMan->nObjs );
+    p->pProved    = ABC_CALLOC( char, pMan->nObjs );
+    p->pProvedNow = ABC_CALLOC( char, pMan->nObjs );
+    // temporaries
+    p->vPat       = Vec_IntAlloc( 1000 );
+    p->vSupp      = Vec_PtrAlloc( 1000 );
+    p->vPiNums    = Vec_IntAlloc( 1000 );
+    p->vPoNums    = Vec_IntAlloc( 1000 );
+    if ( pPars->nLevelMax )
+        Cec_ManCreateLevel( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCswStop( Cec_ManCsw_t * p )
+{
+    Vec_IntFree( p->vPiNums );
+    Vec_IntFree( p->vPoNums );
+    Vec_PtrFree( p->vSupp );
+    Vec_IntFree( p->vPat );
+    Vec_IntFree( p->vCopies );
+    Vec_PtrFree( p->vPres );
+    Vec_VecFree( (Vec_Vec_t *)p->vInfoAll );
+    ABC_FREE( p->pLevel );
+    ABC_FREE( p->pCopy );
+    ABC_FREE( p->pProved );
+    ABC_FREE( p->pProvedNow );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCleanSimInfo( Cec_ManCsw_t * p )
+{
+    if ( p->vInfoAll )
+        Vec_VecFree( (Vec_Vec_t *)p->vInfoAll );
+    if ( p->vPres )
+        Vec_PtrFree( p->vPres );
+    p->vInfoAll = Vec_PtrAlloc( 100 );
+    p->vInfo    = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords );
+    p->vPres    = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords );
+    Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords );
+    Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords );
+    Vec_PtrPush( p->vInfoAll, p->vInfo );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Update information about proved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCountProved( char * pArray, int nSize )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < nSize; i++ )
+        Counter += (pArray[i] == 1);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Update information about proved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCountDisproved( char * pArray, int nSize )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < nSize; i++ )
+        Counter += (pArray[i] == -1);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Update information about proved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCountTimedout( char * pArray, int nSize )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < nSize; i++ )
+        Counter += (pArray[i] == -2);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Update information about proved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManUpdateProved( Cec_ManCsw_t * p )
+{
+    Caig_Man_t * pMan = p->p;
+    int i;
+    for ( i = 1; i < pMan->nObjs; i++ )
+    {
+        if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin
+            continue;
+        if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
+            continue;
+        if ( p->pProvedNow[Cec_Lit2Var(pMan->pFans0[i])] < 0 || 
+             p->pProvedNow[Cec_Lit2Var(pMan->pFans1[i])] < 0  )
+             p->pProvedNow[i] = -1;
+        if ( pMan->pReprs[i] < 0 )
+        {
+            assert( p->pProvedNow[i] <= 0 );
+            continue;
+        }
+        if ( p->pProved[i] )
+        {
+            assert( p->pProvedNow[i] == 1 );
+            continue;
+        }
+        if ( p->pProvedNow[i] == 1 )
+            p->pProved[i] = 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates dynamic partition.]
+
+  Description [PIs point to node IDs. POs point to node IDs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSweepRound( Cec_ManCsw_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Ptr_t * vInfo;
+    Aig_Man_t * pAig, * pTemp;
+    Aig_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    int i, Lit, iNode, iStart, status;
+    int nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles = 0;
+    int clk = clock();
+    Cec_ManCleanSimInfo( p );
+    memset( p->pProvedNow, 0, sizeof(char) * p->p->nObjs );
+    pProgress = Bar_ProgressStart( stdout, p->p->nObjs );
+    for ( iStart = 1; iStart < p->p->nObjs; )
+    {
+        Bar_ProgressUpdate( pProgress, iStart, "Sweep..." );
+        Vec_IntClear( p->vPiNums );
+        Vec_IntClear( p->vPoNums );
+        // generate AIG, synthesize, convert to CNF, and solve
+        pAig = Cec_ManCswCreatePartition( p, &iStart, p->pPars->nCallsRecycle, p->pPars->nSatVarMax, p->pPars->nLevelMax );
+        Aig_ManPrintStats( pAig );
+
+        if ( p->pPars->fRewriting )
+        {
+            pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
+            Aig_ManStop( pTemp );
+        }
+        pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
+        pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+        Aig_ManForEachPo( pAig, pObj, i )
+        {
+            iNode = Vec_IntEntry( p->vPoNums, i );
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+            if ( status == l_False )
+                p->pProvedNow[iNode] = 1;
+            else if ( status == l_Undef ) 
+                p->pProvedNow[iNode] = -2;
+            else if ( status == l_True ) 
+            {
+                p->pProvedNow[iNode] = -1;
+                Cec_ManSatDerivePattern( p, pAig, pObj, pCnf, pSat );
+                Cec_ManSavePattern( p, p->vPat ); 
+            }
+        }
+        // clean up
+        Aig_ManStop( pAig );
+        Cnf_DataFree( pCnf );
+        sat_solver_delete( pSat );
+        nRecycles++;
+    }
+    Bar_ProgressStop( pProgress );
+    // collect statistics
+    nProved = Cec_ManCountProved( p->pProvedNow, p->p->nObjs );
+    nDisproved = Cec_ManCountDisproved( p->pProvedNow, p->p->nObjs );
+    nTimedout = Cec_ManCountTimedout( p->pProvedNow, p->p->nObjs );
+    nBefore = Cec_ManCountProved( p->pProved, p->p->nObjs );
+    Cec_ManUpdateProved( p );
+    nAfter = Cec_ManCountProved( p->pProved, p->p->nObjs );
+    printf( "Pr =%6d. Cex =%6d. Fail =%6d. Bef =%6d. Aft =%6d.  Rcl =%4d.", 
+        nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles );
+    ABC_PRT( "Time", clock() - clk );
+    // resimulate with the collected information
+    Vec_PtrForEachEntry( p->vInfoAll, vInfo, i )
+        Caig_ManSimulateRound( p->p, vInfo, NULL );
+Caig_ManPrintClasses( p->p, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars )
+{
+    Cec_ManCsw_t * p;
+    p = Cec_ManCswCreate( pMan, pPars );
+    Cec_ManSatSweepRound( p );
+    Cec_ManCswStop( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_ManTrasferReprs( Aig_Man_t * pAig, Caig_Man_t * pCaig )
+{
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars )
+{
+/*
+    Aig_Man_t * pAigNew, * pAigDfs;
+    Caig_Man_t * pCaig;
+    Cec_ManCsw_t * p;
+    pAigDfs = Cec_Duplicate( pAig );
+    pCaig = Caig_ManClassesPrepare( pAigDfs, pPars->nWords, pPars->nRounds );
+    p = Cec_ManCswCreate( pCaig, pPars );
+    Cec_ManSatSweep( p, pPars );
+    Cec_ManCswStop( p );
+//    pAigNew = 
+    Caig_ManDelete( pCaig );
+    Aig_ManStop( pAigDfs );
+    return pAigNew;
+*/
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec2/module.make b/src/aig/cec2/module.make
new file mode 100644
index 00000000..537397e3
--- /dev/null
+++ b/src/aig/cec2/module.make
@@ -0,0 +1,9 @@
+SRC +=    src/aig/cec/cecAig.c \
+    src/aig/cec/cecClass.c \
+    src/aig/cec/cecCnf.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/cecSweep.c