From 67e84b719d02fe65bf9fee61f27fbd7c12da4003 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 25 Jul 2011 20:33:55 +0700
Subject: Enhancing printing of counter-examples.

---
 src/misc/util/utilCex.c | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

(limited to 'src/misc/util/utilCex.c')

diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 69cd37cf..72989535 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -174,6 +174,31 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
     return pCex;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints out the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_CexPrintStats( Abc_Cex_t * p )
+{
+    int k, Counter = 0;
+    if ( p == NULL )
+    {
+        printf( "The counter example is NULL.\n" );
+        return;
+    }
+    for ( k = 0; k < p->nBits; k++ )
+        Counter += Abc_InfoHasBit(p->pData, k);
+    printf( "CEX: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d  nOnes = %5d (%5.2f %%)\n", 
+        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / p->nBits );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Prints out the counter-example.]
@@ -188,15 +213,19 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
 void Abc_CexPrint( Abc_Cex_t * p )
 {
     int i, f, k;
-    printf( "Counter-example: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d\n", 
-        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
+    if ( p == NULL )
+    {
+        printf( "The counter example is NULL.\n" );
+        return;
+    }
+    Abc_CexPrintStats( p );
     printf( "State    : " );
     for ( k = 0; k < p->nRegs; k++ )
         printf( "%d", Abc_InfoHasBit(p->pData, k) );
     printf( "\n" );
     for ( f = 0; f <= p->iFrame; f++ )
     {
-        printf( "Frame %2d : ", f );
+        printf( "Frame %3d : ", f );
         for ( i = 0; i < p->nPis; i++ )
             printf( "%d", Abc_InfoHasBit(p->pData, k++) );
         printf( "\n" );
-- 
cgit v1.2.3