Adding new command 'dump_equiv'.

12 files changed, 514 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f2baf7e0..3d2d84ae 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -175,6 +175,8 @@ struct Gia_Man_t_
     Vec_Int_t *    vUserFfIds;    // numbers assigned to FFs by the user
     Vec_Int_t *    vCiNumsOrig;   // original CI names
     Vec_Int_t *    vCoNumsOrig;   // original CO names
+    Vec_Int_t *    vIdsOrig;      // original object IDs
+    Vec_Int_t *    vIdsEquiv;     // original object IDs proved equivalent
     Vec_Int_t *    vCofVars;      // cofactoring variables
     Vec_Vec_t *    vClockDoms;    // clock domains
     Vec_Flt_t *    vTiming;       // arrival/required/slack
@@ -1241,6 +1243,10 @@ extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
 extern Gia_Man_t *         Gia_ManRemoveEnables( Gia_Man_t * p );
 /*=== giaEquiv.c ==========================================================*/
+extern void                Gia_ManOrigIdsInit( Gia_Man_t * p );
+extern void                Gia_ManOrigIdsStart( Gia_Man_t * p );
+extern void                Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
+extern Gia_Man_t *         Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
 extern void                Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b5fd393e..7ced54a4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1383,7 +1383,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     pNew->nConstrs = p->nConstrs;
     if ( p->pCexSeq )
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index d383ce41..584be4cd 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -34,6 +34,143 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Manipulating original IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManOrigIdsInit( Gia_Man_t * p )
+{
+    Vec_IntFreeP( &p->vIdsOrig );
+    p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) );
+}
+void Gia_ManOrigIdsStart( Gia_Man_t * p )
+{
+    Vec_IntFreeP( &p->vIdsOrig );
+    p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) );
+}
+void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew )
+{
+    Gia_Obj_t * pObj; int i;
+    if ( p->vIdsOrig == NULL )
+        return;
+    Gia_ManOrigIdsStart( pNew );
+    Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 );
+    Gia_ManForEachObj1( p, pObj, i )
+        if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 )
+            Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) );
+    Gia_ManForEachObj( pNew, pObj, i )
+        assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 );
+}
+// input is a set of equivalent node pairs in any order
+// output is the mapping of each node into the equiv node with the smallest ID
+void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two )
+{
+    int Smo = One < Two ? One : Two;
+    int Big = One < Two ? Two : One;
+    assert( Smo != Big );
+    if ( Vec_IntEntry(vMap, Big) == -1 )
+        Vec_IntWriteEntry( vMap, Big, Smo );
+    else
+        Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) );
+}
+int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One )
+{
+    if ( Vec_IntEntry(vMap, One) == -1 )
+        return One;
+    return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) );
+}
+Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs )
+{
+    Vec_Int_t * vMapResult;
+    Vec_Int_t * vMap2Smaller;
+    int i, One, Two;
+    // map bigger into smaller one
+    vMap2Smaller = Vec_IntStartFull( nObjs );
+    Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i )
+        Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two );
+    // collect results in the topo order
+    vMapResult = Vec_IntStartFull( nObjs );
+    Vec_IntForEachEntry( vMap2Smaller, One, i )
+        if ( One >= 0 )
+            Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) );
+    Vec_IntFree( vMap2Smaller );
+    return vMapResult;
+}
+// remap the AIG using the equivalent pairs proved
+// returns the reduced AIG and the equivalence classes of the original AIG
+Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+    Gia_Man_t * pNew = NULL;
+    Gia_Obj_t * pObj, * pRepr; int i;
+    Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManFillValue(p);
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Vec_IntEntry(vMap, i) == -1 )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
+        {
+            pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) );
+            pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
+        }
+    }
+    Gia_ManHashStop( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Vec_IntFree( vMap );
+    // compute equivalences
+    assert( !p->pReprs && !p->pNexts );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    Gia_ManFillValue(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        int iRepr = Abc_Lit2Var(pObj->Value);
+        if ( iRepr == 0 )
+        {
+            Gia_ObjSetRepr( p, i, 0 );
+            continue;
+        }
+        pRepr = Gia_ManObj( pNew, iRepr );
+        if ( !~pRepr->Value ) // first time
+        {
+            pRepr->Value = i;
+            continue;
+        }
+        // add equivalence
+        Gia_ObjSetRepr( p, i, pRepr->Value );
+    }
+    p->pNexts = Gia_ManDeriveNexts( p );
+    return pNew;
+}
+Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+    Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs );
+    Gia_ManPrintStats( p, NULL );
+    Gia_ManPrintStats( pNew, NULL );
+    //Gia_ManStop( pNew );
+    // cleanup the resulting one
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if AIG is not in the required topo order.]
 
   Description []
@@ -460,7 +597,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
@@ -641,6 +778,7 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
     pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
     if ( pNew == NULL )
         return NULL;
+    Gia_ManOrigIdsRemap( p, pNew );
     if ( fMiterPairs )
         Gia_ManEquivFixOutputPairs( pNew );
     if ( fSeq )
@@ -649,9 +787,11 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
         Gia_ManCombMarkUsed( pNew );
     Gia_ManEquivUpdatePointers( p, pNew );
     pFinal = Gia_ManDupMarked( pNew );
+    Gia_ManOrigIdsRemap( pNew, pFinal );
     Gia_ManEquivDeriveReprs( p, pNew, pFinal );
     Gia_ManStop( pNew );
     pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
+    Gia_ManOrigIdsRemap( pNew, pFinal );
     Gia_ManStop( pNew );
     return pFinal;
 }
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index d9e878a7..9ccab495 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -93,6 +93,8 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_FltFreeP( &p->vTiming );
     Vec_VecFreeP( &p->vClockDoms );
     Vec_IntFreeP( &p->vCofVars );
+    Vec_IntFreeP( &p->vIdsOrig );
+    Vec_IntFreeP( &p->vIdsEquiv );
     Vec_IntFreeP( &p->vLutConfigs );
     Vec_IntFreeP( &p->vEdgeDelay );
     Vec_IntFreeP( &p->vEdgeDelayR );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index b44a272a..5d0261d7 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -980,7 +980,7 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
     Vec_Int_t * vMapping = NULL;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode, * pFanin;
-    int i, k, nObjs;
+    int i, k, nObjs, iGiaObj;
     assert( Abc_NtkIsAigLogic(p) );
     pHopMan = (Hop_Man_t *)p->pManFunc;
     // create new manager
@@ -1016,15 +1016,14 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
         {
             assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
             Abc_ConvertAigToGia( pNew, pHopObj );
-            if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) )
-                continue;
-            if ( vMapping && !Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) )
+            iGiaObj = Abc_Lit2Var( pHopObj->iData );
+            if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) )
             {
-                Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) );
+                Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) );
                 Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
                 Abc_ObjForEachFanin( pNode, pFanin, k )
                     Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp)  );
-                Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) );
+                Vec_IntPush( vMapping, iGiaObj );
             }
         }
         pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ebd6c368..f19f8449 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -233,6 +233,7 @@ static int Abc_CommandFraigRestore           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandFraigClean             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigSweep             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigDress             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDumpEquiv              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRecStart3              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecStop3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -869,6 +870,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Abc_CommandFraigClean,       0 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "dress",         Abc_CommandFraigDress,       1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "dump_equiv",    Abc_CommandDumpEquiv,        0 );
 
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_start3",    Abc_CommandRecStart3,        0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop3",     Abc_CommandRecStop3,         0 );
@@ -14812,6 +14814,81 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose );
+    FILE * pFile = NULL;
+    Abc_Ntk_t * pNtks[2] = {NULL};
+    char * pFileName[2], * pFileNameOut;
+    int c, nConfs = 1000, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfs < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 3 )
+    {
+        Abc_Print( -1, "Expecting three file names on the command line.\n" );
+        goto usage;
+    }
+    pFileName[0] = argv[globalUtilOptind];
+    pFileName[1] = argv[globalUtilOptind+1];
+    pFileNameOut = argv[globalUtilOptind+2];
+    for ( c = 0; c < 2; c++ )
+    {
+        pNtks[c] = Io_Read( pFileName[c], Io_ReadFileType(pFileName[c]), 1, 0 );
+        if ( pNtks[c] == NULL )
+            goto usage;
+        Abc_NtkToAig( pNtks[c] );
+    }
+    Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fVerbose );
+    Abc_NtkDelete( pNtks[0] );
+    Abc_NtkDelete( pNtks[1] );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: dump_equiv [-C num] [-vh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
+    Abc_Print( -2, "\t          computes equivalence classes of nodes in <file1> and <file2>\n" );
+    Abc_Print( -2, "\t-C num  : the maximum number of conflicts at each node [default = %d]\n", nConfs );
+    Abc_Print( -2, "\t-v      : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h      : print the command usage\n");
+    Abc_Print( -2, "\t<file1> : first network whose nodes are considered\n" );
+    Abc_Print( -2, "\t<file2> : second network whose nodes are considered\n" );
+    Abc_Print( -2, "\t<file_dump_equiv> : text file with node equivalence classes\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char * FileName, * pTemp;
@@ -27022,7 +27099,7 @@ usage:
     Abc_Print( -2, "\t         converts the current network into GIA and moves it to the &-space\n" );
     Abc_Print( -2, "\t         (if the network is a sequential logic network, normalizes the flops\n" );
     Abc_Print( -2, "\t         to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
-    Abc_Print( -2, "\t-c     : toggles allowing simple GIA to be improved [default = %s]\n", fGiaSimple? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
new file mode 100644
index 00000000..ee7eb8e3
--- /dev/null
+++ b/src/base/abci/abcDress3.c
@@ -0,0 +1,259 @@
+/**CFile****************************************************************
+
+  FileName    [abcDress3.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Transfers names from one netlist to the other.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDress3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/io/ioAbc.h"
+#include "proof/cec/cec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Compute equivalence classes of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
+{
+    Gia_Man_t * pTemp;
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec_ManFraSetDefaultParams( pPars );
+    pPars->fUseOrigIds = 1;
+    pPars->fSatSweeping = 1;
+    pPars->nBTLimit = nConfs;
+    pPars->fVerbose = fVerbose;
+    pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
+    Gia_ManStop( pTemp );
+    pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
+    Gia_ManStop( pTemp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add logic from pNtk to the AIG manager p.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
+{
+    extern int Abc_ConvertAigToGia( Gia_Man_t * p, Hop_Obj_t * pRoot );
+    Hop_Man_t * pHopMan;
+    Hop_Obj_t * pHopObj;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode, * pFanin;
+    int i, k;
+    assert( Abc_NtkIsAigLogic(pNtk) );
+    pHopMan = (Hop_Man_t *)pNtk->pManFunc;
+    Hop_ManConst1(pHopMan)->iData = 1;
+    // image primary inputs
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->iTemp = Gia_ManCiLit(p, i);
+    // iterate through nodes used in the mapping
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
+        pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
+        assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
+        if ( Hop_DagSize(pHopObj) > 0 )
+            Abc_ConvertAigToGia( p, pHopObj );
+        pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
+    }
+    Vec_PtrFree( vNodes );
+    // create primary outputs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp );
+}
+Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    Gia_Man_t * p;
+    Gia_Obj_t * pObj;
+    Abc_Obj_t * pNode;
+    int i;
+    assert( Abc_NtkIsAigLogic(pNtk1) );
+    assert( Abc_NtkIsAigLogic(pNtk2) );
+    // create new manager
+    p = Gia_ManStart( 10000 );
+    p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) );
+    p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) );
+    Abc_NtkForEachCi( pNtk1, pNode, i )
+        Gia_ManAppendCi(p);
+    // add logic
+    Gia_ManHashAlloc( p );
+    Abc_NtkAigToGiaOne( p, pNtk1 );
+    Abc_NtkAigToGiaOne( p, pNtk2 );
+    Gia_ManHashStop( p );
+    // add extra POs to dangling nodes
+    Gia_ManCreateValueRefs( p );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( pObj->Value == 0 )
+            Gia_ManAppendCo( p, Abc_Var2Lit(i, 0) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect equivalence class information.]
+
+  Description [Each class is represented as follows: 
+      <num_entries><entry1><entry2>...<entryN> 
+  where <entry> is nodeId with 1-bit for complement and 1-bit for network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_NtkCollectAddOne( int iNtk, int iObj, int iGiaLit, Gia_Man_t * pGia, Vec_Int_t * vGia2Cla, Vec_Int_t * vNexts[2] )
+{
+    int iRepr = Gia_ObjReprSelf( pGia, Abc_Lit2Var(iGiaLit) );
+    int Compl = Abc_LitIsCompl(iGiaLit) ^ Gia_ObjPhase(Gia_ManObj(pGia, iRepr)) ^ Gia_ObjPhase(Gia_ManObj(pGia, Abc_Lit2Var(iGiaLit)));
+    int Added = Abc_Var2Lit( Abc_Var2Lit(iObj, Compl), iNtk );
+    int Entry = Vec_IntEntry( vGia2Cla, iRepr );
+    Vec_IntWriteEntry( vNexts[iNtk], iObj, Entry );
+    Vec_IntWriteEntry( vGia2Cla, iRepr, Added );
+}
+Vec_Int_t * Abc_NtkCollectEquivClasses( Abc_Ntk_t * pNtks[2], Gia_Man_t * pGia )
+{
+    Vec_Int_t * vClass = Vec_IntAlloc( 100 );
+    Vec_Int_t * vClasses = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vGia2Cla = Vec_IntStartFull( Gia_ManObjNum(pGia) ); // mapping objId into classId
+    Vec_Int_t * vNexts[2] = { Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[0])), Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[1])) };
+    Abc_Obj_t * pObj;
+    int n, i, k, Entry, fCompl;
+    Abc_NtkForEachCi( pNtks[0], pObj, i )
+        Abc_NtkCollectAddOne( 0, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+    for ( n = 0; n < 2; n++ )
+        Abc_NtkForEachNode( pNtks[n], pObj, i )
+            Abc_NtkCollectAddOne( n, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+    Vec_IntForEachEntry( vGia2Cla, Entry, i )
+    {
+        Vec_IntClear( vClass );
+        for ( ; Entry >= 0; Entry = Vec_IntEntry(vNexts[Entry&1], Entry>>2) )
+            Vec_IntPush( vClass, Entry );
+        if ( Vec_IntSize(vClass) < 2 )
+            continue;
+        Vec_IntReverseOrder( vClass );
+        fCompl = 2 & Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntry( vClass, Entry, k )
+            Vec_IntWriteEntry( vClass, k, Entry ^ fCompl );        
+        Vec_IntPush( vClasses, Vec_IntSize(vClass) );
+        Vec_IntAppend( vClasses, vClass );
+    }
+    Vec_IntFree( vGia2Cla );
+    Vec_IntFree( vNexts[0] );
+    Vec_IntFree( vNexts[1] );
+    Vec_IntFree( vClass );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the output file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * pNtks[2] )
+{
+    int i, c, k, Entry;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) { printf( "Cannot open file %s for writing.\n", pFileName ); return; }
+    fprintf( pFile, "# Node equivalences computed by ABC for networks \"%s\" and \"%s\" on %s\n\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), Extra_TimeStamp() );
+    for ( i = c = 0; i < Vec_IntSize(vClasses); c++, i += 1 + Vec_IntEntry(vClasses, i) )
+    {
+        Vec_IntForEachEntryStartStop( vClasses, Entry, k, i + 1, i + 1 + Vec_IntEntry(vClasses, i) )
+        {
+            Abc_Ntk_t * pNtk = pNtks[Entry & 1];
+            char * pObjName = Abc_ObjName( Abc_NtkObj(pNtk, Entry>>2) );
+            fprintf( pFile, "%d:%s:%s%s\n", c+1, Abc_NtkName(pNtk), (Entry&2) ? "NOT:":"", pObjName );
+        }
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compute and dump equivalent name classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose )
+{
+    //abctime clk = Abc_Clock();
+    Vec_Int_t * vClasses;
+    // derive shared AIG for the two networks
+    Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1] );
+    if ( fVerbose )
+        printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
+    // compute equivalences in this AIG
+    Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
+    //if ( fVerbose )
+    //    Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
+    if ( fVerbose )
+        Gia_ManPrintStats( pGia, NULL );
+    // collect equivalence class information
+    vClasses = Abc_NtkCollectEquivClasses( pNtks, pGia );
+    Gia_ManStop( pGia );
+    // dump information into the output file
+    Abc_NtkDumpEquivFile( pFileName, vClasses, pNtks );
+    Vec_IntFree( vClasses );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 492fc62a..b97f526f 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDetect.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDress2.c \
+    src/base/abci/abcDress3.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcExact.c \
     src/base/abci/abcExtract.c \
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index a0b92b52..e8b243d3 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -108,6 +108,7 @@ struct Cec_ParFra_t_
     int              fColorDiff;    // miter with separate outputs
     int              fSatSweeping;  // enable SAT sweeping
     int              fRunCSat;      // enable another solver
+    int              fUseOrigIds;   // enable recording of original IDs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the failed output
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c9e9f67a..ed5c4ab7 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -236,7 +236,7 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     Gia_Man_t * pNew;
     Cec_ManPat_t * pPat;
     pPat = Cec_ManPatStart();
-    Cec_ManSatSolve( pPat, pAig, pPars );
+    Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
 //    pNew = Gia_ManDupDfsSkip( pAig );
     pNew = Gia_ManDup( pAig );
     Cec_ManPatStop( pPat );
@@ -351,6 +351,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
     pIni = Gia_ManDup(pAig);
     pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
     pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
+    if ( pPars->fUseOrigIds )
+    {
+        Gia_ManOrigIdsInit( pIni );
+        Vec_IntFreeP( &pAig->vIdsEquiv );
+        pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
+    }
 
     // prepare the managers
     // SAT sweeping
@@ -429,7 +435,7 @@ clk = Abc_Clock();
         if ( pPars->fRunCSat )
             Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); 
         else
-            Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
+            Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); 
 p->timeSat += Abc_Clock() - clk;
         if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
         {
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index ef1dd983..d93e5e86 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -201,7 +201,7 @@ extern int                  Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
 extern int                  Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
-extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
 extern void                 Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
 extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index e3db0b93..f75914e4 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -673,7 +673,7 @@ p->timeSatUndec += Abc_Clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
 {
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
@@ -706,6 +706,16 @@ clk2 = Abc_Clock();
         status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
+        if ( status == 1 && vIdsOrig )
+        {
+            int iObj1 = Vec_IntEntry(vMiterPairs, 2*i);
+            int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1);
+            int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1);
+            int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2);
+            assert( OrigId1 >= 0 && OrigId2 >= 0 );
+            Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
+        }
+
 /*
         if ( status == -1 )
         {