Version abc90807

committer: Baruch Sterin <baruchs@gmail.com>

2 files changed, 42 insertions, 0 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 7f445970..199d6939 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -135,6 +135,7 @@ struct Cec_ParCor_t_
     int              fUseCSat;      // use circuit-based solver
 //    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
+    int              fVerboseFlops; // verbose stats
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 96c45907..27a7dd36 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -990,6 +990,39 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints flop equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    assert( p->vNamesIn != NULL );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
+            printf( "Flop \"%s\" is equivalent to constant 0.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
+        else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+        {
+            if ( Gia_ObjIsCi(pRepr) )
+                printf( "Flop \"%s\" is equivalent to flop \"%s\".\n", 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj)  ), 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
+            else
+                printf( "Flop \"%s\" is equivalent to internal node %d.\n", 
+                    Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Top-level procedure for register correspondence.]
 
   Description []
@@ -1060,6 +1093,14 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     }
     if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
         printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
+    // print verbose info about equivalences
+    if ( pPars->fVerboseFlops )
+    {
+        if ( pAig->vNamesIn == NULL )
+            printf( "Flop output names are not available. Use command \"&get -n\".\n" );
+        else
+            Cec_ManPrintFlopEquivs( pAig );
+    }
     return pNew;
 }