From bfe7333f4105442a7df530c68ed1cf1b7da7edda Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 21 Jul 2016 16:40:56 -0700
Subject: Adding new command 'dump_equiv'.

---
 src/proof/cec/cec.h      |  1 +
 src/proof/cec/cecCore.c  | 10 ++++++++--
 src/proof/cec/cecInt.h   |  2 +-
 src/proof/cec/cecSolve.c | 12 +++++++++++-
 4 files changed, 21 insertions(+), 4 deletions(-)

(limited to 'src/proof')

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 )
         {
-- 
cgit v1.2.3