Major restructuring of the code.

13 files changed, 3058 insertions, 0 deletions

diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
new file mode 100644
index 00000000..731eb776
--- /dev/null
+++ b/src/proof/dch/dch.h
@@ -0,0 +1,90 @@
+/**CFile****************************************************************
+
+  FileName    [dch.h] 
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__dch__dch_h
+#define ABC__aig__dch__dch_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// choicing parameters
+typedef struct Dch_Pars_t_ Dch_Pars_t;
+struct Dch_Pars_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nBTLimit;      // conflict limit at a node
+    int              nSatVarMax;    // the max number of SAT variables
+    int              fSynthesis;    // set to 1 to perform synthesis
+    int              fPolarFlip;    // uses polarity adjustment
+    int              fSimulateTfo;  // uses simulation of TFO classes
+    int              fPower;        // uses power-aware rewriting
+    int              fUseGia;       // uses GIA package 
+    int              fUseCSat;      // uses circuit-based solver
+    int              fLightSynth;   // uses lighter version of synthesis
+    int              fVerbose;      // verbose stats
+    int              timeSynth;     // synthesis runtime
+    int              nNodesAhead;   // the lookahead in terms of nodes
+    int              nCallsRecycle; // calls to perform before recycling SAT solver
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dchAig.c ==========================================================*/
+extern Aig_Man_t *   Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+/*=== dchCore.c ==========================================================*/
+extern void          Dch_ManSetDefaultParams( Dch_Pars_t * p );
+extern int           Dch_ManReadVerbose( Dch_Pars_t * p );
+extern Aig_Man_t *   Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+extern void          Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+/*=== dchScript.c ==========================================================*/
+extern Aig_Man_t *   Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c
new file mode 100644
index 00000000..91a00c63
--- /dev/null
+++ b/src/proof/dch/dchAig.c
@@ -0,0 +1,119 @@
+/**CFile****************************************************************
+
+  FileName    [dchAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [AIG manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cumulative AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return;
+    Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cumulative AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
+{
+    Aig_Man_t * pAig, * pAig2, * pAigTotal;
+    Aig_Obj_t * pObj, * pObjPi, * pObjPo;
+    int i, k, nNodes;
+    assert( Vec_PtrSize(vAigs) > 0 );
+    // make sure they have the same number of PIs/POs
+    nNodes = 0;
+    pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
+    {
+        assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
+        assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
+        nNodes += Aig_ManNodeNum(pAig2);
+        Aig_ManCleanData( pAig2 );
+    }
+    // map constant nodes
+    pAigTotal = Aig_ManStart( nNodes );
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
+        Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
+    // map primary inputs
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        pObjPi = Aig_ObjCreatePi( pAigTotal );
+        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
+            Aig_ManPi( pAig2, i )->pData = pObjPi;
+    }
+    // construct the AIG in the order of POs
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
+        {
+            pObjPo = Aig_ManPo( pAig2, i );
+            Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
+        }
+        Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) );
+    }
+/*
+    // mark the cone of the first AIG
+    Aig_ManIncrementTravId( pAigTotal );
+    Aig_ManForEachObj( pAig, pObj, i )
+        if ( pObj->pData ) 
+            Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
+*/
+    // cleanup should not be done
+    return pAigTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
new file mode 100644
index 00000000..1772f8aa
--- /dev/null
+++ b/src/proof/dch/dchChoice.c
@@ -0,0 +1,508 @@
+/**CFile****************************************************************
+
+  FileName    [dchChoice.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Contrustion of choices.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, nReprs = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pRepr = Aig_ObjRepr( pAig, pObj );
+        if ( pRepr == NULL )
+            continue;
+        assert( pRepr->Id < pObj->Id );
+        nReprs++;
+    }
+    return nReprs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pTemp, * pPrev;
+    int i, nEquivs = 0, Counter = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsChoice(pAig, pObj) )
+            continue;
+        for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; 
+              pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
+        {
+            if ( pTemp->nRefs > 0 )
+            {
+                // remove referenced node from equivalence class
+                assert( pAig->pEquivs[pPrev->Id] == pTemp );
+                pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
+                pAig->pEquivs[pTemp->Id] = NULL;
+                // how about the need to continue iterating over the list?
+                // pPrev = pTemp ???
+                Counter++;
+            }
+            nEquivs++;
+        }
+    }
+//    printf( "Removed %d classes.\n", Counter );
+
+    if ( Counter )
+        Dch_DeriveChoiceCountEquivs( pAig );
+//    if ( Counter )
+//    printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
+    return nEquivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    // check the trivial cases
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsPi(pObj) )
+        return 0;
+    if ( pObj->fMarkA )
+        return 1;
+    // skip the visited node
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    // check the children
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
+        return 1;
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
+        return 1;
+    // check equivalent nodes
+    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pTemp;
+    int RetValue;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pRepr) );
+    // mark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 1;
+    // traverse the new node
+    Aig_ManIncrementTravId( p );
+    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
+    // unmark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
+        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
+    return pObj;
+}
+
+static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    // get the new node
+    pObj->pData = Aig_And( pAigNew, 
+        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
+        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
+    pRepr = Aig_ObjRepr( pAigOld, pObj );
+    if ( pRepr == NULL )
+        return;
+    // get the corresponding new nodes
+    pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
+    pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
+    if ( pObjNew == pReprNew )
+        return;
+    // skip the earlier nodes
+    if ( pReprNew->Id > pObjNew->Id )
+        return;
+    assert( pReprNew->Id < pObjNew->Id );
+    // set the representatives
+    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+    // skip used nodes
+    if ( pObjNew->nRefs > 0 )
+        return;
+    assert( pObjNew->nRefs == 0 );
+    // update new nodes of the object
+    if ( !Aig_ObjIsNode(pRepr) )
+        return;
+    // skip choices with combinational loops
+    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+        return;
+    // add choice
+    pAigNew->pEquivs[pObjNew->Id]  = pAigNew->pEquivs[pReprNew->Id];
+    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pChoices, * pTemp;
+    Aig_Obj_t * pObj;
+    int i;
+    // start recording equivalences
+    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    // map constants and PIs
+    Aig_ManCleanData( pAig );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pChoices );
+    // construct choices for the internal nodes
+    assert( pAig->pReprs != NULL );
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
+    Dch_DeriveChoiceCountEquivs( pChoices );
+    // there is no need for cleanup
+    ABC_FREE( pChoices->pReprs );
+    pChoices = Aig_ManDupDfs( pTemp = pChoices );
+    Aig_ManStop( pTemp );
+    return pChoices;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks for combinational loops in the AIG.]
+
+  Description [Returns 1 if combinational loop is detected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
+{
+    Aig_Obj_t * pFanin;
+    int fAcyclic;
+    if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) )
+        return 1;
+    assert( Aig_ObjIsNode(pNode) );
+    // make sure the node is not visited
+    assert( !Aig_ObjIsTravIdPrevious(p, pNode) );
+    // check if the node is part of the combinational loop
+    if ( Aig_ObjIsTravIdCurrent(p, pNode) )
+    {
+        if ( fVerbose )
+            Abc_Print( 1, "Network \"%s\" contains combinational loop!\n", p->pSpec? p->pSpec : NULL );
+        if ( fVerbose )
+        Abc_Print( 1, "Node \"%d\" is encountered twice on the following path to the COs:\n", Aig_ObjId(pNode) );
+        return 0;
+    }
+    // mark this node as a node on the current path
+    Aig_ObjSetTravIdCurrent( p, pNode );
+
+    // visit the transitive fanin
+    pFanin = Aig_ObjFanin0(pNode);
+    // check if the fanin is visited
+    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
+    {
+        // traverse the fanin's cone searching for the loop
+        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
+        {
+            // return as soon as the loop is detected
+            if ( fVerbose )
+            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
+            return 0;
+        }
+    }
+
+    // visit the transitive fanin
+    pFanin = Aig_ObjFanin1(pNode);
+    // check if the fanin is visited
+    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
+    {
+        // traverse the fanin's cone searching for the loop
+        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
+        {
+            // return as soon as the loop is detected
+            if ( fVerbose )
+            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
+            return 0;
+        }
+    }
+
+    // visit choices
+    if ( Aig_ObjRepr(p, pNode) == NULL && Aig_ObjEquiv(p, pNode) != NULL )
+    {
+        for ( pFanin = Aig_ObjEquiv(p, pNode); pFanin; pFanin = Aig_ObjEquiv(p, pFanin) )
+        {
+            // check if the fanin is visited
+            if ( Aig_ObjIsTravIdPrevious(p, pFanin) ) 
+                continue;
+            // traverse the fanin's cone searching for the loop
+            if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
+                continue;
+            // return as soon as the loop is detected
+            if ( fVerbose )
+            Abc_Print( 1, " %d", Aig_ObjId(pFanin) );
+            if ( fVerbose )
+            Abc_Print( 1, " (choice of %d) -> ", Aig_ObjId(pNode) );
+            return 0;
+        }
+    }
+    // mark this node as a visited node
+    Aig_ObjSetTravIdPrevious( p, pNode );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks for combinational loops in the AIG.]
+
+  Description [Returns 1 if there is no combinational loops.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Obj_t * pNode;
+    int fAcyclic;
+    int i;
+    // set the traversal ID for this DFS ordering
+    Aig_ManIncrementTravId( p );   
+    Aig_ManIncrementTravId( p );   
+    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
+    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
+    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
+    // traverse the network to detect cycles
+    fAcyclic = 1;
+    Aig_ManForEachPo( p, pNode, i )
+    {
+        pNode = Aig_ObjFanin0(pNode);
+        if ( Aig_ObjIsTravIdPrevious(p, pNode) )
+            continue;
+        // traverse the output logic cone
+        if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pNode, fVerbose)) )
+            continue;
+        // stop as soon as the first loop is detected
+        if ( fVerbose )
+        Abc_Print( 1, " CO %d\n", i );
+        break;
+    }
+    return fAcyclic;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes combinational loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0, Counter2 = 0;
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        Counter2++;
+        if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL )
+        {
+            Aig_ObjSetEquiv(p, pObj, NULL);
+            Counter++;
+        }
+    }
+    if ( fVerbose )
+    Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pChoices;
+    Aig_Obj_t * pObj;
+    int i;
+    // start recording equivalences
+    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    // map constants and PIs
+    Aig_ManCleanData( pAig );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pChoices );
+    // construct choices for the internal nodes
+    assert( pAig->pReprs != NULL );
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
+    Dch_DeriveChoiceCountEquivs( pChoices );
+    Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
+    return pChoices;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
+{
+    extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose );
+    Aig_Man_t * pChoices, * pTemp;
+    int fVerbose = 0;
+    pChoices = Dch_DeriveChoiceAigInt( pAig );
+//    pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices );
+//    Aig_ManStop( pTemp );
+    // there is no need for cleanup
+    ABC_FREE( pChoices->pReprs );
+    while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) )
+    {
+        if ( fVerbose )
+        Abc_Print( 1, "There is a loop!\n" );
+        Aig_ManFixLoopProblem( pChoices, fVerbose );
+    }
+    pChoices = Aig_ManDupDfs( pTemp = pChoices );
+    Aig_ManStop( pTemp );
+    return pChoices;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c
new file mode 100644
index 00000000..24476309
--- /dev/null
+++ b/src/proof/dch/dchClass.c
@@ -0,0 +1,611 @@
+/**CFile****************************************************************
+
+  FileName    [dchClass.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Representation of candidate equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+/*
+    The candidate equivalence classes are stored as a vector of pointers 
+    to the array of pointers to the nodes in each class.
+    The first node of the class is its representative node.
+    The representative has the smallest topological order among the class nodes.
+    The nodes inside each class are ordered according to their topological order.
+    The classes are ordered according to the topo order of their representatives.
+*/
+
+// internal representation of candidate equivalence classes
+struct Dch_Cla_t_
+{
+    // class information
+    Aig_Man_t *      pAig;             // original AIG manager
+    Aig_Obj_t ***    pId2Class;        // non-const classes by ID of repr node
+    int *            pClassSizes;      // sizes of each equivalence class
+    // statistics
+    int              nClasses;         // the total number of non-const classes
+    int              nCands1;          // the total number of const candidates
+    int              nLits;            // the number of literals in all classes
+    // memory
+    Aig_Obj_t **     pMemClasses;      // memory allocated for equivalence classes
+    Aig_Obj_t **     pMemClassesFree;  // memory allocated for equivalence classes to be used
+    // temporary data
+    Vec_Ptr_t *      vClassOld;        // old equivalence class after splitting
+    Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
+    // procedures used for class refinement
+    void *           pManData;
+    unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
+    int (*pFuncNodeIsConst)   (void *,Aig_Obj_t *);              // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
+};
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t *  Dch_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
+static inline void         Dch_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+
+// iterator through the equivalence classes
+#define Dch_ManForEachClass( p, ppClass, i )                 \
+    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )        \
+        if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
+// iterator through the nodes in one class
+#define Dch_ClassForEachNode( p, pRepr, pNode, i )           \
+    for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ )        \
+        if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Dch_ObjAddClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize ) 
+{
+    assert( p->pId2Class[pRepr->Id] == NULL );
+    p->pId2Class[pRepr->Id] = pClass; 
+    assert( p->pClassSizes[pRepr->Id] == 0 );
+    assert( nSize > 1 );
+    p->pClassSizes[pRepr->Id] = nSize;
+    p->nClasses++;
+    p->nLits += nSize - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t ** Dch_ObjRemoveClass( Dch_Cla_t * p, Aig_Obj_t * pRepr ) 
+{
+    Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
+    int nSize;
+    assert( pClass != NULL );
+    p->pId2Class[pRepr->Id] = NULL; 
+    nSize = p->pClassSizes[pRepr->Id];
+    assert( nSize > 1 );
+    p->nClasses--;
+    p->nLits -= nSize - 1;
+    p->pClassSizes[pRepr->Id] = 0;
+    return pClass;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig )
+{
+    Dch_Cla_t * p;
+    p = ABC_ALLOC( Dch_Cla_t, 1 );
+    memset( p, 0, sizeof(Dch_Cla_t) );
+    p->pAig         = pAig;
+    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
+    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->vClassOld    = Vec_PtrAlloc( 100 );
+    p->vClassNew    = Vec_PtrAlloc( 100 );
+    assert( pAig->pReprs == NULL );
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, 
+    unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),               // returns hash key of the node
+    int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),                 // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
+{
+    p->pManData           = pManData;
+    p->pFuncNodeHash      = pFuncNodeHash;
+    p->pFuncNodeIsConst   = pFuncNodeIsConst;
+    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesStop( Dch_Cla_t * p )
+{
+    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
+    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
+    ABC_FREE( p->pId2Class );
+    ABC_FREE( p->pClassSizes );
+    ABC_FREE( p->pMemClasses );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ClassesLitNum( Dch_Cla_t * p )
+{
+    return p->nLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
+{
+    assert( p->pId2Class[pRepr->Id] != NULL );
+    assert( p->pClassSizes[pRepr->Id] > 1 );
+    *pnSize = p->pClassSizes[pRepr->Id];
+    return p->pId2Class[pRepr->Id];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks candidate equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesCheck( Dch_Cla_t * p )
+{
+    Aig_Obj_t * pObj, * pPrev, ** ppClass;
+    int i, k, nLits, nClasses, nCands1;
+    nClasses = nLits = 0;
+    Dch_ManForEachClass( p, ppClass, k )
+    {
+        pPrev = NULL;
+        Dch_ClassForEachNode( p, ppClass[0], pObj, i )
+        {
+            if ( i == 0 )
+                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
+            else
+            {
+                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
+                assert( pPrev->Id < pObj->Id );
+                nLits++;
+            }
+            pPrev = pObj;
+        }
+        nClasses++;
+    }
+    nCands1 = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        nCands1 += Dch_ObjIsConst1Cand( p->pAig, pObj );
+    assert( p->nLits == nLits );
+    assert( p->nCands1 == nCands1 );
+    assert( p->nClasses == nClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesPrintOne( Dch_Cla_t * p, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Abc_Print( 1, "{ " );
+    Dch_ClassForEachNode( p, pRepr, pObj, i )
+        Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+    Abc_Print( 1, "}\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose )
+{
+    Aig_Obj_t ** ppClass;
+    Aig_Obj_t * pObj;
+    int i;
+    Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", 
+        p->nCands1, p->nClasses, p->nLits );
+    if ( !fVeryVerbose )
+        return;
+    Abc_Print( 1, "Constants { " );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) )
+            Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+    Abc_Print( 1, "}\n" );
+    Dch_ManForEachClass( p, ppClass, i )
+    {
+        Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
+        Dch_ClassesPrintOne( p, ppClass[0] );
+    }
+    Abc_Print( 1, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
+{
+    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
+    Aig_Obj_t * pObj, * pTemp, * pRepr;
+    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
+
+    // allocate the hash table hashing simulation info into nodes
+    nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
+    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
+
+    // add all the nodes to the hash table
+    nEntries = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( fLatchCorr )
+        {
+            if ( !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        else
+        {
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                continue;
+            // skip the node with more that the given number of levels
+            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+                continue;
+        }
+        // check if the node belongs to the class of constant 1
+        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
+        {
+            Dch_ObjSetConst1Cand( p->pAig, pObj );
+            p->nCands1++;
+            continue;
+        }
+        // hash the node by its simulation info
+        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
+        // add the node to the class
+        if ( ppTable[iEntry] == NULL )
+            ppTable[iEntry] = pObj;
+        else
+        {
+            // set the representative of this node
+            pRepr = ppTable[iEntry];
+            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
+            // add node to the table
+            if ( Dch_ObjNext( ppNexts, pRepr ) == NULL )
+            { // this will be the second entry
+                p->pClassSizes[pRepr->Id]++;
+                nEntries++;
+            }
+            // add the entry to the list
+            Dch_ObjSetNext( ppNexts, pObj, Dch_ObjNext( ppNexts, pRepr ) );
+            Dch_ObjSetNext( ppNexts, pRepr, pObj );
+            p->pClassSizes[pRepr->Id]++;
+            nEntries++;
+        }
+    }
+
+    // allocate room for classes
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
+    p->pMemClassesFree = p->pMemClasses + nEntries;
+ 
+    // copy the entries into storage in the topological order
+    nEntries2 = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            continue;
+        nNodes = p->pClassSizes[pObj->Id];
+        // skip the nodes that are not representatives of non-trivial classes
+        if ( nNodes == 0 )
+            continue;
+        assert( nNodes > 1 );
+        // add the nodes to the class in the topological order
+        ppClassNew = p->pMemClasses + nEntries2;
+        ppClassNew[0] = pObj;
+        for ( pTemp = Dch_ObjNext(ppNexts, pObj), k = 1; pTemp; 
+              pTemp = Dch_ObjNext(ppNexts, pTemp), k++ )
+        {
+            ppClassNew[nNodes-k] = pTemp;
+        }
+        // add the class of nodes
+        p->pClassSizes[pObj->Id] = 0;
+        Dch_ObjAddClass( p, pObj, ppClassNew, nNodes );
+        // increment the number of entries
+        nEntries2 += nNodes;
+    }
+    assert( nEntries == nEntries2 );
+    ABC_FREE( ppTable );
+    ABC_FREE( ppNexts );
+    // now it is time to refine the classes
+    Dch_ClassesRefine( p );
+    Dch_ClassesCheck( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Iteratively refines the classes after simulation.]
+
+  Description [Returns the number of refinements performed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
+{
+    Aig_Obj_t ** pClassOld, ** pClassNew;
+    Aig_Obj_t * pObj, * pReprNew;
+    int i;
+
+    // split the class
+    Vec_PtrClear( p->vClassOld );
+    Vec_PtrClear( p->vClassNew );
+    Dch_ClassForEachNode( p, pReprOld, pObj, i )
+        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
+            Vec_PtrPush( p->vClassOld, pObj );
+        else
+            Vec_PtrPush( p->vClassNew, pObj );
+    // check if splitting happened
+    if ( Vec_PtrSize(p->vClassNew) == 0 )
+        return 0;
+
+    // get the new representative
+    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
+    assert( Vec_PtrSize(p->vClassOld) > 0 );
+    assert( Vec_PtrSize(p->vClassNew) > 0 );
+
+    // create old class
+    pClassOld = Dch_ObjRemoveClass( p, pReprOld );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
+    {
+        pClassOld[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
+    }
+    // create new class
+    pClassNew = pClassOld + i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
+    {
+        pClassNew[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
+    }
+
+    // put classes back
+    if ( Vec_PtrSize(p->vClassOld) > 1 )
+        Dch_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
+    if ( Vec_PtrSize(p->vClassNew) > 1 )
+        Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
+
+    // check if the class should be recursively refined
+    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
+        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes after simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ClassesRefine( Dch_Cla_t * p )
+{
+    Aig_Obj_t ** ppClass;
+    int i, nRefis = 0;
+    Dch_ManForEachClass( p, ppClass, i )
+        nRefis += Dch_ClassesRefineOneClass( p, ppClass[0], 0 );
+    return nRefis;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns equivalence class of the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( vRoots );
+    Dch_ClassForEachNode( p, pRepr, pObj, i )
+        Vec_PtrPush( vRoots, pObj );
+    assert( Vec_PtrSize(vRoots) > 1 ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns equivalence class of the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots )
+{
+    int i, Limit;
+    Vec_PtrClear( vRoots );
+    Limit = Abc_MinInt( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
+    for ( i = pObj->Id; i < Limit; i++ )
+    {
+        pObj = Aig_ManObj( p->pAig, i );
+        if ( pObj && Dch_ObjIsConst1Cand( p->pAig, pObj ) )
+            Vec_PtrPush( vRoots, pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refine the group of constant 1 nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
+{
+    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
+    int i;
+    if ( Vec_PtrSize(vRoots) == 0 )
+        return 0;
+    // collect the nodes to be refined
+    Vec_PtrClear( p->vClassNew );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+        if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+            Vec_PtrPush( p->vClassNew, pObj );
+    // check if there is a new class
+    if ( Vec_PtrSize(p->vClassNew) == 0 )
+        return 0;
+    p->nCands1 -= Vec_PtrSize(p->vClassNew);
+    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
+    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
+    if ( Vec_PtrSize(p->vClassNew) == 1 )
+        return 1;
+    // create a new class composed of these nodes
+    ppClassNew = p->pMemClassesFree;
+    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
+    {
+        ppClassNew[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
+    }
+    Dch_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
+    // refine them recursively
+    if ( fRecursive )
+        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c
new file mode 100644
index 00000000..4175a123
--- /dev/null
+++ b/src/proof/dch/dchCnf.c
@@ -0,0 +1,334 @@
+/**CFile****************************************************************
+
+  FileName    [dchCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Computation of CNF.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_AddClausesMux( Dch_Man_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 = Dch_ObjSatNum(p,pNode);
+    VarI = Dch_ObjSatNum(p,pNodeI);
+    VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT));
+    VarE = Dch_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 Dch_AddClausesSuper( Dch_Man_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( Aig_Obj_t *, vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
+        pLits[1] = toLitCond(Dch_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( Aig_Obj_t *, vSuper, pFanin, i )
+    {
+        pLits[i] = toLitCond(Dch_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(Dch_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 Dch_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
+    Dch_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Dch_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
+{
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPi(pObj) );
+    Vec_PtrClear( vSuper );
+    Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( Dch_ObjSatNum(p,pObj) )
+        return;
+    assert( Dch_ObjSatNum(p,pObj) == 0 );
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    Vec_PtrPush( p->vUsedNodes, pObj );
+    Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
+    if ( Aig_ObjIsNode(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_CnfNodeAddToSolver( Dch_Man_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 ( Dch_ObjSatNum(p,pObj) )
+        return;
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    Dch_ObjAddToFrontier( p, pObj, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( Dch_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( Aig_Obj_t *, p->vFanins, pFanin, k )
+                Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
+            Dch_AddClausesMux( p, pNode );
+        }
+        else
+        {
+            Dch_CollectSuper( pNode, fUseMuxes, p->vFanins );
+            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
+                Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
+            Dch_AddClausesSuper( p, pNode, p->vFanins );
+        }
+        assert( Vec_PtrSize(p->vFanins) > 1 );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
new file mode 100644
index 00000000..bc78682b
--- /dev/null
+++ b/src/proof/dch/dchCore.c
@@ -0,0 +1,158 @@
+/**CFile****************************************************************
+
+  FileName    [dchCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [The core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManSetDefaultParams( Dch_Pars_t * p )
+{
+    memset( p, 0, sizeof(Dch_Pars_t) );
+    p->nWords         =     8;  // the number of simulation words
+    p->nBTLimit       =  1000;  // conflict limit at a node
+    p->nSatVarMax     =  5000;  // the max number of SAT variables
+    p->fSynthesis     =     1;  // derives three snapshots
+    p->fPolarFlip     =     1;  // uses polarity adjustment
+    p->fSimulateTfo   =     1;  // simulate TFO
+    p->fPower         =     0;  // power-aware rewriting
+    p->fLightSynth    =     0;  // uses lighter version of synthesis
+    p->fVerbose       =     0;  // verbose stats
+    p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
+    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns verbose parameter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ManReadVerbose( Dch_Pars_t * p )
+{
+    return p->fVerbose;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    Aig_Man_t * pResult;
+    int clk, clkTotal = clock();
+    // reset random numbers
+    Aig_ManRandom(1);
+    // start the choicing manager
+    p = Dch_ManCreate( pAig, pPars );
+    // compute candidate equivalence classes
+clk = clock(); 
+    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
+p->timeSimInit = clock() - clk;
+//    Dch_ClassesPrint( p->ppClasses, 0 );
+    p->nLits = Dch_ClassesLitNum( p->ppClasses );
+    // perform SAT sweeping
+    Dch_ManSweep( p );
+    // free memory ahead of time
+p->timeTotal = clock() - clkTotal;
+    Dch_ManStop( p );
+    // create choices
+    ABC_FREE( pAig->pTable );
+    pResult = Dch_DeriveChoiceAig( pAig );
+    // count the number of representatives
+    if ( pPars->fVerbose ) 
+        Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
+               Dch_DeriveChoiceCountReprs( pAig ),
+               Dch_DeriveChoiceCountEquivs( pResult ),
+               Aig_ManChoiceNum( pResult ) );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    int clk, clkTotal = clock();
+    // reset random numbers
+    Aig_ManRandom(1);
+    // start the choicing manager
+    p = Dch_ManCreate( pAig, pPars );
+    // compute candidate equivalence classes
+clk = clock(); 
+    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
+p->timeSimInit = clock() - clk;
+//    Dch_ClassesPrint( p->ppClasses, 0 );
+    p->nLits = Dch_ClassesLitNum( p->ppClasses );
+    // perform SAT sweeping
+    Dch_ManSweep( p );
+    // free memory ahead of time
+p->timeTotal = clock() - clkTotal;
+    Dch_ManStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h
new file mode 100644
index 00000000..c9f2f4f6
--- /dev/null
+++ b/src/proof/dch/dchInt.h
@@ -0,0 +1,170 @@
+/**CFile****************************************************************
+
+  FileName    [dchInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__dch__dchInt_h
+#define ABC__aig__dch__dchInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "src/aig/aig/aig.h"
+#include "src/sat/bsat/satSolver.h"
+#include "dch.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// equivalence classes
+typedef struct Dch_Cla_t_ Dch_Cla_t;
+
+// choicing manager
+typedef struct Dch_Man_t_ Dch_Man_t;
+struct Dch_Man_t_
+{
+    // parameters
+    Dch_Pars_t *     pPars;          // choicing parameters
+    // AIGs used in the package
+//    Vec_Ptr_t *      vAigs;          // user-given AIGs
+    Aig_Man_t *      pAigTotal;      // intermediate AIG
+    Aig_Man_t *      pAigFraig;      // final AIG
+    // equivalence classes
+    Dch_Cla_t *      ppClasses;      // equivalence classes of nodes
+    Aig_Obj_t **     pReprsProved;   // equivalences proved
+    // 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
+    Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
+    Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
+    // solver cone size
+    int              nConeThis;
+    int              nConeMax;
+    // SAT calls statistics
+    int              nSatCalls;      // the number of SAT calls
+    int              nSatProof;      // the number of proofs
+    int              nSatFailsReal;  // the number of timeouts
+    int              nSatCallsUnsat; // the number of unsat SAT calls
+    int              nSatCallsSat;   // the number of sat SAT calls
+    // choice node statistics
+    int              nLits;          // the number of lits in the cand equiv classes
+    int              nReprs;         // the number of proved equivalent pairs
+    int              nEquivs;        // the number of final equivalences
+    int              nChoices;       // the number of final choice nodes
+    // runtime stats
+    int              timeSimInit;    // simulation and class computation
+    int              timeSimSat;     // simulation of the counter-examples
+    int              timeSat;        // solving SAT
+    int              timeSatSat;     // sat
+    int              timeSatUnsat;   // unsat
+    int              timeSatUndec;   // undecided
+    int              timeChoice;     // choice computation
+    int              timeOther;      // other runtime
+    int              timeTotal;      // total runtime
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
+static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
+
+static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj )                       { return (Aig_Obj_t *)pObj->pData;  }
+static inline void        Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
+
+static inline int  Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
+{
+    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
+}
+static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
+{
+    assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
+    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dchAig.c ===================================================*/
+/*=== dchChoice.c ===================================================*/
+extern int           Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
+extern int           Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
+extern Aig_Man_t *   Dch_DeriveChoiceAig( Aig_Man_t * pAig );
+/*=== dchClass.c =================================================*/
+extern Dch_Cla_t *   Dch_ClassesStart( Aig_Man_t * pAig );
+extern void          Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
+                         unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
+                         int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
+                         int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
+extern void          Dch_ClassesStop( Dch_Cla_t * p );
+extern int           Dch_ClassesLitNum( Dch_Cla_t * p );
+extern Aig_Obj_t **  Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
+extern void          Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
+extern void          Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
+extern int           Dch_ClassesRefine( Dch_Cla_t * p );
+extern int           Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
+extern void          Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots );
+extern void          Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots );
+extern int           Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
+/*=== dchCnf.c ===================================================*/
+extern void          Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
+/*=== dchMan.c ===================================================*/
+extern Dch_Man_t *   Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+extern void          Dch_ManStop( Dch_Man_t * p );
+extern void          Dch_ManSatSolverRecycle( Dch_Man_t * p );
+/*=== dchSat.c ===================================================*/
+extern int           Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
+/*=== dchSim.c ===================================================*/
+extern Dch_Cla_t *   Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
+/*=== dchSimSat.c ===================================================*/
+extern void          Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+extern void          Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+/*=== dchSweep.c ===================================================*/
+extern void          Dch_ManSweep( Dch_Man_t * p );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/dch/dchMan.c b/src/proof/dch/dchMan.c
new file mode 100644
index 00000000..dc856309
--- /dev/null
+++ b/src/proof/dch/dchMan.c
@@ -0,0 +1,191 @@
+/**CFile****************************************************************
+
+  FileName    [dchMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    // create interpolation manager
+    p = ABC_ALLOC( Dch_Man_t, 1 );
+    memset( p, 0, sizeof(Dch_Man_t) );
+    p->pPars        = pPars;
+    p->pAigTotal    = pAig; //Dch_DeriveTotalAig( vAigs );
+    Aig_ManFanoutStart( p->pAigTotal );
+    // SAT solving
+    p->nSatVars     = 1;
+    p->pSatVars     = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
+    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
+    p->vFanins      = Vec_PtrAlloc( 100 );
+    p->vSimRoots    = Vec_PtrAlloc( 1000 );
+    p->vSimClasses  = Vec_PtrAlloc( 1000 );
+    // equivalences proved
+    p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManPrintStats( Dch_Man_t * p )
+{
+    int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3;
+    Abc_Print( 1, "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", 
+        p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax );
+    Abc_Print( 1, "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", 
+        Aig_ManNodeNum(p->pAigTotal), 
+        Aig_ManNodeNum(p->pAigTotal)-nNodeNum,
+        nNodeNum,
+        100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) );
+    Abc_Print( 1, "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", 
+        p->nSatVars, p->nConeMax, p->nRecycles );
+    Abc_Print( 1, "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", 
+        p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, 
+        p->nSatCallsSat, p->nSatFailsReal );
+    Abc_Print( 1, "Choices   : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", 
+        p->nLits, p->nReprs, p->nEquivs, p->nChoices );
+    Abc_Print( 1, "Choicing runtime statistics:\n" );
+    p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice;
+    Abc_PrintTimeP( 1, "Sim init   ", p->timeSimInit,  p->timeTotal );
+    Abc_PrintTimeP( 1, "Sim SAT    ", p->timeSimSat,   p->timeTotal );
+    Abc_PrintTimeP( 1, "SAT solving", p->timeSat,      p->timeTotal );
+    Abc_PrintTimeP( 1, "  sat      ", p->timeSatSat,   p->timeTotal );
+    Abc_PrintTimeP( 1, "  unsat    ", p->timeSatUnsat, p->timeTotal );
+    Abc_PrintTimeP( 1, "  undecided", p->timeSatUndec, p->timeTotal );
+    Abc_PrintTimeP( 1, "Choice     ", p->timeChoice,   p->timeTotal );
+    Abc_PrintTimeP( 1, "Other      ", p->timeOther,    p->timeTotal );
+    Abc_PrintTimeP( 1, "TOTAL      ", p->timeTotal,    p->timeTotal );
+    if ( p->pPars->timeSynth )
+    {
+    Abc_PrintTime( 1, "Synthesis  ", p->pPars->timeSynth );
+    }
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManStop( Dch_Man_t * p )
+{
+    Aig_ManFanoutStop( p->pAigTotal );
+    if ( p->pPars->fVerbose )
+        Dch_ManPrintStats( p );
+    if ( p->pAigFraig )
+        Aig_ManStop( p->pAigFraig );
+    if ( p->ppClasses )
+        Dch_ClassesStop( p->ppClasses );
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    Vec_PtrFree( p->vUsedNodes );
+    Vec_PtrFree( p->vFanins );
+    Vec_PtrFree( p->vSimRoots );
+    Vec_PtrFree( p->vSimClasses );
+    ABC_FREE( p->pReprsProved );
+    ABC_FREE( p->pSatVars );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManSatSolverRecycle( Dch_Man_t * p )
+{
+    int Lit;
+    if ( p->pSat )
+    {
+        Aig_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i )
+            Dch_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 );
+    Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );
+
+    p->nRecycles++;
+    p->nCallsSince = 0;
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c
new file mode 100644
index 00000000..f5e346ef
--- /dev/null
+++ b/src/proof/dch/dchSat.c
@@ -0,0 +1,166 @@
+/**CFile****************************************************************
+
+  FileName    [dchSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+{
+    int nBTLimit = p->pPars->nBTLimit;
+    int pLits[2], RetValue, RetValue1, status, clk;
+    p->nSatCalls++;
+
+    // sanity checks
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    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) )
+        Dch_ManSatSolverRecycle( p );
+
+    // if the nodes do not have SAT variables, allocate them
+    Dch_CnfNodeAddToSolver( p, pOld );
+    Dch_CnfNodeAddToSolver( p, pNew );
+
+    // 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 
+    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
+    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // if the old node was constant 0, we already know the answer
+    if ( pOld == Aig_ManConst1(p->pAigFraig) )
+    {
+        p->nSatProof++;
+        return 1;
+    }
+
+    // solve under assumptions
+    // A = 0; B = 1     OR     A = 0; B = 0 
+    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
+    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
+clk = clock();
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatFailsReal++;
+        return -1;
+    }
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchSim.c b/src/proof/dch/dchSim.c
new file mode 100644
index 00000000..b2d24761
--- /dev/null
+++ b/src/proof/dch/dchSim.c
@@ -0,0 +1,297 @@
+/**CFile****************************************************************
+
+  FileName    [dchSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Performs random simulation at the beginning.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj )
+{ 
+    return (unsigned *)Vec_PtrEntry( vSims, pObj->Id ); 
+}
+static inline unsigned Dch_ObjRandomSim()    
+{ 
+    return Aig_ManRandom(0);               
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node appears to be constant 1 candidate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
+{
+    return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the nodes appear equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Dch_NodeHash( void * p, Aig_Obj_t * pObj )
+{
+    Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned * pSim;
+    unsigned uHash;
+    int k, nWords;
+    nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
+    uHash = 0;
+    pSim  = Dch_ObjSim( vSims, pObj );
+    if ( pObj->fPhase )
+    {
+        for ( k = 0; k < nWords; k++ )
+            uHash ^= ~pSim[k] * s_FPrimes[k & 0x7F];
+    }
+    else
+    {
+        for ( k = 0; k < nWords; k++ )
+            uHash ^= pSim[k] * s_FPrimes[k & 0x7F];
+    }
+    return uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodeIsConst( void * p, Aig_Obj_t * pObj )
+{
+    Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
+    unsigned * pSim;
+    int k, nWords;
+    nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
+    pSim  = Dch_ObjSim( vSims, pObj );
+    if ( pObj->fPhase )
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( ~pSim[k] )
+                return 0;
+    }
+    else
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( pSim[k] )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodesAreEqual( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
+    unsigned * pSim0, * pSim1;
+    int k, nWords;
+    nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
+    pSim0 = Dch_ObjSim( vSims, pObj0 );
+    pSim1 = Dch_ObjSim( vSims, pObj1 );
+    if ( pObj0->fPhase != pObj1->fPhase )
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( pSim0[k] != ~pSim1[k] )
+                return 0;
+    }
+    else
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( pSim0[k] != pSim1[k] )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims )
+{
+    unsigned * pSim, * pSim0, * pSim1;
+    Aig_Obj_t * pObj;
+    int i, k, nWords;
+    nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
+
+    // assign const 1 sim info
+    pObj = Aig_ManConst1(pAig);
+    pSim = Dch_ObjSim( vSims, pObj );
+    memset( pSim, 0xff, sizeof(unsigned) * nWords );
+
+    // assign primary input random sim info
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        pSim = Dch_ObjSim( vSims, pObj );
+        for ( k = 0; k < nWords; k++ )
+            pSim[k] = Dch_ObjRandomSim();
+        pSim[0] <<= 1;
+    }
+
+    // simulate AIG in the topological order
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) ); 
+        pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) ); 
+        pSim  = Dch_ObjSim( vSims, pObj );
+
+        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & ~pSim1[k];
+        }
+        else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & pSim1[k];
+        }
+        else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & ~pSim1[k];
+        }
+        else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & pSim1[k];
+        }
+    }
+    // get simulation information for primary outputs
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives candidate equivalence classes of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose )
+{
+    Dch_Cla_t * pClasses;
+    Vec_Ptr_t * vSims;
+    int i;
+    // allocate simulation information
+    vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
+    // run random simulation from the primary inputs
+    Dch_PerformRandomSimulation( pAig, vSims );
+    // start storage for equivalence classes
+    pClasses = Dch_ClassesStart( pAig );
+    Dch_ClassesSetData( pClasses, vSims, Dch_NodeHash, Dch_NodeIsConst, Dch_NodesAreEqual );
+    // hash nodes by sim info
+    Dch_ClassesPrepare( pClasses, 0, 0 );
+    // iterate random simulation
+    for ( i = 0; i < 7; i++ )
+    {
+        Dch_PerformRandomSimulation( pAig, vSims );
+        Dch_ClassesRefine( pClasses );
+    }
+    // clean up and return
+    Vec_PtrFree( vSims );
+    // prepare class refinement procedures
+    Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
+    return pClasses;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
new file mode 100644
index 00000000..808e754a
--- /dev/null
+++ b/src/proof/dch/dchSimSat.c
@@ -0,0 +1,258 @@
+/**CFile****************************************************************
+
+  FileName    [dchSimSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Performs resimulation using counter-examples.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the reverse DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanout, * pRepr;
+    int iFanout = -1, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    // traverse the fanouts
+    Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
+        Dch_ManCollectTfoCands_rec( p, pFanout );
+    // check if the given node has a representative
+    pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
+    if ( pRepr == NULL )
+        return;
+    // pRepr is the constant 1 node
+    if ( pRepr == Aig_ManConst1(p->pAigTotal) )
+    {
+        Vec_PtrPush( p->vSimRoots, pObj );
+        return;
+    }
+    // pRepr is the representative of an equivalence class
+    if ( pRepr->fMarkA )
+        return;
+    pRepr->fMarkA = 1;
+    Vec_PtrPush( p->vSimClasses, pRepr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect equivalence classes and const1 cands in the TFO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( p->vSimRoots );
+    Vec_PtrClear( p->vSimClasses );
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );    
+    Dch_ManCollectTfoCands_rec( p, pObj1 );
+    Dch_ManCollectTfoCands_rec( p, pObj2 );
+    Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
+    Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
+        pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the solved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Aig_Obj_t * pObjFraig;
+        int nVarNum;
+        pObjFraig = Dch_ObjFraig( pObj );
+        assert( !Aig_IsComplement(pObjFraig) );
+        nVarNum = Dch_ObjSatNum( p, pObjFraig );
+        // get the value from the SAT solver
+        // (account for the fact that some vars may be minimized away)
+        pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+//        pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
+        return;
+    }
+    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+    // count the cone size
+    if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
+        p->nConeThis++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the other nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        // set random value
+        pObj->fMarkB = Aig_ManRandom(0) & 1;
+        return;
+    }
+    Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pRoot, ** ppClass;
+    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    // get the equivalence classes
+    Dch_ManCollectTfoCands( p, pObj, pRepr );
+    // resimulate the cone of influence of the solved nodes
+    p->nConeThis = 0;
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+    Dch_ManResimulateSolved_rec( p, pObj );
+    Dch_ManResimulateSolved_rec( p, pRepr );
+    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
+    // resimulate the cone of influence of the other nodes
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
+        Dch_ManResimulateOther_rec( p, pRoot );
+    // refine these nodes
+    RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+    // resimulate the cone of influence of the cand classes
+    RetValue2 = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
+    {
+        ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
+        for ( k = 0; k < nSize; k++ )
+            Dch_ManResimulateOther_rec( p, ppClass[k] );
+        // refine this class
+        RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
+    }
+    // make sure refinement happened
+    if ( Aig_ObjIsConst1(pRepr) )
+        assert( RetValue1 );
+    else
+        assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pRoot;
+    int i, RetValue, clk = clock();
+    // get the equivalence class
+    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
+    else
+        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
+    // resimulate the cone of influence of the solved nodes
+    p->nConeThis = 0;
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+    Dch_ManResimulateSolved_rec( p, pObj );
+    Dch_ManResimulateSolved_rec( p, pRepr );
+    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
+    // resimulate the cone of influence of the other nodes
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
+        Dch_ManResimulateOther_rec( p, pRoot );
+    // refine this class
+    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+    else
+        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
+    assert( RetValue );
+p->timeSimSat += clock() - clk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/dchSweep.c b/src/proof/dch/dchSweep.c
new file mode 100644
index 00000000..a1c4f79b
--- /dev/null
+++ b/src/proof/dch/dchSweep.c
@@ -0,0 +1,146 @@
+/**CFile****************************************************************
+
+  FileName    [dchSweep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [One round of SAT sweeping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+#include "src/misc/bar/bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
+{ 
+    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
+    int RetValue;
+    // get representative of this class
+    pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj );
+    if ( pObjRepr == NULL )
+        return;
+    // get the fraiged node
+    pObjFraig = Dch_ObjFraig( pObj );
+    if ( pObjFraig == NULL )
+        return;
+    // get the fraiged representative
+    pObjReprFraig = Dch_ObjFraig( pObjRepr );
+    if ( pObjReprFraig == NULL )
+        return;
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+    {
+        // remember the proved equivalence
+        p->pReprsProved[ pObj->Id ] = pObjRepr;
+        return;
+    }
+    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
+    RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+    if ( RetValue == -1 ) // timed out
+    {
+        Dch_ObjSetFraig( pObj, NULL );
+        return;
+    }
+    if ( RetValue == 1 )  // proved equivalent
+    {
+        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        Dch_ObjSetFraig( pObj, pObjFraig2 );
+        // remember the proved equivalence
+        p->pReprsProved[ pObj->Id ] = pObjRepr;
+        return;
+    }
+    // disproved the equivalence
+    if ( p->pPars->fSimulateTfo )
+        Dch_ManResimulateCex( p, pObj, pObjRepr );
+    else
+        Dch_ManResimulateCex2( p, pObj, pObjRepr );
+    assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManSweep( Dch_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    // map constants and PIs
+    p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
+    Aig_ManCleanData( p->pAigTotal );
+    Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
+    Aig_ManForEachPi( p->pAigTotal, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
+    // sweep internal nodes
+    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
+    Aig_ManForEachNode( p->pAigTotal, pObj, i )
+    {
+        Bar_ProgressUpdate( pProgress, i, NULL );
+        if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL || 
+             Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
+            continue;
+        pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
+        if ( pObjNew == NULL )
+            continue;
+        Dch_ObjSetFraig( pObj, pObjNew );
+        Dch_ManSweepNode( p, pObj );
+    }
+    Bar_ProgressStop( pProgress );
+    // update the representatives of the nodes (makes classes invalid)
+    ABC_FREE( p->pAigTotal->pReprs );
+    p->pAigTotal->pReprs = p->pReprsProved;
+    p->pReprsProved = NULL;
+    // clean the mark
+    Aig_ManCleanMarkB( p->pAigTotal );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/dch/module.make b/src/proof/dch/module.make
new file mode 100644
index 00000000..11163cef
--- /dev/null
+++ b/src/proof/dch/module.make
@@ -0,0 +1,10 @@
+SRC +=    src/proof/dch/dchAig.c \
+    src/proof/dch/dchChoice.c \
+    src/proof/dch/dchClass.c \
+    src/proof/dch/dchCnf.c \
+    src/proof/dch/dchCore.c \
+    src/proof/dch/dchMan.c \
+    src/proof/dch/dchSat.c \
+    src/proof/dch/dchSim.c \
+    src/proof/dch/dchSimSat.c \
+    src/proof/dch/dchSweep.c